%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : CSR090+4 : TPTP v9.3.1. Bugfixed v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n006.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:08 AM UTC 2026
% Result : Theorem 168.51s 34.04s
% Output : Refutation 238.32s
% Verified :
% SZS Type : Refutation
% Derivation depth : 12
% Number of leaves : 29
% Syntax : Number of formulae : 129 ( 50 unt; 18 def)
% Number of atoms : 331 ( 0 equ)
% Maximal formula atoms : 7 ( 2 avg)
% Number of connectives : 377 ( 175 ~; 172 |; 7 &)
% ( 18 <=>; 5 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 3 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 22 ( 21 usr; 19 prp; 0-2 aty)
% Number of functors : 7 ( 7 usr; 7 con; 0-0 aty)
% Number of variables : 56 ( 0 sgn 56 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f26,axiom,
! [X0,X1] :
( s__subclass(X0,X1)
=> ( s__instance(X0,s__SetOrClass)
& s__instance(X1,s__SetOrClass) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR003+0.ax',kb_SUMO_26) ).
fof(f27,axiom,
! [X0,X1,X2] :
( ( s__instance(X1,s__SetOrClass)
& s__instance(X0,s__SetOrClass) )
=> ( ( s__subclass(X0,X1)
& s__instance(X2,X0) )
=> s__instance(X2,X1) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR003+0.ax',kb_SUMO_27) ).
fof(f905,axiom,
s__subclass(s__TimeInterval,s__TimePosition),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR003+0.ax',kb_SUMO_908) ).
fof(f1259,axiom,
! [X0,X1,X2] :
( ( s__instance(X2,s__TimePosition)
& s__instance(X1,s__TimePosition)
& s__instance(X0,s__TimePosition) )
=> ( ( s__temporalPart(X0,X1)
& s__temporalPart(X1,X2) )
=> s__temporalPart(X0,X2) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR003+0.ax',kb_SUMO_1262) ).
fof(f4485,axiom,
s__subclass(s__Year,s__TimeInterval),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR003+0.ax',kb_SUMO_4500) ).
fof(f7218,axiom,
s__instance(s__Time17_1,s__TimeInterval),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',local_1) ).
fof(f7219,axiom,
s__instance(s__Time17_2,s__TimeInterval),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',local_2) ).
fof(f7220,axiom,
s__instance(s__Time17_3,s__TimeInterval),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',local_3) ).
fof(f7221,axiom,
s__temporalPart(s__Time17_1,s__Time17_2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',local_4) ).
fof(f7222,axiom,
s__temporalPart(s__Time17_2,s__Time17_3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',local_5) ).
fof(f7223,conjecture,
s__temporalPart(s__Time17_1,s__Time17_3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_from_SUMO) ).
fof(f7224,negated_conjecture,
~ s__temporalPart(s__Time17_1,s__Time17_3),
inference(negated_conjecture,[status(cth)],[f7223]) ).
fof(f7228,plain,
~ s__temporalPart(s__Time17_1,s__Time17_3),
inference(flattening,[],[f7224]) ).
fof(f7319,plain,
! [X0,X1] :
( ( s__instance(X0,s__SetOrClass)
& s__instance(X1,s__SetOrClass) )
| ~ s__subclass(X0,X1) ),
inference(ennf_transformation,[],[f26]) ).
fof(f7320,plain,
! [X0,X1,X2] :
( s__instance(X2,X1)
| ~ s__subclass(X0,X1)
| ~ s__instance(X2,X0)
| ~ s__instance(X1,s__SetOrClass)
| ~ s__instance(X0,s__SetOrClass) ),
inference(ennf_transformation,[],[f27]) ).
fof(f7321,plain,
! [X0,X1,X2] :
( s__instance(X2,X1)
| ~ s__subclass(X0,X1)
| ~ s__instance(X2,X0)
| ~ s__instance(X1,s__SetOrClass)
| ~ s__instance(X0,s__SetOrClass) ),
inference(flattening,[],[f7320]) ).
fof(f8479,plain,
! [X0,X1,X2] :
( s__temporalPart(X0,X2)
| ~ s__temporalPart(X0,X1)
| ~ s__temporalPart(X1,X2)
| ~ s__instance(X2,s__TimePosition)
| ~ s__instance(X1,s__TimePosition)
| ~ s__instance(X0,s__TimePosition) ),
inference(ennf_transformation,[],[f1259]) ).
fof(f8480,plain,
! [X0,X1,X2] :
( s__temporalPart(X0,X2)
| ~ s__temporalPart(X0,X1)
| ~ s__temporalPart(X1,X2)
| ~ s__instance(X2,s__TimePosition)
| ~ s__instance(X1,s__TimePosition)
| ~ s__instance(X0,s__TimePosition) ),
inference(flattening,[],[f8479]) ).
fof(f14338,plain,
! [X0,X1] :
( s__instance(X1,s__SetOrClass)
| ~ s__subclass(X0,X1) ),
inference(cnf_transformation,[],[f7319]) ).
fof(f14340,plain,
! [X2,X0,X1] :
( s__instance(X2,X1)
| ~ s__subclass(X0,X1)
| ~ s__instance(X2,X0)
| ~ s__instance(X1,s__SetOrClass)
| ~ s__instance(X0,s__SetOrClass) ),
inference(cnf_transformation,[],[f7321]) ).
fof(f15299,plain,
s__subclass(s__TimeInterval,s__TimePosition),
inference(cnf_transformation,[],[f905]) ).
fof(f15725,plain,
! [X2,X0,X1] :
( s__temporalPart(X0,X2)
| ~ s__temporalPart(X0,X1)
| ~ s__temporalPart(X1,X2)
| ~ s__instance(X2,s__TimePosition)
| ~ s__instance(X1,s__TimePosition)
| ~ s__instance(X0,s__TimePosition) ),
inference(cnf_transformation,[],[f8480]) ).
fof(f19176,plain,
s__subclass(s__Year,s__TimeInterval),
inference(cnf_transformation,[],[f4485]) ).
fof(f22560,plain,
s__instance(s__Time17_1,s__TimeInterval),
inference(cnf_transformation,[],[f7218]) ).
fof(f22561,plain,
s__instance(s__Time17_2,s__TimeInterval),
inference(cnf_transformation,[],[f7219]) ).
fof(f22562,plain,
s__instance(s__Time17_3,s__TimeInterval),
inference(cnf_transformation,[],[f7220]) ).
fof(f22563,plain,
s__temporalPart(s__Time17_1,s__Time17_2),
inference(cnf_transformation,[],[f7221]) ).
fof(f22564,plain,
s__temporalPart(s__Time17_2,s__Time17_3),
inference(cnf_transformation,[],[f7222]) ).
fof(f22565,plain,
~ s__temporalPart(s__Time17_1,s__Time17_3),
inference(cnf_transformation,[],[f7228]) ).
fof(f22955,definition,
( spl504_1
<=> s__temporalPart(s__Time17_1,s__Time17_3) ),
introduced(definition,[new_symbols(definition,[spl504_1])],[avatar_definition]) ).
fof(f22957,plain,
( ~ s__temporalPart(s__Time17_1,s__Time17_3)
| spl504_1 ),
inference(avatar_component_clause,[],[f22955]) ).
fof(f22958,plain,
~ spl504_1,
inference(avatar_split_clause,[],[f22565,f22955]) ).
fof(f22960,definition,
( spl504_2
<=> s__temporalPart(s__Time17_2,s__Time17_3) ),
introduced(definition,[new_symbols(definition,[spl504_2])],[avatar_definition]) ).
fof(f22962,plain,
( s__temporalPart(s__Time17_2,s__Time17_3)
| ~ spl504_2 ),
inference(avatar_component_clause,[],[f22960]) ).
fof(f22963,plain,
spl504_2,
inference(avatar_split_clause,[],[f22564,f22960]) ).
fof(f22965,definition,
( spl504_3
<=> s__temporalPart(s__Time17_1,s__Time17_2) ),
introduced(definition,[new_symbols(definition,[spl504_3])],[avatar_definition]) ).
fof(f22967,plain,
( s__temporalPart(s__Time17_1,s__Time17_2)
| ~ spl504_3 ),
inference(avatar_component_clause,[],[f22965]) ).
fof(f22968,plain,
spl504_3,
inference(avatar_split_clause,[],[f22563,f22965]) ).
fof(f22970,definition,
( spl504_4
<=> s__instance(s__Time17_3,s__TimeInterval) ),
introduced(definition,[new_symbols(definition,[spl504_4])],[avatar_definition]) ).
fof(f22972,plain,
( s__instance(s__Time17_3,s__TimeInterval)
| ~ spl504_4 ),
inference(avatar_component_clause,[],[f22970]) ).
fof(f22973,plain,
spl504_4,
inference(avatar_split_clause,[],[f22562,f22970]) ).
fof(f22975,definition,
( spl504_5
<=> s__instance(s__Time17_2,s__TimeInterval) ),
introduced(definition,[new_symbols(definition,[spl504_5])],[avatar_definition]) ).
fof(f22977,plain,
( s__instance(s__Time17_2,s__TimeInterval)
| ~ spl504_5 ),
inference(avatar_component_clause,[],[f22975]) ).
fof(f22978,plain,
spl504_5,
inference(avatar_split_clause,[],[f22561,f22975]) ).
fof(f22980,definition,
( spl504_6
<=> s__instance(s__Time17_1,s__TimeInterval) ),
introduced(definition,[new_symbols(definition,[spl504_6])],[avatar_definition]) ).
fof(f22982,plain,
( s__instance(s__Time17_1,s__TimeInterval)
| ~ spl504_6 ),
inference(avatar_component_clause,[],[f22980]) ).
fof(f22983,plain,
spl504_6,
inference(avatar_split_clause,[],[f22560,f22980]) ).
fof(f43304,definition,
( spl504_4897
<=> s__subclass(s__Year,s__TimeInterval) ),
introduced(definition,[new_symbols(definition,[spl504_4897])],[avatar_definition]) ).
fof(f43306,plain,
( s__subclass(s__Year,s__TimeInterval)
| ~ spl504_4897 ),
inference(avatar_component_clause,[],[f43304]) ).
fof(f43307,plain,
spl504_4897,
inference(avatar_split_clause,[],[f19176,f43304]) ).
fof(f64566,definition,
( spl504_10300
<=> ! [X2,X0,X1] :
( s__temporalPart(X0,X2)
| ~ s__temporalPart(X0,X1)
| ~ s__temporalPart(X1,X2)
| ~ s__instance(X2,s__TimePosition)
| ~ s__instance(X1,s__TimePosition)
| ~ s__instance(X0,s__TimePosition) ) ),
introduced(definition,[new_symbols(definition,[spl504_10300])],[avatar_definition]) ).
fof(f64567,plain,
( ! [X2,X0,X1] :
( ~ s__temporalPart(X1,X2)
| ~ s__temporalPart(X0,X1)
| s__temporalPart(X0,X2)
| ~ s__instance(X2,s__TimePosition)
| ~ s__instance(X1,s__TimePosition)
| ~ s__instance(X0,s__TimePosition) )
| ~ spl504_10300 ),
inference(avatar_component_clause,[],[f64566]) ).
fof(f64568,plain,
spl504_10300,
inference(avatar_split_clause,[],[f15725,f64566]) ).
fof(f66642,definition,
( spl504_10829
<=> s__subclass(s__TimeInterval,s__TimePosition) ),
introduced(definition,[new_symbols(definition,[spl504_10829])],[avatar_definition]) ).
fof(f66644,plain,
( s__subclass(s__TimeInterval,s__TimePosition)
| ~ spl504_10829 ),
inference(avatar_component_clause,[],[f66642]) ).
fof(f66645,plain,
spl504_10829,
inference(avatar_split_clause,[],[f15299,f66642]) ).
fof(f71785,definition,
( spl504_12062
<=> ! [X2,X0,X1] :
( s__instance(X2,X1)
| ~ s__subclass(X0,X1)
| ~ s__instance(X2,X0)
| ~ s__instance(X1,s__SetOrClass)
| ~ s__instance(X0,s__SetOrClass) ) ),
introduced(definition,[new_symbols(definition,[spl504_12062])],[avatar_definition]) ).
fof(f71786,plain,
( ! [X2,X0,X1] :
( ~ s__subclass(X0,X1)
| s__instance(X2,X1)
| ~ s__instance(X2,X0)
| ~ s__instance(X1,s__SetOrClass)
| ~ s__instance(X0,s__SetOrClass) )
| ~ spl504_12062 ),
inference(avatar_component_clause,[],[f71785]) ).
fof(f71787,plain,
spl504_12062,
inference(avatar_split_clause,[],[f14340,f71785]) ).
fof(f71789,definition,
( spl504_12063
<=> ! [X0,X1] :
( s__instance(X1,s__SetOrClass)
| ~ s__subclass(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[spl504_12063])],[avatar_definition]) ).
fof(f71790,plain,
( ! [X0,X1] :
( ~ s__subclass(X0,X1)
| s__instance(X1,s__SetOrClass) )
| ~ spl504_12063 ),
inference(avatar_component_clause,[],[f71789]) ).
fof(f71791,plain,
spl504_12063,
inference(avatar_split_clause,[],[f14338,f71789]) ).
fof(f120271,definition,
( spl504_14070
<=> s__instance(s__Time17_2,s__TimePosition) ),
introduced(definition,[new_symbols(definition,[spl504_14070])],[avatar_definition]) ).
fof(f120272,plain,
( s__instance(s__Time17_2,s__TimePosition)
| ~ spl504_14070 ),
inference(avatar_component_clause,[],[f120271]) ).
fof(f120273,plain,
( ~ s__instance(s__Time17_2,s__TimePosition)
| spl504_14070 ),
inference(avatar_component_clause,[],[f120271]) ).
fof(f120275,definition,
( spl504_14071
<=> s__instance(s__Time17_3,s__TimePosition) ),
introduced(definition,[new_symbols(definition,[spl504_14071])],[avatar_definition]) ).
fof(f120276,plain,
( s__instance(s__Time17_3,s__TimePosition)
| ~ spl504_14071 ),
inference(avatar_component_clause,[],[f120275]) ).
fof(f120284,definition,
( spl504_14073
<=> s__instance(s__Time17_1,s__TimePosition) ),
introduced(definition,[new_symbols(definition,[spl504_14073])],[avatar_definition]) ).
fof(f120285,plain,
( s__instance(s__Time17_1,s__TimePosition)
| ~ spl504_14073 ),
inference(avatar_component_clause,[],[f120284]) ).
fof(f120379,plain,
( ! [X0] :
( ~ s__temporalPart(X0,s__Time17_2)
| s__temporalPart(X0,s__Time17_3)
| ~ s__instance(s__Time17_3,s__TimePosition)
| ~ s__instance(s__Time17_2,s__TimePosition)
| ~ s__instance(X0,s__TimePosition) )
| ~ spl504_2
| ~ spl504_10300 ),
inference(resolution,[],[f64567,f22962]) ).
fof(f140441,plain,
( s__instance(s__TimeInterval,s__SetOrClass)
| ~ spl504_4897
| ~ spl504_12063 ),
inference(resolution,[],[f71790,f43306]) ).
fof(f140538,plain,
( s__instance(s__TimePosition,s__SetOrClass)
| ~ spl504_10829
| ~ spl504_12063 ),
inference(resolution,[],[f71790,f66644]) ).
fof(f142490,definition,
( spl504_18630
<=> s__instance(s__TimePosition,s__SetOrClass) ),
introduced(definition,[new_symbols(definition,[spl504_18630])],[avatar_definition]) ).
fof(f142492,plain,
( s__instance(s__TimePosition,s__SetOrClass)
| ~ spl504_18630 ),
inference(avatar_component_clause,[],[f142490]) ).
fof(f142493,plain,
( spl504_18630
| ~ spl504_10829
| ~ spl504_12063 ),
inference(avatar_split_clause,[],[f140538,f71789,f66642,f142490]) ).
fof(f142670,definition,
( spl504_18652
<=> s__instance(s__TimeInterval,s__SetOrClass) ),
introduced(definition,[new_symbols(definition,[spl504_18652])],[avatar_definition]) ).
fof(f142672,plain,
( s__instance(s__TimeInterval,s__SetOrClass)
| ~ spl504_18652 ),
inference(avatar_component_clause,[],[f142670]) ).
fof(f142678,plain,
( spl504_18652
| ~ spl504_4897
| ~ spl504_12063 ),
inference(avatar_split_clause,[],[f140441,f71789,f43304,f142670]) ).
fof(f149937,plain,
( ! [X0] :
( s__instance(X0,s__TimePosition)
| ~ s__instance(X0,s__TimeInterval)
| ~ s__instance(s__TimePosition,s__SetOrClass)
| ~ s__instance(s__TimeInterval,s__SetOrClass) )
| ~ spl504_10829
| ~ spl504_12062 ),
inference(resolution,[],[f71786,f66644]) ).
fof(f150830,plain,
( ! [X0] :
( s__instance(X0,s__TimePosition)
| ~ s__instance(X0,s__TimeInterval)
| ~ s__instance(s__TimeInterval,s__SetOrClass) )
| ~ spl504_10829
| ~ spl504_12062
| ~ spl504_18630 ),
inference(forward_subsumption_resolution,[],[f149937,f142492]) ).
fof(f151318,plain,
( ! [X0] :
( s__instance(X0,s__TimePosition)
| ~ s__instance(X0,s__TimeInterval) )
| ~ spl504_10829
| ~ spl504_12062
| ~ spl504_18630
| ~ spl504_18652 ),
inference(forward_subsumption_resolution,[],[f150830,f142672]) ).
fof(f153199,definition,
( spl504_20204
<=> ! [X0] :
( s__instance(X0,s__TimePosition)
| ~ s__instance(X0,s__TimeInterval) ) ),
introduced(definition,[new_symbols(definition,[spl504_20204])],[avatar_definition]) ).
fof(f153200,plain,
( ! [X0] :
( ~ s__instance(X0,s__TimeInterval)
| s__instance(X0,s__TimePosition) )
| ~ spl504_20204 ),
inference(avatar_component_clause,[],[f153199]) ).
fof(f153201,plain,
( spl504_20204
| ~ spl504_10829
| ~ spl504_12062
| ~ spl504_18630
| ~ spl504_18652 ),
inference(avatar_split_clause,[],[f151318,f142670,f142490,f71785,f66642,f153199]) ).
fof(f177662,plain,
( s__instance(s__Time17_1,s__TimePosition)
| ~ spl504_6
| ~ spl504_20204 ),
inference(resolution,[],[f153200,f22982]) ).
fof(f177663,plain,
( s__instance(s__Time17_2,s__TimePosition)
| ~ spl504_5
| ~ spl504_20204 ),
inference(resolution,[],[f153200,f22977]) ).
fof(f177664,plain,
( s__instance(s__Time17_3,s__TimePosition)
| ~ spl504_4
| ~ spl504_20204 ),
inference(resolution,[],[f153200,f22972]) ).
fof(f177667,plain,
( spl504_14071
| ~ spl504_4
| ~ spl504_20204 ),
inference(avatar_split_clause,[],[f177664,f153199,f22970,f120275]) ).
fof(f177668,plain,
( $false
| ~ spl504_5
| spl504_14070
| ~ spl504_20204 ),
inference(forward_subsumption_resolution,[],[f177663,f120273]) ).
fof(f177669,plain,
( ~ spl504_5
| spl504_14070
| ~ spl504_20204 ),
inference(avatar_contradiction_clause,[],[f177668]) ).
fof(f177670,plain,
( spl504_14073
| ~ spl504_6
| ~ spl504_20204 ),
inference(avatar_split_clause,[],[f177662,f153199,f22980,f120284]) ).
fof(f177673,plain,
( ! [X0] :
( ~ s__temporalPart(X0,s__Time17_2)
| s__temporalPart(X0,s__Time17_3)
| ~ s__instance(s__Time17_2,s__TimePosition)
| ~ s__instance(X0,s__TimePosition) )
| ~ spl504_2
| ~ spl504_10300
| ~ spl504_14071 ),
inference(forward_subsumption_resolution,[],[f120379,f120276]) ).
fof(f177686,plain,
( ! [X0] :
( ~ s__temporalPart(X0,s__Time17_2)
| s__temporalPart(X0,s__Time17_3)
| ~ s__instance(X0,s__TimePosition) )
| ~ spl504_2
| ~ spl504_10300
| ~ spl504_14070
| ~ spl504_14071 ),
inference(forward_subsumption_resolution,[],[f177673,f120272]) ).
fof(f177724,definition,
( spl504_23163
<=> ! [X0] :
( ~ s__temporalPart(X0,s__Time17_2)
| s__temporalPart(X0,s__Time17_3)
| ~ s__instance(X0,s__TimePosition) ) ),
introduced(definition,[new_symbols(definition,[spl504_23163])],[avatar_definition]) ).
fof(f177725,plain,
( ! [X0] :
( ~ s__temporalPart(X0,s__Time17_2)
| s__temporalPart(X0,s__Time17_3)
| ~ s__instance(X0,s__TimePosition) )
| ~ spl504_23163 ),
inference(avatar_component_clause,[],[f177724]) ).
fof(f177726,plain,
( spl504_23163
| ~ spl504_2
| ~ spl504_10300
| ~ spl504_14070
| ~ spl504_14071 ),
inference(avatar_split_clause,[],[f177686,f120275,f120271,f64566,f22960,f177724]) ).
fof(f177872,plain,
( s__temporalPart(s__Time17_1,s__Time17_3)
| ~ s__instance(s__Time17_1,s__TimePosition)
| ~ spl504_3
| ~ spl504_23163 ),
inference(resolution,[],[f177725,f22967]) ).
fof(f177877,plain,
( ~ s__instance(s__Time17_1,s__TimePosition)
| spl504_1
| ~ spl504_3
| ~ spl504_23163 ),
inference(forward_subsumption_resolution,[],[f177872,f22957]) ).
fof(f177879,plain,
( $false
| spl504_1
| ~ spl504_3
| ~ spl504_14073
| ~ spl504_23163 ),
inference(forward_subsumption_resolution,[],[f177877,f120285]) ).
fof(f177880,plain,
( spl504_1
| ~ spl504_3
| ~ spl504_14073
| ~ spl504_23163 ),
inference(avatar_contradiction_clause,[],[f177879]) ).
cnf(s1,plain,
~ spl504_1,
inference(sat_conversion,[],[f22958]) ).
cnf(s2,plain,
spl504_2,
inference(sat_conversion,[],[f22963]) ).
cnf(s3,plain,
spl504_3,
inference(sat_conversion,[],[f22968]) ).
cnf(s4,plain,
spl504_4,
inference(sat_conversion,[],[f22973]) ).
cnf(s5,plain,
spl504_5,
inference(sat_conversion,[],[f22978]) ).
cnf(s6,plain,
spl504_6,
inference(sat_conversion,[],[f22983]) ).
cnf(s3390,plain,
spl504_4897,
inference(sat_conversion,[],[f43307]) ).
cnf(s6837,plain,
spl504_10300,
inference(sat_conversion,[],[f64568]) ).
cnf(s7262,plain,
spl504_10829,
inference(sat_conversion,[],[f66645]) ).
cnf(s8213,plain,
spl504_12062,
inference(sat_conversion,[],[f71787]) ).
cnf(s8214,plain,
spl504_12063,
inference(sat_conversion,[],[f71791]) ).
cnf(s27733,plain,
( ~ spl504_10829
| ~ spl504_12063
| spl504_18630 ),
inference(sat_conversion,[],[f142493]) ).
cnf(s27830,plain,
( ~ spl504_4897
| ~ spl504_12063
| spl504_18652 ),
inference(sat_conversion,[],[f142678]) ).
cnf(s29299,plain,
( ~ spl504_10829
| ~ spl504_12062
| ~ spl504_18630
| ~ spl504_18652
| spl504_20204 ),
inference(sat_conversion,[],[f153201]) ).
cnf(s33651,plain,
( ~ spl504_4
| spl504_14071
| ~ spl504_20204 ),
inference(sat_conversion,[],[f177667]) ).
cnf(s33652,plain,
( ~ spl504_5
| spl504_14070
| ~ spl504_20204 ),
inference(sat_conversion,[],[f177669]) ).
cnf(s33653,plain,
( ~ spl504_6
| spl504_14073
| ~ spl504_20204 ),
inference(sat_conversion,[],[f177670]) ).
cnf(s33657,plain,
( ~ spl504_2
| ~ spl504_10300
| ~ spl504_14070
| ~ spl504_14071
| spl504_23163 ),
inference(sat_conversion,[],[f177726]) ).
cnf(s33683,plain,
( spl504_1
| ~ spl504_3
| ~ spl504_14073
| ~ spl504_23163 ),
inference(sat_conversion,[],[f177880]) ).
cnf(s33890,plain,
spl504_18630,
inference(rat,[],[s27733,s8214,s7262]) ).
cnf(s35156,plain,
spl504_18652,
inference(rat,[],[s27830,s8214,s3390]) ).
cnf(s35159,plain,
spl504_20204,
inference(rat,[],[s29299,s33890,s7262,s8213,s35156]) ).
cnf(s38373,plain,
spl504_14073,
inference(rat,[],[s33653,s35159,s6]) ).
cnf(s38390,plain,
spl504_14070,
inference(rat,[],[s33652,s35159,s5]) ).
cnf(s38393,plain,
spl504_14071,
inference(rat,[],[s33651,s35159,s4]) ).
cnf(s38405,plain,
spl504_23163,
inference(rat,[],[s33657,s38393,s38390,s6837,s2]) ).
cnf(s38408,plain,
spl504_1,
inference(rat,[],[s33683,s3,s38373,s38405]) ).
cnf(s38410,plain,
$false,
inference(rat,[],[s1,s38408]) ).
fof(f177887,plain,
$false,
inference(avatar_sat_refutation,[],[s38410]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : CSR090+4 : TPTP v9.3.1. Bugfixed v7.3.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.19 % Computer : n006.cluster.edu
% 0.09/0.19 % Model : x86_64 x86_64
% 0.09/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.19 % Memory : 8046.5625MB
% 0.09/0.19 % OS : Linux 6.8.0-71-generic
% 0.09/0.19 % CPULimit : 300
% 0.09/0.19 % WCLimit : 300
% 0.09/0.19 % DateTime : Mon Sep 28 22:39:40 UTC 2026
% 0.09/0.19 % CPUTime :
% 0.09/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.22 Running first-order model finding
% 0.09/0.22 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 7.45/1.67 % (289352)Will run a generic schedule for satisfiability detection.
% 7.45/1.67 % (289363)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3881333850:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 7.45/1.67 % (289358)% WARNING: option uhcvi not known.
% 7.45/1.67 % (289358)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=964624303:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 7.45/1.67 % (289357)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3862501351_2999 on theBenchmark for (2999ds/0Mi)
% 7.45/1.67 % (289359)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2289029854:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 7.45/1.67 % (289360)dis+10_1_sil=32000:sp=arity:random_seed=4194491198:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 7.45/1.67 % (289361)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2350029454:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 7.45/1.67 % (289362)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2953782155:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 7.45/1.67 % (289363)Instruction limit reached!
% 7.45/1.67 % (289363)------------------------------
% 7.45/1.67 % (289363)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.45/1.67 % (289363)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.45/1.67 % (289363)CaDiCaL version: 2.1.3
% 7.45/1.67 % (289363)Termination reason: Instruction limit
% 7.45/1.67 % (289363)Termination phase: Equality resolution with deletion
% 7.45/1.67 % (289363)Time elapsed: 0.051 s
% 7.45/1.67 % (289363)Peak memory usage: 25 MB
% 7.45/1.67 % (289363)Instructions burned: 163 (million)
% 7.45/1.67 % (289371)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2527435722:i=714:nm=2_2998 on theBenchmark for (2998ds/714Mi)
% 7.45/1.67 % (289360)Instruction limit reached!
% 7.45/1.67 % (289360)------------------------------
% 7.45/1.67 % (289360)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.45/1.67 % (289360)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.45/1.67 % (289360)CaDiCaL version: 2.1.3
% 7.45/1.67 % (289360)Termination reason: Instruction limit
% 7.45/1.67 % (289360)Termination phase: Clausification
% 7.45/1.67 % (289360)Time elapsed: 0.063 s
% 7.45/1.67 % (289360)Peak memory usage: 24 MB
% 7.45/1.67 % (289360)Instructions burned: 104 (million)
% 7.45/1.67 % (289361)Instruction limit reached!
% 7.45/1.67 % (289361)------------------------------
% 7.45/1.67 % (289361)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.45/1.67 % (289361)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.45/1.67 % (289361)CaDiCaL version: 2.1.3
% 7.45/1.67 % (289361)Termination reason: Instruction limit
% 7.45/1.67 % (289361)Termination phase: Property scanning
% 7.45/1.67 % (289361)Time elapsed: 0.072 s
% 7.45/1.67 % (289361)Peak memory usage: 26 MB
% 7.45/1.67 % (289361)Instructions burned: 116 (million)
% 7.45/1.67 % (289373)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2853551004:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 7.45/1.67 % (289374)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=1406215621:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 7.45/1.67 % (289362)Instruction limit reached!
% 7.45/1.67 % (289362)------------------------------
% 7.45/1.67 % (289362)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.45/1.67 % (289362)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.45/1.67 % (289362)CaDiCaL version: 2.1.3
% 7.45/1.67 % (289362)Termination reason: Instruction limit
% 7.45/1.67 % (289362)Termination phase: Property scanning
% 7.45/1.67 % (289362)Time elapsed: 0.141 s
% 7.45/1.67 % (289362)Peak memory usage: 24 MB
% 7.45/1.67 % (289362)Instructions burned: 131 (million)
% 7.45/1.67 % (289373)Instruction limit reached!
% 7.45/1.67 % (289373)------------------------------
% 7.45/1.67 % (289373)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.45/1.67 % (289373)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.45/1.67 % (289373)CaDiCaL version: 2.1.3
% 7.45/1.67 % (289373)Termination reason: Instruction limit
% 7.45/1.67 % (289373)Termination phase: Property scanning
% 7.45/1.67 % (289373)Time elapsed: 0.077 s
% 15.49/2.72 % (289373)Peak memory usage: 24 MB
% 15.49/2.72 % (289373)Instructions burned: 133 (million)
% 15.49/2.72 % (289377)ott-21_1_sil=16000:fs=off:random_seed=3115607046:i=180:av=off:fsr=off_2997 on theBenchmark for (2997ds/180Mi)
% 15.49/2.72 % (289378)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3994874377:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 15.49/2.72 % (289371)Instruction limit reached!
% 15.49/2.72 % (289371)------------------------------
% 15.49/2.72 % (289371)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.49/2.72 % (289371)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.49/2.72 % (289371)CaDiCaL version: 2.1.3
% 15.49/2.72 % (289371)Termination reason: Instruction limit
% 15.49/2.72 % (289371)Termination phase: Finite model building preprocessing
% 15.49/2.72 % (289371)Time elapsed: 0.188 s
% 15.49/2.72 % (289371)Peak memory usage: 36 MB
% 15.49/2.72 % (289371)Instructions burned: 719 (million)
% 15.49/2.72 % (289381)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=848544843:fmbsr=1.3:i=865:ins=25_2996 on theBenchmark for (2996ds/865Mi)
% 15.49/2.72 % (289377)Instruction limit reached!
% 15.49/2.72 % (289377)------------------------------
% 15.49/2.72 % (289377)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.49/2.72 % (289377)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.49/2.72 % (289377)CaDiCaL version: 2.1.3
% 15.49/2.72 % (289377)Termination reason: Instruction limit
% 15.49/2.72 % (289377)Termination phase: Property scanning
% 15.49/2.72 % (289377)Time elapsed: 0.149 s
% 15.49/2.72 % (289377)Peak memory usage: 25 MB
% 15.49/2.72 % (289377)Instructions burned: 182 (million)
% 15.49/2.72 % (289383)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2457344353:i=1179_2995 on theBenchmark for (2995ds/1179Mi)
% 15.49/2.72 % (289378)Instruction limit reached!
% 15.49/2.72 % (289378)------------------------------
% 15.49/2.72 % (289378)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.49/2.72 % (289378)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.49/2.72 % (289378)CaDiCaL version: 2.1.3
% 15.49/2.72 % (289378)Termination reason: Instruction limit
% 15.49/2.72 % (289378)Termination phase: Saturation
% 15.49/2.72 % (289378)Time elapsed: 0.247 s
% 15.49/2.72 % (289378)Peak memory usage: 31 MB
% 15.49/2.72 % (289378)Instructions burned: 478 (million)
% 15.49/2.72 % (289385)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2389617470:i=889:ins=1_2994 on theBenchmark for (2994ds/889Mi)
% 15.49/2.72 % (289381)Instruction limit reached!
% 15.49/2.72 % (289381)------------------------------
% 15.49/2.72 % (289381)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.49/2.72 % (289381)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.49/2.72 % (289381)CaDiCaL version: 2.1.3
% 15.49/2.72 % (289381)Termination reason: Instruction limit
% 15.49/2.72 % (289381)Termination phase: Finite model building preprocessing
% 15.49/2.72 % (289381)Time elapsed: 0.228 s
% 15.49/2.72 % (289381)Peak memory usage: 39 MB
% 15.49/2.72 % (289381)Instructions burned: 869 (million)
% 15.49/2.72 % (289387)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=3950788902:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2994 on theBenchmark for (2994ds/692Mi)
% 15.49/2.72 % (289374)Instruction limit reached!
% 15.49/2.72 % (289374)------------------------------
% 15.49/2.72 % (289374)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.49/2.72 % (289374)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.49/2.72 % (289374)CaDiCaL version: 2.1.3
% 15.49/2.72 % (289374)Termination reason: Instruction limit
% 15.49/2.72 % (289374)Termination phase: Saturation
% 15.49/2.72 % (289374)Time elapsed: 0.447 s
% 15.49/2.72 % (289374)Peak memory usage: 32 MB
% 15.49/2.72 % (289374)Instructions burned: 685 (million)
% 15.49/2.72 % (289389)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=630598164:i=879:kws=inv_precedence:fsr=off_2993 on theBenchmark for (2993ds/879Mi)
% 15.49/2.72 % Detected minimum model sizes of [51]
% 15.49/2.72 % Detected maximum model sizes of [max]
% 15.49/2.72 % (289357)Cannot represent all propositional literals internally
% 15.49/2.72 % (289357)Refutation not found, incomplete strategy
% 15.49/2.72 % (289357)------------------------------
% 15.49/2.72 % (289357)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 34.73/5.24 % (289357)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.73/5.24 % (289357)CaDiCaL version: 2.1.3
% 34.73/5.24 % (289357)Termination reason: Refutation not found, incomplete strategy
% 34.73/5.24 % (289357)Time elapsed: 0.701 s
% 34.73/5.24 % (289357)Peak memory usage: 49 MB
% 34.73/5.24 % (289357)Instructions burned: 1467 (million)
% 34.73/5.24 % (289357)------------------------------
% 34.73/5.24 % (289357)------------------------------
% 34.73/5.24 % (289387)Instruction limit reached!
% 34.73/5.24 % (289387)------------------------------
% 34.73/5.24 % (289387)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 34.73/5.24 % (289387)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.73/5.24 % (289387)CaDiCaL version: 2.1.3
% 34.73/5.24 % (289387)Termination reason: Instruction limit
% 34.73/5.24 % (289387)Termination phase: Saturation
% 34.73/5.24 % (289387)Time elapsed: 0.214 s
% 34.73/5.24 % (289387)Peak memory usage: 35 MB
% 34.73/5.24 % (289387)Instructions burned: 693 (million)
% 34.73/5.24 % (289391)fmb+10_1_sil=64000:random_seed=430221148:i=22061:nm=2:gsp=on_2991 on theBenchmark for (2991ds/22061Mi)
% 34.73/5.24 % (289392)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=561198782:i=9515:nm=5_2991 on theBenchmark for (2991ds/9515Mi)
% 34.73/5.24 % (289385)Instruction limit reached!
% 34.73/5.24 % (289385)------------------------------
% 34.73/5.24 % (289385)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 34.73/5.24 % (289385)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.73/5.24 % (289385)CaDiCaL version: 2.1.3
% 34.73/5.24 % (289385)Termination reason: Instruction limit
% 34.73/5.24 % (289385)Termination phase: Finite model building preprocessing
% 34.73/5.24 % (289385)Time elapsed: 0.425 s
% 34.73/5.24 % (289385)Peak memory usage: 40 MB
% 34.73/5.24 % (289385)Instructions burned: 891 (million)
% 34.73/5.24 % (289395)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2758023956:fmbsr=1.7:i=920_2990 on theBenchmark for (2990ds/920Mi)
% 34.73/5.24 % (289383)Instruction limit reached!
% 34.73/5.24 % (289383)------------------------------
% 34.73/5.24 % (289383)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 34.73/5.24 % (289383)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.73/5.24 % (289383)CaDiCaL version: 2.1.3
% 34.73/5.24 % (289383)Termination reason: Instruction limit
% 34.73/5.24 % (289383)Termination phase: Saturation
% 34.73/5.24 % (289383)Time elapsed: 0.588 s
% 34.73/5.24 % (289383)Peak memory usage: 36 MB
% 34.73/5.24 % (289383)Instructions burned: 1179 (million)
% 34.73/5.24 % (289397)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=3791206003:i=5131_2989 on theBenchmark for (2989ds/5131Mi)
% 34.73/5.24 % (289389)Instruction limit reached!
% 34.73/5.24 % (289389)------------------------------
% 34.73/5.24 % (289389)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 34.73/5.24 % (289389)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.73/5.24 % (289389)CaDiCaL version: 2.1.3
% 34.73/5.24 % (289389)Termination reason: Instruction limit
% 34.73/5.24 % (289389)Termination phase: Saturation
% 34.73/5.24 % (289389)Time elapsed: 0.678 s
% 34.73/5.24 % (289389)Peak memory usage: 37 MB
% 34.73/5.24 % (289389)Instructions burned: 879 (million)
% 34.73/5.24 % (289399)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3620876663:i=1472:ins=7:fdi=8:gsp=on_2986 on theBenchmark for (2986ds/1472Mi)
% 34.73/5.24 % Detected minimum model sizes of [51]
% 34.73/5.24 % Detected maximum model sizes of [max]
% 34.73/5.24 % (289391)Cannot represent all propositional literals internally
% 34.73/5.24 % (289391)Refutation not found, incomplete strategy
% 34.73/5.24 % (289391)------------------------------
% 34.73/5.24 % (289391)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 34.73/5.24 % (289391)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.73/5.24 % (289391)CaDiCaL version: 2.1.3
% 34.73/5.24 % (289391)Termination reason: Refutation not found, incomplete strategy
% 34.73/5.24 % (289391)Time elapsed: 0.557 s
% 34.73/5.24 % (289391)Peak memory usage: 42 MB
% 34.73/5.24 % (289391)Instructions burned: 1181 (million)
% 34.73/5.24 % (289391)------------------------------
% 34.73/5.24 % (289391)------------------------------
% 34.73/5.24 % (289401)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=2416835560:i=6324_2985 on theBenchmark for (2985ds/6324Mi)
% 34.73/5.24 % (289395)Instruction limit reached!
% 34.73/5.24 % (289395)------------------------------
% 50.38/7.48 % (289395)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 50.38/7.48 % (289395)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.38/7.48 % (289395)CaDiCaL version: 2.1.3
% 50.38/7.48 % (289395)Termination reason: Instruction limit
% 50.38/7.48 % (289395)Termination phase: Finite model building preprocessing
% 50.38/7.48 % (289395)Time elapsed: 0.433 s
% 50.38/7.48 % (289395)Peak memory usage: 39 MB
% 50.38/7.48 % (289395)Instructions burned: 921 (million)
% 50.38/7.48 % Detected minimum model sizes of [51]
% 50.38/7.48 % Detected maximum model sizes of [max]
% 50.38/7.48 % (289392)Cannot represent all propositional literals internally
% 50.38/7.48 % (289392)Refutation not found, incomplete strategy
% 50.38/7.48 % (289392)------------------------------
% 50.38/7.48 % (289392)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 50.38/7.48 % (289392)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.38/7.48 % (289392)CaDiCaL version: 2.1.3
% 50.38/7.48 % (289392)Termination reason: Refutation not found, incomplete strategy
% 50.38/7.48 % (289392)Time elapsed: 0.615 s
% 50.38/7.49 % (289392)Peak memory usage: 44 MB
% 50.38/7.49 % (289392)Instructions burned: 1256 (million)
% 50.38/7.49 % (289403)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1542358902:fmbsr=2.30978:i=2174_2985 on theBenchmark for (2985ds/2174Mi)
% 50.38/7.49 % (289392)------------------------------
% 50.38/7.49 % (289392)------------------------------
% 50.38/7.49 % (289405)ott-2_1_sil=16000:newcnf=on:random_seed=3160866565:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2985 on theBenchmark for (2985ds/869Mi)
% 50.38/7.49 % (289399)Instruction limit reached!
% 50.38/7.49 % (289399)------------------------------
% 50.38/7.49 % (289399)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 50.38/7.49 % (289399)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.38/7.49 % (289399)CaDiCaL version: 2.1.3
% 50.38/7.49 % (289399)Termination reason: Instruction limit
% 50.38/7.49 % (289399)Termination phase: Saturation
% 50.38/7.49 % (289399)Time elapsed: 0.416 s
% 50.38/7.49 % (289399)Peak memory usage: 44 MB
% 50.38/7.49 % (289399)Instructions burned: 1475 (million)
% 50.38/7.49 % (289407)ott+10_1_sil=32000:tgt=ground:random_seed=1980256989:i=5114:av=off_2982 on theBenchmark for (2982ds/5114Mi)
% 50.38/7.49 % (289405)Instruction limit reached!
% 50.38/7.49 % (289405)------------------------------
% 50.38/7.49 % (289405)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 50.38/7.49 % (289405)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.38/7.49 % (289405)CaDiCaL version: 2.1.3
% 50.38/7.49 % (289405)Termination reason: Instruction limit
% 50.38/7.49 % (289405)Termination phase: Saturation
% 50.38/7.49 % (289405)Time elapsed: 0.485 s
% 50.38/7.49 % (289405)Peak memory usage: 38 MB
% 50.38/7.49 % (289405)Instructions burned: 869 (million)
% 50.38/7.49 % (289409)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=33901194:i=54282_2980 on theBenchmark for (2980ds/54282Mi)
% 50.38/7.49 % Detected minimum model sizes of [51]
% 50.38/7.49 % Detected maximum model sizes of [max]
% 50.38/7.49 % (289401)Cannot represent all propositional literals internally
% 50.38/7.49 % (289401)Refutation not found, incomplete strategy
% 50.38/7.49 % (289401)------------------------------
% 50.38/7.49 % (289401)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 50.38/7.49 % (289401)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.38/7.49 % (289401)CaDiCaL version: 2.1.3
% 50.38/7.49 % (289401)Termination reason: Refutation not found, incomplete strategy
% 50.38/7.49 % (289401)Time elapsed: 0.685 s
% 50.38/7.49 % (289401)Peak memory usage: 48 MB
% 50.38/7.49 % (289401)Instructions burned: 1456 (million)
% 50.38/7.49 % (289401)------------------------------
% 50.38/7.49 % (289401)------------------------------
% 50.38/7.49 % (289411)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=2116638957:i=3512:aac=none_2978 on theBenchmark for (2978ds/3512Mi)
% 50.38/7.49 % (289403)Instruction limit reached!
% 50.38/7.49 % (289403)------------------------------
% 50.38/7.49 % (289403)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 50.38/7.49 % (289403)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.38/7.49 % (289403)CaDiCaL version: 2.1.3
% 50.38/7.49 % (289403)Termination reason: Instruction limit
% 50.38/7.49 % (289403)Termination phase: Finite model building preprocessing
% 50.38/7.49 % (289403)Time elapsed: 1.031 s
% 50.38/7.49 % (289403)Peak memory usage: 62 MB
% 159.98/22.81 % (289403)Instructions burned: 2176 (million)
% 159.98/22.81 % (289413)dis+21_1_sil=32000:sas=cadical:random_seed=1006744786:i=3773:amm=off_2975 on theBenchmark for (2975ds/3773Mi)
% 159.98/22.81 % Detected minimum model sizes of [51]
% 159.98/22.81 % Detected maximum model sizes of [max]
% 159.98/22.81 % (289409)Cannot represent all propositional literals internally
% 159.98/22.81 % (289409)Refutation not found, incomplete strategy
% 159.98/22.81 % (289409)------------------------------
% 159.98/22.81 % (289409)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 159.98/22.81 % (289409)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 159.98/22.81 % (289409)CaDiCaL version: 2.1.3
% 159.98/22.81 % (289409)Termination reason: Refutation not found, incomplete strategy
% 159.98/22.81 % (289409)Time elapsed: 0.741 s
% 159.98/22.81 % (289409)Peak memory usage: 48 MB
% 159.98/22.81 % (289409)Instructions burned: 1464 (million)
% 159.98/22.81 % (289409)------------------------------
% 159.98/22.81 % (289409)------------------------------
% 159.98/22.81 % (289415)ott+11_1_sil=16000:gs=on:random_seed=4149392868:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2972 on theBenchmark for (2972ds/2251Mi)
% 159.98/22.81 % (289407)Instruction limit reached!
% 159.98/22.81 % (289407)------------------------------
% 159.98/22.81 % (289407)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 159.98/22.81 % (289407)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 159.98/22.81 % (289407)CaDiCaL version: 2.1.3
% 159.98/22.81 % (289407)Termination reason: Instruction limit
% 159.98/22.81 % (289407)Termination phase: Saturation
% 159.98/22.81 % (289407)Time elapsed: 1.574 s
% 159.98/22.81 % (289407)Peak memory usage: 63 MB
% 159.98/22.81 % (289407)Instructions burned: 5118 (million)
% 159.98/22.81 % (289443)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=2661724727:fmbsr=1.6:i=67534_2966 on theBenchmark for (2966ds/67534Mi)
% 159.98/22.81 % Detected minimum model sizes of [51]
% 159.98/22.81 % Detected maximum model sizes of [max]
% 159.98/22.81 % (289443)Cannot represent all propositional literals internally
% 159.98/22.81 % (289443)Refutation not found, incomplete strategy
% 159.98/22.81 % (289443)------------------------------
% 159.98/22.81 % (289443)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 159.98/22.81 % (289443)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 159.98/22.81 % (289443)CaDiCaL version: 2.1.3
% 159.98/22.81 % (289443)Termination reason: Refutation not found, incomplete strategy
% 159.98/22.81 % (289443)Time elapsed: 0.666 s
% 159.98/22.81 % (289443)Peak memory usage: 46 MB
% 159.98/22.81 % (289443)Instructions burned: 1418 (million)
% 159.98/22.81 % (289443)------------------------------
% 159.98/22.81 % (289443)------------------------------
% 159.98/22.81 % (289451)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=2850205274:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2959 on theBenchmark for (2959ds/4591Mi)
% 159.98/22.81 % (289411)Instruction limit reached!
% 159.98/22.81 % (289411)------------------------------
% 159.98/22.81 % (289411)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 159.98/22.81 % (289411)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 159.98/22.81 % (289411)CaDiCaL version: 2.1.3
% 159.98/22.81 % (289411)Termination reason: Instruction limit
% 159.98/22.81 % (289411)Termination phase: Saturation
% 159.98/22.81 % (289411)Time elapsed: 2.083 s
% 159.98/22.81 % (289411)Peak memory usage: 59 MB
% 159.98/22.81 % (289411)Instructions burned: 3512 (million)
% 159.98/22.81 % (289455)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=3693440823:i=29340_2957 on theBenchmark for (2957ds/29340Mi)
% 159.98/22.81 % (289397)Instruction limit reached!
% 159.98/22.81 % (289397)------------------------------
% 159.98/22.81 % (289397)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 159.98/22.81 % (289397)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 159.98/22.81 % (289397)CaDiCaL version: 2.1.3
% 159.98/22.81 % (289397)Termination reason: Instruction limit
% 159.98/22.81 % (289397)Termination phase: Saturation
% 159.98/22.81 % (289397)Time elapsed: 3.383 s
% 159.98/22.81 % (289397)Peak memory usage: 57 MB
% 159.98/22.81 % (289397)Instructions burned: 5131 (million)
% 159.98/22.81 % (289457)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=3636317751:i=5211_2955 on theBenchmark for (2955ds/5211Mi)
% 159.98/22.81 % (289415)Instruction limit reached!
% 159.98/22.81 % (289415)------------------------------
% 159.98/22.81 % (289415)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 213.36/30.37 % (289415)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 213.36/30.37 % (289415)CaDiCaL version: 2.1.3
% 213.36/30.37 % (289415)Termination reason: Instruction limit
% 213.36/30.37 % (289415)Termination phase: Saturation
% 213.36/30.37 % (289415)Time elapsed: 2.234 s
% 213.36/30.37 % (289415)Peak memory usage: 67 MB
% 213.36/30.37 % (289415)Instructions burned: 2251 (million)
% 213.36/30.37 % (289464)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=3216830684:i=5497:nm=2_2949 on theBenchmark for (2949ds/5497Mi)
% 213.36/30.37 % (289413)Instruction limit reached!
% 213.36/30.37 % (289413)------------------------------
% 213.36/30.37 % (289413)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 213.36/30.37 % (289413)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 213.36/30.37 % (289413)CaDiCaL version: 2.1.3
% 213.36/30.37 % (289413)Termination reason: Instruction limit
% 213.36/30.37 % (289413)Termination phase: Saturation
% 213.36/30.37 % (289413)Time elapsed: 2.884 s
% 213.36/30.37 % (289413)Peak memory usage: 62 MB
% 213.36/30.37 % (289413)Instructions burned: 3774 (million)
% 213.36/30.37 % (289469)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=2381356067:fmbsr=2:i=46332_2945 on theBenchmark for (2945ds/46332Mi)
% 213.36/30.37 % Detected minimum model sizes of [51]
% 213.36/30.37 % Detected maximum model sizes of [max]
% 213.36/30.37 % (289464)Cannot represent all propositional literals internally
% 213.36/30.37 % (289464)Refutation not found, incomplete strategy
% 213.36/30.37 % (289464)------------------------------
% 213.36/30.37 % (289464)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 213.36/30.37 % (289464)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 213.36/30.37 % (289464)CaDiCaL version: 2.1.3
% 213.36/30.37 % (289464)Termination reason: Refutation not found, incomplete strategy
% 213.36/30.37 % (289464)Time elapsed: 1.052 s
% 213.36/30.37 % (289464)Peak memory usage: 45 MB
% 213.36/30.37 % (289464)Instructions burned: 1327 (million)
% 213.36/30.37 % (289464)------------------------------
% 213.36/30.37 % (289464)------------------------------
% 213.36/30.37 % (289473)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=1386535963:i=14071_2938 on theBenchmark for (2938ds/14071Mi)
% 213.36/30.37 % (289451)Instruction limit reached!
% 213.36/30.37 % (289451)------------------------------
% 213.36/30.37 % (289451)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 213.36/30.37 % (289451)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 213.36/30.37 % (289451)CaDiCaL version: 2.1.3
% 213.36/30.37 % (289451)Termination reason: Instruction limit
% 213.36/30.37 % (289451)Termination phase: Saturation
% 213.36/30.37 % (289451)Time elapsed: 2.252 s
% 213.36/30.37 % (289451)Peak memory usage: 96 MB
% 213.36/30.37 % (289451)Instructions burned: 4592 (million)
% 213.36/30.37 % (289475)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1629895546:i=22565:add=on:rawr=on_2936 on theBenchmark for (2936ds/22565Mi)
% 213.36/30.37 % Detected minimum model sizes of [51]
% 213.36/30.37 % Detected maximum model sizes of [max]
% 213.36/30.37 % (289469)Cannot represent all propositional literals internally
% 213.36/30.37 % (289469)Refutation not found, incomplete strategy
% 213.36/30.37 % (289469)------------------------------
% 213.36/30.37 % (289469)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 213.36/30.37 % (289469)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 213.36/30.37 % (289469)CaDiCaL version: 2.1.3
% 213.36/30.37 % (289469)Termination reason: Refutation not found, incomplete strategy
% 213.36/30.37 % (289469)Time elapsed: 1.100 s
% 213.36/30.37 % (289469)Peak memory usage: 45 MB
% 213.36/30.37 % (289469)Instructions burned: 1418 (million)
% 213.36/30.37 % (289469)------------------------------
% 213.36/30.37 % (289469)------------------------------
% 213.36/30.37 % (289477)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=4281097449:i=8173:av=off_2934 on theBenchmark for (2934ds/8173Mi)
% 213.36/30.37 % Detected minimum model sizes of [51]
% 213.36/30.37 % Detected maximum model sizes of [max]
% 213.36/30.37 % (289473)Cannot represent all propositional literals internally
% 213.36/30.37 % (289473)Refutation not found, incomplete strategy
% 213.36/30.37 % (289473)------------------------------
% 213.36/30.37 % (289473)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 213.36/30.37 % (289473)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 213.36/30.37 % (289473)CaDiCaL version: 2.1.3
% 213.36/30.37 % (289473)Termination reason: Refutation not found, incomplete strategy
% 226.86/32.28 % (289473)Time elapsed: 1.104 s
% 226.86/32.28 % (289473)Peak memory usage: 46 MB
% 226.86/32.28 % (289473)Instructions burned: 1286 (million)
% 226.86/32.28 % (289473)------------------------------
% 226.86/32.28 % (289473)------------------------------
% 226.86/32.28 % (289479)dis+10_16:1_sil=16000:random_seed=1719660858:i=9155:fsr=off_2927 on theBenchmark for (2927ds/9155Mi)
% 226.86/32.28 % (289457)Instruction limit reached!
% 226.86/32.28 % (289457)------------------------------
% 226.86/32.28 % (289457)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 226.86/32.28 % (289457)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 226.86/32.28 % (289457)CaDiCaL version: 2.1.3
% 226.86/32.28 % (289457)Termination reason: Instruction limit
% 226.86/32.28 % (289457)Termination phase: Saturation
% 226.86/32.28 % (289457)Time elapsed: 3.585 s
% 226.86/32.28 % (289457)Peak memory usage: 47 MB
% 226.86/32.28 % (289457)Instructions burned: 5211 (million)
% 226.86/32.28 % (289483)ott-3_8_sil=64000:random_seed=875291384:i=20139:bs=on_2919 on theBenchmark for (2919ds/20139Mi)
% 226.86/32.28 % (289477)Instruction limit reached!
% 226.86/32.28 % (289477)------------------------------
% 226.86/32.28 % (289477)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 226.86/32.28 % (289477)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 226.86/32.28 % (289477)CaDiCaL version: 2.1.3
% 226.86/32.28 % (289477)Termination reason: Instruction limit
% 226.86/32.28 % (289477)Termination phase: Saturation
% 226.86/32.28 % (289477)Time elapsed: 7.328 s
% 226.86/32.28 % (289477)Peak memory usage: 110 MB
% 226.86/32.28 % (289477)Instructions burned: 8173 (million)
% 226.86/32.28 % (289495)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=3446291148:fmbsr=2:i=32576_2860 on theBenchmark for (2860ds/32576Mi)
% 226.86/32.28 % (289479)Instruction limit reached!
% 226.86/32.28 % (289479)------------------------------
% 226.86/32.28 % (289479)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 226.86/32.28 % (289479)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 226.86/32.28 % (289479)CaDiCaL version: 2.1.3
% 226.86/32.28 % (289479)Termination reason: Instruction limit
% 226.86/32.28 % (289479)Termination phase: Saturation
% 226.86/32.28 % (289479)Time elapsed: 7.423 s
% 226.86/32.28 % (289479)Peak memory usage: 92 MB
% 226.86/32.28 % (289479)Instructions burned: 9156 (million)
% 226.86/32.28 % (289497)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=3241826300:i=11404_2852 on theBenchmark for (2852ds/11404Mi)
% 226.86/32.28 % Detected minimum model sizes of [51]
% 226.86/32.28 % Detected maximum model sizes of [max]
% 226.86/32.28 % (289495)Cannot represent all propositional literals internally
% 226.86/32.28 % (289495)Refutation not found, incomplete strategy
% 226.86/32.28 % (289495)------------------------------
% 226.86/32.28 % (289495)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 226.86/32.28 % (289495)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 226.86/32.28 % (289495)CaDiCaL version: 2.1.3
% 226.86/32.28 % (289495)Termination reason: Refutation not found, incomplete strategy
% 226.86/32.28 % (289495)Time elapsed: 1.293 s
% 226.86/32.28 % (289495)Peak memory usage: 48 MB
% 226.86/32.28 % (289495)Instructions burned: 1456 (million)
% 226.86/32.28 % (289495)------------------------------
% 226.86/32.28 % (289495)------------------------------
% 226.86/32.28 % (289499)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=3956893340:i=14134_2846 on theBenchmark for (2846ds/14134Mi)
% 226.86/32.28 % (289475)Instruction limit reached!
% 226.86/32.28 % (289475)------------------------------
% 226.86/32.28 % (289475)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 226.86/32.28 % (289475)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 226.86/32.28 % (289475)CaDiCaL version: 2.1.3
% 226.86/32.28 % (289475)Termination reason: Instruction limit
% 226.86/32.28 % (289475)Termination phase: Saturation
% 226.86/32.28 % (289475)Time elapsed: 10.312 s
% 226.86/32.28 % (289475)Peak memory usage: 949 MB
% 226.86/32.28 % (289475)Instructions burned: 22565 (million)
% 226.86/32.28 % (289503)dis+33_16_sil=32000:sac=on:random_seed=923767561:i=15851:nm=0_2832 on theBenchmark for (2832ds/15851Mi)
% 226.86/32.28 % (289503)Instruction limit reached!
% 226.86/32.28 % (289503)------------------------------
% 226.86/32.28 % (289503)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 226.86/32.28 % (289503)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 226.86/32.28 % (289503)CaDiCaL version: 2.1.3
% 226.86/32.28 % (289503)Termination reason: Instruction limit
% 226.86/32.28 % (289503)Termination phase: Saturation
% 236.78/33.61 % (289503)Time elapsed: 5.782 s
% 236.78/33.61 % (289503)Peak memory usage: 85 MB
% 236.78/33.61 % (289503)Instructions burned: 15855 (million)
% 236.78/33.61 % (289515)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=2968498185:avsq=on:i=17627:add=on:amm=off_2774 on theBenchmark for (2774ds/17627Mi)
% 236.78/33.61 % (289497)Instruction limit reached!
% 236.78/33.61 % (289497)------------------------------
% 236.78/33.61 % (289497)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 236.78/33.61 % (289497)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 236.78/33.61 % (289497)CaDiCaL version: 2.1.3
% 236.78/33.61 % (289497)Termination reason: Instruction limit
% 236.78/33.61 % (289497)Termination phase: Saturation
% 236.78/33.61 % (289497)Time elapsed: 12.010 s
% 236.78/33.61 % (289497)Peak memory usage: 404 MB
% 236.78/33.61 % (289497)Instructions burned: 11405 (million)
% 236.78/33.61 % (289523)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=2615359383:s2a=on:i=53295_2731 on theBenchmark for (2731ds/53295Mi)
% 236.78/33.61 % (289483)Instruction limit reached!
% 236.78/33.61 % (289483)------------------------------
% 236.78/33.61 % (289483)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 236.78/33.61 % (289483)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 236.78/33.61 % (289483)CaDiCaL version: 2.1.3
% 236.78/33.61 % (289483)Termination reason: Instruction limit
% 236.78/33.61 % (289483)Termination phase: Saturation
% 236.78/33.61 % (289483)Time elapsed: 19.979 s
% 236.78/33.61 % (289483)Peak memory usage: 135 MB
% 236.78/33.61 % (289483)Instructions burned: 20140 (million)
% 236.78/33.61 % (289525)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=18192537:i=26857:ins=20_2718 on theBenchmark for (2718ds/26857Mi)
% 236.78/33.61 % (289499)Instruction limit reached!
% 236.78/33.61 % (289499)------------------------------
% 236.78/33.61 % (289499)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 236.78/33.61 % (289499)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 236.78/33.61 % (289499)CaDiCaL version: 2.1.3
% 236.78/33.61 % (289499)Termination reason: Instruction limit
% 236.78/33.61 % (289499)Termination phase: Saturation
% 236.78/33.61 % (289499)Time elapsed: 12.807 s
% 236.78/33.61 % (289499)Peak memory usage: 115 MB
% 236.78/33.61 % (289499)Instructions burned: 14134 (million)
% 236.78/33.61 % (289527)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=2734977013:i=28120:bs=on:fsr=off_2718 on theBenchmark for (2718ds/28120Mi)
% 236.78/33.61 % (289455)Instruction limit reached!
% 236.78/33.61 % (289455)------------------------------
% 236.78/33.61 % (289455)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 236.78/33.61 % (289455)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 236.78/33.61 % (289455)CaDiCaL version: 2.1.3
% 236.78/33.61 % (289455)Termination reason: Instruction limit
% 236.78/33.61 % (289455)Termination phase: Saturation
% 236.78/33.61 % (289455)Time elapsed: 24.703 s
% 236.78/33.61 % (289455)Peak memory usage: 73 MB
% 236.78/33.61 % (289455)Instructions burned: 29341 (million)
% 236.78/33.61 % (289533)fmb+10_1_sil=256000:fmbss=7:random_seed=4263882586:fmbsr=1.6:i=182295_2709 on theBenchmark for (2709ds/182295Mi)
% 236.78/33.61 % Detected minimum model sizes of [51]
% 236.78/33.61 % Detected maximum model sizes of [max]
% 236.78/33.61 % (289525)Cannot represent all propositional literals internally
% 236.78/33.61 % (289525)Refutation not found, incomplete strategy
% 236.78/33.61 % (289525)------------------------------
% 236.78/33.61 % (289525)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 236.78/33.61 % (289525)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 236.78/33.61 % (289525)CaDiCaL version: 2.1.3
% 236.78/33.61 % (289525)Termination reason: Refutation not found, incomplete strategy
% 236.78/33.61 % (289525)Time elapsed: 1.074 s
% 236.78/33.61 % (289525)Peak memory usage: 46 MB
% 236.78/33.61 % (289525)Instructions burned: 1286 (million)
% 236.78/33.61 % (289525)------------------------------
% 236.78/33.61 % (289525)------------------------------
% 236.78/33.61 % (289535)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=2413978329:i=44625:gsp=on_2707 on theBenchmark for (2707ds/44625Mi)
% 236.78/33.61 % Detected minimum model sizes of [51]
% 236.78/33.61 % Detected maximum model sizes of [max]
% 236.78/33.61 % (289533)Cannot represent all propositional literals internally
% 236.78/33.61 % (289533)Refutation not found, incomplete strategy
% 236.78/33.61 % (289533)------------------------------
% 236.78/33.61 % (289533)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 168.51/34.04 % (289533)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 168.51/34.04 % (289533)CaDiCaL version: 2.1.3
% 168.51/34.04 % (289533)Termination reason: Refutation not found, incomplete strategy
% 168.51/34.04 % (289533)Time elapsed: 1.105 s
% 168.51/34.04 % (289533)Peak memory usage: 46 MB
% 168.51/34.04 % (289533)Instructions burned: 1286 (million)
% 168.51/34.04 % (289533)------------------------------
% 168.51/34.04 % (289533)------------------------------
% 168.51/34.04 % (289537)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=1384369686:i=160505_2698 on theBenchmark for (2698ds/160505Mi)
% 168.51/34.04 % Detected minimum model sizes of [51]
% 168.51/34.04 % Detected maximum model sizes of [max]
% 168.51/34.04 % (289535)Cannot represent all propositional literals internally
% 168.51/34.04 % (289535)Refutation not found, incomplete strategy
% 168.51/34.04 % (289535)------------------------------
% 168.51/34.04 % (289535)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 168.51/34.04 % (289535)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 168.51/34.04 % (289535)CaDiCaL version: 2.1.3
% 168.51/34.04 % (289535)Termination reason: Refutation not found, incomplete strategy
% 168.51/34.04 % (289535)Time elapsed: 1.159 s
% 168.51/34.04 % (289535)Peak memory usage: 48 MB
% 168.51/34.04 % (289535)Instructions burned: 1362 (million)
% 168.51/34.04 % (289535)------------------------------
% 168.51/34.04 % (289535)------------------------------
% 168.51/34.04 % (289539)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=2773439967:fmbsr=1.3:i=225729_2695 on theBenchmark for (2695ds/225729Mi)
% 168.51/34.04 % Detected minimum model sizes of [51]
% 168.51/34.04 % Detected maximum model sizes of [max]
% 168.51/34.04 % (289537)Cannot represent all propositional literals internally
% 168.51/34.04 % (289537)Refutation not found, incomplete strategy
% 168.51/34.04 % (289537)------------------------------
% 168.51/34.04 % (289537)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 168.51/34.04 % (289537)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 168.51/34.04 % (289537)CaDiCaL version: 2.1.3
% 168.51/34.04 % (289537)Termination reason: Refutation not found, incomplete strategy
% 168.51/34.04 % (289537)Time elapsed: 1.091 s
% 168.51/34.04 % (289537)Peak memory usage: 46 MB
% 168.51/34.04 % (289537)Instructions burned: 1286 (million)
% 168.51/34.04 % (289537)------------------------------
% 168.51/34.04 % (289537)------------------------------
% 168.51/34.04 % (289541)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=2630845211:fmbsr=2:i=185024:ins=7_2686 on theBenchmark for (2686ds/185024Mi)
% 168.51/34.04 % (289515)Instruction limit reached!
% 168.51/34.04 % (289515)------------------------------
% 168.51/34.04 % (289515)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 168.51/34.04 % (289515)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 168.51/34.04 % (289515)CaDiCaL version: 2.1.3
% 168.51/34.04 % (289515)Termination reason: Instruction limit
% 168.51/34.04 % (289515)Termination phase: Saturation
% 168.51/34.04 % (289515)Time elapsed: 8.921 s
% 168.51/34.04 % (289515)Peak memory usage: 660 MB
% 168.51/34.04 % (289515)Instructions burned: 17627 (million)
% 168.51/34.04 % Detected minimum model sizes of [51]
% 168.51/34.04 % Detected maximum model sizes of [max]
% 168.51/34.04 % (289539)Cannot represent all propositional literals internally
% 168.51/34.04 % (289539)Refutation not found, incomplete strategy
% 168.51/34.04 % (289539)------------------------------
% 168.51/34.04 % (289539)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 168.51/34.04 % (289539)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 168.51/34.04 % (289539)CaDiCaL version: 2.1.3
% 168.51/34.04 % (289539)Termination reason: Refutation not found, incomplete strategy
% 168.51/34.04 % (289539)Time elapsed: 1.084 s
% 168.51/34.04 % (289539)Peak memory usage: 45 MB
% 168.51/34.04 % (289539)Instructions burned: 1286 (million)
% 168.51/34.04 % (289539)------------------------------
% 168.51/34.04 % (289539)------------------------------
% 168.51/34.04 % (289545)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=881242935:rtra=on_2684 on theBenchmark for (2684ds/0Mi)
% 168.51/34.04 % (289546)% WARNING: option uhcvi not known.
% 168.51/34.04 % (289546)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2669718939:i=271062:add=off:rtra=on:rawr=on_2683 on theBenchmark for (2683ds/271062Mi)
% 168.51/34.04 % Detected minimum model sizes of [51]
% 168.51/34.04 % Detected maximum model sizes of [max]
% 168.51/34.04 % (289541)Cannot represent all propositional literals internally
% 168.51/34.04 % (289541)Refutation not found, incomplete strategy
% 168.51/34.04 % (289541)------------------------------
% 168.51/34.04 % (289541)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 168.51/34.04 % (289541)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 168.51/34.04 % (289541)CaDiCaL version: 2.1.3
% 168.51/34.04 % (289541)Termination reason: Refutation not found, incomplete strategy
% 168.51/34.04 % (289541)Time elapsed: 0.704 s
% 168.51/34.04 % (289541)Peak memory usage: 46 MB
% 168.51/34.04 % (289541)Instructions burned: 1286 (million)
% 168.51/34.04 % (289541)------------------------------
% 168.51/34.04 % (289541)------------------------------
% 168.51/34.04 % (289549)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=202935765:i=176048:add=on:rtra=on:rawr=on_2679 on theBenchmark for (2679ds/176048Mi)
% 168.51/34.04 % Detected minimum model sizes of [51]
% 168.51/34.04 % Detected maximum model sizes of [max]
% 168.51/34.04 % (289545)Cannot represent all propositional literals internally
% 168.51/34.04 % (289545)Refutation not found, incomplete strategy
% 168.51/34.04 % (289545)------------------------------
% 168.51/34.04 % (289545)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 168.51/34.04 % (289545)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 168.51/34.04 % (289545)CaDiCaL version: 2.1.3
% 168.51/34.04 % (289545)Termination reason: Refutation not found, incomplete strategy
% 168.51/34.04 % (289545)Time elapsed: 0.965 s
% 168.51/34.04 % (289545)Peak memory usage: 54 MB
% 168.51/34.04 % (289545)Instructions burned: 1518 (million)
% 168.51/34.04 % (289545)------------------------------
% 168.51/34.04 % (289545)------------------------------
% 168.51/34.04 % (289553)dis+10_1_sil=32000:si=on:sp=arity:random_seed=1742589267:i=206:fgj=on:rtra=on_2673 on theBenchmark for (2673ds/206Mi)
% 168.51/34.04 % (289553)Instruction limit reached!
% 168.51/34.04 % (289553)------------------------------
% 168.51/34.04 % (289553)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 168.51/34.04 % (289553)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 168.51/34.04 % (289553)CaDiCaL version: 2.1.3
% 168.51/34.04 % (289553)Termination reason: Instruction limit
% 168.51/34.04 % (289553)Termination phase: Property scanning
% 168.51/34.04 % (289553)Time elapsed: 0.131 s
% 168.51/34.04 % (289553)Peak memory usage: 28 MB
% 168.51/34.04 % (289553)Instructions burned: 207 (million)
% 168.51/34.04 % (289555)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=3146550864:i=232:rtra=on_2672 on theBenchmark for (2672ds/232Mi)
% 168.51/34.04 % (289555)Instruction limit reached!
% 168.51/34.04 % (289555)------------------------------
% 168.51/34.04 % (289555)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 168.51/34.04 % (289555)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 168.51/34.04 % (289555)CaDiCaL version: 2.1.3
% 168.51/34.04 % (289555)Termination reason: Instruction limit
% 168.51/34.04 % (289555)Termination phase: Property scanning
% 168.51/34.04 % (289555)Time elapsed: 0.142 s
% 168.51/34.04 % (289555)Peak memory usage: 29 MB
% 168.51/34.04 % (289555)Instructions burned: 232 (million)
% 168.51/34.04 % (289557)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=2262144491:i=262:rtra=on_2670 on theBenchmark for (2670ds/262Mi)
% 168.51/34.04 % (289557)Instruction limit reached!
% 168.51/34.04 % (289557)------------------------------
% 168.51/34.04 % (289557)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 168.51/34.04 % (289557)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 168.51/34.04 % (289557)CaDiCaL version: 2.1.3
% 168.51/34.04 % (289557)Termination reason: Instruction limit
% 168.51/34.04 % (289557)Termination phase: Saturation
% 168.51/34.04 % (289557)Time elapsed: 0.152 s
% 168.51/34.04 % (289557)Peak memory usage: 28 MB
% 168.51/34.04 % (289557)Instructions burned: 265 (million)
% 168.51/34.04 % (289559)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=553869614:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2668 on theBenchmark for (2668ds/318Mi)
% 168.51/34.04 % (289559)Instruction limit reached!
% 168.51/34.04 % (289559)------------------------------
% 168.51/34.04 % (289559)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 168.51/34.04 % (289559)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 168.51/34.04 % (289559)CaDiCaL version: 2.1.3
% 168.51/34.04 % (289559)Termination reason: Instruction limit
% 168.51/34.04 % (289559)Termination phase: Saturation
% 168.51/34.04 % (289559)Time elapsed: 0.217 s
% 168.51/34.04 % (289559)Peak memory usage: 29 MB
% 168.51/34.04 % (289559)Instructions burned: 320 (million)
% 168.51/34.04 % (289561)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=879427480:i=1428:nm=2:rtra=on_2666 on theBenchmark for (2666ds/1428Mi)
% 168.51/34.04 % (289523) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-289352-289523"...
% 168.51/34.04 % (289523)...printing done.
% 168.51/34.04 % (289523)Refutation found. Thanks to Tanya!
% 168.51/34.04 % SZS status Theorem for theBenchmark
% 168.51/34.04 % SZS output start Proof for theBenchmark
% See solution above
% 238.32/34.05 % (289523)------------------------------
% 238.32/34.05 % (289523)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 238.32/34.05 % (289523)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 238.32/34.05 % (289523)CaDiCaL version: 2.1.3
% 238.32/34.05 % (289523)Termination reason: Refutation
% 238.32/34.05 % (289523)Time elapsed: 6.558 s
% 238.32/34.05 % (289523)Peak memory usage: 110 MB
% 238.32/34.05 % (289523)Instructions burned: 7955 (million)
% 238.32/34.06 % (289352)Success in time 33.813 s
% 238.32/34.06 % Vampire exiting
%------------------------------------------------------------------------------