%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : HWV068-1 : TPTP v9.3.1. Bugfixed v5.5.1.
% 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 10:37:45 AM UTC 2026
% Result : Unsatisfiable 84.88s 13.89s
% Output : Refutation 84.88s
% Verified :
% SZS Type : Refutation
% Derivation depth : 8
% Number of leaves : 20
% Syntax : Number of formulae : 37 ( 21 unt; 0 def)
% Number of atoms : 65 ( 0 equ)
% Maximal formula atoms : 6 ( 1 avg)
% Number of connectives : 63 ( 35 ~; 28 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 5 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 20 ( 19 usr; 3 prp; 0-4 aty)
% Number of functors : 1 ( 1 usr; 1 con; 0-0 aty)
% Number of variables : 84 ( 84 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f3266,axiom,
! [X2,X3,X0,X1] :
( esk16516_4(X0,X1,X2,X3)
| ~ esk17157_4(X0,X1,X2,X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_3266) ).
fof(f4556,axiom,
esk2_0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_4556) ).
fof(f6107,axiom,
! [X2,X3,X0,X1] :
( esk16516_4(X0,X1,X2,X3)
| ~ esk18138_4(X0,X1,X2,X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_6107) ).
fof(f16515,axiom,
! [X2,X3,X0,X1] :
( ~ esk17609_4(X0,X1,X2,X3)
| esk18140_4(X0,X1,X2,X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_16515) ).
fof(f21184,axiom,
! [X2,X3,X0,X1] : ~ esk16516_4(X0,X1,X2,X3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_21184) ).
fof(f22074,axiom,
! [X2,X3,X0,X1] :
( ~ esk17148_4(X0,X1,X2,X3)
| esk17564_4(X0,X1,X2,X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_22074) ).
fof(f23116,axiom,
! [X2,X3,X0,X1] :
( ~ esk18140_4(X0,X1,X2,X3)
| esk18139_4(X0,X1,X2,X3)
| esk18137_4(X0,X1,X2,X3)
| esk18138_4(X0,X1,X2,X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_23116) ).
fof(f25870,axiom,
! [X2,X3,X0,X1] :
( ~ esk16349_4(X0,X1,X2,X3)
| esk16348_4(X0,X1,X2,X3)
| esk16347_4(X0,X1,X2,X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_25870) ).
fof(f26220,axiom,
! [X2,X3,X0,X1] :
( ~ esk16347_4(X0,X1,X2,X3)
| esk17148_4(X0,X1,X2,X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_26220) ).
fof(f32444,axiom,
! [X2,X3,X0,X1] :
( ~ esk18139_4(X0,X1,X2,X3)
| esk17148_4(X0,X1,X2,X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_32444) ).
fof(f33259,axiom,
! [X2,X3,X0,X1] :
( ~ esk16222_4(X0,X1,X2,X3)
| esk16220_4(X0,X1,X2,X3)
| esk16221_4(X0,X1,X2,X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_33259) ).
fof(f34555,axiom,
! [X2,X3,X0,X1] :
( esk17147_4(X0,X3,X1,X2)
| ~ p(X1)
| ~ p(X2)
| ~ p(X0)
| ~ esk2_0
| ~ p(X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_34555) ).
fof(f37238,axiom,
~ esk1_0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_37238) ).
fof(f40742,axiom,
! [X2,X3,X0,X1] :
( ~ esk18137_4(X0,X1,X2,X3)
| esk16516_4(X0,X1,X2,X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_40742) ).
fof(f41865,axiom,
! [X2,X3,X0,X1] :
( ~ esk16221_4(X0,X1,X2,X3)
| esk17157_4(X0,X1,X2,X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_41865) ).
fof(f43176,axiom,
! [X2,X3,X0,X1] :
( ~ esk17564_4(X1,X2,X3,X0)
| esk1_0
| ~ p(X1)
| ~ p(X0)
| ~ p(X3)
| ~ p(X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_43176) ).
fof(f44955,axiom,
! [X2,X3,X0,X1] :
( ~ esk16348_4(X0,X1,X2,X3)
| esk17609_4(X0,X1,X2,X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_44955) ).
fof(f45914,axiom,
! [X2,X3,X0,X1] :
( ~ esk17147_4(X0,X1,X2,X3)
| esk16222_4(X0,X1,X2,X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_45914) ).
fof(f47728,axiom,
! [X2,X3,X0,X1] :
( ~ esk16220_4(X0,X1,X2,X3)
| esk16349_4(X0,X1,X2,X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_47728) ).
fof(f49911,axiom,
p(true),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rule_true) ).
fof(f50454,plain,
! [X2,X3,X0,X1] : ~ esk18138_4(X0,X1,X2,X3),
inference(forward_subsumption_resolution,[],[f6107,f21184]) ).
fof(f50520,plain,
! [X2,X3,X0,X1] : ~ esk17157_4(X0,X1,X2,X3),
inference(forward_subsumption_resolution,[],[f3266,f21184]) ).
fof(f50708,plain,
~ esk17564_4(true,true,true,true),
inference(unit_resulting_resolution,[],[f43176,f49911,f49911,f49911,f49911,f37238]) ).
fof(f50712,plain,
esk17147_4(true,true,true,true),
inference(unit_resulting_resolution,[],[f34555,f49911,f4556,f49911,f49911,f49911]) ).
fof(f50801,plain,
! [X2,X3,X0,X1] : ~ esk18137_4(X0,X1,X2,X3),
inference(unit_resulting_resolution,[],[f40742,f21184]) ).
fof(f50881,plain,
esk16222_4(true,true,true,true),
inference(unit_resulting_resolution,[],[f45914,f50712]) ).
fof(f51117,plain,
! [X2,X3,X0,X1] : ~ esk16221_4(X0,X1,X2,X3),
inference(unit_resulting_resolution,[],[f41865,f50520]) ).
fof(f51118,plain,
esk16220_4(true,true,true,true),
inference(unit_resulting_resolution,[],[f33259,f50881,f51117]) ).
fof(f51543,plain,
esk16349_4(true,true,true,true),
inference(unit_resulting_resolution,[],[f47728,f51118]) ).
fof(f53435,plain,
~ esk17148_4(true,true,true,true),
inference(unit_resulting_resolution,[],[f22074,f50708]) ).
fof(f53437,plain,
~ esk16347_4(true,true,true,true),
inference(unit_resulting_resolution,[],[f26220,f53435]) ).
fof(f53439,plain,
~ esk18139_4(true,true,true,true),
inference(unit_resulting_resolution,[],[f32444,f53435]) ).
fof(f53442,plain,
~ esk18140_4(true,true,true,true),
inference(unit_resulting_resolution,[],[f23116,f50454,f50801,f53439]) ).
fof(f53443,plain,
esk16348_4(true,true,true,true),
inference(unit_resulting_resolution,[],[f25870,f51543,f53437]) ).
fof(f53445,plain,
esk17609_4(true,true,true,true),
inference(unit_resulting_resolution,[],[f44955,f53443]) ).
fof(f53448,plain,
esk18140_4(true,true,true,true),
inference(unit_resulting_resolution,[],[f16515,f53445]) ).
fof(f53449,plain,
$false,
inference(forward_subsumption_resolution,[],[f53448,f53442]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : HWV068-1 : TPTP v9.3.1. Bugfixed v5.5.1.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.13/0.39 % Computer : n014.cluster.edu
% 0.13/0.39 % Model : x86_64 x86_64
% 0.13/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.39 % Memory : 8046.5625MB
% 0.13/0.39 % OS : Linux 6.8.0-71-generic
% 0.13/0.39 % CPULimit : 300
% 0.13/0.40 % WCLimit : 300
% 0.13/0.40 % DateTime : Sun Sep 27 11:21:02 UTC 2026
% 0.13/0.40 % CPUTime :
% 0.13/0.40 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.13/0.44 Running first-order theorem proving
% 0.13/0.45 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
% 13.46/3.74 % (647299)Input is clausal, will run a generic CNF schedule.
% 13.46/3.74 % (647304)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=4119273542:i=140167_2990 on theBenchmark for (2990ds/140167Mi)
% 13.46/3.74 % (647305)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=497387718:i=132376:av=off_2990 on theBenchmark for (2990ds/132376Mi)
% 13.46/3.74 % (647308)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=2192523722:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2990 on theBenchmark for (2990ds/114Mi)
% 13.46/3.74 % (647306)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=4088632110:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2990 on theBenchmark for (2990ds/137899Mi)
% 13.46/3.74 % (647307)lrs+10_1_sil=8000:sp=occurrence:random_seed=673825497:i=107:sd=3:ss=axioms:sgt=8_2990 on theBenchmark for (2990ds/107Mi)
% 13.46/3.74 % (647310)dis-21_1_sil=8000:lcm=predicate:random_seed=3288928154:st=5:avsq=on:i=117:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2990 on theBenchmark for (2990ds/117Mi)
% 13.46/3.74 % (647309)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1609959002:s2a=on:i=180:gtg=position_2990 on theBenchmark for (2990ds/180Mi)
% 13.46/3.74 % (647308)Instruction limit reached!
% 13.46/3.74 % (647308)------------------------------
% 13.46/3.74 % (647308)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.46/3.74 % (647308)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.46/3.74 % (647308)CaDiCaL version: 2.1.3
% 13.46/3.74 % (647308)Termination reason: Instruction limit
% 13.46/3.74 % (647308)Termination phase: SInE selection
% 13.46/3.74 % (647308)Time elapsed: 0.075 s
% 13.46/3.74 % (647308)Peak memory usage: 122 MB
% 13.46/3.74 % (647308)Instructions burned: 114 (million)
% 13.46/3.74 % (647307)Refutation not found, incomplete strategy
% 13.46/3.74 % (647307)------------------------------
% 13.46/3.74 % (647307)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.46/3.74 % (647307)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.46/3.74 % (647307)CaDiCaL version: 2.1.3
% 13.46/3.74 % (647307)Termination reason: Refutation not found, incomplete strategy
% 13.46/3.74 % (647307)Time elapsed: 0.097 s
% 13.46/3.74 % (647307)Peak memory usage: 135 MB
% 13.46/3.74 % (647307)Instructions burned: 95 (million)
% 13.46/3.74 % (647309)Instruction limit reached!
% 13.46/3.74 % (647309)------------------------------
% 13.46/3.74 % (647309)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.46/3.74 % (647309)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.46/3.74 % (647309)CaDiCaL version: 2.1.3
% 13.46/3.74 % (647309)Termination reason: Instruction limit
% 13.46/3.74 % (647309)Termination phase: Property scanning
% 13.46/3.74 % (647309)Time elapsed: 0.093 s
% 13.46/3.74 % (647309)Peak memory usage: 121 MB
% 13.46/3.74 % (647309)Instructions burned: 181 (million)
% 13.46/3.74 % (647310)Instruction limit reached!
% 13.46/3.74 % (647310)------------------------------
% 13.46/3.74 % (647310)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.46/3.74 % (647310)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.46/3.74 % (647310)CaDiCaL version: 2.1.3
% 13.46/3.74 % (647310)Termination reason: Instruction limit
% 13.46/3.74 % (647310)Termination phase: Property scanning
% 13.46/3.74 % (647310)Time elapsed: 0.130 s
% 13.46/3.74 % (647310)Peak memory usage: 132 MB
% 13.46/3.74 % (647310)Instructions burned: 118 (million)
% 13.46/3.74 % (647318)dis+1010_3_sil=8000:plsq=on:drc=off:fde=none:plsqc=1:bsd=on:plsqr=7,2:sos=on:spb=goal_then_units:random_seed=792425427:i=143:sd=2:aac=none:ss=axioms:sgt=16_2987 on theBenchmark for (2987ds/143Mi)
% 13.46/3.74 % (647319)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=425799873:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2987 on theBenchmark for (2987ds/189Mi)
% 13.46/3.74 % (647320)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=4232869415:st=4:i=219:sd=3:ss=axioms_2986 on theBenchmark for (2986ds/219Mi)
% 13.46/3.74 % (647307)------------------------------
% 13.46/3.74 % (647307)------------------------------
% 13.46/3.74 % (647318)Refutation not found, incomplete strategy
% 13.46/3.74 % (647318)------------------------------
% 13.46/3.74 % (647318)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.61/6.16 % (647318)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.61/6.16 % (647318)CaDiCaL version: 2.1.3
% 31.61/6.16 % (647318)Termination reason: Refutation not found, incomplete strategy
% 31.61/6.16 % (647318)Time elapsed: 0.113 s
% 31.61/6.16 % (647318)Peak memory usage: 135 MB
% 31.61/6.16 % (647318)Instructions burned: 127 (million)
% 31.61/6.16 % (647319)Instruction limit reached!
% 31.61/6.16 % (647319)------------------------------
% 31.61/6.16 % (647319)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.61/6.16 % (647319)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.61/6.16 % (647319)CaDiCaL version: 2.1.3
% 31.61/6.16 % (647319)Termination reason: Instruction limit
% 31.61/6.16 % (647319)Termination phase: SInE selection
% 31.61/6.16 % (647319)Time elapsed: 0.128 s
% 31.61/6.16 % (647319)Peak memory usage: 122 MB
% 31.61/6.16 % (647319)Instructions burned: 190 (million)
% 31.61/6.16 % (647320)Refutation not found, incomplete strategy
% 31.61/6.16 % (647320)------------------------------
% 31.61/6.16 % (647320)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.61/6.16 % (647320)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.61/6.16 % (647320)CaDiCaL version: 2.1.3
% 31.61/6.16 % (647320)Termination reason: Refutation not found, incomplete strategy
% 31.61/6.16 % (647320)Time elapsed: 0.128 s
% 31.61/6.16 % (647320)Peak memory usage: 135 MB
% 31.61/6.16 % (647320)Instructions burned: 161 (million)
% 31.61/6.16 % (647324)lrs+10_64_to=lpo:sil=8000:random_seed=449062120:i=126:bd=preordered_2984 on theBenchmark for (2984ds/126Mi)
% 31.61/6.16 % (647325)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=763822431:avsq=on:i=194:fgj=on:bd=preordered_2984 on theBenchmark for (2984ds/194Mi)
% 31.61/6.16 % (647318)------------------------------
% 31.61/6.16 % (647318)------------------------------
% 31.61/6.16 % (647324)Instruction limit reached!
% 31.61/6.16 % (647324)------------------------------
% 31.61/6.16 % (647324)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.61/6.16 % (647324)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.61/6.16 % (647324)CaDiCaL version: 2.1.3
% 31.61/6.16 % (647324)Termination reason: Instruction limit
% 31.61/6.16 % (647324)Termination phase: Saturation
% 31.61/6.16 % (647324)Time elapsed: 0.130 s
% 31.61/6.16 % (647324)Peak memory usage: 135 MB
% 31.61/6.16 % (647324)Instructions burned: 127 (million)
% 31.61/6.16 % (647320)------------------------------
% 31.61/6.16 % (647320)------------------------------
% 31.61/6.16 % (647328)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=319648537:i=157:gtg=all_2982 on theBenchmark for (2982ds/157Mi)
% 31.61/6.16 % (647325)Instruction limit reached!
% 31.61/6.16 % (647325)------------------------------
% 31.61/6.16 % (647325)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.61/6.16 % (647325)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.61/6.16 % (647325)CaDiCaL version: 2.1.3
% 31.61/6.16 % (647325)Termination reason: Instruction limit
% 31.61/6.16 % (647325)Termination phase: Saturation
% 31.61/6.16 % (647325)Time elapsed: 0.166 s
% 31.61/6.16 % (647325)Peak memory usage: 135 MB
% 31.61/6.16 % (647325)Instructions burned: 195 (million)
% 31.61/6.16 % (647328)Instruction limit reached!
% 31.61/6.16 % (647328)------------------------------
% 31.61/6.17 % (647328)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.61/6.17 % (647328)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.61/6.17 % (647328)CaDiCaL version: 2.1.3
% 31.61/6.17 % (647328)Termination reason: Instruction limit
% 31.61/6.17 % (647328)Termination phase: Property scanning
% 31.61/6.17 % (647328)Time elapsed: 0.052 s
% 31.61/6.17 % (647328)Peak memory usage: 122 MB
% 31.61/6.17 % (647328)Instructions burned: 157 (million)
% 31.61/6.17 % (647329)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=3232493054:i=3394:sd=4:ss=included:sgt=64_2981 on theBenchmark for (2981ds/3394Mi)
% 31.61/6.17 % (647330)lrs+1011_5_to=lpo:sil=8000:tgt=full:plsq=on:prc=on:drc=off:plsqr=31,4:sp=occurrence:urr=on:nwc=0.8:s2agt=16:br=off:random_seed=80322797:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2981 on theBenchmark for (2981ds/106Mi)
% 31.61/6.17 % (647332)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=1261245400:i=107_2980 on theBenchmark for (2980ds/107Mi)
% 43.02/7.87 % (647333)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=366248135:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2980 on theBenchmark for (2980ds/242Mi)
% 43.02/7.87 % (647330)Instruction limit reached!
% 43.02/7.87 % (647330)------------------------------
% 43.02/7.87 % (647330)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 43.02/7.87 % (647330)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.02/7.87 % (647330)CaDiCaL version: 2.1.3
% 43.02/7.87 % (647330)Termination reason: Instruction limit
% 43.02/7.87 % (647330)Termination phase: SInE selection
% 43.02/7.87 % (647330)Time elapsed: 0.091 s
% 43.02/7.87 % (647330)Peak memory usage: 123 MB
% 43.02/7.87 % (647330)Instructions burned: 106 (million)
% 43.02/7.87 % (647332)Instruction limit reached!
% 43.02/7.87 % (647332)------------------------------
% 43.02/7.87 % (647332)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 43.02/7.87 % (647332)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.02/7.88 % (647332)CaDiCaL version: 2.1.3
% 43.02/7.88 % (647332)Termination reason: Instruction limit
% 43.02/7.88 % (647332)Termination phase: Saturation
% 43.02/7.88 % (647332)Time elapsed: 0.088 s
% 43.02/7.88 % (647332)Peak memory usage: 134 MB
% 43.02/7.88 % (647332)Instructions burned: 108 (million)
% 43.02/7.88 % (647333)Instruction limit reached!
% 43.02/7.88 % (647333)------------------------------
% 43.02/7.88 % (647333)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 43.02/7.88 % (647333)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.02/7.88 % (647333)CaDiCaL version: 2.1.3
% 43.02/7.88 % (647333)Termination reason: Instruction limit
% 43.02/7.88 % (647333)Termination phase: Property scanning
% 43.02/7.88 % (647333)Time elapsed: 0.077 s
% 43.02/7.88 % (647333)Peak memory usage: 121 MB
% 43.02/7.88 % (647333)Instructions burned: 244 (million)
% 43.02/7.88 % (647338)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=2617728120:cond=fast:i=5208:av=off_2978 on theBenchmark for (2978ds/5208Mi)
% 43.02/7.88 % (647340)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=952483083:i=499:bd=all_2978 on theBenchmark for (2978ds/499Mi)
% 43.02/7.88 % (647339)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=991405380:i=134:sd=2:doe=on:ss=axioms:sgt=14_2978 on theBenchmark for (2978ds/134Mi)
% 43.02/7.88 % (647339)Refutation not found, incomplete strategy
% 43.02/7.88 % (647339)------------------------------
% 43.02/7.88 % (647339)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 43.02/7.88 % (647339)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.02/7.88 % (647339)CaDiCaL version: 2.1.3
% 43.02/7.88 % (647339)Termination reason: Refutation not found, incomplete strategy
% 43.02/7.88 % (647339)Time elapsed: 0.111 s
% 43.02/7.88 % (647339)Peak memory usage: 135 MB
% 43.02/7.88 % (647339)Instructions burned: 122 (million)
% 43.02/7.88 % (647340)Instruction limit reached!
% 43.02/7.88 % (647340)------------------------------
% 43.02/7.88 % (647340)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 43.02/7.88 % (647340)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.02/7.88 % (647340)CaDiCaL version: 2.1.3
% 43.02/7.88 % (647340)Termination reason: Instruction limit
% 43.02/7.88 % (647340)Termination phase: Saturation
% 43.02/7.88 % (647340)Time elapsed: 0.211 s
% 43.02/7.88 % (647340)Peak memory usage: 144 MB
% 43.02/7.88 % (647340)Instructions burned: 501 (million)
% 43.02/7.88 % (647344)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=3370533972:i=191:fgj=on:bd=all_2974 on theBenchmark for (2974ds/191Mi)
% 43.02/7.88 % (647339)------------------------------
% 43.02/7.88 % (647339)------------------------------
% 43.02/7.88 % (647344)Instruction limit reached!
% 43.02/7.88 % (647344)------------------------------
% 43.02/7.88 % (647344)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 43.02/7.88 % (647344)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.02/7.88 % (647344)CaDiCaL version: 2.1.3
% 43.02/7.88 % (647344)Termination reason: Instruction limit
% 43.02/7.88 % (647344)Termination phase: Saturation
% 43.02/7.88 % (647344)Time elapsed: 0.103 s
% 43.02/7.88 % (647344)Peak memory usage: 136 MB
% 43.02/7.88 % (647344)Instructions burned: 192 (million)
% 43.02/7.88 % (647346)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=470630098:i=264:kws=precedence:fsr=off_2973 on theBenchmark for (2973ds/264Mi)
% 40.63/8.19 % (647347)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=2893846566:cond=on:i=156:bs=on:gtg=exists_all:er=known_2972 on theBenchmark for (2972ds/156Mi)
% 40.63/8.19 % (647347)Instruction limit reached!
% 40.63/8.19 % (647347)------------------------------
% 40.63/8.19 % (647347)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.63/8.19 % (647347)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.63/8.19 % (647347)CaDiCaL version: 2.1.3
% 40.63/8.19 % (647347)Termination reason: Instruction limit
% 40.63/8.19 % (647347)Termination phase: Property scanning
% 40.63/8.19 % (647347)Time elapsed: 0.051 s
% 40.63/8.19 % (647347)Peak memory usage: 121 MB
% 40.63/8.19 % (647347)Instructions burned: 159 (million)
% 40.63/8.19 % (647346)Instruction limit reached!
% 40.63/8.19 % (647346)------------------------------
% 40.63/8.19 % (647346)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.63/8.19 % (647346)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.63/8.19 % (647346)CaDiCaL version: 2.1.3
% 40.63/8.19 % (647346)Termination reason: Instruction limit
% 40.63/8.19 % (647346)Termination phase: Saturation
% 40.63/8.19 % (647346)Time elapsed: 0.200 s
% 40.63/8.19 % (647346)Peak memory usage: 134 MB
% 40.63/8.19 % (647346)Instructions burned: 264 (million)
% 40.63/8.19 % (647350)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=reverse_frequency:spb=units:lcm=predicate:urr=on:s2agt=8:updr=off:random_seed=4041349763:i=3256:kws=precedence:bd=preordered:av=off_2970 on theBenchmark for (2970ds/3256Mi)
% 40.63/8.19 % (647351)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=2979107498:i=537:av=off:ss=included_2969 on theBenchmark for (2969ds/537Mi)
% 40.63/8.19 % (647351)Instruction limit reached!
% 40.63/8.19 % (647351)------------------------------
% 40.63/8.19 % (647351)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.63/8.19 % (647351)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.63/8.19 % (647351)CaDiCaL version: 2.1.3
% 40.63/8.19 % (647351)Termination reason: Instruction limit
% 40.63/8.19 % (647351)Termination phase: Saturation
% 40.63/8.19 % (647351)Time elapsed: 0.366 s
% 40.63/8.19 % (647351)Peak memory usage: 134 MB
% 40.63/8.19 % (647351)Instructions burned: 537 (million)
% 40.63/8.19 % (647354)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=2481517068:i=180:bd=preordered:av=off_2963 on theBenchmark for (2963ds/180Mi)
% 40.63/8.19 % (647354)Instruction limit reached!
% 40.63/8.19 % (647354)------------------------------
% 40.63/8.19 % (647354)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.63/8.19 % (647354)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.63/8.19 % (647354)CaDiCaL version: 2.1.3
% 40.63/8.19 % (647354)Termination reason: Instruction limit
% 40.63/8.19 % (647354)Termination phase: Saturation
% 40.63/8.19 % (647354)Time elapsed: 0.176 s
% 40.63/8.19 % (647354)Peak memory usage: 134 MB
% 40.63/8.19 % (647354)Instructions burned: 181 (million)
% 40.63/8.19 % (647356)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:sas=cadical:sp=reverse_frequency:bsr=on:alpa=false:sac=on:random_seed=565523915:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2960 on theBenchmark for (2960ds/10307Mi)
% 40.63/8.19 % (647350)Instruction limit reached!
% 40.63/8.19 % (647350)------------------------------
% 40.63/8.19 % (647350)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.63/8.19 % (647350)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.63/8.19 % (647350)CaDiCaL version: 2.1.3
% 40.63/8.19 % (647350)Termination reason: Instruction limit
% 40.63/8.19 % (647350)Termination phase: Saturation
% 40.63/8.19 % (647350)Time elapsed: 1.935 s
% 40.63/8.19 % (647350)Peak memory usage: 446 MB
% 40.63/8.19 % (647350)Instructions burned: 3258 (million)
% 40.63/8.19 % (647358)lrs-1010_1024_to=lpo:sil=8000:tgt=ground:plsq=on:plsqc=1:sas=cadical:plsqr=1,32:sp=arity:lma=off:spb=goal:acc=on:bce=on:nwc=1.2:alpa=false:random_seed=2828838390:i=412:gtgl=4:gtg=exists_all_2949 on theBenchmark for (2949ds/412Mi)
% 40.63/8.19 % (647329)Instruction limit reached!
% 40.63/8.19 % (647329)------------------------------
% 40.63/8.19 % (647329)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.63/8.19 % (647329)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 61.72/10.53 % (647329)CaDiCaL version: 2.1.3
% 61.72/10.53 % (647329)Termination reason: Instruction limit
% 61.72/10.53 % (647329)Termination phase: Saturation
% 61.72/10.53 % (647329)Time elapsed: 3.285 s
% 61.72/10.53 % (647329)Peak memory usage: 470 MB
% 61.72/10.53 % (647329)Instructions burned: 3394 (million)
% 61.72/10.53 % (647358)Instruction limit reached!
% 61.72/10.53 % (647358)------------------------------
% 61.72/10.53 % (647358)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 61.72/10.53 % (647358)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 61.72/10.53 % (647358)CaDiCaL version: 2.1.3
% 61.72/10.53 % (647358)Termination reason: Instruction limit
% 61.72/10.53 % (647358)Termination phase: Property scanning
% 61.72/10.53 % (647358)Time elapsed: 0.146 s
% 61.72/10.53 % (647358)Peak memory usage: 122 MB
% 61.72/10.53 % (647358)Instructions burned: 413 (million)
% 61.72/10.53 % (647361)ott-1011_2_sil=32000:bsd=on:sp=reverse_frequency:erd=off:urr=on:rnwc=on:gs=on:s2agt=70:updr=off:lftc=20:random_seed=2753609304:s2a=on:i=303:s2at=2:sd=1:kws=inv_arity:bs=on:ins=10:fdi=1024:sup=off:ss=included_2946 on theBenchmark for (2946ds/303Mi)
% 61.72/10.53 % (647360)ott+1002_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:etr=on:spb=units:urr=on:bsr=unit_only:gs=on:s2agt=16:br=off:random_seed=2513273041:s2pl=no:i=8478:s2at=4:nm=6_2946 on theBenchmark for (2946ds/8478Mi)
% 61.72/10.53 % (647361)Instruction limit reached!
% 61.72/10.53 % (647361)------------------------------
% 61.72/10.53 % (647361)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 61.72/10.53 % (647361)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 61.72/10.53 % (647361)CaDiCaL version: 2.1.3
% 61.72/10.53 % (647361)Termination reason: Instruction limit
% 61.72/10.53 % (647361)Termination phase: Property scanning
% 61.72/10.53 % (647361)Time elapsed: 0.163 s
% 61.72/10.53 % (647361)Peak memory usage: 125 MB
% 61.72/10.53 % (647361)Instructions burned: 305 (million)
% 61.72/10.53 % (647364)lrs+10_1_to=lpo:sil=16000:fde=none:sos=on:urr=on:bsr=on:random_seed=1144939187:st=4:i=720:sd=3:fsr=off:ss=axioms_2943 on theBenchmark for (2943ds/720Mi)
% 61.72/10.53 % (647364)Refutation not found, incomplete strategy
% 61.72/10.53 % (647364)------------------------------
% 61.72/10.53 % (647364)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 61.72/10.53 % (647364)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 61.72/10.53 % (647364)CaDiCaL version: 2.1.3
% 61.72/10.53 % (647364)Termination reason: Refutation not found, incomplete strategy
% 61.72/10.53 % (647364)Time elapsed: 0.091 s
% 61.72/10.53 % (647364)Peak memory usage: 135 MB
% 61.72/10.53 % (647364)Instructions burned: 160 (million)
% 61.72/10.53 % (647364)------------------------------
% 61.72/10.53 % (647364)------------------------------
% 61.72/10.53 % (647366)lrs-20_1_to=lpo:sil=32000:tgt=ground:sp=reverse_frequency:spb=goal:urr=on:bsr=unit_only:nwc=1.5:random_seed=1964158251:i=598:bs=on:bd=preordered:av=off:ss=axioms_2939 on theBenchmark for (2939ds/598Mi)
% 61.72/10.53 % (647366)Refutation not found, incomplete strategy
% 61.72/10.53 % (647366)------------------------------
% 61.72/10.53 % (647366)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 61.72/10.53 % (647366)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 61.72/10.53 % (647366)CaDiCaL version: 2.1.3
% 61.72/10.53 % (647366)Termination reason: Refutation not found, incomplete strategy
% 61.72/10.53 % (647366)Time elapsed: 0.089 s
% 61.72/10.53 % (647366)Peak memory usage: 134 MB
% 61.72/10.53 % (647366)Instructions burned: 124 (million)
% 61.72/10.53 % (647366)------------------------------
% 61.72/10.53 % (647366)------------------------------
% 61.72/10.53 % (647368)dis-1010_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=occurrence:random_seed=958964635:i=2989:sd=3:ss=axioms:sgt=60_2935 on theBenchmark for (2935ds/2989Mi)
% 61.72/10.53 [W927 11:21:09.405680765 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.
% 61.72/10.53 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 61.72/10.53 [W927 11:21:09.405707456 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.
% 61.72/10.53 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 67.59/11.23 [W927 11:21:09.405730042 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.
% 67.59/11.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 67.59/11.23 [W927 11:21:09.405746379 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.
% 67.59/11.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 67.59/11.23 [W927 11:21:09.405760376 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.
% 67.59/11.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 67.59/11.23 [W927 11:21:09.405765702 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.
% 67.59/11.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 67.59/11.23 [W927 11:21:09.405778728 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.
% 67.59/11.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 67.59/11.23 [W927 11:21:09.405784175 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.
% 67.59/11.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 67.59/11.23 [W927 11:21:09.405797271 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.
% 67.59/11.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 67.59/11.23 [W927 11:21:09.405802764 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.
% 67.59/11.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 67.59/11.23 [W927 11:21:09.405817179 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.
% 67.59/11.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 67.59/11.23 [W927 11:21:09.405822806 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.
% 67.59/11.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 67.59/11.23 % (647338)Instruction limit reached!
% 67.59/11.23 % (647338)------------------------------
% 67.59/11.23 % (647338)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 67.59/11.23 % (647338)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.59/11.23 % (647338)CaDiCaL version: 2.1.3
% 67.59/11.23 % (647338)Termination reason: Instruction limit
% 67.59/11.23 % (647338)Termination phase: Saturation
% 67.59/11.23 % (647338)Time elapsed: 4.901 s
% 67.59/11.23 % (647338)Peak memory usage: 809 MB
% 67.59/11.23 % (647338)Instructions burned: 5208 (million)
% 67.59/11.23 % (647368)Refutation not found, incomplete strategy
% 67.59/11.23 % (647368)------------------------------
% 67.59/11.23 % (647368)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 67.59/11.23 % (647368)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.59/11.23 % (647368)CaDiCaL version: 2.1.3
% 67.59/11.23 % (647368)Termination reason: Refutation not found, incomplete strategy
% 67.59/11.23 % (647368)Time elapsed: 0.669 s
% 67.59/11.26 % (647368)Peak memory usage: 240 MB
% 67.59/11.26 % (647368)Instructions burned: 1393 (million)
% 67.59/11.26 % (647370)dis+1011_1_ncem=casc2026/models/loop5.pt:sil=8000:tgt=full:npcc=on:bsd=on:sp=const_min:spb=goal_then_units:lcm=predicate:urr=ec_only:s2agt=16:random_seed=3481801899:i=1997:bd=preordered:av=off:gtg=all:gsp=on_2927 on theBenchmark for (2927ds/1997Mi)
% 67.59/11.26 % (647368)------------------------------
% 67.59/11.26 % (647368)------------------------------
% 67.59/11.26 % (647372)lrs-1010_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:drc=off:sp=unary_frequency:urr=ec_only:fd=preordered:random_seed=324849411:i=2088:bd=preordered:av=off_2925 on theBenchmark for (2925ds/2088Mi)
% 67.59/11.26 % (647370)Instruction limit reached!
% 67.59/11.26 % (647370)------------------------------
% 67.59/11.26 % (647370)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 67.59/11.26 % (647370)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.59/11.26 % (647370)CaDiCaL version: 2.1.3
% 67.59/11.26 % (647370)Termination reason: Instruction limit
% 67.59/11.26 % (647370)Termination phase: Saturation
% 67.59/11.26 % (647370)Time elapsed: 1.271 s
% 67.59/11.26 % (647370)Peak memory usage: 243 MB
% 67.59/11.26 % (647370)Instructions burned: 1998 (million)
% 67.59/11.26 % (647372)Instruction limit reached!
% 67.59/11.26 % (647372)------------------------------
% 67.59/11.26 % (647372)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 67.59/11.26 % (647372)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.59/11.26 % (647372)CaDiCaL version: 2.1.3
% 67.59/11.26 % (647372)Termination reason: Instruction limit
% 67.59/11.26 % (647372)Termination phase: Saturation
% 67.59/11.26 % (647372)Time elapsed: 1.105 s
% 67.59/11.26 % (647372)Peak memory usage: 422 MB
% 67.59/11.26 % (647372)Instructions burned: 2094 (million)
% 67.59/11.26 % (647375)lrs-1011_32:1_to=lpo:sil=32000:tgt=ground:sos=on:spb=goal_then_units:acc=on:random_seed=1609782100:i=433:bd=preordered_2912 on theBenchmark for (2912ds/433Mi)
% 67.59/11.26 % (647374)lrs+1010_64:1_anc=all:to=lpo:sil=16000:fde=none:sp=const_frequency:urr=full:sac=on:random_seed=1285957623:i=1098:nicw=on_2912 on theBenchmark for (2912ds/1098Mi)
% 67.59/11.26 % (647375)Instruction limit reached!
% 67.59/11.26 % (647375)------------------------------
% 67.59/11.26 % (647375)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 67.59/11.26 % (647375)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.59/11.26 % (647375)CaDiCaL version: 2.1.3
% 67.59/11.26 % (647375)Termination reason: Instruction limit
% 67.59/11.26 % (647375)Termination phase: Saturation
% 67.59/11.26 % (647375)Time elapsed: 0.175 s
% 67.59/11.26 % (647375)Peak memory usage: 139 MB
% 67.59/11.26 % (647375)Instructions burned: 435 (million)
% 67.59/11.26 % (647378)lrs+1002_1_ncem=casc2026/models/loop3.pt:sil=32000:npcc=on:prc=on:etr=on:spb=goal:flr=on:random_seed=2304711379:st=5.37:cond=on:i=2942:s2at=20:aac=none:fgj=on:bs=on:gtg=exists_sym:ss=axioms:er=filter:sgt=16_2909 on theBenchmark for (2909ds/2942Mi)
% 67.59/11.26 % (647374)Instruction limit reached!
% 67.59/11.26 % (647374)------------------------------
% 67.59/11.26 % (647374)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 67.59/11.26 % (647374)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.59/11.26 % (647374)CaDiCaL version: 2.1.3
% 67.59/11.26 % (647374)Termination reason: Instruction limit
% 67.59/11.26 % (647374)Termination phase: Saturation
% 67.59/11.26 % (647374)Time elapsed: 0.725 s
% 67.59/11.26 % (647374)Peak memory usage: 150 MB
% 67.59/11.26 % (647374)Instructions burned: 1098 (million)
% 67.59/11.26 [W927 11:21:12.057471973 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.
% 67.59/11.26 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 67.59/11.26 [W927 11:21:12.057513008 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.
% 67.59/11.26 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 67.59/11.26 [W927 11:21:12.057534382 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.
% 77.56/12.78 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 77.56/12.78 [W927 11:21:12.057540831 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.
% 77.56/12.78 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 77.56/12.78 [W927 11:21:12.057554472 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.
% 77.56/12.78 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 77.56/12.78 [W927 11:21:12.057572685 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.
% 77.56/12.78 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 77.56/12.78 [W927 11:21:12.057586261 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.
% 77.56/12.78 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 77.56/12.78 [W927 11:21:12.057591599 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.
% 77.56/12.78 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 77.56/12.78 [W927 11:21:12.057604314 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.
% 77.56/12.78 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 77.56/12.78 [W927 11:21:12.057609754 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.
% 77.56/12.78 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 77.56/12.78 [W927 11:21:12.057623186 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.
% 77.56/12.78 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 77.56/12.78 [W927 11:21:12.057628592 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.
% 77.56/12.78 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 77.56/12.78 % (647380)lrs+35_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=reverse_arity:urr=full:rp=on:br=off:random_seed=3930459214:i=6922:s2at=5:sd=3:bd=all:ss=axioms:er=known:sgt=32_2903 on theBenchmark for (2903ds/6922Mi)
% 77.56/12.78 % (647378)Refutation not found, incomplete strategy
% 77.56/12.78 % (647378)------------------------------
% 77.56/12.78 % (647378)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 77.56/12.78 % (647378)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 77.56/12.78 % (647378)CaDiCaL version: 2.1.3
% 77.56/12.78 % (647378)Termination reason: Refutation not found, incomplete strategy
% 77.56/12.78 % (647378)Time elapsed: 0.694 s
% 77.56/12.78 % (647378)Peak memory usage: 181 MB
% 77.56/12.78 % (647378)Instructions burned: 1817 (million)
% 77.56/12.78 % (647378)------------------------------
% 77.56/12.78 % (647378)------------------------------
% 77.56/12.78 % (647382)dis+10_5:1_sil=8000:tgt=full:plsq=on:plsqc=1:plsqr=32,1:urr=on:fd=off:nwc=0.5:br=off:slsqc=3:slsq=on:random_seed=4170119102:s2a=on:i=596:s2at=2.3:gtgl=5:gtg=all:sup=off_2899 on theBenchmark for (2899ds/596Mi)
% 77.56/12.78 % (647382)Instruction limit reached!
% 77.56/12.78 % (647382)------------------------------
% 77.56/12.78 % (647382)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 57.70/13.67 % (647382)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.70/13.67 % (647382)CaDiCaL version: 2.1.3
% 57.70/13.67 % (647382)Termination reason: Instruction limit
% 57.70/13.67 % (647382)Termination phase: SInE selection
% 57.70/13.67 % (647382)Time elapsed: 0.170 s
% 57.70/13.67 % (647382)Peak memory usage: 122 MB
% 57.70/13.67 % (647382)Instructions burned: 596 (million)
% 57.70/13.67 [W927 11:21:13.792424091 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.
% 57.70/13.67 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 57.70/13.67 [W927 11:21:13.792462201 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.
% 57.70/13.67 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 57.70/13.67 [W927 11:21:13.792505708 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.
% 57.70/13.67 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 57.70/13.67 [W927 11:21:13.792518298 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.
% 57.70/13.67 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 57.70/13.67 [W927 11:21:13.792546281 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.
% 57.70/13.67 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 57.70/13.67 [W927 11:21:13.792557398 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.
% 57.70/13.67 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 57.70/13.67 [W927 11:21:13.792584421 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.
% 57.70/13.67 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 57.70/13.67 [W927 11:21:13.792595575 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.
% 57.70/13.67 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 57.70/13.67 [W927 11:21:13.792622365 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.
% 57.70/13.67 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 57.70/13.67 [W927 11:21:13.792633552 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.
% 57.70/13.67 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 57.70/13.67 [W927 11:21:13.792660632 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.
% 57.70/13.67 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 57.70/13.67 [W927 11:21:13.792671688 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.
% 57.70/13.67 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 57.70/13.67 % (647384)lrs+21_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=non_intro:urr=on:fd=preordered:random_seed=1323472045:i=4123:kws=inv_frequency:bd=preordered:av=off:er=known_2896 on theBenchmark for (2896ds/4123Mi)
% 57.70/13.67 % (647380)Refutation not found, incomplete strategy
% 57.70/13.67 % (647380)------------------------------
% 57.70/13.67 % (647380)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 57.70/13.67 % (647380)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.70/13.67 % (647380)CaDiCaL version: 2.1.3
% 57.70/13.67 % (647380)Termination reason: Refutation not found, incomplete strategy
% 57.70/13.67 % (647380)Time elapsed: 1.088 s
% 57.70/13.67 % (647380)Peak memory usage: 253 MB
% 57.70/13.67 % (647380)Instructions burned: 1463 (million)
% 57.70/13.67 % (647380)------------------------------
% 57.70/13.67 % (647380)------------------------------
% 57.70/13.67 % (647386)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=3350416037:i=16411:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2888 on theBenchmark for (2888ds/16411Mi)
% 57.70/13.67 [W927 11:21:14.312677516 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.
% 57.70/13.67 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 57.70/13.67 [W927 11:21:14.312711523 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.
% 57.70/13.67 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 57.70/13.67 [W927 11:21:14.312748606 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.
% 57.70/13.67 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 57.70/13.67 [W927 11:21:14.312760616 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.
% 57.70/13.67 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 57.70/13.67 [W927 11:21:14.312787406 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.
% 57.70/13.67 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 57.70/13.67 [W927 11:21:14.312798553 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.
% 57.70/13.67 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 57.70/13.67 [W927 11:21:14.312826116 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.
% 57.70/13.67 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 57.70/13.67 [W927 11:21:14.312837830 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.
% 57.70/13.67 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 57.70/13.67 [W927 11:21:14.312863343 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.
% 57.70/13.67 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 57.70/13.67 [W927 11:21:14.312874286 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.
% 84.88/13.89 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 84.88/13.89 [W927 11:21:14.312900393 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.
% 84.88/13.89 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 84.88/13.89 [W927 11:21:14.312910403 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.
% 84.88/13.89 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 84.88/13.89 % (647356)Instruction limit reached!
% 84.88/13.89 % (647356)------------------------------
% 84.88/13.89 % (647356)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 84.88/13.89 % (647356)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 84.88/13.89 % (647356)CaDiCaL version: 2.1.3
% 84.88/13.89 % (647356)Termination reason: Instruction limit
% 84.88/13.89 % (647356)Termination phase: Saturation
% 84.88/13.89 % (647356)Time elapsed: 7.901 s
% 84.88/13.89 % (647356)Peak memory usage: 769 MB
% 84.88/13.89 % (647356)Instructions burned: 10311 (million)
% 84.88/13.89 % (647388)lrs+0_1_ncem=casc2026/models/loop1.pt:sil=8000:tgt=full:npcc=on:sp=reverse_frequency:gs=on:random_seed=3812398467:i=1670:kws=inv_precedence:bd=all:av=off:gtg=exists_all_2878 on theBenchmark for (2878ds/1670Mi)
% 84.88/13.89 % (647305)First to succeed.
% 84.88/13.89 % (647305)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-647299"
% 84.88/13.89 % (647386)Refutation not found, incomplete strategy
% 84.88/13.89 % (647386)------------------------------
% 84.88/13.89 % (647386)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 84.88/13.89 % (647386)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 84.88/13.89 % (647386)CaDiCaL version: 2.1.3
% 84.88/13.89 % (647386)Termination reason: Refutation not found, incomplete strategy
% 84.88/13.89 % (647386)Time elapsed: 1.056 s
% 84.88/13.89 % (647386)Peak memory usage: 235 MB
% 84.88/13.89 % (647386)Instructions burned: 1418 (million)
% 84.88/13.89 % (647360)Instruction limit reached!
% 84.88/13.89 % (647360)------------------------------
% 84.88/13.89 % (647360)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 84.88/13.89 % (647360)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 84.88/13.89 % (647360)CaDiCaL version: 2.1.3
% 84.88/13.89 % (647360)Termination reason: Instruction limit
% 84.88/13.89 % (647360)Termination phase: Saturation
% 84.88/13.89 % (647360)Time elapsed: 6.962 s
% 84.88/13.89 % (647360)Peak memory usage: 489 MB
% 84.88/13.89 % (647360)Instructions burned: 8480 (million)
% 84.88/13.89 % (647386)------------------------------
% 84.88/13.89 % (647386)------------------------------
% 84.88/13.89 % (647390)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:prc=on:drc=off:fde=unused:sp=reverse_frequency:updr=off:random_seed=873275070:st=3:cond=fast:i=1722:sd=2:ss=included:fsd=on_2874 on theBenchmark for (2874ds/1722Mi)
% 84.88/13.89 % (647305)Refutation found. Thanks to Tanya!
% 84.88/13.89 % SZS status Unsatisfiable for theBenchmark
% 84.88/13.89 % SZS output start Proof for theBenchmark
% See solution above
% 84.88/13.89 % (647305)------------------------------
% 84.88/13.89 % (647305)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 84.88/13.89 % (647305)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 84.88/13.89 % (647305)CaDiCaL version: 2.1.3
% 84.88/13.89 % (647305)Termination reason: Refutation
% 84.88/13.89 % (647305)Time elapsed: 11.190 s
% 84.88/13.89 % (647305)Peak memory usage: 768 MB
% 84.88/13.89 % (647305)Instructions burned: 15376 (million)
% 84.88/13.89 % (647305)------------------------------
% 84.88/13.89 % (647305)------------------------------
% 84.88/13.89 % (647299)Success in time 12.785 s
% 84.88/13.89 % Vampire exiting
%------------------------------------------------------------------------------