%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : CSR236+1 : TPTP v9.3.1. Released v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n003.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:09 AM UTC 2026
% Result : Theorem 26.38s 4.63s
% Output : Refutation 27.58s
% Verified :
% SZS Type : Refutation
% Derivation depth : 18
% Number of leaves : 15
% Syntax : Number of formulae : 77 ( 18 unt; 3 def)
% Number of atoms : 185 ( 0 equ)
% Maximal formula atoms : 7 ( 2 avg)
% Number of connectives : 188 ( 80 ~; 73 |; 27 &)
% ( 3 <=>; 5 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 4 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 8 ( 7 usr; 4 prp; 0-2 aty)
% Number of functors : 13 ( 13 usr; 9 con; 0-1 aty)
% Number of variables : 69 ( 0 sgn 57 !; 12 ?)
% 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/sandbox2/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/sandbox2/benchmark/theBenchmark.p',predefinitionsA12) ).
fof(f110,axiom,
! [X0] :
( p__d__subclass(X0,c__Entity)
=> ? [X1] : p__d__instance(X1,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mergeA176) ).
fof(f112,axiom,
p__d__subclass(c__Physical,c__Entity),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mergeA178) ).
fof(f115,axiom,
p__d__subclass(c__Object,c__Physical),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mergeA181) ).
fof(f2267,axiom,
p__d__subclass(c__Artifact,c__Object),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mergeA3134) ).
fof(f2305,axiom,
p__d__subclass(c__Device,c__Artifact),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mergeA3181) ).
fof(f2319,axiom,
p__d__subclass(c__EngineeringComponent,c__Device),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mergeA3200) ).
fof(f2904,axiom,
p__d__subclass(c__SwitchDevice,c__EngineeringComponent),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',miloA286) ).
fof(f2905,axiom,
! [X0] :
( p__d__instance(X0,c__SwitchDevice)
=> ? [X1,X2,X3] :
( p__d__instance(X1,c__Process)
& p__d__instance(X2,c__Process)
& p__instrument(X1,X0)
& p__causes(X1,X2)
& p__instrument(X2,X3)
& p__d__instance(X3,c__ElectricDevice) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',miloA287) ).
fof(f7288,axiom,
! [X0,X1] :
( p__instrument(X0,X1)
=> ( p__d__instance(X1,c__Physical)
& p__d__instance(X0,c__Process) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',typeA435) ).
fof(f7433,conjecture,
? [X0,X1] :
( p__d__instance(X0,c__Process)
& p__d__instance(X1,c__Physical)
& p__d__instance(X0,c__Process)
& p__d__instance(X1,c__EngineeringComponent)
& p__instrument(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',instrumentRelation0042) ).
fof(f7434,negated_conjecture,
~ ? [X0,X1] :
( p__d__instance(X0,c__Process)
& p__d__instance(X1,c__Physical)
& p__d__instance(X0,c__Process)
& p__d__instance(X1,c__EngineeringComponent)
& p__instrument(X0,X1) ),
inference(negated_conjecture,[status(cth)],[f7433]) ).
fof(f7449,plain,
! [X0,X1,X2] :
( p__d__subclass(X0,X2)
| ~ p__d__subclass(X0,X1)
| ~ p__d__subclass(X1,X2) ),
inference(ennf_transformation,[],[f2]) ).
fof(f7450,plain,
! [X0,X1,X2] :
( p__d__subclass(X0,X2)
| ~ p__d__subclass(X0,X1)
| ~ p__d__subclass(X1,X2) ),
inference(flattening,[],[f7449]) ).
fof(f7453,plain,
! [X0,X1,X2] :
( p__d__instance(X0,X2)
| ~ p__d__instance(X0,X1)
| ~ p__d__subclass(X1,X2) ),
inference(ennf_transformation,[],[f4]) ).
fof(f7454,plain,
! [X0,X1,X2] :
( p__d__instance(X0,X2)
| ~ p__d__instance(X0,X1)
| ~ p__d__subclass(X1,X2) ),
inference(flattening,[],[f7453]) ).
fof(f7503,plain,
! [X0] :
( ? [X1] : p__d__instance(X1,X0)
| ~ p__d__subclass(X0,c__Entity) ),
inference(ennf_transformation,[],[f110]) ).
fof(f8625,plain,
! [X0] :
( ? [X1,X2,X3] :
( p__d__instance(X1,c__Process)
& p__d__instance(X2,c__Process)
& p__instrument(X1,X0)
& p__causes(X1,X2)
& p__instrument(X2,X3)
& p__d__instance(X3,c__ElectricDevice) )
| ~ p__d__instance(X0,c__SwitchDevice) ),
inference(ennf_transformation,[],[f2905]) ).
fof(f11460,plain,
! [X0,X1] :
( ( p__d__instance(X1,c__Physical)
& p__d__instance(X0,c__Process) )
| ~ p__instrument(X0,X1) ),
inference(ennf_transformation,[],[f7288]) ).
fof(f11600,plain,
! [X0,X1] :
( ~ p__d__instance(X0,c__Process)
| ~ p__d__instance(X1,c__Physical)
| ~ p__d__instance(X0,c__Process)
| ~ p__d__instance(X1,c__EngineeringComponent)
| ~ p__instrument(X0,X1) ),
inference(ennf_transformation,[],[f7434]) ).
fof(f11721,plain,
! [X0] :
( p__d__instance(sK60(X0),X0)
| ~ p__d__subclass(X0,c__Entity) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK60]),skolemize(X1,sK60(X0))],[f7503]) ).
fof(f12182,plain,
! [X0] :
( ( p__d__instance(sK460(X0),c__Process)
& p__d__instance(sK461(X0),c__Process)
& p__instrument(sK460(X0),X0)
& p__causes(sK460(X0),sK461(X0))
& p__instrument(sK461(X0),sK462(X0))
& p__d__instance(sK462(X0),c__ElectricDevice) )
| ~ p__d__instance(X0,c__SwitchDevice) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK460,sK461,sK462]),skolemize(X1,sK460(X0)),skolemize(X2,sK461(X0)),skolemize(X3,sK462(X0))],[f8625]) ).
fof(f13400,plain,
! [X2,X0,X1] :
( p__d__subclass(X0,X2)
| ~ p__d__subclass(X0,X1)
| ~ p__d__subclass(X1,X2) ),
inference(cnf_transformation,[],[f7450]) ).
fof(f13402,plain,
! [X2,X0,X1] :
( p__d__instance(X0,X2)
| ~ p__d__instance(X0,X1)
| ~ p__d__subclass(X1,X2) ),
inference(cnf_transformation,[],[f7454]) ).
fof(f13680,plain,
! [X0] :
( p__d__instance(sK60(X0),X0)
| ~ p__d__subclass(X0,c__Entity) ),
inference(cnf_transformation,[],[f11721]) ).
fof(f13683,plain,
p__d__subclass(c__Physical,c__Entity),
inference(cnf_transformation,[],[f112]) ).
fof(f13689,plain,
p__d__subclass(c__Object,c__Physical),
inference(cnf_transformation,[],[f115]) ).
fof(f16455,plain,
p__d__subclass(c__Artifact,c__Object),
inference(cnf_transformation,[],[f2267]) ).
fof(f16504,plain,
p__d__subclass(c__Device,c__Artifact),
inference(cnf_transformation,[],[f2305]) ).
fof(f16522,plain,
p__d__subclass(c__EngineeringComponent,c__Device),
inference(cnf_transformation,[],[f2319]) ).
fof(f17242,plain,
p__d__subclass(c__SwitchDevice,c__EngineeringComponent),
inference(cnf_transformation,[],[f2904]) ).
fof(f17246,plain,
! [X0] :
( p__instrument(sK460(X0),X0)
| ~ p__d__instance(X0,c__SwitchDevice) ),
inference(cnf_transformation,[],[f12182]) ).
fof(f23888,plain,
! [X0,X1] :
( ~ p__instrument(X0,X1)
| p__d__instance(X0,c__Process) ),
inference(cnf_transformation,[],[f11460]) ).
fof(f23889,plain,
! [X0,X1] :
( ~ p__instrument(X0,X1)
| p__d__instance(X1,c__Physical) ),
inference(cnf_transformation,[],[f11460]) ).
fof(f24205,plain,
! [X0,X1] :
( ~ p__d__instance(X0,c__Process)
| ~ p__d__instance(X1,c__Physical)
| ~ p__d__instance(X0,c__Process)
| ~ p__d__instance(X1,c__EngineeringComponent)
| ~ p__instrument(X0,X1) ),
inference(cnf_transformation,[],[f11600]) ).
fof(f24674,plain,
! [X0,X1] :
( ~ p__d__instance(X0,c__Process)
| ~ p__d__instance(X1,c__Physical)
| ~ p__d__instance(X1,c__EngineeringComponent)
| ~ p__instrument(X0,X1) ),
inference(duplicate_literal_removal,[],[f24205]) ).
fof(f24675,plain,
! [X0,X1] :
( ~ p__d__instance(X1,c__Physical)
| ~ p__d__instance(X1,c__EngineeringComponent)
| ~ p__instrument(X0,X1) ),
inference(forward_subsumption_resolution,[],[f24674,f23888]) ).
fof(f24676,plain,
! [X0,X1] :
( ~ p__instrument(X0,X1)
| ~ p__d__instance(X1,c__EngineeringComponent) ),
inference(forward_subsumption_resolution,[],[f24675,f23889]) ).
fof(f24718,plain,
! [X0] :
( ~ p__d__instance(X0,c__SwitchDevice)
| ~ p__d__instance(X0,c__EngineeringComponent) ),
inference(resolution,[],[f24676,f17246]) ).
fof(f24764,plain,
( ~ p__d__instance(sK60(c__SwitchDevice),c__EngineeringComponent)
| ~ p__d__subclass(c__SwitchDevice,c__Entity) ),
inference(resolution,[],[f24718,f13680]) ).
fof(f24877,definition,
( spl1264_1
<=> p__d__subclass(c__EngineeringComponent,c__Entity) ),
introduced(definition,[new_symbols(definition,[spl1264_1])],[avatar_definition]) ).
fof(f24878,plain,
( p__d__subclass(c__EngineeringComponent,c__Entity)
| ~ spl1264_1 ),
inference(avatar_component_clause,[],[f24877]) ).
fof(f24879,plain,
( ~ p__d__subclass(c__EngineeringComponent,c__Entity)
| spl1264_1 ),
inference(avatar_component_clause,[],[f24877]) ).
fof(f24885,plain,
( ! [X0] :
( ~ p__d__subclass(c__EngineeringComponent,X0)
| ~ p__d__subclass(X0,c__Entity) )
| spl1264_1 ),
inference(resolution,[],[f24879,f13400]) ).
fof(f24886,plain,
( ~ p__d__subclass(c__Device,c__Entity)
| spl1264_1 ),
inference(resolution,[],[f24885,f16522]) ).
fof(f24889,plain,
( ! [X0] :
( ~ p__d__subclass(c__Device,X0)
| ~ p__d__subclass(X0,c__Entity) )
| spl1264_1 ),
inference(resolution,[],[f24886,f13400]) ).
fof(f24890,plain,
( ~ p__d__subclass(c__Artifact,c__Entity)
| spl1264_1 ),
inference(resolution,[],[f24889,f16504]) ).
fof(f24893,plain,
( ! [X0] :
( ~ p__d__subclass(c__Artifact,X0)
| ~ p__d__subclass(X0,c__Entity) )
| spl1264_1 ),
inference(resolution,[],[f24890,f13400]) ).
fof(f24894,plain,
( ~ p__d__subclass(c__Object,c__Entity)
| spl1264_1 ),
inference(resolution,[],[f24893,f16455]) ).
fof(f24897,plain,
( ! [X0] :
( ~ p__d__subclass(c__Object,X0)
| ~ p__d__subclass(X0,c__Entity) )
| spl1264_1 ),
inference(resolution,[],[f24894,f13400]) ).
fof(f24898,plain,
( ~ p__d__subclass(c__Physical,c__Entity)
| spl1264_1 ),
inference(resolution,[],[f24897,f13689]) ).
fof(f24901,plain,
( $false
| spl1264_1 ),
inference(forward_subsumption_resolution,[],[f24898,f13683]) ).
fof(f24902,plain,
spl1264_1,
inference(avatar_contradiction_clause,[],[f24901]) ).
fof(f24909,definition,
( spl1264_3
<=> p__d__subclass(c__SwitchDevice,c__Entity) ),
introduced(definition,[new_symbols(definition,[spl1264_3])],[avatar_definition]) ).
fof(f24910,plain,
( p__d__subclass(c__SwitchDevice,c__Entity)
| ~ spl1264_3 ),
inference(avatar_component_clause,[],[f24909]) ).
fof(f24911,plain,
( ~ p__d__subclass(c__SwitchDevice,c__Entity)
| spl1264_3 ),
inference(avatar_component_clause,[],[f24909]) ).
fof(f24913,definition,
( spl1264_4
<=> p__d__instance(sK60(c__SwitchDevice),c__EngineeringComponent) ),
introduced(definition,[new_symbols(definition,[spl1264_4])],[avatar_definition]) ).
fof(f24915,plain,
( ~ p__d__instance(sK60(c__SwitchDevice),c__EngineeringComponent)
| spl1264_4 ),
inference(avatar_component_clause,[],[f24913]) ).
fof(f24916,plain,
( ~ spl1264_3
| ~ spl1264_4 ),
inference(avatar_split_clause,[],[f24764,f24913,f24909]) ).
fof(f24917,plain,
( ! [X0] :
( ~ p__d__subclass(c__SwitchDevice,X0)
| ~ p__d__subclass(X0,c__Entity) )
| spl1264_3 ),
inference(resolution,[],[f24911,f13400]) ).
fof(f24918,plain,
( ~ p__d__subclass(c__EngineeringComponent,c__Entity)
| spl1264_3 ),
inference(resolution,[],[f24917,f17242]) ).
fof(f24921,plain,
( $false
| ~ spl1264_1
| spl1264_3 ),
inference(forward_subsumption_resolution,[],[f24918,f24878]) ).
fof(f24922,plain,
( ~ spl1264_1
| spl1264_3 ),
inference(avatar_contradiction_clause,[],[f24921]) ).
fof(f24923,plain,
( ! [X0] :
( ~ p__d__instance(sK60(c__SwitchDevice),X0)
| ~ p__d__subclass(X0,c__EngineeringComponent) )
| spl1264_4 ),
inference(resolution,[],[f24915,f13402]) ).
fof(f25147,plain,
( ~ p__d__subclass(c__SwitchDevice,c__EngineeringComponent)
| ~ p__d__subclass(c__SwitchDevice,c__Entity)
| spl1264_4 ),
inference(resolution,[],[f24923,f13680]) ).
fof(f25176,plain,
( ~ p__d__subclass(c__SwitchDevice,c__Entity)
| spl1264_4 ),
inference(forward_subsumption_resolution,[],[f25147,f17242]) ).
fof(f25177,plain,
( $false
| ~ spl1264_3
| spl1264_4 ),
inference(forward_subsumption_resolution,[],[f25176,f24910]) ).
fof(f25178,plain,
( ~ spl1264_3
| spl1264_4 ),
inference(avatar_contradiction_clause,[],[f25177]) ).
cnf(s2,plain,
spl1264_1,
inference(sat_conversion,[],[f24902]) ).
cnf(s3,plain,
( ~ spl1264_3
| ~ spl1264_4 ),
inference(sat_conversion,[],[f24916]) ).
cnf(s4,plain,
( ~ spl1264_1
| spl1264_3 ),
inference(sat_conversion,[],[f24922]) ).
cnf(s13,plain,
( ~ spl1264_3
| spl1264_4 ),
inference(sat_conversion,[],[f25178]) ).
cnf(s18,plain,
spl1264_3,
inference(rat,[],[s4,s2]) ).
cnf(s19,plain,
spl1264_4,
inference(rat,[],[s13,s18]) ).
cnf(s20,plain,
$false,
inference(rat,[],[s3,s19,s18]) ).
fof(f25179,plain,
$false,
inference(avatar_sat_refutation,[],[s20]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR236+1 : TPTP v9.3.1. Released v7.3.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.20 % Computer : n003.cluster.edu
% 0.08/0.20 % Model : x86_64 x86_64
% 0.08/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.20 % Memory : 8046.5625MB
% 0.08/0.20 % OS : Linux 6.8.0-71-generic
% 0.08/0.20 % CPULimit : 300
% 0.08/0.20 % WCLimit : 300
% 0.08/0.20 % DateTime : Mon Sep 28 23:52:13 UTC 2026
% 0.08/0.20 % CPUTime :
% 0.08/0.20 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.24 Running first-order theorem proving
% 0.08/0.24 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 3.77/1.44 % (2142486)Detected formulas, will run a generic FOF schedule.
% 3.77/1.44 % (2142493)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=1983295878:i=141695:sd=1:nm=32:gsp=on:ss=included_2998 on theBenchmark for (2998ds/141695Mi)
% 3.77/1.44 % (2142495)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=1938897898:i=119:av=off:ss=axioms_2998 on theBenchmark for (2998ds/119Mi)
% 3.77/1.44 % (2142494)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=2625280929:i=109:sd=1:ins=1:gsp=on:ss=axioms_2998 on theBenchmark for (2998ds/109Mi)
% 3.77/1.44 % (2142492)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=848105297:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2998 on theBenchmark for (2998ds/134677Mi)
% 3.77/1.44 % (2142491)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=2541201275:i=141193_2998 on theBenchmark for (2998ds/141193Mi)
% 3.77/1.44 % (2142497)dis-21_1_sil=8000:lcm=predicate:random_seed=1619806064: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)
% 3.77/1.44 % (2142496)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3364130484:s2a=on:i=139:gtg=position_2998 on theBenchmark for (2998ds/139Mi)
% 3.77/1.44 % (2142494)Refutation not found, incomplete strategy
% 3.77/1.44 % (2142494)------------------------------
% 3.77/1.44 % (2142494)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.77/1.44 % (2142494)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.77/1.44 % (2142494)CaDiCaL version: 2.1.3
% 3.77/1.44 % (2142494)Termination reason: Refutation not found, incomplete strategy
% 3.77/1.44 % (2142494)Time elapsed: 0.016 s
% 3.77/1.44 % (2142494)Peak memory usage: 92 MB
% 3.77/1.44 % (2142494)Instructions burned: 23 (million)
% 3.77/1.44 % (2142495)Refutation not found, incomplete strategy
% 3.77/1.44 % (2142495)------------------------------
% 3.77/1.44 % (2142495)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.77/1.44 % (2142495)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.77/1.44 % (2142495)CaDiCaL version: 2.1.3
% 3.77/1.44 % (2142495)Termination reason: Refutation not found, incomplete strategy
% 3.77/1.44 % (2142495)Time elapsed: 0.016 s
% 3.77/1.44 % (2142495)Peak memory usage: 93 MB
% 3.77/1.44 % (2142495)Instructions burned: 24 (million)
% 3.77/1.44 % (2142497)Instruction limit reached!
% 3.77/1.44 % (2142497)------------------------------
% 3.77/1.44 % (2142497)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.77/1.44 % (2142497)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.77/1.44 % (2142497)CaDiCaL version: 2.1.3
% 3.77/1.44 % (2142497)Termination reason: Instruction limit
% 3.77/1.44 % (2142497)Termination phase: Saturation
% 3.77/1.44 % (2142497)Time elapsed: 0.075 s
% 3.77/1.44 % (2142497)Peak memory usage: 95 MB
% 3.77/1.44 % (2142497)Instructions burned: 129 (million)
% 3.77/1.44 % (2142496)Instruction limit reached!
% 3.77/1.44 % (2142496)------------------------------
% 3.77/1.44 % (2142496)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.77/1.44 % (2142496)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.77/1.44 % (2142496)CaDiCaL version: 2.1.3
% 3.77/1.44 % (2142496)Termination reason: Instruction limit
% 3.77/1.44 % (2142496)Termination phase: Preprocessing 3
% 3.77/1.44 % (2142496)Time elapsed: 0.086 s
% 3.77/1.44 % (2142496)Peak memory usage: 94 MB
% 3.77/1.44 % (2142496)Instructions burned: 140 (million)
% 3.77/1.44 [W928 23:52:14.571120008 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.
% 3.77/1.44 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 3.77/1.44 [W928 23:52:14.571146664 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.
% 3.77/1.44 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 3.77/1.44 [W928 23:52:14.571168733 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.
% 5.85/1.71 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 5.85/1.71 [W928 23:52:14.571175589 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.
% 5.85/1.71 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 5.85/1.71 [W928 23:52:14.571188651 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.
% 5.85/1.71 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 5.85/1.71 [W928 23:52:14.571194042 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.
% 5.85/1.71 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 5.85/1.71 [W928 23:52:14.571206571 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.
% 5.85/1.71 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 5.85/1.71 [W928 23:52:14.571211835 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.
% 5.85/1.71 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 5.85/1.71 [W928 23:52:14.571224033 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.
% 5.85/1.71 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 5.85/1.71 [W928 23:52:14.571235920 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.
% 5.85/1.71 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 5.85/1.71 [W928 23:52:14.571249707 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.
% 5.85/1.71 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 5.85/1.71 [W928 23:52:14.571254926 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.
% 5.85/1.71 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 5.85/1.71 % (2142505)lrs+10_1_sil=8000:sp=occurrence:random_seed=2941124361:i=285:sd=3:ss=axioms:sgt=8_2995 on theBenchmark for (2995ds/285Mi)
% 5.85/1.71 % (2142505)Refutation not found, incomplete strategy
% 5.85/1.71 % (2142505)------------------------------
% 5.85/1.71 % (2142505)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.85/1.71 % (2142505)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.85/1.71 % (2142505)CaDiCaL version: 2.1.3
% 5.85/1.71 % (2142505)Termination reason: Refutation not found, incomplete strategy
% 5.85/1.71 % (2142505)Time elapsed: 0.016 s
% 5.85/1.71 % (2142505)Peak memory usage: 94 MB
% 5.85/1.71 % (2142505)Instructions burned: 20 (million)
% 5.85/1.71 % (2142506)lrs+10_1_sil=32000:urr=on:br=off:random_seed=57682648:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2995 on theBenchmark for (2995ds/157Mi)
% 5.85/1.71 % (2142495)------------------------------
% 5.85/1.71 % (2142495)------------------------------
% 5.85/1.71 % (2142494)------------------------------
% 5.85/1.71 % (2142494)------------------------------
% 5.85/1.71 % (2142506)Refutation not found, incomplete strategy
% 9.06/2.12 % (2142506)------------------------------
% 9.06/2.12 % (2142506)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.06/2.12 % (2142506)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.06/2.12 % (2142506)CaDiCaL version: 2.1.3
% 9.06/2.12 % (2142506)Termination reason: Refutation not found, incomplete strategy
% 9.06/2.12 % (2142506)Time elapsed: 0.032 s
% 9.06/2.12 % (2142506)Peak memory usage: 93 MB
% 9.06/2.12 % (2142506)Instructions burned: 60 (million)
% 9.06/2.12 % (2142493)Refutation not found, incomplete strategy
% 9.06/2.12 % (2142493)------------------------------
% 9.06/2.12 % (2142493)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.06/2.12 % (2142493)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.06/2.12 % (2142493)CaDiCaL version: 2.1.3
% 9.06/2.12 % (2142493)Termination reason: Refutation not found, incomplete strategy
% 9.06/2.12 % (2142493)Time elapsed: 0.400 s
% 9.06/2.12 % (2142493)Peak memory usage: 148 MB
% 9.06/2.12 % (2142493)Instructions burned: 957 (million)
% 9.06/2.12 % (2142510)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=919734328:s2a=on:i=248:s2at=1.23:gtg=position_2994 on theBenchmark for (2994ds/248Mi)
% 9.06/2.12 % (2142509)lrs+1011_1_sil=32000:sp=occurrence:random_seed=431959800:i=325:sd=1:ss=axioms:sgt=32_2994 on theBenchmark for (2994ds/325Mi)
% 9.06/2.12 [W928 23:52:14.827000035 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.06/2.12 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 9.06/2.12 [W928 23:52:14.827040586 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.06/2.12 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 9.06/2.12 [W928 23:52:14.827078229 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.06/2.12 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 9.06/2.12 [W928 23:52:14.827090936 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.06/2.12 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 9.06/2.12 [W928 23:52:14.827116156 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.06/2.12 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 9.06/2.12 [W928 23:52:14.827127257 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.06/2.12 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 9.06/2.12 [W928 23:52:14.827153350 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.06/2.12 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 9.06/2.12 [W928 23:52:14.827164920 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.06/2.12 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 9.06/2.12 [W928 23:52:14.827189514 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.06/2.12 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 13.14/2.81 [W928 23:52:14.827199804 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.
% 13.14/2.81 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 13.14/2.81 [W928 23:52:14.827231864 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.
% 13.14/2.81 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 13.14/2.81 [W928 23:52:14.827242145 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.
% 13.14/2.81 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 13.14/2.81 % (2142509)Refutation not found, incomplete strategy
% 13.14/2.81 % (2142509)------------------------------
% 13.14/2.81 % (2142509)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.14/2.81 % (2142509)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.14/2.81 % (2142509)CaDiCaL version: 2.1.3
% 13.14/2.81 % (2142509)Termination reason: Refutation not found, incomplete strategy
% 13.14/2.81 % (2142509)Time elapsed: 0.018 s
% 13.14/2.81 % (2142509)Peak memory usage: 94 MB
% 13.14/2.81 % (2142509)Instructions burned: 22 (million)
% 13.14/2.81 % (2142510)Instruction limit reached!
% 13.14/2.81 % (2142510)------------------------------
% 13.14/2.81 % (2142510)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.14/2.81 % (2142510)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.14/2.81 % (2142510)CaDiCaL version: 2.1.3
% 13.14/2.81 % (2142510)Termination reason: Instruction limit
% 13.14/2.81 % (2142510)Termination phase: Saturation
% 13.14/2.81 % (2142510)Time elapsed: 0.075 s
% 13.14/2.81 % (2142510)Peak memory usage: 99 MB
% 13.14/2.81 % (2142510)Instructions burned: 250 (million)
% 13.14/2.81 % (2142505)------------------------------
% 13.14/2.81 % (2142505)------------------------------
% 13.14/2.81 % (2142506)------------------------------
% 13.14/2.81 % (2142506)------------------------------
% 13.14/2.81 % (2142513)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=2294038142:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2992 on theBenchmark for (2992ds/294Mi)
% 13.14/2.81 % (2142493)------------------------------
% 13.14/2.81 % (2142493)------------------------------
% 13.14/2.81 % (2142514)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=952763504:i=2350_2991 on theBenchmark for (2991ds/2350Mi)
% 13.14/2.81 % (2142513)Instruction limit reached!
% 13.14/2.81 % (2142513)------------------------------
% 13.14/2.81 % (2142513)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.14/2.81 % (2142513)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.14/2.81 % (2142513)CaDiCaL version: 2.1.3
% 13.14/2.81 % (2142513)Termination reason: Instruction limit
% 13.14/2.81 % (2142513)Termination phase: Saturation
% 13.14/2.81 % (2142513)Time elapsed: 0.078 s
% 13.14/2.81 % (2142513)Peak memory usage: 94 MB
% 13.14/2.81 % (2142513)Instructions burned: 296 (million)
% 13.14/2.81 % (2142492)Refutation not found, incomplete strategy
% 13.14/2.81 % (2142492)------------------------------
% 13.14/2.81 % (2142492)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.14/2.81 % (2142492)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.14/2.81 % (2142492)CaDiCaL version: 2.1.3
% 13.14/2.81 % (2142492)Termination reason: Refutation not found, incomplete strategy
% 13.14/2.81 % (2142492)Time elapsed: 0.670 s
% 13.14/2.81 % (2142492)Peak memory usage: 147 MB
% 13.14/2.81 % (2142492)Instructions burned: 967 (million)
% 13.14/2.81 % (2142509)------------------------------
% 13.14/2.81 % (2142509)------------------------------
% 13.14/2.81 % (2142515)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=870845899:cts=off:i=113:fsr=off:ss=included:sgt=4_2991 on theBenchmark for (2991ds/113Mi)
% 13.14/2.81 % (2142515)Refutation not found, incomplete strategy
% 13.14/2.81 % (2142515)------------------------------
% 13.14/2.81 % (2142515)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.14/2.81 % (2142515)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.32/3.36 % (2142515)CaDiCaL version: 2.1.3
% 17.32/3.36 % (2142515)Termination reason: Refutation not found, incomplete strategy
% 17.32/3.36 % (2142515)Time elapsed: 0.017 s
% 17.32/3.36 % (2142515)Peak memory usage: 93 MB
% 17.32/3.36 % (2142515)Instructions burned: 23 (million)
% 17.32/3.36 % (2142517)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=2706179448:i=127:av=off:fsr=off:sup=off_2990 on theBenchmark for (2990ds/127Mi)
% 17.32/3.36 % (2142519)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=937637795:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2990 on theBenchmark for (2990ds/114Mi)
% 17.32/3.36 % (2142519)Instruction limit reached!
% 17.32/3.36 % (2142519)------------------------------
% 17.32/3.36 % (2142519)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.32/3.36 % (2142519)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.32/3.36 % (2142519)CaDiCaL version: 2.1.3
% 17.32/3.36 % (2142519)Termination reason: Instruction limit
% 17.32/3.36 % (2142519)Termination phase: Property scanning
% 17.32/3.36 % (2142519)Time elapsed: 0.034 s
% 17.32/3.36 % (2142519)Peak memory usage: 92 MB
% 17.32/3.36 % (2142519)Instructions burned: 119 (million)
% 17.32/3.36 % (2142517)Instruction limit reached!
% 17.32/3.36 % (2142517)------------------------------
% 17.32/3.36 % (2142517)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.32/3.36 % (2142517)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.32/3.36 % (2142517)CaDiCaL version: 2.1.3
% 17.32/3.36 % (2142517)Termination reason: Instruction limit
% 17.32/3.36 % (2142517)Termination phase: Property scanning
% 17.32/3.36 % (2142517)Time elapsed: 0.080 s
% 17.32/3.36 % (2142517)Peak memory usage: 96 MB
% 17.32/3.36 % (2142517)Instructions burned: 127 (million)
% 17.32/3.36 % (2142521)lrs+10_1_sil=8000:sp=occurrence:random_seed=1360168980:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2989 on theBenchmark for (2989ds/907Mi)
% 17.32/3.36 % (2142521)Refutation not found, incomplete strategy
% 17.32/3.36 % (2142521)------------------------------
% 17.32/3.36 % (2142521)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.32/3.36 % (2142521)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.32/3.36 % (2142521)CaDiCaL version: 2.1.3
% 17.32/3.36 % (2142521)Termination reason: Refutation not found, incomplete strategy
% 17.32/3.36 % (2142521)Time elapsed: 0.018 s
% 17.32/3.36 % (2142521)Peak memory usage: 94 MB
% 17.32/3.36 % (2142521)Instructions burned: 21 (million)
% 17.32/3.36 % (2142492)------------------------------
% 17.32/3.36 % (2142492)------------------------------
% 17.32/3.36 % (2142515)------------------------------
% 17.32/3.36 % (2142515)------------------------------
% 17.32/3.36 % (2142524)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=1636891732:i=437:sd=1:aac=none:ss=included_2988 on theBenchmark for (2988ds/437Mi)
% 17.32/3.36 % (2142524)Refutation not found, incomplete strategy
% 17.32/3.36 % (2142524)------------------------------
% 17.32/3.36 % (2142524)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.32/3.36 % (2142524)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.32/3.36 % (2142524)CaDiCaL version: 2.1.3
% 17.32/3.36 % (2142524)Termination reason: Refutation not found, incomplete strategy
% 17.32/3.36 % (2142524)Time elapsed: 0.009 s
% 17.32/3.36 % (2142524)Peak memory usage: 93 MB
% 17.32/3.36 % (2142524)Instructions burned: 19 (million)
% 17.32/3.36 % (2142526)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=2603583398:i=5202:ss=axioms:sgt=16_2988 on theBenchmark for (2988ds/5202Mi)
% 17.32/3.36 % (2142527)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=2265625514:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2987 on theBenchmark for (2987ds/134Mi)
% 17.32/3.36 % (2142527)Refutation not found, incomplete strategy
% 17.32/3.36 % (2142527)------------------------------
% 17.32/3.36 % (2142527)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.32/3.36 % (2142527)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.32/3.36 % (2142527)CaDiCaL version: 2.1.3
% 17.32/3.36 % (2142527)Termination reason: Refutation not found, incomplete strategy
% 17.32/3.36 % (2142527)Time elapsed: 0.019 s
% 17.32/3.36 % (2142527)Peak memory usage: 94 MB
% 17.32/3.36 % (2142527)Instructions burned: 24 (million)
% 17.32/3.36 % (2142524)------------------------------
% 17.32/3.36 % (2142524)------------------------------
% 20.82/3.91 % (2142529)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=3545663066:st=8:i=592:sd=3:ep=RST:ss=axioms_2987 on theBenchmark for (2987ds/592Mi)
% 20.82/3.91 % (2142521)------------------------------
% 20.82/3.91 % (2142521)------------------------------
% 20.82/3.91 % (2142533)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=1956194625:st=3:i=13193:sd=3:ss=axioms_2985 on theBenchmark for (2985ds/13193Mi)
% 20.82/3.91 % (2142534)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=177273589:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2985 on theBenchmark for (2985ds/125Mi)
% 20.82/3.91 % (2142534)Refutation not found, incomplete strategy
% 20.82/3.91 % (2142534)------------------------------
% 20.82/3.91 % (2142534)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.82/3.91 % (2142534)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.82/3.91 % (2142534)CaDiCaL version: 2.1.3
% 20.82/3.91 % (2142534)Termination reason: Refutation not found, incomplete strategy
% 20.82/3.91 % (2142534)Time elapsed: 0.043 s
% 20.82/3.91 % (2142534)Peak memory usage: 94 MB
% 20.82/3.91 % (2142534)Instructions burned: 78 (million)
% 20.82/3.91 % (2142527)------------------------------
% 20.82/3.91 % (2142527)------------------------------
% 20.82/3.91 % (2142529)Instruction limit reached!
% 20.82/3.91 % (2142529)------------------------------
% 20.82/3.91 % (2142529)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.82/3.91 % (2142529)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.82/3.91 % (2142529)CaDiCaL version: 2.1.3
% 20.82/3.91 % (2142529)Termination reason: Instruction limit
% 20.82/3.91 % (2142529)Termination phase: Saturation
% 20.82/3.91 % (2142529)Time elapsed: 0.323 s
% 20.82/3.91 % (2142529)Peak memory usage: 102 MB
% 20.82/3.91 % (2142529)Instructions burned: 594 (million)
% 20.82/3.91 % (2142537)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=2721924552:i=134:gtgl=5:slsql=off:gtg=exists_sym_2983 on theBenchmark for (2983ds/134Mi)
% 20.82/3.91 % (2142534)------------------------------
% 20.82/3.91 % (2142534)------------------------------
% 20.82/3.91 % (2142538)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=546093731:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2982 on theBenchmark for (2982ds/141Mi)
% 20.82/3.91 % (2142537)Instruction limit reached!
% 20.82/3.91 % (2142537)------------------------------
% 20.82/3.91 % (2142537)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.82/3.91 % (2142537)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.82/3.91 % (2142537)CaDiCaL version: 2.1.3
% 20.82/3.91 % (2142537)Termination reason: Instruction limit
% 20.82/3.91 % (2142537)Termination phase: Preprocessing 2
% 20.82/3.91 % (2142537)Time elapsed: 0.077 s
% 20.82/3.91 % (2142537)Peak memory usage: 92 MB
% 20.82/3.91 % (2142537)Instructions burned: 134 (million)
% 20.82/3.91 % (2142538)Refutation not found, incomplete strategy
% 20.82/3.91 % (2142538)------------------------------
% 20.82/3.91 % (2142538)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.82/3.91 % (2142538)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.82/3.91 % (2142538)CaDiCaL version: 2.1.3
% 20.82/3.91 % (2142538)Termination reason: Refutation not found, incomplete strategy
% 20.82/3.91 % (2142538)Time elapsed: 0.017 s
% 20.82/3.91 % (2142538)Peak memory usage: 93 MB
% 20.82/3.91 % (2142538)Instructions burned: 23 (million)
% 20.82/3.91 % (2142526)Refutation not found, incomplete strategy
% 20.82/3.91 % (2142526)------------------------------
% 20.82/3.91 % (2142526)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.82/3.91 % (2142526)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.82/3.91 % (2142526)CaDiCaL version: 2.1.3
% 20.82/3.91 % (2142526)Termination reason: Refutation not found, incomplete strategy
% 20.82/3.91 % (2142526)Time elapsed: 0.623 s
% 20.82/3.91 % (2142526)Peak memory usage: 144 MB
% 20.82/3.91 % (2142526)Instructions burned: 984 (million)
% 20.82/3.91 % (2142541)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=1370840972:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2980 on theBenchmark for (2980ds/431Mi)
% 20.82/3.91 % (2142542)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=1723523894:i=6060:aac=none:ins=25_2980 on theBenchmark for (2980ds/6060Mi)
% 26.38/4.63 % (2142526)------------------------------
% 26.38/4.63 % (2142526)------------------------------
% 26.38/4.63 % (2142538)------------------------------
% 26.38/4.63 % (2142538)------------------------------
% 26.38/4.63 % (2142545)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=3089717110:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2978 on theBenchmark for (2978ds/150Mi)
% 26.38/4.63 % (2142545)Instruction limit reached!
% 26.38/4.63 % (2142545)------------------------------
% 26.38/4.63 % (2142545)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.38/4.63 % (2142545)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.38/4.63 % (2142545)CaDiCaL version: 2.1.3
% 26.38/4.63 % (2142545)Termination reason: Instruction limit
% 26.38/4.63 % (2142545)Termination phase: Property scanning
% 26.38/4.63 % (2142545)Time elapsed: 0.048 s
% 26.38/4.63 % (2142545)Peak memory usage: 96 MB
% 26.38/4.63 % (2142545)Instructions burned: 151 (million)
% 26.38/4.63 % (2142541)Instruction limit reached!
% 26.38/4.63 % (2142541)------------------------------
% 26.38/4.63 % (2142541)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.38/4.63 % (2142541)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.38/4.63 % (2142541)CaDiCaL version: 2.1.3
% 26.38/4.63 % (2142541)Termination reason: Instruction limit
% 26.38/4.63 % (2142541)Termination phase: Saturation
% 26.38/4.63 % (2142541)Time elapsed: 0.233 s
% 26.38/4.63 % (2142541)Peak memory usage: 98 MB
% 26.38/4.63 % (2142541)Instructions burned: 431 (million)
% 26.38/4.63 % (2142546)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=1933228241:i=14155:bd=all_2977 on theBenchmark for (2977ds/14155Mi)
% 26.38/4.63 % (2142548)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=1872928318:i=667:av=off:fsr=off_2976 on theBenchmark for (2976ds/667Mi)
% 26.38/4.63 % (2142514)Instruction limit reached!
% 26.38/4.63 % (2142514)------------------------------
% 26.38/4.63 % (2142514)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.38/4.63 % (2142514)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.38/4.63 % (2142514)CaDiCaL version: 2.1.3
% 26.38/4.63 % (2142514)Termination reason: Instruction limit
% 26.38/4.63 % (2142514)Termination phase: Saturation
% 26.38/4.63 % (2142514)Time elapsed: 1.491 s
% 26.38/4.63 % (2142514)Peak memory usage: 207 MB
% 26.38/4.63 % (2142514)Instructions burned: 2352 (million)
% 26.38/4.63 % (2142549)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=896558501:s2a=on:i=185:s2at=1.8:fdi=4_2976 on theBenchmark for (2976ds/185Mi)
% 26.38/4.63 % (2142548)Instruction limit reached!
% 26.38/4.63 % (2142548)------------------------------
% 26.38/4.63 % (2142548)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.38/4.63 % (2142548)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.38/4.63 % (2142548)CaDiCaL version: 2.1.3
% 26.38/4.63 % (2142548)Termination reason: Instruction limit
% 26.38/4.63 % (2142548)Termination phase: Saturation
% 26.38/4.63 % (2142548)Time elapsed: 0.197 s
% 26.38/4.63 % (2142548)Peak memory usage: 105 MB
% 26.38/4.63 % (2142548)Instructions burned: 668 (million)
% 26.38/4.63 % (2142549)Instruction limit reached!
% 26.38/4.63 % (2142549)------------------------------
% 26.38/4.63 % (2142549)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.38/4.63 % (2142549)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.38/4.63 % (2142549)CaDiCaL version: 2.1.3
% 26.38/4.63 % (2142549)Termination reason: Instruction limit
% 26.38/4.63 % (2142549)Termination phase: Property scanning
% 26.38/4.63 % (2142549)Time elapsed: 0.119 s
% 26.38/4.63 % (2142549)Peak memory usage: 97 MB
% 26.38/4.63 % (2142549)Instructions burned: 185 (million)
% 26.38/4.63 % (2142552)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=3490806031:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2975 on theBenchmark for (2975ds/193Mi)
% 26.38/4.63 % (2142552)Refutation not found, incomplete strategy
% 26.38/4.63 % (2142552)------------------------------
% 26.38/4.63 % (2142552)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.38/4.63 % (2142552)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.38/4.63 % (2142552)CaDiCaL version: 2.1.3
% 26.38/4.63 % (2142552)Termination reason: Refutation not found, incomplete strategy
% 26.38/4.63 % (2142552)Time elapsed: 0.029 s
% 26.38/4.63 % (2142552)Peak memory usage: 94 MB
% 26.38/4.63 % (2142552)Instructions burned: 41 (million)
% 26.38/4.63 % (2142554)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=1764073508:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2973 on theBenchmark for (2973ds/4850Mi)
% 26.38/4.63 % (2142555)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=1646644316:i=12111:sd=1:ss=included_2973 on theBenchmark for (2973ds/12111Mi)
% 26.38/4.63 % (2142552)------------------------------
% 26.38/4.63 % (2142552)------------------------------
% 26.38/4.63 % (2142559)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=1780046886:i=319:kws=precedence:fsr=off_2970 on theBenchmark for (2970ds/319Mi)
% 26.38/4.63 [W928 23:52:17.303117434 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.
% 26.38/4.63 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 26.38/4.63 [W928 23:52:17.303154258 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.
% 26.38/4.63 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 26.38/4.63 [W928 23:52:17.303193198 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.
% 26.38/4.63 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 26.38/4.63 [W928 23:52:17.303207325 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.
% 26.38/4.63 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 26.38/4.63 [W928 23:52:17.303233239 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.
% 26.38/4.63 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 26.38/4.63 [W928 23:52:17.303244469 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.
% 26.38/4.63 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 26.38/4.63 [W928 23:52:17.303271273 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.
% 26.38/4.63 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 26.38/4.63 [W928 23:52:17.303282336 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.
% 26.38/4.63 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 26.38/4.63 [W928 23:52:17.303307390 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.
% 26.38/4.63 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 26.38/4.63 [W928 23:52:17.303318547 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.
% 26.38/4.63 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 26.38/4.63 [W928 23:52:17.303343780 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.
% 26.38/4.63 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 26.38/4.63 [W928 23:52:17.303354907 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.
% 26.38/4.63 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 26.38/4.63 % (2142559)Instruction limit reached!
% 26.38/4.63 % (2142559)------------------------------
% 26.38/4.63 % (2142559)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.38/4.63 % (2142559)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.38/4.63 % (2142559)CaDiCaL version: 2.1.3
% 26.38/4.63 % (2142559)Termination reason: Instruction limit
% 26.38/4.63 % (2142559)Termination phase: Saturation
% 26.38/4.63 % (2142559)Time elapsed: 0.169 s
% 26.38/4.63 % (2142559)Peak memory usage: 101 MB
% 26.38/4.63 % (2142559)Instructions burned: 319 (million)
% 26.38/4.63 % (2142561)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=482454445:i=2064:ep=RST_2967 on theBenchmark for (2967ds/2064Mi)
% 26.38/4.63 % (2142555)Refutation not found, incomplete strategy
% 26.38/4.63 % (2142555)------------------------------
% 26.38/4.63 % (2142555)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.38/4.63 % (2142555)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.38/4.63 % (2142555)CaDiCaL version: 2.1.3
% 26.38/4.63 % (2142555)Termination reason: Refutation not found, incomplete strategy
% 26.38/4.63 % (2142555)Time elapsed: 0.651 s
% 26.38/4.63 % (2142555)Peak memory usage: 148 MB
% 26.38/4.63 % (2142555)Instructions burned: 953 (million)
% 26.38/4.63 % (2142561)First to succeed.
% 26.38/4.63 % (2142561)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2142486"
% 26.38/4.63 % (2142555)------------------------------
% 26.38/4.63 % (2142555)------------------------------
% 26.38/4.63 % (2142563)dis-1011_128_sil=32000:random_seed=616610793:i=3706:ep=RST:av=off_2962 on theBenchmark for (2962ds/3706Mi)
% 26.38/4.63 % (2142561)Refutation found. Thanks to Tanya!
% 26.38/4.63 % SZS status Theorem for theBenchmark
% 26.38/4.63 % SZS output start Proof for theBenchmark
% See solution above
% 27.58/4.84 % (2142561)------------------------------
% 27.58/4.84 % (2142561)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.58/4.84 % (2142561)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.58/4.84 % (2142561)CaDiCaL version: 2.1.3
% 27.58/4.84 % (2142561)Termination reason: Refutation
% 27.58/4.84 % (2142561)Time elapsed: 0.230 s
% 27.58/4.84 % (2142561)Peak memory usage: 106 MB
% 27.58/4.84 % (2142561)Instructions burned: 445 (million)
% 27.58/4.84 % (2142561)------------------------------
% 27.58/4.84 % (2142561)------------------------------
% 27.58/4.84 % (2142486)Success in time 3.955 s
% 27.58/4.84 % Vampire exiting
%------------------------------------------------------------------------------