%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : CSR246+1 : TPTP v9.3.1. Released v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n014.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:44:11 AM UTC 2026
% Result : Theorem 82.78s 17.33s
% Output : Refutation 117.22s
% Verified :
% SZS Type : Refutation
% Derivation depth : 23
% Number of leaves : 15
% Syntax : Number of formulae : 76 ( 23 unt; 2 def)
% Number of atoms : 177 ( 0 equ)
% Maximal formula atoms : 6 ( 2 avg)
% Number of connectives : 199 ( 98 ~; 79 |; 15 &)
% ( 3 <=>; 4 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 4 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 6 ( 5 usr; 3 prp; 0-2 aty)
% Number of functors : 12 ( 12 usr; 10 con; 0-1 aty)
% Number of variables : 79 ( 0 sgn 70 !; 9 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f2,axiom,
! [X0,X1,X2] :
( ( p__d__subclass(X0,X1)
& p__d__subclass(X1,X2) )
=> p__d__subclass(X0,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',predefinitionsA8) ).
fof(f4,axiom,
! [X0,X1,X2] :
( ( p__d__instance(X0,X1)
& p__d__subclass(X1,X2) )
=> p__d__instance(X0,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',predefinitionsA12) ).
fof(f110,axiom,
! [X0] :
( p__d__subclass(X0,c__Entity)
=> ? [X1] : p__d__instance(X1,X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mergeA176) ).
fof(f112,axiom,
p__d__subclass(c__Physical,c__Entity),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mergeA178) ).
fof(f115,axiom,
p__d__subclass(c__Object,c__Physical),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mergeA181) ).
fof(f2051,axiom,
p__d__subclass(c__LandTransitway,c__LandArea),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mergeA2890) ).
fof(f2267,axiom,
p__d__subclass(c__Artifact,c__Object),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mergeA3134) ).
fof(f2268,axiom,
! [X0] :
( p__d__instance(X0,c__Artifact)
<=> ? [X1] :
( p__d__instance(X1,c__Making)
& p__result(X1,X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mergeA3135) ).
fof(f2275,axiom,
p__d__subclass(c__StationaryArtifact,c__Artifact),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mergeA3144) ).
fof(f5871,axiom,
p__d__subclass(c__RunningTrack,c__StationaryArtifact),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',miloA4060) ).
fof(f5872,axiom,
p__d__subclass(c__RunningTrack,c__LandTransitway),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',miloA4061) ).
fof(f7290,axiom,
! [X0,X1] :
( p__result(X0,X1)
=> p__d__instance(X0,c__Process) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',typeA437) ).
fof(f7433,conjecture,
? [X0,X1] :
( p__d__instance(X0,c__Process)
& p__d__instance(X0,c__Process)
& p__d__instance(X1,c__LandArea)
& p__result(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',resultRelation0043) ).
fof(f7434,negated_conjecture,
~ ? [X0,X1] :
( p__d__instance(X0,c__Process)
& p__d__instance(X0,c__Process)
& p__d__instance(X1,c__LandArea)
& p__result(X0,X1) ),
inference(negated_conjecture,[status(cth)],[f7433]) ).
fof(f7516,plain,
! [X0,X1] :
( ~ p__d__instance(X0,c__Process)
| ~ p__d__instance(X0,c__Process)
| ~ p__d__instance(X1,c__LandArea)
| ~ p__result(X0,X1) ),
inference(ennf_transformation,[],[f7434]) ).
fof(f7517,plain,
! [X0,X1,X2] :
( p__d__instance(X0,X2)
| ~ p__d__instance(X0,X1)
| ~ p__d__subclass(X1,X2) ),
inference(ennf_transformation,[],[f4]) ).
fof(f7518,plain,
! [X0,X1,X2] :
( p__d__instance(X0,X2)
| ~ p__d__instance(X0,X1)
| ~ p__d__subclass(X1,X2) ),
inference(flattening,[],[f7517]) ).
fof(f7519,plain,
! [X0,X1] :
( p__d__instance(X0,c__Process)
| ~ p__result(X0,X1) ),
inference(ennf_transformation,[],[f7290]) ).
fof(f7543,plain,
! [X0,X1,X2] :
( p__d__subclass(X0,X2)
| ~ p__d__subclass(X0,X1)
| ~ p__d__subclass(X1,X2) ),
inference(ennf_transformation,[],[f2]) ).
fof(f7544,plain,
! [X0,X1,X2] :
( p__d__subclass(X0,X2)
| ~ p__d__subclass(X0,X1)
| ~ p__d__subclass(X1,X2) ),
inference(flattening,[],[f7543]) ).
fof(f7952,plain,
! [X0] :
( ? [X1] : p__d__instance(X1,X0)
| ~ p__d__subclass(X0,c__Entity) ),
inference(ennf_transformation,[],[f110]) ).
fof(f8289,plain,
! [X0] :
( ( p__d__instance(X0,c__Artifact)
| ! [X1] :
( ~ p__d__instance(X1,c__Making)
| ~ p__result(X1,X0) ) )
& ( ? [X1] :
( p__d__instance(X1,c__Making)
& p__result(X1,X0) )
| ~ p__d__instance(X0,c__Artifact) ) ),
inference(nnf_transformation,[],[f2268]) ).
fof(f8290,plain,
! [X0] :
( ( p__d__instance(X0,c__Artifact)
| ! [X1] :
( ~ p__d__instance(X1,c__Making)
| ~ p__result(X1,X0) ) )
& ( ? [X2] :
( p__d__instance(X2,c__Making)
& p__result(X2,X0) )
| ~ p__d__instance(X0,c__Artifact) ) ),
inference(rectify,[],[f8289]) ).
fof(f8291,plain,
! [X0] :
( ( p__d__instance(X0,c__Artifact)
| ! [X1] :
( ~ p__d__instance(X1,c__Making)
| ~ p__result(X1,X0) ) )
& ( ( p__d__instance(sK157(X0),c__Making)
& p__result(sK157(X0),X0) )
| ~ p__d__instance(X0,c__Artifact) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK157]),skolemize(X2,sK157(X0))],[f8290]) ).
fof(f8324,plain,
! [X0] :
( p__d__instance(sK189(X0),X0)
| ~ p__d__subclass(X0,c__Entity) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK189]),skolemize(X1,sK189(X0))],[f7952]) ).
fof(f8412,plain,
! [X0,X1] :
( ~ p__d__instance(X0,c__Process)
| ~ p__d__instance(X0,c__Process)
| ~ p__d__instance(X1,c__LandArea)
| ~ p__result(X0,X1) ),
inference(cnf_transformation,[],[f7516]) ).
fof(f8413,plain,
! [X2,X0,X1] :
( p__d__instance(X0,X2)
| ~ p__d__instance(X0,X1)
| ~ p__d__subclass(X1,X2) ),
inference(cnf_transformation,[],[f7518]) ).
fof(f8414,plain,
! [X0,X1] :
( ~ p__result(X0,X1)
| p__d__instance(X0,c__Process) ),
inference(cnf_transformation,[],[f7519]) ).
fof(f8447,plain,
p__d__subclass(c__LandTransitway,c__LandArea),
inference(cnf_transformation,[],[f2051]) ).
fof(f8455,plain,
! [X2,X0,X1] :
( p__d__subclass(X0,X2)
| ~ p__d__subclass(X0,X1)
| ~ p__d__subclass(X1,X2) ),
inference(cnf_transformation,[],[f7544]) ).
fof(f8461,plain,
p__d__subclass(c__Object,c__Physical),
inference(cnf_transformation,[],[f115]) ).
fof(f8599,plain,
p__d__subclass(c__RunningTrack,c__LandTransitway),
inference(cnf_transformation,[],[f5872]) ).
fof(f9193,plain,
p__d__subclass(c__StationaryArtifact,c__Artifact),
inference(cnf_transformation,[],[f2275]) ).
fof(f9194,plain,
! [X0] :
( p__result(sK157(X0),X0)
| ~ p__d__instance(X0,c__Artifact) ),
inference(cnf_transformation,[],[f8291]) ).
fof(f9197,plain,
p__d__subclass(c__Artifact,c__Object),
inference(cnf_transformation,[],[f2267]) ).
fof(f9470,plain,
p__d__subclass(c__Physical,c__Entity),
inference(cnf_transformation,[],[f112]) ).
fof(f9473,plain,
! [X0] :
( p__d__instance(sK189(X0),X0)
| ~ p__d__subclass(X0,c__Entity) ),
inference(cnf_transformation,[],[f8324]) ).
fof(f9559,plain,
p__d__subclass(c__RunningTrack,c__StationaryArtifact),
inference(cnf_transformation,[],[f5871]) ).
fof(f9837,plain,
! [X0,X1] :
( ~ p__d__instance(X0,c__Process)
| ~ p__d__instance(X1,c__LandArea)
| ~ p__result(X0,X1) ),
inference(duplicate_literal_removal,[],[f8412]) ).
fof(f9838,plain,
! [X0,X1] :
( ~ p__result(X0,X1)
| ~ p__d__instance(X1,c__LandArea) ),
inference(forward_subsumption_resolution,[],[f9837,f8414]) ).
fof(f9849,plain,
! [X0] :
( ~ p__d__instance(X0,c__Artifact)
| ~ p__d__instance(X0,c__LandArea) ),
inference(resolution,[],[f9838,f9194]) ).
fof(f9858,plain,
! [X0,X1] :
( ~ p__d__instance(X0,c__LandArea)
| ~ p__d__instance(X0,X1)
| ~ p__d__subclass(X1,c__Artifact) ),
inference(resolution,[],[f9849,f8413]) ).
fof(f9862,definition,
( spl240_1
<=> p__d__subclass(c__Artifact,c__Entity) ),
introduced(definition,[new_symbols(definition,[spl240_1])],[avatar_definition]) ).
fof(f9863,plain,
( p__d__subclass(c__Artifact,c__Entity)
| ~ spl240_1 ),
inference(avatar_component_clause,[],[f9862]) ).
fof(f9864,plain,
( ~ p__d__subclass(c__Artifact,c__Entity)
| spl240_1 ),
inference(avatar_component_clause,[],[f9862]) ).
fof(f11831,plain,
! [X2,X0,X1] :
( ~ p__d__instance(X0,X2)
| ~ p__d__subclass(X1,c__Artifact)
| ~ p__d__instance(X0,X1)
| ~ p__d__subclass(X2,c__LandArea) ),
inference(resolution,[],[f9858,f8413]) ).
fof(f12058,plain,
! [X0,X1] :
( ~ p__d__instance(sK189(X1),X0)
| ~ p__d__subclass(X0,c__Artifact)
| ~ p__d__subclass(X1,c__LandArea)
| ~ p__d__subclass(X1,c__Entity) ),
inference(resolution,[],[f11831,f9473]) ).
fof(f12118,plain,
! [X0] :
( ~ p__d__subclass(X0,c__Artifact)
| ~ p__d__subclass(X0,c__LandArea)
| ~ p__d__subclass(X0,c__Entity)
| ~ p__d__subclass(X0,c__Entity) ),
inference(resolution,[],[f12058,f9473]) ).
fof(f12125,plain,
! [X0] :
( ~ p__d__subclass(X0,c__Artifact)
| ~ p__d__subclass(X0,c__LandArea)
| ~ p__d__subclass(X0,c__Entity) ),
inference(duplicate_literal_removal,[],[f12118]) ).
fof(f12158,plain,
! [X0,X1] :
( ~ p__d__subclass(X1,c__Artifact)
| ~ p__d__subclass(X0,c__Entity)
| ~ p__d__subclass(X0,X1)
| ~ p__d__subclass(X0,c__LandArea) ),
inference(resolution,[],[f12125,f8455]) ).
fof(f12178,definition,
( spl240_409
<=> p__d__subclass(c__StationaryArtifact,c__Entity) ),
introduced(definition,[new_symbols(definition,[spl240_409])],[avatar_definition]) ).
fof(f12180,plain,
( ~ p__d__subclass(c__StationaryArtifact,c__Entity)
| spl240_409 ),
inference(avatar_component_clause,[],[f12178]) ).
fof(f12196,plain,
! [X0] :
( ~ p__d__subclass(X0,c__LandArea)
| ~ p__d__subclass(X0,c__StationaryArtifact)
| ~ p__d__subclass(X0,c__Entity) ),
inference(resolution,[],[f12158,f9193]) ).
fof(f12257,plain,
! [X0,X1] :
( ~ p__d__subclass(X1,c__LandArea)
| ~ p__d__subclass(X0,c__Entity)
| ~ p__d__subclass(X0,X1)
| ~ p__d__subclass(X0,c__StationaryArtifact) ),
inference(resolution,[],[f12196,f8455]) ).
fof(f12552,plain,
! [X0] :
( ~ p__d__subclass(X0,c__LandTransitway)
| ~ p__d__subclass(X0,c__Entity)
| ~ p__d__subclass(X0,c__StationaryArtifact) ),
inference(resolution,[],[f12257,f8447]) ).
fof(f12559,plain,
( ~ p__d__subclass(c__RunningTrack,c__Entity)
| ~ p__d__subclass(c__RunningTrack,c__StationaryArtifact) ),
inference(resolution,[],[f12552,f8599]) ).
fof(f12572,plain,
~ p__d__subclass(c__RunningTrack,c__Entity),
inference(forward_subsumption_resolution,[],[f12559,f9559]) ).
fof(f12573,plain,
! [X0] :
( ~ p__d__subclass(c__RunningTrack,X0)
| ~ p__d__subclass(X0,c__Entity) ),
inference(resolution,[],[f12572,f8455]) ).
fof(f12576,plain,
~ p__d__subclass(c__StationaryArtifact,c__Entity),
inference(resolution,[],[f12573,f9559]) ).
fof(f12578,plain,
~ spl240_409,
inference(avatar_split_clause,[],[f12576,f12178]) ).
fof(f12579,plain,
( ! [X0] :
( ~ p__d__subclass(c__StationaryArtifact,X0)
| ~ p__d__subclass(X0,c__Entity) )
| spl240_409 ),
inference(resolution,[],[f12180,f8455]) ).
fof(f12582,plain,
( ~ p__d__subclass(c__Artifact,c__Entity)
| spl240_409 ),
inference(resolution,[],[f12579,f9193]) ).
fof(f14917,plain,
( ! [X0] :
( ~ p__d__subclass(c__Artifact,X0)
| ~ p__d__subclass(X0,c__Entity) )
| spl240_1 ),
inference(resolution,[],[f9864,f8455]) ).
fof(f14920,plain,
( ~ p__d__subclass(c__Object,c__Entity)
| spl240_1 ),
inference(resolution,[],[f14917,f9197]) ).
fof(f14921,plain,
( ! [X0] :
( ~ p__d__subclass(c__Object,X0)
| ~ p__d__subclass(X0,c__Entity) )
| spl240_1 ),
inference(resolution,[],[f14920,f8455]) ).
fof(f14924,plain,
( ~ p__d__subclass(c__Physical,c__Entity)
| spl240_1 ),
inference(resolution,[],[f14921,f8461]) ).
fof(f14925,plain,
( $false
| spl240_1 ),
inference(forward_subsumption_resolution,[],[f14924,f9470]) ).
fof(f14926,plain,
spl240_1,
inference(avatar_contradiction_clause,[],[f14925]) ).
fof(f14929,plain,
( $false
| ~ spl240_1
| spl240_409 ),
inference(forward_subsumption_resolution,[],[f12582,f9863]) ).
fof(f14930,plain,
( ~ spl240_1
| spl240_409 ),
inference(avatar_contradiction_clause,[],[f14929]) ).
cnf(s320,plain,
~ spl240_409,
inference(sat_conversion,[],[f12578]) ).
cnf(s594,plain,
spl240_1,
inference(sat_conversion,[],[f14926]) ).
cnf(s596,plain,
( ~ spl240_1
| spl240_409 ),
inference(sat_conversion,[],[f14930]) ).
cnf(s597,plain,
spl240_409,
inference(rat,[],[s596,s594]) ).
cnf(s599,plain,
$false,
inference(rat,[],[s320,s597]) ).
fof(f14931,plain,
$false,
inference(avatar_sat_refutation,[],[s599]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : CSR246+1 : TPTP v9.3.1. Released v7.3.0.
% 0.00/0.08 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.10/0.25 % Computer : n014.cluster.edu
% 0.10/0.25 % Model : x86_64 x86_64
% 0.10/0.25 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.25 % Memory : 8046.5625MB
% 0.10/0.25 % OS : Linux 6.8.0-71-generic
% 0.10/0.25 % CPULimit : 300
% 0.10/0.25 % WCLimit : 300
% 0.10/0.25 % DateTime : Mon Sep 28 23:52:59 UTC 2026
% 0.10/0.25 % CPUTime :
% 0.10/0.25 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.26/0.31 Running first-order theorem proving
% 0.26/0.31 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
% 9.77/2.23 % (2296644)Detected formulas, will run a generic FOF schedule.
% 9.77/2.23 % (2296657)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=762615753:i=141193_2998 on theBenchmark for (2998ds/141193Mi)
% 9.77/2.23 % (2296660)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=2822686423:i=141695:sd=1:nm=32:gsp=on:ss=included_2998 on theBenchmark for (2998ds/141695Mi)
% 9.77/2.23 % (2296658)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=470478872:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2998 on theBenchmark for (2998ds/134677Mi)
% 9.77/2.23 % (2296664)dis-21_1_sil=8000:lcm=predicate:random_seed=1142588448:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2998 on theBenchmark for (2998ds/129Mi)
% 9.77/2.23 % (2296661)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=1355392447:i=109:sd=1:ins=1:gsp=on:ss=axioms_2998 on theBenchmark for (2998ds/109Mi)
% 9.77/2.23 % (2296662)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2302934177:i=119:av=off:ss=axioms_2998 on theBenchmark for (2998ds/119Mi)
% 9.77/2.23 % (2296663)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3021140421:s2a=on:i=139:gtg=position_2998 on theBenchmark for (2998ds/139Mi)
% 9.77/2.23 % (2296661)Refutation not found, incomplete strategy
% 9.77/2.23 % (2296661)------------------------------
% 9.77/2.23 % (2296661)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.77/2.23 % (2296661)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.77/2.23 % (2296661)CaDiCaL version: 2.1.3
% 9.77/2.23 % (2296661)Termination reason: Refutation not found, incomplete strategy
% 9.77/2.23 % (2296661)Time elapsed: 0.023 s
% 9.77/2.23 % (2296661)Peak memory usage: 92 MB
% 9.77/2.23 % (2296661)Instructions burned: 23 (million)
% 9.77/2.23 % (2296662)Instruction limit reached!
% 9.77/2.23 % (2296662)------------------------------
% 9.77/2.23 % (2296662)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.77/2.23 % (2296662)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.77/2.23 % (2296662)CaDiCaL version: 2.1.3
% 9.77/2.23 % (2296662)Termination reason: Instruction limit
% 9.77/2.23 % (2296662)Termination phase: Saturation
% 9.77/2.23 % (2296662)Time elapsed: 0.107 s
% 9.77/2.23 % (2296662)Peak memory usage: 94 MB
% 9.77/2.23 % (2296662)Instructions burned: 119 (million)
% 9.77/2.23 % (2296664)Instruction limit reached!
% 9.77/2.23 % (2296664)------------------------------
% 9.77/2.23 % (2296664)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.77/2.23 % (2296664)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.77/2.23 % (2296664)CaDiCaL version: 2.1.3
% 9.77/2.23 % (2296664)Termination reason: Instruction limit
% 9.77/2.23 % (2296664)Termination phase: Saturation
% 9.77/2.23 % (2296664)Time elapsed: 0.123 s
% 9.77/2.23 % (2296664)Peak memory usage: 95 MB
% 9.77/2.23 % (2296664)Instructions burned: 130 (million)
% 9.77/2.23 % (2296663)Instruction limit reached!
% 9.77/2.23 % (2296663)------------------------------
% 9.77/2.23 % (2296663)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.77/2.23 % (2296663)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.77/2.23 % (2296663)CaDiCaL version: 2.1.3
% 9.77/2.23 % (2296663)Termination reason: Instruction limit
% 9.77/2.23 % (2296663)Termination phase: Preprocessing 3
% 9.77/2.23 % (2296663)Time elapsed: 0.147 s
% 9.77/2.23 % (2296663)Peak memory usage: 94 MB
% 9.77/2.23 % (2296663)Instructions burned: 140 (million)
% 9.77/2.23 [W928 23:53:00.780595686 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 9.77/2.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 9.77/2.23 [W928 23:53:00.780626624 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 9.77/2.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 9.77/2.23 [W928 23:53:00.780659249 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 11.24/2.56 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 11.24/2.56 [W928 23:53:00.780670173 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 11.24/2.56 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 11.24/2.56 [W928 23:53:00.780706605 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 11.24/2.56 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 11.24/2.56 [W928 23:53:00.780725059 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 11.24/2.56 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 11.24/2.56 [W928 23:53:00.780747828 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 11.24/2.56 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 11.24/2.56 [W928 23:53:00.780756619 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 11.24/2.56 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 11.24/2.56 [W928 23:53:00.780777665 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 11.24/2.56 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 11.24/2.56 [W928 23:53:00.780786563 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 11.24/2.56 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 11.24/2.56 [W928 23:53:00.780809739 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 11.24/2.56 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 11.24/2.56 [W928 23:53:00.780819888 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 11.24/2.56 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 11.24/2.56 % (2296673)lrs+10_1_sil=8000:sp=occurrence:random_seed=2225592968:i=285:sd=3:ss=axioms:sgt=8_2995 on theBenchmark for (2995ds/285Mi)
% 11.24/2.56 % (2296675)lrs+1011_1_sil=32000:sp=occurrence:random_seed=3026482115:i=325:sd=1:ss=axioms:sgt=32_2994 on theBenchmark for (2994ds/325Mi)
% 11.24/2.56 % (2296674)lrs+10_1_sil=32000:urr=on:br=off:random_seed=2645397298:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2995 on theBenchmark for (2995ds/157Mi)
% 11.24/2.56 % (2296673)Refutation not found, incomplete strategy
% 11.24/2.56 % (2296673)------------------------------
% 11.24/2.56 % (2296673)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.24/2.56 % (2296673)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.24/2.56 % (2296673)CaDiCaL version: 2.1.3
% 11.24/2.56 % (2296673)Termination reason: Refutation not found, incomplete strategy
% 11.24/2.56 % (2296673)Time elapsed: 0.024 s
% 11.24/2.56 % (2296673)Peak memory usage: 94 MB
% 11.24/2.56 % (2296673)Instructions burned: 20 (million)
% 11.24/2.56 % (2296675)Refutation not found, incomplete strategy
% 11.24/2.56 % (2296675)------------------------------
% 18.82/3.57 % (2296675)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.82/3.57 % (2296675)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.82/3.57 % (2296675)CaDiCaL version: 2.1.3
% 18.82/3.57 % (2296675)Termination reason: Refutation not found, incomplete strategy
% 18.82/3.57 % (2296675)Time elapsed: 0.027 s
% 18.82/3.57 % (2296675)Peak memory usage: 94 MB
% 18.82/3.57 % (2296675)Instructions burned: 20 (million)
% 18.82/3.57 % (2296674)Refutation not found, incomplete strategy
% 18.82/3.57 % (2296674)------------------------------
% 18.82/3.57 % (2296674)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.82/3.57 % (2296674)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.82/3.57 % (2296674)CaDiCaL version: 2.1.3
% 18.82/3.57 % (2296674)Termination reason: Refutation not found, incomplete strategy
% 18.82/3.57 % (2296674)Time elapsed: 0.055 s
% 18.82/3.57 % (2296674)Peak memory usage: 93 MB
% 18.82/3.57 % (2296674)Instructions burned: 60 (million)
% 18.82/3.57 % (2296661)------------------------------
% 18.82/3.57 % (2296661)------------------------------
% 18.82/3.57 % (2296660)Refutation not found, incomplete strategy
% 18.82/3.57 % (2296660)------------------------------
% 18.82/3.57 % (2296660)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.82/3.57 % (2296660)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.82/3.57 % (2296660)CaDiCaL version: 2.1.3
% 18.82/3.57 % (2296660)Termination reason: Refutation not found, incomplete strategy
% 18.82/3.57 % (2296660)Time elapsed: 0.567 s
% 18.82/3.57 % (2296660)Peak memory usage: 146 MB
% 18.82/3.57 % (2296660)Instructions burned: 956 (million)
% 18.82/3.57 % (2296679)dis+10_5:1_slsqr=1,4:sil=8000:fde=unused:erd=off:urr=full:fd=off:s2agt=8:br=off:slsq=on:random_seed=3743628995:s2a=on:i=248:s2at=1.23:gtg=position_2992 on theBenchmark for (2992ds/248Mi)
% 18.82/3.57 % (2296673)------------------------------
% 18.82/3.57 % (2296673)------------------------------
% 18.82/3.57 % (2296675)------------------------------
% 18.82/3.57 % (2296675)------------------------------
% 18.82/3.57 % (2296660)------------------------------
% 18.82/3.57 % (2296660)------------------------------
% 18.82/3.57 % (2296674)------------------------------
% 18.82/3.57 % (2296674)------------------------------
% 18.82/3.57 % (2296679)Instruction limit reached!
% 18.82/3.57 % (2296679)------------------------------
% 18.82/3.57 % (2296679)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.82/3.57 % (2296679)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.82/3.57 % (2296679)CaDiCaL version: 2.1.3
% 18.82/3.57 % (2296679)Termination reason: Instruction limit
% 18.82/3.57 % (2296679)Termination phase: Saturation
% 18.82/3.57 % (2296679)Time elapsed: 0.238 s
% 18.82/3.57 % (2296679)Peak memory usage: 99 MB
% 18.82/3.57 % (2296679)Instructions burned: 249 (million)
% 18.82/3.57 % (2296687)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=3459160741:cts=off:i=113:fsr=off:ss=included:sgt=4_2988 on theBenchmark for (2988ds/113Mi)
% 18.82/3.57 % (2296685)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=3825412153:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2988 on theBenchmark for (2988ds/294Mi)
% 18.82/3.57 % (2296687)Refutation not found, incomplete strategy
% 18.82/3.57 % (2296687)------------------------------
% 18.82/3.57 % (2296687)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.82/3.57 % (2296687)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.82/3.57 % (2296687)CaDiCaL version: 2.1.3
% 18.82/3.57 % (2296687)Termination reason: Refutation not found, incomplete strategy
% 18.82/3.57 % (2296687)Time elapsed: 0.017 s
% 18.82/3.57 % (2296687)Peak memory usage: 94 MB
% 18.82/3.57 % (2296687)Instructions burned: 24 (million)
% 18.82/3.57 % (2296686)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=3359336136:i=2350_2988 on theBenchmark for (2988ds/2350Mi)
% 18.82/3.57 % (2296688)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=1026405374:i=127:av=off:fsr=off:sup=off_2988 on theBenchmark for (2988ds/127Mi)
% 18.82/3.57 % (2296689)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=3971828237:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2987 on theBenchmark for (2987ds/114Mi)
% 18.82/3.57 % (2296688)Instruction limit reached!
% 18.82/3.57 % (2296688)------------------------------
% 18.82/3.57 % (2296688)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.72/5.17 % (2296688)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.72/5.17 % (2296688)CaDiCaL version: 2.1.3
% 30.72/5.17 % (2296688)Termination reason: Instruction limit
% 30.72/5.17 % (2296688)Termination phase: Property scanning
% 30.72/5.17 % (2296688)Time elapsed: 0.131 s
% 30.72/5.17 % (2296688)Peak memory usage: 96 MB
% 30.72/5.17 % (2296688)Instructions burned: 128 (million)
% 30.72/5.17 % (2296658)Refutation not found, incomplete strategy
% 30.72/5.17 % (2296658)------------------------------
% 30.72/5.17 % (2296658)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.72/5.17 % (2296658)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.72/5.17 % (2296658)CaDiCaL version: 2.1.3
% 30.72/5.17 % (2296658)Termination reason: Refutation not found, incomplete strategy
% 30.72/5.17 % (2296658)Time elapsed: 1.144 s
% 30.72/5.17 % (2296658)Peak memory usage: 145 MB
% 30.72/5.17 % (2296658)Instructions burned: 1070 (million)
% 30.72/5.17 % (2296687)------------------------------
% 30.72/5.17 % (2296687)------------------------------
% 30.72/5.17 % (2296685)Instruction limit reached!
% 30.72/5.17 % (2296685)------------------------------
% 30.72/5.17 % (2296685)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.72/5.17 % (2296685)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.72/5.17 % (2296685)CaDiCaL version: 2.1.3
% 30.72/5.17 % (2296685)Termination reason: Instruction limit
% 30.72/5.17 % (2296685)Termination phase: Saturation
% 30.72/5.17 % (2296685)Time elapsed: 0.246 s
% 30.72/5.17 % (2296685)Peak memory usage: 94 MB
% 30.72/5.17 % (2296685)Instructions burned: 294 (million)
% 30.72/5.17 % (2296689)Instruction limit reached!
% 30.72/5.17 % (2296689)------------------------------
% 30.72/5.17 % (2296689)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.72/5.17 % (2296689)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.72/5.17 % (2296689)CaDiCaL version: 2.1.3
% 30.72/5.17 % (2296689)Termination reason: Instruction limit
% 30.72/5.17 % (2296689)Termination phase: Property scanning
% 30.72/5.17 % (2296689)Time elapsed: 0.073 s
% 30.72/5.17 % (2296689)Peak memory usage: 91 MB
% 30.72/5.17 % (2296689)Instructions burned: 115 (million)
% 30.72/5.17 % (2296696)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=291268278:i=437:sd=1:aac=none:ss=included_2984 on theBenchmark for (2984ds/437Mi)
% 30.72/5.17 % (2296695)lrs+10_1_sil=8000:sp=occurrence:random_seed=3087517659:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2984 on theBenchmark for (2984ds/907Mi)
% 30.72/5.17 % (2296696)Refutation not found, incomplete strategy
% 30.72/5.17 % (2296696)------------------------------
% 30.72/5.17 % (2296696)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.72/5.17 % (2296696)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.72/5.17 % (2296696)CaDiCaL version: 2.1.3
% 30.72/5.17 % (2296696)Termination reason: Refutation not found, incomplete strategy
% 30.72/5.17 % (2296696)Time elapsed: 0.015 s
% 30.72/5.17 % (2296696)Peak memory usage: 93 MB
% 30.72/5.17 % (2296696)Instructions burned: 19 (million)
% 30.72/5.17 % (2296695)Refutation not found, incomplete strategy
% 30.72/5.17 % (2296695)------------------------------
% 30.72/5.17 % (2296695)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.72/5.17 % (2296695)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.72/5.17 % (2296695)CaDiCaL version: 2.1.3
% 30.72/5.17 % (2296695)Termination reason: Refutation not found, incomplete strategy
% 30.72/5.17 % (2296695)Time elapsed: 0.035 s
% 30.72/5.17 % (2296695)Peak memory usage: 94 MB
% 30.72/5.17 % (2296695)Instructions burned: 29 (million)
% 30.72/5.17 % (2296697)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=439002310:i=5202:ss=axioms:sgt=16_2984 on theBenchmark for (2984ds/5202Mi)
% 30.72/5.17 % (2296698)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=3455842429:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2984 on theBenchmark for (2984ds/134Mi)
% 30.72/5.17 % (2296698)Refutation not found, incomplete strategy
% 30.72/5.17 % (2296698)------------------------------
% 30.72/5.17 % (2296698)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.72/5.17 % (2296698)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.72/5.17 % (2296698)CaDiCaL version: 2.1.3
% 30.72/5.17 % (2296698)Termination reason: Refutation not found, incomplete strategy
% 34.57/6.00 % (2296698)Time elapsed: 0.028 s
% 34.57/6.00 % (2296698)Peak memory usage: 94 MB
% 34.57/6.00 % (2296698)Instructions burned: 24 (million)
% 34.57/6.00 % (2296658)------------------------------
% 34.57/6.00 % (2296658)------------------------------
% 34.57/6.00 % (2296696)------------------------------
% 34.57/6.00 % (2296696)------------------------------
% 34.57/6.00 % (2296703)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=3305018929:st=8:i=592:sd=3:ep=RST:ss=axioms_2980 on theBenchmark for (2980ds/592Mi)
% 34.57/6.00 % (2296704)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=141110609:st=3:i=13193:sd=3:ss=axioms_2980 on theBenchmark for (2980ds/13193Mi)
% 34.57/6.00 % (2296695)------------------------------
% 34.57/6.00 % (2296695)------------------------------
% 34.57/6.00 % (2296698)------------------------------
% 34.57/6.00 % (2296698)------------------------------
% 34.57/6.00 % (2296709)lrs+1666_7_slsqr=4,1:sil=8000:plsq=on:plsqc=1:sos=on:urr=on:plsql=on:rp=on:alpa=false:sac=on:slsq=on:random_seed=1121845448:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2978 on theBenchmark for (2978ds/125Mi)
% 34.57/6.00 % (2296709)Refutation not found, incomplete strategy
% 34.57/6.00 % (2296709)------------------------------
% 34.57/6.00 % (2296709)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.57/6.00 % (2296709)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.57/6.00 % (2296709)CaDiCaL version: 2.1.3
% 34.57/6.00 % (2296709)Termination reason: Refutation not found, incomplete strategy
% 34.57/6.00 % (2296709)Time elapsed: 0.073 s
% 34.57/6.00 % (2296709)Peak memory usage: 94 MB
% 34.57/6.00 % (2296709)Instructions burned: 79 (million)
% 34.57/6.00 % (2296712)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=28737649:i=134:gtgl=5:slsql=off:gtg=exists_sym_2977 on theBenchmark for (2977ds/134Mi)
% 34.57/6.00 % (2296703)Instruction limit reached!
% 34.57/6.00 % (2296703)------------------------------
% 34.57/6.00 % (2296703)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.57/6.00 % (2296703)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.57/6.00 % (2296703)CaDiCaL version: 2.1.3
% 34.57/6.00 % (2296703)Termination reason: Instruction limit
% 34.57/6.00 % (2296703)Termination phase: Saturation
% 34.57/6.00 % (2296703)Time elapsed: 0.508 s
% 34.57/6.00 % (2296703)Peak memory usage: 101 MB
% 34.57/6.00 % (2296703)Instructions burned: 593 (million)
% 34.57/6.00 % (2296712)Instruction limit reached!
% 34.57/6.00 % (2296712)------------------------------
% 34.57/6.00 % (2296712)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.57/6.00 % (2296712)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.57/6.00 % (2296712)CaDiCaL version: 2.1.3
% 34.57/6.00 % (2296712)Termination reason: Instruction limit
% 34.57/6.00 % (2296712)Termination phase: Preprocessing 2
% 34.57/6.00 % (2296712)Time elapsed: 0.131 s
% 34.57/6.00 % (2296712)Peak memory usage: 92 MB
% 34.57/6.00 % (2296712)Instructions burned: 134 (million)
% 34.57/6.00 % (2296709)------------------------------
% 34.57/6.00 % (2296709)------------------------------
% 34.57/6.00 % (2296716)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=327059775:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2974 on theBenchmark for (2974ds/431Mi)
% 34.57/6.00 % (2296715)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=3950403798:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2974 on theBenchmark for (2974ds/141Mi)
% 34.57/6.00 % (2296716)Refutation not found, incomplete strategy
% 34.57/6.00 % (2296716)------------------------------
% 34.57/6.00 % (2296716)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.57/6.00 % (2296716)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.57/6.00 % (2296716)CaDiCaL version: 2.1.3
% 34.57/6.00 % (2296716)Termination reason: Refutation not found, incomplete strategy
% 34.57/6.00 % (2296716)Time elapsed: 0.024 s
% 34.57/6.00 % (2296716)Peak memory usage: 94 MB
% 34.57/6.00 % (2296716)Instructions burned: 20 (million)
% 34.57/6.00 % (2296715)Refutation not found, incomplete strategy
% 34.57/6.00 % (2296715)------------------------------
% 34.57/6.00 % (2296715)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.57/6.00 % (2296715)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.57/6.00 % (2296715)CaDiCaL version: 2.1.3
% 34.57/6.00 % (2296715)Termination reason: Refutation not found, incomplete strategy
% 53.89/8.50 % (2296715)Time elapsed: 0.025 s
% 53.89/8.50 % (2296715)Peak memory usage: 93 MB
% 53.89/8.50 % (2296715)Instructions burned: 23 (million)
% 53.89/8.50 % (2296719)lrs+1010_1_ncem=casc2026/models/loop6.pt:sil=64000:tgt=full:npcc=on:prc=on:urr=ec_only:bsr=on:fd=preordered:gs=on:sac=on:newcnf=on:random_seed=1001475217:i=6060:aac=none:ins=25_2971 on theBenchmark for (2971ds/6060Mi)
% 53.89/8.50 % (2296716)------------------------------
% 53.89/8.50 % (2296716)------------------------------
% 53.89/8.50 % (2296715)------------------------------
% 53.89/8.50 % (2296715)------------------------------
% 53.89/8.50 % (2296724)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=1149393287:i=14155:bd=all_2967 on theBenchmark for (2967ds/14155Mi)
% 53.89/8.50 % (2296723)lrs+10_16_anc=all:slsqr=32,1:sil=8000:avsql=on:sp=unary_frequency:lcm=predicate:urr=full:rp=on:br=off:slsqc=4:flr=on:sac=on:slsq=on:avsqc=1:random_seed=676366176:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2967 on theBenchmark for (2967ds/150Mi)
% 53.89/8.50 % (2296723)Instruction limit reached!
% 53.89/8.50 % (2296723)------------------------------
% 53.89/8.50 % (2296723)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 53.89/8.50 % (2296723)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.89/8.50 % (2296723)CaDiCaL version: 2.1.3
% 53.89/8.50 % (2296723)Termination reason: Instruction limit
% 53.89/8.50 % (2296723)Termination phase: Property scanning
% 53.89/8.50 % (2296723)Time elapsed: 0.154 s
% 53.89/8.50 % (2296723)Peak memory usage: 96 MB
% 53.89/8.50 % (2296723)Instructions burned: 150 (million)
% 53.89/8.50 % (2296686)Instruction limit reached!
% 53.89/8.50 % (2296686)------------------------------
% 53.89/8.50 % (2296686)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 53.89/8.50 % (2296686)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.89/8.50 % (2296686)CaDiCaL version: 2.1.3
% 53.89/8.50 % (2296686)Termination reason: Instruction limit
% 53.89/8.50 % (2296686)Termination phase: Saturation
% 53.89/8.50 % (2296686)Time elapsed: 2.313 s
% 53.89/8.50 % (2296686)Peak memory usage: 215 MB
% 53.89/8.50 % (2296686)Instructions burned: 2351 (million)
% 53.89/8.50 % (2296727)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=237054333:i=667:av=off:fsr=off_2963 on theBenchmark for (2963ds/667Mi)
% 53.89/8.50 % (2296728)ott-1011_3:1_anc=all_dependent:to=lpo:sil=8000:drc=ordering:sas=cadical:fdtod=off:sp=reverse_frequency:spb=goal_then_units:urr=full:lftc=20:newcnf=on:random_seed=3262471128:s2a=on:i=185:s2at=1.8:fdi=4_2963 on theBenchmark for (2963ds/185Mi)
% 53.89/8.50 % (2296728)Instruction limit reached!
% 53.89/8.50 % (2296728)------------------------------
% 53.89/8.50 % (2296728)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 53.89/8.50 % (2296728)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.89/8.50 % (2296728)CaDiCaL version: 2.1.3
% 53.89/8.50 % (2296728)Termination reason: Instruction limit
% 53.89/8.50 % (2296728)Termination phase: Property scanning
% 53.89/8.50 % (2296728)Time elapsed: 0.191 s
% 53.89/8.50 % (2296728)Peak memory usage: 96 MB
% 53.89/8.50 % (2296728)Instructions burned: 185 (million)
% 53.89/8.50 % (2296733)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=1508137796:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2959 on theBenchmark for (2959ds/193Mi)
% 53.89/8.50 % (2296733)Instruction limit reached!
% 53.89/8.50 % (2296733)------------------------------
% 53.89/8.50 % (2296733)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 53.89/8.50 % (2296733)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.89/8.50 % (2296733)CaDiCaL version: 2.1.3
% 53.89/8.50 % (2296733)Termination reason: Instruction limit
% 53.89/8.50 % (2296733)Termination phase: Saturation
% 53.89/8.50 % (2296733)Time elapsed: 0.091 s
% 53.89/8.50 % (2296733)Peak memory usage: 94 MB
% 53.89/8.50 % (2296733)Instructions burned: 195 (million)
% 53.89/8.50 % (2296727)Instruction limit reached!
% 53.89/8.50 % (2296727)------------------------------
% 53.89/8.50 % (2296727)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 53.89/8.50 % (2296727)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.89/8.50 % (2296727)CaDiCaL version: 2.1.3
% 53.89/8.50 % (2296727)Termination reason: Instruction limit
% 53.89/8.50 % (2296727)Termination phase: Saturation
% 53.89/8.50 % (2296727)Time elapsed: 0.614 s
% 53.89/8.50 % (2296727)Peak memory usage: 104 MB
% 66.67/10.29 % (2296727)Instructions burned: 667 (million)
% 66.67/10.29 % (2296735)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=996295521:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2956 on theBenchmark for (2956ds/4850Mi)
% 66.67/10.29 % (2296736)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=659577347:i=12111:sd=1:ss=included_2955 on theBenchmark for (2955ds/12111Mi)
% 66.67/10.29 [W928 23:53:04.376807347 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 66.67/10.29 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 66.67/10.29 [W928 23:53:04.376896620 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 66.67/10.29 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 66.67/10.29 [W928 23:53:04.376960727 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 66.67/10.29 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 66.67/10.29 [W928 23:53:04.376993514 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 66.67/10.29 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 66.67/10.29 [W928 23:53:04.377056104 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 66.67/10.29 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 66.67/10.29 [W928 23:53:04.377088161 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 66.67/10.29 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 66.67/10.29 [W928 23:53:04.377132921 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 66.67/10.29 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 66.67/10.29 [W928 23:53:04.377162088 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 66.67/10.29 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 66.67/10.29 [W928 23:53:04.377205418 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 66.67/10.29 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 66.67/10.29 [W928 23:53:04.377234521 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 66.67/10.29 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 66.67/10.29 [W928 23:53:04.377277071 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 66.67/10.29 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 66.67/10.29 [W928 23:53:04.377305895 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 100.98/15.08 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 100.98/15.08 % (2296736)Refutation not found, incomplete strategy
% 100.98/15.08 % (2296736)------------------------------
% 100.98/15.08 % (2296736)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 100.98/15.08 % (2296736)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 100.98/15.08 % (2296736)CaDiCaL version: 2.1.3
% 100.98/15.08 % (2296736)Termination reason: Refutation not found, incomplete strategy
% 100.98/15.08 % (2296736)Time elapsed: 0.835 s
% 100.98/15.08 % (2296736)Peak memory usage: 144 MB
% 100.98/15.08 % (2296736)Instructions burned: 956 (million)
% 100.98/15.08 % (2296697)Instruction limit reached!
% 100.98/15.08 % (2296697)------------------------------
% 100.98/15.08 % (2296697)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 100.98/15.08 % (2296697)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 100.98/15.08 % (2296697)CaDiCaL version: 2.1.3
% 100.98/15.08 % (2296697)Termination reason: Instruction limit
% 100.98/15.08 % (2296697)Termination phase: Saturation
% 100.98/15.08 % (2296697)Time elapsed: 3.818 s
% 100.98/15.08 % (2296697)Peak memory usage: 139 MB
% 100.98/15.08 % (2296697)Instructions burned: 5203 (million)
% 100.98/15.08 % (2296741)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=1327457725:i=319:kws=precedence:fsr=off_2943 on theBenchmark for (2943ds/319Mi)
% 100.98/15.08 % (2296736)------------------------------
% 100.98/15.08 % (2296736)------------------------------
% 100.98/15.08 % (2296743)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=2297596915:i=2064:ep=RST_2941 on theBenchmark for (2941ds/2064Mi)
% 100.98/15.08 % (2296741)Instruction limit reached!
% 100.98/15.08 % (2296741)------------------------------
% 100.98/15.08 % (2296741)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 100.98/15.08 % (2296741)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 100.98/15.08 % (2296741)CaDiCaL version: 2.1.3
% 100.98/15.08 % (2296741)Termination reason: Instruction limit
% 100.98/15.08 % (2296741)Termination phase: Saturation
% 100.98/15.08 % (2296741)Time elapsed: 0.287 s
% 100.98/15.08 % (2296741)Peak memory usage: 101 MB
% 100.98/15.08 % (2296741)Instructions burned: 319 (million)
% 100.98/15.08 % (2296745)dis-1011_128_sil=32000:random_seed=3301686306:i=3706:ep=RST:av=off_2938 on theBenchmark for (2938ds/3706Mi)
% 100.98/15.08 % (2296735)Instruction limit reached!
% 100.98/15.08 % (2296735)------------------------------
% 100.98/15.08 % (2296735)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 100.98/15.08 % (2296735)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 100.98/15.08 % (2296735)CaDiCaL version: 2.1.3
% 100.98/15.08 % (2296735)Termination reason: Instruction limit
% 100.98/15.08 % (2296735)Termination phase: Saturation
% 100.98/15.08 % (2296735)Time elapsed: 2.103 s
% 100.98/15.08 % (2296735)Peak memory usage: 119 MB
% 100.98/15.08 % (2296735)Instructions burned: 4853 (million)
% 100.98/15.08 % (2296747)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=2545615808:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2934 on theBenchmark for (2934ds/757Mi)
% 100.98/15.08 % (2296747)Refutation not found, incomplete strategy
% 100.98/15.08 % (2296747)------------------------------
% 100.98/15.08 % (2296747)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 100.98/15.08 % (2296747)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 100.98/15.08 % (2296747)CaDiCaL version: 2.1.3
% 100.98/15.08 % (2296747)Termination reason: Refutation not found, incomplete strategy
% 100.98/15.08 % (2296747)Time elapsed: 0.019 s
% 100.98/15.08 % (2296747)Peak memory usage: 94 MB
% 100.98/15.08 % (2296747)Instructions burned: 28 (million)
% 100.98/15.08 % (2296747)------------------------------
% 100.98/15.08 % (2296747)------------------------------
% 100.98/15.08 % (2296749)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=occurrence:random_seed=1311232862:i=13913:ss=axioms:sgt=8_2930 on theBenchmark for (2930ds/13913Mi)
% 100.98/15.08 % (2296749)Refutation not found, incomplete strategy
% 100.98/15.08 % (2296749)------------------------------
% 100.98/15.08 % (2296749)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 100.98/15.08 % (2296749)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 100.98/15.08 % (2296749)CaDiCaL version: 2.1.3
% 100.98/15.08 % (2296749)Termination reason: Refutation not found, incomplete strategy
% 100.98/15.08 % (2296749)Time elapsed: 0.613 s
% 100.98/15.08 % (2296749)Peak memory usage: 137 MB
% 82.78/17.33 % (2296749)Instructions burned: 1051 (million)
% 82.78/17.33 % (2296743)Instruction limit reached!
% 82.78/17.33 % (2296743)------------------------------
% 82.78/17.33 % (2296743)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 82.78/17.33 % (2296743)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 82.78/17.33 % (2296743)CaDiCaL version: 2.1.3
% 82.78/17.33 % (2296743)Termination reason: Instruction limit
% 82.78/17.33 % (2296743)Termination phase: Saturation
% 82.78/17.33 % (2296743)Time elapsed: 1.751 s
% 82.78/17.33 % (2296743)Peak memory usage: 119 MB
% 82.78/17.33 % (2296743)Instructions burned: 2065 (million)
% 82.78/17.33 % (2296749)------------------------------
% 82.78/17.33 % (2296749)------------------------------
% 82.78/17.33 % (2296754)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_frequency:sos=all:lma=off:random_seed=116729578:i=9925:aac=none_2921 on theBenchmark for (2921ds/9925Mi)
% 82.78/17.33 % (2296756)dis-1010_50_to=lpo:sil=32000:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=2561316281:i=2479:sd=2:nm=16:fsr=off:ss=axioms_2919 on theBenchmark for (2919ds/2479Mi)
% 82.78/17.33 % (2296756)Refutation not found, incomplete strategy
% 82.78/17.33 % (2296756)------------------------------
% 82.78/17.33 % (2296756)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 82.78/17.33 % (2296756)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 82.78/17.33 % (2296756)CaDiCaL version: 2.1.3
% 82.78/17.33 % (2296756)Termination reason: Refutation not found, incomplete strategy
% 82.78/17.33 % (2296756)Time elapsed: 0.027 s
% 82.78/17.33 % (2296756)Peak memory usage: 93 MB
% 82.78/17.33 % (2296756)Instructions burned: 41 (million)
% 82.78/17.33 % (2296756)------------------------------
% 82.78/17.33 % (2296756)------------------------------
% 82.78/17.33 % (2296759)ott+1002_64_sil=16000:sp=const_min:nwc=0.5:random_seed=1731425108:i=440:nm=2:av=off:gtg=exists_all:fdi=8:gsp=on_2915 on theBenchmark for (2915ds/440Mi)
% 82.78/17.33 % (2296759)Instruction limit reached!
% 82.78/17.33 % (2296759)------------------------------
% 82.78/17.33 % (2296759)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 82.78/17.33 % (2296759)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 82.78/17.33 % (2296759)CaDiCaL version: 2.1.3
% 82.78/17.33 % (2296759)Termination reason: Instruction limit
% 82.78/17.33 % (2296759)Termination phase: Saturation
% 82.78/17.33 % (2296759)Time elapsed: 0.223 s
% 82.78/17.33 % (2296759)Peak memory usage: 102 MB
% 82.78/17.33 % (2296759)Instructions burned: 442 (million)
% 82.78/17.33 % (2296761)dis-1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=100608773:st=1.5:i=11145:s2at=3:sd=3:fsr=off:ss=axioms_2911 on theBenchmark for (2911ds/11145Mi)
% 82.78/17.33 % (2296719)Instruction limit reached!
% 82.78/17.33 % (2296719)------------------------------
% 82.78/17.33 % (2296719)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 82.78/17.33 % (2296719)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 82.78/17.33 % (2296719)CaDiCaL version: 2.1.3
% 82.78/17.33 % (2296719)Termination reason: Instruction limit
% 82.78/17.33 % (2296719)Termination phase: Saturation
% 82.78/17.33 % (2296719)Time elapsed: 6.068 s
% 82.78/17.33 % (2296719)Peak memory usage: 237 MB
% 82.78/17.33 % (2296719)Instructions burned: 6060 (million)
% 82.78/17.33 % (2296745)Instruction limit reached!
% 82.78/17.33 % (2296745)------------------------------
% 82.78/17.33 % (2296745)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 82.78/17.33 % (2296745)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 82.78/17.33 % (2296745)CaDiCaL version: 2.1.3
% 82.78/17.33 % (2296745)Termination reason: Instruction limit
% 82.78/17.33 % (2296745)Termination phase: Saturation
% 82.78/17.33 % (2296745)Time elapsed: 2.961 s
% 82.78/17.33 % (2296745)Peak memory usage: 102 MB
% 82.78/17.33 % (2296745)Instructions burned: 3706 (million)
% 82.78/17.33 % (2296763)lrs+1002_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=unary_frequency:lcm=reverse:urr=on:bsr=on:random_seed=171678505:cts=off:i=3034:av=off:er=known:fsd=on_2908 on theBenchmark for (2908ds/3034Mi)
% 82.78/17.33 % (2296764)lrs-1011_64:1_sil=8000:erd=off:urr=on:nwc=0.7:br=off:random_seed=1991157114:st=2:s2a=on:i=524:s2at=2:ss=axioms_2907 on theBenchmark for (2907ds/524Mi)
% 82.78/17.33 % (2296761)Refutation not found, incomplete strategy
% 82.78/17.33 % (2296761)------------------------------
% 82.78/17.33 % (2296761)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 82.78/17.33 % (2296761)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 82.78/17.33 % (2296761)CaDiCaL version: 2.1.3
% 82.78/17.33 % (2296761)Termination reason: Refutation not found, incomplete strategy
% 82.78/17.33 % (2296761)Time elapsed: 0.555 s
% 82.78/17.33 % (2296761)Peak memory usage: 146 MB
% 82.78/17.33 % (2296761)Instructions burned: 1014 (million)
% 82.78/17.33 % (2296761)------------------------------
% 82.78/17.33 % (2296761)------------------------------
% 82.78/17.33 % (2296764)Instruction limit reached!
% 82.78/17.33 % (2296764)------------------------------
% 82.78/17.33 % (2296764)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 82.78/17.33 % (2296764)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 82.78/17.33 % (2296764)CaDiCaL version: 2.1.3
% 82.78/17.33 % (2296764)Termination reason: Instruction limit
% 82.78/17.33 % (2296764)Termination phase: Saturation
% 82.78/17.33 % (2296764)Time elapsed: 0.491 s
% 82.78/17.33 % (2296764)Peak memory usage: 100 MB
% 82.78/17.33 % (2296764)Instructions burned: 524 (million)
% 82.78/17.33 % (2296767)lrs+1011_16:1_sil=8000:acc=on:urr=on:fd=preordered:flr=on:random_seed=3234411819:avsq=on:i=1016:avsqr=676809,524288:sd=1:ss=axioms_2901 on theBenchmark for (2901ds/1016Mi)
% 82.78/17.33 % (2296767)Refutation not found, incomplete strategy
% 82.78/17.33 % (2296767)------------------------------
% 82.78/17.33 % (2296767)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 82.78/17.33 % (2296767)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 82.78/17.33 % (2296767)CaDiCaL version: 2.1.3
% 82.78/17.33 % (2296767)Termination reason: Refutation not found, incomplete strategy
% 82.78/17.33 % (2296767)Time elapsed: 0.016 s
% 82.78/17.33 % (2296767)Peak memory usage: 93 MB
% 82.78/17.33 % (2296767)Instructions burned: 24 (million)
% 82.78/17.33 % (2296768)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:fde=none:s2agt=16:random_seed=2648726411:i=14123:bd=preordered:ins=4_2901 on theBenchmark for (2901ds/14123Mi)
% 82.78/17.33 % (2296767)------------------------------
% 82.78/17.33 % (2296767)------------------------------
% 82.78/17.33 % (2296773)dis+10_4096_slsqr=16,1:sil=32000:tgt=full:plsq=on:bsr=unit_only:slsqc=1:slsq=on:random_seed=1192484390:i=5781:kws=precedence:bd=all:rawr=on_2897 on theBenchmark for (2897ds/5781Mi)
% 82.78/17.33 % (2296763)Instruction limit reached!
% 82.78/17.33 % (2296763)------------------------------
% 82.78/17.33 % (2296763)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 82.78/17.33 % (2296763)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 82.78/17.33 % (2296763)CaDiCaL version: 2.1.3
% 82.78/17.33 % (2296763)Termination reason: Instruction limit
% 82.78/17.33 % (2296763)Termination phase: Saturation
% 82.78/17.33 % (2296763)Time elapsed: 2.929 s
% 82.78/17.33 % (2296763)Peak memory usage: 212 MB
% 82.78/17.33 % (2296763)Instructions burned: 3035 (million)
% 82.78/17.33 % (2296777)lrs-1011_1_to=lpo:ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:drc=off:sp=reverse_frequency:erd=off:urr=on:br=off:random_seed=1213619727:i=2448:gtgl=5:bd=preordered:gtg=all_2876 on theBenchmark for (2876ds/2448Mi)
% 82.78/17.33 % (2296773)Instruction limit reached!
% 82.78/17.33 % (2296773)------------------------------
% 82.78/17.33 % (2296773)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 82.78/17.33 % (2296773)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 82.78/17.33 % (2296773)CaDiCaL version: 2.1.3
% 82.78/17.33 % (2296773)Termination reason: Instruction limit
% 82.78/17.33 % (2296773)Termination phase: Saturation
% 82.78/17.33 % (2296773)Time elapsed: 2.907 s
% 82.78/17.33 % (2296773)Peak memory usage: 124 MB
% 82.78/17.33 % (2296773)Instructions burned: 5783 (million)
% 82.78/17.33 % (2296779)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:lcm=reverse:random_seed=1959592267:i=3223:kws=precedence:fgj=on:av=off_2866 on theBenchmark for (2866ds/3223Mi)
% 82.78/17.33 % (2296704)Instruction limit reached!
% 82.78/17.33 % (2296704)------------------------------
% 82.78/17.33 % (2296704)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 82.78/17.33 % (2296704)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 82.78/17.33 % (2296704)CaDiCaL version: 2.1.3
% 82.78/17.33 % (2296704)Termination reason: Instruction limit
% 82.78/17.33 % (2296704)Termination phase: Saturation
% 82.78/17.33 % (2296704)Time elapsed: 12.237 s
% 82.78/17.33 % (2296704)Peak memory usage: 173 MB
% 82.78/17.33 % (2296704)Instructions burned: 13193 (million)
% 82.78/17.33 % (2296781)lrs+1002_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:sp=occurrence:sos=on:random_seed=384284908:st=5.6:i=2033:sd=3:ss=axioms_2856 on theBenchmark for (2856ds/2033Mi)
% 82.78/17.33 % (2296777)Instruction limit reached!
% 82.78/17.33 % (2296777)------------------------------
% 82.78/17.33 % (2296777)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 82.78/17.33 % (2296777)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 82.78/17.33 % (2296777)CaDiCaL version: 2.1.3
% 82.78/17.33 % (2296777)Termination reason: Instruction limit
% 82.78/17.33 % (2296777)Termination phase: Saturation
% 82.78/17.33 % (2296777)Time elapsed: 2.377 s
% 82.78/17.33 % (2296777)Peak memory usage: 202 MB
% 82.78/17.33 % (2296777)Instructions burned: 2449 (million)
% 82.78/17.33 % (2296783)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:bsd=on:random_seed=1511811903:i=2055:nm=16:gtg=position:ss=axioms:fsd=on_2851 on theBenchmark for (2851ds/2055Mi)
% 82.78/17.33 % (2296779)Instruction limit reached!
% 82.78/17.33 % (2296779)------------------------------
% 82.78/17.33 % (2296779)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 82.78/17.33 % (2296779)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 82.78/17.33 % (2296779)CaDiCaL version: 2.1.3
% 82.78/17.33 % (2296779)Termination reason: Instruction limit
% 82.78/17.33 % (2296779)Termination phase: Saturation
% 82.78/17.33 % (2296779)Time elapsed: 1.679 s
% 82.78/17.33 % (2296779)Peak memory usage: 214 MB
% 82.78/17.33 % (2296779)Instructions burned: 3224 (million)
% 82.78/17.33 % (2296787)dis+1010_1_ncem=casc2026/models/loop7.pt:sil=64000:tgt=full:npcc=on:fde=unused:sp=const_frequency:spb=goal:acc=on:random_seed=3908884967:i=21611:sd=3:ss=axioms_2848 on theBenchmark for (2848ds/21611Mi)
% 82.78/17.33 % (2296787)Refutation not found, incomplete strategy
% 82.78/17.33 % (2296787)------------------------------
% 82.78/17.33 % (2296787)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 82.78/17.33 % (2296787)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 82.78/17.33 % (2296787)CaDiCaL version: 2.1.3
% 82.78/17.33 % (2296787)Termination reason: Refutation not found, incomplete strategy
% 82.78/17.33 % (2296787)Time elapsed: 0.585 s
% 82.78/17.33 % (2296787)Peak memory usage: 137 MB
% 82.78/17.33 % (2296787)Instructions burned: 1035 (million)
% 82.78/17.33 % (2296781)First to succeed.
% 82.78/17.33 % (2296781)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-2296644"
% 82.78/17.33 % (2296787)------------------------------
% 82.78/17.33 % (2296787)------------------------------
% 82.78/17.33 % (2296791)lrs+10_1_sil=8000:sp=occurrence:sos=all:lma=off:random_seed=3896170171:i=4835:sd=13:ss=axioms:sgt=23_2838 on theBenchmark for (2838ds/4835Mi)
% 82.78/17.33 % (2296781)Refutation found. Thanks to Tanya!
% 82.78/17.33 % SZS status Theorem for theBenchmark
% 82.78/17.33 % SZS output start Proof for theBenchmark
% See solution above
% 117.22/17.55 % (2296781)------------------------------
% 117.22/17.55 % (2296781)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 117.22/17.55 % (2296781)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 117.22/17.55 % (2296781)CaDiCaL version: 2.1.3
% 117.22/17.55 % (2296781)Termination reason: Refutation
% 117.22/17.55 % (2296781)Time elapsed: 1.467 s
% 117.22/17.55 % (2296781)Peak memory usage: 155 MB
% 117.22/17.55 % (2296781)Instructions burned: 1461 (million)
% 117.22/17.55 % (2296781)------------------------------
% 117.22/17.55 % (2296781)------------------------------
% 117.22/17.55 % (2296644)Success in time 16.596 s
% 117.22/17.55 % Vampire exiting
%------------------------------------------------------------------------------