%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : CSR089+4 : TPTP v9.3.1. Bugfixed v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n012.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 09:45:07 AM UTC 2026
% Result : Theorem 106.52s 26.39s
% Output : Refutation 183.87s
% Verified :
% SZS Type : Refutation
% Derivation depth : 20
% Number of leaves : 19
% Syntax : Number of formulae : 105 ( 29 unt; 3 def)
% Number of atoms : 283 ( 0 equ)
% Maximal formula atoms : 5 ( 2 avg)
% Number of connectives : 327 ( 149 ~; 142 |; 14 &)
% ( 6 <=>; 16 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 4 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 11 ( 10 usr; 4 prp; 0-3 aty)
% Number of functors : 9 ( 9 usr; 9 con; 0-0 aty)
% Number of variables : 83 ( 0 sgn 80 !; 3 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f26,axiom,
! [X0,X1] :
( s__subclass(X0,X1)
=> ( s__instance(X0,s__SetOrClass)
& s__instance(X1,s__SetOrClass) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR003+0.ax',kb_SUMO_26) ).
fof(f27,axiom,
! [X1,X0,X2] :
( ( s__instance(X1,s__SetOrClass)
& s__instance(X0,s__SetOrClass) )
=> ( ( s__instance(X2,X0)
& s__subclass(X0,X1) )
=> s__instance(X2,X1) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR003+0.ax',kb_SUMO_27) ).
fof(f55,axiom,
! [X1,X0] :
( ( s__instance(X0,s__EngineeringComponent)
& s__instance(X1,s__EngineeringComponent) )
=> ( s__connectedEngineeringComponents(X0,X1)
=> s__connected(X0,X1) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR003+0.ax',kb_SUMO_55) ).
fof(f1138,axiom,
! [X1,X0] :
( ( s__instance(X1,s__Object)
& s__instance(X0,s__Object) )
=> ( s__connected(X0,X1)
=> s__connected(X1,X0) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR003+0.ax',kb_SUMO_1141) ).
fof(f1140,axiom,
! [X0,X1] :
( ( s__instance(X1,s__EngineeringComponent)
& s__instance(X0,s__EngineeringComponent) )
=> ( s__connectedEngineeringComponents(X0,X1)
=> s__connectedEngineeringComponents(X1,X0) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR003+0.ax',kb_SUMO_1143) ).
fof(f4643,axiom,
! [X1,X0] :
( ( s__instance(X1,s__Object)
& s__instance(X0,s__Object) )
=> ( s__connected(X0,X1)
=> ( s__meetsSpatially(X0,X1)
| s__overlapsSpatially(X0,X1) ) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR003+0.ax',kb_SUMO_4658) ).
fof(f6310,axiom,
s__subclass(s__Artifact,s__Object),
file('/export/starexec/sandbox/benchmark/Axioms/CSR003+0.ax',kb_SUMO_6388) ).
fof(f6387,axiom,
s__subclass(s__Device,s__Artifact),
file('/export/starexec/sandbox/benchmark/Axioms/CSR003+0.ax',kb_SUMO_6466) ).
fof(f6420,axiom,
s__subclass(s__EngineeringComponent,s__Device),
file('/export/starexec/sandbox/benchmark/Axioms/CSR003+0.ax',kb_SUMO_6501) ).
fof(f6441,axiom,
! [X0,X1] :
( ( s__instance(X0,s__EngineeringComponent)
& s__instance(X1,s__EngineeringComponent) )
=> ( s__connectedEngineeringComponents(X1,X0)
<=> ? [X2] :
( s__instance(X2,s__EngineeringConnection)
& s__connectsEngineeringComponents(X2,X1,X0) ) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR003+0.ax',kb_SUMO_6522) ).
fof(f7218,axiom,
s__instance(s__Object16_1,s__EngineeringConnection),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',local_1) ).
fof(f7219,axiom,
s__instance(s__Object16_2,s__EngineeringComponent),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',local_2) ).
fof(f7220,axiom,
s__instance(s__Object16_3,s__EngineeringComponent),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',local_3) ).
fof(f7221,axiom,
s__connectsEngineeringComponents(s__Object16_1,s__Object16_2,s__Object16_3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',local_4) ).
fof(f7222,axiom,
~ s__overlapsSpatially(s__Object16_2,s__Object16_3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',local_5) ).
fof(f7223,conjecture,
s__meetsSpatially(s__Object16_2,s__Object16_3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_from_SUMO) ).
fof(f7224,negated_conjecture,
~ s__meetsSpatially(s__Object16_2,s__Object16_3),
inference(negated_conjecture,[status(cth)],[f7223]) ).
fof(f7547,plain,
! [X0,X1] :
( ( s__instance(X0,s__Object)
& s__instance(X1,s__Object) )
=> ( s__connected(X1,X0)
=> s__connected(X0,X1) ) ),
inference(rectify,[],[f1138]) ).
fof(f8342,plain,
! [X0,X1] :
( ( s__instance(X1,s__EngineeringComponent)
& s__instance(X0,s__EngineeringComponent) )
=> ( s__connectedEngineeringComponents(X1,X0)
=> s__connected(X1,X0) ) ),
inference(rectify,[],[f55]) ).
fof(f8413,plain,
~ s__meetsSpatially(s__Object16_2,s__Object16_3),
inference(flattening,[],[f7224]) ).
fof(f8844,plain,
! [X1,X0] :
( s__meetsSpatially(X0,X1)
| s__overlapsSpatially(X0,X1)
| ~ s__connected(X0,X1)
| ~ s__instance(X1,s__Object)
| ~ s__instance(X0,s__Object) ),
inference(ennf_transformation,[],[f4643]) ).
fof(f8845,plain,
! [X0,X1] :
( s__meetsSpatially(X0,X1)
| ~ s__instance(X1,s__Object)
| ~ s__connected(X0,X1)
| s__overlapsSpatially(X0,X1)
| ~ s__instance(X0,s__Object) ),
inference(flattening,[],[f8844]) ).
fof(f8931,plain,
! [X0,X1] :
( s__connectedEngineeringComponents(X1,X0)
| ~ s__connectedEngineeringComponents(X0,X1)
| ~ s__instance(X1,s__EngineeringComponent)
| ~ s__instance(X0,s__EngineeringComponent) ),
inference(ennf_transformation,[],[f1140]) ).
fof(f8932,plain,
! [X1,X0] :
( s__connectedEngineeringComponents(X1,X0)
| ~ s__connectedEngineeringComponents(X0,X1)
| ~ s__instance(X1,s__EngineeringComponent)
| ~ s__instance(X0,s__EngineeringComponent) ),
inference(flattening,[],[f8931]) ).
fof(f9793,plain,
! [X0,X1] :
( s__connected(X1,X0)
| ~ s__connectedEngineeringComponents(X1,X0)
| ~ s__instance(X1,s__EngineeringComponent)
| ~ s__instance(X0,s__EngineeringComponent) ),
inference(ennf_transformation,[],[f8342]) ).
fof(f9794,plain,
! [X1,X0] :
( s__connected(X1,X0)
| ~ s__instance(X0,s__EngineeringComponent)
| ~ s__connectedEngineeringComponents(X1,X0)
| ~ s__instance(X1,s__EngineeringComponent) ),
inference(flattening,[],[f9793]) ).
fof(f10249,plain,
! [X1,X0,X2] :
( s__instance(X2,X1)
| ~ s__instance(X2,X0)
| ~ s__subclass(X0,X1)
| ~ s__instance(X1,s__SetOrClass)
| ~ s__instance(X0,s__SetOrClass) ),
inference(ennf_transformation,[],[f27]) ).
fof(f10250,plain,
! [X2,X1,X0] :
( ~ s__instance(X2,X0)
| s__instance(X2,X1)
| ~ s__instance(X1,s__SetOrClass)
| ~ s__instance(X0,s__SetOrClass)
| ~ s__subclass(X0,X1) ),
inference(flattening,[],[f10249]) ).
fof(f11894,plain,
! [X0,X1] :
( s__connected(X0,X1)
| ~ s__connected(X1,X0)
| ~ s__instance(X0,s__Object)
| ~ s__instance(X1,s__Object) ),
inference(ennf_transformation,[],[f7547]) ).
fof(f11895,plain,
! [X0,X1] :
( ~ s__instance(X1,s__Object)
| ~ s__connected(X1,X0)
| ~ s__instance(X0,s__Object)
| s__connected(X0,X1) ),
inference(flattening,[],[f11894]) ).
fof(f12061,plain,
! [X1,X0] :
( ( s__instance(X0,s__SetOrClass)
& s__instance(X1,s__SetOrClass) )
| ~ s__subclass(X0,X1) ),
inference(ennf_transformation,[],[f26]) ).
fof(f12756,plain,
! [X0,X1] :
( ( s__connectedEngineeringComponents(X1,X0)
<=> ? [X2] :
( s__instance(X2,s__EngineeringConnection)
& s__connectsEngineeringComponents(X2,X1,X0) ) )
| ~ s__instance(X0,s__EngineeringComponent)
| ~ s__instance(X1,s__EngineeringComponent) ),
inference(ennf_transformation,[],[f6441]) ).
fof(f12757,plain,
! [X1,X0] :
( ~ s__instance(X0,s__EngineeringComponent)
| ( s__connectedEngineeringComponents(X1,X0)
<=> ? [X2] :
( s__instance(X2,s__EngineeringConnection)
& s__connectsEngineeringComponents(X2,X1,X0) ) )
| ~ s__instance(X1,s__EngineeringComponent) ),
inference(flattening,[],[f12756]) ).
fof(f13690,plain,
s__instance(s__Object16_2,s__EngineeringComponent),
inference(cnf_transformation,[],[f7219]) ).
fof(f14053,plain,
~ s__meetsSpatially(s__Object16_2,s__Object16_3),
inference(cnf_transformation,[],[f8413]) ).
fof(f16076,plain,
s__instance(s__Object16_3,s__EngineeringComponent),
inference(cnf_transformation,[],[f7220]) ).
fof(f16405,plain,
~ s__overlapsSpatially(s__Object16_2,s__Object16_3),
inference(cnf_transformation,[],[f7222]) ).
fof(f16937,plain,
! [X0,X1] :
( s__connectedEngineeringComponents(X1,X0)
| ~ s__instance(X0,s__EngineeringComponent)
| ~ s__instance(X1,s__EngineeringComponent)
| ~ s__connectedEngineeringComponents(X0,X1) ),
inference(cnf_transformation,[],[f8932]) ).
fof(f17259,plain,
s__subclass(s__Artifact,s__Object),
inference(cnf_transformation,[],[f6310]) ).
fof(f18466,plain,
s__connectsEngineeringComponents(s__Object16_1,s__Object16_2,s__Object16_3),
inference(cnf_transformation,[],[f7221]) ).
fof(f18687,plain,
s__subclass(s__EngineeringComponent,s__Device),
inference(cnf_transformation,[],[f6420]) ).
fof(f18908,plain,
s__instance(s__Object16_1,s__EngineeringConnection),
inference(cnf_transformation,[],[f7218]) ).
fof(f18999,plain,
! [X0,X1] :
( s__instance(X1,s__SetOrClass)
| ~ s__subclass(X0,X1) ),
inference(cnf_transformation,[],[f12061]) ).
fof(f19000,plain,
! [X0,X1] :
( s__instance(X0,s__SetOrClass)
| ~ s__subclass(X0,X1) ),
inference(cnf_transformation,[],[f12061]) ).
fof(f20390,plain,
! [X0,X1] :
( s__meetsSpatially(X0,X1)
| ~ s__instance(X0,s__Object)
| s__overlapsSpatially(X0,X1)
| ~ s__instance(X1,s__Object)
| ~ s__connected(X0,X1) ),
inference(cnf_transformation,[],[f8845]) ).
fof(f20556,plain,
! [X2,X0,X1] :
( ~ s__subclass(X0,X1)
| ~ s__instance(X1,s__SetOrClass)
| s__instance(X2,X1)
| ~ s__instance(X0,s__SetOrClass)
| ~ s__instance(X2,X0) ),
inference(cnf_transformation,[],[f10250]) ).
fof(f20616,plain,
! [X2,X0,X1] :
( s__connectedEngineeringComponents(X1,X0)
| ~ s__instance(X1,s__EngineeringComponent)
| ~ s__instance(X0,s__EngineeringComponent)
| ~ s__connectsEngineeringComponents(X2,X1,X0)
| ~ s__instance(X2,s__EngineeringConnection) ),
inference(cnf_transformation,[],[f12757]) ).
fof(f21454,plain,
! [X0,X1] :
( s__connected(X0,X1)
| ~ s__instance(X1,s__Object)
| ~ s__instance(X0,s__Object)
| ~ s__connected(X1,X0) ),
inference(cnf_transformation,[],[f11895]) ).
fof(f21652,plain,
s__subclass(s__Device,s__Artifact),
inference(cnf_transformation,[],[f6387]) ).
fof(f22761,plain,
! [X0,X1] :
( s__connected(X1,X0)
| ~ s__instance(X0,s__EngineeringComponent)
| ~ s__instance(X1,s__EngineeringComponent)
| ~ s__connectedEngineeringComponents(X1,X0) ),
inference(cnf_transformation,[],[f9794]) ).
fof(f124312,definition,
( spl478_100
<=> s__instance(s__Object16_3,s__Object) ),
introduced(definition,[new_symbols(definition,[spl478_100])],[avatar_definition]) ).
fof(f124313,plain,
( s__instance(s__Object16_3,s__Object)
| ~ spl478_100 ),
inference(avatar_component_clause,[],[f124312]) ).
fof(f124314,plain,
( ~ s__instance(s__Object16_3,s__Object)
| spl478_100 ),
inference(avatar_component_clause,[],[f124312]) ).
fof(f125195,definition,
( spl478_123
<=> s__instance(s__Object16_2,s__Object) ),
introduced(definition,[new_symbols(definition,[spl478_123])],[avatar_definition]) ).
fof(f125196,plain,
( s__instance(s__Object16_2,s__Object)
| ~ spl478_123 ),
inference(avatar_component_clause,[],[f125195]) ).
fof(f125197,plain,
( ~ s__instance(s__Object16_2,s__Object)
| spl478_123 ),
inference(avatar_component_clause,[],[f125195]) ).
fof(f152508,plain,
( ~ s__connected(s__Object16_2,s__Object16_3)
| ~ s__instance(s__Object16_2,s__Object)
| s__overlapsSpatially(s__Object16_2,s__Object16_3)
| ~ s__instance(s__Object16_3,s__Object) ),
inference(resolution,[],[f20390,f14053]) ).
fof(f152645,plain,
! [X2,X0,X1] :
( ~ s__instance(X0,s__SetOrClass)
| s__instance(X2,X1)
| ~ s__subclass(X0,X1)
| ~ s__instance(X2,X0) ),
inference(forward_subsumption_resolution,[],[f20556,f18999]) ).
fof(f152646,plain,
! [X2,X0,X1] :
( s__instance(X2,X1)
| ~ s__subclass(X0,X1)
| ~ s__instance(X2,X0) ),
inference(forward_subsumption_resolution,[],[f152645,f19000]) ).
fof(f152899,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Object)
| ~ s__instance(s__Object16_3,X0) )
| spl478_100 ),
inference(resolution,[],[f152646,f124314]) ).
fof(f152996,plain,
( ~ s__instance(s__Object16_3,s__Artifact)
| spl478_100 ),
inference(resolution,[],[f152899,f17259]) ).
fof(f153011,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Artifact)
| ~ s__instance(s__Object16_3,X0) )
| spl478_100 ),
inference(resolution,[],[f152996,f152646]) ).
fof(f153393,plain,
( ~ s__instance(s__Object16_3,s__Device)
| spl478_100 ),
inference(resolution,[],[f153011,f21652]) ).
fof(f153414,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Device)
| ~ s__instance(s__Object16_3,X0) )
| spl478_100 ),
inference(resolution,[],[f153393,f152646]) ).
fof(f158178,plain,
( ~ s__instance(s__Object16_3,s__EngineeringComponent)
| spl478_100 ),
inference(resolution,[],[f153414,f18687]) ).
fof(f158185,plain,
( $false
| spl478_100 ),
inference(forward_subsumption_resolution,[],[f158178,f16076]) ).
fof(f158186,plain,
spl478_100,
inference(avatar_contradiction_clause,[],[f158185]) ).
fof(f158187,plain,
( ~ s__connected(s__Object16_2,s__Object16_3)
| ~ s__instance(s__Object16_2,s__Object)
| ~ s__instance(s__Object16_3,s__Object) ),
inference(forward_subsumption_resolution,[],[f152508,f16405]) ).
fof(f158504,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Object)
| ~ s__instance(s__Object16_2,X0) )
| spl478_123 ),
inference(resolution,[],[f125197,f152646]) ).
fof(f159728,plain,
( ~ s__instance(s__Object16_2,s__Artifact)
| spl478_123 ),
inference(resolution,[],[f158504,f17259]) ).
fof(f160568,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Artifact)
| ~ s__instance(s__Object16_2,X0) )
| spl478_123 ),
inference(resolution,[],[f159728,f152646]) ).
fof(f162652,plain,
( ~ s__instance(s__Object16_2,s__Device)
| spl478_123 ),
inference(resolution,[],[f160568,f21652]) ).
fof(f163958,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Device)
| ~ s__instance(s__Object16_2,X0) )
| spl478_123 ),
inference(resolution,[],[f162652,f152646]) ).
fof(f169030,plain,
( ~ s__instance(s__Object16_2,s__EngineeringComponent)
| spl478_123 ),
inference(resolution,[],[f163958,f18687]) ).
fof(f169037,plain,
( $false
| spl478_123 ),
inference(forward_subsumption_resolution,[],[f169030,f13690]) ).
fof(f169038,plain,
spl478_123,
inference(avatar_contradiction_clause,[],[f169037]) ).
fof(f169368,definition,
( spl478_196
<=> s__connected(s__Object16_3,s__Object16_2) ),
introduced(definition,[new_symbols(definition,[spl478_196])],[avatar_definition]) ).
fof(f169369,plain,
( s__connected(s__Object16_3,s__Object16_2)
| ~ spl478_196 ),
inference(avatar_component_clause,[],[f169368]) ).
fof(f169370,plain,
( ~ s__connected(s__Object16_3,s__Object16_2)
| spl478_196 ),
inference(avatar_component_clause,[],[f169368]) ).
fof(f169379,plain,
( ~ s__instance(s__Object16_2,s__EngineeringComponent)
| ~ s__connectedEngineeringComponents(s__Object16_3,s__Object16_2)
| ~ s__instance(s__Object16_3,s__EngineeringComponent)
| spl478_196 ),
inference(resolution,[],[f169370,f22761]) ).
fof(f169382,plain,
( ~ s__instance(s__Object16_3,s__EngineeringComponent)
| ~ s__connectedEngineeringComponents(s__Object16_3,s__Object16_2)
| spl478_196 ),
inference(forward_subsumption_resolution,[],[f169379,f13690]) ).
fof(f169385,plain,
( ~ s__connectedEngineeringComponents(s__Object16_3,s__Object16_2)
| spl478_196 ),
inference(forward_subsumption_resolution,[],[f169382,f16076]) ).
fof(f169391,plain,
( ~ s__connectedEngineeringComponents(s__Object16_2,s__Object16_3)
| ~ s__instance(s__Object16_3,s__EngineeringComponent)
| ~ s__instance(s__Object16_2,s__EngineeringComponent)
| spl478_196 ),
inference(resolution,[],[f169385,f16937]) ).
fof(f169392,plain,
( ~ s__connectedEngineeringComponents(s__Object16_2,s__Object16_3)
| ~ s__instance(s__Object16_2,s__EngineeringComponent)
| spl478_196 ),
inference(forward_subsumption_resolution,[],[f169391,f16076]) ).
fof(f169393,plain,
( ~ s__connectedEngineeringComponents(s__Object16_2,s__Object16_3)
| spl478_196 ),
inference(forward_subsumption_resolution,[],[f169392,f13690]) ).
fof(f179162,plain,
( ! [X0] :
( ~ s__instance(s__Object16_3,s__EngineeringComponent)
| ~ s__connectsEngineeringComponents(X0,s__Object16_2,s__Object16_3)
| ~ s__instance(s__Object16_2,s__EngineeringComponent)
| ~ s__instance(X0,s__EngineeringConnection) )
| spl478_196 ),
inference(resolution,[],[f20616,f169393]) ).
fof(f179166,plain,
( ! [X0] :
( ~ s__instance(s__Object16_2,s__EngineeringComponent)
| ~ s__connectsEngineeringComponents(X0,s__Object16_2,s__Object16_3)
| ~ s__instance(X0,s__EngineeringConnection) )
| spl478_196 ),
inference(forward_subsumption_resolution,[],[f179162,f16076]) ).
fof(f179168,plain,
( ! [X0] :
( ~ s__connectsEngineeringComponents(X0,s__Object16_2,s__Object16_3)
| ~ s__instance(X0,s__EngineeringConnection) )
| spl478_196 ),
inference(forward_subsumption_resolution,[],[f179166,f13690]) ).
fof(f179196,plain,
( ~ s__instance(s__Object16_1,s__EngineeringConnection)
| spl478_196 ),
inference(resolution,[],[f179168,f18466]) ).
fof(f179198,plain,
( $false
| spl478_196 ),
inference(forward_subsumption_resolution,[],[f179196,f18908]) ).
fof(f179199,plain,
spl478_196,
inference(avatar_contradiction_clause,[],[f179198]) ).
fof(f179200,plain,
( ~ s__connected(s__Object16_2,s__Object16_3)
| ~ s__instance(s__Object16_3,s__Object)
| ~ spl478_123 ),
inference(forward_subsumption_resolution,[],[f158187,f125196]) ).
fof(f179201,plain,
( ~ s__connected(s__Object16_2,s__Object16_3)
| ~ spl478_100
| ~ spl478_123 ),
inference(forward_subsumption_resolution,[],[f179200,f124313]) ).
fof(f179256,plain,
( ~ s__instance(s__Object16_2,s__Object)
| ~ s__instance(s__Object16_3,s__Object)
| ~ s__connected(s__Object16_3,s__Object16_2)
| ~ spl478_100
| ~ spl478_123 ),
inference(resolution,[],[f179201,f21454]) ).
fof(f179258,plain,
( ~ s__connected(s__Object16_3,s__Object16_2)
| ~ s__instance(s__Object16_3,s__Object)
| ~ spl478_100
| ~ spl478_123 ),
inference(forward_subsumption_resolution,[],[f179256,f125196]) ).
fof(f179260,plain,
( ~ s__connected(s__Object16_3,s__Object16_2)
| ~ spl478_100
| ~ spl478_123 ),
inference(forward_subsumption_resolution,[],[f179258,f124313]) ).
fof(f179363,plain,
( $false
| ~ spl478_100
| ~ spl478_123
| ~ spl478_196 ),
inference(forward_subsumption_resolution,[],[f179260,f169369]) ).
fof(f179364,plain,
( ~ spl478_100
| ~ spl478_123
| ~ spl478_196 ),
inference(avatar_contradiction_clause,[],[f179363]) ).
cnf(s7798,plain,
spl478_100,
inference(sat_conversion,[],[f158186]) ).
cnf(s7813,plain,
spl478_123,
inference(sat_conversion,[],[f169038]) ).
cnf(s7866,plain,
spl478_196,
inference(sat_conversion,[],[f179199]) ).
cnf(s7867,plain,
( ~ spl478_100
| ~ spl478_123
| ~ spl478_196 ),
inference(sat_conversion,[],[f179364]) ).
cnf(s7869,plain,
~ spl478_100,
inference(rat,[],[s7867,s7866,s7813]) ).
cnf(s7870,plain,
$false,
inference(rat,[],[s7798,s7869]) ).
fof(f179365,plain,
$false,
inference(avatar_sat_refutation,[],[s7870]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : CSR089+4 : TPTP v9.3.1. Bugfixed v7.3.0.
% 0.00/0.03 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.00/0.10 % Computer : n012.cluster.edu
% 0.00/0.10 % Model : x86_64 x86_64
% 0.00/0.10 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.00/0.10 % Memory : 8046.5625MB
% 0.00/0.10 % OS : Linux 6.8.0-71-generic
% 0.00/0.10 % CPULimit : 300
% 0.00/0.10 % WCLimit : 300
% 0.00/0.10 % DateTime : Mon Sep 28 22:39:04 UTC 2026
% 0.00/0.10 % CPUTime :
% 0.00/0.10 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.09/0.12 Running first-order model finding
% 0.09/0.12 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 4.27/1.01 % (3874792)Will run a generic schedule for satisfiability detection.
% 4.27/1.01 % (3874803)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2293474246:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 4.27/1.01 % (3874800)dis+10_1_sil=32000:sp=arity:random_seed=2079767475:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 4.27/1.01 % (3874797)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=4056539985_2999 on theBenchmark for (2999ds/0Mi)
% 4.27/1.01 % (3874799)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3077138682:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 4.27/1.01 % (3874801)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1676080042:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 4.27/1.01 % (3874802)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2499570849:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 4.27/1.01 % (3874798)% WARNING: option uhcvi not known.
% 4.27/1.01 % (3874798)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1612172147:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 4.27/1.01 % (3874800)Instruction limit reached!
% 4.27/1.01 % (3874800)------------------------------
% 4.27/1.01 % (3874800)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.27/1.01 % (3874800)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.27/1.01 % (3874800)CaDiCaL version: 2.1.3
% 4.27/1.01 % (3874800)Termination reason: Instruction limit
% 4.27/1.01 % (3874800)Termination phase: Clausification
% 4.27/1.01 % (3874800)Time elapsed: 0.038 s
% 4.27/1.01 % (3874800)Peak memory usage: 24 MB
% 4.27/1.01 % (3874800)Instructions burned: 103 (million)
% 4.27/1.01 % (3874801)Instruction limit reached!
% 4.27/1.01 % (3874801)------------------------------
% 4.27/1.01 % (3874801)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.27/1.01 % (3874801)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.27/1.01 % (3874801)CaDiCaL version: 2.1.3
% 4.27/1.01 % (3874801)Termination reason: Instruction limit
% 4.27/1.01 % (3874801)Termination phase: Property scanning
% 4.27/1.01 % (3874801)Time elapsed: 0.043 s
% 4.27/1.01 % (3874801)Peak memory usage: 26 MB
% 4.27/1.01 % (3874801)Instructions burned: 116 (million)
% 4.27/1.01 % (3874802)Instruction limit reached!
% 4.27/1.01 % (3874802)------------------------------
% 4.27/1.01 % (3874802)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.27/1.01 % (3874802)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.27/1.01 % (3874802)CaDiCaL version: 2.1.3
% 4.27/1.01 % (3874802)Termination reason: Instruction limit
% 4.27/1.01 % (3874802)Termination phase: Property scanning
% 4.27/1.01 % (3874802)Time elapsed: 0.047 s
% 4.27/1.01 % (3874802)Peak memory usage: 24 MB
% 4.27/1.01 % (3874802)Instructions burned: 132 (million)
% 4.27/1.01 % (3874811)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=964418064:i=714:nm=2_2998 on theBenchmark for (2998ds/714Mi)
% 4.27/1.01 % (3874803)Instruction limit reached!
% 4.27/1.01 % (3874803)------------------------------
% 4.27/1.01 % (3874803)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.27/1.01 % (3874803)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.27/1.01 % (3874803)CaDiCaL version: 2.1.3
% 4.27/1.01 % (3874803)Termination reason: Instruction limit
% 4.27/1.01 % (3874803)Termination phase: Equality resolution with deletion
% 4.27/1.01 % (3874803)Time elapsed: 0.053 s
% 4.27/1.01 % (3874803)Peak memory usage: 24 MB
% 4.27/1.01 % (3874803)Instructions burned: 161 (million)
% 4.27/1.01 % (3874812)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=168485984:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 4.27/1.01 % (3874813)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=1732527417:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 4.27/1.01 % (3874815)ott-21_1_sil=16000:fs=off:random_seed=780274114:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 4.27/1.01 % (3874812)Instruction limit reached!
% 4.27/1.01 % (3874812)------------------------------
% 4.27/1.01 % (3874812)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.27/1.01 % (3874812)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.54/1.60 % (3874812)CaDiCaL version: 2.1.3
% 8.54/1.60 % (3874812)Termination reason: Instruction limit
% 8.54/1.60 % (3874812)Termination phase: Property scanning
% 8.54/1.60 % (3874812)Time elapsed: 0.048 s
% 8.54/1.60 % (3874812)Peak memory usage: 24 MB
% 8.54/1.60 % (3874812)Instructions burned: 133 (million)
% 8.54/1.60 % (3874819)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=969154401:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 8.54/1.60 % (3874815)Instruction limit reached!
% 8.54/1.60 % (3874815)------------------------------
% 8.54/1.60 % (3874815)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.54/1.60 % (3874815)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.54/1.60 % (3874815)CaDiCaL version: 2.1.3
% 8.54/1.60 % (3874815)Termination reason: Instruction limit
% 8.54/1.60 % (3874815)Termination phase: Property scanning
% 8.54/1.60 % (3874815)Time elapsed: 0.060 s
% 8.54/1.60 % (3874815)Peak memory usage: 25 MB
% 8.54/1.60 % (3874815)Instructions burned: 183 (million)
% 8.54/1.60 % (3874821)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3417711686:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 8.54/1.60 % (3874811)Instruction limit reached!
% 8.54/1.60 % (3874811)------------------------------
% 8.54/1.60 % (3874811)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.54/1.60 % (3874811)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.54/1.60 % (3874811)CaDiCaL version: 2.1.3
% 8.54/1.60 % (3874811)Termination reason: Instruction limit
% 8.54/1.60 % (3874811)Termination phase: Finite model building preprocessing
% 8.54/1.60 % (3874811)Time elapsed: 0.194 s
% 8.54/1.60 % (3874811)Peak memory usage: 36 MB
% 8.54/1.60 % (3874811)Instructions burned: 716 (million)
% 8.54/1.60 % (3874819)Instruction limit reached!
% 8.54/1.60 % (3874819)------------------------------
% 8.54/1.60 % (3874819)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.54/1.60 % (3874819)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.54/1.60 % (3874819)CaDiCaL version: 2.1.3
% 8.54/1.60 % (3874819)Termination reason: Instruction limit
% 8.54/1.60 % (3874819)Termination phase: Saturation
% 8.54/1.60 % (3874819)Time elapsed: 0.141 s
% 8.54/1.60 % (3874819)Peak memory usage: 31 MB
% 8.54/1.60 % (3874819)Instructions burned: 479 (million)
% 8.54/1.60 % (3874823)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2142559234:i=1179_2996 on theBenchmark for (2996ds/1179Mi)
% 8.54/1.60 % (3874813)Instruction limit reached!
% 8.54/1.60 % (3874813)------------------------------
% 8.54/1.60 % (3874813)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.54/1.60 % (3874813)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.54/1.60 % (3874813)CaDiCaL version: 2.1.3
% 8.54/1.60 % (3874813)Termination reason: Instruction limit
% 8.54/1.60 % (3874813)Termination phase: Saturation
% 8.54/1.60 % (3874813)Time elapsed: 0.207 s
% 8.54/1.60 % (3874813)Peak memory usage: 34 MB
% 8.54/1.60 % (3874813)Instructions burned: 686 (million)
% 8.54/1.60 % (3874825)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3086361727:i=889:ins=1_2996 on theBenchmark for (2996ds/889Mi)
% 8.54/1.60 % (3874826)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=3839292401: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)
% 8.54/1.60 % (3874821)Instruction limit reached!
% 8.54/1.60 % (3874821)------------------------------
% 8.54/1.60 % (3874821)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.54/1.60 % (3874821)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.54/1.60 % (3874821)CaDiCaL version: 2.1.3
% 8.54/1.60 % (3874821)Termination reason: Instruction limit
% 8.54/1.60 % (3874821)Termination phase: Finite model building preprocessing
% 8.54/1.60 % (3874821)Time elapsed: 0.235 s
% 8.54/1.60 % (3874821)Peak memory usage: 39 MB
% 8.54/1.60 % (3874821)Instructions burned: 869 (million)
% 8.54/1.60 % (3874829)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1124744166:i=879:kws=inv_precedence:fsr=off_2995 on theBenchmark for (2995ds/879Mi)
% 8.54/1.60 % Detected minimum model sizes of [51]
% 8.54/1.60 % Detected maximum model sizes of [max]
% 8.54/1.60 % (3874797)Cannot represent all propositional literals internally
% 8.54/1.60 % (3874797)Refutation not found, incomplete strategy
% 8.54/1.60 % (3874797)------------------------------
% 16.82/2.72 % (3874797)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.82/2.72 % (3874797)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.82/2.72 % (3874797)CaDiCaL version: 2.1.3
% 16.82/2.72 % (3874797)Termination reason: Refutation not found, incomplete strategy
% 16.82/2.72 % (3874797)Time elapsed: 0.413 s
% 16.82/2.72 % (3874797)Peak memory usage: 49 MB
% 16.82/2.72 % (3874797)Instructions burned: 1471 (million)
% 16.82/2.72 % (3874797)------------------------------
% 16.82/2.72 % (3874797)------------------------------
% 16.82/2.72 % (3874831)fmb+10_1_sil=64000:random_seed=2641176098:i=22061:nm=2:gsp=on_2994 on theBenchmark for (2994ds/22061Mi)
% 16.82/2.72 % (3874826)Instruction limit reached!
% 16.82/2.72 % (3874826)------------------------------
% 16.82/2.72 % (3874826)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.82/2.72 % (3874826)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.82/2.72 % (3874826)CaDiCaL version: 2.1.3
% 16.82/2.72 % (3874826)Termination reason: Instruction limit
% 16.82/2.72 % (3874826)Termination phase: Saturation
% 16.82/2.72 % (3874826)Time elapsed: 0.216 s
% 16.82/2.72 % (3874826)Peak memory usage: 35 MB
% 16.82/2.72 % (3874826)Instructions burned: 693 (million)
% 16.82/2.72 % (3874833)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=862241773:i=9515:nm=5_2993 on theBenchmark for (2993ds/9515Mi)
% 16.82/2.72 % (3874825)Instruction limit reached!
% 16.82/2.72 % (3874825)------------------------------
% 16.82/2.72 % (3874825)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.82/2.72 % (3874825)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.82/2.72 % (3874825)CaDiCaL version: 2.1.3
% 16.82/2.72 % (3874825)Termination reason: Instruction limit
% 16.82/2.72 % (3874825)Termination phase: Finite model building preprocessing
% 16.82/2.72 % (3874825)Time elapsed: 0.245 s
% 16.82/2.72 % (3874825)Peak memory usage: 40 MB
% 16.82/2.72 % (3874825)Instructions burned: 890 (million)
% 16.82/2.72 % (3874835)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=4113132310:fmbsr=1.7:i=920_2993 on theBenchmark for (2993ds/920Mi)
% 16.82/2.72 % (3874823)Instruction limit reached!
% 16.82/2.72 % (3874823)------------------------------
% 16.82/2.72 % (3874823)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.82/2.72 % (3874823)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.82/2.72 % (3874823)CaDiCaL version: 2.1.3
% 16.82/2.72 % (3874823)Termination reason: Instruction limit
% 16.82/2.72 % (3874823)Termination phase: Saturation
% 16.82/2.72 % (3874823)Time elapsed: 0.335 s
% 16.82/2.72 % (3874823)Peak memory usage: 36 MB
% 16.82/2.72 % (3874823)Instructions burned: 1180 (million)
% 16.82/2.72 % (3874837)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2274987627:i=5131_2992 on theBenchmark for (2992ds/5131Mi)
% 16.82/2.72 % (3874829)Instruction limit reached!
% 16.82/2.72 % (3874829)------------------------------
% 16.82/2.72 % (3874829)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.82/2.72 % (3874829)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.82/2.72 % (3874829)CaDiCaL version: 2.1.3
% 16.82/2.72 % (3874829)Termination reason: Instruction limit
% 16.82/2.72 % (3874829)Termination phase: Saturation
% 16.82/2.72 % (3874829)Time elapsed: 0.233 s
% 16.82/2.72 % (3874829)Peak memory usage: 37 MB
% 16.82/2.72 % (3874829)Instructions burned: 879 (million)
% 16.82/2.72 % (3874839)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=334813220:i=1472:ins=7:fdi=8:gsp=on_2992 on theBenchmark for (2992ds/1472Mi)
% 16.82/2.72 % Detected minimum model sizes of [51]
% 16.82/2.72 % Detected maximum model sizes of [max]
% 16.82/2.72 % (3874831)Cannot represent all propositional literals internally
% 16.82/2.72 % (3874831)Refutation not found, incomplete strategy
% 16.82/2.72 % (3874831)------------------------------
% 16.82/2.72 % (3874831)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.82/2.72 % (3874831)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.82/2.72 % (3874831)CaDiCaL version: 2.1.3
% 16.82/2.72 % (3874831)Termination reason: Refutation not found, incomplete strategy
% 16.82/2.72 % (3874831)Time elapsed: 0.330 s
% 16.82/2.72 % (3874831)Peak memory usage: 42 MB
% 16.82/2.72 % (3874831)Instructions burned: 1181 (million)
% 16.82/2.72 % (3874831)------------------------------
% 16.82/2.72 % (3874831)------------------------------
% 16.82/2.72 % (3874835)Instruction limit reached!
% 22.90/3.50 % (3874835)------------------------------
% 22.90/3.50 % (3874835)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.90/3.50 % (3874835)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.90/3.50 % (3874835)CaDiCaL version: 2.1.3
% 22.90/3.50 % (3874835)Termination reason: Instruction limit
% 22.90/3.50 % (3874835)Termination phase: Finite model building preprocessing
% 22.90/3.50 % (3874835)Time elapsed: 0.250 s
% 22.90/3.50 % (3874835)Peak memory usage: 40 MB
% 22.90/3.50 % (3874835)Instructions burned: 922 (million)
% 22.90/3.50 % (3874841)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=2755918292:i=6324_2991 on theBenchmark for (2991ds/6324Mi)
% 22.90/3.50 % (3874842)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=3550142548:fmbsr=2.30978:i=2174_2991 on theBenchmark for (2991ds/2174Mi)
% 22.90/3.50 % Detected minimum model sizes of [51]
% 22.90/3.50 % Detected maximum model sizes of [max]
% 22.90/3.50 % (3874833)Cannot represent all propositional literals internally
% 22.90/3.50 % (3874833)Refutation not found, incomplete strategy
% 22.90/3.50 % (3874833)------------------------------
% 22.90/3.50 % (3874833)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.90/3.50 % (3874833)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.90/3.50 % (3874833)CaDiCaL version: 2.1.3
% 22.90/3.50 % (3874833)Termination reason: Refutation not found, incomplete strategy
% 22.90/3.50 % (3874833)Time elapsed: 0.330 s
% 22.90/3.50 % (3874833)Peak memory usage: 44 MB
% 22.90/3.50 % (3874833)Instructions burned: 1257 (million)
% 22.90/3.50 % (3874833)------------------------------
% 22.90/3.50 % (3874833)------------------------------
% 22.90/3.50 % (3874845)ott-2_1_sil=16000:newcnf=on:random_seed=285095926:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2990 on theBenchmark for (2990ds/869Mi)
% 22.90/3.50 % (3874839)Instruction limit reached!
% 22.90/3.50 % (3874839)------------------------------
% 22.90/3.50 % (3874839)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.90/3.50 % (3874839)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.90/3.50 % (3874839)CaDiCaL version: 2.1.3
% 22.90/3.50 % (3874839)Termination reason: Instruction limit
% 22.90/3.50 % (3874839)Termination phase: Saturation
% 22.90/3.50 % (3874839)Time elapsed: 0.420 s
% 22.90/3.50 % (3874839)Peak memory usage: 43 MB
% 22.90/3.50 % (3874839)Instructions burned: 1472 (million)
% 22.90/3.50 % (3874847)ott+10_1_sil=32000:tgt=ground:random_seed=2529012257:i=5114:av=off_2988 on theBenchmark for (2988ds/5114Mi)
% 22.90/3.50 % (3874845)Instruction limit reached!
% 22.90/3.50 % (3874845)------------------------------
% 22.90/3.50 % (3874845)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.90/3.50 % (3874845)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.90/3.50 % (3874845)CaDiCaL version: 2.1.3
% 22.90/3.50 % (3874845)Termination reason: Instruction limit
% 22.90/3.50 % (3874845)Termination phase: Saturation
% 22.90/3.50 % (3874845)Time elapsed: 0.249 s
% 22.90/3.50 % (3874845)Peak memory usage: 38 MB
% 22.90/3.50 % (3874845)Instructions burned: 869 (million)
% 22.90/3.50 % (3874849)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2258578772:i=54282_2987 on theBenchmark for (2987ds/54282Mi)
% 22.90/3.50 % Detected minimum model sizes of [51]
% 22.90/3.50 % Detected maximum model sizes of [max]
% 22.90/3.50 % (3874841)Cannot represent all propositional literals internally
% 22.90/3.50 % (3874841)Refutation not found, incomplete strategy
% 22.90/3.50 % (3874841)------------------------------
% 22.90/3.50 % (3874841)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.90/3.50 % (3874841)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.90/3.50 % (3874841)CaDiCaL version: 2.1.3
% 22.90/3.50 % (3874841)Termination reason: Refutation not found, incomplete strategy
% 22.90/3.50 % (3874841)Time elapsed: 0.404 s
% 22.90/3.50 % (3874841)Peak memory usage: 48 MB
% 22.90/3.50 % (3874841)Instructions burned: 1456 (million)
% 22.90/3.50 % (3874841)------------------------------
% 22.90/3.50 % (3874841)------------------------------
% 22.90/3.50 % (3874851)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3937844559:i=3512:aac=none_2986 on theBenchmark for (2986ds/3512Mi)
% 22.90/3.50 % (3874842)Instruction limit reached!
% 22.90/3.50 % (3874842)------------------------------
% 22.90/3.50 % (3874842)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.90/3.50 % (3874842)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 71.22/10.39 % (3874842)CaDiCaL version: 2.1.3
% 71.22/10.39 % (3874842)Termination reason: Instruction limit
% 71.22/10.39 % (3874842)Termination phase: Finite model building preprocessing
% 71.22/10.39 % (3874842)Time elapsed: 0.577 s
% 71.22/10.39 % (3874842)Peak memory usage: 62 MB
% 71.22/10.39 % (3874842)Instructions burned: 2175 (million)
% 71.22/10.39 % (3874853)dis+21_1_sil=32000:sas=cadical:random_seed=1713792910:i=3773:amm=off_2985 on theBenchmark for (2985ds/3773Mi)
% 71.22/10.39 % Detected minimum model sizes of [51]
% 71.22/10.39 % Detected maximum model sizes of [max]
% 71.22/10.39 % (3874849)Cannot represent all propositional literals internally
% 71.22/10.39 % (3874849)Refutation not found, incomplete strategy
% 71.22/10.39 % (3874849)------------------------------
% 71.22/10.39 % (3874849)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 71.22/10.39 % (3874849)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 71.22/10.39 % (3874849)CaDiCaL version: 2.1.3
% 71.22/10.39 % (3874849)Termination reason: Refutation not found, incomplete strategy
% 71.22/10.39 % (3874849)Time elapsed: 0.400 s
% 71.22/10.39 % (3874849)Peak memory usage: 49 MB
% 71.22/10.39 % (3874849)Instructions burned: 1466 (million)
% 71.22/10.39 % (3874849)------------------------------
% 71.22/10.39 % (3874849)------------------------------
% 71.22/10.39 % (3874855)ott+11_1_sil=16000:gs=on:random_seed=3964714142:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2983 on theBenchmark for (2983ds/2251Mi)
% 71.22/10.39 % (3874851)Instruction limit reached!
% 71.22/10.39 % (3874851)------------------------------
% 71.22/10.39 % (3874851)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 71.22/10.39 % (3874851)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 71.22/10.39 % (3874851)CaDiCaL version: 2.1.3
% 71.22/10.39 % (3874851)Termination reason: Instruction limit
% 71.22/10.39 % (3874851)Termination phase: Saturation
% 71.22/10.39 % (3874851)Time elapsed: 0.894 s
% 71.22/10.39 % (3874851)Peak memory usage: 60 MB
% 71.22/10.39 % (3874851)Instructions burned: 3515 (million)
% 71.22/10.39 % (3874857)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=3619016206:fmbsr=1.6:i=67534_2977 on theBenchmark for (2977ds/67534Mi)
% 71.22/10.39 % (3874837)Instruction limit reached!
% 71.22/10.39 % (3874837)------------------------------
% 71.22/10.39 % (3874837)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 71.22/10.39 % (3874837)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 71.22/10.39 % (3874837)CaDiCaL version: 2.1.3
% 71.22/10.39 % (3874837)Termination reason: Instruction limit
% 71.22/10.39 % (3874837)Termination phase: Saturation
% 71.22/10.39 % (3874837)Time elapsed: 1.531 s
% 71.22/10.39 % (3874837)Peak memory usage: 57 MB
% 71.22/10.39 % (3874837)Instructions burned: 5132 (million)
% 71.22/10.39 % (3874859)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=3140268451:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2977 on theBenchmark for (2977ds/4591Mi)
% 71.22/10.39 % (3874855)Instruction limit reached!
% 71.22/10.39 % (3874855)------------------------------
% 71.22/10.39 % (3874855)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 71.22/10.39 % (3874855)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 71.22/10.39 % (3874855)CaDiCaL version: 2.1.3
% 71.22/10.39 % (3874855)Termination reason: Instruction limit
% 71.22/10.39 % (3874855)Termination phase: Saturation
% 71.22/10.39 % (3874855)Time elapsed: 0.798 s
% 71.22/10.39 % (3874855)Peak memory usage: 82 MB
% 71.22/10.39 % (3874855)Instructions burned: 2252 (million)
% 71.22/10.39 % (3874861)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=2061511755:i=29340_2975 on theBenchmark for (2975ds/29340Mi)
% 71.22/10.39 % (3874853)Instruction limit reached!
% 71.22/10.39 % (3874853)------------------------------
% 71.22/10.39 % (3874853)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 71.22/10.39 % (3874853)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 71.22/10.39 % (3874853)CaDiCaL version: 2.1.3
% 71.22/10.39 % (3874853)Termination reason: Instruction limit
% 71.22/10.39 % (3874853)Termination phase: Saturation
% 71.22/10.39 % (3874853)Time elapsed: 1.051 s
% 71.22/10.39 % (3874853)Peak memory usage: 62 MB
% 71.22/10.39 % (3874853)Instructions burned: 3774 (million)
% 71.22/10.39 % (3874863)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=410829662:i=5211_2974 on theBenchmark for (2974ds/5211Mi)
% 71.22/10.39 % (3874847)Instruction limit reached!
% 71.22/10.39 % (3874847)------------------------------
% 81.65/11.99 % (3874847)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 81.65/11.99 % (3874847)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 81.65/11.99 % (3874847)CaDiCaL version: 2.1.3
% 81.65/11.99 % (3874847)Termination reason: Instruction limit
% 81.65/11.99 % (3874847)Termination phase: Saturation
% 81.65/11.99 % (3874847)Time elapsed: 1.427 s
% 81.65/11.99 % (3874847)Peak memory usage: 63 MB
% 81.65/11.99 % (3874847)Instructions burned: 5114 (million)
% 81.65/11.99 % Detected minimum model sizes of [51]
% 81.65/11.99 % Detected maximum model sizes of [max]
% 81.65/11.99 % (3874857)Cannot represent all propositional literals internally
% 81.65/11.99 % (3874857)Refutation not found, incomplete strategy
% 81.65/11.99 % (3874857)------------------------------
% 81.65/11.99 % (3874857)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 81.65/11.99 % (3874857)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 81.65/11.99 % (3874857)CaDiCaL version: 2.1.3
% 81.65/11.99 % (3874857)Termination reason: Refutation not found, incomplete strategy
% 81.65/11.99 % (3874857)Time elapsed: 0.377 s
% 81.65/11.99 % (3874857)Peak memory usage: 45 MB
% 81.65/11.99 % (3874857)Instructions burned: 1418 (million)
% 81.65/11.99 % (3874865)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=935975118:i=5497:nm=2_2973 on theBenchmark for (2973ds/5497Mi)
% 81.65/11.99 % (3874857)------------------------------
% 81.65/11.99 % (3874857)------------------------------
% 81.65/11.99 % (3874867)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=2296539124:fmbsr=2:i=46332_2973 on theBenchmark for (2973ds/46332Mi)
% 81.65/11.99 % Detected minimum model sizes of [51]
% 81.65/11.99 % Detected maximum model sizes of [max]
% 81.65/11.99 % (3874865)Cannot represent all propositional literals internally
% 81.65/11.99 % (3874865)Refutation not found, incomplete strategy
% 81.65/11.99 % (3874865)------------------------------
% 81.65/11.99 % (3874865)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 81.65/11.99 % (3874865)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 81.65/11.99 % (3874865)CaDiCaL version: 2.1.3
% 81.65/11.99 % (3874865)Termination reason: Refutation not found, incomplete strategy
% 81.65/11.99 % (3874865)Time elapsed: 0.367 s
% 81.65/11.99 % (3874865)Peak memory usage: 45 MB
% 81.65/11.99 % (3874865)Instructions burned: 1327 (million)
% 81.65/11.99 % (3874865)------------------------------
% 81.65/11.99 % (3874865)------------------------------
% 81.65/11.99 % Detected minimum model sizes of [51]
% 81.65/11.99 % Detected maximum model sizes of [max]
% 81.65/11.99 % (3874867)Cannot represent all propositional literals internally
% 81.65/11.99 % (3874867)Refutation not found, incomplete strategy
% 81.65/11.99 % (3874867)------------------------------
% 81.65/11.99 % (3874867)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 81.65/11.99 % (3874867)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 81.65/11.99 % (3874867)CaDiCaL version: 2.1.3
% 81.65/11.99 % (3874867)Termination reason: Refutation not found, incomplete strategy
% 81.65/11.99 % (3874867)Time elapsed: 0.364 s
% 81.65/11.99 % (3874867)Peak memory usage: 45 MB
% 81.65/11.99 % (3874867)Instructions burned: 1418 (million)
% 81.65/11.99 % (3874869)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=1895155285:i=14071_2970 on theBenchmark for (2970ds/14071Mi)
% 81.65/11.99 % (3874867)------------------------------
% 81.65/11.99 % (3874867)------------------------------
% 81.65/11.99 % (3874871)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2687779866:i=22565:add=on:rawr=on_2969 on theBenchmark for (2969ds/22565Mi)
% 81.65/11.99 % Detected minimum model sizes of [51]
% 81.65/11.99 % Detected maximum model sizes of [max]
% 81.65/11.99 % (3874869)Cannot represent all propositional literals internally
% 81.65/11.99 % (3874869)Refutation not found, incomplete strategy
% 81.65/11.99 % (3874869)------------------------------
% 81.65/11.99 % (3874869)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 81.65/11.99 % (3874869)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 81.65/11.99 % (3874869)CaDiCaL version: 2.1.3
% 81.65/11.99 % (3874869)Termination reason: Refutation not found, incomplete strategy
% 81.65/11.99 % (3874869)Time elapsed: 0.343 s
% 81.65/11.99 % (3874869)Peak memory usage: 46 MB
% 81.65/11.99 % (3874869)Instructions burned: 1286 (million)
% 81.65/11.99 % (3874869)------------------------------
% 81.65/11.99 % (3874869)------------------------------
% 81.65/11.99 % (3874873)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=1791179580:i=8173:av=off_2966 on theBenchmark for (2966ds/8173Mi)
% 97.49/14.11 % (3874863)Instruction limit reached!
% 97.49/14.11 % (3874863)------------------------------
% 97.49/14.11 % (3874863)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 97.49/14.11 % (3874863)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 97.49/14.11 % (3874863)CaDiCaL version: 2.1.3
% 97.49/14.11 % (3874863)Termination reason: Instruction limit
% 97.49/14.11 % (3874863)Termination phase: Saturation
% 97.49/14.11 % (3874863)Time elapsed: 1.117 s
% 97.49/14.11 % (3874863)Peak memory usage: 47 MB
% 97.49/14.11 % (3874863)Instructions burned: 5214 (million)
% 97.49/14.11 % (3874875)dis+10_16:1_sil=16000:random_seed=3275383540:i=9155:fsr=off_2963 on theBenchmark for (2963ds/9155Mi)
% 97.49/14.11 % (3874859)Instruction limit reached!
% 97.49/14.11 % (3874859)------------------------------
% 97.49/14.11 % (3874859)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 97.49/14.11 % (3874859)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 97.49/14.11 % (3874859)CaDiCaL version: 2.1.3
% 97.49/14.11 % (3874859)Termination reason: Instruction limit
% 97.49/14.11 % (3874859)Termination phase: Saturation
% 97.49/14.11 % (3874859)Time elapsed: 1.479 s
% 97.49/14.11 % (3874859)Peak memory usage: 95 MB
% 97.49/14.11 % (3874859)Instructions burned: 4593 (million)
% 97.49/14.11 % (3874877)ott-3_8_sil=64000:random_seed=3871771921:i=20139:bs=on_2962 on theBenchmark for (2962ds/20139Mi)
% 97.49/14.11 % (3874873)Instruction limit reached!
% 97.49/14.11 % (3874873)------------------------------
% 97.49/14.11 % (3874873)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 97.49/14.11 % (3874873)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 97.49/14.11 % (3874873)CaDiCaL version: 2.1.3
% 97.49/14.11 % (3874873)Termination reason: Instruction limit
% 97.49/14.11 % (3874873)Termination phase: Saturation
% 97.49/14.11 % (3874873)Time elapsed: 2.509 s
% 97.49/14.11 % (3874873)Peak memory usage: 110 MB
% 97.49/14.11 % (3874873)Instructions burned: 8174 (million)
% 97.49/14.11 % (3874879)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=2322032425:fmbsr=2:i=32576_2941 on theBenchmark for (2941ds/32576Mi)
% 97.49/14.11 % Detected minimum model sizes of [51]
% 97.49/14.11 % Detected maximum model sizes of [max]
% 97.49/14.11 % (3874879)Cannot represent all propositional literals internally
% 97.49/14.11 % (3874879)Refutation not found, incomplete strategy
% 97.49/14.11 % (3874879)------------------------------
% 97.49/14.11 % (3874879)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 97.49/14.11 % (3874879)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 97.49/14.11 % (3874879)CaDiCaL version: 2.1.3
% 97.49/14.11 % (3874879)Termination reason: Refutation not found, incomplete strategy
% 97.49/14.11 % (3874879)Time elapsed: 0.411 s
% 97.49/14.11 % (3874879)Peak memory usage: 48 MB
% 97.49/14.11 % (3874879)Instructions burned: 1457 (million)
% 97.49/14.11 % (3874879)------------------------------
% 97.49/14.11 % (3874879)------------------------------
% 97.49/14.11 % (3874881)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=856600300:i=11404_2936 on theBenchmark for (2936ds/11404Mi)
% 97.49/14.11 % (3874875)Instruction limit reached!
% 97.49/14.11 % (3874875)------------------------------
% 97.49/14.11 % (3874875)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 97.49/14.11 % (3874875)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 97.49/14.11 % (3874875)CaDiCaL version: 2.1.3
% 97.49/14.11 % (3874875)Termination reason: Instruction limit
% 97.49/14.11 % (3874875)Termination phase: Saturation
% 97.49/14.11 % (3874875)Time elapsed: 2.664 s
% 97.49/14.11 % (3874875)Peak memory usage: 92 MB
% 97.49/14.11 % (3874875)Instructions burned: 9159 (million)
% 97.49/14.11 % (3874883)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=1928697768:i=14134_2936 on theBenchmark for (2936ds/14134Mi)
% 97.49/14.11 % (3874861)Instruction limit reached!
% 97.49/14.11 % (3874861)------------------------------
% 97.49/14.11 % (3874861)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 97.49/14.11 % (3874861)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 97.49/14.11 % (3874861)CaDiCaL version: 2.1.3
% 97.49/14.11 % (3874861)Termination reason: Instruction limit
% 97.49/14.11 % (3874861)Termination phase: Saturation
% 97.49/14.11 % (3874861)Time elapsed: 7.769 s
% 97.49/14.11 % (3874861)Peak memory usage: 78 MB
% 97.49/14.11 % (3874861)Instructions burned: 29341 (million)
% 97.49/14.11 % (3874885)dis+33_16_sil=32000:sac=on:random_seed=2846519574:i=15851:nm=0_2897 on theBenchmark for (2897ds/15851Mi)
% 121.30/17.49 % (3874871)Instruction limit reached!
% 121.30/17.49 % (3874871)------------------------------
% 121.30/17.49 % (3874871)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 121.30/17.49 % (3874871)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 121.30/17.49 % (3874871)CaDiCaL version: 2.1.3
% 121.30/17.49 % (3874871)Termination reason: Instruction limit
% 121.30/17.49 % (3874871)Termination phase: Saturation
% 121.30/17.49 % (3874871)Time elapsed: 7.262 s
% 121.30/17.49 % (3874871)Peak memory usage: 697 MB
% 121.30/17.49 % (3874871)Instructions burned: 22567 (million)
% 121.30/17.49 % (3874887)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=71259454:avsq=on:i=17627:add=on:amm=off_2896 on theBenchmark for (2896ds/17627Mi)
% 121.30/17.49 % (3874877)Instruction limit reached!
% 121.30/17.49 % (3874877)------------------------------
% 121.30/17.49 % (3874877)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 121.30/17.49 % (3874877)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 121.30/17.49 % (3874877)CaDiCaL version: 2.1.3
% 121.30/17.49 % (3874877)Termination reason: Instruction limit
% 121.30/17.49 % (3874877)Termination phase: Saturation
% 121.30/17.49 % (3874877)Time elapsed: 6.822 s
% 121.30/17.49 % (3874877)Peak memory usage: 133 MB
% 121.30/17.49 % (3874877)Instructions burned: 20140 (million)
% 121.30/17.49 % (3874889)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=3820071369:s2a=on:i=53295_2894 on theBenchmark for (2894ds/53295Mi)
% 121.30/17.49 % (3874883)Instruction limit reached!
% 121.30/17.49 % (3874883)------------------------------
% 121.30/17.49 % (3874883)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 121.30/17.49 % (3874883)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 121.30/17.49 % (3874883)CaDiCaL version: 2.1.3
% 121.30/17.49 % (3874883)Termination reason: Instruction limit
% 121.30/17.49 % (3874883)Termination phase: Saturation
% 121.30/17.49 % (3874883)Time elapsed: 4.728 s
% 121.30/17.49 % (3874883)Peak memory usage: 119 MB
% 121.30/17.49 % (3874883)Instructions burned: 14134 (million)
% 121.30/17.49 % (3874891)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=579440377:i=26857:ins=20_2888 on theBenchmark for (2888ds/26857Mi)
% 121.30/17.49 % (3874881)Instruction limit reached!
% 121.30/17.49 % (3874881)------------------------------
% 121.30/17.49 % (3874881)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 121.30/17.49 % (3874881)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 121.30/17.49 % (3874881)CaDiCaL version: 2.1.3
% 121.30/17.49 % (3874881)Termination reason: Instruction limit
% 121.30/17.49 % (3874881)Termination phase: Saturation
% 121.30/17.49 % (3874881)Time elapsed: 4.796 s
% 121.30/17.49 % (3874881)Peak memory usage: 402 MB
% 121.30/17.49 % (3874881)Instructions burned: 11406 (million)
% 121.30/17.49 % (3874893)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=3984373320:i=28120:bs=on:fsr=off_2888 on theBenchmark for (2888ds/28120Mi)
% 121.30/17.49 % Detected minimum model sizes of [51]
% 121.30/17.49 % Detected maximum model sizes of [max]
% 121.30/17.49 % (3874891)Cannot represent all propositional literals internally
% 121.30/17.49 % (3874891)Refutation not found, incomplete strategy
% 121.30/17.49 % (3874891)------------------------------
% 121.30/17.49 % (3874891)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 121.30/17.49 % (3874891)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 121.30/17.49 % (3874891)CaDiCaL version: 2.1.3
% 121.30/17.49 % (3874891)Termination reason: Refutation not found, incomplete strategy
% 121.30/17.49 % (3874891)Time elapsed: 0.349 s
% 121.30/17.49 % (3874891)Peak memory usage: 46 MB
% 121.30/17.49 % (3874891)Instructions burned: 1286 (million)
% 121.30/17.49 % (3874891)------------------------------
% 121.30/17.49 % (3874891)------------------------------
% 121.30/17.49 % (3874895)fmb+10_1_sil=256000:fmbss=7:random_seed=1470947723:fmbsr=1.6:i=182295_2885 on theBenchmark for (2885ds/182295Mi)
% 121.30/17.49 % Detected minimum model sizes of [51]
% 121.30/17.49 % Detected maximum model sizes of [max]
% 121.30/17.49 % (3874895)Cannot represent all propositional literals internally
% 121.30/17.49 % (3874895)Refutation not found, incomplete strategy
% 121.30/17.49 % (3874895)------------------------------
% 121.30/17.49 % (3874895)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 121.30/17.49 % (3874895)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 121.30/17.49 % (3874895)CaDiCaL version: 2.1.3
% 134.03/19.23 % (3874895)Termination reason: Refutation not found, incomplete strategy
% 134.03/19.23 % (3874895)Time elapsed: 0.354 s
% 134.03/19.23 % (3874895)Peak memory usage: 46 MB
% 134.03/19.23 % (3874895)Instructions burned: 1286 (million)
% 134.03/19.23 % (3874895)------------------------------
% 134.03/19.23 % (3874895)------------------------------
% 134.03/19.23 % (3874897)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=425980589:i=44625:gsp=on_2881 on theBenchmark for (2881ds/44625Mi)
% 134.03/19.23 % Detected minimum model sizes of [51]
% 134.03/19.23 % Detected maximum model sizes of [max]
% 134.03/19.23 % (3874897)Cannot represent all propositional literals internally
% 134.03/19.23 % (3874897)Refutation not found, incomplete strategy
% 134.03/19.23 % (3874897)------------------------------
% 134.03/19.23 % (3874897)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 134.03/19.23 % (3874897)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 134.03/19.23 % (3874897)CaDiCaL version: 2.1.3
% 134.03/19.23 % (3874897)Termination reason: Refutation not found, incomplete strategy
% 134.03/19.23 % (3874897)Time elapsed: 0.379 s
% 134.03/19.23 % (3874897)Peak memory usage: 48 MB
% 134.03/19.23 % (3874897)Instructions burned: 1362 (million)
% 134.03/19.23 % (3874897)------------------------------
% 134.03/19.23 % (3874897)------------------------------
% 134.03/19.23 % (3874899)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=3945884261:i=160505_2877 on theBenchmark for (2877ds/160505Mi)
% 134.03/19.23 % Detected minimum model sizes of [51]
% 134.03/19.23 % Detected maximum model sizes of [max]
% 134.03/19.23 % (3874899)Cannot represent all propositional literals internally
% 134.03/19.23 % (3874899)Refutation not found, incomplete strategy
% 134.03/19.23 % (3874899)------------------------------
% 134.03/19.23 % (3874899)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 134.03/19.23 % (3874899)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 134.03/19.23 % (3874899)CaDiCaL version: 2.1.3
% 134.03/19.23 % (3874899)Termination reason: Refutation not found, incomplete strategy
% 134.03/19.23 % (3874899)Time elapsed: 0.354 s
% 134.03/19.23 % (3874899)Peak memory usage: 46 MB
% 134.03/19.23 % (3874899)Instructions burned: 1286 (million)
% 134.03/19.23 % (3874899)------------------------------
% 134.03/19.23 % (3874899)------------------------------
% 134.03/19.23 % (3874901)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=3661696900:fmbsr=1.3:i=225729_2873 on theBenchmark for (2873ds/225729Mi)
% 134.03/19.23 % Detected minimum model sizes of [51]
% 134.03/19.23 % Detected maximum model sizes of [max]
% 134.03/19.23 % (3874901)Cannot represent all propositional literals internally
% 134.03/19.23 % (3874901)Refutation not found, incomplete strategy
% 134.03/19.23 % (3874901)------------------------------
% 134.03/19.23 % (3874901)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 134.03/19.23 % (3874901)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 134.03/19.23 % (3874901)CaDiCaL version: 2.1.3
% 134.03/19.23 % (3874901)Termination reason: Refutation not found, incomplete strategy
% 134.03/19.23 % (3874901)Time elapsed: 0.353 s
% 134.03/19.23 % (3874901)Peak memory usage: 46 MB
% 134.03/19.23 % (3874901)Instructions burned: 1286 (million)
% 134.03/19.23 % (3874901)------------------------------
% 134.03/19.23 % (3874901)------------------------------
% 134.03/19.23 % (3874903)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=400073063:fmbsr=2:i=185024:ins=7_2869 on theBenchmark for (2869ds/185024Mi)
% 134.03/19.23 % Detected minimum model sizes of [51]
% 134.03/19.23 % Detected maximum model sizes of [max]
% 134.03/19.23 % (3874903)Cannot represent all propositional literals internally
% 134.03/19.23 % (3874903)Refutation not found, incomplete strategy
% 134.03/19.23 % (3874903)------------------------------
% 134.03/19.23 % (3874903)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 134.03/19.23 % (3874903)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 134.03/19.23 % (3874903)CaDiCaL version: 2.1.3
% 134.03/19.23 % (3874903)Termination reason: Refutation not found, incomplete strategy
% 134.03/19.23 % (3874903)Time elapsed: 0.358 s
% 134.03/19.23 % (3874903)Peak memory usage: 46 MB
% 134.03/19.23 % (3874903)Instructions burned: 1286 (million)
% 134.03/19.23 % (3874903)------------------------------
% 134.03/19.23 % (3874903)------------------------------
% 134.03/19.23 % (3874905)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=1980082118:rtra=on_2865 on theBenchmark for (2865ds/0Mi)
% 134.03/19.23 % Detected minimum model sizes of [51]
% 134.03/19.23 % Detected maximum model sizes of [max]
% 134.03/19.23 % (3874905)Cannot represent all propositional literals internally
% 134.03/19.23 % (3874905)Refutation not found, incomplete strategy
% 154.10/22.14 % (3874905)------------------------------
% 154.10/22.14 % (3874905)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 154.10/22.14 % (3874905)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 154.10/22.14 % (3874905)CaDiCaL version: 2.1.3
% 154.10/22.14 % (3874905)Termination reason: Refutation not found, incomplete strategy
% 154.10/22.14 % (3874905)Time elapsed: 0.512 s
% 154.10/22.14 % (3874905)Peak memory usage: 55 MB
% 154.10/22.14 % (3874905)Instructions burned: 1545 (million)
% 154.10/22.14 % (3874905)------------------------------
% 154.10/22.14 % (3874905)------------------------------
% 154.10/22.14 % (3874907)% WARNING: option uhcvi not known.
% 154.10/22.14 % (3874907)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=576577800:i=271062:add=off:rtra=on:rawr=on_2860 on theBenchmark for (2860ds/271062Mi)
% 154.10/22.14 % (3874885)Instruction limit reached!
% 154.10/22.14 % (3874885)------------------------------
% 154.10/22.14 % (3874885)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 154.10/22.14 % (3874885)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 154.10/22.14 % (3874885)CaDiCaL version: 2.1.3
% 154.10/22.14 % (3874885)Termination reason: Instruction limit
% 154.10/22.14 % (3874885)Termination phase: Saturation
% 154.10/22.14 % (3874885)Time elapsed: 3.809 s
% 154.10/22.14 % (3874885)Peak memory usage: 89 MB
% 154.10/22.14 % (3874885)Instructions burned: 15856 (million)
% 154.10/22.14 % (3874909)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=4232814797:i=176048:add=on:rtra=on:rawr=on_2859 on theBenchmark for (2859ds/176048Mi)
% 154.10/22.14 % (3874887)Instruction limit reached!
% 154.10/22.14 % (3874887)------------------------------
% 154.10/22.14 % (3874887)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 154.10/22.14 % (3874887)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 154.10/22.14 % (3874887)CaDiCaL version: 2.1.3
% 154.10/22.14 % (3874887)Termination reason: Instruction limit
% 154.10/22.14 % (3874887)Termination phase: Saturation
% 154.10/22.14 % (3874887)Time elapsed: 6.585 s
% 154.10/22.14 % (3874887)Peak memory usage: 650 MB
% 154.10/22.14 % (3874887)Instructions burned: 17627 (million)
% 154.10/22.14 % (3874911)dis+10_1_sil=32000:si=on:sp=arity:random_seed=1431408348:i=206:fgj=on:rtra=on_2830 on theBenchmark for (2830ds/206Mi)
% 154.10/22.14 % (3874911)Instruction limit reached!
% 154.10/22.14 % (3874911)------------------------------
% 154.10/22.14 % (3874911)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 154.10/22.14 % (3874911)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 154.10/22.14 % (3874911)CaDiCaL version: 2.1.3
% 154.10/22.14 % (3874911)Termination reason: Instruction limit
% 154.10/22.14 % (3874911)Termination phase: Property scanning
% 154.10/22.14 % (3874911)Time elapsed: 0.093 s
% 154.10/22.14 % (3874911)Peak memory usage: 28 MB
% 154.10/22.14 % (3874911)Instructions burned: 209 (million)
% 154.10/22.14 % (3874913)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=2579943994:i=232:rtra=on_2828 on theBenchmark for (2828ds/232Mi)
% 154.10/22.14 % (3874913)Instruction limit reached!
% 154.10/22.14 % (3874913)------------------------------
% 154.10/22.14 % (3874913)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 154.10/22.14 % (3874913)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 154.10/22.14 % (3874913)CaDiCaL version: 2.1.3
% 154.10/22.14 % (3874913)Termination reason: Instruction limit
% 154.10/22.14 % (3874913)Termination phase: Property scanning
% 154.10/22.14 % (3874913)Time elapsed: 0.095 s
% 154.10/22.14 % (3874913)Peak memory usage: 29 MB
% 154.10/22.14 % (3874913)Instructions burned: 234 (million)
% 154.10/22.14 % (3874915)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=3643631492:i=262:rtra=on_2827 on theBenchmark for (2827ds/262Mi)
% 154.10/22.14 % (3874915)Instruction limit reached!
% 154.10/22.14 % (3874915)------------------------------
% 154.10/22.14 % (3874915)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 154.10/22.14 % (3874915)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 154.10/22.14 % (3874915)CaDiCaL version: 2.1.3
% 154.10/22.14 % (3874915)Termination reason: Instruction limit
% 154.10/22.14 % (3874915)Termination phase: Saturation
% 154.10/22.14 % (3874915)Time elapsed: 0.100 s
% 154.10/22.14 % (3874915)Peak memory usage: 28 MB
% 154.10/22.14 % (3874915)Instructions burned: 266 (million)
% 154.10/22.14 % (3874917)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=381197672:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2826 on theBenchmark for (2826ds/318Mi)
% 177.80/25.43 % (3874917)Instruction limit reached!
% 177.80/25.43 % (3874917)------------------------------
% 177.80/25.43 % (3874917)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 177.80/25.43 % (3874917)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 177.80/25.43 % (3874917)CaDiCaL version: 2.1.3
% 177.80/25.43 % (3874917)Termination reason: Instruction limit
% 177.80/25.43 % (3874917)Termination phase: Saturation
% 177.80/25.43 % (3874917)Time elapsed: 0.119 s
% 177.80/25.43 % (3874917)Peak memory usage: 29 MB
% 177.80/25.43 % (3874917)Instructions burned: 318 (million)
% 177.80/25.43 % (3874919)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=3706960235:i=1428:nm=2:rtra=on_2825 on theBenchmark for (2825ds/1428Mi)
% 177.80/25.43 % Detected minimum model sizes of [51]
% 177.80/25.43 % Detected maximum model sizes of [max]
% 177.80/25.43 % (3874919)Cannot represent all propositional literals internally
% 177.80/25.43 % (3874919)Refutation not found, incomplete strategy
% 177.80/25.43 % (3874919)------------------------------
% 177.80/25.43 % (3874919)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 177.80/25.43 % (3874919)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 177.80/25.43 % (3874919)CaDiCaL version: 2.1.3
% 177.80/25.43 % (3874919)Termination reason: Refutation not found, incomplete strategy
% 177.80/25.43 % (3874919)Time elapsed: 0.417 s
% 177.80/25.43 % (3874919)Peak memory usage: 47 MB
% 177.80/25.43 % (3874919)Instructions burned: 1336 (million)
% 177.80/25.43 % (3874919)------------------------------
% 177.80/25.43 % (3874919)------------------------------
% 177.80/25.43 % (3874921)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=562179928:i=262:bd=preordered:rtra=on:fsd=on_2820 on theBenchmark for (2820ds/262Mi)
% 177.80/25.43 % (3874921)Instruction limit reached!
% 177.80/25.43 % (3874921)------------------------------
% 177.80/25.43 % (3874921)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 177.80/25.43 % (3874921)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 177.80/25.43 % (3874921)CaDiCaL version: 2.1.3
% 177.80/25.43 % (3874921)Termination reason: Instruction limit
% 177.80/25.43 % (3874921)Termination phase: Blocked clause elimination
% 177.80/25.43 % (3874921)Time elapsed: 0.114 s
% 177.80/25.43 % (3874921)Peak memory usage: 30 MB
% 177.80/25.43 % (3874921)Instructions burned: 262 (million)
% 177.80/25.43 % (3874923)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:si=on:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=229078661:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2819 on theBenchmark for (2819ds/1368Mi)
% 177.80/25.43 % (3874923)Instruction limit reached!
% 177.80/25.43 % (3874923)------------------------------
% 177.80/25.43 % (3874923)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 177.80/25.43 % (3874923)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 177.80/25.43 % (3874923)CaDiCaL version: 2.1.3
% 177.80/25.43 % (3874923)Termination reason: Instruction limit
% 177.80/25.43 % (3874923)Termination phase: Saturation
% 177.80/25.43 % (3874923)Time elapsed: 0.471 s
% 177.80/25.43 % (3874923)Peak memory usage: 37 MB
% 177.80/25.43 % (3874923)Instructions burned: 1371 (million)
% 177.80/25.43 % (3874925)ott-21_1_sil=16000:si=on:fs=off:random_seed=121562055:i=360:av=off:fsr=off:rtra=on_2814 on theBenchmark for (2814ds/360Mi)
% 177.80/25.43 % (3874925)Instruction limit reached!
% 177.80/25.43 % (3874925)------------------------------
% 177.80/25.43 % (3874925)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 177.80/25.43 % (3874925)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 177.80/25.43 % (3874925)CaDiCaL version: 2.1.3
% 177.80/25.43 % (3874925)Termination reason: Instruction limit
% 177.80/25.43 % (3874925)Termination phase: Saturation
% 177.80/25.43 % (3874925)Time elapsed: 0.144 s
% 177.80/25.43 % (3874925)Peak memory usage: 29 MB
% 177.80/25.43 % (3874925)Instructions burned: 361 (million)
% 177.80/25.43 % (3874927)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2987245011:i=954:bd=all:rtra=on_2812 on theBenchmark for (2812ds/954Mi)
% 177.80/25.43 % (3874927)Instruction limit reached!
% 177.80/25.43 % (3874927)------------------------------
% 177.80/25.43 % (3874927)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 177.80/25.43 % (3874927)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 177.80/25.43 % (3874927)CaDiCaL version: 2.1.3
% 177.80/25.43 % (3874927)Termination reason: Instruction limit
% 106.52/26.39 % (3874927)Termination phase: Saturation
% 106.52/26.39 % (3874927)Time elapsed: 0.339 s
% 106.52/26.39 % (3874927)Peak memory usage: 36 MB
% 106.52/26.39 % (3874927)Instructions burned: 957 (million)
% 106.52/26.39 % (3874929)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=2226152499:fmbsr=1.3:i=1730:ins=25:rtra=on_2808 on theBenchmark for (2808ds/1730Mi)
% 106.52/26.39 % Detected minimum model sizes of [51]
% 106.52/26.39 % Detected maximum model sizes of [max]
% 106.52/26.39 % (3874929)Cannot represent all propositional literals internally
% 106.52/26.39 % (3874929)Refutation not found, incomplete strategy
% 106.52/26.39 % (3874929)------------------------------
% 106.52/26.39 % (3874929)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 106.52/26.39 % (3874929)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 106.52/26.39 % (3874929)CaDiCaL version: 2.1.3
% 106.52/26.39 % (3874929)Termination reason: Refutation not found, incomplete strategy
% 106.52/26.39 % (3874929)Time elapsed: 0.413 s
% 106.52/26.39 % (3874929)Peak memory usage: 49 MB
% 106.52/26.39 % (3874929)Instructions burned: 1273 (million)
% 106.52/26.39 % (3874929)------------------------------
% 106.52/26.39 % (3874929)------------------------------
% 106.52/26.39 % (3874931)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=2515598506:i=2358:rtra=on_2804 on theBenchmark for (2804ds/2358Mi)
% 106.52/26.39 % (3874931)Instruction limit reached!
% 106.52/26.39 % (3874931)------------------------------
% 106.52/26.39 % (3874931)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 106.52/26.39 % (3874931)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 106.52/26.39 % (3874931)CaDiCaL version: 2.1.3
% 106.52/26.39 % (3874931)Termination reason: Instruction limit
% 106.52/26.39 % (3874931)Termination phase: Saturation
% 106.52/26.39 % (3874931)Time elapsed: 0.831 s
% 106.52/26.39 % (3874931)Peak memory usage: 47 MB
% 106.52/26.39 % (3874931)Instructions burned: 2358 (million)
% 106.52/26.39 % (3874933)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=3396344530:i=1778:ins=1:rtra=on_2795 on theBenchmark for (2795ds/1778Mi)
% 106.52/26.39 % (3874933)Cannot represent all propositional literals internally
% 106.52/26.39 % (3874933)Refutation not found, incomplete strategy
% 106.52/26.39 % (3874933)------------------------------
% 106.52/26.39 % (3874933)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 106.52/26.39 % (3874933)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 106.52/26.39 % (3874933)CaDiCaL version: 2.1.3
% 106.52/26.39 % (3874933)Termination reason: Refutation not found, incomplete strategy
% 106.52/26.39 % (3874933)Time elapsed: 0.444 s
% 106.52/26.39 % (3874933)Peak memory usage: 50 MB
% 106.52/26.39 % (3874933)Instructions burned: 1328 (million)
% 106.52/26.39 % (3874933)------------------------------
% 106.52/26.39 % (3874933)------------------------------
% 106.52/26.39 % (3874935)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:si=on:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=976648502:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2791 on theBenchmark for (2791ds/1384Mi)
% 106.52/26.39 % (3874935)Instruction limit reached!
% 106.52/26.39 % (3874935)------------------------------
% 106.52/26.39 % (3874935)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 106.52/26.39 % (3874935)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 106.52/26.39 % (3874935)CaDiCaL version: 2.1.3
% 106.52/26.39 % (3874935)Termination reason: Instruction limit
% 106.52/26.39 % (3874935)Termination phase: Saturation
% 106.52/26.39 % (3874935)Time elapsed: 0.532 s
% 106.52/26.39 % (3874935)Peak memory usage: 48 MB
% 106.52/26.39 % (3874935)Instructions burned: 1384 (million)
% 106.52/26.39 % (3874937)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=1059818058:i=1758:kws=inv_precedence:fsr=off:rtra=on_2785 on theBenchmark for (2785ds/1758Mi)
% 106.52/26.39 % (3874937)Instruction limit reached!
% 106.52/26.39 % (3874937)------------------------------
% 106.52/26.39 % (3874937)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 106.52/26.39 % (3874937)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 106.52/26.39 % (3874937)CaDiCaL version: 2.1.3
% 106.52/26.39 % (3874937)Termination reason: Instruction limit
% 106.52/26.39 % (3874937)Termination phase: Saturation
% 106.52/26.39 % (3874937)Time elapsed: 0.517 s
% 106.52/26.39 % (3874937)Peak memory usage: 41 MB
% 106.52/26.39 % (3874937)Instructions burned: 1758 (million)
% 106.52/26.39 % (3874939)fmb+10_1_sil=64000:si=on:random_seed=807715693:i=44122:nm=2:rtra=on:gsp=on_2780 on theBenchmark for (2780ds/44122Mi)
% 106.52/26.39 % Detected minimum model sizes of [51]
% 106.52/26.39 % Detected maximum model sizes of [max]
% 106.52/26.39 % (3874939)Cannot represent all propositional literals internally
% 106.52/26.39 % (3874939)Refutation not found, incomplete strategy
% 106.52/26.39 % (3874939)------------------------------
% 106.52/26.39 % (3874939)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 106.52/26.39 % (3874939)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 106.52/26.39 % (3874939)CaDiCaL version: 2.1.3
% 106.52/26.39 % (3874939)Termination reason: Refutation not found, incomplete strategy
% 106.52/26.39 % (3874939)Time elapsed: 0.401 s
% 106.52/26.39 % (3874939)Peak memory usage: 46 MB
% 106.52/26.39 % (3874939)Instructions burned: 1213 (million)
% 106.52/26.39 % (3874939)------------------------------
% 106.52/26.39 % (3874939)------------------------------
% 106.52/26.39 % (3874941)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=1299491802:i=19030:nm=5:rtra=on_2775 on theBenchmark for (2775ds/19030Mi)
% 106.52/26.39 % Detected minimum model sizes of [51]
% 106.52/26.39 % Detected maximum model sizes of [max]
% 106.52/26.39 % (3874941)Cannot represent all propositional literals internally
% 106.52/26.39 % (3874941)Refutation not found, incomplete strategy
% 106.52/26.39 % (3874941)------------------------------
% 106.52/26.39 % (3874941)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 106.52/26.39 % (3874941)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 106.52/26.39 % (3874941)CaDiCaL version: 2.1.3
% 106.52/26.39 % (3874941)Termination reason: Refutation not found, incomplete strategy
% 106.52/26.39 % (3874941)Time elapsed: 0.417 s
% 106.52/26.39 % (3874941)Peak memory usage: 47 MB
% 106.52/26.39 % (3874941)Instructions burned: 1291 (million)
% 106.52/26.39 % (3874941)------------------------------
% 106.52/26.39 % (3874941)------------------------------
% 106.52/26.39 % (3874943)fmb+10_1_sil=64000:sas=cadical:si=on:fmbss=8:random_seed=762227551:fmbsr=1.7:i=1840:rtra=on_2771 on theBenchmark for (2771ds/1840Mi)
% 106.52/26.39 % Detected minimum model sizes of [51]
% 106.52/26.39 % Detected maximum model sizes of [max]
% 106.52/26.39 % (3874943)Cannot represent all propositional literals internally
% 106.52/26.39 % (3874943)Refutation not found, incomplete strategy
% 106.52/26.39 % (3874943)------------------------------
% 106.52/26.39 % (3874943)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 106.52/26.39 % (3874943)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 106.52/26.39 % (3874943)CaDiCaL version: 2.1.3
% 106.52/26.39 % (3874943)Termination reason: Refutation not found, incomplete strategy
% 106.52/26.39 % (3874943)Time elapsed: 0.427 s
% 106.52/26.39 % (3874943)Peak memory usage: 49 MB
% 106.52/26.39 % (3874943)Instructions burned: 1319 (million)
% 106.52/26.39 % (3874943)------------------------------
% 106.52/26.39 % (3874943)------------------------------
% 106.52/26.39 % (3874945)dis-4_1_sil=16000:drc=ordering:si=on:sp=const_frequency:sac=on:newcnf=on:random_seed=2129747064:i=10262:rtra=on_2766 on theBenchmark for (2766ds/10262Mi)
% 106.52/26.39 % (3874893)Instruction limit reached!
% 106.52/26.39 % (3874893)------------------------------
% 106.52/26.39 % (3874893)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 106.52/26.39 % (3874893)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 106.52/26.39 % (3874893)CaDiCaL version: 2.1.3
% 106.52/26.39 % (3874893)Termination reason: Instruction limit
% 106.52/26.39 % (3874893)Termination phase: Saturation
% 106.52/26.39 % (3874893)Time elapsed: 13.356 s
% 106.52/26.39 % (3874893)Peak memory usage: 690 MB
% 106.52/26.39 % (3874893)Instructions burned: 28121 (million)
% 106.52/26.39 % (3874947)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:si=on:sp=arity:spb=units:lsd=10:nwc=3:random_seed=393200680:i=2944:ins=7:rtra=on:fdi=8:gsp=on_2753 on theBenchmark for (2753ds/2944Mi)
% 106.52/26.39 % (3874889)Instruction limit reached!
% 106.52/26.39 % (3874889)------------------------------
% 106.52/26.39 % (3874889)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 106.52/26.39 % (3874889)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 106.52/26.39 % (3874889)CaDiCaL version: 2.1.3
% 106.52/26.39 % (3874889)Termination reason: Instruction limit
% 106.52/26.39 % (3874889)Termination phase: Saturation
% 106.52/26.39 % (3874889)Time elapsed: 14.670 s
% 106.52/26.39 % (3874889)Peak memory usage: 155 MB
% 106.52/26.39 % (3874889)Instructions burned: 53297 (million)
% 106.52/26.39 % (3874949)fmb+10_1_sil=16000:sas=cadical:si=on:bce=on:fmbss=77:random_seed=3532682510:i=12648:rtra=on_2747 on theBenchmark for (2747ds/12648Mi)
% 106.52/26.39 % (3874947)Instruction limit reached!
% 106.52/26.39 % (3874947)------------------------------
% 106.52/26.39 % (3874947)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 106.52/26.39 % (3874947)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 106.52/26.39 % (3874947)CaDiCaL version: 2.1.3
% 106.52/26.39 % (3874947)Termination reason: Instruction limit
% 106.52/26.39 % (3874947)Termination phase: Saturation
% 106.52/26.39 % (3874947)Time elapsed: 1.003 s
% 106.52/26.39 % (3874947)Peak memory usage: 56 MB
% 106.52/26.39 % (3874947)Instructions burned: 2944 (million)
% 106.52/26.39 % (3874951)fmb+10_1_fmbas=function:sil=32000:sas=cadical:si=on:fmbss=16:random_seed=2018445215:fmbsr=2.30978:i=4348:rtra=on_2743 on theBenchmark for (2743ds/4348Mi)
% 106.52/26.39 % Detected minimum model sizes of [51]
% 106.52/26.39 % Detected maximum model sizes of [max]
% 106.52/26.39 % (3874949)Cannot represent all propositional literals internally
% 106.52/26.39 % (3874949)Refutation not found, incomplete strategy
% 106.52/26.39 % (3874949)------------------------------
% 106.52/26.39 % (3874949)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 106.52/26.39 % (3874949)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 106.52/26.39 % (3874949)CaDiCaL version: 2.1.3
% 106.52/26.39 % (3874949)Termination reason: Refutation not found, incomplete strategy
% 106.52/26.39 % (3874949)Time elapsed: 0.484 s
% 106.52/26.39 % (3874949)Peak memory usage: 54 MB
% 106.52/26.39 % (3874949)Instructions burned: 1502 (million)
% 106.52/26.39 % (3874949)------------------------------
% 106.52/26.39 % (3874949)------------------------------
% 106.52/26.39 % (3874953)ott-2_1_sil=16000:si=on:newcnf=on:random_seed=1187809533:avsq=on:i=1738:avsqr=1,16:kws=inv_arity_squared:rtra=on_2741 on theBenchmark for (2741ds/1738Mi)
% 106.52/26.39 % (3874945) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-3874792-3874945"...
% 106.52/26.39 % (3874945)...printing done.
% 106.52/26.39 % (3874945)Refutation found. Thanks to Tanya!
% 106.52/26.39 % SZS status Theorem for theBenchmark
% 106.52/26.39 % SZS output start Proof for theBenchmark
% See solution above
% 183.87/26.40 % (3874945)------------------------------
% 183.87/26.40 % (3874945)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 183.87/26.40 % (3874945)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 183.87/26.40 % (3874945)CaDiCaL version: 2.1.3
% 183.87/26.40 % (3874945)Termination reason: Refutation
% 183.87/26.40 % (3874945)Time elapsed: 2.700 s
% 183.87/26.40 % (3874945)Peak memory usage: 70 MB
% 183.87/26.40 % (3874945)Instructions burned: 7611 (million)
% 183.87/26.40 % (3874792)Success in time 26.268 s
% 183.87/26.40 % Vampire exiting
%------------------------------------------------------------------------------