%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : GEO061-3 : TPTP v9.3.1. Bugfixed v1.2.1.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n008.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:51:24 AM UTC 2026
% Result : Unsatisfiable 146.95s 37.05s
% Output : Refutation 0.17s
% Verified :
% SZS Type : Refutation
% Derivation depth : 15
% Number of leaves : 55
% Syntax : Number of formulae : 213 ( 43 unt; 28 def)
% Number of atoms : 498 ( 41 equ)
% Maximal formula atoms : 8 ( 2 avg)
% Number of connectives : 535 ( 250 ~; 259 |; 0 &)
% ( 26 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 17 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 30 ( 28 usr; 27 prp; 0-4 aty)
% Number of functors : 11 ( 11 usr; 9 con; 0-4 aty)
% Number of variables : 130 ( 0 sgn 130 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f2,axiom,
! [X2,X3,X0,X1,X4,X5] :
( equidistant(X2,X3,X4,X5)
| ~ equidistant(X0,X1,X4,X5)
| ~ equidistant(X0,X1,X2,X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',transitivity_for_equidistance) ).
fof(f3,axiom,
! [X2,X0,X1] :
( ~ equidistant(X0,X1,X2,X2)
| X0 = X1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',identity_for_equidistance) ).
fof(f4,axiom,
! [X2,X3,X0,X1] : between(X0,X1,extension(X0,X1,X2,X3)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',segment_construction1) ).
fof(f5,axiom,
! [X2,X3,X0,X1] : equidistant(X0,extension(X1,X0,X2,X3),X2,X3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',segment_construction2) ).
fof(f6,axiom,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( equidistant(X4,X6,X5,X7)
| ~ equidistant(X1,X4,X3,X5)
| ~ equidistant(X0,X6,X2,X7)
| ~ equidistant(X1,X6,X3,X7)
| ~ between(X0,X1,X4)
| ~ between(X2,X3,X5)
| X0 = X1
| ~ equidistant(X0,X1,X2,X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',outer_five_segment) ).
fof(f20,axiom,
! [X2,X3,X0,X1] : insertion(X0,X1,X2,X3) = extension(extension(X1,X0,lower_dimension_point_1,lower_dimension_point_2),X0,X2,X3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',insertion) ).
fof(f21,axiom,
! [X0,X1] : equidistant(X0,X1,X0,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d1) ).
fof(f22,axiom,
! [X2,X3,X0,X1] :
( equidistant(X2,X3,X0,X1)
| ~ equidistant(X0,X1,X2,X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d2) ).
fof(f25,axiom,
! [X2,X3,X0,X1] :
( equidistant(X1,X0,X3,X2)
| ~ equidistant(X0,X1,X2,X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d4_2) ).
fof(f27,axiom,
! [X2,X3,X0,X1] :
( equidistant(X3,X2,X0,X1)
| ~ equidistant(X0,X1,X2,X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d4_4) ).
fof(f28,axiom,
! [X2,X3,X0,X1] :
( equidistant(X3,X2,X1,X0)
| ~ equidistant(X0,X1,X2,X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d4_5) ).
fof(f30,axiom,
! [X2,X0,X1] : X0 = extension(X1,X0,X2,X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e1) ).
fof(f31,plain,
! [X2,X0,X1] : extension(X1,X0,X2,X2) = X0,
inference(reorient_equations,[],[f30]) ).
fof(f42,axiom,
! [X0,X1] : equidistant(X0,X0,X1,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d7) ).
fof(f47,axiom,
! [X2,X3,X0,X1,X4,X5] :
( ~ equidistant(X0,X1,X2,X3)
| extension(X4,X5,X0,X1) = extension(X4,X5,X2,X3)
| X4 = X5 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d10_2) ).
fof(f52,axiom,
! [X0,X1] : between(X0,X1,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t3) ).
fof(f54,axiom,
! [X2,X0,X1] :
( between(X2,X1,X0)
| ~ between(X0,X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t1) ).
fof(f55,axiom,
! [X0,X1] : between(X0,X0,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t2) ).
fof(f56,axiom,
! [X2,X0,X1] :
( ~ between(X0,X1,X2)
| ~ between(X1,X0,X2)
| X0 = X1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',b2) ).
fof(f61,axiom,
! [X2,X3,X0,X1] :
( between(X1,X2,X3)
| ~ between(X0,X2,X3)
| ~ between(X0,X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',b5) ).
fof(f69,axiom,
! [X0,X1] : X0 != extension(X1,X0,lower_dimension_point_1,lower_dimension_point_2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e3_1) ).
fof(f70,plain,
! [X0,X1] : extension(X1,X0,lower_dimension_point_1,lower_dimension_point_2) != X0,
inference(reorient_equations,[],[f69]) ).
fof(f71,axiom,
! [X2,X3,X0,X1] : equidistant(X0,extension(X1,X0,lower_dimension_point_1,lower_dimension_point_2),X2,extension(X3,X2,lower_dimension_point_1,lower_dimension_point_2)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e3_2) ).
fof(f75,axiom,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( equidistant(X1,X6,X3,X7)
| ~ equidistant(X0,X4,X2,X5)
| ~ equidistant(X0,X6,X2,X7)
| ~ equidistant(X4,X6,X5,X7)
| ~ between(X0,X1,X4)
| ~ between(X2,X3,X5)
| ~ equidistant(X0,X1,X2,X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d12) ).
fof(f76,axiom,
! [X2,X3,X0,X1,X4,X5] :
( equidistant(X1,X2,X4,X5)
| ~ between(X3,X4,X5)
| ~ equidistant(X0,X1,X3,X4)
| ~ equidistant(X0,X2,X3,X5)
| ~ between(X0,X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d13) ).
fof(f79,negated_conjecture,
( ~ equidistant(u,v,u1,insertion(u1,w1,u,v))
| between(u,v,w) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',part_1) ).
fof(f80,negated_conjecture,
( ~ equidistant(u,v,u1,insertion(u1,w1,u,v))
| equidistant(u,w,u1,w1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',part_2) ).
fof(f81,negated_conjecture,
( ~ equidistant(u,v,u1,insertion(u1,w1,u,v))
| ~ between(u1,insertion(u1,w1,u,v),w1)
| ~ equidistant(v,w,insertion(u1,w1,u,v),w1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',part_3) ).
fof(f89,plain,
( ~ equidistant(u,v,u1,extension(extension(w1,u1,lower_dimension_point_1,lower_dimension_point_2),u1,u,v))
| between(u,v,w) ),
inference(definition_unfolding,[],[f79,f20]) ).
fof(f90,plain,
( ~ equidistant(u,v,u1,extension(extension(w1,u1,lower_dimension_point_1,lower_dimension_point_2),u1,u,v))
| equidistant(u,w,u1,w1) ),
inference(definition_unfolding,[],[f80,f20]) ).
fof(f91,plain,
( ~ equidistant(u,v,u1,extension(extension(w1,u1,lower_dimension_point_1,lower_dimension_point_2),u1,u,v))
| ~ between(u1,extension(extension(w1,u1,lower_dimension_point_1,lower_dimension_point_2),u1,u,v),w1)
| ~ equidistant(v,w,extension(extension(w1,u1,lower_dimension_point_1,lower_dimension_point_2),u1,u,v),w1) ),
inference(definition_unfolding,[],[f81,f20,f20,f20]) ).
fof(f95,definition,
sF0 = extension(w1,u1,lower_dimension_point_1,lower_dimension_point_2),
introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).
fof(f96,plain,
extension(w1,u1,lower_dimension_point_1,lower_dimension_point_2) = sF0,
inference(reorient_equations,[],[f95]) ).
fof(f97,definition,
sF1 = extension(sF0,u1,u,v),
introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).
fof(f98,plain,
extension(sF0,u1,u,v) = sF1,
inference(reorient_equations,[],[f97]) ).
fof(f99,plain,
( ~ equidistant(u,v,u1,sF1)
| between(u,v,w) ),
inference(definition_folding,[],[f89,f98,f96]) ).
fof(f100,plain,
( ~ equidistant(u,v,u1,sF1)
| equidistant(u,w,u1,w1) ),
inference(definition_folding,[],[f90,f98,f96]) ).
fof(f101,plain,
( ~ equidistant(u,v,u1,sF1)
| ~ between(u1,sF1,w1)
| ~ equidistant(v,w,sF1,w1) ),
inference(definition_folding,[],[f91,f98,f96,f98,f96,f98,f96]) ).
fof(f118,definition,
( spl2_4
<=> equidistant(v,w,sF1,w1) ),
introduced(definition,[new_symbols(definition,[spl2_4])],[avatar_definition]) ).
fof(f119,plain,
( equidistant(v,w,sF1,w1)
| ~ spl2_4 ),
inference(avatar_component_clause,[],[f118]) ).
fof(f120,plain,
( ~ equidistant(v,w,sF1,w1)
| spl2_4 ),
inference(avatar_component_clause,[],[f118]) ).
fof(f122,definition,
( spl2_5
<=> between(u1,sF1,w1) ),
introduced(definition,[new_symbols(definition,[spl2_5])],[avatar_definition]) ).
fof(f124,plain,
( ~ between(u1,sF1,w1)
| spl2_5 ),
inference(avatar_component_clause,[],[f122]) ).
fof(f126,definition,
( spl2_6
<=> equidistant(u,v,u1,sF1) ),
introduced(definition,[new_symbols(definition,[spl2_6])],[avatar_definition]) ).
fof(f127,plain,
( equidistant(u,v,u1,sF1)
| ~ spl2_6 ),
inference(avatar_component_clause,[],[f126]) ).
fof(f128,plain,
( ~ equidistant(u,v,u1,sF1)
| spl2_6 ),
inference(avatar_component_clause,[],[f126]) ).
fof(f129,plain,
( ~ spl2_4
| ~ spl2_5
| ~ spl2_6 ),
inference(avatar_split_clause,[],[f101,f126,f122,f118]) ).
fof(f131,definition,
( spl2_7
<=> equidistant(u,w,u1,w1) ),
introduced(definition,[new_symbols(definition,[spl2_7])],[avatar_definition]) ).
fof(f133,plain,
( equidistant(u,w,u1,w1)
| ~ spl2_7 ),
inference(avatar_component_clause,[],[f131]) ).
fof(f134,plain,
( spl2_7
| ~ spl2_6 ),
inference(avatar_split_clause,[],[f100,f126,f131]) ).
fof(f136,definition,
( spl2_8
<=> between(u,v,w) ),
introduced(definition,[new_symbols(definition,[spl2_8])],[avatar_definition]) ).
fof(f138,plain,
( between(u,v,w)
| ~ spl2_8 ),
inference(avatar_component_clause,[],[f136]) ).
fof(f139,plain,
( spl2_8
| ~ spl2_6 ),
inference(avatar_split_clause,[],[f99,f126,f136]) ).
fof(f157,definition,
( spl2_12
<=> extension(w1,u1,lower_dimension_point_1,lower_dimension_point_2) = sF0 ),
introduced(definition,[new_symbols(definition,[spl2_12])],[avatar_definition]) ).
fof(f159,plain,
( extension(w1,u1,lower_dimension_point_1,lower_dimension_point_2) = sF0
| ~ spl2_12 ),
inference(avatar_component_clause,[],[f157]) ).
fof(f160,plain,
spl2_12,
inference(avatar_split_clause,[],[f96,f157]) ).
fof(f162,definition,
( spl2_13
<=> extension(sF0,u1,u,v) = sF1 ),
introduced(definition,[new_symbols(definition,[spl2_13])],[avatar_definition]) ).
fof(f164,plain,
( extension(sF0,u1,u,v) = sF1
| ~ spl2_13 ),
inference(avatar_component_clause,[],[f162]) ).
fof(f165,plain,
spl2_13,
inference(avatar_split_clause,[],[f98,f162]) ).
fof(f166,plain,
( between(sF0,u1,sF1)
| ~ spl2_13 ),
inference(superposition,[],[f4,f164]) ).
fof(f167,plain,
( between(w1,u1,sF0)
| ~ spl2_12 ),
inference(superposition,[],[f4,f159]) ).
fof(f169,definition,
( spl2_14
<=> between(w1,u1,sF0) ),
introduced(definition,[new_symbols(definition,[spl2_14])],[avatar_definition]) ).
fof(f171,plain,
( between(w1,u1,sF0)
| ~ spl2_14 ),
inference(avatar_component_clause,[],[f169]) ).
fof(f172,plain,
( spl2_14
| ~ spl2_12 ),
inference(avatar_split_clause,[],[f167,f157,f169]) ).
fof(f174,definition,
( spl2_15
<=> between(sF0,u1,sF1) ),
introduced(definition,[new_symbols(definition,[spl2_15])],[avatar_definition]) ).
fof(f176,plain,
( between(sF0,u1,sF1)
| ~ spl2_15 ),
inference(avatar_component_clause,[],[f174]) ).
fof(f177,plain,
( spl2_15
| ~ spl2_13 ),
inference(avatar_split_clause,[],[f166,f162,f174]) ).
fof(f178,plain,
( equidistant(u1,sF1,u,v)
| ~ spl2_13 ),
inference(superposition,[],[f5,f164]) ).
fof(f186,definition,
( spl2_17
<=> equidistant(u1,sF1,u,v) ),
introduced(definition,[new_symbols(definition,[spl2_17])],[avatar_definition]) ).
fof(f188,plain,
( equidistant(u1,sF1,u,v)
| ~ spl2_17 ),
inference(avatar_component_clause,[],[f186]) ).
fof(f189,plain,
( spl2_17
| ~ spl2_13 ),
inference(avatar_split_clause,[],[f178,f162,f186]) ).
fof(f190,plain,
! [X2,X3,X0,X1] : between(extension(X0,X1,X2,X3),X1,X0),
inference(unit_resulting_resolution,[],[f54,f4]) ).
fof(f191,plain,
( between(sF0,u1,w1)
| ~ spl2_14 ),
inference(unit_resulting_resolution,[],[f54,f171]) ).
fof(f193,definition,
( spl2_18
<=> between(sF0,u1,w1) ),
introduced(definition,[new_symbols(definition,[spl2_18])],[avatar_definition]) ).
fof(f196,plain,
( spl2_18
| ~ spl2_14 ),
inference(avatar_split_clause,[],[f191,f169,f193]) ).
fof(f198,plain,
( between(sF1,u1,sF0)
| ~ spl2_13 ),
inference(superposition,[],[f190,f164]) ).
fof(f201,definition,
( spl2_19
<=> between(sF1,u1,sF0) ),
introduced(definition,[new_symbols(definition,[spl2_19])],[avatar_definition]) ).
fof(f203,plain,
( between(sF1,u1,sF0)
| ~ spl2_19 ),
inference(avatar_component_clause,[],[f201]) ).
fof(f204,plain,
( spl2_19
| ~ spl2_13 ),
inference(avatar_split_clause,[],[f198,f162,f201]) ).
fof(f445,plain,
( ~ equidistant(u1,sF1,u,v)
| spl2_6 ),
inference(unit_resulting_resolution,[],[f2,f21,f128]) ).
fof(f473,plain,
( $false
| spl2_6
| ~ spl2_17 ),
inference(forward_subsumption_resolution,[],[f445,f188]) ).
fof(f474,plain,
( spl2_6
| ~ spl2_17 ),
inference(avatar_contradiction_clause,[],[f473]) ).
fof(f528,plain,
( between(w,v,u)
| ~ spl2_8 ),
inference(unit_resulting_resolution,[],[f54,f138]) ).
fof(f566,definition,
( spl2_40
<=> between(w,v,u) ),
introduced(definition,[new_symbols(definition,[spl2_40])],[avatar_definition]) ).
fof(f568,plain,
( between(w,v,u)
| ~ spl2_40 ),
inference(avatar_component_clause,[],[f566]) ).
fof(f569,plain,
( spl2_40
| ~ spl2_8 ),
inference(avatar_split_clause,[],[f528,f136,f566]) ).
fof(f576,plain,
( ! [X0,X1] : between(v,u,extension(w,u,X0,X1))
| ~ spl2_40 ),
inference(unit_resulting_resolution,[],[f61,f4,f568]) ).
fof(f619,plain,
( ~ between(u1,sF1,w1)
| spl2_4
| ~ spl2_6
| ~ spl2_7
| ~ spl2_8 ),
inference(unit_resulting_resolution,[],[f75,f120,f42,f133,f138,f133,f127]) ).
fof(f628,plain,
( ~ spl2_5
| spl2_4
| ~ spl2_6
| ~ spl2_7
| ~ spl2_8 ),
inference(avatar_split_clause,[],[f619,f136,f131,f126,f118,f122]) ).
fof(f632,plain,
( ~ between(sF0,sF1,w1)
| spl2_5
| ~ spl2_15 ),
inference(unit_resulting_resolution,[],[f61,f176,f124]) ).
fof(f645,definition,
( spl2_45
<=> between(sF0,sF1,w1) ),
introduced(definition,[new_symbols(definition,[spl2_45])],[avatar_definition]) ).
fof(f648,plain,
( ~ spl2_45
| spl2_5
| ~ spl2_15 ),
inference(avatar_split_clause,[],[f632,f174,f122,f645]) ).
fof(f719,plain,
! [X2,X3,X0,X1,X4] :
( X0 = X1
| ~ between(X2,X3,X3)
| ~ equidistant(X4,X0,X2,X3)
| ~ equidistant(X4,X1,X2,X3)
| ~ between(X4,X0,X1) ),
inference(resolution,[],[f3,f76]) ).
fof(f723,plain,
! [X2,X3,X0,X1,X4] :
( ~ between(X4,X0,X1)
| ~ equidistant(X4,X0,X2,X3)
| ~ equidistant(X4,X1,X2,X3)
| X0 = X1 ),
inference(forward_subsumption_resolution,[],[f719,f52]) ).
fof(f973,plain,
( ! [X0,X1] : equidistant(X0,extension(X1,X0,lower_dimension_point_1,lower_dimension_point_2),u1,sF0)
| ~ spl2_12 ),
inference(superposition,[],[f71,f159]) ).
fof(f1010,plain,
! [X2,X0,X1] :
( ~ equidistant(X0,X0,X1,X2)
| X1 = X2 ),
inference(resolution,[],[f22,f3]) ).
fof(f1045,plain,
( equidistant(w,u,w1,u1)
| ~ spl2_7 ),
inference(unit_resulting_resolution,[],[f25,f133]) ).
fof(f1046,plain,
( equidistant(v,u,sF1,u1)
| ~ spl2_6 ),
inference(unit_resulting_resolution,[],[f25,f127]) ).
fof(f1050,plain,
( ~ equidistant(w,v,w1,sF1)
| spl2_4 ),
inference(resolution,[],[f25,f120]) ).
fof(f1052,definition,
( spl2_56
<=> equidistant(w,v,w1,sF1) ),
introduced(definition,[new_symbols(definition,[spl2_56])],[avatar_definition]) ).
fof(f1054,plain,
( ~ equidistant(w,v,w1,sF1)
| spl2_56 ),
inference(avatar_component_clause,[],[f1052]) ).
fof(f1055,plain,
( ~ spl2_56
| spl2_4 ),
inference(avatar_split_clause,[],[f1050,f118,f1052]) ).
fof(f1067,definition,
( spl2_59
<=> equidistant(w,u,w1,u1) ),
introduced(definition,[new_symbols(definition,[spl2_59])],[avatar_definition]) ).
fof(f1069,plain,
( equidistant(w,u,w1,u1)
| ~ spl2_59 ),
inference(avatar_component_clause,[],[f1067]) ).
fof(f1070,plain,
( spl2_59
| ~ spl2_7 ),
inference(avatar_split_clause,[],[f1045,f131,f1067]) ).
fof(f1072,definition,
( spl2_60
<=> equidistant(v,u,sF1,u1) ),
introduced(definition,[new_symbols(definition,[spl2_60])],[avatar_definition]) ).
fof(f1074,plain,
( equidistant(v,u,sF1,u1)
| ~ spl2_60 ),
inference(avatar_component_clause,[],[f1072]) ).
fof(f1075,plain,
( spl2_60
| ~ spl2_6 ),
inference(avatar_split_clause,[],[f1046,f126,f1072]) ).
fof(f1152,plain,
! [X2,X3,X0,X1] : equidistant(X0,X1,X2,extension(X3,X2,X1,X0)),
inference(unit_resulting_resolution,[],[f27,f5]) ).
fof(f1177,plain,
! [X2,X3,X0,X1] : equidistant(X0,X1,extension(X2,X3,X1,X0),X3),
inference(unit_resulting_resolution,[],[f28,f5]) ).
fof(f1345,definition,
( spl2_75
<=> u1 = w1 ),
introduced(definition,[new_symbols(definition,[spl2_75])],[avatar_definition]) ).
fof(f1346,plain,
( u1 != w1
| spl2_75 ),
inference(avatar_component_clause,[],[f1345]) ).
fof(f1347,plain,
( u1 = w1
| ~ spl2_75 ),
inference(avatar_component_clause,[],[f1345]) ).
fof(f1354,definition,
( spl2_77
<=> u1 = sF1 ),
introduced(definition,[new_symbols(definition,[spl2_77])],[avatar_definition]) ).
fof(f1355,plain,
( u1 != sF1
| spl2_77 ),
inference(avatar_component_clause,[],[f1354]) ).
fof(f1363,definition,
( spl2_79
<=> u = v ),
introduced(definition,[new_symbols(definition,[spl2_79])],[avatar_definition]) ).
fof(f1364,plain,
( u != v
| spl2_79 ),
inference(avatar_component_clause,[],[f1363]) ).
fof(f1365,plain,
( u = v
| ~ spl2_79 ),
inference(avatar_component_clause,[],[f1363]) ).
fof(f1592,definition,
( spl2_97
<=> u = w ),
introduced(definition,[new_symbols(definition,[spl2_97])],[avatar_definition]) ).
fof(f1593,plain,
( u != w
| spl2_97 ),
inference(avatar_component_clause,[],[f1592]) ).
fof(f1594,plain,
( u = w
| ~ spl2_97 ),
inference(avatar_component_clause,[],[f1592]) ).
fof(f1602,plain,
( between(u,v,u)
| ~ spl2_8
| ~ spl2_97 ),
inference(superposition,[],[f138,f1594]) ).
fof(f1613,definition,
( spl2_100
<=> between(u,v,u) ),
introduced(definition,[new_symbols(definition,[spl2_100])],[avatar_definition]) ).
fof(f1615,plain,
( between(u,v,u)
| ~ spl2_100 ),
inference(avatar_component_clause,[],[f1613]) ).
fof(f1617,plain,
( spl2_100
| ~ spl2_8
| ~ spl2_97 ),
inference(avatar_split_clause,[],[f1602,f1592,f136,f1613]) ).
fof(f1999,plain,
( u1 != sF1
| between(sF0,sF1,w1)
| ~ between(sF0,u1,w1) ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f2117,plain,
( ~ between(v,u,u)
| u = v
| ~ spl2_100 ),
inference(resolution,[],[f1615,f56]) ).
fof(f2120,plain,
( u = v
| ~ spl2_100 ),
inference(forward_subsumption_resolution,[],[f2117,f52]) ).
fof(f2158,plain,
( $false
| spl2_79
| ~ spl2_100 ),
inference(forward_subsumption_resolution,[],[f2120,f1364]) ).
fof(f2159,plain,
( spl2_79
| ~ spl2_100 ),
inference(avatar_contradiction_clause,[],[f2158]) ).
fof(f12690,plain,
( ~ equidistant(w,w,w1,u1)
| ~ spl2_59
| spl2_97 ),
inference(unit_resulting_resolution,[],[f723,f1593,f1069,f55]) ).
fof(f12910,definition,
( spl2_317
<=> equidistant(w,w,w1,u1) ),
introduced(definition,[new_symbols(definition,[spl2_317])],[avatar_definition]) ).
fof(f12912,plain,
( ~ equidistant(w,w,w1,u1)
| spl2_317 ),
inference(avatar_component_clause,[],[f12910]) ).
fof(f12913,plain,
( ~ spl2_317
| ~ spl2_59
| spl2_97 ),
inference(avatar_split_clause,[],[f12690,f1592,f1067,f12910]) ).
fof(f13009,plain,
( ~ equidistant(w,w,u1,u1)
| ~ spl2_75
| spl2_317 ),
inference(forward_demodulation,[],[f12912,f1347]) ).
fof(f13036,plain,
( $false
| ~ spl2_75
| spl2_317 ),
inference(forward_subsumption_resolution,[],[f13009,f42]) ).
fof(f13037,plain,
( ~ spl2_75
| spl2_317 ),
inference(avatar_contradiction_clause,[],[f13036]) ).
fof(f14127,plain,
( ! [X2,X3,X0,X1] : extension(w1,u1,X0,X1) = extension(w1,u1,X2,extension(X3,X2,X0,X1))
| spl2_75 ),
inference(unit_resulting_resolution,[],[f47,f5,f1346]) ).
fof(f19331,definition,
( spl2_495
<=> equidistant(w,w,extension(u1,sF1,w,v),w1) ),
introduced(definition,[new_symbols(definition,[spl2_495])],[avatar_definition]) ).
fof(f19332,plain,
( equidistant(w,w,extension(u1,sF1,w,v),w1)
| ~ spl2_495 ),
inference(avatar_component_clause,[],[f19331]) ).
fof(f19333,plain,
( ~ equidistant(w,w,extension(u1,sF1,w,v),w1)
| spl2_495 ),
inference(avatar_component_clause,[],[f19331]) ).
fof(f19594,plain,
( ~ equidistant(v,w,sF1,w1)
| ~ spl2_6
| ~ spl2_7
| ~ spl2_8
| spl2_79
| spl2_495 ),
inference(unit_resulting_resolution,[],[f6,f1364,f138,f127,f133,f4,f1152,f19333]) ).
fof(f20063,plain,
( ~ equidistant(extension(w,u,lower_dimension_point_1,lower_dimension_point_2),v,extension(w1,u1,u,extension(w,u,lower_dimension_point_1,lower_dimension_point_2)),sF1)
| ~ spl2_6
| ~ spl2_7
| spl2_56 ),
inference(unit_resulting_resolution,[],[f6,f70,f190,f1054,f133,f127,f190,f1177]) ).
fof(f23180,plain,
( ~ equidistant(extension(w,u,lower_dimension_point_1,lower_dimension_point_2),v,extension(w1,u1,lower_dimension_point_1,lower_dimension_point_2),sF1)
| ~ spl2_6
| ~ spl2_7
| spl2_56
| spl2_75 ),
inference(forward_demodulation,[],[f20063,f14127]) ).
fof(f23439,plain,
( ~ equidistant(extension(w,u,lower_dimension_point_1,lower_dimension_point_2),v,sF0,sF1)
| ~ spl2_6
| ~ spl2_7
| ~ spl2_12
| spl2_56
| spl2_75 ),
inference(forward_demodulation,[],[f23180,f159]) ).
fof(f23468,definition,
( spl2_529
<=> equidistant(extension(w,u,lower_dimension_point_1,lower_dimension_point_2),v,sF0,sF1) ),
introduced(definition,[new_symbols(definition,[spl2_529])],[avatar_definition]) ).
fof(f23470,plain,
( ~ equidistant(extension(w,u,lower_dimension_point_1,lower_dimension_point_2),v,sF0,sF1)
| spl2_529 ),
inference(avatar_component_clause,[],[f23468]) ).
fof(f23471,plain,
( ~ spl2_529
| ~ spl2_6
| ~ spl2_7
| ~ spl2_12
| spl2_56
| spl2_75 ),
inference(avatar_split_clause,[],[f23439,f1345,f1052,f157,f131,f126,f23468]) ).
fof(f23598,plain,
( ~ between(v,u,extension(w,u,lower_dimension_point_1,lower_dimension_point_2))
| ~ spl2_6
| ~ spl2_12
| ~ spl2_19
| ~ spl2_60
| spl2_79
| spl2_529 ),
inference(unit_resulting_resolution,[],[f6,f1364,f203,f1074,f42,f127,f973,f23470]) ).
fof(f23685,plain,
( $false
| ~ spl2_6
| ~ spl2_12
| ~ spl2_19
| ~ spl2_40
| ~ spl2_60
| spl2_79
| spl2_529 ),
inference(forward_subsumption_resolution,[],[f23598,f576]) ).
fof(f23686,plain,
( ~ spl2_6
| ~ spl2_12
| ~ spl2_19
| ~ spl2_40
| ~ spl2_60
| spl2_79
| spl2_529 ),
inference(avatar_contradiction_clause,[],[f23685]) ).
fof(f23729,plain,
( $false
| ~ spl2_4
| ~ spl2_6
| ~ spl2_7
| ~ spl2_8
| spl2_79
| spl2_495 ),
inference(forward_subsumption_resolution,[],[f19594,f119]) ).
fof(f23730,plain,
( ~ spl2_4
| ~ spl2_6
| ~ spl2_7
| ~ spl2_8
| spl2_79
| spl2_495 ),
inference(avatar_contradiction_clause,[],[f23729]) ).
fof(f24991,plain,
( w1 = extension(u1,sF1,w,v)
| ~ spl2_495 ),
inference(resolution,[],[f19332,f1010]) ).
fof(f24997,definition,
( spl2_602
<=> w1 = extension(u1,sF1,w,v) ),
introduced(definition,[new_symbols(definition,[spl2_602])],[avatar_definition]) ).
fof(f24999,plain,
( w1 = extension(u1,sF1,w,v)
| ~ spl2_602 ),
inference(avatar_component_clause,[],[f24997]) ).
fof(f25000,plain,
( spl2_602
| ~ spl2_495 ),
inference(avatar_split_clause,[],[f24991,f19331,f24997]) ).
fof(f28667,plain,
( between(u1,sF1,w1)
| ~ spl2_602 ),
inference(superposition,[],[f4,f24999]) ).
fof(f28681,plain,
( $false
| spl2_5
| ~ spl2_602 ),
inference(forward_subsumption_resolution,[],[f28667,f124]) ).
fof(f28682,plain,
( spl2_5
| ~ spl2_602 ),
inference(avatar_contradiction_clause,[],[f28681]) ).
fof(f29188,plain,
( sF1 = extension(sF0,u1,u,u)
| ~ spl2_13
| ~ spl2_79 ),
inference(superposition,[],[f164,f1365]) ).
fof(f29253,plain,
( u1 = sF1
| ~ spl2_13
| ~ spl2_79 ),
inference(forward_demodulation,[],[f29188,f31]) ).
fof(f29269,plain,
( $false
| ~ spl2_13
| spl2_77
| ~ spl2_79 ),
inference(forward_subsumption_resolution,[],[f29253,f1355]) ).
fof(f29270,plain,
( ~ spl2_13
| spl2_77
| ~ spl2_79 ),
inference(avatar_contradiction_clause,[],[f29269]) ).
cnf(s4,plain,
( ~ spl2_4
| ~ spl2_5
| ~ spl2_6 ),
inference(sat_conversion,[],[f129]) ).
cnf(s5,plain,
( ~ spl2_6
| spl2_7 ),
inference(sat_conversion,[],[f134]) ).
cnf(s6,plain,
( ~ spl2_6
| spl2_8 ),
inference(sat_conversion,[],[f139]) ).
cnf(s10,plain,
spl2_12,
inference(sat_conversion,[],[f160]) ).
cnf(s11,plain,
spl2_13,
inference(sat_conversion,[],[f165]) ).
cnf(s12,plain,
( ~ spl2_12
| spl2_14 ),
inference(sat_conversion,[],[f172]) ).
cnf(s13,plain,
( ~ spl2_13
| spl2_15 ),
inference(sat_conversion,[],[f177]) ).
cnf(s15,plain,
( ~ spl2_13
| spl2_17 ),
inference(sat_conversion,[],[f189]) ).
cnf(s16,plain,
( ~ spl2_14
| spl2_18 ),
inference(sat_conversion,[],[f196]) ).
cnf(s17,plain,
( ~ spl2_13
| spl2_19 ),
inference(sat_conversion,[],[f204]) ).
cnf(s30,plain,
( spl2_6
| ~ spl2_17 ),
inference(sat_conversion,[],[f474]) ).
cnf(s39,plain,
( ~ spl2_8
| spl2_40 ),
inference(sat_conversion,[],[f569]) ).
cnf(s44,plain,
( spl2_4
| ~ spl2_5
| ~ spl2_6
| ~ spl2_7
| ~ spl2_8 ),
inference(sat_conversion,[],[f628]) ).
cnf(s47,plain,
( spl2_5
| ~ spl2_15
| ~ spl2_45 ),
inference(sat_conversion,[],[f648]) ).
cnf(s61,plain,
( spl2_4
| ~ spl2_56 ),
inference(sat_conversion,[],[f1055]) ).
cnf(s64,plain,
( ~ spl2_7
| spl2_59 ),
inference(sat_conversion,[],[f1070]) ).
cnf(s65,plain,
( ~ spl2_6
| spl2_60 ),
inference(sat_conversion,[],[f1075]) ).
cnf(s105,plain,
( ~ spl2_8
| ~ spl2_97
| spl2_100 ),
inference(sat_conversion,[],[f1617]) ).
cnf(s128,plain,
( ~ spl2_18
| spl2_45
| ~ spl2_77 ),
inference(sat_conversion,[],[f1999]) ).
cnf(s150,plain,
( spl2_79
| ~ spl2_100 ),
inference(sat_conversion,[],[f2159]) ).
cnf(s492,plain,
( ~ spl2_59
| spl2_97
| ~ spl2_317 ),
inference(sat_conversion,[],[f12913]) ).
cnf(s521,plain,
( ~ spl2_75
| spl2_317 ),
inference(sat_conversion,[],[f13037]) ).
cnf(s899,plain,
( ~ spl2_6
| ~ spl2_7
| ~ spl2_12
| spl2_56
| spl2_75
| ~ spl2_529 ),
inference(sat_conversion,[],[f23471]) ).
cnf(s933,plain,
( ~ spl2_6
| ~ spl2_12
| ~ spl2_19
| ~ spl2_40
| ~ spl2_60
| spl2_79
| spl2_529 ),
inference(sat_conversion,[],[f23686]) ).
cnf(s956,plain,
( ~ spl2_4
| ~ spl2_6
| ~ spl2_7
| ~ spl2_8
| spl2_79
| spl2_495 ),
inference(sat_conversion,[],[f23730]) ).
cnf(s1054,plain,
( ~ spl2_495
| spl2_602 ),
inference(sat_conversion,[],[f25000]) ).
cnf(s1466,plain,
( spl2_5
| ~ spl2_602 ),
inference(sat_conversion,[],[f28682]) ).
cnf(s1616,plain,
( ~ spl2_13
| spl2_77
| ~ spl2_79 ),
inference(sat_conversion,[],[f29270]) ).
cnf(s1617,plain,
spl2_19,
inference(rat,[],[s17,s11]) ).
cnf(s1618,plain,
spl2_17,
inference(rat,[],[s15,s11]) ).
cnf(s1619,plain,
spl2_15,
inference(rat,[],[s13,s11]) ).
cnf(s1631,plain,
spl2_6,
inference(rat,[],[s30,s1618]) ).
cnf(s1645,plain,
spl2_60,
inference(rat,[],[s65,s1631]) ).
cnf(s1667,plain,
spl2_14,
inference(rat,[],[s12,s10]) ).
cnf(s1716,plain,
spl2_18,
inference(rat,[],[s16,s1667]) ).
cnf(s1772,plain,
spl2_8,
inference(rat,[],[s6,s1631]) ).
cnf(s1784,plain,
spl2_40,
inference(rat,[],[s39,s1772]) ).
cnf(s1809,plain,
spl2_7,
inference(rat,[],[s5,s1631]) ).
cnf(s1816,plain,
spl2_59,
inference(rat,[],[s64,s1809]) ).
cnf(s1877,plain,
( ~ spl2_4
| ~ spl2_5 ),
inference(rat,[],[s4,s1631]) ).
cnf(s1878,plain,
spl2_4,
inference(rat,[],[s521,s492,s899,s105,s933,s150,s1616,s128,s47,s44,s61,s1816,s1631,s10,s1809,s1772,s1617,s1645,s1784,s11,s1716,s1619]) ).
cnf(s1892,plain,
~ spl2_5,
inference(rat,[],[s1877,s1878]) ).
cnf(s1916,plain,
~ spl2_602,
inference(rat,[],[s1466,s1892]) ).
cnf(s1923,plain,
~ spl2_45,
inference(rat,[],[s47,s1619,s1892]) ).
cnf(s1925,plain,
~ spl2_495,
inference(rat,[],[s1054,s1916]) ).
cnf(s1954,plain,
~ spl2_77,
inference(rat,[],[s128,s1716,s1923]) ).
cnf(s1964,plain,
spl2_79,
inference(rat,[],[s956,s1878,s1809,s1772,s1631,s1925]) ).
cnf(s1975,plain,
$false,
inference(rat,[],[s1616,s11,s1964,s1954]) ).
fof(f29271,plain,
$false,
inference(avatar_sat_refutation,[],[s1975]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GEO061-3 : TPTP v9.3.1. Bugfixed v1.2.1.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.13/0.38 % Computer : n008.cluster.edu
% 0.13/0.38 % Model : x86_64 x86_64
% 0.13/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.38 % Memory : 8046.5625MB
% 0.13/0.38 % OS : Linux 6.8.0-71-generic
% 0.13/0.38 % CPULimit : 300
% 0.13/0.38 % WCLimit : 300
% 0.13/0.38 % DateTime : Sun Sep 27 06:47:39 UTC 2026
% 0.13/0.38 % CPUTime :
% 0.13/0.38 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.16/0.42 Running first-order theorem proving
% 0.16/0.42 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 11.53/2.53 % (876056)Input is clausal, will run a generic CNF schedule.
% 11.53/2.53 % (876150)lrs+10_1_sil=8000:sp=occurrence:random_seed=1593457010:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 11.53/2.53 % (876147)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=2133928344:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 11.53/2.53 % (876149)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=567950762:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 11.53/2.53 % (876148)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=339832610:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 11.53/2.53 % (876150)Instruction limit reached!
% 11.53/2.53 % (876150)------------------------------
% 11.53/2.53 % (876150)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.53/2.53 % (876150)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.53/2.53 % (876150)CaDiCaL version: 2.1.3
% 11.53/2.53 % (876150)Termination reason: Instruction limit
% 11.53/2.53 % (876150)Termination phase: Saturation
% 11.53/2.53 % (876150)Time elapsed: 0.038 s
% 11.53/2.53 % (876150)Peak memory usage: 89 MB
% 11.53/2.53 % (876150)Instructions burned: 109 (million)
% 11.53/2.53 % (876157)dis-21_1_sil=8000:lcm=predicate:random_seed=1152979126:st=5:avsq=on:i=117:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/117Mi)
% 11.53/2.53 % (876154)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3347962506:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 11.53/2.53 % (876151)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=2826496398:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 11.53/2.53 % (876157)Instruction limit reached!
% 11.53/2.53 % (876157)------------------------------
% 11.53/2.53 % (876157)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.53/2.53 % (876157)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.53/2.53 % (876157)CaDiCaL version: 2.1.3
% 11.53/2.53 % (876157)Termination reason: Instruction limit
% 11.53/2.53 % (876157)Termination phase: Saturation
% 11.53/2.53 % (876157)Time elapsed: 0.065 s
% 11.53/2.53 % (876157)Peak memory usage: 89 MB
% 11.53/2.53 % (876157)Instructions burned: 118 (million)
% 11.53/2.53 % (876151)Instruction limit reached!
% 11.53/2.53 % (876151)------------------------------
% 11.53/2.53 % (876151)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.53/2.53 % (876151)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.53/2.53 % (876151)CaDiCaL version: 2.1.3
% 11.53/2.53 % (876151)Termination reason: Instruction limit
% 11.53/2.53 % (876151)Termination phase: Saturation
% 11.53/2.53 % (876151)Time elapsed: 0.070 s
% 11.53/2.53 % (876151)Peak memory usage: 89 MB
% 11.53/2.53 % (876151)Instructions burned: 115 (million)
% 11.53/2.53 % (876154)Instruction limit reached!
% 11.53/2.53 % (876154)------------------------------
% 11.53/2.53 % (876154)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.53/2.53 % (876154)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.53/2.53 % (876154)CaDiCaL version: 2.1.3
% 11.53/2.53 % (876154)Termination reason: Instruction limit
% 11.53/2.53 % (876154)Termination phase: Saturation
% 11.53/2.53 % (876154)Time elapsed: 0.112 s
% 11.53/2.53 % (876154)Peak memory usage: 89 MB
% 11.53/2.53 % (876154)Instructions burned: 182 (million)
% 11.53/2.53 % (876173)dis+1010_3_sil=8000:plsq=on:drc=off:fde=none:plsqc=1:bsd=on:plsqr=7,2:sos=on:spb=goal_then_units:random_seed=2873420243:i=143:sd=2:aac=none:ss=axioms:sgt=16_2998 on theBenchmark for (2998ds/143Mi)
% 11.53/2.53 % (876173)Refutation not found, incomplete strategy
% 11.53/2.53 % (876173)------------------------------
% 11.53/2.53 % (876173)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.53/2.53 % (876173)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.53/2.53 % (876173)CaDiCaL version: 2.1.3
% 11.53/2.53 % (876173)Termination reason: Refutation not found, incomplete strategy
% 11.53/2.53 % (876173)Time elapsed: 0.001 s
% 11.53/2.53 % (876173)Peak memory usage: 88 MB
% 11.53/2.53 % (876173)Instructions burned: 3 (million)
% 11.53/2.53 % (876177)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=3316772789:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2997 on theBenchmark for (2997ds/189Mi)
% 20.44/3.85 % (876178)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=3549818721:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 20.44/3.85 % (876173)------------------------------
% 20.44/3.85 % (876173)------------------------------
% 20.44/3.85 % (876180)lrs+10_64_to=lpo:sil=8000:random_seed=1380667627:i=126:bd=preordered_2997 on theBenchmark for (2997ds/126Mi)
% 20.44/3.85 % (876177)Instruction limit reached!
% 20.44/3.85 % (876177)------------------------------
% 20.44/3.85 % (876177)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.44/3.85 % (876177)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.44/3.85 % (876177)CaDiCaL version: 2.1.3
% 20.44/3.85 % (876177)Termination reason: Instruction limit
% 20.44/3.85 % (876177)Termination phase: Saturation
% 20.44/3.85 % (876177)Time elapsed: 0.149 s
% 20.44/3.85 % (876177)Peak memory usage: 89 MB
% 20.44/3.85 % (876177)Instructions burned: 189 (million)
% 20.44/3.85 % (876180)Instruction limit reached!
% 20.44/3.85 % (876180)------------------------------
% 20.44/3.85 % (876180)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.44/3.85 % (876180)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.44/3.85 % (876180)CaDiCaL version: 2.1.3
% 20.44/3.85 % (876180)Termination reason: Instruction limit
% 20.44/3.85 % (876180)Termination phase: Saturation
% 20.44/3.85 % (876180)Time elapsed: 0.135 s
% 20.44/3.85 % (876180)Peak memory usage: 89 MB
% 20.44/3.85 % (876180)Instructions burned: 126 (million)
% 20.44/3.85 % (876178)Instruction limit reached!
% 20.44/3.85 % (876178)------------------------------
% 20.44/3.85 % (876178)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.44/3.85 % (876178)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.44/3.85 % (876178)CaDiCaL version: 2.1.3
% 20.44/3.85 % (876178)Termination reason: Instruction limit
% 20.44/3.85 % (876178)Termination phase: Saturation
% 20.44/3.85 % (876178)Time elapsed: 0.211 s
% 20.44/3.85 % (876178)Peak memory usage: 90 MB
% 20.44/3.85 % (876178)Instructions burned: 220 (million)
% 20.44/3.85 % (876211)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=2211779624:avsq=on:i=194:fgj=on:bd=preordered_2994 on theBenchmark for (2994ds/194Mi)
% 20.44/3.85 % (876211)Instruction limit reached!
% 20.44/3.85 % (876211)------------------------------
% 20.44/3.85 % (876211)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.44/3.85 % (876211)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.44/3.85 % (876211)CaDiCaL version: 2.1.3
% 20.44/3.85 % (876211)Termination reason: Instruction limit
% 20.44/3.85 % (876211)Termination phase: Saturation
% 20.44/3.85 % (876211)Time elapsed: 0.074 s
% 20.44/3.85 % (876211)Peak memory usage: 90 MB
% 20.44/3.85 % (876211)Instructions burned: 196 (million)
% 20.44/3.85 % (876220)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=674421101:i=157:gtg=all_2994 on theBenchmark for (2994ds/157Mi)
% 20.44/3.85 % (876221)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=4281225495:i=3394:sd=4:ss=included:sgt=64_2993 on theBenchmark for (2993ds/3394Mi)
% 20.44/3.85 % (876223)lrs+1011_5_to=lpo:sil=8000:tgt=full:plsq=on:prc=on:drc=off:plsqr=31,4:sp=occurrence:urr=on:nwc=0.8:s2agt=16:br=off:random_seed=2517217144:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2993 on theBenchmark for (2993ds/106Mi)
% 20.44/3.85 % (876230)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=1049052950:i=107_2992 on theBenchmark for (2992ds/107Mi)
% 20.44/3.85 % (876230)Refutation not found, incomplete strategy
% 20.44/3.85 % (876230)------------------------------
% 20.44/3.85 % (876230)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.44/3.85 % (876230)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.44/3.85 % (876230)CaDiCaL version: 2.1.3
% 20.44/3.85 % (876230)Termination reason: Refutation not found, incomplete strategy
% 20.44/3.85 % (876230)Time elapsed: 0.001 s
% 20.44/3.85 % (876230)Peak memory usage: 88 MB
% 20.44/3.85 % (876230)Instructions burned: 3 (million)
% 20.44/3.85 % (876220)Instruction limit reached!
% 20.44/3.85 % (876220)------------------------------
% 20.44/3.85 % (876220)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.44/3.85 % (876220)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.59/5.83 % (876220)CaDiCaL version: 2.1.3
% 34.59/5.83 % (876220)Termination reason: Instruction limit
% 34.59/5.83 % (876220)Termination phase: Saturation
% 34.59/5.83 % (876220)Time elapsed: 0.104 s
% 34.59/5.83 % (876220)Peak memory usage: 90 MB
% 34.59/5.83 % (876220)Instructions burned: 158 (million)
% 34.59/5.83 % (876223)Instruction limit reached!
% 34.59/5.83 % (876223)------------------------------
% 34.59/5.83 % (876223)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.59/5.83 % (876223)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.59/5.83 % (876223)CaDiCaL version: 2.1.3
% 34.59/5.83 % (876223)Termination reason: Instruction limit
% 34.59/5.83 % (876223)Termination phase: Saturation
% 34.59/5.83 % (876223)Time elapsed: 0.060 s
% 34.59/5.83 % (876223)Peak memory usage: 89 MB
% 34.59/5.83 % (876223)Instructions burned: 107 (million)
% 34.59/5.83 % (876230)------------------------------
% 34.59/5.83 % (876230)------------------------------
% 34.59/5.83 % (876236)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=1884325327:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2990 on theBenchmark for (2990ds/242Mi)
% 34.59/5.83 % (876238)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=1939397990:cond=fast:i=5208:av=off_2990 on theBenchmark for (2990ds/5208Mi)
% 34.59/5.83 % (876284)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=886575125:i=134:sd=2:doe=on:ss=axioms:sgt=14_2989 on theBenchmark for (2989ds/134Mi)
% 34.59/5.83 % (876284)Instruction limit reached!
% 34.59/5.83 % (876284)------------------------------
% 34.59/5.83 % (876284)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.59/5.83 % (876284)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.59/5.83 % (876284)CaDiCaL version: 2.1.3
% 34.59/5.83 % (876284)Termination reason: Instruction limit
% 34.59/5.83 % (876284)Termination phase: Saturation
% 34.59/5.83 % (876284)Time elapsed: 0.049 s
% 34.59/5.83 % (876284)Peak memory usage: 89 MB
% 34.59/5.83 % (876284)Instructions burned: 134 (million)
% 34.59/5.83 % (876236)Instruction limit reached!
% 34.59/5.83 % (876236)------------------------------
% 34.59/5.83 % (876236)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.59/5.83 % (876236)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.59/5.83 % (876236)CaDiCaL version: 2.1.3
% 34.59/5.83 % (876236)Termination reason: Instruction limit
% 34.59/5.83 % (876236)Termination phase: Saturation
% 34.59/5.83 % (876236)Time elapsed: 0.155 s
% 34.59/5.83 % (876236)Peak memory usage: 90 MB
% 34.59/5.83 % (876236)Instructions burned: 243 (million)
% 34.59/5.83 % (876347)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=3652194728:i=499:bd=all_2987 on theBenchmark for (2987ds/499Mi)
% 34.59/5.83 % (876348)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=1861834512:i=191:fgj=on:bd=all_2987 on theBenchmark for (2987ds/191Mi)
% 34.59/5.83 % (876347)Instruction limit reached!
% 34.59/5.83 % (876347)------------------------------
% 34.59/5.83 % (876347)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.59/5.83 % (876347)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.59/5.83 % (876347)CaDiCaL version: 2.1.3
% 34.59/5.83 % (876347)Termination reason: Instruction limit
% 34.59/5.83 % (876347)Termination phase: Saturation
% 34.59/5.83 % (876347)Time elapsed: 0.135 s
% 34.59/5.83 % (876347)Peak memory usage: 91 MB
% 34.59/5.83 % (876347)Instructions burned: 502 (million)
% 34.59/5.83 % (876348)Instruction limit reached!
% 34.59/5.83 % (876348)------------------------------
% 34.59/5.83 % (876348)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.59/5.83 % (876348)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.59/5.83 % (876348)CaDiCaL version: 2.1.3
% 34.59/5.83 % (876348)Termination reason: Instruction limit
% 34.59/5.83 % (876348)Termination phase: Saturation
% 34.59/5.83 % (876348)Time elapsed: 0.122 s
% 34.59/5.83 % (876348)Peak memory usage: 90 MB
% 34.59/5.83 % (876348)Instructions burned: 192 (million)
% 34.59/5.83 % (876398)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=448192853:i=264:kws=precedence:fsr=off_2985 on theBenchmark for (2985ds/264Mi)
% 34.59/5.83 % (876398)Instruction limit reached!
% 34.59/5.83 % (876398)------------------------------
% 34.59/5.83 % (876398)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 52.07/8.23 % (876398)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.07/8.23 % (876398)CaDiCaL version: 2.1.3
% 52.07/8.23 % (876398)Termination reason: Instruction limit
% 52.07/8.23 % (876398)Termination phase: Saturation
% 52.07/8.23 % (876398)Time elapsed: 0.083 s
% 52.07/8.23 % (876398)Peak memory usage: 90 MB
% 52.07/8.23 % (876398)Instructions burned: 267 (million)
% 52.07/8.23 % (876399)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=243383172:cond=on:i=156:bs=on:gtg=exists_all:er=known_2985 on theBenchmark for (2985ds/156Mi)
% 52.07/8.23 % (876399)Instruction limit reached!
% 52.07/8.23 % (876399)------------------------------
% 52.07/8.23 % (876399)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 52.07/8.23 % (876399)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.07/8.23 % (876399)CaDiCaL version: 2.1.3
% 52.07/8.23 % (876399)Termination reason: Instruction limit
% 52.07/8.23 % (876399)Termination phase: Saturation
% 52.07/8.23 % (876399)Time elapsed: 0.088 s
% 52.07/8.23 % (876399)Peak memory usage: 89 MB
% 52.07/8.23 % (876399)Instructions burned: 157 (million)
% 52.07/8.23 % (876401)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=reverse_frequency:spb=units:lcm=predicate:urr=on:s2agt=8:updr=off:random_seed=3895677290:i=3256:kws=precedence:bd=preordered:av=off_2983 on theBenchmark for (2983ds/3256Mi)
% 52.07/8.23 % (876403)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=2998835752:i=537:av=off:ss=included_2982 on theBenchmark for (2982ds/537Mi)
% 52.07/8.23 % (876403)Instruction limit reached!
% 52.07/8.23 % (876403)------------------------------
% 52.07/8.23 % (876403)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 52.07/8.23 % (876403)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.07/8.23 % (876403)CaDiCaL version: 2.1.3
% 52.07/8.23 % (876403)Termination reason: Instruction limit
% 52.07/8.23 % (876403)Termination phase: Saturation
% 52.07/8.23 % (876403)Time elapsed: 0.276 s
% 52.07/8.23 % (876403)Peak memory usage: 89 MB
% 52.07/8.23 % (876403)Instructions burned: 537 (million)
% 52.07/8.23 % (876406)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=1148298935:i=180:bd=preordered:av=off_2977 on theBenchmark for (2977ds/180Mi)
% 52.07/8.23 % (876406)Instruction limit reached!
% 52.07/8.23 % (876406)------------------------------
% 52.07/8.23 % (876406)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 52.07/8.23 % (876406)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.07/8.23 % (876406)CaDiCaL version: 2.1.3
% 52.07/8.23 % (876406)Termination reason: Instruction limit
% 52.07/8.23 % (876406)Termination phase: Saturation
% 52.07/8.23 % (876406)Time elapsed: 0.096 s
% 52.07/8.23 % (876406)Peak memory usage: 89 MB
% 52.07/8.23 % (876406)Instructions burned: 181 (million)
% 52.07/8.23 % (876408)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:sas=cadical:sp=reverse_frequency:bsr=on:alpa=false:sac=on:random_seed=2588818193:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2975 on theBenchmark for (2975ds/10307Mi)
% 52.07/8.23 % (876401)Instruction limit reached!
% 52.07/8.23 % (876401)------------------------------
% 52.07/8.23 % (876401)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 52.07/8.23 % (876401)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.07/8.23 % (876401)CaDiCaL version: 2.1.3
% 52.07/8.23 % (876401)Termination reason: Instruction limit
% 52.07/8.23 % (876401)Termination phase: Saturation
% 52.07/8.23 % (876401)Time elapsed: 1.031 s
% 52.07/8.23 % (876401)Peak memory usage: 141 MB
% 52.07/8.23 % (876401)Instructions burned: 3258 (million)
% 52.07/8.23 % (876410)lrs-1010_1024_to=lpo:sil=8000:tgt=ground:plsq=on:plsqc=1:sas=cadical:plsqr=1,32:sp=arity:lma=off:spb=goal:acc=on:bce=on:nwc=1.2:alpa=false:random_seed=1814073072:i=412:gtgl=4:gtg=exists_all_2971 on theBenchmark for (2971ds/412Mi)
% 52.07/8.23 % (876221)Instruction limit reached!
% 52.07/8.23 % (876221)------------------------------
% 52.07/8.23 % (876221)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 52.07/8.23 % (876221)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.07/8.23 % (876221)CaDiCaL version: 2.1.3
% 52.07/8.23 % (876221)Termination reason: Instruction limit
% 52.07/8.23 % (876221)Termination phase: Saturation
% 52.07/8.23 % (876221)Time elapsed: 2.113 s
% 52.07/8.23 % (876221)Peak memory usage: 148 MB
% 70.29/10.87 % (876221)Instructions burned: 3395 (million)
% 70.29/10.87 % (876410)Instruction limit reached!
% 70.29/10.87 % (876410)------------------------------
% 70.29/10.87 % (876410)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 70.29/10.87 % (876410)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 70.29/10.87 % (876410)CaDiCaL version: 2.1.3
% 70.29/10.87 % (876410)Termination reason: Instruction limit
% 70.29/10.87 % (876410)Termination phase: Saturation
% 70.29/10.87 % (876410)Time elapsed: 0.097 s
% 70.29/10.87 % (876410)Peak memory usage: 89 MB
% 70.29/10.87 % (876410)Instructions burned: 414 (million)
% 70.29/10.87 % (876412)ott+1002_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:etr=on:spb=units:urr=on:bsr=unit_only:gs=on:s2agt=16:br=off:random_seed=1652311722:s2pl=no:i=8478:s2at=4:nm=6_2970 on theBenchmark for (2970ds/8478Mi)
% 70.29/10.87 % (876413)ott-1011_2_sil=32000:bsd=on:sp=reverse_frequency:erd=off:urr=on:rnwc=on:gs=on:s2agt=70:updr=off:lftc=20:random_seed=763316903:s2a=on:i=303:s2at=2:sd=1:kws=inv_arity:bs=on:ins=10:fdi=1024:sup=off:ss=included_2969 on theBenchmark for (2969ds/303Mi)
% 70.29/10.87 % (876413)Instruction limit reached!
% 70.29/10.87 % (876413)------------------------------
% 70.29/10.87 % (876413)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 70.29/10.87 % (876413)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 70.29/10.87 % (876413)CaDiCaL version: 2.1.3
% 70.29/10.87 % (876413)Termination reason: Instruction limit
% 70.29/10.87 % (876413)Termination phase: Saturation
% 70.29/10.87 % (876413)Time elapsed: 0.082 s
% 70.29/10.87 % (876413)Peak memory usage: 91 MB
% 70.29/10.87 % (876413)Instructions burned: 308 (million)
% 70.29/10.87 % (876416)lrs+10_1_to=lpo:sil=16000:fde=none:sos=on:urr=on:bsr=on:random_seed=932093695:st=4:i=720:sd=3:fsr=off:ss=axioms_2967 on theBenchmark for (2967ds/720Mi)
% 70.29/10.87 % (876416)Instruction limit reached!
% 70.29/10.87 % (876416)------------------------------
% 70.29/10.87 % (876416)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 70.29/10.87 % (876416)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 70.29/10.87 % (876416)CaDiCaL version: 2.1.3
% 70.29/10.87 % (876416)Termination reason: Instruction limit
% 70.29/10.87 % (876416)Termination phase: Saturation
% 70.29/10.87 % (876416)Time elapsed: 0.191 s
% 70.29/10.87 % (876416)Peak memory usage: 92 MB
% 70.29/10.87 % (876416)Instructions burned: 722 (million)
% 70.29/10.87 % (876418)lrs-20_1_to=lpo:sil=32000:tgt=ground:sp=reverse_frequency:spb=goal:urr=on:bsr=unit_only:nwc=1.5:random_seed=3276290344:i=598:bs=on:bd=preordered:av=off:ss=axioms_2964 on theBenchmark for (2964ds/598Mi)
% 70.29/10.87 % (876418)Instruction limit reached!
% 70.29/10.87 % (876418)------------------------------
% 70.29/10.87 % (876418)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 70.29/10.87 % (876418)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 70.29/10.87 % (876418)CaDiCaL version: 2.1.3
% 70.29/10.87 % (876418)Termination reason: Instruction limit
% 70.29/10.87 % (876418)Termination phase: Saturation
% 70.29/10.87 % (876418)Time elapsed: 0.157 s
% 70.29/10.87 % (876418)Peak memory usage: 90 MB
% 70.29/10.87 % (876418)Instructions burned: 599 (million)
% 70.29/10.87 % (876420)dis-1010_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=occurrence:random_seed=3652901484:i=2989:sd=3:ss=axioms:sgt=60_2961 on theBenchmark for (2961ds/2989Mi)
% 70.29/10.87 % (876238)Instruction limit reached!
% 70.29/10.87 % (876238)------------------------------
% 70.29/10.87 % (876238)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 70.29/10.87 % (876238)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 70.29/10.87 % (876238)CaDiCaL version: 2.1.3
% 70.29/10.87 % (876238)Termination reason: Instruction limit
% 70.29/10.87 % (876238)Termination phase: Saturation
% 70.29/10.87 % (876238)Time elapsed: 3.223 s
% 70.29/10.87 % (876238)Peak memory usage: 158 MB
% 70.29/10.87 % (876238)Instructions burned: 5209 (million)
% 70.29/10.87 % (876422)dis+1011_1_ncem=casc2026/models/loop5.pt:sil=8000:tgt=full:npcc=on:bsd=on:sp=const_min:spb=goal_then_units:lcm=predicate:urr=ec_only:s2agt=16:random_seed=69388192:i=1997:bd=preordered:av=off:gtg=all:gsp=on_2956 on theBenchmark for (2956ds/1997Mi)
% 70.29/10.87 % (876420)Instruction limit reached!
% 70.29/10.87 % (876420)------------------------------
% 70.29/10.87 % (876420)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 70.29/10.87 % (876420)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 96.11/14.55 % (876420)CaDiCaL version: 2.1.3
% 96.11/14.55 % (876420)Termination reason: Instruction limit
% 96.11/14.55 % (876420)Termination phase: Saturation
% 96.11/14.55 % (876420)Time elapsed: 0.974 s
% 96.11/14.55 % (876420)Peak memory usage: 144 MB
% 96.11/14.55 % (876420)Instructions burned: 2991 (million)
% 96.11/14.55 % (876424)lrs-1010_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:drc=off:sp=unary_frequency:urr=ec_only:fd=preordered:random_seed=1472346239:i=2088:bd=preordered:av=off_2950 on theBenchmark for (2950ds/2088Mi)
% 96.11/14.55 % (876422)Instruction limit reached!
% 96.11/14.55 % (876422)------------------------------
% 96.11/14.55 % (876422)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 96.11/14.55 % (876422)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 96.11/14.55 % (876422)CaDiCaL version: 2.1.3
% 96.11/14.55 % (876422)Termination reason: Instruction limit
% 96.11/14.55 % (876422)Termination phase: Saturation
% 96.11/14.55 % (876422)Time elapsed: 1.237 s
% 96.11/14.55 % (876422)Peak memory usage: 135 MB
% 96.11/14.55 % (876422)Instructions burned: 1997 (million)
% 96.11/14.55 % (876424)Instruction limit reached!
% 96.11/14.55 % (876424)------------------------------
% 96.11/14.55 % (876424)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 96.11/14.55 % (876424)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 96.11/14.55 % (876424)CaDiCaL version: 2.1.3
% 96.11/14.55 % (876424)Termination reason: Instruction limit
% 96.11/14.55 % (876424)Termination phase: Saturation
% 96.11/14.55 % (876424)Time elapsed: 0.698 s
% 96.11/14.55 % (876424)Peak memory usage: 136 MB
% 96.11/14.55 % (876424)Instructions burned: 2089 (million)
% 96.11/14.55 % (876426)lrs+1010_64:1_anc=all:to=lpo:sil=16000:fde=none:sp=const_frequency:urr=full:sac=on:random_seed=3425315496:i=1098:nicw=on_2942 on theBenchmark for (2942ds/1098Mi)
% 96.11/14.55 % (876427)lrs-1011_32:1_to=lpo:sil=32000:tgt=ground:sos=on:spb=goal_then_units:acc=on:random_seed=4044307290:i=433:bd=preordered_2942 on theBenchmark for (2942ds/433Mi)
% 96.11/14.55 % (876427)Instruction limit reached!
% 96.11/14.55 % (876427)------------------------------
% 96.11/14.55 % (876427)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 96.11/14.55 % (876427)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 96.11/14.55 % (876427)CaDiCaL version: 2.1.3
% 96.11/14.55 % (876427)Termination reason: Instruction limit
% 96.11/14.55 % (876427)Termination phase: Saturation
% 96.11/14.55 % (876427)Time elapsed: 0.144 s
% 96.11/14.55 % (876427)Peak memory usage: 93 MB
% 96.11/14.55 % (876427)Instructions burned: 436 (million)
% 96.11/14.55 % (876430)lrs+1002_1_ncem=casc2026/models/loop3.pt:sil=32000:npcc=on:prc=on:etr=on:spb=goal:flr=on:random_seed=2357957873:st=5.37:cond=on:i=2942:s2at=20:aac=none:fgj=on:bs=on:gtg=exists_sym:ss=axioms:er=filter:sgt=16_2939 on theBenchmark for (2939ds/2942Mi)
% 96.11/14.55 % (876426)Instruction limit reached!
% 96.11/14.55 % (876426)------------------------------
% 96.11/14.55 % (876426)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 96.11/14.55 % (876426)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 96.11/14.55 % (876426)CaDiCaL version: 2.1.3
% 96.11/14.55 % (876426)Termination reason: Instruction limit
% 96.11/14.55 % (876426)Termination phase: Saturation
% 96.11/14.55 % (876426)Time elapsed: 0.576 s
% 96.11/14.55 % (876426)Peak memory usage: 97 MB
% 96.11/14.55 % (876426)Instructions burned: 1100 (million)
% 96.11/14.55 % (876432)lrs+35_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=reverse_arity:urr=full:rp=on:br=off:random_seed=4033360969:i=6922:s2at=5:sd=3:bd=all:ss=axioms:er=known:sgt=32_2935 on theBenchmark for (2935ds/6922Mi)
% 96.11/14.55 % (876430)Instruction limit reached!
% 96.11/14.55 % (876430)------------------------------
% 96.11/14.55 % (876430)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 96.11/14.55 % (876430)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 96.11/14.55 % (876430)CaDiCaL version: 2.1.3
% 96.11/14.55 % (876430)Termination reason: Instruction limit
% 96.11/14.55 % (876430)Termination phase: Saturation
% 96.11/14.55 % (876430)Time elapsed: 1.025 s
% 96.11/14.55 % (876430)Peak memory usage: 138 MB
% 96.11/14.55 % (876430)Instructions burned: 2943 (million)
% 96.11/14.55 % (876434)dis+10_5:1_sil=8000:tgt=full:plsq=on:plsqc=1:plsqr=32,1:urr=on:fd=off:nwc=0.5:br=off:slsqc=3:slsq=on:random_seed=2676456230:s2a=on:i=596:s2at=2.3:gtgl=5:gtg=all:sup=off_2927 on theBenchmark for (2927ds/596Mi)
% 120.05/17.96 % (876434)Instruction limit reached!
% 120.05/17.96 % (876434)------------------------------
% 120.05/17.96 % (876434)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 120.05/17.96 % (876434)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 120.05/17.96 % (876434)CaDiCaL version: 2.1.3
% 120.05/17.96 % (876434)Termination reason: Instruction limit
% 120.05/17.96 % (876434)Termination phase: Saturation
% 120.05/17.96 % (876434)Time elapsed: 0.165 s
% 120.05/17.96 % (876434)Peak memory usage: 91 MB
% 120.05/17.96 % (876434)Instructions burned: 600 (million)
% 120.05/17.96 % (876412)Instruction limit reached!
% 120.05/17.96 % (876412)------------------------------
% 120.05/17.96 % (876412)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 120.05/17.96 % (876412)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 120.05/17.96 % (876412)CaDiCaL version: 2.1.3
% 120.05/17.96 % (876412)Termination reason: Instruction limit
% 120.05/17.96 % (876412)Termination phase: Saturation
% 120.05/17.96 % (876412)Time elapsed: 4.459 s
% 120.05/17.96 % (876412)Peak memory usage: 177 MB
% 120.05/17.96 % (876412)Instructions burned: 8479 (million)
% 120.05/17.96 % (876436)lrs+21_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=non_intro:urr=on:fd=preordered:random_seed=938059062:i=4123:kws=inv_frequency:bd=preordered:av=off:er=known_2924 on theBenchmark for (2924ds/4123Mi)
% 120.05/17.96 % (876437)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=3859420013:i=16411:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2923 on theBenchmark for (2923ds/16411Mi)
% 120.05/17.96 % (876408)Instruction limit reached!
% 120.05/17.96 % (876408)------------------------------
% 120.05/17.96 % (876408)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 120.05/17.96 % (876408)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 120.05/17.96 % (876408)CaDiCaL version: 2.1.3
% 120.05/17.96 % (876408)Termination reason: Instruction limit
% 120.05/17.96 % (876408)Termination phase: Saturation
% 120.05/17.96 % (876408)Time elapsed: 6.205 s
% 120.05/17.96 % (876408)Peak memory usage: 158 MB
% 120.05/17.96 % (876408)Instructions burned: 10310 (million)
% 120.05/17.96 % (876436)Instruction limit reached!
% 120.05/17.96 % (876436)------------------------------
% 120.05/17.96 % (876436)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 120.05/17.96 % (876436)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 120.05/17.96 % (876436)CaDiCaL version: 2.1.3
% 120.05/17.96 % (876436)Termination reason: Instruction limit
% 120.05/17.96 % (876436)Termination phase: Saturation
% 120.05/17.96 % (876436)Time elapsed: 1.228 s
% 120.05/17.96 % (876436)Peak memory usage: 147 MB
% 120.05/17.96 % (876436)Instructions burned: 4124 (million)
% 120.05/17.96 % (876440)lrs+0_1_ncem=casc2026/models/loop1.pt:sil=8000:tgt=full:npcc=on:sp=reverse_frequency:gs=on:random_seed=3943752713:i=1670:kws=inv_precedence:bd=all:av=off:gtg=exists_all_2911 on theBenchmark for (2911ds/1670Mi)
% 120.05/17.96 % (876441)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:prc=on:drc=off:fde=unused:sp=reverse_frequency:updr=off:random_seed=1683661357:st=3:cond=fast:i=1722:sd=2:ss=included:fsd=on_2911 on theBenchmark for (2911ds/1722Mi)
% 120.05/17.96 % (876441)Instruction limit reached!
% 120.05/17.96 % (876441)------------------------------
% 120.05/17.96 % (876441)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 120.05/17.96 % (876441)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 120.05/17.96 % (876441)CaDiCaL version: 2.1.3
% 120.05/17.96 % (876441)Termination reason: Instruction limit
% 120.05/17.96 % (876441)Termination phase: Saturation
% 120.05/17.96 % (876441)Time elapsed: 0.584 s
% 120.05/17.96 % (876441)Peak memory usage: 132 MB
% 120.05/17.96 % (876441)Instructions burned: 1724 (million)
% 120.05/17.96 % (876444)ott-1004_1_anc=all_dependent:to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:tgt=full:npcc=on:sas=cadical:sp=const_frequency:acc=on:urr=ec_only:gs=on:s2agt=40:alpa=false:sac=on:random_seed=2385655463:cts=off:cond=on:i=9530:bs=on:fsd=on_2904 on theBenchmark for (2904ds/9530Mi)
% 120.05/17.96 % (876440)Instruction limit reached!
% 120.05/17.96 % (876440)------------------------------
% 120.05/17.96 % (876440)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 120.05/17.96 % (876440)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 120.05/17.96 % (876440)CaDiCaL version: 2.1.3
% 120.05/17.96 % (876440)Termination reason: Instruction limit
% 145.76/21.41 % (876440)Termination phase: Saturation
% 145.76/21.41 % (876440)Time elapsed: 1.008 s
% 145.76/21.41 % (876440)Peak memory usage: 133 MB
% 145.76/21.41 % (876440)Instructions burned: 1671 (million)
% 145.76/21.41 % (876446)lrs+10_1_ncem=casc2026/models/loop4.pt:sil=64000:npcc=on:sp=occurrence:random_seed=2843273458:st=2:i=4495:sd=10:ss=included_2900 on theBenchmark for (2900ds/4495Mi)
% 145.76/21.41 % (876432)Instruction limit reached!
% 145.76/21.41 % (876432)------------------------------
% 145.76/21.41 % (876432)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 145.76/21.41 % (876432)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 145.76/21.41 % (876432)CaDiCaL version: 2.1.3
% 145.76/21.41 % (876432)Termination reason: Instruction limit
% 145.76/21.41 % (876432)Termination phase: Saturation
% 145.76/21.41 % (876432)Time elapsed: 3.770 s
% 145.76/21.41 % (876432)Peak memory usage: 156 MB
% 145.76/21.41 % (876432)Instructions burned: 6922 (million)
% 145.76/21.41 % (876448)lrs+1002_1_sfv=off:ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=reverse_arity:spb=non_intro:s2agt=16:random_seed=2236629040:cond=fast:i=4920:s2at=1.9:kws=inv_frequency:av=off:er=filter_2895 on theBenchmark for (2895ds/4920Mi)
% 145.76/21.41 % (876444)Instruction limit reached!
% 145.76/21.41 % (876444)------------------------------
% 145.76/21.41 % (876444)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 145.76/21.41 % (876444)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 145.76/21.41 % (876444)CaDiCaL version: 2.1.3
% 145.76/21.41 % (876444)Termination reason: Instruction limit
% 145.76/21.41 % (876444)Termination phase: Saturation
% 145.76/21.41 % (876444)Time elapsed: 2.599 s
% 145.76/21.41 % (876444)Peak memory usage: 143 MB
% 145.76/21.41 % (876444)Instructions burned: 9533 (million)
% 145.76/21.41 % (876450)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:lcm=reverse:bce=on:bsr=unit_only:random_seed=2647679450:cts=off:cond=on:i=2083:s2at=-1:fgj=on:av=off_2876 on theBenchmark for (2876ds/2083Mi)
% 145.76/21.41 % (876446)Instruction limit reached!
% 145.76/21.41 % (876446)------------------------------
% 145.76/21.41 % (876446)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 145.76/21.41 % (876446)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 145.76/21.41 % (876446)CaDiCaL version: 2.1.3
% 145.76/21.41 % (876446)Termination reason: Instruction limit
% 145.76/21.41 % (876446)Termination phase: Saturation
% 145.76/21.41 % (876446)Time elapsed: 2.784 s
% 145.76/21.41 % (876446)Peak memory usage: 156 MB
% 145.76/21.41 % (876446)Instructions burned: 4496 (million)
% 145.76/21.41 % (876452)lrs+31_1_to=lpo:ncem=casc2026/models/loop2.pt:sil=16000:npcc=on:sp=weighted_frequency:sos=all:spb=units:lcm=predicate:bsr=on:gs=on:random_seed=3756144554:i=4629:av=off:gsp=on_2870 on theBenchmark for (2870ds/4629Mi)
% 145.76/21.41 % (876450)Instruction limit reached!
% 145.76/21.41 % (876450)------------------------------
% 145.76/21.41 % (876450)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 145.76/21.41 % (876450)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 145.76/21.41 % (876450)CaDiCaL version: 2.1.3
% 145.76/21.41 % (876450)Termination reason: Instruction limit
% 145.76/21.41 % (876450)Termination phase: Saturation
% 145.76/21.41 % (876450)Time elapsed: 0.704 s
% 145.76/21.41 % (876450)Peak memory usage: 134 MB
% 145.76/21.41 % (876450)Instructions burned: 2084 (million)
% 145.76/21.41 % (876455)dis+10_64_sil=16000:tgt=full:plsq=on:prc=on:drc=off:plsqc=2:plsqr=32,1:spb=goal:random_seed=3057915788:i=1258:av=off_2868 on theBenchmark for (2868ds/1258Mi)
% 145.76/21.41 % (876448)Instruction limit reached!
% 145.76/21.41 % (876448)------------------------------
% 145.76/21.41 % (876448)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 145.76/21.41 % (876448)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 145.76/21.41 % (876448)CaDiCaL version: 2.1.3
% 145.76/21.41 % (876448)Termination reason: Instruction limit
% 145.76/21.41 % (876448)Termination phase: Saturation
% 145.76/21.41 % (876448)Time elapsed: 2.747 s
% 145.76/21.41 % (876448)Peak memory usage: 145 MB
% 145.76/21.41 % (876448)Instructions burned: 4920 (million)
% 145.76/21.41 % (876474)ott+1_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:fdtod=off:random_seed=2231170174:i=7343:av=off:ss=included_2866 on theBenchmark for (2866ds/7343Mi)
% 145.76/21.41 % (876455)Instruction limit reached!
% 145.76/21.41 % (876455)------------------------------
% 145.76/21.41 % (876455)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 162.95/23.96 % (876455)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 162.95/23.96 % (876455)CaDiCaL version: 2.1.3
% 162.95/23.96 % (876455)Termination reason: Instruction limit
% 162.95/23.96 % (876455)Termination phase: Saturation
% 162.95/23.96 % (876455)Time elapsed: 0.375 s
% 162.95/23.96 % (876455)Peak memory usage: 97 MB
% 162.95/23.96 % (876455)Instructions burned: 1259 (million)
% 162.95/23.96 % (876608)lrs-1002_1_to=lpo:sil=16000:sp=reverse_arity:sos=on:random_seed=3667020249:i=1325:sd=2:ss=axioms:sgt=16_2863 on theBenchmark for (2863ds/1325Mi)
% 162.95/23.96 % (876608)Instruction limit reached!
% 162.95/23.96 % (876608)------------------------------
% 162.95/23.96 % (876608)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 162.95/23.96 % (876608)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 162.95/23.96 % (876608)CaDiCaL version: 2.1.3
% 162.95/23.96 % (876608)Termination reason: Instruction limit
% 162.95/23.96 % (876608)Termination phase: Saturation
% 162.95/23.96 % (876608)Time elapsed: 0.440 s
% 162.95/23.96 % (876608)Peak memory usage: 97 MB
% 162.95/23.96 % (876608)Instructions burned: 1325 (million)
% 162.95/23.96 % (876682)dis+1011_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:prc=on:sp=arity:lma=off:spb=intro:urr=ec_only:sac=on:random_seed=648855751:st=3.9:cond=fast:i=2646:s2at=1.8:sd=5:amm=off:gtg=position:ss=axioms:fsd=on_2857 on theBenchmark for (2857ds/2646Mi)
% 162.95/23.96 % (876682)Instruction limit reached!
% 162.95/23.96 % (876682)------------------------------
% 162.95/23.96 % (876682)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 162.95/23.96 % (876682)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 162.95/23.96 % (876682)CaDiCaL version: 2.1.3
% 162.95/23.96 % (876682)Termination reason: Instruction limit
% 162.95/23.96 % (876682)Termination phase: Saturation
% 162.95/23.96 % (876682)Time elapsed: 1.210 s
% 162.95/23.96 % (876682)Peak memory usage: 139 MB
% 162.95/23.96 % (876682)Instructions burned: 2649 (million)
% 162.95/23.96 % (876743)dis-1003_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:sp=arity:sos=on:urr=on:random_seed=3931233552:i=1489:sd=2:ep=R:ss=axioms_2844 on theBenchmark for (2844ds/1489Mi)
% 162.95/23.96 % (876452)Instruction limit reached!
% 162.95/23.96 % (876452)------------------------------
% 162.95/23.96 % (876452)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 162.95/23.96 % (876452)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 162.95/23.96 % (876452)CaDiCaL version: 2.1.3
% 162.95/23.96 % (876452)Termination reason: Instruction limit
% 162.95/23.96 % (876452)Termination phase: Saturation
% 162.95/23.96 % (876452)Time elapsed: 2.742 s
% 162.95/23.96 % (876452)Peak memory usage: 145 MB
% 162.95/23.96 % (876452)Instructions burned: 4630 (million)
% 162.95/23.96 % (876818)lrs+20_1_ncem=casc2026/models/loop3.pt:sil=32000:npcc=on:fde=unused:sp=occurrence:sos=on:lcm=predicate:urr=full:sac=on:random_seed=1499393599:i=1503_2841 on theBenchmark for (2841ds/1503Mi)
% 162.95/23.96 % (876743)Instruction limit reached!
% 162.95/23.96 % (876743)------------------------------
% 162.95/23.96 % (876743)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 162.95/23.96 % (876743)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 162.95/23.96 % (876743)CaDiCaL version: 2.1.3
% 162.95/23.96 % (876743)Termination reason: Instruction limit
% 162.95/23.96 % (876743)Termination phase: Saturation
% 162.95/23.96 % (876743)Time elapsed: 0.507 s
% 162.95/23.96 % (876743)Peak memory usage: 131 MB
% 162.95/23.96 % (876743)Instructions burned: 1491 (million)
% 162.95/23.96 % (876899)lrs+10_1_ncem=casc2026/models/loop3.pt:sil=16000:tgt=ground:npcc=on:random_seed=2163423901:i=13942:kws=frequency_2837 on theBenchmark for (2837ds/13942Mi)
% 162.95/23.96 % (876818)Instruction limit reached!
% 162.95/23.96 % (876818)------------------------------
% 162.95/23.96 % (876818)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 162.95/23.96 % (876818)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 162.95/23.96 % (876818)CaDiCaL version: 2.1.3
% 162.95/23.96 % (876818)Termination reason: Instruction limit
% 162.95/23.96 % (876818)Termination phase: Saturation
% 162.95/23.96 % (876818)Time elapsed: 0.902 s
% 162.95/23.96 % (876818)Peak memory usage: 131 MB
% 162.95/23.96 % (876818)Instructions burned: 1504 (million)
% 162.95/23.96 % (876901)lrs-1002_1_to=lpo:ncem=casc2026/models/loop4.pt:sil=16000:npcc=on:bsd=on:sp=unary_frequency:spb=goal:lcm=predicate:acc=on:urr=full:bce=on:bsr=unit_only:s2agt=64:sac=on:random_seed=3535461902:i=3604:fsr=off:er=filter_2830 on theBenchmark for (2830ds/3604Mi)
% 186.37/27.18 % (876474)Instruction limit reached!
% 186.37/27.18 % (876474)------------------------------
% 186.37/27.18 % (876474)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 186.37/27.18 % (876474)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 186.37/27.18 % (876474)CaDiCaL version: 2.1.3
% 186.37/27.18 % (876474)Termination reason: Instruction limit
% 186.37/27.18 % (876474)Termination phase: Saturation
% 186.37/27.18 % (876474)Time elapsed: 4.580 s
% 186.37/27.18 % (876474)Peak memory usage: 183 MB
% 186.37/27.18 % (876474)Instructions burned: 7344 (million)
% 186.37/27.18 % (876437)Instruction limit reached!
% 186.37/27.18 % (876437)------------------------------
% 186.37/27.18 % (876437)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 186.37/27.18 % (876437)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 186.37/27.18 % (876437)CaDiCaL version: 2.1.3
% 186.37/27.18 % (876437)Termination reason: Instruction limit
% 186.37/27.18 % (876437)Termination phase: Saturation
% 186.37/27.18 % (876437)Time elapsed: 10.293 s
% 186.37/27.18 % (876437)Peak memory usage: 235 MB
% 186.37/27.18 % (876437)Instructions burned: 16412 (million)
% 186.37/27.18 % (876903)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=32000:npcc=on:random_seed=3977238769:i=1876:sd=1:ss=included:sgt=32_2819 on theBenchmark for (2819ds/1876Mi)
% 186.37/27.18 % (876904)lrs+10_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:fde=none:sp=arity:urr=on:br=off:random_seed=859317419:i=1932:bd=preordered:ins=10:sup=off:ss=axioms_2819 on theBenchmark for (2819ds/1932Mi)
% 186.37/27.18 % (876901)Instruction limit reached!
% 186.37/27.18 % (876901)------------------------------
% 186.37/27.18 % (876901)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 186.37/27.18 % (876901)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 186.37/27.18 % (876901)CaDiCaL version: 2.1.3
% 186.37/27.18 % (876901)Termination reason: Instruction limit
% 186.37/27.18 % (876901)Termination phase: Saturation
% 186.37/27.18 % (876901)Time elapsed: 2.052 s
% 186.37/27.18 % (876901)Peak memory usage: 142 MB
% 186.37/27.18 % (876901)Instructions burned: 3606 (million)
% 186.37/27.18 % (876907)dis-1010_1_ncem=casc2026/models/loop1.pt:sil=8000:npcc=on:fde=unused:etr=on:sp=weighted_frequency:spb=goal_then_units:urr=ec_only:fd=preordered:kmz=on:random_seed=3855420494:s2pl=on:cond=fast:i=1980:s2at=2:kws=inv_precedence:doe=on:ins=1:av=off:gsp=on_2808 on theBenchmark for (2808ds/1980Mi)
% 186.37/27.18 % (876904)Instruction limit reached!
% 186.37/27.18 % (876904)------------------------------
% 186.37/27.18 % (876904)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 186.37/27.18 % (876904)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 186.37/27.18 % (876904)CaDiCaL version: 2.1.3
% 186.37/27.18 % (876904)Termination reason: Instruction limit
% 186.37/27.18 % (876904)Termination phase: Saturation
% 186.37/27.18 % (876904)Time elapsed: 1.126 s
% 186.37/27.18 % (876904)Peak memory usage: 134 MB
% 186.37/27.18 % (876904)Instructions burned: 1932 (million)
% 186.37/27.18 % (876903)Instruction limit reached!
% 186.37/27.18 % (876903)------------------------------
% 186.37/27.18 % (876903)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 186.37/27.18 % (876903)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 186.37/27.18 % (876903)CaDiCaL version: 2.1.3
% 186.37/27.18 % (876903)Termination reason: Instruction limit
% 186.37/27.18 % (876903)Termination phase: Saturation
% 186.37/27.18 % (876903)Time elapsed: 1.168 s
% 186.37/27.18 % (876903)Peak memory usage: 136 MB
% 186.37/27.18 % (876903)Instructions burned: 1876 (million)
% 186.37/27.18 % (876910)dis+10_32_sil=16000:tgt=ground:drc=off:sas=cadical:acc=on:alpa=false:avsqc=3:random_seed=2863954841:avsq=on:i=3916:aac=none:amm=off_2806 on theBenchmark for (2806ds/3916Mi)
% 186.37/27.18 % (876909)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=unary_first:sos=all:spb=units:urr=on:br=off:random_seed=928748983:i=3902:kws=inv_arity_squared:fgj=on:ss=axioms:sgt=11_2806 on theBenchmark for (2806ds/3902Mi)
% 186.37/27.18 % (876907)Instruction limit reached!
% 186.37/27.18 % (876907)------------------------------
% 186.37/27.18 % (876907)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 186.37/27.18 % (876907)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 186.37/27.18 % (876907)CaDiCaL version: 2.1.3
% 186.37/27.18 % (876907)Termination reason: Instruction limit
% 233.03/33.75 % (876907)Termination phase: Saturation
% 233.03/33.75 % (876907)Time elapsed: 1.239 s
% 233.03/33.75 % (876907)Peak memory usage: 136 MB
% 233.03/33.75 % (876907)Instructions burned: 1980 (million)
% 233.03/33.75 % (876913)dis+10_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=full:npcc=on:drc=ordering:lcm=predicate:random_seed=64495791:cond=on:i=3940:av=off:er=known_2794 on theBenchmark for (2794ds/3940Mi)
% 233.03/33.75 % (876899)Instruction limit reached!
% 233.03/33.75 % (876899)------------------------------
% 233.03/33.75 % (876899)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 233.03/33.75 % (876899)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 233.03/33.75 % (876899)CaDiCaL version: 2.1.3
% 233.03/33.75 % (876899)Termination reason: Instruction limit
% 233.03/33.75 % (876899)Termination phase: Saturation
% 233.03/33.75 % (876899)Time elapsed: 4.704 s
% 233.03/33.75 % (876899)Peak memory usage: 219 MB
% 233.03/33.75 % (876899)Instructions burned: 13945 (million)
% 233.03/33.75 % (876915)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=reverse_frequency:bce=on:random_seed=1969913192:s2pl=on:i=3980:gtgl=3:kws=precedence:fgj=on:gtg=all_2789 on theBenchmark for (2789ds/3980Mi)
% 233.03/33.75 % (876909)Instruction limit reached!
% 233.03/33.75 % (876909)------------------------------
% 233.03/33.75 % (876909)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 233.03/33.75 % (876909)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 233.03/33.75 % (876909)CaDiCaL version: 2.1.3
% 233.03/33.75 % (876909)Termination reason: Instruction limit
% 233.03/33.75 % (876909)Termination phase: Saturation
% 233.03/33.75 % (876909)Time elapsed: 2.122 s
% 233.03/33.75 % (876909)Peak memory usage: 141 MB
% 233.03/33.75 % (876909)Instructions burned: 3903 (million)
% 233.03/33.75 % (876917)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:prc=on:sp=reverse_frequency:spb=units:lsd=20:urr=ec_only:bce=on:fd=off:kmz=on:random_seed=2810011888:i=2087:s2at=3:kws=frequency:av=off:fsr=off_2783 on theBenchmark for (2783ds/2087Mi)
% 233.03/33.75 % (876910)Instruction limit reached!
% 233.03/33.75 % (876910)------------------------------
% 233.03/33.75 % (876910)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 233.03/33.75 % (876910)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 233.03/33.75 % (876910)CaDiCaL version: 2.1.3
% 233.03/33.75 % (876910)Termination reason: Instruction limit
% 233.03/33.75 % (876910)Termination phase: Saturation
% 233.03/33.75 % (876910)Time elapsed: 2.408 s
% 233.03/33.75 % (876910)Peak memory usage: 113 MB
% 233.03/33.75 % (876910)Instructions burned: 3918 (million)
% 233.03/33.75 % (876919)ott-1004_1_anc=all_dependent:to=lpo:ncem=casc2026/models/loop5.pt:sil=8000:tgt=full:npcc=on:sas=cadical:sp=const_frequency:acc=on:urr=ec_only:gs=on:s2agt=40:alpa=false:sac=on:random_seed=3658557765:cts=off:cond=on:i=4272:bs=on:fsd=on_2780 on theBenchmark for (2780ds/4272Mi)
% 233.03/33.75 % (876915)Instruction limit reached!
% 233.03/33.75 % (876915)------------------------------
% 233.03/33.75 % (876915)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 233.03/33.75 % (876915)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 233.03/33.75 % (876915)CaDiCaL version: 2.1.3
% 233.03/33.75 % (876915)Termination reason: Instruction limit
% 233.03/33.75 % (876915)Termination phase: Saturation
% 233.03/33.75 % (876915)Time elapsed: 1.325 s
% 233.03/33.75 % (876915)Peak memory usage: 153 MB
% 233.03/33.75 % (876915)Instructions burned: 3982 (million)
% 233.03/33.75 % (876921)lrs-30_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:urr=on:bce=on:rp=on:br=off:flr=on:random_seed=1310848858:st=-1:i=2197:kws=precedence:av=off:ss=axioms:er=known_2775 on theBenchmark for (2775ds/2197Mi)
% 233.03/33.75 % (876913)Instruction limit reached!
% 233.03/33.75 % (876913)------------------------------
% 233.03/33.75 % (876913)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 233.03/33.75 % (876913)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 233.03/33.75 % (876913)CaDiCaL version: 2.1.3
% 233.03/33.75 % (876913)Termination reason: Instruction limit
% 233.03/33.75 % (876913)Termination phase: Saturation
% 233.03/33.75 % (876913)Time elapsed: 2.278 s
% 233.03/33.75 % (876913)Peak memory usage: 146 MB
% 233.03/33.75 % (876913)Instructions burned: 3941 (million)
% 233.03/33.75 % (876917)Instruction limit reached!
% 233.03/33.75 % (876917)------------------------------
% 233.03/33.75 % (876917)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 233.03/33.75 % (876917)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 146.95/37.05 % (876917)CaDiCaL version: 2.1.3
% 146.95/37.05 % (876917)Termination reason: Instruction limit
% 146.95/37.05 % (876917)Termination phase: Saturation
% 146.95/37.05 % (876917)Time elapsed: 1.266 s
% 146.95/37.05 % (876917)Peak memory usage: 137 MB
% 146.95/37.05 % (876917)Instructions burned: 2087 (million)
% 146.95/37.05 % (876923)dis+21_1_sil=8000:spb=goal_then_units:random_seed=1089718967:avsq=on:i=6508:avsqr=1,16:kws=arity_squared:fgj=on_2769 on theBenchmark for (2769ds/6508Mi)
% 146.95/37.05 % (876924)dis-1002_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=occurrence:random_seed=4081347059:i=2330:fgj=on:av=off:fsr=off_2769 on theBenchmark for (2769ds/2330Mi)
% 146.95/37.05 % (876919)Instruction limit reached!
% 146.95/37.05 % (876919)------------------------------
% 146.95/37.05 % (876919)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 146.95/37.05 % (876919)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 146.95/37.05 % (876919)CaDiCaL version: 2.1.3
% 146.95/37.05 % (876919)Termination reason: Instruction limit
% 146.95/37.05 % (876919)Termination phase: Saturation
% 146.95/37.05 % (876919)Time elapsed: 1.586 s
% 146.95/37.05 % (876919)Peak memory usage: 141 MB
% 146.95/37.05 % (876919)Instructions burned: 4277 (million)
% 146.95/37.05 % (876927)dis+10_2_anc=none:sil=64000:bsr=on:rp=on:alpa=true:avsqc=1:random_seed=1237302629:avsq=on:i=7592:avsqr=1,16:bs=on:gsp=on_2763 on theBenchmark for (2763ds/7592Mi)
% 146.95/37.05 % (876921)Instruction limit reached!
% 146.95/37.05 % (876921)------------------------------
% 146.95/37.05 % (876921)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 146.95/37.05 % (876921)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 146.95/37.05 % (876921)CaDiCaL version: 2.1.3
% 146.95/37.05 % (876921)Termination reason: Instruction limit
% 146.95/37.05 % (876921)Termination phase: Saturation
% 146.95/37.05 % (876921)Time elapsed: 1.241 s
% 146.95/37.05 % (876921)Peak memory usage: 135 MB
% 146.95/37.05 % (876921)Instructions burned: 2197 (million)
% 146.95/37.05 % (876929)lrs-1002_1_ncem=casc2026/models/loop6.pt:sil=64000:tgt=ground:npcc=on:prc=on:sims=off:sp=reverse_frequency:spb=goal_then_units:bce=on:bsr=unit_only:gs=on:flr=on:random_seed=3790533201:i=2693:kws=precedence:ins=1:av=off_2761 on theBenchmark for (2761ds/2693Mi)
% 146.95/37.05 % (876924)Instruction limit reached!
% 146.95/37.05 % (876924)------------------------------
% 146.95/37.05 % (876924)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 146.95/37.05 % (876924)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 146.95/37.05 % (876924)CaDiCaL version: 2.1.3
% 146.95/37.05 % (876924)Termination reason: Instruction limit
% 146.95/37.05 % (876924)Termination phase: Saturation
% 146.95/37.05 % (876924)Time elapsed: 1.380 s
% 146.95/37.05 % (876924)Peak memory usage: 138 MB
% 146.95/37.05 % (876924)Instructions burned: 2330 (million)
% 146.95/37.05 % (876931)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:random_seed=2072491275:i=28651:sd=4:ss=included:sgt=64_2753 on theBenchmark for (2753ds/28651Mi)
% 146.95/37.05 % (876929)Instruction limit reached!
% 146.95/37.05 % (876929)------------------------------
% 146.95/37.05 % (876929)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 146.95/37.05 % (876929)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 146.95/37.05 % (876929)CaDiCaL version: 2.1.3
% 146.95/37.05 % (876929)Termination reason: Instruction limit
% 146.95/37.05 % (876929)Termination phase: Saturation
% 146.95/37.05 % (876929)Time elapsed: 1.679 s
% 146.95/37.05 % (876929)Peak memory usage: 140 MB
% 146.95/37.05 % (876929)Instructions burned: 2693 (million)
% 146.95/37.05 % (876933)lrs-1010_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:sp=unary_frequency:random_seed=1986516461:i=2700:kws=precedence:fgj=on:bd=preordered:ins=1_2742 on theBenchmark for (2742ds/2700Mi)
% 146.95/37.05 % (876927)Instruction limit reached!
% 146.95/37.05 % (876927)------------------------------
% 146.95/37.05 % (876927)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 146.95/37.05 % (876927)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 146.95/37.05 % (876927)CaDiCaL version: 2.1.3
% 146.95/37.05 % (876927)Termination reason: Instruction limit
% 146.95/37.05 % (876927)Termination phase: Saturation
% 146.95/37.05 % (876927)Time elapsed: 2.348 s
% 146.95/37.05 % (876927)Peak memory usage: 114 MB
% 146.95/37.05 % (876927)Instructions burned: 7595 (million)
% 146.95/37.05 % (876935)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_min:sos=on:erd=off:spb=goal:lsd=20:urr=full:sac=on:random_seed=3270055687:i=3196:nm=4_2738 on theBenchmark for (2738ds/3196Mi)
% 146.95/37.05 % (876923)Instruction limit reached!
% 146.95/37.05 % (876923)------------------------------
% 146.95/37.05 % (876923)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 146.95/37.05 % (876923)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 146.95/37.05 % (876923)CaDiCaL version: 2.1.3
% 146.95/37.05 % (876923)Termination reason: Instruction limit
% 146.95/37.05 % (876923)Termination phase: Saturation
% 146.95/37.05 % (876923)Time elapsed: 3.854 s
% 146.95/37.05 % (876923)Peak memory usage: 120 MB
% 146.95/37.05 % (876923)Instructions burned: 6509 (million)
% 146.95/37.05 % (876937)ott+11_1_ncem=casc2026/models/loop4.pt:sil=64000:tgt=full:irw=on:npcc=on:spb=units:flr=on:random_seed=4139966944:cts=off:i=3254:av=off_2729 on theBenchmark for (2729ds/3254Mi)
% 146.95/37.05 % (876935)Instruction limit reached!
% 146.95/37.05 % (876935)------------------------------
% 146.95/37.05 % (876935)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 146.95/37.05 % (876935)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 146.95/37.05 % (876935)CaDiCaL version: 2.1.3
% 146.95/37.05 % (876935)Termination reason: Instruction limit
% 146.95/37.05 % (876935)Termination phase: Saturation
% 146.95/37.05 % (876935)Time elapsed: 0.963 s
% 146.95/37.05 % (876935)Peak memory usage: 144 MB
% 146.95/37.05 % (876935)Instructions burned: 3199 (million)
% 146.95/37.05 % (876939)dis+1011_1_sfv=off:ncem=casc2026/models/loop2.pt:sil=32000:tgt=ground:npcc=on:lcm=predicate:bce=on:sac=on:random_seed=4211081681:i=3264:bd=all:gtg=exists_sym:ss=included:er=known_2727 on theBenchmark for (2727ds/3264Mi)
% 146.95/37.05 % (876933)Instruction limit reached!
% 146.95/37.05 % (876933)------------------------------
% 146.95/37.05 % (876933)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 146.95/37.05 % (876933)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 146.95/37.05 % (876933)CaDiCaL version: 2.1.3
% 146.95/37.05 % (876933)Termination reason: Instruction limit
% 146.95/37.05 % (876933)Termination phase: Saturation
% 146.95/37.05 % (876933)Time elapsed: 1.595 s
% 146.95/37.05 % (876933)Peak memory usage: 136 MB
% 146.95/37.05 % (876933)Instructions burned: 2700 (million)
% 146.95/37.05 % (876941)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:sp=unary_first:sos=on:lma=off:lsd=20:urr=on:kmz=on:sac=on:random_seed=2779174674:st=6:i=9708:kws=inv_frequency:doe=on:fgj=on:ss=axioms_2725 on theBenchmark for (2725ds/9708Mi)
% 146.95/37.05 % (876937)Instruction limit reached!
% 146.95/37.05 % (876937)------------------------------
% 146.95/37.05 % (876937)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 146.95/37.05 % (876937)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 146.95/37.05 % (876937)CaDiCaL version: 2.1.3
% 146.95/37.05 % (876937)Termination reason: Instruction limit
% 146.95/37.05 % (876937)Termination phase: Saturation
% 146.95/37.05 % (876937)Time elapsed: 1.248 s
% 146.95/37.05 % (876937)Peak memory usage: 139 MB
% 146.95/37.05 % (876937)Instructions burned: 3255 (million)
% 146.95/37.05 % (876969)lrs+1010_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=full:npcc=on:erd=off:spb=goal:sac=on:newcnf=on:random_seed=756007106:i=21997:s2at=5:gtg=all_2715 on theBenchmark for (2715ds/21997Mi)
% 146.95/37.05 % (876939)Instruction limit reached!
% 146.95/37.05 % (876939)------------------------------
% 146.95/37.05 % (876939)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 146.95/37.05 % (876939)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 146.95/37.05 % (876939)CaDiCaL version: 2.1.3
% 146.95/37.05 % (876939)Termination reason: Instruction limit
% 146.95/37.05 % (876939)Termination phase: Saturation
% 146.95/37.05 % (876939)Time elapsed: 1.844 s
% 146.95/37.05 % (876939)Peak memory usage: 145 MB
% 146.95/37.05 % (876939)Instructions burned: 3264 (million)
% 146.95/37.05 % (877118)dis+10_14_to=lpo:sil=8000:tgt=full:drc=off:sp=const_frequency:sos=all:random_seed=4007264108:i=7551:gtgl=5:bs=unit_only:fsr=off:gtg=exists_all_2707 on theBenchmark for (2707ds/7551Mi)
% 146.95/37.05 % (876941)Instruction limit reached!
% 146.95/37.05 % (876941)------------------------------
% 146.95/37.05 % (876941)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 146.95/37.05 % (876941)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 146.95/37.05 % (876941)CaDiCaL version: 2.1.3
% 146.95/37.05 % (876941)Termination reason: Instruction limit
% 146.95/37.05 % (876941)Termination phase: Saturation
% 146.95/37.05 % (876941)Time elapsed: 5.221 s
% 146.95/37.05 % (876941)Peak memory usage: 167 MB
% 146.95/37.05 % (876941)Instructions burned: 9708 (million)
% 146.95/37.05 % (877274)lrs+1011_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=1742397627:i=8924:sd=1:ss=included_2671 on theBenchmark for (2671ds/8924Mi)
% 146.95/37.05 % (877118)Instruction limit reached!
% 146.95/37.05 % (877118)------------------------------
% 146.95/37.05 % (877118)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 146.95/37.05 % (877118)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 146.95/37.05 % (877118)CaDiCaL version: 2.1.3
% 146.95/37.05 % (877118)Termination reason: Instruction limit
% 146.95/37.05 % (877118)Termination phase: Saturation
% 146.95/37.05 % (877118)Time elapsed: 4.171 s
% 146.95/37.05 % (877118)Peak memory usage: 134 MB
% 146.95/37.05 % (877118)Instructions burned: 7551 (million)
% 146.95/37.05 % (877276)lrs+1011_1_ncem=casc2026/models/loop2.pt:sil=16000:npcc=on:sp=arity:fd=preordered:random_seed=2220247577:i=9638:kws=frequency:bd=preordered_2663 on theBenchmark for (2663ds/9638Mi)
% 146.95/37.05 % (877274)First to succeed.
% 146.95/37.05 % (877274)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-876056"
% 146.95/37.05 % (877274)Refutation found. Thanks to Tanya!
% 146.95/37.05 % SZS status Unsatisfiable for theBenchmark
% 146.95/37.05 % SZS output start Proof for theBenchmark
% See solution above
% 0.17/37.14 % (877274)------------------------------
% 0.17/37.14 % (877274)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.17/37.14 % (877274)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.17/37.14 % (877274)CaDiCaL version: 2.1.3
% 0.17/37.14 % (877274)Termination reason: Refutation
% 0.17/37.14 % (877274)Time elapsed: 2.818 s
% 0.17/37.14 % (877274)Peak memory usage: 156 MB
% 0.17/37.14 % (877274)Instructions burned: 4911 (million)
% 0.17/37.14 % (877274)------------------------------
% 0.17/37.14 % (877274)------------------------------
% 0.17/37.14 % (876056)Success in time 36.17 s
% 0.17/37.14 % Vampire exiting
%------------------------------------------------------------------------------