%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LAT058-1 : TPTP v9.3.1. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n003.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 11:45:55 AM UTC 2026
% Result : Satisfiable 231.65s 33.63s
% Output : Saturation 231.65s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u2739,axiom,
n0 = n1 ).
cnf(u2743,axiom,
n1 = X0 ).
cnf(u5441,axiom,
join(X1,X0) = n1 ).
cnf(unique_complement3,axiom,
( complement(X0,f(X0,X1))
| ~ complement(X0,X1)
| unique_complement(X0,X1) ) ).
cnf(u2985,axiom,
( meet(X1,X0) = X0
| n0 != X0 ) ).
cnf(u4225,axiom,
X0 = X1 ).
cnf(u657,axiom,
join(X1,meet(X0,meet(X1,X2))) = X1 ).
cnf(u205,axiom,
meet(X2,join(X0,join(X1,X2))) = X2 ).
cnf(u562,axiom,
meet(X0,join(X2,join(X0,X1))) = X0 ).
cnf(u217,axiom,
meet(X1,X0) = meet(X0,meet(X1,X0)) ).
cnf(u138,axiom,
( meet(X1,X0) != X1
| meet(X0,X1) = X1 ) ).
cnf(u71,axiom,
meet(X0,meet(X1,X2)) = meet(X1,meet(X2,X0)) ).
cnf(u9201,axiom,
( unique_complement(X0,X1)
| ~ complement(X0,X1)
| complement(X0,n0) ) ).
cnf(u45,axiom,
n1 = join(n1,X0) ).
cnf(u2678,axiom,
( join(X0,join(X1,X2)) = n1
| n1 != X2 ) ).
cnf(x_meet_1,axiom,
meet(X0,n1) = X0 ).
cnf(u212,axiom,
meet(X0,X2) = meet(X0,meet(join(X1,X0),X2)) ).
cnf(u113,axiom,
( ~ unique_complement(X0,X2)
| unique_complement(X0,X1)
| ~ complement(X0,X1)
| f(X0,X1) = X2 ) ).
cnf(u2677,axiom,
( join(X0,join(X1,X2)) = n1
| n1 != X1 ) ).
cnf(u192,axiom,
join(X0,X2) = join(X0,join(meet(X1,X0),X2)) ).
cnf(unique_complement4,axiom,
( unique_complement(X0,X1)
| ~ complement(X0,X1)
| f(X0,X1) != X1 ) ).
cnf(u30,axiom,
meet(n1,X0) = X0 ).
cnf(u121,axiom,
( meet(X2,join(X3,meet(X0,X1))) = join(X3,meet(X0,meet(X1,X2)))
| meet(X3,X2) != X3 ) ).
cnf(absorption1,axiom,
meet(X0,join(X0,X1)) = X0 ).
cnf(u2666,axiom,
( join(X0,X1) = n1
| n1 != X1 ) ).
cnf(x_join_0,axiom,
join(X0,n0) = X0 ).
cnf(u29,axiom,
n0 = meet(n0,X0) ).
cnf(u185,axiom,
join(X2,meet(X0,meet(X1,X2))) = X2 ).
cnf(u1640,axiom,
( join(X0,X1) = X0
| meet(X1,X0) != X1 ) ).
cnf(commutativity_of_join,axiom,
join(X0,X1) = join(X1,X0) ).
cnf(associativity_of_join,axiom,
join(join(X0,X1),X2) = join(X0,join(X1,X2)) ).
cnf(u97,axiom,
join(X0,join(X1,X2)) = join(X1,join(X2,X0)) ).
cnf(u18,axiom,
( ~ complement(X0,X2)
| ~ unique_complement(X0,X1)
| X1 = X2 ) ).
cnf(u1639,axiom,
( join(X1,X0) = X0
| meet(X1,X0) != X1 ) ).
cnf(u2980,axiom,
( join(X0,X1) = X0
| n0 != X1 ) ).
cnf(unique_complement1,axiom,
( ~ unique_complement(X0,X1)
| complement(X0,X1) ) ).
cnf(absorption2,axiom,
join(X0,meet(X0,X1)) = X0 ).
cnf(u14,axiom,
n1 = join(X0,n1) ).
cnf(u3062,axiom,
( meet(X0,X1) != n1
| n1 = X0 ) ).
cnf(u131,axiom,
( join(X1,join(meet(X2,X0),X3)) = join(meet(X0,join(X1,X2)),X3)
| meet(X1,X0) != X1 ) ).
cnf(u896,axiom,
join(X1,X0) = join(X1,join(X0,meet(X1,X2))) ).
cnf(u216,axiom,
join(X1,X0) = join(X0,join(X1,X0)) ).
cnf(u44,axiom,
join(n0,X0) = X0 ).
cnf(commutativity_of_meet,axiom,
meet(X0,X1) = meet(X1,X0) ).
cnf(modular,axiom,
( meet(X1,join(X0,X2)) = join(X0,meet(X2,X1))
| meet(X0,X1) != X0 ) ).
cnf(u521,axiom,
meet(X1,X0) = meet(X1,meet(X0,join(X1,X2))) ).
cnf(u9400,axiom,
( ~ complement(X1,X2)
| complement(X1,X0)
| unique_complement(X1,X2) ) ).
cnf(u2660,axiom,
( join(X1,X2) = n1
| n1 != X1 ) ).
cnf(u62,axiom,
meet(meet(X0,X1),X2) = meet(X1,meet(X0,X2)) ).
cnf(u90,axiom,
join(join(X0,X1),X2) = join(X1,join(X0,X2)) ).
cnf(u134,axiom,
( meet(X1,meet(X0,join(X1,X2))) = X1
| meet(X1,X0) != X1 ) ).
cnf(u136,axiom,
( join(X1,join(X2,meet(X3,X0))) = meet(X0,join(X1,join(X2,X3)))
| join(X1,X2) != meet(join(X1,X2),X0) ) ).
cnf(u118,axiom,
( join(X2,X0) = meet(join(X0,X1),join(X2,X0))
| meet(X2,join(X0,X1)) != X2 ) ).
cnf(u105,axiom,
join(X0,X1) = meet(join(X0,X1),join(X0,join(X1,X2))) ).
cnf(u79,axiom,
meet(X0,X1) = join(meet(X0,X1),meet(X0,meet(X1,X2))) ).
cnf(idempotence_of_join,axiom,
join(X0,X0) = X0 ).
cnf(u3518,axiom,
( n0 != X1
| n0 != X0
| X0 = X1 ) ).
cnf(u2662,axiom,
( join(X0,X2) = X2
| n0 != X0 ) ).
cnf(u116,axiom,
( meet(X0,join(X2,X1)) = join(X2,meet(X0,X1))
| meet(X2,X0) != X2 ) ).
cnf(u33,axiom,
join(X1,meet(X0,X1)) = X1 ).
cnf(u2982,axiom,
( meet(X0,X1) = X0
| n0 != X0 ) ).
cnf(u126,axiom,
( join(meet(X0,X1),X2) = meet(X1,join(X2,X0))
| meet(X2,X1) != X2 ) ).
cnf(u73,axiom,
meet(X0,X1) = meet(X0,meet(X1,join(meet(X0,X1),X2))) ).
cnf(u61,axiom,
meet(X0,X1) = meet(X0,meet(X0,X1)) ).
cnf(u89,axiom,
join(X0,X1) = join(X0,join(X0,X1)) ).
cnf(u10,axiom,
n0 = meet(X0,n0) ).
cnf(u99,axiom,
join(X0,X1) = join(X0,join(X1,meet(join(X0,X1),X2))) ).
cnf(u3065,axiom,
( meet(X1,X0) != n1
| n1 = X0 ) ).
cnf(idempotence_of_meet,axiom,
meet(X0,X0) = X0 ).
cnf(u2745,axiom,
( n1 != meet(X0,X2)
| join(X0,X1) = n1 ) ).
cnf(u64,axiom,
meet(X0,X2) = meet(X0,meet(join(X0,X1),X2)) ).
cnf(associativity_of_meet,axiom,
meet(meet(X0,X1),X2) = meet(X0,meet(X1,X2)) ).
cnf(u48,axiom,
meet(X1,join(X0,X1)) = X1 ).
cnf(u92,axiom,
join(X0,X2) = join(X0,join(meet(X0,X1),X2)) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT058-1 : TPTP v9.3.1. Released v2.5.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.13/0.39 % Computer : n003.cluster.edu
% 0.13/0.39 % Model : x86_64 x86_64
% 0.13/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.39 % Memory : 8046.5625MB
% 0.13/0.39 % OS : Linux 6.8.0-71-generic
% 0.13/0.39 % CPULimit : 300
% 0.13/0.39 % WCLimit : 300
% 0.13/0.39 % DateTime : Sun Sep 27 14:00:26 UTC 2026
% 0.13/0.39 % CPUTime :
% 0.13/0.40 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.13/0.45 Running first-order theorem proving
% 0.13/0.45 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
% 14.06/2.74 % (548278)Input is clausal, will run a generic CNF schedule.
% 14.06/2.74 % (548291)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=4063945172:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_3000 on theBenchmark for (3000ds/137899Mi)
% 14.06/2.74 % (548294)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2710730416:s2a=on:i=180:gtg=position_3000 on theBenchmark for (3000ds/180Mi)
% 14.06/2.74 % (548290)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=4287837597:i=132376:av=off_3000 on theBenchmark for (3000ds/132376Mi)
% 14.06/2.74 % (548293)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=3502290110:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_3000 on theBenchmark for (3000ds/114Mi)
% 14.06/2.74 % (548295)dis-21_1_sil=8000:lcm=predicate:random_seed=1178933063:st=5:avsq=on:i=117:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_3000 on theBenchmark for (3000ds/117Mi)
% 14.06/2.74 % (548292)lrs+10_1_sil=8000:sp=occurrence:random_seed=3484345559:i=107:sd=3:ss=axioms:sgt=8_3000 on theBenchmark for (3000ds/107Mi)
% 14.06/2.74 % (548289)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=4221413627:i=140167_3000 on theBenchmark for (3000ds/140167Mi)
% 14.06/2.74 % (548295)Refutation not found, incomplete strategy
% 14.06/2.74 % (548295)------------------------------
% 14.06/2.74 % (548295)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.06/2.74 % (548295)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.06/2.74 % (548295)CaDiCaL version: 2.1.3
% 14.06/2.74 % (548295)Termination reason: Refutation not found, incomplete strategy
% 14.06/2.74 % (548295)Time elapsed: 0.001 s
% 14.06/2.74 % (548293)Refutation not found, incomplete strategy
% 14.06/2.74 % (548293)------------------------------
% 14.06/2.74 % (548293)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.06/2.74 % (548295)Peak memory usage: 86 MB
% 14.06/2.74 % (548293)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.06/2.74 % (548293)CaDiCaL version: 2.1.3
% 14.06/2.74 % (548293)Termination reason: Refutation not found, incomplete strategy
% 14.06/2.74 % (548293)Time elapsed: 0.001 s
% 14.06/2.74 % (548293)Peak memory usage: 86 MB
% 14.06/2.74 % (548292)Refutation not found, incomplete strategy
% 14.06/2.74 % (548292)------------------------------
% 14.06/2.74 % (548292)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.06/2.74 % (548292)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.06/2.74 % (548292)CaDiCaL version: 2.1.3
% 14.06/2.74 % (548292)Termination reason: Refutation not found, incomplete strategy
% 14.06/2.74 % (548292)Time elapsed: 0.001 s
% 14.06/2.74 % (548292)Peak memory usage: 86 MB
% 14.06/2.74 % (548294)Instruction limit reached!
% 14.06/2.74 % (548294)------------------------------
% 14.06/2.74 % (548294)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.06/2.74 % (548294)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.06/2.74 % (548294)CaDiCaL version: 2.1.3
% 14.06/2.74 % (548294)Termination reason: Instruction limit
% 14.06/2.74 % (548294)Termination phase: Saturation
% 14.06/2.74 % (548294)Time elapsed: 0.159 s
% 14.06/2.74 % (548294)Peak memory usage: 89 MB
% 14.06/2.74 % (548294)Instructions burned: 180 (million)
% 14.06/2.74 % (548293)------------------------------
% 14.06/2.74 % (548293)------------------------------
% 14.06/2.74 % (548307)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=1334003442:i=143:sd=2:aac=none:ss=axioms:sgt=16_2996 on theBenchmark for (2996ds/143Mi)
% 14.06/2.74 % (548307)Refutation not found, incomplete strategy
% 14.06/2.74 % (548307)------------------------------
% 14.06/2.74 % (548307)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.06/2.74 % (548307)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.06/2.74 % (548307)CaDiCaL version: 2.1.3
% 14.06/2.74 % (548307)Termination reason: Refutation not found, incomplete strategy
% 14.06/2.74 % (548307)Time elapsed: 0.001 s
% 14.06/2.74 % (548307)Peak memory usage: 86 MB
% 14.06/2.74 % (548292)------------------------------
% 14.06/2.74 % (548292)------------------------------
% 14.06/2.74 % (548295)------------------------------
% 14.06/2.74 % (548295)------------------------------
% 14.06/2.74 % (548313)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=3902540515:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2994 on theBenchmark for (2994ds/189Mi)
% 19.34/3.58 % (548313)Refutation not found, incomplete strategy
% 19.34/3.58 % (548313)------------------------------
% 19.34/3.58 % (548313)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.34/3.58 % (548313)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.34/3.58 % (548313)CaDiCaL version: 2.1.3
% 19.34/3.58 % (548313)Termination reason: Refutation not found, incomplete strategy
% 19.34/3.58 % (548313)Time elapsed: 0.001 s
% 19.34/3.58 % (548313)Peak memory usage: 86 MB
% 19.34/3.58 % (548314)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=4081569765:st=4:i=219:sd=3:ss=axioms_2994 on theBenchmark for (2994ds/219Mi)
% 19.34/3.58 % (548314)Refutation not found, incomplete strategy
% 19.34/3.58 % (548314)------------------------------
% 19.34/3.58 % (548314)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.34/3.58 % (548314)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.34/3.58 % (548314)CaDiCaL version: 2.1.3
% 19.34/3.58 % (548314)Termination reason: Refutation not found, incomplete strategy
% 19.34/3.58 % (548314)Time elapsed: 0.001 s
% 19.34/3.58 % (548314)Peak memory usage: 86 MB
% 19.34/3.58 % (548315)lrs+10_64_to=lpo:sil=8000:random_seed=482518754:i=126:bd=preordered_2994 on theBenchmark for (2994ds/126Mi)
% 19.34/3.58 % (548307)------------------------------
% 19.34/3.58 % (548307)------------------------------
% 19.34/3.58 % (548315)Instruction limit reached!
% 19.34/3.58 % (548315)------------------------------
% 19.34/3.58 % (548315)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.34/3.58 % (548315)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.34/3.58 % (548315)CaDiCaL version: 2.1.3
% 19.34/3.58 % (548315)Termination reason: Instruction limit
% 19.34/3.58 % (548315)Termination phase: Saturation
% 19.34/3.58 % (548315)Time elapsed: 0.122 s
% 19.34/3.58 % (548315)Peak memory usage: 88 MB
% 19.34/3.58 % (548315)Instructions burned: 126 (million)
% 19.34/3.58 % (548313)------------------------------
% 19.34/3.58 % (548313)------------------------------
% 19.34/3.58 % (548326)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=815971470:i=157:gtg=all_2990 on theBenchmark for (2990ds/157Mi)
% 19.34/3.58 % (548325)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=3758616163:avsq=on:i=194:fgj=on:bd=preordered_2990 on theBenchmark for (2990ds/194Mi)
% 19.34/3.58 % (548314)------------------------------
% 19.34/3.58 % (548314)------------------------------
% 19.34/3.58 % (548326)Instruction limit reached!
% 19.34/3.58 % (548326)------------------------------
% 19.34/3.58 % (548326)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.34/3.58 % (548326)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.34/3.58 % (548326)CaDiCaL version: 2.1.3
% 19.34/3.58 % (548326)Termination reason: Instruction limit
% 19.34/3.58 % (548326)Termination phase: Saturation
% 19.34/3.58 % (548326)Time elapsed: 0.145 s
% 19.34/3.58 % (548326)Peak memory usage: 89 MB
% 19.34/3.58 % (548326)Instructions burned: 159 (million)
% 19.34/3.58 % (548325)Instruction limit reached!
% 19.34/3.58 % (548325)------------------------------
% 19.34/3.58 % (548325)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.34/3.58 % (548325)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.34/3.58 % (548325)CaDiCaL version: 2.1.3
% 19.34/3.58 % (548325)Termination reason: Instruction limit
% 19.34/3.58 % (548325)Termination phase: Saturation
% 19.34/3.58 % (548325)Time elapsed: 0.184 s
% 19.34/3.58 % (548325)Peak memory usage: 89 MB
% 19.34/3.58 % (548325)Instructions burned: 194 (million)
% 19.34/3.58 % (548328)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=805389584:i=3394:sd=4:ss=included:sgt=64_2988 on theBenchmark for (2988ds/3394Mi)
% 19.34/3.58 % (548331)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=2110034020:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2987 on theBenchmark for (2987ds/106Mi)
% 19.34/3.58 % (548331)Refutation not found, incomplete strategy
% 19.34/3.58 % (548331)------------------------------
% 19.34/3.58 % (548331)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.34/3.58 % (548331)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.64/5.00 % (548331)CaDiCaL version: 2.1.3
% 28.64/5.00 % (548331)Termination reason: Refutation not found, incomplete strategy
% 28.64/5.00 % (548331)Time elapsed: 0.001 s
% 28.64/5.00 % (548331)Peak memory usage: 86 MB
% 28.64/5.00 % (548333)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=638251359:i=107_2986 on theBenchmark for (2986ds/107Mi)
% 28.64/5.00 % (548333)Refutation not found, incomplete strategy
% 28.64/5.00 % (548333)------------------------------
% 28.64/5.00 % (548333)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.64/5.00 % (548333)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.64/5.00 % (548333)CaDiCaL version: 2.1.3
% 28.64/5.00 % (548333)Termination reason: Refutation not found, incomplete strategy
% 28.64/5.00 % (548333)Time elapsed: 0.001 s
% 28.64/5.00 % (548333)Peak memory usage: 87 MB
% 28.64/5.00 % (548336)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=1668941326:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2986 on theBenchmark for (2986ds/242Mi)
% 28.64/5.00 % (548336)Refutation not found, incomplete strategy
% 28.64/5.00 % (548336)------------------------------
% 28.64/5.00 % (548336)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.64/5.00 % (548336)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.64/5.00 % (548336)CaDiCaL version: 2.1.3
% 28.64/5.00 % (548336)Termination reason: Refutation not found, incomplete strategy
% 28.64/5.00 % (548336)Time elapsed: 0.001 s
% 28.64/5.00 % (548336)Peak memory usage: 86 MB
% 28.64/5.00 % (548331)------------------------------
% 28.64/5.00 % (548331)------------------------------
% 28.64/5.00 % (548333)------------------------------
% 28.64/5.00 % (548333)------------------------------
% 28.64/5.00 % (548336)------------------------------
% 28.64/5.00 % (548336)------------------------------
% 28.64/5.00 % (548343)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=3898709425:cond=fast:i=5208:av=off_2981 on theBenchmark for (2981ds/5208Mi)
% 28.64/5.00 [W927 14:00:29.317287421 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 28.64/5.00 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 28.64/5.00 [W927 14:00:29.317337929 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 28.64/5.00 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 28.64/5.00 [W927 14:00:29.317397873 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 28.64/5.00 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 28.64/5.00 [W927 14:00:29.317420120 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 28.64/5.00 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 28.64/5.00 [W927 14:00:29.317468334 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 28.64/5.00 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 28.64/5.00 [W927 14:00:29.317488517 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 28.64/5.00 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 28.64/5.00 [W927 14:00:29.317535424 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 60.37/9.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 60.37/9.23 [W927 14:00:29.317555998 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 60.37/9.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 60.37/9.23 [W927 14:00:29.317604965 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 60.37/9.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 60.37/9.23 [W927 14:00:29.317685266 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 60.37/9.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 60.37/9.23 [W927 14:00:29.317747214 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 60.37/9.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 60.37/9.23 [W927 14:00:29.317766417 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 60.37/9.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 60.37/9.23 % (548345)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=283048634:i=134:sd=2:doe=on:ss=axioms:sgt=14_2980 on theBenchmark for (2980ds/134Mi)
% 60.37/9.23 % (548345)Refutation not found, incomplete strategy
% 60.37/9.23 % (548345)------------------------------
% 60.37/9.23 % (548345)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 60.37/9.23 % (548345)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 60.37/9.23 % (548345)CaDiCaL version: 2.1.3
% 60.37/9.23 % (548345)Termination reason: Refutation not found, incomplete strategy
% 60.37/9.23 % (548345)Time elapsed: 0.001 s
% 60.37/9.23 % (548345)Peak memory usage: 86 MB
% 60.37/9.23 % (548346)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=957215720:i=499:bd=all_2980 on theBenchmark for (2980ds/499Mi)
% 60.37/9.23 % (548328)Refutation not found, incomplete strategy
% 60.37/9.23 % (548328)------------------------------
% 60.37/9.23 % (548328)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 60.37/9.23 % (548328)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 60.37/9.23 % (548328)CaDiCaL version: 2.1.3
% 60.37/9.23 % (548328)Termination reason: Refutation not found, incomplete strategy
% 60.37/9.23 % (548328)Time elapsed: 0.880 s
% 60.37/9.23 % (548328)Peak memory usage: 125 MB
% 60.37/9.23 % (548328)Instructions burned: 820 (million)
% 60.37/9.23 % (548345)------------------------------
% 60.37/9.23 % (548345)------------------------------
% 60.37/9.23 % (548328)------------------------------
% 60.37/9.23 % (548328)------------------------------
% 60.37/9.23 % (548346)Instruction limit reached!
% 60.37/9.23 % (548346)------------------------------
% 60.37/9.23 % (548346)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 60.37/9.23 % (548346)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 60.37/9.23 % (548346)CaDiCaL version: 2.1.3
% 60.37/9.23 % (548346)Termination reason: Instruction limit
% 60.37/9.23 % (548346)Termination phase: Saturation
% 60.37/9.23 % (548346)Time elapsed: 0.475 s
% 60.37/9.23 % (548346)Peak memory usage: 93 MB
% 60.37/9.23 % (548346)Instructions burned: 499 (million)
% 60.37/9.23 % (548357)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=16415798:i=191:fgj=on:bd=all_2975 on theBenchmark for (2975ds/191Mi)
% 60.37/9.23 % (548357)Instruction limit reached!
% 60.37/9.23 % (548357)------------------------------
% 60.37/9.23 % (548357)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 60.37/9.23 % (548357)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 60.37/9.23 % (548357)CaDiCaL version: 2.1.3
% 60.37/9.23 % (548357)Termination reason: Instruction limit
% 61.79/9.48 % (548357)Termination phase: Saturation
% 61.79/9.48 % (548357)Time elapsed: 0.193 s
% 61.79/9.48 % (548357)Peak memory usage: 90 MB
% 61.79/9.48 % (548357)Instructions burned: 191 (million)
% 61.79/9.48 % (548361)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=3961578647:i=264:kws=precedence:fsr=off_2973 on theBenchmark for (2973ds/264Mi)
% 61.79/9.48 % (548362)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=143732472:cond=on:i=156:bs=on:gtg=exists_all:er=known_2973 on theBenchmark for (2973ds/156Mi)
% 61.79/9.48 % (548362)Instruction limit reached!
% 61.79/9.48 % (548362)------------------------------
% 61.79/9.48 % (548362)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 61.79/9.48 % (548362)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 61.79/9.48 % (548362)CaDiCaL version: 2.1.3
% 61.79/9.48 % (548362)Termination reason: Instruction limit
% 61.79/9.48 % (548362)Termination phase: Saturation
% 61.79/9.48 % (548362)Time elapsed: 0.152 s
% 61.79/9.48 % (548362)Peak memory usage: 88 MB
% 61.79/9.48 % (548362)Instructions burned: 156 (million)
% 61.79/9.48 % (548365)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=1511495642:i=3256:kws=precedence:bd=preordered:av=off_2971 on theBenchmark for (2971ds/3256Mi)
% 61.79/9.48 % (548361)Instruction limit reached!
% 61.79/9.48 % (548361)------------------------------
% 61.79/9.48 % (548361)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 61.79/9.48 % (548361)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 61.79/9.48 % (548361)CaDiCaL version: 2.1.3
% 61.79/9.48 % (548361)Termination reason: Instruction limit
% 61.79/9.48 % (548361)Termination phase: Saturation
% 61.79/9.48 % (548361)Time elapsed: 0.243 s
% 61.79/9.48 % (548361)Peak memory usage: 91 MB
% 61.79/9.48 % (548361)Instructions burned: 265 (million)
% 61.79/9.48 % (548369)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=1001424017:i=537:av=off:ss=included_2969 on theBenchmark for (2969ds/537Mi)
% 61.79/9.48 % (548369)Refutation not found, incomplete strategy
% 61.79/9.48 % (548369)------------------------------
% 61.79/9.48 % (548369)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 61.79/9.48 % (548369)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 61.79/9.48 % (548369)CaDiCaL version: 2.1.3
% 61.79/9.48 % (548369)Termination reason: Refutation not found, incomplete strategy
% 61.79/9.48 % (548369)Time elapsed: 0.001 s
% 61.79/9.48 % (548369)Peak memory usage: 86 MB
% 61.79/9.48 % (548372)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=3539488062:i=180:bd=preordered:av=off_2968 on theBenchmark for (2968ds/180Mi)
% 61.79/9.48 % (548372)Instruction limit reached!
% 61.79/9.48 % (548372)------------------------------
% 61.79/9.48 % (548372)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 61.79/9.48 % (548372)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 61.79/9.48 % (548372)CaDiCaL version: 2.1.3
% 61.79/9.48 % (548372)Termination reason: Instruction limit
% 61.79/9.48 % (548372)Termination phase: Saturation
% 61.79/9.48 % (548372)Time elapsed: 0.174 s
% 61.79/9.48 % (548372)Peak memory usage: 88 MB
% 61.79/9.48 % (548372)Instructions burned: 180 (million)
% 61.79/9.48 % (548369)------------------------------
% 61.79/9.48 % (548369)------------------------------
% 61.79/9.48 % (548377)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=127551997:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2965 on theBenchmark for (2965ds/10307Mi)
% 61.79/9.48 % (548378)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=694262589:i=412:gtgl=4:gtg=exists_all_2963 on theBenchmark for (2963ds/412Mi)
% 61.79/9.48 % (548378)Instruction limit reached!
% 61.79/9.48 % (548378)------------------------------
% 61.79/9.48 % (548378)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 61.79/9.48 % (548378)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 61.79/9.48 % (548378)CaDiCaL version: 2.1.3
% 61.79/9.48 % (548378)Termination reason: Instruction limit
% 61.79/9.48 % (548378)Termination phase: Saturation
% 61.79/9.48 % (548378)Time elapsed: 0.375 s
% 61.79/9.48 % (548378)Peak memory usage: 90 MB
% 61.79/9.48 % (548378)Instructions burned: 412 (million)
% 87.66/13.07 % (548383)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=209329898:s2pl=no:i=8478:s2at=4:nm=6_2957 on theBenchmark for (2957ds/8478Mi)
% 87.66/13.07 % (548365)Instruction limit reached!
% 87.66/13.07 % (548365)------------------------------
% 87.66/13.07 % (548365)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 87.66/13.07 % (548365)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 87.66/13.07 % (548365)CaDiCaL version: 2.1.3
% 87.66/13.07 % (548365)Termination reason: Instruction limit
% 87.66/13.07 % (548365)Termination phase: Saturation
% 87.66/13.07 % (548365)Time elapsed: 3.285 s
% 87.66/13.07 % (548365)Peak memory usage: 148 MB
% 87.66/13.07 % (548365)Instructions burned: 3256 (million)
% 87.66/13.07 % (548387)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=2840750163:s2a=on:i=303:s2at=2:sd=1:kws=inv_arity:bs=on:ins=10:fdi=1024:sup=off:ss=included_2936 on theBenchmark for (2936ds/303Mi)
% 87.66/13.07 % (548387)Refutation not found, incomplete strategy
% 87.66/13.07 % (548387)------------------------------
% 87.66/13.07 % (548387)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 87.66/13.07 % (548387)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 87.66/13.07 % (548387)CaDiCaL version: 2.1.3
% 87.66/13.07 % (548387)Termination reason: Refutation not found, incomplete strategy
% 87.66/13.07 % (548387)Time elapsed: 0.001 s
% 87.66/13.07 % (548387)Peak memory usage: 87 MB
% 87.66/13.07 % (548387)------------------------------
% 87.66/13.07 % (548387)------------------------------
% 87.66/13.07 % (548393)lrs+10_1_to=lpo:sil=16000:fde=none:sos=on:urr=on:bsr=on:random_seed=522304580:st=4:i=720:sd=3:fsr=off:ss=axioms_2929 on theBenchmark for (2929ds/720Mi)
% 87.66/13.07 % (548393)Refutation not found, incomplete strategy
% 87.66/13.07 % (548393)------------------------------
% 87.66/13.07 % (548393)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 87.66/13.07 % (548393)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 87.66/13.07 % (548393)CaDiCaL version: 2.1.3
% 87.66/13.07 % (548393)Termination reason: Refutation not found, incomplete strategy
% 87.66/13.07 % (548393)Time elapsed: 0.001 s
% 87.66/13.07 % (548393)Peak memory usage: 86 MB
% 87.66/13.07 % (548343)Instruction limit reached!
% 87.66/13.07 % (548343)------------------------------
% 87.66/13.07 % (548343)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 87.66/13.07 % (548343)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 87.66/13.07 % (548343)CaDiCaL version: 2.1.3
% 87.66/13.07 % (548343)Termination reason: Instruction limit
% 87.66/13.07 % (548343)Termination phase: Saturation
% 87.66/13.07 % (548343)Time elapsed: 5.307 s
% 87.66/13.07 % (548343)Peak memory usage: 163 MB
% 87.66/13.07 % (548343)Instructions burned: 5208 (million)
% 87.66/13.07 % (548396)lrs-20_1_to=lpo:sil=32000:tgt=ground:sp=reverse_frequency:spb=goal:urr=on:bsr=unit_only:nwc=1.5:random_seed=3459607379:i=598:bs=on:bd=preordered:av=off:ss=axioms_2926 on theBenchmark for (2926ds/598Mi)
% 87.66/13.07 % (548396)Refutation not found, incomplete strategy
% 87.66/13.07 % (548396)------------------------------
% 87.66/13.07 % (548396)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 87.66/13.07 % (548396)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 87.66/13.07 % (548396)CaDiCaL version: 2.1.3
% 87.66/13.07 % (548396)Termination reason: Refutation not found, incomplete strategy
% 87.66/13.07 % (548396)Time elapsed: 0.001 s
% 87.66/13.07 % (548396)Peak memory usage: 86 MB
% 87.66/13.07 % (548393)------------------------------
% 87.66/13.07 % (548393)------------------------------
% 87.66/13.07 % (548400)dis-1010_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=occurrence:random_seed=3738117626:i=2989:sd=3:ss=axioms:sgt=60_2923 on theBenchmark for (2923ds/2989Mi)
% 87.66/13.07 % (548396)------------------------------
% 87.66/13.07 % (548396)------------------------------
% 87.66/13.07 % (548403)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=326409420:i=1997:bd=preordered:av=off:gtg=all:gsp=on_2921 on theBenchmark for (2921ds/1997Mi)
% 87.66/13.07 [W927 14:00:35.804034761 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 89.50/13.38 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 89.50/13.38 [W927 14:00:35.804080434 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 89.50/13.38 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 89.50/13.38 [W927 14:00:35.804143562 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 89.50/13.38 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 89.50/13.38 [W927 14:00:35.804163005 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 89.50/13.38 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 89.50/13.38 [W927 14:00:35.804210753 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 89.50/13.38 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 89.50/13.38 [W927 14:00:35.804228180 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 89.50/13.38 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 89.50/13.38 [W927 14:00:35.804271503 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 89.50/13.38 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 89.50/13.38 [W927 14:00:35.804288944 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 89.50/13.38 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 89.50/13.38 [W927 14:00:35.804330214 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 89.50/13.38 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 89.50/13.38 [W927 14:00:35.804347518 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 89.50/13.38 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 89.50/13.38 [W927 14:00:35.804388378 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 89.50/13.38 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 89.50/13.38 [W927 14:00:35.804405312 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 89.50/13.38 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 89.50/13.38 % (548400)Refutation not found, incomplete strategy
% 89.50/13.38 % (548400)------------------------------
% 89.50/13.38 % (548400)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 89.50/13.38 % (548400)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 89.50/13.38 % (548400)CaDiCaL version: 2.1.3
% 89.50/13.38 % (548400)Termination reason: Refutation not found, incomplete strategy
% 89.50/13.38 % (548400)Time elapsed: 0.872 s
% 89.50/13.38 % (548400)Peak memory usage: 125 MB
% 89.50/13.38 % (548400)Instructions burned: 821 (million)
% 92.22/13.72 % (548400)------------------------------
% 92.22/13.72 % (548400)------------------------------
% 92.22/13.72 % (548407)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=44444199:i=2088:bd=preordered:av=off_2909 on theBenchmark for (2909ds/2088Mi)
% 92.22/13.72 % (548403)Instruction limit reached!
% 92.22/13.72 % (548403)------------------------------
% 92.22/13.72 % (548403)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 92.22/13.72 % (548403)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 92.22/13.72 % (548403)CaDiCaL version: 2.1.3
% 92.22/13.72 % (548403)Termination reason: Instruction limit
% 92.22/13.72 % (548403)Termination phase: Saturation
% 92.22/13.72 % (548403)Time elapsed: 1.974 s
% 92.22/13.72 % (548403)Peak memory usage: 138 MB
% 92.22/13.72 % (548403)Instructions burned: 1998 (million)
% 92.22/13.72 % (548411)lrs+1010_64:1_anc=all:to=lpo:sil=16000:fde=none:sp=const_frequency:urr=full:sac=on:random_seed=1217463900:i=1098:nicw=on_2899 on theBenchmark for (2899ds/1098Mi)
% 92.22/13.72 % (548411)Instruction limit reached!
% 92.22/13.72 % (548411)------------------------------
% 92.22/13.72 % (548411)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 92.22/13.72 % (548411)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 92.22/13.72 % (548411)CaDiCaL version: 2.1.3
% 92.22/13.72 % (548411)Termination reason: Instruction limit
% 92.22/13.72 % (548411)Termination phase: Saturation
% 92.22/13.72 % (548411)Time elapsed: 0.982 s
% 92.22/13.72 % (548411)Peak memory usage: 98 MB
% 92.22/13.72 % (548411)Instructions burned: 1098 (million)
% 92.22/13.72 % (548416)lrs-1011_32:1_to=lpo:sil=32000:tgt=ground:sos=on:spb=goal_then_units:acc=on:random_seed=2454831684:i=433:bd=preordered_2886 on theBenchmark for (2886ds/433Mi)
% 92.22/13.72 % (548416)Refutation not found, incomplete strategy
% 92.22/13.72 % (548416)------------------------------
% 92.22/13.72 % (548416)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 92.22/13.72 % (548416)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 92.22/13.72 % (548416)CaDiCaL version: 2.1.3
% 92.22/13.72 % (548416)Termination reason: Refutation not found, incomplete strategy
% 92.22/13.72 % (548416)Time elapsed: 0.001 s
% 92.22/13.72 % (548416)Peak memory usage: 87 MB
% 92.22/13.72 % (548407)Instruction limit reached!
% 92.22/13.72 % (548407)------------------------------
% 92.22/13.72 % (548407)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 92.22/13.72 % (548407)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 92.22/13.72 % (548407)CaDiCaL version: 2.1.3
% 92.22/13.72 % (548407)Termination reason: Instruction limit
% 92.22/13.72 % (548407)Termination phase: Saturation
% 92.22/13.72 % (548407)Time elapsed: 2.190 s
% 92.22/13.72 % (548407)Peak memory usage: 138 MB
% 92.22/13.72 % (548407)Instructions burned: 2089 (million)
% 92.22/13.72 % (548419)lrs+1002_1_ncem=casc2026/models/loop3.pt:sil=32000:npcc=on:prc=on:etr=on:spb=goal:flr=on:random_seed=1512472181:st=5.37:cond=on:i=2942:s2at=20:aac=none:fgj=on:bs=on:gtg=exists_sym:ss=axioms:er=filter:sgt=16_2884 on theBenchmark for (2884ds/2942Mi)
% 92.22/13.72 % (548416)------------------------------
% 92.22/13.72 % (548416)------------------------------
% 92.22/13.72 % (548422)lrs+35_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=reverse_arity:urr=full:rp=on:br=off:random_seed=2152421610:i=6922:s2at=5:sd=3:bd=all:ss=axioms:er=known:sgt=32_2881 on theBenchmark for (2881ds/6922Mi)
% 92.22/13.73 [W927 14:00:39.649860840 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 92.22/13.73 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 92.22/13.73 [W927 14:00:39.649906461 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 92.22/13.73 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 92.22/13.73 [W927 14:00:39.649967631 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 92.22/13.73 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 99.24/15.05 [W927 14:00:39.649989205 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 99.24/15.05 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 99.24/15.05 [W927 14:00:39.650047269 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 99.24/15.05 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 99.24/15.05 [W927 14:00:39.650066146 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 99.24/15.05 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 99.24/15.05 [W927 14:00:39.650109090 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 99.24/15.05 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 99.24/15.05 [W927 14:00:39.650141353 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 99.24/15.05 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 99.24/15.05 [W927 14:00:39.650186327 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 99.24/15.05 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 99.24/15.05 [W927 14:00:39.650203694 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 99.24/15.05 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 99.24/15.05 [W927 14:00:39.650246195 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 99.24/15.05 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 99.24/15.05 [W927 14:00:39.650263352 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 99.24/15.05 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 99.24/15.05 % (548419)Refutation not found, incomplete strategy
% 99.24/15.05 % (548419)------------------------------
% 99.24/15.05 % (548419)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 99.24/15.05 % (548419)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 99.24/15.05 % (548419)CaDiCaL version: 2.1.3
% 99.24/15.05 % (548419)Termination reason: Refutation not found, incomplete strategy
% 99.24/15.05 % (548419)Time elapsed: 0.895 s
% 99.24/15.05 % (548419)Peak memory usage: 126 MB
% 99.24/15.05 % (548419)Instructions burned: 825 (million)
% 99.24/15.05 % (548383)Refutation not found, incomplete strategy
% 99.24/15.05 % (548383)------------------------------
% 99.24/15.05 % (548383)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 99.24/15.05 % (548383)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 99.24/15.05 % (548383)CaDiCaL version: 2.1.3
% 99.24/15.05 % (548383)Termination reason: Refutation not found, incomplete strategy
% 99.24/15.05 % (548383)Time elapsed: 8.118 s
% 99.24/15.05 % (548383)Peak memory usage: 226 MB
% 99.24/15.05 % (548383)Instructions burned: 8422 (million)
% 99.24/15.05 [W927 14:00:39.956547037 register_special_ops.cpp:225] Warning: Creating a tensor from 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.75/15.55 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 104.75/15.55 [W927 14:00:39.956579587 register_special_ops.cpp:225] Warning: Creating a tensor from 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.75/15.55 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 104.75/15.55 [W927 14:00:39.956626308 register_special_ops.cpp:225] Warning: Creating a tensor from 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.75/15.55 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 104.75/15.55 [W927 14:00:39.956637258 register_special_ops.cpp:225] Warning: Creating a tensor from 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.75/15.55 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 104.75/15.55 [W927 14:00:39.956662022 register_special_ops.cpp:225] Warning: Creating a tensor from 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.75/15.55 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 104.75/15.55 [W927 14:00:39.956671948 register_special_ops.cpp:225] Warning: Creating a tensor from 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.75/15.55 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 104.75/15.55 [W927 14:00:39.956695785 register_special_ops.cpp:225] Warning: Creating a tensor from 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.75/15.55 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 104.75/15.55 [W927 14:00:39.956705842 register_special_ops.cpp:225] Warning: Creating a tensor from 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.75/15.55 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 104.75/15.55 [W927 14:00:39.956733413 register_special_ops.cpp:225] Warning: Creating a tensor from 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.75/15.55 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 104.75/15.55 [W927 14:00:39.956749353 register_special_ops.cpp:225] Warning: Creating a tensor from 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.75/15.55 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 104.75/15.55 [W927 14:00:39.956794510 register_special_ops.cpp:225] Warning: Creating a tensor from 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.75/15.55 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 104.75/15.55 [W927 14:00:39.956868444 register_special_ops.cpp:225] Warning: Creating a tensor from 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.75/15.55 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 104.75/15.55 % (548422)Refutation not found, incomplete strategy
% 104.75/15.55 % (548422)------------------------------
% 104.75/15.55 % (548422)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 104.75/15.55 % (548422)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 104.75/15.55 % (548422)CaDiCaL version: 2.1.3
% 104.75/15.55 % (548422)Termination reason: Refutation not found, incomplete strategy
% 104.75/15.55 % (548422)Time elapsed: 0.837 s
% 104.75/15.55 % (548422)Peak memory usage: 125 MB
% 104.75/15.55 % (548422)Instructions burned: 821 (million)
% 104.75/15.55 % (548419)------------------------------
% 110.72/16.42 % (548419)------------------------------
% 110.72/16.42 % (548383)------------------------------
% 110.72/16.42 % (548383)------------------------------
% 110.72/16.42 % (548429)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=4141561181:s2a=on:i=596:s2at=2.3:gtgl=5:gtg=all:sup=off_2869 on theBenchmark for (2869ds/596Mi)
% 110.72/16.42 % (548429)Refutation not found, incomplete strategy
% 110.72/16.42 % (548429)------------------------------
% 110.72/16.42 % (548429)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 110.72/16.42 % (548429)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 110.72/16.42 % (548429)CaDiCaL version: 2.1.3
% 110.72/16.42 % (548429)Termination reason: Refutation not found, incomplete strategy
% 110.72/16.42 % (548429)Time elapsed: 0.002 s
% 110.72/16.42 % (548429)Peak memory usage: 88 MB
% 110.72/16.42 % (548429)Instructions burned: 1 (million)
% 110.72/16.42 % (548430)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=2685497800:i=4123:kws=inv_frequency:bd=preordered:av=off:er=known_2869 on theBenchmark for (2869ds/4123Mi)
% 110.72/16.42 % (548422)------------------------------
% 110.72/16.42 % (548422)------------------------------
% 110.72/16.42 % (548429)------------------------------
% 110.72/16.42 % (548429)------------------------------
% 110.72/16.42 % (548436)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=2281322833:i=16411:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2866 on theBenchmark for (2866ds/16411Mi)
% 110.72/16.42 % (548439)lrs+0_1_ncem=casc2026/models/loop1.pt:sil=8000:tgt=full:npcc=on:sp=reverse_frequency:gs=on:random_seed=831039634:i=1670:kws=inv_precedence:bd=all:av=off:gtg=exists_all_2864 on theBenchmark for (2864ds/1670Mi)
% 110.72/16.42 % (548377)Instruction limit reached!
% 110.72/16.42 % (548377)------------------------------
% 110.72/16.42 % (548377)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 110.72/16.42 % (548377)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 110.72/16.42 % (548377)CaDiCaL version: 2.1.3
% 110.72/16.42 % (548377)Termination reason: Instruction limit
% 110.72/16.42 % (548377)Termination phase: Saturation
% 110.72/16.42 % (548377)Time elapsed: 10.322 s
% 110.72/16.42 % (548377)Peak memory usage: 193 MB
% 110.72/16.42 % (548377)Instructions burned: 10307 (million)
% 110.72/16.42 % (548443)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=3862767920:st=3:cond=fast:i=1722:sd=2:ss=included:fsd=on_2859 on theBenchmark for (2859ds/1722Mi)
% 110.72/16.42 [W927 14:00:41.629360328 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 110.72/16.42 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 110.72/16.42 [W927 14:00:41.629473419 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 110.72/16.42 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 110.72/16.42 [W927 14:00:41.629573184 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 110.72/16.42 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 110.72/16.42 [W927 14:00:41.629630195 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 110.72/16.42 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 110.72/16.42 [W927 14:00:41.629712069 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 110.72/16.42 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 110.72/16.42 [W927 14:00:41.629765936 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 116.54/17.17 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 116.54/17.17 [W927 14:00:41.629879961 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 116.54/17.17 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 116.54/17.17 [W927 14:00:41.629935965 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 116.54/17.17 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 116.54/17.17 [W927 14:00:41.630029076 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 116.54/17.17 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 116.54/17.17 [W927 14:00:41.630088977 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 116.54/17.17 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 116.54/17.17 [W927 14:00:41.630169584 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 116.54/17.17 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 116.54/17.17 [W927 14:00:41.630222305 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 116.54/17.17 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 116.54/17.17 % (548436)Refutation not found, incomplete strategy
% 116.54/17.17 % (548436)------------------------------
% 116.54/17.17 % (548436)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 116.54/17.17 % (548436)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 116.54/17.17 % (548436)CaDiCaL version: 2.1.3
% 116.54/17.17 % (548436)Termination reason: Refutation not found, incomplete strategy
% 116.54/17.17 % (548436)Time elapsed: 1.009 s
% 116.54/17.17 % (548436)Peak memory usage: 125 MB
% 116.54/17.17 % (548436)Instructions burned: 820 (million)
% 116.54/17.17 [W927 14:00:41.125276224 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 116.54/17.17 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 116.54/17.17 [W927 14:00:41.125319088 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 116.54/17.17 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 116.54/17.17 [W927 14:00:41.125371282 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 116.54/17.17 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 116.54/17.17 [W927 14:00:41.125389482 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 116.54/17.17 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 116.54/17.17 [W927 14:00:41.125428276 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 140.90/20.63 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 140.90/20.63 [W927 14:00:41.125444709 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 140.90/20.63 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 140.90/20.63 [W927 14:00:41.125485053 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 140.90/20.63 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 140.90/20.63 [W927 14:00:41.125500003 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 140.90/20.63 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 140.90/20.63 [W927 14:00:41.125536361 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 140.90/20.63 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 140.90/20.63 [W927 14:00:41.125551237 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 140.90/20.63 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 140.90/20.63 [W927 14:00:41.125586631 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 140.90/20.63 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 140.90/20.63 [W927 14:00:41.125601715 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 140.90/20.63 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 140.90/20.63 % (548436)------------------------------
% 140.90/20.63 % (548436)------------------------------
% 140.90/20.63 % (548443)Refutation not found, incomplete strategy
% 140.90/20.63 % (548443)------------------------------
% 140.90/20.63 % (548443)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 140.90/20.63 % (548443)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 140.90/20.63 % (548443)CaDiCaL version: 2.1.3
% 140.90/20.63 % (548443)Termination reason: Refutation not found, incomplete strategy
% 140.90/20.63 % (548443)Time elapsed: 0.774 s
% 140.90/20.63 % (548443)Peak memory usage: 125 MB
% 140.90/20.63 % (548443)Instructions burned: 825 (million)
% 140.90/20.63 % (548448)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=2799169004:cts=off:cond=on:i=9530:bs=on:fsd=on_2850 on theBenchmark for (2850ds/9530Mi)
% 140.90/20.63 % (548443)------------------------------
% 140.90/20.63 % (548443)------------------------------
% 140.90/20.63 % (548439)Instruction limit reached!
% 140.90/20.63 % (548439)------------------------------
% 140.90/20.63 % (548439)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 140.90/20.63 % (548439)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 140.90/20.63 % (548439)CaDiCaL version: 2.1.3
% 140.90/20.63 % (548439)Termination reason: Instruction limit
% 140.90/20.63 % (548439)Termination phase: Saturation
% 140.90/20.63 % (548439)Time elapsed: 1.663 s
% 140.90/20.63 % (548439)Peak memory usage: 134 MB
% 140.90/20.63 % (548439)Instructions burned: 1670 (million)
% 140.90/20.63 % (548452)lrs+10_1_ncem=casc2026/models/loop4.pt:sil=64000:npcc=on:sp=occurrence:random_seed=2447858546:st=2:i=4495:sd=10:ss=included_2845 on theBenchmark for (2845ds/4495Mi)
% 140.90/20.63 % (548454)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=2501897489:cond=fast:i=4920:s2at=1.9:kws=inv_frequency:av=off:er=filter_2845 on theBenchmark for (2845ds/4920Mi)
% 143.82/21.22 [W927 14:00:43.545761535 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 143.82/21.22 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 143.82/21.22 [W927 14:00:43.545818672 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 143.82/21.22 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 143.82/21.22 [W927 14:00:43.545877266 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 143.82/21.22 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 143.82/21.22 [W927 14:00:43.545897853 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 143.82/21.22 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 143.82/21.22 [W927 14:00:43.545943177 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 143.82/21.22 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 143.82/21.22 [W927 14:00:43.545962287 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 143.82/21.22 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 143.82/21.22 [W927 14:00:43.546019725 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 143.82/21.22 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 143.82/21.22 [W927 14:00:43.546040725 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 143.82/21.22 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 143.82/21.22 [W927 14:00:43.546085049 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 143.82/21.22 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 143.82/21.22 [W927 14:00:43.546103552 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 143.82/21.22 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 143.82/21.22 [W927 14:00:43.546147916 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 143.82/21.22 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 143.82/21.22 [W927 14:00:43.546166460 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 143.82/21.22 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 143.82/21.22 % (548452)Refutation not found, incomplete strategy
% 143.82/21.22 % (548452)------------------------------
% 143.82/21.22 % (548452)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 143.82/21.22 % (548452)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 148.64/22.02 % (548452)CaDiCaL version: 2.1.3
% 148.64/22.02 % (548452)Termination reason: Refutation not found, incomplete strategy
% 148.64/22.02 % (548452)Time elapsed: 0.815 s
% 148.64/22.02 % (548452)Peak memory usage: 125 MB
% 148.64/22.02 % (548452)Instructions burned: 825 (million)
% 148.64/22.02 % (548452)------------------------------
% 148.64/22.02 % (548452)------------------------------
% 148.64/22.02 % (548460)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=3737900140:cts=off:cond=on:i=2083:s2at=-1:fgj=on:av=off_2831 on theBenchmark for (2831ds/2083Mi)
% 148.64/22.02 % (548430)Instruction limit reached!
% 148.64/22.02 % (548430)------------------------------
% 148.64/22.02 % (548430)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 148.64/22.02 % (548430)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 148.64/22.02 % (548430)CaDiCaL version: 2.1.3
% 148.64/22.02 % (548430)Termination reason: Instruction limit
% 148.64/22.02 % (548430)Termination phase: Saturation
% 148.64/22.02 % (548430)Time elapsed: 4.282 s
% 148.64/22.02 % (548430)Peak memory usage: 154 MB
% 148.64/22.02 % (548430)Instructions burned: 4123 (million)
% 148.64/22.02 % (548465)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=3096148438:i=4629:av=off:gsp=on_2824 on theBenchmark for (2824ds/4629Mi)
% 148.64/22.02 % (548465)Refutation not found, incomplete strategy
% 148.64/22.02 % (548465)------------------------------
% 148.64/22.02 % (548465)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 148.64/22.02 % (548465)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 148.64/22.02 % (548465)CaDiCaL version: 2.1.3
% 148.64/22.02 % (548465)Termination reason: Refutation not found, incomplete strategy
% 148.64/22.02 % (548465)Time elapsed: 0.886 s
% 148.64/22.02 % (548465)Peak memory usage: 127 MB
% 148.64/22.02 % (548465)Instructions burned: 825 (million)
% 148.64/22.02 % (548465)------------------------------
% 148.64/22.02 % (548465)------------------------------
% 148.64/22.02 % (548460)Instruction limit reached!
% 148.64/22.02 % (548460)------------------------------
% 148.64/22.02 % (548460)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 148.64/22.02 % (548460)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 148.64/22.02 % (548460)CaDiCaL version: 2.1.3
% 148.64/22.02 % (548460)Termination reason: Instruction limit
% 148.64/22.02 % (548460)Termination phase: Saturation
% 148.64/22.02 % (548460)Time elapsed: 2.045 s
% 148.64/22.02 % (548460)Peak memory usage: 140 MB
% 148.64/22.02 % (548460)Instructions burned: 2084 (million)
% 148.64/22.02 % (548469)dis+10_64_sil=16000:tgt=full:plsq=on:prc=on:drc=off:plsqc=2:plsqr=32,1:spb=goal:random_seed=3387824991:i=1258:av=off_2809 on theBenchmark for (2809ds/1258Mi)
% 148.64/22.02 % (548471)ott+1_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:fdtod=off:random_seed=619797734:i=7343:av=off:ss=included_2808 on theBenchmark for (2808ds/7343Mi)
% 148.64/22.02 [W927 14:00:46.206028869 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 148.64/22.02 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 148.64/22.02 [W927 14:00:46.206089090 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 148.64/22.02 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 148.64/22.02 [W927 14:00:46.206149867 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 148.64/22.02 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 148.64/22.02 [W927 14:00:46.206167241 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 148.64/22.02 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 148.64/22.02 [W927 14:00:46.206206705 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 151.86/22.16 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 151.86/22.16 [W927 14:00:46.206222521 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 151.86/22.16 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 151.86/22.16 [W927 14:00:46.206261879 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 151.86/22.16 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 151.86/22.16 [W927 14:00:46.206278062 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 151.86/22.16 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 151.86/22.16 [W927 14:00:46.206315456 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 151.86/22.16 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 151.86/22.16 [W927 14:00:46.206331569 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 151.86/22.16 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 151.86/22.16 [W927 14:00:46.206370930 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 151.86/22.16 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 151.86/22.16 [W927 14:00:46.206388230 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 151.86/22.16 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 151.86/22.16 % (548471)Refutation not found, incomplete strategy
% 151.86/22.16 % (548471)------------------------------
% 151.86/22.16 % (548471)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 151.86/22.16 % (548471)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 151.86/22.16 % (548471)CaDiCaL version: 2.1.3
% 151.86/22.16 % (548471)Termination reason: Refutation not found, incomplete strategy
% 151.86/22.16 % (548471)Time elapsed: 0.820 s
% 151.86/22.16 % (548471)Peak memory usage: 125 MB
% 151.86/22.16 % (548471)Instructions burned: 821 (million)
% 151.86/22.16 % (548469)Instruction limit reached!
% 151.86/22.16 % (548469)------------------------------
% 151.86/22.16 % (548469)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 151.86/22.16 % (548469)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 151.86/22.16 % (548469)CaDiCaL version: 2.1.3
% 151.86/22.16 % (548469)Termination reason: Instruction limit
% 151.86/22.16 % (548469)Termination phase: Saturation
% 151.86/22.16 % (548469)Time elapsed: 0.953 s
% 151.86/22.16 % (548469)Peak memory usage: 92 MB
% 151.86/22.16 % (548469)Instructions burned: 1258 (million)
% 151.86/22.16 % (548471)------------------------------
% 151.86/22.16 % (548471)------------------------------
% 151.86/22.16 % (548478)lrs-1002_1_to=lpo:sil=16000:sp=reverse_arity:sos=on:random_seed=425170331:i=1325:sd=2:ss=axioms:sgt=16_2797 on theBenchmark for (2797ds/1325Mi)
% 151.86/22.16 % (548478)Refutation not found, incomplete strategy
% 151.86/22.16 % (548478)------------------------------
% 151.86/22.16 % (548478)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 151.86/22.16 % (548478)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 151.86/22.16 % (548478)CaDiCaL version: 2.1.3
% 151.86/22.16 % (548478)Termination reason: Refutation not found, incomplete strategy
% 151.86/22.16 % (548478)Time elapsed: 0.001 s
% 162.92/23.87 % (548478)Peak memory usage: 86 MB
% 162.92/23.87 % (548454)Instruction limit reached!
% 162.92/23.87 % (548454)------------------------------
% 162.92/23.87 % (548454)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 162.92/23.87 % (548454)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 162.92/23.87 % (548454)CaDiCaL version: 2.1.3
% 162.92/23.87 % (548454)Termination reason: Instruction limit
% 162.92/23.87 % (548454)Termination phase: Saturation
% 162.92/23.87 % (548454)Time elapsed: 4.912 s
% 162.92/23.87 % (548454)Peak memory usage: 154 MB
% 162.92/23.87 % (548454)Instructions burned: 4921 (million)
% 162.92/23.87 % (548480)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=1671138183:st=3.9:cond=fast:i=2646:s2at=1.8:sd=5:amm=off:gtg=position:ss=axioms:fsd=on_2795 on theBenchmark for (2795ds/2646Mi)
% 162.92/23.87 % (548483)dis-1003_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:sp=arity:sos=on:urr=on:random_seed=4017933133:i=1489:sd=2:ep=R:ss=axioms_2793 on theBenchmark for (2793ds/1489Mi)
% 162.92/23.87 % (548478)------------------------------
% 162.92/23.87 % (548478)------------------------------
% 162.92/23.87 % (548488)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=1781042899:i=1503_2791 on theBenchmark for (2791ds/1503Mi)
% 162.92/23.87 [W927 14:00:48.597934051 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 162.92/23.87 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 162.92/23.87 [W927 14:00:48.597992435 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 162.92/23.87 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 162.92/23.87 [W927 14:00:48.598067090 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 162.92/23.87 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 162.92/23.87 [W927 14:00:48.598086860 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 162.92/23.87 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 162.92/23.87 [W927 14:00:48.598128830 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 162.92/23.87 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 162.92/23.87 [W927 14:00:48.598145721 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 162.92/23.87 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 162.92/23.87 [W927 14:00:48.598187714 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 162.92/23.87 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 162.92/23.87 [W927 14:00:48.598204741 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 162.92/23.87 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 162.92/23.87 [W927 14:00:48.598244985 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 162.92/23.87 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 174.27/25.38 [W927 14:00:48.598261975 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 174.27/25.38 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 174.27/25.38 [W927 14:00:48.598304693 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 174.27/25.38 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 174.27/25.38 [W927 14:00:48.598322353 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 174.27/25.38 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 174.27/25.38 [W927 14:00:48.741794695 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 174.27/25.38 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 174.27/25.38 [W927 14:00:48.741846569 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 174.27/25.38 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 174.27/25.38 [W927 14:00:48.741906796 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 174.27/25.38 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 174.27/25.38 [W927 14:00:48.741929883 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 174.27/25.38 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 174.27/25.38 [W927 14:00:48.741977350 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 174.27/25.38 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 174.27/25.38 [W927 14:00:48.741998361 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 174.27/25.38 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 174.27/25.38 [W927 14:00:48.742059035 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 174.27/25.38 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 174.27/25.38 [W927 14:00:48.742078692 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 174.27/25.38 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 174.27/25.38 [W927 14:00:48.742124795 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 174.27/25.38 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 174.27/25.38 [W927 14:00:48.742144532 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 174.27/25.38 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 174.27/25.38 [W927 14:00:48.742189230 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 176.45/25.66 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 176.45/25.66 [W927 14:00:48.742209537 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 176.45/25.66 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 176.45/25.66 % (548480)Refutation not found, incomplete strategy
% 176.45/25.66 % (548480)------------------------------
% 176.45/25.66 % (548480)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 176.45/25.66 % (548480)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 176.45/25.66 % (548480)CaDiCaL version: 2.1.3
% 176.45/25.66 % (548480)Termination reason: Refutation not found, incomplete strategy
% 176.45/25.66 % (548480)Time elapsed: 0.854 s
% 176.45/25.66 % (548480)Peak memory usage: 125 MB
% 176.45/25.66 % (548480)Instructions burned: 821 (million)
% 176.45/25.66 % (548483)Refutation not found, incomplete strategy
% 176.45/25.66 % (548483)------------------------------
% 176.45/25.66 % (548483)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 176.45/25.66 % (548483)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 176.45/25.66 % (548483)CaDiCaL version: 2.1.3
% 176.45/25.66 % (548483)Termination reason: Refutation not found, incomplete strategy
% 176.45/25.66 % (548483)Time elapsed: 0.844 s
% 176.45/25.66 % (548483)Peak memory usage: 125 MB
% 176.45/25.66 % (548483)Instructions burned: 824 (million)
% 176.45/25.66 % (548480)------------------------------
% 176.45/25.66 % (548480)------------------------------
% 176.45/25.66 % (548488)Refutation not found, incomplete strategy
% 176.45/25.66 % (548488)------------------------------
% 176.45/25.66 % (548488)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 176.45/25.66 % (548488)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 176.45/25.66 % (548488)CaDiCaL version: 2.1.3
% 176.45/25.66 % (548488)Termination reason: Refutation not found, incomplete strategy
% 176.45/25.66 % (548488)Time elapsed: 0.897 s
% 176.45/25.66 % (548488)Peak memory usage: 127 MB
% 176.45/25.66 % (548488)Instructions burned: 833 (million)
% 176.45/25.66 % (548483)------------------------------
% 176.45/25.66 % (548483)------------------------------
% 176.45/25.66 % (548493)lrs+10_1_ncem=casc2026/models/loop3.pt:sil=16000:tgt=ground:npcc=on:random_seed=3814079128:i=13942:kws=frequency_2780 on theBenchmark for (2780ds/13942Mi)
% 176.45/25.66 % (548494)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=868330010:i=3604:fsr=off:er=filter_2779 on theBenchmark for (2779ds/3604Mi)
% 176.45/25.66 % (548488)------------------------------
% 176.45/25.66 % (548488)------------------------------
% 176.45/25.66 % (548500)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=32000:npcc=on:random_seed=3496593157:i=1876:sd=1:ss=included:sgt=32_2776 on theBenchmark for (2776ds/1876Mi)
% 176.45/25.66 [W927 14:00:50.446259611 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 176.45/25.66 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 176.45/25.66 [W927 14:00:50.446318868 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 176.45/25.66 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 176.45/25.66 [W927 14:00:50.446377879 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 176.45/25.66 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 176.45/25.66 [W927 14:00:50.446399869 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 184.11/26.92 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 184.11/26.92 [W927 14:00:50.446444853 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 184.11/26.92 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 184.11/26.92 [W927 14:00:50.446535934 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 184.11/26.92 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 184.11/26.92 [W927 14:00:50.446595762 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 184.11/26.92 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 184.11/26.92 [W927 14:00:50.446615012 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 184.11/26.92 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 184.11/26.92 [W927 14:00:50.446658452 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 184.11/26.92 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 184.11/26.92 [W927 14:00:50.446676363 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 184.11/26.92 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 184.11/26.92 [W927 14:00:50.446719943 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 184.11/26.92 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 184.11/26.92 [W927 14:00:50.446738100 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 184.11/26.92 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 184.11/26.92 % (548500)Refutation not found, incomplete strategy
% 184.11/26.92 % (548500)------------------------------
% 184.11/26.92 % (548500)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 184.11/26.92 % (548500)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 184.11/26.92 % (548500)CaDiCaL version: 2.1.3
% 184.11/26.92 % (548500)Termination reason: Refutation not found, incomplete strategy
% 184.11/26.92 % (548500)Time elapsed: 0.810 s
% 184.11/26.92 % (548500)Peak memory usage: 125 MB
% 184.11/26.92 % (548500)Instructions burned: 820 (million)
% 184.11/26.92 % (548500)------------------------------
% 184.11/26.92 % (548500)------------------------------
% 184.11/26.92 % (548504)lrs+10_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:fde=none:sp=arity:urr=on:br=off:random_seed=1301221073:i=1932:bd=preordered:ins=10:sup=off:ss=axioms_2762 on theBenchmark for (2762ds/1932Mi)
% 184.11/26.92 [W927 14:00:51.959066859 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 184.11/26.92 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 184.11/26.92 [W927 14:00:51.959124106 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 184.11/26.92 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 184.11/26.92 [W927 14:00:51.959189364 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 221.06/31.97 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 221.06/31.97 [W927 14:00:51.959208314 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 221.06/31.97 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 221.06/31.97 [W927 14:00:51.959260178 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 221.06/31.97 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 221.06/31.97 [W927 14:00:51.959277835 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 221.06/31.97 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 221.06/31.97 [W927 14:00:51.959322499 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 221.06/31.97 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 221.06/31.97 [W927 14:00:51.959340046 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 221.06/31.97 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 221.06/31.97 [W927 14:00:51.959388853 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 221.06/31.97 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 221.06/31.97 [W927 14:00:51.959418940 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 221.06/31.97 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 221.06/31.97 [W927 14:00:51.959465047 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 221.06/31.97 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 221.06/31.97 [W927 14:00:51.959482907 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 221.06/31.97 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 221.06/31.97 % (548448)Instruction limit reached!
% 221.06/31.97 % (548448)------------------------------
% 221.06/31.97 % (548448)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 221.06/31.97 % (548448)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 221.06/31.97 % (548448)CaDiCaL version: 2.1.3
% 221.06/31.97 % (548448)Termination reason: Instruction limit
% 221.06/31.97 % (548448)Termination phase: Saturation
% 221.06/31.97 % (548448)Time elapsed: 9.623 s
% 221.06/31.97 % (548448)Peak memory usage: 177 MB
% 221.06/31.97 % (548448)Instructions burned: 9531 (million)
% 221.06/31.97 % (548504)Refutation not found, incomplete strategy
% 221.06/31.97 % (548504)------------------------------
% 221.06/31.97 % (548504)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 221.06/31.97 % (548504)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 221.06/31.97 % (548504)CaDiCaL version: 2.1.3
% 221.06/31.97 % (548504)Termination reason: Refutation not found, incomplete strategy
% 221.06/31.97 % (548504)Time elapsed: 0.905 s
% 221.06/31.97 % (548504)Peak memory usage: 125 MB
% 221.06/31.97 % (548504)Instructions burned: 825 (million)
% 226.47/32.79 % (548509)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=1965007226:s2pl=on:cond=fast:i=1980:s2at=2:kws=inv_precedence:doe=on:ins=1:av=off:gsp=on_2751 on theBenchmark for (2751ds/1980Mi)
% 226.47/32.79 % (548504)------------------------------
% 226.47/32.79 % (548504)------------------------------
% 226.47/32.79 % (548494)Instruction limit reached!
% 226.47/32.79 % (548494)------------------------------
% 226.47/32.79 % (548494)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 226.47/32.79 % (548494)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 226.47/32.79 % (548494)CaDiCaL version: 2.1.3
% 226.47/32.79 % (548494)Termination reason: Instruction limit
% 226.47/32.79 % (548494)Termination phase: Saturation
% 226.47/32.79 % (548494)Time elapsed: 3.276 s
% 226.47/32.79 % (548494)Peak memory usage: 135 MB
% 226.47/32.79 % (548494)Instructions burned: 3604 (million)
% 226.47/32.79 % (548512)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=596772339:i=3902:kws=inv_arity_squared:fgj=on:ss=axioms:sgt=11_2746 on theBenchmark for (2746ds/3902Mi)
% 226.47/32.79 % (548513)dis+10_32_sil=16000:tgt=ground:drc=off:sas=cadical:acc=on:alpa=false:avsqc=3:random_seed=1456574669:avsq=on:i=3916:aac=none:amm=off_2745 on theBenchmark for (2745ds/3916Mi)
% 226.47/32.79 [W927 14:00:53.498102421 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 226.47/32.79 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 226.47/32.79 [W927 14:00:53.498144628 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 226.47/32.79 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 226.47/32.79 [W927 14:00:53.498204618 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 226.47/32.79 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 226.47/32.79 [W927 14:00:53.498226789 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 226.47/32.79 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 226.47/32.79 [W927 14:00:53.498275269 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 226.47/32.79 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 226.47/32.79 [W927 14:00:53.498294843 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 226.47/32.79 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 226.47/32.79 [W927 14:00:53.498341923 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 226.47/32.79 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 226.47/32.79 [W927 14:00:53.498361857 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 226.47/32.79 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 226.47/32.79 [W927 14:00:53.498407968 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 226.47/32.79 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 118.36/33.40 [W927 14:00:53.498426888 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 118.36/33.40 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 118.36/33.40 [W927 14:00:53.498484262 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 118.36/33.40 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 118.36/33.40 [W927 14:00:53.498572840 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 118.36/33.40 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 118.36/33.40 % (548512)Refutation not found, incomplete strategy
% 118.36/33.40 % (548512)------------------------------
% 118.36/33.40 % (548512)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 118.36/33.40 % (548512)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 118.36/33.40 % (548512)CaDiCaL version: 2.1.3
% 118.36/33.40 % (548512)Termination reason: Refutation not found, incomplete strategy
% 118.36/33.40 % (548512)Time elapsed: 0.895 s
% 118.36/33.40 % (548512)Peak memory usage: 125 MB
% 118.36/33.40 % (548512)Instructions burned: 821 (million)
% 118.36/33.40 % (548512)------------------------------
% 118.36/33.40 % (548512)------------------------------
% 118.36/33.40 % (548509)Instruction limit reached!
% 118.36/33.40 % (548509)------------------------------
% 118.36/33.40 % (548509)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 118.36/33.40 % (548509)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 118.36/33.40 % (548509)CaDiCaL version: 2.1.3
% 118.36/33.40 % (548509)Termination reason: Instruction limit
% 118.36/33.40 % (548509)Termination phase: Saturation
% 118.36/33.40 % (548509)Time elapsed: 1.866 s
% 118.36/33.40 % (548509)Peak memory usage: 138 MB
% 118.36/33.40 % (548509)Instructions burned: 1980 (million)
% 118.36/33.40 % (548521)dis+10_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=full:npcc=on:drc=ordering:lcm=predicate:random_seed=94379361:cond=on:i=3940:av=off:er=known_2731 on theBenchmark for (2731ds/3940Mi)
% 118.36/33.40 % (548522)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=reverse_frequency:bce=on:random_seed=2099293029:s2pl=on:i=3980:gtgl=3:kws=precedence:fgj=on:gtg=all_2730 on theBenchmark for (2730ds/3980Mi)
% 118.36/33.40 % (548513)Instruction limit reached!
% 118.36/33.40 % (548513)------------------------------
% 118.36/33.40 % (548513)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 118.36/33.40 % (548513)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 118.36/33.40 % (548513)CaDiCaL version: 2.1.3
% 118.36/33.40 % (548513)Termination reason: Instruction limit
% 118.36/33.40 % (548513)Termination phase: Saturation
% 118.36/33.40 % (548513)Time elapsed: 3.439 s
% 118.36/33.40 % (548513)Peak memory usage: 114 MB
% 118.36/33.40 % (548513)Instructions burned: 3917 (million)
% 118.36/33.40 % (548528)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=2026804984:i=2087:s2at=3:kws=frequency:av=off:fsr=off_2708 on theBenchmark for (2708ds/2087Mi)
% 118.36/33.40 % (548521)Instruction limit reached!
% 118.36/33.40 % (548521)------------------------------
% 118.36/33.40 % (548521)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 118.36/33.40 % (548521)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 118.36/33.40 % (548521)CaDiCaL version: 2.1.3
% 118.36/33.40 % (548521)Termination reason: Instruction limit
% 118.36/33.40 % (548521)Termination phase: Saturation
% 118.36/33.40 % (548521)Time elapsed: 3.866 s
% 118.36/33.40 % (548521)Peak memory usage: 157 MB
% 118.36/33.40 % (548521)Instructions burned: 3940 (million)
% 118.36/33.40 % (548533)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=3923105738:cts=off:cond=on:i=4272:bs=on:fsd=on_2690 on theBenchmark for (2690ds/4272Mi)
% 118.36/33.40 % (548522)Instruction limit reached!
% 231.65/33.63 % (548522)------------------------------
% 231.65/33.63 % (548522)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 231.65/33.63 % (548522)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 231.65/33.63 % (548522)CaDiCaL version: 2.1.3
% 231.65/33.63 % (548522)Termination reason: Instruction limit
% 231.65/33.63 % (548522)Termination phase: Saturation
% 231.65/33.63 % (548522)Time elapsed: 4.084 s
% 231.65/33.63 % (548522)Peak memory usage: 159 MB
% 231.65/33.63 % (548522)Instructions burned: 3981 (million)
% 231.65/33.63 % (548537)lrs-30_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:urr=on:bce=on:rp=on:br=off:flr=on:random_seed=2489575846:st=-1:i=2197:kws=precedence:av=off:ss=axioms:er=known_2687 on theBenchmark for (2687ds/2197Mi)
% 231.65/33.63 % (548528)Instruction limit reached!
% 231.65/33.63 % (548528)------------------------------
% 231.65/33.63 % (548528)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 231.65/33.63 % (548528)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 231.65/33.63 % (548528)CaDiCaL version: 2.1.3
% 231.65/33.63 % (548528)Termination reason: Instruction limit
% 231.65/33.63 % (548528)Termination phase: Saturation
% 231.65/33.63 % (548528)Time elapsed: 2.194 s
% 231.65/33.63 % (548528)Peak memory usage: 140 MB
% 231.65/33.63 % (548528)Instructions burned: 2088 (million)
% 231.65/33.63 % (548540)dis+21_1_sil=8000:spb=goal_then_units:random_seed=2263735744:avsq=on:i=6508:avsqr=1,16:kws=arity_squared:fgj=on_2684 on theBenchmark for (2684ds/6508Mi)
% 231.65/33.63 [W927 14:00:59.370905892 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 231.65/33.63 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 231.65/33.63 [W927 14:00:59.370946056 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 231.65/33.63 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 231.65/33.63 [W927 14:00:59.371014264 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 231.65/33.63 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 231.65/33.63 [W927 14:00:59.371035594 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 231.65/33.63 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 231.65/33.63 [W927 14:00:59.371081031 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 231.65/33.63 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 231.65/33.63 [W927 14:00:59.371099391 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 231.65/33.63 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 231.65/33.63 [W927 14:00:59.371143359 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 231.65/33.63 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 231.65/33.63 [W927 14:00:59.371161992 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 231.65/33.63 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 231.65/33.63 [W927 14:00:59.371203959 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 231.65/33.63 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 231.65/33.63 [W927 14:00:59.371222259 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 231.65/33.63 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 231.65/33.63 [W927 14:00:59.371262863 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 231.65/33.63 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 231.65/33.63 [W927 14:00:59.371279780 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 231.65/33.63 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 231.65/33.63 % (548540)First to succeed.
% 231.65/33.63 % (548540)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-548278"
% 231.65/33.63 % (548537)Refutation not found, incomplete strategy
% 231.65/33.63 % (548537)------------------------------
% 231.65/33.63 % (548537)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 231.65/33.63 % (548537)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 231.65/33.63 % (548537)CaDiCaL version: 2.1.3
% 231.65/33.63 % (548537)Termination reason: Refutation not found, incomplete strategy
% 231.65/33.63 % (548537)Time elapsed: 0.895 s
% 231.65/33.63 % (548537)Peak memory usage: 125 MB
% 231.65/33.63 % (548537)Instructions burned: 825 (million)
% 231.65/33.63 % SZS status Satisfiable for theBenchmark
% 231.65/33.63 % SZS output start Saturation.
% See solution above
% 231.65/33.63 % SZS output start Definitions and Model Updates.
% 231.65/33.63 % SZS output end Definitions and Model Updates.
% 231.65/33.63 % (548540)------------------------------
% 231.65/33.63 % (548540)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 231.65/33.63 % (548540)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 231.65/33.63 % (548540)CaDiCaL version: 2.1.3
% 231.65/33.63 % (548540)Termination reason: Satisfiable
% 231.65/33.63 % (548540)Time elapsed: 0.364 s
% 231.65/33.63 % (548540)Peak memory usage: 90 MB
% 231.65/33.63 % (548540)Instructions burned: 407 (million)
% 231.65/33.63 % (548540)------------------------------
% 231.65/33.63 % (548540)------------------------------
% 231.65/33.63 % (548278)Success in time 32.659 s
% 231.65/33.63 % Vampire exiting
%------------------------------------------------------------------------------