%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : HWV096-1 : TPTP v9.3.1. Released v6.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n007.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:42:36 AM UTC 2026
% Result : Unsatisfiable 0.29s 20.33s
% Output : Refutation 0.29s
% Verified :
% SZS Type : Derivation
% Derivation depth : 0
% Number of leaves : 1
% Syntax : Number of formulae : 1 ( 1 unt; 0 def)
% Number of atoms : 1 ( 0 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 0 ( 0 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 1 ( 1 avg)
% Maximal term depth : 0 ( 0 avg)
% Number of predicates : 1 ( 0 usr; 1 prp; 0-0 aty)
% Number of functors : 0 ( 0 usr; 0 con; --- aty)
% Number of variables : 0 ( 0 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f3033,negated_conjecture,
$false,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u1693507) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : HWV096-1 : TPTP v9.3.1. Released v6.1.0.
% 0.11/0.15 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.20/0.50 % Computer : n007.cluster.edu
% 0.20/0.50 % Model : x86_64 x86_64
% 0.20/0.50 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.20/0.50 % Memory : 8046.5625MB
% 0.20/0.50 % OS : Linux 6.8.0-71-generic
% 0.20/0.50 % CPULimit : 300
% 0.20/0.50 % WCLimit : 300
% 0.20/0.50 % DateTime : Sun Sep 27 11:28:13 UTC 2026
% 0.20/0.50 % CPUTime :
% 0.20/0.50 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.26/0.58 Running first-order theorem proving
% 0.26/0.58 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
% 20.00/10.05 % (1259943)Input is clausal, will run a generic CNF schedule.
% 20.00/10.05 % (1259949)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=3855210317:i=140167_2927 on theBenchmark for (2927ds/140167Mi)
% 20.00/10.05 % (1259950)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=468675880:i=132376:av=off_2927 on theBenchmark for (2927ds/132376Mi)
% 20.00/10.05 % (1259951)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=1757245760:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2927 on theBenchmark for (2927ds/137899Mi)
% 20.00/10.05 % (1259952)lrs+10_1_sil=8000:sp=occurrence:random_seed=3477135664:i=107:sd=3:ss=axioms:sgt=8_2927 on theBenchmark for (2927ds/107Mi)
% 20.00/10.05 % (1259954)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2007505841:s2a=on:i=180:gtg=position_2927 on theBenchmark for (2927ds/180Mi)
% 20.00/10.05 % (1259953)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=3239632323:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2927 on theBenchmark for (2927ds/114Mi)
% 20.00/10.05 % (1259955)dis-21_1_sil=8000:lcm=predicate:random_seed=1633762235:st=5:avsq=on:i=117:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2927 on theBenchmark for (2927ds/117Mi)
% 20.00/10.05 % (1259952)Instruction limit reached!
% 20.00/10.05 % (1259952)------------------------------
% 20.00/10.05 % (1259952)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.00/10.05 % (1259952)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.00/10.05 % (1259952)CaDiCaL version: 2.1.3
% 20.00/10.05 % (1259952)Termination reason: Instruction limit
% 20.00/10.05 % (1259952)Termination phase: SInE selection
% 20.00/10.05 % (1259952)Time elapsed: 0.051 s
% 20.00/10.05 % (1259952)Peak memory usage: 335 MB
% 20.00/10.05 % (1259952)Instructions burned: 109 (million)
% 20.00/10.05 % (1259953)Instruction limit reached!
% 20.00/10.05 % (1259953)------------------------------
% 20.00/10.05 % (1259953)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.00/10.05 % (1259953)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.00/10.05 % (1259953)CaDiCaL version: 2.1.3
% 20.00/10.05 % (1259953)Termination reason: Instruction limit
% 20.00/10.05 % (1259953)Termination phase: SInE selection
% 20.00/10.05 % (1259953)Time elapsed: 0.054 s
% 20.00/10.05 % (1259953)Peak memory usage: 335 MB
% 20.00/10.05 % (1259953)Instructions burned: 115 (million)
% 20.00/10.05 % (1259955)Instruction limit reached!
% 20.00/10.05 % (1259955)------------------------------
% 20.00/10.05 % (1259955)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.00/10.05 % (1259955)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.00/10.05 % (1259955)CaDiCaL version: 2.1.3
% 20.00/10.05 % (1259955)Termination reason: Instruction limit
% 20.00/10.05 % (1259955)Termination phase: SInE selection
% 20.00/10.05 % (1259955)Time elapsed: 0.057 s
% 20.00/10.05 % (1259955)Peak memory usage: 335 MB
% 20.00/10.05 % (1259955)Instructions burned: 119 (million)
% 20.00/10.05 % (1259954)Instruction limit reached!
% 20.00/10.05 % (1259954)------------------------------
% 20.00/10.05 % (1259954)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.00/10.05 % (1259954)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.00/10.05 % (1259954)CaDiCaL version: 2.1.3
% 20.00/10.05 % (1259954)Termination reason: Instruction limit
% 20.00/10.05 % (1259954)Termination phase: Property scanning
% 20.00/10.05 % (1259954)Time elapsed: 0.152 s
% 20.00/10.05 % (1259954)Peak memory usage: 336 MB
% 20.00/10.05 % (1259954)Instructions burned: 181 (million)
% 20.00/10.05 % (1259963)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=1343521825:i=143:sd=2:aac=none:ss=axioms:sgt=16_2925 on theBenchmark for (2925ds/143Mi)
% 20.00/10.05 % (1259964)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=3111391513:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2925 on theBenchmark for (2925ds/189Mi)
% 20.00/10.05 % (1259965)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=1958486953:st=4:i=219:sd=3:ss=axioms_2925 on theBenchmark for (2925ds/219Mi)
% 20.00/10.05 % (1259963)Instruction limit reached!
% 20.00/10.05 % (1259963)------------------------------
% 20.00/10.05 % (1259963)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.88/11.21 % (1259963)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.88/11.21 % (1259963)CaDiCaL version: 2.1.3
% 28.88/11.21 % (1259963)Termination reason: Instruction limit
% 28.88/11.21 % (1259963)Termination phase: SInE selection
% 28.88/11.21 % (1259963)Time elapsed: 0.066 s
% 28.88/11.21 % (1259963)Peak memory usage: 335 MB
% 28.88/11.21 % (1259963)Instructions burned: 145 (million)
% 28.88/11.21 % (1259964)Instruction limit reached!
% 28.88/11.21 % (1259964)------------------------------
% 28.88/11.21 % (1259964)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.88/11.21 % (1259964)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.88/11.21 % (1259964)CaDiCaL version: 2.1.3
% 28.88/11.21 % (1259964)Termination reason: Instruction limit
% 28.88/11.21 % (1259964)Termination phase: SInE selection
% 28.88/11.21 % (1259964)Time elapsed: 0.085 s
% 28.88/11.21 % (1259964)Peak memory usage: 335 MB
% 28.88/11.21 % (1259964)Instructions burned: 190 (million)
% 28.88/11.21 % (1259966)lrs+10_64_to=lpo:sil=8000:random_seed=3495738134:i=126:bd=preordered_2924 on theBenchmark for (2924ds/126Mi)
% 28.88/11.21 % (1259965)Instruction limit reached!
% 28.88/11.21 % (1259965)------------------------------
% 28.88/11.21 % (1259965)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.88/11.21 % (1259965)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.88/11.21 % (1259965)CaDiCaL version: 2.1.3
% 28.88/11.21 % (1259965)Termination reason: Instruction limit
% 28.88/11.21 % (1259965)Termination phase: SInE selection
% 28.88/11.21 % (1259965)Time elapsed: 0.101 s
% 28.88/11.21 % (1259965)Peak memory usage: 335 MB
% 28.88/11.21 % (1259965)Instructions burned: 220 (million)
% 28.88/11.21 % (1259970)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=4043585819:avsq=on:i=194:fgj=on:bd=preordered_2923 on theBenchmark for (2923ds/194Mi)
% 28.88/11.21 % (1259971)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=2664652415:i=157:gtg=all_2923 on theBenchmark for (2923ds/157Mi)
% 28.88/11.21 % (1259973)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=3994100933:i=3394:sd=4:ss=included:sgt=64_2922 on theBenchmark for (2922ds/3394Mi)
% 28.88/11.21 % (1259966)Instruction limit reached!
% 28.88/11.21 % (1259966)------------------------------
% 28.88/11.21 % (1259966)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.88/11.21 % (1259966)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.88/11.21 % (1259966)CaDiCaL version: 2.1.3
% 28.88/11.21 % (1259966)Termination reason: Instruction limit
% 28.88/11.21 % (1259966)Termination phase: Unused predicate definition removal
% 28.88/11.21 % (1259966)Time elapsed: 0.201 s
% 28.88/11.21 % (1259966)Peak memory usage: 381 MB
% 28.88/11.21 % (1259966)Instructions burned: 126 (million)
% 28.88/11.21 % (1259971)Instruction limit reached!
% 28.88/11.21 % (1259971)------------------------------
% 28.88/11.21 % (1259971)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.88/11.21 % (1259971)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.88/11.21 % (1259971)CaDiCaL version: 2.1.3
% 28.88/11.21 % (1259971)Termination reason: Instruction limit
% 28.88/11.21 % (1259971)Termination phase: Property scanning
% 28.88/11.21 % (1259971)Time elapsed: 0.146 s
% 28.88/11.21 % (1259971)Peak memory usage: 336 MB
% 28.88/11.21 % (1259971)Instructions burned: 158 (million)
% 28.88/11.21 % (1259977)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=193611335:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2920 on theBenchmark for (2920ds/106Mi)
% 28.88/11.21 % (1259970)Instruction limit reached!
% 28.88/11.21 % (1259970)------------------------------
% 28.88/11.21 % (1259970)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.88/11.21 % (1259970)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.88/11.21 % (1259970)CaDiCaL version: 2.1.3
% 28.88/11.21 % (1259970)Termination reason: Instruction limit
% 28.88/11.21 % (1259970)Termination phase: Equality resolution with deletion
% 28.88/11.21 % (1259970)Time elapsed: 0.264 s
% 28.88/11.21 % (1259970)Peak memory usage: 383 MB
% 28.88/11.21 % (1259970)Instructions burned: 194 (million)
% 28.88/11.21 % (1259977)Instruction limit reached!
% 28.88/11.21 % (1259977)------------------------------
% 28.88/11.21 % (1259977)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.88/11.21 % (1259977)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.83/12.28 % (1259977)CaDiCaL version: 2.1.3
% 35.83/12.28 % (1259977)Termination reason: Instruction limit
% 35.83/12.28 % (1259977)Termination phase: SInE selection
% 35.83/12.28 % (1259977)Time elapsed: 0.051 s
% 35.83/12.28 % (1259977)Peak memory usage: 335 MB
% 35.83/12.28 % (1259977)Instructions burned: 106 (million)
% 35.83/12.28 % (1259978)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=1597850800:i=107_2920 on theBenchmark for (2920ds/107Mi)
% 35.83/12.28 % (1259980)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=2074478421:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2919 on theBenchmark for (2919ds/242Mi)
% 35.83/12.28 % (1259982)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=763607253:cond=fast:i=5208:av=off_2918 on theBenchmark for (2918ds/5208Mi)
% 35.83/12.28 % (1259978)Instruction limit reached!
% 35.83/12.28 % (1259978)------------------------------
% 35.83/12.28 % (1259978)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.83/12.28 % (1259978)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.83/12.28 % (1259978)CaDiCaL version: 2.1.3
% 35.83/12.28 % (1259978)Termination reason: Instruction limit
% 35.83/12.28 % (1259978)Termination phase: Unused predicate definition removal
% 35.83/12.28 % (1259978)Time elapsed: 0.167 s
% 35.83/12.28 % (1259978)Peak memory usage: 379 MB
% 35.83/12.28 % (1259978)Instructions burned: 107 (million)
% 35.83/12.28 % (1259980)Instruction limit reached!
% 35.83/12.28 % (1259980)------------------------------
% 35.83/12.28 % (1259980)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.83/12.28 % (1259980)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.83/12.28 % (1259980)CaDiCaL version: 2.1.3
% 35.83/12.28 % (1259980)Termination reason: Instruction limit
% 35.83/12.28 % (1259980)Termination phase: Property scanning
% 35.83/12.28 % (1259980)Time elapsed: 0.175 s
% 35.83/12.28 % (1259980)Peak memory usage: 336 MB
% 35.83/12.28 % (1259980)Instructions burned: 242 (million)
% 35.83/12.28 % (1259985)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=915657250:i=134:sd=2:doe=on:ss=axioms:sgt=14_2917 on theBenchmark for (2917ds/134Mi)
% 35.83/12.28 % (1259985)Instruction limit reached!
% 35.83/12.28 % (1259985)------------------------------
% 35.83/12.28 % (1259985)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.83/12.28 % (1259985)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.83/12.28 % (1259985)CaDiCaL version: 2.1.3
% 35.83/12.28 % (1259985)Termination reason: Instruction limit
% 35.83/12.28 % (1259985)Termination phase: SInE selection
% 35.83/12.28 % (1259985)Time elapsed: 0.062 s
% 35.83/12.28 % (1259985)Peak memory usage: 335 MB
% 35.83/12.28 % (1259985)Instructions burned: 136 (million)
% 35.83/12.28 % (1259986)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=1949818153:i=499:bd=all_2916 on theBenchmark for (2916ds/499Mi)
% 35.83/12.28 % (1259988)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=2526348381:i=191:fgj=on:bd=all_2915 on theBenchmark for (2915ds/191Mi)
% 35.83/12.28 % (1259988)Instruction limit reached!
% 35.83/12.28 % (1259988)------------------------------
% 35.83/12.28 % (1259988)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.83/12.28 % (1259988)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.83/12.28 % (1259988)CaDiCaL version: 2.1.3
% 35.83/12.28 % (1259988)Termination reason: Instruction limit
% 35.83/12.28 % (1259988)Termination phase: Equality resolution with deletion
% 35.83/12.28 % (1259988)Time elapsed: 0.244 s
% 35.83/12.28 % (1259988)Peak memory usage: 383 MB
% 35.83/12.28 % (1259988)Instructions burned: 191 (million)
% 35.83/12.28 % (1259986)Instruction limit reached!
% 35.83/12.28 % (1259986)------------------------------
% 35.83/12.28 % (1259986)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.83/12.28 % (1259986)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.83/12.28 % (1259986)CaDiCaL version: 2.1.3
% 35.83/12.28 % (1259986)Termination reason: Instruction limit
% 35.83/12.28 % (1259986)Termination phase: Property scanning
% 35.83/12.28 % (1259986)Time elapsed: 0.462 s
% 35.83/12.28 % (1259986)Peak memory usage: 384 MB
% 35.83/12.28 % (1259986)Instructions burned: 500 (million)
% 35.83/12.28 % (1259991)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=1687378068:i=264:kws=precedence:fsr=off_2911 on theBenchmark for (2911ds/264Mi)
% 59.41/15.57 % (1259973)Instruction limit reached!
% 59.41/15.57 % (1259973)------------------------------
% 59.41/15.57 % (1259973)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 59.41/15.57 % (1259993)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=3918954356:cond=on:i=156:bs=on:gtg=exists_all:er=known_2909 on theBenchmark for (2909ds/156Mi)
% 59.41/15.57 % (1259973)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.41/15.57 % (1259973)CaDiCaL version: 2.1.3
% 59.41/15.57 % (1259973)Termination reason: Instruction limit
% 59.41/15.57 % (1259973)Termination phase: SInE selection
% 59.41/15.57 % (1259973)Time elapsed: 1.294 s
% 59.41/15.57 % (1259973)Peak memory usage: 353 MB
% 59.41/15.57 % (1259973)Instructions burned: 3395 (million)
% 59.41/15.57 % (1259993)Instruction limit reached!
% 59.41/15.57 % (1259993)------------------------------
% 59.41/15.57 % (1259993)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 59.41/15.57 % (1259993)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.41/15.57 % (1259993)CaDiCaL version: 2.1.3
% 59.41/15.57 % (1259993)Termination reason: Instruction limit
% 59.41/15.57 % (1259993)Termination phase: Property scanning
% 59.41/15.57 % (1259993)Time elapsed: 0.144 s
% 59.41/15.57 % (1259993)Peak memory usage: 336 MB
% 59.41/15.57 % (1259993)Instructions burned: 159 (million)
% 59.41/15.57 % (1259995)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=403543114:i=3256:kws=precedence:bd=preordered:av=off_2908 on theBenchmark for (2908ds/3256Mi)
% 59.41/15.57 % (1259991)Instruction limit reached!
% 59.41/15.57 % (1259991)------------------------------
% 59.41/15.57 % (1259991)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 59.41/15.57 % (1259991)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.41/15.57 % (1259991)CaDiCaL version: 2.1.3
% 59.41/15.57 % (1259991)Termination reason: Instruction limit
% 59.41/15.57 % (1259991)Termination phase: Property scanning
% 59.41/15.57 % (1259991)Time elapsed: 0.365 s
% 59.41/15.57 % (1259991)Peak memory usage: 384 MB
% 59.41/15.57 % (1259991)Instructions burned: 266 (million)
% 59.41/15.57 % (1259997)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=2211371089:i=537:av=off:ss=included_2906 on theBenchmark for (2906ds/537Mi)
% 59.41/15.57 % (1259998)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=2765966964:i=180:bd=preordered:av=off_2905 on theBenchmark for (2905ds/180Mi)
% 59.41/15.57 % (1259997)Instruction limit reached!
% 59.41/15.57 % (1259997)------------------------------
% 59.41/15.57 % (1259997)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 59.41/15.57 % (1259997)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.41/15.57 % (1259997)CaDiCaL version: 2.1.3
% 59.41/15.57 % (1259997)Termination reason: Instruction limit
% 59.41/15.57 % (1259997)Termination phase: SInE selection
% 59.41/15.57 % (1259997)Time elapsed: 0.222 s
% 59.41/15.57 % (1259997)Peak memory usage: 335 MB
% 59.41/15.57 % (1259997)Instructions burned: 538 (million)
% 59.41/15.57 % (1259998)Instruction limit reached!
% 59.41/15.57 % (1259998)------------------------------
% 59.41/15.57 % (1259998)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 59.41/15.57 % (1259998)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.41/15.57 % (1259998)CaDiCaL version: 2.1.3
% 59.41/15.57 % (1259998)Termination reason: Instruction limit
% 59.41/15.57 % (1259998)Termination phase: Equality resolution with deletion
% 59.41/15.57 % (1259998)Time elapsed: 0.240 s
% 59.41/15.57 % (1259998)Peak memory usage: 383 MB
% 59.41/15.57 % (1259998)Instructions burned: 181 (million)
% 59.41/15.57 % (1260001)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=2983186498:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2902 on theBenchmark for (2902ds/10307Mi)
% 59.41/15.57 % (1260002)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=880420130:i=412:gtgl=4:gtg=exists_all_2901 on theBenchmark for (2901ds/412Mi)
% 59.41/15.57 % (1260002)Instruction limit reached!
% 59.41/15.57 % (1260002)------------------------------
% 59.41/15.57 % (1260002)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 72.17/17.32 % (1260002)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 72.17/17.32 % (1260002)CaDiCaL version: 2.1.3
% 72.17/17.32 % (1260002)Termination reason: Instruction limit
% 72.17/17.32 % (1260002)Termination phase: Property scanning
% 72.17/17.32 % (1260002)Time elapsed: 0.241 s
% 72.17/17.32 % (1260002)Peak memory usage: 336 MB
% 72.17/17.32 % (1260002)Instructions burned: 412 (million)
% 72.17/17.32 % (1260005)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=742996236:s2pl=no:i=8478:s2at=4:nm=6_2897 on theBenchmark for (2897ds/8478Mi)
% 72.17/17.32 % (1259982)Instruction limit reached!
% 72.17/17.32 % (1259982)------------------------------
% 72.17/17.32 % (1259982)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 72.17/17.32 % (1259982)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 72.17/17.32 % (1259982)CaDiCaL version: 2.1.3
% 72.17/17.32 % (1259982)Termination reason: Instruction limit
% 72.17/17.32 % (1259982)Termination phase: Property scanning
% 72.17/17.32 % (1259982)Time elapsed: 2.147 s
% 72.17/17.32 % (1259982)Peak memory usage: 390 MB
% 72.17/17.32 % (1259982)Instructions burned: 5209 (million)
% 72.17/17.32 % (1260007)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=3687543902:s2a=on:i=303:s2at=2:sd=1:kws=inv_arity:bs=on:ins=10:fdi=1024:sup=off:ss=included_2895 on theBenchmark for (2895ds/303Mi)
% 72.17/17.32 % (1259995)Instruction limit reached!
% 72.17/17.32 % (1259995)------------------------------
% 72.17/17.32 % (1259995)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 72.17/17.32 % (1259995)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 72.17/17.32 % (1259995)CaDiCaL version: 2.1.3
% 72.17/17.32 % (1259995)Termination reason: Instruction limit
% 72.17/17.32 % (1259995)Termination phase: Property scanning
% 72.17/17.32 % (1259995)Time elapsed: 1.290 s
% 72.17/17.32 % (1259995)Peak memory usage: 341 MB
% 72.17/17.32 % (1259995)Instructions burned: 3257 (million)
% 72.17/17.32 % (1260007)Instruction limit reached!
% 72.17/17.32 % (1260007)------------------------------
% 72.17/17.32 % (1260007)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 72.17/17.32 % (1260007)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 72.17/17.32 % (1260007)CaDiCaL version: 2.1.3
% 72.17/17.32 % (1260007)Termination reason: Instruction limit
% 72.17/17.32 % (1260007)Termination phase: SInE selection
% 72.17/17.32 % (1260007)Time elapsed: 0.130 s
% 72.17/17.32 % (1260007)Peak memory usage: 335 MB
% 72.17/17.32 % (1260007)Instructions burned: 305 (million)
% 72.17/17.32 % (1260009)lrs+10_1_to=lpo:sil=16000:fde=none:sos=on:urr=on:bsr=on:random_seed=1015259068:st=4:i=720:sd=3:fsr=off:ss=axioms_2893 on theBenchmark for (2893ds/720Mi)
% 72.17/17.32 % (1260010)lrs-20_1_to=lpo:sil=32000:tgt=ground:sp=reverse_frequency:spb=goal:urr=on:bsr=unit_only:nwc=1.5:random_seed=3821286471:i=598:bs=on:bd=preordered:av=off:ss=axioms_2892 on theBenchmark for (2892ds/598Mi)
% 72.17/17.32 % (1260009)Instruction limit reached!
% 72.17/17.32 % (1260009)------------------------------
% 72.17/17.32 % (1260009)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 72.17/17.32 % (1260009)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 72.17/17.32 % (1260009)CaDiCaL version: 2.1.3
% 72.17/17.32 % (1260009)Termination reason: Instruction limit
% 72.17/17.32 % (1260009)Termination phase: SInE selection
% 72.17/17.32 % (1260009)Time elapsed: 0.288 s
% 72.17/17.32 % (1260009)Peak memory usage: 335 MB
% 72.17/17.32 % (1260009)Instructions burned: 721 (million)
% 72.17/17.32 % (1260010)Instruction limit reached!
% 72.17/17.32 % (1260010)------------------------------
% 72.17/17.32 % (1260010)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 72.17/17.32 % (1260010)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 72.17/17.32 % (1260010)CaDiCaL version: 2.1.3
% 72.17/17.32 % (1260010)Termination reason: Instruction limit
% 72.17/17.32 % (1260010)Termination phase: SInE selection
% 72.17/17.32 % (1260010)Time elapsed: 0.243 s
% 72.17/17.32 % (1260010)Peak memory usage: 335 MB
% 72.17/17.32 % (1260010)Instructions burned: 598 (million)
% 72.17/17.32 % (1260013)dis-1010_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=occurrence:random_seed=3432491748:i=2989:sd=3:ss=axioms:sgt=60_2889 on theBenchmark for (2889ds/2989Mi)
% 72.17/17.32 % (1260014)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=1370845912:i=1997:bd=preordered:av=off:gtg=all:gsp=on_2888 on theBenchmark for (2888ds/1997Mi)
% 78.57/18.28 % (1260014)Instruction limit reached!
% 78.57/18.28 % (1260014)------------------------------
% 78.57/18.28 % (1260014)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 78.57/18.28 % (1260014)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 78.57/18.28 % (1260014)CaDiCaL version: 2.1.3
% 78.57/18.28 % (1260014)Termination reason: Instruction limit
% 78.57/18.28 % (1260014)Termination phase: Property scanning
% 78.57/18.28 % (1260014)Time elapsed: 0.809 s
% 78.57/18.28 % (1260014)Peak memory usage: 336 MB
% 78.57/18.28 % (1260014)Instructions burned: 1999 (million)
% 78.57/18.28 % (1260017)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=3939041473:i=2088:bd=preordered:av=off_2879 on theBenchmark for (2879ds/2088Mi)
% 78.57/18.28 % (1260013)Instruction limit reached!
% 78.57/18.28 % (1260013)------------------------------
% 78.57/18.28 % (1260013)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 78.57/18.28 % (1260013)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 78.57/18.28 % (1260013)CaDiCaL version: 2.1.3
% 78.57/18.28 % (1260013)Termination reason: Instruction limit
% 78.57/18.28 % (1260013)Termination phase: SInE selection
% 78.57/18.28 % (1260013)Time elapsed: 1.093 s
% 78.57/18.28 % (1260013)Peak memory usage: 340 MB
% 78.57/18.28 % (1260013)Instructions burned: 2990 (million)
% 78.57/18.28 % (1260019)lrs+1010_64:1_anc=all:to=lpo:sil=16000:fde=none:sp=const_frequency:urr=full:sac=on:random_seed=2559669042:i=1098:nicw=on_2876 on theBenchmark for (2876ds/1098Mi)
% 78.57/18.28 % (1260019)Instruction limit reached!
% 78.57/18.28 % (1260019)------------------------------
% 78.57/18.28 % (1260019)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 78.57/18.28 % (1260019)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 78.57/18.28 % (1260019)CaDiCaL version: 2.1.3
% 78.57/18.28 % (1260019)Termination reason: Instruction limit
% 78.57/18.28 % (1260019)Termination phase: Property scanning
% 78.57/18.28 % (1260019)Time elapsed: 0.685 s
% 78.57/18.28 % (1260019)Peak memory usage: 384 MB
% 78.57/18.28 % (1260019)Instructions burned: 1100 (million)
% 78.57/18.28 % (1260017)Instruction limit reached!
% 78.57/18.28 % (1260017)------------------------------
% 78.57/18.28 % (1260017)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 78.57/18.28 % (1260017)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 78.57/18.28 % (1260017)CaDiCaL version: 2.1.3
% 78.57/18.28 % (1260017)Termination reason: Instruction limit
% 78.57/18.28 % (1260017)Termination phase: Property scanning
% 78.57/18.28 % (1260017)Time elapsed: 1.021 s
% 78.57/18.28 % (1260017)Peak memory usage: 389 MB
% 78.57/18.28 % (1260017)Instructions burned: 2089 (million)
% 78.57/18.28 % (1260021)lrs-1011_32:1_to=lpo:sil=32000:tgt=ground:sos=on:spb=goal_then_units:acc=on:random_seed=3993216828:i=433:bd=preordered_2868 on theBenchmark for (2868ds/433Mi)
% 78.57/18.28 % (1260022)lrs+1002_1_ncem=casc2026/models/loop3.pt:sil=32000:npcc=on:prc=on:etr=on:spb=goal:flr=on:random_seed=2469362372:st=5.37:cond=on:i=2942:s2at=20:aac=none:fgj=on:bs=on:gtg=exists_sym:ss=axioms:er=filter:sgt=16_2867 on theBenchmark for (2867ds/2942Mi)
% 78.57/18.28 % (1260021)Instruction limit reached!
% 78.57/18.28 % (1260021)------------------------------
% 78.57/18.28 % (1260021)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 78.57/18.28 % (1260021)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 78.57/18.28 % (1260021)CaDiCaL version: 2.1.3
% 78.57/18.28 % (1260021)Termination reason: Instruction limit
% 78.57/18.28 % (1260021)Termination phase: Property scanning
% 78.57/18.28 % (1260021)Time elapsed: 0.460 s
% 78.57/18.28 % (1260021)Peak memory usage: 384 MB
% 78.57/18.28 % (1260021)Instructions burned: 435 (million)
% 78.57/18.28 % (1260025)lrs+35_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=reverse_arity:urr=full:rp=on:br=off:random_seed=1262958530:i=6922:s2at=5:sd=3:bd=all:ss=axioms:er=known:sgt=32_2861 on theBenchmark for (2861ds/6922Mi)
% 78.57/18.28 % (1260022)Instruction limit reached!
% 78.57/18.28 % (1260022)------------------------------
% 78.57/18.28 % (1260022)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 78.57/18.28 % (1260022)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 80.76/18.55 % (1260022)CaDiCaL version: 2.1.3
% 80.76/18.55 % (1260022)Termination reason: Instruction limit
% 80.76/18.55 % (1260022)Termination phase: SInE selection
% 80.76/18.55 % (1260022)Time elapsed: 1.133 s
% 80.76/18.55 % (1260022)Peak memory usage: 336 MB
% 80.76/18.55 % (1260022)Instructions burned: 2943 (million)
% 80.76/18.55 % (1260005)Instruction limit reached!
% 80.76/18.55 % (1260005)------------------------------
% 80.76/18.55 % (1260005)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 80.76/18.55 % (1260005)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 80.76/18.55 % (1260005)CaDiCaL version: 2.1.3
% 80.76/18.55 % (1260005)Termination reason: Instruction limit
% 80.76/18.55 % (1260005)Termination phase: Saturation
% 80.76/18.55 % (1260005)Time elapsed: 4.338 s
% 80.76/18.55 % (1260005)Peak memory usage: 711 MB
% 80.76/18.55 % (1260005)Instructions burned: 8479 (million)
% 80.76/18.55 % (1260027)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=63449776:s2a=on:i=596:s2at=2.3:gtgl=5:gtg=all:sup=off_2854 on theBenchmark for (2854ds/596Mi)
% 80.76/18.55 % (1260029)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=398138679:i=4123:kws=inv_frequency:bd=preordered:av=off:er=known_2852 on theBenchmark for (2852ds/4123Mi)
% 80.76/18.55 % (1260027)Instruction limit reached!
% 80.76/18.55 % (1260027)------------------------------
% 80.76/18.55 % (1260027)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 80.76/18.55 % (1260027)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 80.76/18.55 % (1260027)CaDiCaL version: 2.1.3
% 80.76/18.55 % (1260027)Termination reason: Instruction limit
% 80.76/18.55 % (1260027)Termination phase: Property scanning
% 80.76/18.55 % (1260027)Time elapsed: 0.313 s
% 80.76/18.55 % (1260027)Peak memory usage: 336 MB
% 80.76/18.55 % (1260027)Instructions burned: 596 (million)
% 80.76/18.55 % (1260031)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=882760750:i=16411:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2849 on theBenchmark for (2849ds/16411Mi)
% 80.76/18.55 [W927 11:28:30.899296966 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.
% 80.76/18.55 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 80.76/18.55 [W927 11:28:30.899344070 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.
% 80.76/18.55 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 80.76/18.55 [W927 11:28:30.899387670 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.
% 80.76/18.55 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 80.76/18.55 [W927 11:28:30.899401166 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.
% 80.76/18.55 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 80.76/18.55 [W927 11:28:30.899429040 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.
% 80.76/18.55 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 80.76/18.55 [W927 11:28:30.899441336 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.
% 80.76/18.55 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 80.76/18.55 [W927 11:28:30.899470723 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.
% 0.29/20.33 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 0.29/20.33 [W927 11:28:30.899482873 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.
% 0.29/20.33 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 0.29/20.33 [W927 11:28:30.899514783 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.
% 0.29/20.33 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 0.29/20.33 [W927 11:28:30.899525546 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.
% 0.29/20.33 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 0.29/20.33 [W927 11:28:30.899550060 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.
% 0.29/20.33 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 0.29/20.33 [W927 11:28:30.899560656 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.
% 0.29/20.33 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 0.29/20.33 % (1260001)Instruction limit reached!
% 0.29/20.33 % (1260001)------------------------------
% 0.29/20.33 % (1260001)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.29/20.33 % (1260001)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.29/20.33 % (1260001)CaDiCaL version: 2.1.3
% 0.29/20.33 % (1260001)Termination reason: Instruction limit
% 0.29/20.33 % (1260001)Termination phase: Saturation
% 0.29/20.33 % (1260001)Time elapsed: 6.727 s
% 0.29/20.33 % (1260001)Peak memory usage: 1113 MB
% 0.29/20.33 % (1260001)Instructions burned: 10307 (million)
% 0.29/20.33 % (1260029)Instruction limit reached!
% 0.29/20.33 % (1260029)------------------------------
% 0.29/20.33 % (1260029)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.29/20.33 % (1260029)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.29/20.33 % (1260029)CaDiCaL version: 2.1.3
% 0.29/20.33 % (1260029)Termination reason: Instruction limit
% 0.29/20.33 % (1260029)Termination phase: Property scanning
% 0.29/20.33 % (1260029)Time elapsed: 1.821 s
% 0.29/20.33 % (1260029)Peak memory usage: 390 MB
% 0.29/20.33 % (1260029)Instructions burned: 4123 (million)
% 0.29/20.33 % (1260033)lrs+0_1_ncem=casc2026/models/loop1.pt:sil=8000:tgt=full:npcc=on:sp=reverse_frequency:gs=on:random_seed=2656023357:i=1670:kws=inv_precedence:bd=all:av=off:gtg=exists_all_2833 on theBenchmark for (2833ds/1670Mi)
% 0.29/20.33 % (1260034)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=3604937510:st=3:cond=fast:i=1722:sd=2:ss=included:fsd=on_2832 on theBenchmark for (2832ds/1722Mi)
% 0.29/20.33 [W927 11:28:31.857508842 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.
% 0.29/20.33 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 0.29/20.33 [W927 11:28:31.857554772 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.
% 0.29/20.33 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 0.29/20.33 [W927 11:28:31.857598539 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.
% 0.29/20.33 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 0.29/20.33 [W927 11:28:31.857611765 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.
% 0.29/20.33 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 0.29/20.33 [W927 11:28:31.857646092 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.
% 0.29/20.33 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 0.29/20.33 [W927 11:28:31.857657009 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.
% 0.29/20.33 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 0.29/20.33 [W927 11:28:31.857683669 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.
% 0.29/20.33 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 0.29/20.33 [W927 11:28:31.857694715 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.
% 0.29/20.33 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 0.29/20.33 [W927 11:28:31.857719329 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.
% 0.29/20.33 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 0.29/20.33 [W927 11:28:31.857730309 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.
% 0.29/20.33 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 0.29/20.33 [W927 11:28:31.857755979 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.
% 0.29/20.33 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 0.29/20.33 [W927 11:28:31.857823496 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.
% 0.29/20.33 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 0.29/20.33 % (1260025)Instruction limit reached!
% 0.29/20.33 % (1260025)------------------------------
% 0.29/20.33 % (1260025)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.29/20.33 % (1260025)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.29/20.33 % (1260025)CaDiCaL version: 2.1.3
% 0.29/20.33 % (1260025)Termination reason: Instruction limit
% 0.29/20.33 % (1260025)Termination phase: Saturation
% 0.29/20.33 % (1260025)Time elapsed: 3.454 s
% 0.29/20.33 % (1260025)Peak memory usage: 660 MB
% 0.29/20.33 % (1260025)Instructions burned: 6926 (million)
% 0.29/20.33 % (1260033)Instruction limit reached!
% 0.29/20.33 % (1260033)------------------------------
% 0.29/20.33 % (1260033)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.29/20.33 % (1260033)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.29/20.33 % (1260033)CaDiCaL version: 2.1.3
% 0.29/20.33 % (1260033)Termination reason: Instruction limit
% 0.29/20.33 % (1260033)Termination phase: Property scanning
% 0.29/20.33 % (1260033)Time elapsed: 0.692 s
% 0.29/20.33 % (1260033)Peak memory usage: 336 MB
% 0.29/20.33 % (1260033)Instructions burned: 1672 (million)
% 0.29/20.33 % (1260034)Instruction limit reached!
% 0.29/20.33 % (1260034)------------------------------
% 0.29/20.33 % (1260034)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.29/20.33 % (1260034)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.29/20.33 % (1260034)CaDiCaL version: 2.1.3
% 0.29/20.33 % (1260034)Termination reason: Instruction limit
% 0.29/20.33 % (1260034)Termination phase: SInE selection
% 0.29/20.33 % (1260034)Time elapsed: 0.636 s
% 0.29/20.33 % (1260034)Peak memory usage: 339 MB
% 0.29/20.33 % (1260034)Instructions burned: 1724 (million)
% 0.29/20.33 % (1260037)ott-1004_1_anc=all_dependent:to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:tgt=full:npcc=on:sas=cadical:sp=const_frequency:acc=on:urr=ec_only:gs=on:s2agt=40:alpa=false:sac=on:random_seed=3269418959:cts=off:cond=on:i=9530:bs=on:fsd=on_2825 on theBenchmark for (2825ds/9530Mi)
% 0.29/20.33 % (1260038)lrs+10_1_ncem=casc2026/models/loop4.pt:sil=64000:npcc=on:sp=occurrence:random_seed=3939809810:st=2:i=4495:sd=10:ss=included_2824 on theBenchmark for (2824ds/4495Mi)
% 0.29/20.33 % (1260039)lrs+1002_1_sfv=off:ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=reverse_arity:spb=non_intro:s2agt=16:random_seed=2077403949:cond=fast:i=4920:s2at=1.9:kws=inv_frequency:av=off:er=filter_2824 on theBenchmark for (2824ds/4920Mi)
% 0.29/20.33 % (1260031)First to succeed.
% 0.29/20.33 % (1260031)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-1259943"
% 0.29/20.33 % (1260031)Refutation found. Thanks to Tanya!
% 0.29/20.33 % SZS status Unsatisfiable for theBenchmark
% 0.29/20.33 % SZS output start Proof for theBenchmark
% See solution above
% 0.29/20.33 % (1260031)------------------------------
% 0.29/20.33 % (1260031)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.29/20.33 % (1260031)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.29/20.33 % (1260031)CaDiCaL version: 2.1.3
% 0.29/20.33 % (1260031)Termination reason: Refutation
% 0.29/20.33 % (1260031)Time elapsed: 3.348 s
% 0.29/20.33 % (1260031)Peak memory usage: 654 MB
% 0.29/20.33 % (1260031)Instructions burned: 6183 (million)
% 0.29/20.33 % (1260031)------------------------------
% 0.29/20.33 % (1260031)------------------------------
% 0.29/20.33 % (1259943)Success in time 18.992 s
% 0.29/20.33 % Vampire exiting
%------------------------------------------------------------------------------