%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LAT396-1 : TPTP v9.3.1. Released v6.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n017.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 11:47:35 AM UTC 2026
% Result : Satisfiable 135.30s 20.11s
% Output : Saturation 135.30s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u2059,axiom,
one = zero ).
cnf(absorption1,axiom,
meet(X0,join(X0,X1)) = X0 ).
cnf(u100,axiom,
one = join(one,X0) ).
cnf(u82,axiom,
join(X0,X1) = meet(join(X0,X1),join(X0,join(X1,X2))) ).
cnf(u13,axiom,
meet(X0,one) = X0 ).
cnf(u42,axiom,
meet(meet(X0,X1),X2) = meet(X1,meet(X0,X2)) ).
cnf(commutativity_of_meet,axiom,
meet(X0,X1) = meet(X1,X0) ).
cnf(u52,axiom,
meet(X0,X1) = meet(X0,meet(X1,join(meet(X0,X1),X2))) ).
cnf(associativity_of_meet,axiom,
meet(meet(X0,X1),X2) = meet(X0,meet(X1,X2)) ).
cnf(u44,axiom,
meet(X0,X2) = meet(X0,meet(join(X0,X1),X2)) ).
cnf(u89,axiom,
( join(X0,X1) != one
| meet(X1,X0) != zero
| complement(X1) = X0 ) ).
cnf(u74,axiom,
join(X0,join(X1,X2)) = join(X1,join(X2,X0)) ).
cnf(u115,axiom,
zero = meet(zero,X0) ).
cnf(u66,axiom,
join(X0,X1) = join(X0,join(X0,X1)) ).
cnf(u2068,axiom,
one = meet(one,X0) ).
cnf(u76,axiom,
join(X0,X1) = join(X0,join(X1,meet(join(X0,X1),X2))) ).
cnf(u69,axiom,
join(X0,X2) = join(X0,join(meet(X0,X1),X2)) ).
cnf(u28,axiom,
meet(X1,join(X0,X1)) = X1 ).
cnf(u277,axiom,
one = join(X0,join(complement(X0),X1)) ).
cnf(u2067,axiom,
one = meet(X0,one) ).
cnf(u94,axiom,
( complement(X0) = X0
| one != X0
| zero != X0 ) ).
cnf(u149,axiom,
zero = meet(X0,zero) ).
cnf(associativity_of_join,axiom,
join(join(X0,X1),X2) = join(X0,join(X1,X2)) ).
cnf(complement_meet,axiom,
meet(X0,complement(X0)) = zero ).
cnf(idempotence_of_join,axiom,
join(X0,X0) = X0 ).
cnf(commutativity_of_join,axiom,
join(X0,X1) = join(X1,X0) ).
cnf(u53,axiom,
zero = meet(X0,meet(X1,complement(meet(X0,X1)))) ).
cnf(u131,axiom,
one = complement(zero) ).
cnf(u2189,axiom,
X0 = X1 ).
cnf(u168,axiom,
one = join(X0,one) ).
cnf(u49,axiom,
meet(X0,X1) = meet(X0,meet(X1,meet(X0,X1))) ).
cnf(u41,axiom,
meet(X0,X1) = meet(X0,meet(X0,X1)) ).
cnf(u93,axiom,
( join(X0,join(X1,X2)) != one
| zero != meet(join(X0,X1),X2)
| complement(join(X0,X1)) = X2 ) ).
cnf(u35,axiom,
zero = complement(one) ).
cnf(absorption2,axiom,
join(X0,meet(X0,X1)) = X0 ).
cnf(u45,axiom,
meet(X0,meet(complement(X0),X1)) = meet(zero,X1) ).
cnf(u73,axiom,
join(X0,X1) = join(X0,join(X1,join(X0,X1))) ).
cnf(u67,axiom,
join(join(X0,X1),X2) = join(X1,join(X0,X2)) ).
cnf(u403,axiom,
( complement(X0) = one
| zero != X0 ) ).
cnf(u77,axiom,
one = join(X0,join(X1,complement(join(X0,X1)))) ).
cnf(u19,axiom,
meet(one,X0) = X0 ).
cnf(u26,axiom,
join(zero,X0) = X0 ).
cnf(u1891,axiom,
( complement(X0) = zero
| one != X0 ) ).
cnf(u1824,axiom,
( meet(X0,X1) = complement(X0)
| one != X0
| meet(X0,X1) != zero ) ).
cnf(u58,axiom,
meet(X0,X1) = join(meet(X0,X1),meet(X0,meet(X1,X2))) ).
cnf(u21,axiom,
join(X1,meet(X0,X1)) = X1 ).
cnf(u50,axiom,
meet(X0,meet(X1,X2)) = meet(X1,meet(X2,X0)) ).
cnf(u1804,axiom,
complement(complement(X0)) = X0 ).
cnf(u15,axiom,
join(X0,zero) = X0 ).
cnf(complement_join,axiom,
join(X0,complement(X0)) = one ).
cnf(meet_join_complement,axiom,
( join(X0,X1) != one
| meet(X0,X1) != zero
| complement(X0) = X1 ) ).
cnf(idempotence_of_meet,axiom,
meet(X0,X0) = X0 ).
cnf(u2072,axiom,
one = X0 ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT396-1 : TPTP v9.3.1. Released v6.4.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.38 % Computer : n017.cluster.edu
% 0.11/0.38 % Model : x86_64 x86_64
% 0.11/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.38 % Memory : 8046.5625MB
% 0.11/0.38 % OS : Linux 6.8.0-71-generic
% 0.11/0.38 % CPULimit : 300
% 0.11/0.38 % WCLimit : 300
% 0.11/0.38 % DateTime : Sun Sep 27 15:09:50 UTC 2026
% 0.11/0.38 % CPUTime :
% 0.11/0.39 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.42 Running first-order theorem proving
% 0.11/0.42 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
% 8.63/2.10 % (2708219)Input is clausal, will run a generic CNF schedule.
% 8.63/2.10 % (2708226)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=2973619579:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 8.63/2.10 % (2708228)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=3996085087:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 8.63/2.10 % (2708224)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=3057030138:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 8.63/2.10 % (2708225)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=1887941819:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 8.63/2.10 % (2708227)lrs+10_1_sil=8000:sp=occurrence:random_seed=1037113378:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 8.63/2.10 % (2708230)dis-21_1_sil=8000:lcm=predicate:random_seed=951393265:st=5:avsq=on:i=117:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/117Mi)
% 8.63/2.10 % (2708229)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3966337921:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 8.63/2.10 % (2708228)Refutation not found, incomplete strategy
% 8.63/2.10 % (2708228)------------------------------
% 8.63/2.10 % (2708228)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.63/2.10 % (2708227)Refutation not found, incomplete strategy
% 8.63/2.10 % (2708227)------------------------------
% 8.63/2.10 % (2708227)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.63/2.10 % (2708230)Refutation not found, incomplete strategy
% 8.63/2.10 % (2708230)------------------------------
% 8.63/2.10 % (2708230)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.63/2.10 % (2708228)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.63/2.10 % (2708227)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.63/2.10 % (2708230)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.63/2.10 % (2708230)CaDiCaL version: 2.1.3
% 8.63/2.10 % (2708227)CaDiCaL version: 2.1.3
% 8.63/2.10 % (2708228)CaDiCaL version: 2.1.3
% 8.63/2.10 % (2708227)Termination reason: Refutation not found, incomplete strategy
% 8.63/2.10 % (2708227)Time elapsed: 0.001 s
% 8.63/2.10 % (2708228)Termination reason: Refutation not found, incomplete strategy
% 8.63/2.10 % (2708228)Time elapsed: 0.001 s
% 8.63/2.10 % (2708230)Termination reason: Refutation not found, incomplete strategy
% 8.63/2.10 % (2708230)Time elapsed: 0.001 s
% 8.63/2.10 % (2708228)Peak memory usage: 86 MB
% 8.63/2.10 % (2708227)Peak memory usage: 86 MB
% 8.63/2.10 % (2708230)Peak memory usage: 86 MB
% 8.63/2.10 % (2708229)Instruction limit reached!
% 8.63/2.10 % (2708229)------------------------------
% 8.63/2.10 % (2708229)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.63/2.10 % (2708229)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.63/2.10 % (2708229)CaDiCaL version: 2.1.3
% 8.63/2.10 % (2708229)Termination reason: Instruction limit
% 8.63/2.10 % (2708229)Termination phase: Saturation
% 8.63/2.10 % (2708229)Time elapsed: 0.104 s
% 8.63/2.10 % (2708229)Peak memory usage: 89 MB
% 8.63/2.10 % (2708229)Instructions burned: 181 (million)
% 8.63/2.10 % (2708228)------------------------------
% 8.63/2.10 % (2708228)------------------------------
% 8.63/2.10 % (2708230)------------------------------
% 8.63/2.10 % (2708230)------------------------------
% 8.63/2.10 % (2708227)------------------------------
% 8.63/2.10 % (2708227)------------------------------
% 8.63/2.10 % (2708238)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=2798010283:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi)
% 8.63/2.10 % (2708238)Refutation not found, incomplete strategy
% 8.63/2.10 % (2708238)------------------------------
% 8.63/2.10 % (2708238)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.63/2.10 % (2708238)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.63/2.10 % (2708238)CaDiCaL version: 2.1.3
% 8.63/2.10 % (2708238)Termination reason: Refutation not found, incomplete strategy
% 8.63/2.10 % (2708238)Time elapsed: 0.001 s
% 12.03/2.75 % (2708238)Peak memory usage: 86 MB
% 12.03/2.75 % (2708240)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=3741300655:st=4:i=219:sd=3:ss=axioms_2995 on theBenchmark for (2995ds/219Mi)
% 12.03/2.75 % (2708240)Refutation not found, incomplete strategy
% 12.03/2.75 % (2708240)------------------------------
% 12.03/2.75 % (2708240)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.03/2.75 % (2708240)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.03/2.75 % (2708240)CaDiCaL version: 2.1.3
% 12.03/2.75 % (2708240)Termination reason: Refutation not found, incomplete strategy
% 12.03/2.75 % (2708240)Time elapsed: 0.0000 s
% 12.03/2.75 % (2708240)Peak memory usage: 86 MB
% 12.03/2.75 % (2708239)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=1294267412:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2995 on theBenchmark for (2995ds/189Mi)
% 12.03/2.75 % (2708241)lrs+10_64_to=lpo:sil=8000:random_seed=3895791208:i=126:bd=preordered_2995 on theBenchmark for (2995ds/126Mi)
% 12.03/2.75 % (2708239)Refutation not found, incomplete strategy
% 12.03/2.75 % (2708239)------------------------------
% 12.03/2.75 % (2708239)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.03/2.75 % (2708239)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.03/2.75 % (2708239)CaDiCaL version: 2.1.3
% 12.03/2.75 % (2708239)Termination reason: Refutation not found, incomplete strategy
% 12.03/2.75 % (2708239)Time elapsed: 0.001 s
% 12.03/2.75 % (2708239)Peak memory usage: 86 MB
% 12.03/2.75 % (2708241)Instruction limit reached!
% 12.03/2.75 % (2708241)------------------------------
% 12.03/2.75 % (2708241)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.03/2.75 % (2708241)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.03/2.75 % (2708241)CaDiCaL version: 2.1.3
% 12.03/2.75 % (2708241)Termination reason: Instruction limit
% 12.03/2.75 % (2708241)Termination phase: Saturation
% 12.03/2.75 % (2708241)Time elapsed: 0.073 s
% 12.03/2.75 % (2708241)Peak memory usage: 88 MB
% 12.03/2.75 % (2708241)Instructions burned: 127 (million)
% 12.03/2.75 % (2708240)------------------------------
% 12.03/2.75 % (2708240)------------------------------
% 12.03/2.75 % (2708238)------------------------------
% 12.03/2.75 % (2708238)------------------------------
% 12.03/2.75 % (2708246)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=3523423540:avsq=on:i=194:fgj=on:bd=preordered_2993 on theBenchmark for (2993ds/194Mi)
% 12.03/2.75 % (2708239)------------------------------
% 12.03/2.75 % (2708239)------------------------------
% 12.03/2.75 % (2708248)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=3282028080:i=3394:sd=4:ss=included:sgt=64_2993 on theBenchmark for (2993ds/3394Mi)
% 12.03/2.75 % (2708247)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=199197935:i=157:gtg=all_2993 on theBenchmark for (2993ds/157Mi)
% 12.03/2.75 % (2708246)Instruction limit reached!
% 12.03/2.75 % (2708246)------------------------------
% 12.03/2.75 % (2708246)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.03/2.75 % (2708246)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.03/2.75 % (2708246)CaDiCaL version: 2.1.3
% 12.03/2.75 % (2708246)Termination reason: Instruction limit
% 12.03/2.75 % (2708246)Termination phase: Saturation
% 12.03/2.75 % (2708246)Time elapsed: 0.116 s
% 12.03/2.75 % (2708246)Peak memory usage: 89 MB
% 12.03/2.75 % (2708246)Instructions burned: 195 (million)
% 12.03/2.75 % (2708247)Instruction limit reached!
% 12.03/2.75 % (2708247)------------------------------
% 12.03/2.75 % (2708247)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.03/2.75 % (2708247)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.03/2.75 % (2708247)CaDiCaL version: 2.1.3
% 12.03/2.75 % (2708247)Termination reason: Instruction limit
% 12.03/2.75 % (2708247)Termination phase: Saturation
% 12.03/2.75 % (2708247)Time elapsed: 0.094 s
% 12.03/2.75 % (2708247)Peak memory usage: 89 MB
% 12.03/2.75 % (2708247)Instructions burned: 158 (million)
% 12.03/2.75 % (2708250)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=2447354905:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2991 on theBenchmark for (2991ds/106Mi)
% 12.03/2.75 % (2708250)Refutation not found, incomplete strategy
% 12.03/2.75 % (2708250)------------------------------
% 19.58/3.70 % (2708250)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.58/3.70 % (2708250)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.58/3.70 % (2708250)CaDiCaL version: 2.1.3
% 19.58/3.70 % (2708250)Termination reason: Refutation not found, incomplete strategy
% 19.58/3.70 % (2708250)Time elapsed: 0.001 s
% 19.58/3.70 % (2708250)Peak memory usage: 86 MB
% 19.58/3.70 % (2708253)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=3026347258:i=107_2990 on theBenchmark for (2990ds/107Mi)
% 19.58/3.70 % (2708253)Refutation not found, incomplete strategy
% 19.58/3.70 % (2708253)------------------------------
% 19.58/3.70 % (2708253)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.58/3.70 % (2708253)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.58/3.70 % (2708253)CaDiCaL version: 2.1.3
% 19.58/3.70 % (2708253)Termination reason: Refutation not found, incomplete strategy
% 19.58/3.70 % (2708253)Time elapsed: 0.001 s
% 19.58/3.70 % (2708253)Peak memory usage: 87 MB
% 19.58/3.70 % (2708254)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=711496425:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2990 on theBenchmark for (2990ds/242Mi)
% 19.58/3.70 % (2708254)Refutation not found, incomplete strategy
% 19.58/3.70 % (2708254)------------------------------
% 19.58/3.70 % (2708254)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.58/3.70 % (2708254)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.58/3.70 % (2708254)CaDiCaL version: 2.1.3
% 19.58/3.70 % (2708254)Termination reason: Refutation not found, incomplete strategy
% 19.58/3.70 % (2708254)Time elapsed: 0.001 s
% 19.58/3.70 % (2708254)Peak memory usage: 86 MB
% 19.58/3.70 % (2708250)------------------------------
% 19.58/3.70 % (2708250)------------------------------
% 19.58/3.70 [W927 15:09:52.294667920 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.
% 19.58/3.70 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 19.58/3.70 [W927 15:09:52.294714354 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.
% 19.58/3.70 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 19.58/3.70 [W927 15:09:52.294751514 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.
% 19.58/3.70 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 19.58/3.70 [W927 15:09:52.294769704 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.
% 19.58/3.70 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 19.58/3.70 [W927 15:09:52.294795251 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.
% 19.58/3.70 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 19.58/3.70 [W927 15:09:52.294818208 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.
% 19.58/3.70 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 19.58/3.70 [W927 15:09:52.294845554 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.
% 19.58/3.70 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 19.58/3.70 [W927 15:09:52.294855871 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.
% 35.74/5.92 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 35.74/5.92 [W927 15:09:52.294884965 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.
% 35.74/5.92 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 35.74/5.92 [W927 15:09:52.294895231 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.
% 35.74/5.92 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 35.74/5.92 [W927 15:09:52.294918982 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.
% 35.74/5.92 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 35.74/5.92 [W927 15:09:52.294930605 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.
% 35.74/5.92 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 35.74/5.92 % (2708253)------------------------------
% 35.74/5.92 % (2708253)------------------------------
% 35.74/5.92 % (2708254)------------------------------
% 35.74/5.92 % (2708254)------------------------------
% 35.74/5.92 % (2708258)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=3654508509:cond=fast:i=5208:av=off_2987 on theBenchmark for (2987ds/5208Mi)
% 35.74/5.92 % (2708248)Refutation not found, incomplete strategy
% 35.74/5.92 % (2708248)------------------------------
% 35.74/5.92 % (2708248)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.74/5.92 % (2708248)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.74/5.92 % (2708248)CaDiCaL version: 2.1.3
% 35.74/5.92 % (2708248)Termination reason: Refutation not found, incomplete strategy
% 35.74/5.92 % (2708248)Time elapsed: 0.556 s
% 35.74/5.92 % (2708248)Peak memory usage: 125 MB
% 35.74/5.92 % (2708248)Instructions burned: 826 (million)
% 35.74/5.92 % (2708259)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=3106204789:i=134:sd=2:doe=on:ss=axioms:sgt=14_2986 on theBenchmark for (2986ds/134Mi)
% 35.74/5.92 % (2708259)Refutation not found, incomplete strategy
% 35.74/5.92 % (2708259)------------------------------
% 35.74/5.92 % (2708259)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.74/5.92 % (2708259)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.74/5.92 % (2708259)CaDiCaL version: 2.1.3
% 35.74/5.92 % (2708259)Termination reason: Refutation not found, incomplete strategy
% 35.74/5.92 % (2708259)Time elapsed: 0.001 s
% 35.74/5.92 % (2708259)Peak memory usage: 86 MB
% 35.74/5.92 % (2708260)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=1390631040:i=499:bd=all_2986 on theBenchmark for (2986ds/499Mi)
% 35.74/5.92 % (2708248)------------------------------
% 35.74/5.92 % (2708248)------------------------------
% 35.74/5.92 % (2708259)------------------------------
% 35.74/5.92 % (2708259)------------------------------
% 35.74/5.92 % (2708264)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=2392906588:i=191:fgj=on:bd=all_2983 on theBenchmark for (2983ds/191Mi)
% 35.74/5.92 % (2708260)Instruction limit reached!
% 35.74/5.92 % (2708260)------------------------------
% 35.74/5.92 % (2708260)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.74/5.92 % (2708260)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.74/5.92 % (2708260)CaDiCaL version: 2.1.3
% 35.74/5.92 % (2708260)Termination reason: Instruction limit
% 35.74/5.92 % (2708260)Termination phase: Saturation
% 35.74/5.92 % (2708260)Time elapsed: 0.305 s
% 35.74/5.92 % (2708260)Peak memory usage: 94 MB
% 35.74/5.92 % (2708260)Instructions burned: 501 (million)
% 35.74/5.92 % (2708265)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=1805626035:i=264:kws=precedence:fsr=off_2982 on theBenchmark for (2982ds/264Mi)
% 38.92/6.40 % (2708264)Instruction limit reached!
% 38.92/6.40 % (2708264)------------------------------
% 38.92/6.40 % (2708264)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.92/6.40 % (2708264)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.92/6.40 % (2708264)CaDiCaL version: 2.1.3
% 38.92/6.40 % (2708264)Termination reason: Instruction limit
% 38.92/6.40 % (2708264)Termination phase: Saturation
% 38.92/6.40 % (2708264)Time elapsed: 0.122 s
% 38.92/6.40 % (2708264)Peak memory usage: 91 MB
% 38.92/6.40 % (2708264)Instructions burned: 191 (million)
% 38.92/6.40 % (2708267)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=3371874843:cond=on:i=156:bs=on:gtg=exists_all:er=known_2981 on theBenchmark for (2981ds/156Mi)
% 38.92/6.40 % (2708265)Instruction limit reached!
% 38.92/6.40 % (2708265)------------------------------
% 38.92/6.40 % (2708265)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.92/6.40 % (2708265)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.92/6.40 % (2708265)CaDiCaL version: 2.1.3
% 38.92/6.40 % (2708265)Termination reason: Instruction limit
% 38.92/6.40 % (2708265)Termination phase: Saturation
% 38.92/6.40 % (2708265)Time elapsed: 0.160 s
% 38.92/6.40 % (2708265)Peak memory usage: 92 MB
% 38.92/6.40 % (2708265)Instructions burned: 264 (million)
% 38.92/6.40 % (2708269)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=4003626235:i=3256:kws=precedence:bd=preordered:av=off_2980 on theBenchmark for (2980ds/3256Mi)
% 38.92/6.40 % (2708267)Instruction limit reached!
% 38.92/6.40 % (2708267)------------------------------
% 38.92/6.40 % (2708267)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.92/6.40 % (2708267)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.92/6.40 % (2708267)CaDiCaL version: 2.1.3
% 38.92/6.40 % (2708267)Termination reason: Instruction limit
% 38.92/6.40 % (2708267)Termination phase: Saturation
% 38.92/6.40 % (2708267)Time elapsed: 0.095 s
% 38.92/6.40 % (2708267)Peak memory usage: 89 MB
% 38.92/6.40 % (2708267)Instructions burned: 157 (million)
% 38.92/6.40 % (2708271)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=2287816681:i=537:av=off:ss=included_2979 on theBenchmark for (2979ds/537Mi)
% 38.92/6.40 % (2708271)Refutation not found, incomplete strategy
% 38.92/6.40 % (2708271)------------------------------
% 38.92/6.40 % (2708271)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.92/6.40 % (2708271)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.92/6.40 % (2708271)CaDiCaL version: 2.1.3
% 38.92/6.40 % (2708271)Termination reason: Refutation not found, incomplete strategy
% 38.92/6.40 % (2708271)Time elapsed: 0.0000 s
% 38.92/6.40 % (2708271)Peak memory usage: 86 MB
% 38.92/6.40 % (2708273)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=1367414782:i=180:bd=preordered:av=off_2979 on theBenchmark for (2979ds/180Mi)
% 38.92/6.40 % (2708273)Instruction limit reached!
% 38.92/6.40 % (2708273)------------------------------
% 38.92/6.40 % (2708273)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.92/6.40 % (2708273)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.92/6.40 % (2708273)CaDiCaL version: 2.1.3
% 38.92/6.40 % (2708273)Termination reason: Instruction limit
% 38.92/6.40 % (2708273)Termination phase: Saturation
% 38.92/6.40 % (2708273)Time elapsed: 0.101 s
% 38.92/6.40 % (2708273)Peak memory usage: 88 MB
% 38.92/6.40 % (2708273)Instructions burned: 180 (million)
% 38.92/6.40 % (2708271)------------------------------
% 38.92/6.40 % (2708271)------------------------------
% 38.92/6.40 % (2708276)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=576069118:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2976 on theBenchmark for (2976ds/10307Mi)
% 38.92/6.40 % (2708277)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=1365917003:i=412:gtgl=4:gtg=exists_all_2975 on theBenchmark for (2975ds/412Mi)
% 38.92/6.40 % (2708277)Instruction limit reached!
% 38.92/6.40 % (2708277)------------------------------
% 38.92/6.40 % (2708277)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.92/6.40 % (2708277)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 54.48/8.64 % (2708277)CaDiCaL version: 2.1.3
% 54.48/8.64 % (2708277)Termination reason: Instruction limit
% 54.48/8.64 % (2708277)Termination phase: Saturation
% 54.48/8.64 % (2708277)Time elapsed: 0.228 s
% 54.48/8.64 % (2708277)Peak memory usage: 94 MB
% 54.48/8.64 % (2708277)Instructions burned: 412 (million)
% 54.48/8.64 % (2708280)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=1337977494:s2pl=no:i=8478:s2at=4:nm=6_2971 on theBenchmark for (2971ds/8478Mi)
% 54.48/8.64 % (2708269)Instruction limit reached!
% 54.48/8.64 % (2708269)------------------------------
% 54.48/8.64 % (2708269)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 54.48/8.64 % (2708269)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 54.48/8.64 % (2708269)CaDiCaL version: 2.1.3
% 54.48/8.64 % (2708269)Termination reason: Instruction limit
% 54.48/8.64 % (2708269)Termination phase: Saturation
% 54.48/8.64 % (2708269)Time elapsed: 1.977 s
% 54.48/8.64 % (2708269)Peak memory usage: 149 MB
% 54.48/8.64 % (2708269)Instructions burned: 3257 (million)
% 54.48/8.64 % (2708282)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=1357331788:s2a=on:i=303:s2at=2:sd=1:kws=inv_arity:bs=on:ins=10:fdi=1024:sup=off:ss=included_2959 on theBenchmark for (2959ds/303Mi)
% 54.48/8.64 % (2708282)Refutation not found, incomplete strategy
% 54.48/8.64 % (2708282)------------------------------
% 54.48/8.64 % (2708282)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 54.48/8.64 % (2708282)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 54.48/8.64 % (2708282)CaDiCaL version: 2.1.3
% 54.48/8.64 % (2708282)Termination reason: Refutation not found, incomplete strategy
% 54.48/8.64 % (2708282)Time elapsed: 0.001 s
% 54.48/8.64 % (2708282)Peak memory usage: 87 MB
% 54.48/8.64 % (2708258)Instruction limit reached!
% 54.48/8.64 % (2708258)------------------------------
% 54.48/8.64 % (2708258)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 54.48/8.64 % (2708258)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 54.48/8.64 % (2708258)CaDiCaL version: 2.1.3
% 54.48/8.64 % (2708258)Termination reason: Instruction limit
% 54.48/8.64 % (2708258)Termination phase: Saturation
% 54.48/8.64 % (2708258)Time elapsed: 3.056 s
% 54.48/8.64 % (2708258)Peak memory usage: 167 MB
% 54.48/8.64 % (2708258)Instructions burned: 5209 (million)
% 54.48/8.64 % (2708282)------------------------------
% 54.48/8.64 % (2708282)------------------------------
% 54.48/8.64 % (2708284)lrs+10_1_to=lpo:sil=16000:fde=none:sos=on:urr=on:bsr=on:random_seed=326807211:st=4:i=720:sd=3:fsr=off:ss=axioms_2955 on theBenchmark for (2955ds/720Mi)
% 54.48/8.64 % (2708284)Refutation not found, incomplete strategy
% 54.48/8.64 % (2708284)------------------------------
% 54.48/8.64 % (2708284)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 54.48/8.64 % (2708284)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 54.48/8.64 % (2708284)CaDiCaL version: 2.1.3
% 54.48/8.64 % (2708284)Termination reason: Refutation not found, incomplete strategy
% 54.48/8.64 % (2708284)Time elapsed: 0.001 s
% 54.48/8.64 % (2708284)Peak memory usage: 86 MB
% 54.48/8.64 % (2708285)lrs-20_1_to=lpo:sil=32000:tgt=ground:sp=reverse_frequency:spb=goal:urr=on:bsr=unit_only:nwc=1.5:random_seed=6245727:i=598:bs=on:bd=preordered:av=off:ss=axioms_2955 on theBenchmark for (2955ds/598Mi)
% 54.48/8.64 % (2708285)Refutation not found, incomplete strategy
% 54.48/8.64 % (2708285)------------------------------
% 54.48/8.64 % (2708285)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 54.48/8.64 % (2708285)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 54.48/8.64 % (2708285)CaDiCaL version: 2.1.3
% 54.48/8.64 % (2708285)Termination reason: Refutation not found, incomplete strategy
% 54.48/8.64 % (2708285)Time elapsed: 0.0000 s
% 54.48/8.64 % (2708285)Peak memory usage: 86 MB
% 54.48/8.64 % (2708284)------------------------------
% 54.48/8.64 % (2708284)------------------------------
% 54.48/8.64 % (2708285)------------------------------
% 54.48/8.64 % (2708285)------------------------------
% 54.48/8.64 % (2708288)dis-1010_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=occurrence:random_seed=1810939849:i=2989:sd=3:ss=axioms:sgt=60_2951 on theBenchmark for (2951ds/2989Mi)
% 54.48/8.64 % (2708289)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=2777150591:i=1997:bd=preordered:av=off:gtg=all:gsp=on_2951 on theBenchmark for (2951ds/1997Mi)
% 55.52/8.88 [W927 15:09:56.427498658 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.
% 55.52/8.88 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 55.52/8.88 [W927 15:09:56.427533932 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.
% 55.52/8.88 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 55.52/8.88 [W927 15:09:56.427572452 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.
% 55.52/8.89 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 55.52/8.89 [W927 15:09:56.427585935 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.
% 55.52/8.89 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 55.52/8.89 [W927 15:09:56.427614179 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.
% 55.52/8.89 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 55.52/8.89 [W927 15:09:56.427626412 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.
% 55.52/8.89 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 55.52/8.89 [W927 15:09:56.427652259 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.
% 55.52/8.89 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 55.52/8.89 [W927 15:09:56.427664182 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.
% 55.52/8.89 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 55.52/8.89 [W927 15:09:56.427689256 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.
% 55.52/8.89 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 55.52/8.89 [W927 15:09:56.427700543 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.
% 55.52/8.89 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 55.52/8.89 [W927 15:09:56.427725843 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.
% 55.52/8.89 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 55.52/8.89 [W927 15:09:56.427737326 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.
% 55.52/8.89 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 55.52/8.89 % (2708288)Refutation not found, incomplete strategy
% 55.52/8.89 % (2708288)------------------------------
% 55.52/8.89 % (2708288)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 59.37/9.24 % (2708288)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.37/9.24 % (2708288)CaDiCaL version: 2.1.3
% 59.37/9.24 % (2708288)Termination reason: Refutation not found, incomplete strategy
% 59.37/9.24 % (2708288)Time elapsed: 0.547 s
% 59.37/9.24 % (2708288)Peak memory usage: 125 MB
% 59.37/9.24 % (2708288)Instructions burned: 825 (million)
% 59.37/9.24 % (2708288)------------------------------
% 59.37/9.24 % (2708288)------------------------------
% 59.37/9.24 % (2708292)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=496173855:i=2088:bd=preordered:av=off_2942 on theBenchmark for (2942ds/2088Mi)
% 59.37/9.24 % (2708289)Instruction limit reached!
% 59.37/9.24 % (2708289)------------------------------
% 59.37/9.24 % (2708289)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 59.37/9.24 % (2708289)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.37/9.24 % (2708289)CaDiCaL version: 2.1.3
% 59.37/9.24 % (2708289)Termination reason: Instruction limit
% 59.37/9.24 % (2708289)Termination phase: Saturation
% 59.37/9.24 % (2708289)Time elapsed: 1.235 s
% 59.37/9.24 % (2708289)Peak memory usage: 138 MB
% 59.37/9.24 % (2708289)Instructions burned: 1997 (million)
% 59.37/9.24 % (2708294)lrs+1010_64:1_anc=all:to=lpo:sil=16000:fde=none:sp=const_frequency:urr=full:sac=on:random_seed=4272443475:i=1098:nicw=on_2937 on theBenchmark for (2937ds/1098Mi)
% 59.37/9.24 % (2708294)Instruction limit reached!
% 59.37/9.24 % (2708294)------------------------------
% 59.37/9.24 % (2708294)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 59.37/9.24 % (2708294)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.37/9.24 % (2708294)CaDiCaL version: 2.1.3
% 59.37/9.24 % (2708294)Termination reason: Instruction limit
% 59.37/9.24 % (2708294)Termination phase: Saturation
% 59.37/9.24 % (2708294)Time elapsed: 0.621 s
% 59.37/9.24 % (2708294)Peak memory usage: 101 MB
% 59.37/9.24 % (2708294)Instructions burned: 1099 (million)
% 59.37/9.24 % (2708292)Instruction limit reached!
% 59.37/9.24 % (2708292)------------------------------
% 59.37/9.24 % (2708292)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 59.37/9.24 % (2708292)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.37/9.24 % (2708292)CaDiCaL version: 2.1.3
% 59.37/9.24 % (2708292)Termination reason: Instruction limit
% 59.37/9.24 % (2708292)Termination phase: Saturation
% 59.37/9.24 % (2708292)Time elapsed: 1.294 s
% 59.37/9.24 % (2708292)Peak memory usage: 139 MB
% 59.37/9.24 % (2708292)Instructions burned: 2089 (million)
% 59.37/9.24 % (2708296)lrs-1011_32:1_to=lpo:sil=32000:tgt=ground:sos=on:spb=goal_then_units:acc=on:random_seed=1672299949:i=433:bd=preordered_2929 on theBenchmark for (2929ds/433Mi)
% 59.37/9.24 % (2708296)Refutation not found, incomplete strategy
% 59.37/9.24 % (2708296)------------------------------
% 59.37/9.24 % (2708296)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 59.37/9.24 % (2708296)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.37/9.24 % (2708296)CaDiCaL version: 2.1.3
% 59.37/9.24 % (2708296)Termination reason: Refutation not found, incomplete strategy
% 59.37/9.24 % (2708296)Time elapsed: 0.001 s
% 59.37/9.24 % (2708296)Peak memory usage: 87 MB
% 59.37/9.24 % (2708298)lrs+1002_1_ncem=casc2026/models/loop3.pt:sil=32000:npcc=on:prc=on:etr=on:spb=goal:flr=on:random_seed=1479613095:st=5.37:cond=on:i=2942:s2at=20:aac=none:fgj=on:bs=on:gtg=exists_sym:ss=axioms:er=filter:sgt=16_2927 on theBenchmark for (2927ds/2942Mi)
% 59.37/9.24 % (2708296)------------------------------
% 59.37/9.24 % (2708296)------------------------------
% 59.37/9.24 % (2708300)lrs+35_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=reverse_arity:urr=full:rp=on:br=off:random_seed=1442805249:i=6922:s2at=5:sd=3:bd=all:ss=axioms:er=known:sgt=32_2925 on theBenchmark for (2925ds/6922Mi)
% 59.37/9.24 [W927 15:09:58.841976930 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.
% 59.37/9.24 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 59.37/9.24 [W927 15:09:58.842031317 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.
% 63.25/10.03 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 63.25/10.03 [W927 15:09:58.842069091 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.
% 63.25/10.03 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 63.25/10.03 [W927 15:09:58.842081254 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.
% 63.25/10.03 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 63.25/10.03 [W927 15:09:58.842105218 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.
% 63.25/10.03 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 63.25/10.03 [W927 15:09:58.842172598 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.
% 63.25/10.03 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 63.25/10.03 [W927 15:09:58.842224929 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.
% 63.25/10.03 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 63.25/10.03 [W927 15:09:58.842256392 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.
% 63.25/10.03 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 63.25/10.03 [W927 15:09:58.842287239 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.
% 63.25/10.03 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 63.25/10.03 [W927 15:09:58.842298146 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.
% 63.25/10.03 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 63.25/10.03 [W927 15:09:58.842322463 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.
% 63.25/10.03 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 63.25/10.03 [W927 15:09:58.842332709 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.
% 63.25/10.03 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 63.25/10.03 % (2708298)Refutation not found, incomplete strategy
% 63.25/10.03 % (2708298)------------------------------
% 63.25/10.03 % (2708298)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 63.25/10.03 % (2708298)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 63.25/10.03 % (2708298)CaDiCaL version: 2.1.3
% 63.25/10.03 % (2708298)Termination reason: Refutation not found, incomplete strategy
% 63.25/10.03 % (2708298)Time elapsed: 0.548 s
% 63.25/10.03 % (2708298)Peak memory usage: 126 MB
% 63.25/10.03 % (2708298)Instructions burned: 821 (million)
% 63.25/10.03 [W927 15:09:58.083615539 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.
% 63.25/10.03 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 71.05/10.98 [W927 15:09:58.083659083 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.
% 71.05/10.98 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 71.05/10.98 [W927 15:09:58.083696630 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.
% 71.05/10.98 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 71.05/10.98 [W927 15:09:58.083709023 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.
% 71.05/10.98 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 71.05/10.98 [W927 15:09:58.083734087 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.
% 71.05/10.98 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 71.05/10.98 [W927 15:09:58.083759914 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.
% 71.05/10.98 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 71.05/10.98 [W927 15:09:58.083787147 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.
% 71.05/10.98 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 71.05/10.98 [W927 15:09:58.083797287 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.
% 71.05/10.98 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 71.05/10.98 [W927 15:09:58.083820614 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.
% 71.05/10.98 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 71.05/10.98 [W927 15:09:58.083830727 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.
% 71.05/10.98 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 71.05/10.98 [W927 15:09:58.083854271 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.
% 71.05/10.98 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 71.05/10.98 [W927 15:09:58.083864471 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.
% 71.05/10.98 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 71.05/10.98 % (2708300)Refutation not found, incomplete strategy
% 71.05/10.98 % (2708300)------------------------------
% 71.05/10.98 % (2708300)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 71.05/10.98 % (2708300)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 71.05/10.98 % (2708300)CaDiCaL version: 2.1.3
% 71.05/10.98 % (2708300)Termination reason: Refutation not found, incomplete strategy
% 71.05/10.98 % (2708300)Time elapsed: 0.545 s
% 71.05/10.98 % (2708300)Peak memory usage: 125 MB
% 71.05/10.98 % (2708300)Instructions burned: 824 (million)
% 71.05/10.98 % (2708298)------------------------------
% 71.05/10.98 % (2708298)------------------------------
% 71.05/10.98 % (2708302)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=2618482952:s2a=on:i=596:s2at=2.3:gtgl=5:gtg=all:sup=off_2917 on theBenchmark for (2917ds/596Mi)
% 76.89/11.70 % (2708302)Refutation not found, incomplete strategy
% 76.89/11.70 % (2708302)------------------------------
% 76.89/11.70 % (2708302)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 76.89/11.70 % (2708302)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 76.89/11.70 % (2708302)CaDiCaL version: 2.1.3
% 76.89/11.70 % (2708302)Termination reason: Refutation not found, incomplete strategy
% 76.89/11.70 % (2708302)Time elapsed: 0.002 s
% 76.89/11.70 % (2708302)Peak memory usage: 88 MB
% 76.89/11.70 % (2708302)Instructions burned: 1 (million)
% 76.89/11.70 % (2708300)------------------------------
% 76.89/11.70 % (2708300)------------------------------
% 76.89/11.70 % (2708304)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=562169150:i=4123:kws=inv_frequency:bd=preordered:av=off:er=known_2915 on theBenchmark for (2915ds/4123Mi)
% 76.89/11.70 % (2708302)------------------------------
% 76.89/11.70 % (2708302)------------------------------
% 76.89/11.70 % (2708306)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=1858686443:i=16411:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2913 on theBenchmark for (2913ds/16411Mi)
% 76.89/11.70 % (2708276)Instruction limit reached!
% 76.89/11.70 % (2708276)------------------------------
% 76.89/11.70 % (2708276)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 76.89/11.70 % (2708276)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 76.89/11.70 % (2708276)CaDiCaL version: 2.1.3
% 76.89/11.70 % (2708276)Termination reason: Instruction limit
% 76.89/11.70 % (2708276)Termination phase: Saturation
% 76.89/11.70 % (2708276)Time elapsed: 6.314 s
% 76.89/11.70 % (2708276)Peak memory usage: 200 MB
% 76.89/11.70 % (2708276)Instructions burned: 10308 (million)
% 76.89/11.70 % (2708308)lrs+0_1_ncem=casc2026/models/loop1.pt:sil=8000:tgt=full:npcc=on:sp=reverse_frequency:gs=on:random_seed=887006019:i=1670:kws=inv_precedence:bd=all:av=off:gtg=exists_all_2911 on theBenchmark for (2911ds/1670Mi)
% 76.89/11.70 [W927 15:10:00.224522396 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.
% 76.89/11.70 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 76.89/11.70 [W927 15:10:00.224566636 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.
% 76.89/11.70 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 76.89/11.70 [W927 15:10:00.224606013 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.
% 76.89/11.70 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 76.89/11.70 [W927 15:10:00.224621650 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.
% 76.89/11.70 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 76.89/11.70 [W927 15:10:00.224647050 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.
% 76.89/11.70 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 76.89/11.70 [W927 15:10:00.224657880 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.
% 76.89/11.70 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 76.89/11.70 [W927 15:10:00.224682591 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.92/11.95 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 77.92/11.95 [W927 15:10:00.224692984 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.92/11.95 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 77.92/11.95 [W927 15:10:00.224717051 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.92/11.95 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 77.92/11.95 [W927 15:10:00.224727238 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.92/11.95 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 77.92/11.95 [W927 15:10:00.224750618 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.92/11.95 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 77.92/11.95 [W927 15:10:00.224760641 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.92/11.95 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 77.92/11.95 % (2708306)Refutation not found, incomplete strategy
% 77.92/11.95 % (2708306)------------------------------
% 77.92/11.95 % (2708306)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 77.92/11.95 % (2708306)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 77.92/11.95 % (2708306)CaDiCaL version: 2.1.3
% 77.92/11.95 % (2708306)Termination reason: Refutation not found, incomplete strategy
% 77.92/11.95 % (2708306)Time elapsed: 0.540 s
% 77.92/11.95 % (2708306)Peak memory usage: 125 MB
% 77.92/11.95 % (2708306)Instructions burned: 820 (million)
% 77.92/11.95 % (2708306)------------------------------
% 77.92/11.95 % (2708306)------------------------------
% 77.92/11.95 % (2708310)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=3214073787:st=3:cond=fast:i=1722:sd=2:ss=included:fsd=on_2904 on theBenchmark for (2904ds/1722Mi)
% 77.92/11.95 % (2708308)Instruction limit reached!
% 77.92/11.95 % (2708308)------------------------------
% 77.92/11.95 % (2708308)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 77.92/11.95 % (2708308)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 77.92/11.95 % (2708308)CaDiCaL version: 2.1.3
% 77.92/11.95 % (2708308)Termination reason: Instruction limit
% 77.92/11.95 % (2708308)Termination phase: Saturation
% 77.92/11.95 % (2708308)Time elapsed: 1.047 s
% 77.92/11.95 % (2708308)Peak memory usage: 134 MB
% 77.92/11.95 % (2708308)Instructions burned: 1670 (million)
% 77.92/11.95 [W927 15:10:01.176807119 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.92/11.95 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 77.92/11.95 [W927 15:10:01.176853466 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.92/11.95 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 77.92/11.95 [W927 15:10:01.176890273 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.92/11.95 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 77.92/11.95 [W927 15:10:01.176902217 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.
% 90.09/13.62 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 90.09/13.62 [W927 15:10:01.176928817 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.
% 90.09/13.62 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 90.09/13.62 [W927 15:10:01.176939857 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.
% 90.09/13.62 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 90.09/13.62 [W927 15:10:01.176964864 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.
% 90.09/13.62 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 90.09/13.62 [W927 15:10:01.176974927 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.
% 90.09/13.62 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 90.09/13.62 [W927 15:10:01.176999917 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.
% 90.09/13.62 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 90.09/13.62 [W927 15:10:01.177021451 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.
% 90.09/13.62 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 90.09/13.62 [W927 15:10:01.177046861 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.
% 90.09/13.62 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 90.09/13.62 [W927 15:10:01.177057241 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.
% 90.09/13.62 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 90.09/13.62 % (2708312)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=2866713007:cts=off:cond=on:i=9530:bs=on:fsd=on_2899 on theBenchmark for (2899ds/9530Mi)
% 90.09/13.62 % (2708310)Refutation not found, incomplete strategy
% 90.09/13.62 % (2708310)------------------------------
% 90.09/13.62 % (2708310)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 90.09/13.62 % (2708310)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 90.09/13.62 % (2708310)CaDiCaL version: 2.1.3
% 90.09/13.62 % (2708310)Termination reason: Refutation not found, incomplete strategy
% 90.09/13.62 % (2708310)Time elapsed: 0.547 s
% 90.09/13.62 % (2708310)Peak memory usage: 125 MB
% 90.09/13.62 % (2708310)Instructions burned: 824 (million)
% 90.09/13.62 % (2708310)------------------------------
% 90.09/13.62 % (2708310)------------------------------
% 90.09/13.62 % (2708314)lrs+10_1_ncem=casc2026/models/loop4.pt:sil=64000:npcc=on:sp=occurrence:random_seed=488559594:st=2:i=4495:sd=10:ss=included_2894 on theBenchmark for (2894ds/4495Mi)
% 90.09/13.62 % (2708280)Instruction limit reached!
% 90.09/13.62 % (2708280)------------------------------
% 90.09/13.62 % (2708280)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 90.09/13.62 % (2708280)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 90.09/13.62 % (2708280)CaDiCaL version: 2.1.3
% 91.70/13.92 % (2708280)Termination reason: Instruction limit
% 91.70/13.92 % (2708280)Termination phase: Saturation
% 91.70/13.92 % (2708280)Time elapsed: 7.823 s
% 91.70/13.92 % (2708280)Peak memory usage: 143 MB
% 91.70/13.92 % (2708280)Instructions burned: 8480 (million)
% 91.70/13.92 % (2708316)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=3538326623:cond=fast:i=4920:s2at=1.9:kws=inv_frequency:av=off:er=filter_2891 on theBenchmark for (2891ds/4920Mi)
% 91.70/13.92 % (2708304)Instruction limit reached!
% 91.70/13.92 % (2708304)------------------------------
% 91.70/13.92 % (2708304)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 91.70/13.92 % (2708304)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 91.70/13.92 % (2708304)CaDiCaL version: 2.1.3
% 91.70/13.92 % (2708304)Termination reason: Instruction limit
% 91.70/13.92 % (2708304)Termination phase: Saturation
% 91.70/13.92 % (2708304)Time elapsed: 2.464 s
% 91.70/13.92 % (2708304)Peak memory usage: 154 MB
% 91.70/13.92 % (2708304)Instructions burned: 4124 (million)
% 91.70/13.92 [W927 15:10:02.149588267 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.
% 91.70/13.92 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 91.70/13.92 [W927 15:10:02.149619430 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.
% 91.70/13.92 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 91.70/13.92 [W927 15:10:02.149656387 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.
% 91.70/13.92 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 91.70/13.92 [W927 15:10:02.149667667 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.
% 91.70/13.92 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 91.70/13.92 [W927 15:10:02.149691951 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.
% 91.70/13.92 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 91.70/13.92 [W927 15:10:02.149714061 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.
% 91.70/13.92 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 91.70/13.92 [W927 15:10:02.149740011 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.
% 91.70/13.92 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 91.70/13.92 [W927 15:10:02.149750141 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.
% 91.70/13.92 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 91.70/13.92 [W927 15:10:02.149774848 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.
% 91.70/13.92 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 91.70/13.92 [W927 15:10:02.149784944 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.
% 91.70/13.92 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 95.92/14.40 [W927 15:10:02.149808008 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.
% 95.92/14.40 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 95.92/14.40 [W927 15:10:02.149821901 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.
% 95.92/14.40 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 95.92/14.40 % (2708318)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:lcm=reverse:bce=on:bsr=unit_only:random_seed=1622275985:cts=off:cond=on:i=2083:s2at=-1:fgj=on:av=off_2889 on theBenchmark for (2889ds/2083Mi)
% 95.92/14.40 % (2708314)Refutation not found, incomplete strategy
% 95.92/14.40 % (2708314)------------------------------
% 95.92/14.40 % (2708314)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 95.92/14.40 % (2708314)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.92/14.40 % (2708314)CaDiCaL version: 2.1.3
% 95.92/14.40 % (2708314)Termination reason: Refutation not found, incomplete strategy
% 95.92/14.40 % (2708314)Time elapsed: 0.551 s
% 95.92/14.40 % (2708314)Peak memory usage: 125 MB
% 95.92/14.40 % (2708314)Instructions burned: 822 (million)
% 95.92/14.40 % (2708314)------------------------------
% 95.92/14.40 % (2708314)------------------------------
% 95.92/14.40 % (2708320)lrs+31_1_to=lpo:ncem=casc2026/models/loop2.pt:sil=16000:npcc=on:sp=weighted_frequency:sos=all:spb=units:lcm=predicate:bsr=on:gs=on:random_seed=1433859720:i=4629:av=off:gsp=on_2884 on theBenchmark for (2884ds/4629Mi)
% 95.92/14.40 % (2708320)Refutation not found, incomplete strategy
% 95.92/14.40 % (2708320)------------------------------
% 95.92/14.40 % (2708320)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 95.92/14.40 % (2708320)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.92/14.40 % (2708320)CaDiCaL version: 2.1.3
% 95.92/14.40 % (2708320)Termination reason: Refutation not found, incomplete strategy
% 95.92/14.40 % (2708320)Time elapsed: 0.553 s
% 95.92/14.40 % (2708320)Peak memory usage: 127 MB
% 95.92/14.40 % (2708320)Instructions burned: 828 (million)
% 95.92/14.40 % (2708226)Refutation not found, incomplete strategy
% 95.92/14.40 % (2708226)------------------------------
% 95.92/14.40 % (2708226)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 95.92/14.40 % (2708226)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.92/14.40 % (2708226)CaDiCaL version: 2.1.3
% 95.92/14.40 % (2708226)Termination reason: Refutation not found, incomplete strategy
% 95.92/14.40 % (2708226)Time elapsed: 12.198 s
% 95.92/14.40 % (2708226)Peak memory usage: 368 MB
% 95.92/14.40 % (2708226)Instructions burned: 21811 (million)
% 95.92/14.40 % (2708320)------------------------------
% 95.92/14.40 % (2708320)------------------------------
% 95.92/14.40 % (2708318)Instruction limit reached!
% 95.92/14.40 % (2708318)------------------------------
% 95.92/14.40 % (2708318)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 95.92/14.40 % (2708318)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.92/14.40 % (2708318)CaDiCaL version: 2.1.3
% 95.92/14.40 % (2708318)Termination reason: Instruction limit
% 95.92/14.40 % (2708318)Termination phase: Saturation
% 95.92/14.40 % (2708318)Time elapsed: 1.284 s
% 95.92/14.40 % (2708318)Peak memory usage: 138 MB
% 95.92/14.40 % (2708318)Instructions burned: 2083 (million)
% 95.92/14.40 % (2708226)------------------------------
% 95.92/14.40 % (2708226)------------------------------
% 95.92/14.40 % (2708322)dis+10_64_sil=16000:tgt=full:plsq=on:prc=on:drc=off:plsqc=2:plsqr=32,1:spb=goal:random_seed=2985634797:i=1258:av=off_2875 on theBenchmark for (2875ds/1258Mi)
% 95.92/14.40 % (2708323)ott+1_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:fdtod=off:random_seed=1204356414:i=7343:av=off:ss=included_2874 on theBenchmark for (2874ds/7343Mi)
% 95.92/14.40 % (2708324)lrs-1002_1_to=lpo:sil=16000:sp=reverse_arity:sos=on:random_seed=4290073494:i=1325:sd=2:ss=axioms:sgt=16_2873 on theBenchmark for (2873ds/1325Mi)
% 95.92/14.40 % (2708324)Refutation not found, incomplete strategy
% 95.92/14.40 % (2708324)------------------------------
% 95.92/14.40 % (2708324)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 96.40/14.58 % (2708324)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 96.40/14.58 % (2708324)CaDiCaL version: 2.1.3
% 96.40/14.58 % (2708324)Termination reason: Refutation not found, incomplete strategy
% 96.40/14.58 % (2708324)Time elapsed: 0.0000 s
% 96.40/14.58 % (2708324)Peak memory usage: 86 MB
% 96.40/14.58 % (2708324)------------------------------
% 96.40/14.58 % (2708324)------------------------------
% 96.40/14.58 [W927 15:10:04.119173352 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.
% 96.40/14.58 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 96.40/14.58 [W927 15:10:04.119208805 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.
% 96.40/14.58 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 96.40/14.58 [W927 15:10:04.119247059 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.
% 96.40/14.58 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 96.40/14.58 [W927 15:10:04.119260826 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.
% 96.40/14.58 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 96.40/14.58 [W927 15:10:04.119286766 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.
% 96.40/14.58 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 96.40/14.58 [W927 15:10:04.119299466 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.
% 96.40/14.58 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 96.40/14.58 [W927 15:10:04.119325726 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.
% 96.40/14.58 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 96.40/14.58 [W927 15:10:04.119337833 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.
% 96.40/14.58 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 96.40/14.58 [W927 15:10:04.119363160 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.
% 96.40/14.58 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 96.40/14.58 [W927 15:10:04.119375610 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.
% 96.40/14.58 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 96.40/14.58 [W927 15:10:04.119401257 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.
% 96.40/14.58 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 96.40/14.58 [W927 15:10:04.119413887 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.
% 96.40/14.58 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 102.93/15.47 % (2708328)dis+1011_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:prc=on:sp=arity:lma=off:spb=intro:urr=ec_only:sac=on:random_seed=3828061660:st=3.9:cond=fast:i=2646:s2at=1.8:sd=5:amm=off:gtg=position:ss=axioms:fsd=on_2870 on theBenchmark for (2870ds/2646Mi)
% 102.93/15.47 % (2708322)Instruction limit reached!
% 102.93/15.47 % (2708322)------------------------------
% 102.93/15.47 % (2708322)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 102.93/15.47 % (2708322)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 102.93/15.47 % (2708322)CaDiCaL version: 2.1.3
% 102.93/15.47 % (2708322)Termination reason: Instruction limit
% 102.93/15.47 % (2708322)Termination phase: Saturation
% 102.93/15.47 % (2708322)Time elapsed: 0.532 s
% 102.93/15.47 % (2708322)Peak memory usage: 91 MB
% 102.93/15.47 % (2708322)Instructions burned: 1261 (million)
% 102.93/15.47 % (2708323)Refutation not found, incomplete strategy
% 102.93/15.47 % (2708323)------------------------------
% 102.93/15.47 % (2708323)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 102.93/15.47 % (2708323)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 102.93/15.47 % (2708323)CaDiCaL version: 2.1.3
% 102.93/15.47 % (2708323)Termination reason: Refutation not found, incomplete strategy
% 102.93/15.47 % (2708323)Time elapsed: 0.550 s
% 102.93/15.47 % (2708323)Peak memory usage: 125 MB
% 102.93/15.47 % (2708323)Instructions burned: 824 (million)
% 102.93/15.47 % (2708330)dis-1003_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:sp=arity:sos=on:urr=on:random_seed=3051333642:i=1489:sd=2:ep=R:ss=axioms_2868 on theBenchmark for (2868ds/1489Mi)
% 102.93/15.47 % (2708323)------------------------------
% 102.93/15.47 % (2708323)------------------------------
% 102.93/15.47 [W927 15:10:04.599157501 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.
% 102.93/15.47 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 102.93/15.47 [W927 15:10:04.599192571 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.
% 102.93/15.47 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 102.93/15.47 [W927 15:10:04.599229438 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.
% 102.93/15.47 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 102.93/15.47 [W927 15:10:04.599242465 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.
% 102.93/15.47 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 102.93/15.47 [W927 15:10:04.599270978 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.
% 102.93/15.47 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 102.93/15.47 [W927 15:10:04.599282748 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.
% 102.93/15.47 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 102.93/15.47 [W927 15:10:04.599308055 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.
% 102.93/15.47 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 102.93/15.47 [W927 15:10:04.599319372 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.
% 102.93/15.47 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 104.44/15.70 [W927 15:10:04.599344339 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.
% 104.44/15.70 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 104.44/15.70 [W927 15:10:04.599354862 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.
% 104.44/15.70 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 104.44/15.70 [W927 15:10:04.599393586 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.
% 104.44/15.70 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 104.44/15.70 [W927 15:10:04.599404666 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.
% 104.44/15.70 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 104.44/15.70 % (2708332)lrs+20_1_ncem=casc2026/models/loop3.pt:sil=32000:npcc=on:fde=unused:sp=occurrence:sos=on:lcm=predicate:urr=full:sac=on:random_seed=1203642329:i=1503_2865 on theBenchmark for (2865ds/1503Mi)
% 104.44/15.70 % (2708328)Refutation not found, incomplete strategy
% 104.44/15.70 % (2708328)------------------------------
% 104.44/15.70 % (2708328)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 104.44/15.70 % (2708328)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 104.44/15.70 % (2708328)CaDiCaL version: 2.1.3
% 104.44/15.70 % (2708328)Termination reason: Refutation not found, incomplete strategy
% 104.44/15.70 % (2708328)Time elapsed: 0.547 s
% 104.44/15.70 % (2708328)Peak memory usage: 125 MB
% 104.44/15.70 % (2708328)Instructions burned: 822 (million)
% 104.44/15.70 [W927 15:10:04.775713387 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.
% 104.44/15.70 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 104.44/15.70 [W927 15:10:04.775756794 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.
% 104.44/15.70 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 104.44/15.70 [W927 15:10:04.775793527 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.
% 104.44/15.70 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 104.44/15.70 [W927 15:10:04.775807394 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.
% 104.44/15.70 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 104.44/15.70 [W927 15:10:04.775832761 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.
% 104.44/15.70 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 104.44/15.70 [W927 15:10:04.775846161 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.
% 104.44/15.70 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 104.44/15.70 [W927 15:10:04.775872075 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.
% 104.94/15.85 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 104.94/15.85 [W927 15:10:04.775883628 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.
% 104.94/15.85 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 104.94/15.85 [W927 15:10:04.775914515 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.
% 104.94/15.85 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 104.94/15.85 [W927 15:10:04.775937702 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.
% 104.94/15.85 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 104.94/15.85 [W927 15:10:04.775963492 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.
% 104.94/15.85 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 104.94/15.85 [W927 15:10:04.775973955 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.
% 104.94/15.85 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 104.94/15.85 % (2708316)Instruction limit reached!
% 104.94/15.85 % (2708316)------------------------------
% 104.94/15.85 % (2708316)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 104.94/15.85 % (2708316)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 104.94/15.85 % (2708316)CaDiCaL version: 2.1.3
% 104.94/15.85 % (2708316)Termination reason: Instruction limit
% 104.94/15.85 % (2708316)Termination phase: Saturation
% 104.94/15.85 % (2708316)Time elapsed: 2.864 s
% 104.94/15.85 % (2708316)Peak memory usage: 152 MB
% 104.94/15.85 % (2708316)Instructions burned: 4920 (million)
% 104.94/15.85 % (2708330)Refutation not found, incomplete strategy
% 104.94/15.85 % (2708330)------------------------------
% 104.94/15.85 % (2708330)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 104.94/15.85 % (2708330)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 104.94/15.85 % (2708330)CaDiCaL version: 2.1.3
% 104.94/15.85 % (2708330)Termination reason: Refutation not found, incomplete strategy
% 104.94/15.85 % (2708330)Time elapsed: 0.548 s
% 104.94/15.85 % (2708330)Peak memory usage: 125 MB
% 104.94/15.85 % (2708330)Instructions burned: 826 (million)
% 104.94/15.85 % (2708328)------------------------------
% 104.94/15.85 % (2708328)------------------------------
% 104.94/15.85 % (2708334)lrs+10_1_ncem=casc2026/models/loop3.pt:sil=16000:tgt=ground:npcc=on:random_seed=3609442140:i=13942:kws=frequency_2861 on theBenchmark for (2861ds/13942Mi)
% 104.94/15.85 % (2708335)lrs-1002_1_to=lpo:ncem=casc2026/models/loop4.pt:sil=16000:npcc=on:bsd=on:sp=unary_frequency:spb=goal:lcm=predicate:acc=on:urr=full:bce=on:bsr=unit_only:s2agt=64:sac=on:random_seed=365089534:i=3604:fsr=off:er=filter_2860 on theBenchmark for (2860ds/3604Mi)
% 104.94/15.85 % (2708330)------------------------------
% 104.94/15.85 % (2708330)------------------------------
% 104.94/15.85 % (2708332)Refutation not found, incomplete strategy
% 104.94/15.85 % (2708332)------------------------------
% 104.94/15.85 % (2708332)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 104.94/15.85 % (2708332)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 104.94/15.85 % (2708332)CaDiCaL version: 2.1.3
% 104.94/15.85 % (2708332)Termination reason: Refutation not found, incomplete strategy
% 104.94/15.85 % (2708332)Time elapsed: 0.557 s
% 104.94/15.85 % (2708332)Peak memory usage: 127 MB
% 104.94/15.85 % (2708332)Instructions burned: 829 (million)
% 104.94/15.85 % (2708338)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=32000:npcc=on:random_seed=1481223261:i=1876:sd=1:ss=included:sgt=32_2858 on theBenchmark for (2858ds/1876Mi)
% 104.94/15.85 % (2708332)------------------------------
% 104.94/15.85 % (2708332)------------------------------
% 104.94/15.85 % (2708340)lrs+10_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:fde=none:sp=arity:urr=on:br=off:random_seed=589892163:i=1932:bd=preordered:ins=10:sup=off:ss=axioms_2855 on theBenchmark for (2855ds/1932Mi)
% 112.62/16.81 [W927 15:10:05.733495030 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.
% 112.62/16.81 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 112.62/16.81 [W927 15:10:05.733531291 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.
% 112.62/16.81 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 112.62/16.81 [W927 15:10:05.733569304 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.
% 112.62/16.81 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 112.62/16.81 [W927 15:10:05.733582804 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.
% 112.62/16.81 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 112.62/16.81 [W927 15:10:05.733609374 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.
% 112.62/16.81 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 112.62/16.81 [W927 15:10:05.733621648 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.
% 112.62/16.81 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 112.62/16.81 [W927 15:10:05.733647525 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.
% 112.62/16.81 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 112.62/16.81 [W927 15:10:05.733658838 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.
% 112.62/16.81 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 112.62/16.81 [W927 15:10:05.733683675 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.
% 112.62/16.81 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 112.62/16.81 [W927 15:10:05.733695108 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.
% 112.62/16.81 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 112.62/16.81 [W927 15:10:05.733720092 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.
% 112.62/16.81 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 112.62/16.81 [W927 15:10:05.733731359 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.
% 112.62/16.81 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 112.62/16.81 % (2708338)Refutation not found, incomplete strategy
% 112.62/16.81 % (2708338)------------------------------
% 112.62/16.81 % (2708338)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 126.75/18.76 % (2708338)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 126.75/18.76 % (2708338)CaDiCaL version: 2.1.3
% 126.75/18.76 % (2708338)Termination reason: Refutation not found, incomplete strategy
% 126.75/18.76 % (2708338)Time elapsed: 0.546 s
% 126.75/18.76 % (2708338)Peak memory usage: 125 MB
% 126.75/18.76 % (2708338)Instructions burned: 826 (million)
% 126.75/18.76 [W927 15:10:05.048660865 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.
% 126.75/18.76 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 126.75/18.76 [W927 15:10:05.048707745 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.
% 126.75/18.76 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 126.75/18.76 [W927 15:10:05.048745842 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.
% 126.75/18.76 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 126.75/18.76 [W927 15:10:05.048757646 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.
% 126.75/18.76 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 126.75/18.76 [W927 15:10:05.048782916 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.
% 126.75/18.76 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 126.75/18.76 [W927 15:10:05.048802343 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.
% 126.75/18.76 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 126.75/18.76 [W927 15:10:05.048829246 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.
% 126.75/18.76 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 126.75/18.76 [W927 15:10:05.048841136 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.
% 126.75/18.76 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 126.75/18.76 [W927 15:10:05.048866266 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.
% 126.75/18.76 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 126.75/18.76 [W927 15:10:05.048878487 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.
% 126.75/18.76 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 126.75/18.76 [W927 15:10:05.048904030 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.
% 126.75/18.76 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 126.75/18.76 [W927 15:10:05.048915570 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.
% 126.75/18.76 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 129.32/19.44 % (2708338)------------------------------
% 129.32/19.44 % (2708338)------------------------------
% 129.32/19.44 % (2708340)Refutation not found, incomplete strategy
% 129.32/19.44 % (2708340)------------------------------
% 129.32/19.44 % (2708340)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 129.32/19.44 % (2708340)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 129.32/19.44 % (2708340)CaDiCaL version: 2.1.3
% 129.32/19.44 % (2708340)Termination reason: Refutation not found, incomplete strategy
% 129.32/19.44 % (2708340)Time elapsed: 0.549 s
% 129.32/19.44 % (2708340)Peak memory usage: 125 MB
% 129.32/19.44 % (2708340)Instructions burned: 820 (million)
% 129.32/19.44 % (2708342)dis-1010_1_ncem=casc2026/models/loop1.pt:sil=8000:npcc=on:fde=unused:etr=on:sp=weighted_frequency:spb=goal_then_units:urr=ec_only:fd=preordered:kmz=on:random_seed=1407336131:s2pl=on:cond=fast:i=1980:s2at=2:kws=inv_precedence:doe=on:ins=1:av=off:gsp=on_2849 on theBenchmark for (2849ds/1980Mi)
% 129.32/19.44 % (2708340)------------------------------
% 129.32/19.44 % (2708340)------------------------------
% 129.32/19.44 % (2708344)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=unary_first:sos=all:spb=units:urr=on:br=off:random_seed=1306771028:i=3902:kws=inv_arity_squared:fgj=on:ss=axioms:sgt=11_2845 on theBenchmark for (2845ds/3902Mi)
% 129.32/19.44 % (2708312)Instruction limit reached!
% 129.32/19.44 % (2708312)------------------------------
% 129.32/19.44 % (2708312)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 129.32/19.44 % (2708312)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 129.32/19.44 % (2708312)CaDiCaL version: 2.1.3
% 129.32/19.44 % (2708312)Termination reason: Instruction limit
% 129.32/19.44 % (2708312)Termination phase: Saturation
% 129.32/19.44 % (2708312)Time elapsed: 5.557 s
% 129.32/19.44 % (2708312)Peak memory usage: 185 MB
% 129.32/19.44 % (2708312)Instructions burned: 9530 (million)
% 129.32/19.44 % (2708346)dis+10_32_sil=16000:tgt=ground:drc=off:sas=cadical:acc=on:alpa=false:avsqc=3:random_seed=2780997859:avsq=on:i=3916:aac=none:amm=off_2842 on theBenchmark for (2842ds/3916Mi)
% 129.32/19.44 [W927 15:10:06.007031169 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.
% 129.32/19.44 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 129.32/19.44 [W927 15:10:06.007060456 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.
% 129.32/19.44 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 129.32/19.44 [W927 15:10:06.007100496 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.
% 129.32/19.44 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 129.32/19.44 [W927 15:10:06.007113576 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.
% 129.32/19.44 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 129.32/19.44 [W927 15:10:06.007139946 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.
% 129.32/19.44 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 129.32/19.44 [W927 15:10:06.007151663 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.
% 129.32/19.44 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 129.32/19.44 [W927 15:10:06.007178253 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.
% 129.32/19.44 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 90.29/19.91 [W927 15:10:06.007190060 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.
% 90.29/19.91 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 90.29/19.91 [W927 15:10:06.007220367 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.
% 90.29/19.91 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 90.29/19.91 [W927 15:10:06.007240734 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.
% 90.29/19.91 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 90.29/19.91 [W927 15:10:06.007265784 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.
% 90.29/19.91 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 90.29/19.91 [W927 15:10:06.007276094 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.
% 90.29/19.91 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 90.29/19.91 % (2708344)Refutation not found, incomplete strategy
% 90.29/19.91 % (2708344)------------------------------
% 90.29/19.91 % (2708344)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 90.29/19.91 % (2708344)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 90.29/19.91 % (2708344)CaDiCaL version: 2.1.3
% 90.29/19.91 % (2708344)Termination reason: Refutation not found, incomplete strategy
% 90.29/19.91 % (2708344)Time elapsed: 0.543 s
% 90.29/19.91 % (2708344)Peak memory usage: 125 MB
% 90.29/19.91 % (2708344)Instructions burned: 825 (million)
% 90.29/19.91 % (2708335)Instruction limit reached!
% 90.29/19.91 % (2708335)------------------------------
% 90.29/19.91 % (2708335)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 90.29/19.91 % (2708335)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 90.29/19.91 % (2708335)CaDiCaL version: 2.1.3
% 90.29/19.91 % (2708335)Termination reason: Instruction limit
% 90.29/19.91 % (2708335)Termination phase: Saturation
% 90.29/19.91 % (2708335)Time elapsed: 2.003 s
% 90.29/19.91 % (2708335)Peak memory usage: 139 MB
% 90.29/19.91 % (2708335)Instructions burned: 3604 (million)
% 90.29/19.91 % (2708348)dis+10_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=full:npcc=on:drc=ordering:lcm=predicate:random_seed=3764433091:cond=on:i=3940:av=off:er=known_2838 on theBenchmark for (2838ds/3940Mi)
% 90.29/19.91 % (2708344)------------------------------
% 90.29/19.91 % (2708344)------------------------------
% 90.29/19.91 % (2708342)Instruction limit reached!
% 90.29/19.91 % (2708342)------------------------------
% 90.29/19.91 % (2708342)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 90.29/19.91 % (2708342)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 90.29/19.91 % (2708342)CaDiCaL version: 2.1.3
% 90.29/19.91 % (2708342)Termination reason: Instruction limit
% 90.29/19.91 % (2708342)Termination phase: Saturation
% 90.29/19.91 % (2708342)Time elapsed: 1.200 s
% 90.29/19.91 % (2708342)Peak memory usage: 137 MB
% 90.29/19.91 % (2708342)Instructions burned: 1980 (million)
% 90.29/19.91 % (2708350)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=reverse_frequency:bce=on:random_seed=4157653365:s2pl=on:i=3980:gtgl=3:kws=precedence:fgj=on:gtg=all_2836 on theBenchmark for (2836ds/3980Mi)
% 90.29/19.91 % (2708351)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:prc=on:sp=reverse_frequency:spb=units:lsd=20:urr=ec_only:bce=on:fd=off:kmz=on:random_seed=1447683964:i=2087:s2at=3:kws=frequency:av=off:fsr=off_2835 on theBenchmark for (2835ds/2087Mi)
% 90.29/19.91 % (2708351)Instruction limit reached!
% 90.29/19.91 % (2708351)------------------------------
% 90.29/19.91 % (2708351)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 135.30/20.11 % (2708351)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 135.30/20.11 % (2708351)CaDiCaL version: 2.1.3
% 135.30/20.11 % (2708351)Termination reason: Instruction limit
% 135.30/20.11 % (2708351)Termination phase: Saturation
% 135.30/20.11 % (2708351)Time elapsed: 1.279 s
% 135.30/20.11 % (2708351)Peak memory usage: 142 MB
% 135.30/20.11 % (2708351)Instructions burned: 2088 (million)
% 135.30/20.11 % (2708346)Instruction limit reached!
% 135.30/20.11 % (2708346)------------------------------
% 135.30/20.11 % (2708346)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 135.30/20.11 % (2708346)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 135.30/20.11 % (2708346)CaDiCaL version: 2.1.3
% 135.30/20.11 % (2708346)Termination reason: Instruction limit
% 135.30/20.11 % (2708346)Termination phase: Saturation
% 135.30/20.11 % (2708346)Time elapsed: 2.097 s
% 135.30/20.11 % (2708346)Peak memory usage: 123 MB
% 135.30/20.11 % (2708346)Instructions burned: 3918 (million)
% 135.30/20.11 % (2708354)ott-1004_1_anc=all_dependent:to=lpo:ncem=casc2026/models/loop5.pt:sil=8000:tgt=full:npcc=on:sas=cadical:sp=const_frequency:acc=on:urr=ec_only:gs=on:s2agt=40:alpa=false:sac=on:random_seed=2268698355:cts=off:cond=on:i=4272:bs=on:fsd=on_2820 on theBenchmark for (2820ds/4272Mi)
% 135.30/20.11 % (2708355)lrs-30_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:urr=on:bce=on:rp=on:br=off:flr=on:random_seed=589006796:st=-1:i=2197:kws=precedence:av=off:ss=axioms:er=known_2819 on theBenchmark for (2819ds/2197Mi)
% 135.30/20.11 % (2708348)Instruction limit reached!
% 135.30/20.11 % (2708348)------------------------------
% 135.30/20.11 % (2708348)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 135.30/20.11 % (2708348)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 135.30/20.11 % (2708348)CaDiCaL version: 2.1.3
% 135.30/20.11 % (2708348)Termination reason: Instruction limit
% 135.30/20.11 % (2708348)Termination phase: Saturation
% 135.30/20.11 % (2708348)Time elapsed: 2.239 s
% 135.30/20.11 % (2708348)Peak memory usage: 157 MB
% 135.30/20.11 % (2708348)Instructions burned: 3942 (million)
% 135.30/20.11 [W927 15:10:09.636326904 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.
% 135.30/20.11 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 135.30/20.11 [W927 15:10:09.636375074 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.
% 135.30/20.11 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 135.30/20.11 [W927 15:10:09.636414321 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.
% 135.30/20.11 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 135.30/20.11 [W927 15:10:09.636427171 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.
% 135.30/20.11 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 135.30/20.11 [W927 15:10:09.636453352 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.
% 135.30/20.11 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 135.30/20.11 [W927 15:10:09.636465398 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.
% 135.30/20.11 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 135.30/20.11 [W927 15:10:09.636490938 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.
% 135.30/20.11 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 135.30/20.11 [W927 15:10:09.636502815 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.
% 135.30/20.11 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 135.30/20.11 [W927 15:10:09.636526705 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.
% 135.30/20.11 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 135.30/20.11 [W927 15:10:09.636546389 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.
% 135.30/20.11 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 135.30/20.11 [W927 15:10:09.636572346 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.
% 135.30/20.11 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 135.30/20.11 [W927 15:10:09.636582942 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.
% 135.30/20.11 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 135.30/20.11 % (2708358)dis+21_1_sil=8000:spb=goal_then_units:random_seed=1063118585:avsq=on:i=6508:avsqr=1,16:kws=arity_squared:fgj=on_2814 on theBenchmark for (2814ds/6508Mi)
% 135.30/20.11 % (2708358)First to succeed.
% 135.30/20.11 % (2708358)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2708219"
% 135.30/20.11 % (2708355)Refutation not found, incomplete strategy
% 135.30/20.11 % (2708355)------------------------------
% 135.30/20.11 % (2708355)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 135.30/20.11 % (2708355)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 135.30/20.11 % (2708355)CaDiCaL version: 2.1.3
% 135.30/20.11 % (2708355)Termination reason: Refutation not found, incomplete strategy
% 135.30/20.11 % (2708355)Time elapsed: 0.549 s
% 135.30/20.11 % (2708355)Peak memory usage: 125 MB
% 135.30/20.11 % (2708355)Instructions burned: 826 (million)
% 135.30/20.11 % (2708350)Instruction limit reached!
% 135.30/20.11 % (2708350)------------------------------
% 135.30/20.11 % (2708350)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 135.30/20.11 % (2708350)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 135.30/20.11 % (2708350)CaDiCaL version: 2.1.3
% 135.30/20.11 % (2708350)Termination reason: Instruction limit
% 135.30/20.11 % (2708350)Termination phase: Saturation
% 135.30/20.11 % (2708350)Time elapsed: 2.391 s
% 135.30/20.11 % (2708350)Peak memory usage: 154 MB
% 135.30/20.11 % (2708350)Instructions burned: 3980 (million)
% 135.30/20.11 % (2708355)------------------------------
% 135.30/20.11 % (2708355)------------------------------
% 135.30/20.11 % SZS status Satisfiable for theBenchmark
% 135.30/20.11 % SZS output start Saturation.
% See solution above
% 135.30/20.11 % SZS output start Definitions and Model Updates.
% 135.30/20.11 % SZS output end Definitions and Model Updates.
% 135.30/20.11 % (2708358)------------------------------
% 135.30/20.11 % (2708358)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 135.30/20.11 % (2708358)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 135.30/20.11 % (2708358)CaDiCaL version: 2.1.3
% 135.30/20.11 % (2708358)Termination reason: Satisfiable
% 135.30/20.11 % (2708358)Time elapsed: 0.049 s
% 135.30/20.11 % (2708358)Peak memory usage: 89 MB
% 135.30/20.11 % (2708358)Instructions burned: 84 (million)
% 135.30/20.11 % (2708358)------------------------------
% 135.30/20.11 % (2708358)------------------------------
% 135.30/20.11 % (2708219)Success in time 19.042 s
% 135.30/20.11 % Vampire exiting
%------------------------------------------------------------------------------