%------------------------------------------------------------------------------ % File : Vampire---5.0.1 % Problem : SWB025+3 : TPTP v9.3.1. Released v5.2.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % Computer : n014.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 29 01:00:12 PM UTC 2026 % Result : Timeout 288.98s 41.73s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : SWB025+3 : TPTP v9.3.1. Released v5.2.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.11/0.36 % Computer : n014.cluster.edu % 0.11/0.36 % Model : x86_64 x86_64 % 0.11/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.36 % Memory : 8046.5625MB % 0.11/0.36 % OS : Linux 6.8.0-71-generic % 0.11/0.36 % CPULimit : 300 % 0.11/0.36 % WCLimit : 300 % 0.11/0.36 % DateTime : Mon Sep 28 07:05:31 UTC 2026 % 0.11/0.36 % CPUTime : % 0.11/0.36 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.11/0.39 Running first-order theorem proving % 0.11/0.39 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 6.93/1.98 % (1597191)Detected formulas, will run a generic FOF schedule. % 6.93/1.98 % (1597202)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=993230087:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi) % 6.93/1.98 % (1597202)Refutation not found, incomplete strategy % 6.93/1.98 % (1597202)------------------------------ % 6.93/1.98 % (1597202)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.93/1.98 % (1597202)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.93/1.98 % (1597202)CaDiCaL version: 2.1.3 % 6.93/1.98 % (1597202)Termination reason: Refutation not found, incomplete strategy % 6.93/1.98 % (1597202)Time elapsed: 0.0000 s % 6.93/1.98 % (1597202)Peak memory usage: 86 MB % 6.93/1.98 % (1597204)dis-21_1_sil=8000:lcm=predicate:random_seed=3623636917:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi) % 6.93/1.98 % (1597203)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1692035331:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi) % 6.93/1.98 % (1597200)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=2800458465:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi) % 6.93/1.98 % (1597199)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=1705767984:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi) % 6.93/1.98 % (1597201)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=3304731798:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi) % 6.93/1.98 % (1597198)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=646550690:i=141193_2999 on theBenchmark for (2999ds/141193Mi) % 6.93/1.98 % (1597201)Refutation not found, incomplete strategy % 6.93/1.98 % (1597201)------------------------------ % 6.93/1.98 % (1597201)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.93/1.98 % (1597201)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.93/1.98 % (1597201)CaDiCaL version: 2.1.3 % 6.93/1.98 % (1597201)Termination reason: Refutation not found, incomplete strategy % 6.93/1.98 % (1597201)Time elapsed: 0.001 s % 6.93/1.98 % (1597201)Peak memory usage: 86 MB % 6.93/1.98 % (1597204)Instruction limit reached! % 6.93/1.98 % (1597204)------------------------------ % 6.93/1.98 % (1597204)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.93/1.98 % (1597204)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.93/1.98 % (1597204)CaDiCaL version: 2.1.3 % 6.93/1.98 % (1597204)Termination reason: Instruction limit % 6.93/1.98 % (1597204)Termination phase: Saturation % 6.93/1.98 % (1597204)Time elapsed: 0.074 s % 6.93/1.98 % (1597204)Peak memory usage: 88 MB % 6.93/1.98 % (1597204)Instructions burned: 130 (million) % 6.93/1.98 % (1597203)Instruction limit reached! % 6.93/1.98 % (1597203)------------------------------ % 6.93/1.98 % (1597203)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.93/1.98 % (1597203)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.93/1.98 % (1597203)CaDiCaL version: 2.1.3 % 6.93/1.98 % (1597203)Termination reason: Instruction limit % 6.93/1.98 % (1597203)Termination phase: Saturation % 6.93/1.98 % (1597203)Time elapsed: 0.090 s % 6.93/1.98 % (1597203)Peak memory usage: 90 MB % 6.93/1.98 % (1597203)Instructions burned: 140 (million) % 6.93/1.98 % (1597202)------------------------------ % 6.93/1.98 % (1597202)------------------------------ % 6.93/1.98 % (1597212)lrs+10_1_sil=8000:sp=occurrence:random_seed=3360072736:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi) % 6.93/1.98 % (1597212)Refutation not found, incomplete strategy % 6.93/1.98 % (1597212)------------------------------ % 6.93/1.98 % (1597212)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.93/1.98 % (1597212)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.93/1.98 % (1597212)CaDiCaL version: 2.1.3 % 6.93/1.98 % (1597212)Termination reason: Refutation not found, incomplete strategy % 6.93/1.98 % (1597212)Time elapsed: 0.002 s % 6.93/1.98 % (1597212)Peak memory usage: 88 MB % 6.93/1.98 % (1597212)Instructions burned: 1 (million) % 6.93/1.98 % (1597213)lrs+10_1_sil=32000:urr=on:br=off:random_seed=3553067210:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi) % 12.18/2.62 % (1597201)------------------------------ % 12.18/2.62 % (1597201)------------------------------ % 12.18/2.62 % (1597213)Refutation not found, incomplete strategy % 12.18/2.62 % (1597213)------------------------------ % 12.18/2.62 % (1597213)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.18/2.62 % (1597213)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.18/2.62 % (1597213)CaDiCaL version: 2.1.3 % 12.18/2.62 % (1597213)Termination reason: Refutation not found, incomplete strategy % 12.18/2.62 % (1597213)Time elapsed: 0.002 s % 12.18/2.62 % (1597213)Peak memory usage: 88 MB % 12.18/2.62 % (1597213)Instructions burned: 1 (million) % 12.18/2.62 % (1597214)lrs+1011_1_sil=32000:sp=occurrence:random_seed=3870406217:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi) % 12.18/2.62 % (1597214)Refutation not found, incomplete strategy % 12.18/2.62 % (1597214)------------------------------ % 12.18/2.62 % (1597214)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.18/2.62 % (1597214)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.18/2.62 % (1597214)CaDiCaL version: 2.1.3 % 12.18/2.62 % (1597214)Termination reason: Refutation not found, incomplete strategy % 12.18/2.62 % (1597214)Time elapsed: 0.001 s % 12.18/2.62 % (1597214)Peak memory usage: 88 MB % 12.18/2.62 % (1597214)Instructions burned: 1 (million) % 12.18/2.62 [W928 07:05:32.863610604 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 12.18/2.62 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 12.18/2.62 [W928 07:05:32.863657878 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 12.18/2.62 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 12.18/2.62 [W928 07:05:32.863693228 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 12.18/2.62 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 12.18/2.62 [W928 07:05:32.863704548 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 12.18/2.62 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 12.18/2.62 [W928 07:05:32.863730688 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 12.18/2.62 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 12.18/2.62 [W928 07:05:32.863742971 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 12.18/2.62 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 12.18/2.62 % (1597214)------------------------------ % 12.18/2.62 % (1597214)------------------------------ % 12.18/2.62 % (1597218)dis+10_5:1_slsqr=1,4:sil=8000:fde=unused:erd=off:urr=full:fd=off:s2agt=8:br=off:slsq=on:random_seed=2329685650:s2a=on:i=248:s2at=1.23:gtg=position_2995 on theBenchmark for (2995ds/248Mi) % 12.18/2.62 % (1597212)------------------------------ % 12.18/2.62 % (1597212)------------------------------ % 12.18/2.62 % (1597213)------------------------------ % 12.18/2.62 % (1597213)------------------------------ % 12.18/2.62 % (1597219)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=3148497051:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2994 on theBenchmark for (2994ds/294Mi) % 12.18/2.62 % (1597219)Refutation not found, incomplete strategy % 12.18/2.62 % (1597219)------------------------------ % 12.18/2.62 % (1597219)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.18/2.62 % (1597219)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.34/3.86 % (1597219)CaDiCaL version: 2.1.3 % 20.34/3.86 % (1597219)Termination reason: Refutation not found, incomplete strategy % 20.34/3.86 % (1597219)Time elapsed: 0.002 s % 20.34/3.86 % (1597219)Peak memory usage: 88 MB % 20.34/3.86 % (1597219)Instructions burned: 4 (million) % 20.34/3.86 % (1597218)Instruction limit reached! % 20.34/3.86 % (1597218)------------------------------ % 20.34/3.86 % (1597218)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 20.34/3.86 % (1597218)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.34/3.86 % (1597218)CaDiCaL version: 2.1.3 % 20.34/3.86 % (1597218)Termination reason: Instruction limit % 20.34/3.86 % (1597218)Termination phase: Saturation % 20.34/3.86 % (1597218)Time elapsed: 0.123 s % 20.34/3.86 % (1597218)Peak memory usage: 92 MB % 20.34/3.86 % (1597218)Instructions burned: 249 (million) % 20.34/3.86 % (1597200)Refutation not found, incomplete strategy % 20.34/3.86 % (1597200)------------------------------ % 20.34/3.86 % (1597200)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 20.34/3.86 % (1597200)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.34/3.86 % (1597200)CaDiCaL version: 2.1.3 % 20.34/3.86 % (1597200)Termination reason: Refutation not found, incomplete strategy % 20.34/3.86 % (1597200)Time elapsed: 0.613 s % 20.34/3.86 % (1597200)Peak memory usage: 126 MB % 20.34/3.86 % (1597200)Instructions burned: 889 (million) % 20.34/3.86 % (1597221)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=2782498385:i=2350_2993 on theBenchmark for (2993ds/2350Mi) % 20.34/3.86 % (1597222)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=817167396:cts=off:i=113:fsr=off:ss=included:sgt=4_2993 on theBenchmark for (2993ds/113Mi) % 20.34/3.86 % (1597222)Refutation not found, incomplete strategy % 20.34/3.86 % (1597222)------------------------------ % 20.34/3.86 % (1597222)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 20.34/3.86 % (1597222)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.34/3.86 % (1597222)CaDiCaL version: 2.1.3 % 20.34/3.86 % (1597222)Termination reason: Refutation not found, incomplete strategy % 20.34/3.86 % (1597222)Time elapsed: 0.002 s % 20.34/3.86 % (1597222)Peak memory usage: 88 MB % 20.34/3.86 % (1597222)Instructions burned: 1 (million) % 20.34/3.86 % (1597219)------------------------------ % 20.34/3.86 % (1597219)------------------------------ % 20.34/3.86 % (1597224)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=1025559869:i=127:av=off:fsr=off:sup=off_2992 on theBenchmark for (2992ds/127Mi) % 20.34/3.86 % (1597224)Instruction limit reached! % 20.34/3.86 % (1597224)------------------------------ % 20.34/3.86 % (1597224)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 20.34/3.86 % (1597224)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.34/3.86 % (1597224)CaDiCaL version: 2.1.3 % 20.34/3.86 % (1597224)Termination reason: Instruction limit % 20.34/3.86 % (1597224)Termination phase: Saturation % 20.34/3.86 % (1597224)Time elapsed: 0.063 s % 20.34/3.86 % (1597224)Peak memory usage: 88 MB % 20.34/3.86 % (1597224)Instructions burned: 127 (million) % 20.34/3.86 % (1597227)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=94661539:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2991 on theBenchmark for (2991ds/114Mi) % 20.34/3.86 % (1597227)Instruction limit reached! % 20.34/3.86 % (1597227)------------------------------ % 20.34/3.86 % (1597227)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 20.34/3.86 % (1597227)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.34/3.86 % (1597227)CaDiCaL version: 2.1.3 % 20.34/3.86 % (1597227)Termination reason: Instruction limit % 20.34/3.86 % (1597227)Termination phase: Saturation % 20.34/3.86 % (1597227)Time elapsed: 0.032 s % 20.34/3.86 % (1597227)Peak memory usage: 89 MB % 20.34/3.86 % (1597227)Instructions burned: 115 (million) % 20.34/3.86 % (1597200)------------------------------ % 20.34/3.86 % (1597200)------------------------------ % 20.34/3.86 % (1597222)------------------------------ % 20.34/3.86 % (1597222)------------------------------ % 20.34/3.86 % (1597229)lrs+10_1_sil=8000:sp=occurrence:random_seed=1874595608:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2990 on theBenchmark for (2990ds/907Mi) % 20.34/3.86 % (1597231)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=1663847932:i=437:sd=1:aac=none:ss=included_2989 on theBenchmark for (2989ds/437Mi) % 20.34/3.86 % (1597231)Refutation not found, incomplete strategy % 32.55/5.49 % (1597231)------------------------------ % 32.55/5.49 % (1597231)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 32.55/5.49 % (1597231)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.55/5.49 % (1597231)CaDiCaL version: 2.1.3 % 32.55/5.49 % (1597231)Termination reason: Refutation not found, incomplete strategy % 32.55/5.49 % (1597231)Time elapsed: 0.001 s % 32.55/5.49 % (1597231)Peak memory usage: 88 MB % 32.55/5.49 % (1597232)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=753828975:i=5202:ss=axioms:sgt=16_2989 on theBenchmark for (2989ds/5202Mi) % 32.55/5.49 % (1597229)Refutation not found, incomplete strategy % 32.55/5.49 % (1597229)------------------------------ % 32.55/5.49 % (1597229)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 32.55/5.49 % (1597229)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.55/5.49 % (1597229)CaDiCaL version: 2.1.3 % 32.55/5.49 % (1597229)Termination reason: Refutation not found, incomplete strategy % 32.55/5.49 % (1597229)Time elapsed: 0.124 s % 32.55/5.49 % (1597229)Peak memory usage: 90 MB % 32.55/5.49 % (1597229)Instructions burned: 195 (million) % 32.55/5.49 % (1597233)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=937980572:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2989 on theBenchmark for (2989ds/134Mi) % 32.55/5.49 % (1597233)Refutation not found, incomplete strategy % 32.55/5.49 % (1597233)------------------------------ % 32.55/5.49 % (1597233)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 32.55/5.49 % (1597233)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.55/5.49 % (1597233)CaDiCaL version: 2.1.3 % 32.55/5.49 % (1597233)Termination reason: Refutation not found, incomplete strategy % 32.55/5.49 % (1597233)Time elapsed: 0.003 s % 32.55/5.49 % (1597233)Peak memory usage: 88 MB % 32.55/5.49 % (1597233)Instructions burned: 3 (million) % 32.55/5.49 % (1597231)------------------------------ % 32.55/5.49 % (1597231)------------------------------ % 32.55/5.49 % (1597238)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=2657429047:st=8:i=592:sd=3:ep=RST:ss=axioms_2986 on theBenchmark for (2986ds/592Mi) % 32.55/5.49 % (1597229)------------------------------ % 32.55/5.49 % (1597229)------------------------------ % 32.55/5.49 % (1597233)------------------------------ % 32.55/5.49 % (1597233)------------------------------ % 32.55/5.49 % (1597238)Instruction limit reached! % 32.55/5.49 % (1597238)------------------------------ % 32.55/5.49 % (1597238)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 32.55/5.49 % (1597238)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.55/5.49 % (1597238)CaDiCaL version: 2.1.3 % 32.55/5.49 % (1597238)Termination reason: Instruction limit % 32.55/5.49 % (1597238)Termination phase: Saturation % 32.55/5.49 % (1597238)Time elapsed: 0.186 s % 32.55/5.49 % (1597238)Peak memory usage: 91 MB % 32.55/5.49 % (1597238)Instructions burned: 594 (million) % 32.55/5.49 % (1597240)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=3686378731:st=3:i=13193:sd=3:ss=axioms_2985 on theBenchmark for (2985ds/13193Mi) % 32.55/5.49 % (1597241)lrs+1666_7_slsqr=4,1:sil=8000:plsq=on:plsqc=1:sos=on:urr=on:plsql=on:rp=on:alpa=false:sac=on:slsq=on:random_seed=788353155:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2984 on theBenchmark for (2984ds/125Mi) % 32.55/5.49 % (1597241)Refutation not found, incomplete strategy % 32.55/5.49 % (1597241)------------------------------ % 32.55/5.49 % (1597241)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 32.55/5.49 % (1597241)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.55/5.49 % (1597241)CaDiCaL version: 2.1.3 % 32.55/5.49 % (1597241)Termination reason: Refutation not found, incomplete strategy % 32.55/5.49 % (1597241)Time elapsed: 0.004 s % 32.55/5.49 % (1597241)Peak memory usage: 89 MB % 32.55/5.49 % (1597241)Instructions burned: 3 (million) % 32.55/5.49 % (1597242)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=2802615250:i=134:gtgl=5:slsql=off:gtg=exists_sym_2983 on theBenchmark for (2983ds/134Mi) % 32.55/5.49 % (1597242)Instruction limit reached! % 32.55/5.49 % (1597242)------------------------------ % 32.55/5.49 % (1597242)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 32.55/5.49 % (1597242)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 44.98/7.14 % (1597242)CaDiCaL version: 2.1.3 % 44.98/7.14 % (1597242)Termination reason: Instruction limit % 44.98/7.14 % (1597242)Termination phase: Saturation % 44.98/7.14 % (1597242)Time elapsed: 0.042 s % 44.98/7.14 % (1597242)Peak memory usage: 90 MB % 44.98/7.14 % (1597242)Instructions burned: 136 (million) % 44.98/7.14 % (1597241)------------------------------ % 44.98/7.14 % (1597241)------------------------------ % 44.98/7.14 % (1597246)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=3990960397:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2982 on theBenchmark for (2982ds/141Mi) % 44.98/7.14 % (1597246)Refutation not found, incomplete strategy % 44.98/7.14 % (1597246)------------------------------ % 44.98/7.14 % (1597246)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 44.98/7.14 % (1597246)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 44.98/7.14 % (1597246)CaDiCaL version: 2.1.3 % 44.98/7.14 % (1597246)Termination reason: Refutation not found, incomplete strategy % 44.98/7.14 % (1597246)Time elapsed: 0.001 s % 44.98/7.14 % (1597246)Peak memory usage: 88 MB % 44.98/7.14 % (1597246)------------------------------ % 44.98/7.14 % (1597246)------------------------------ % 44.98/7.14 % (1597247)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=3824851532:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2980 on theBenchmark for (2980ds/431Mi) % 44.98/7.14 % (1597247)Refutation not found, incomplete strategy % 44.98/7.14 % (1597247)------------------------------ % 44.98/7.14 % (1597247)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 44.98/7.14 % (1597247)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 44.98/7.14 % (1597247)CaDiCaL version: 2.1.3 % 44.98/7.14 % (1597247)Termination reason: Refutation not found, incomplete strategy % 44.98/7.14 % (1597247)Time elapsed: 0.001 s % 44.98/7.14 % (1597247)Peak memory usage: 88 MB % 44.98/7.14 % (1597249)lrs+1010_1_ncem=casc2026/models/loop6.pt:sil=64000:tgt=full:npcc=on:prc=on:urr=ec_only:bsr=on:fd=preordered:gs=on:sac=on:newcnf=on:random_seed=1121139723:i=6060:aac=none:ins=25_2979 on theBenchmark for (2979ds/6060Mi) % 44.98/7.14 % (1597247)------------------------------ % 44.98/7.14 % (1597247)------------------------------ % 44.98/7.14 % (1597221)Instruction limit reached! % 44.98/7.14 % (1597221)------------------------------ % 44.98/7.14 % (1597221)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 44.98/7.14 % (1597221)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 44.98/7.14 % (1597221)CaDiCaL version: 2.1.3 % 44.98/7.14 % (1597221)Termination reason: Instruction limit % 44.98/7.14 % (1597221)Termination phase: Saturation % 44.98/7.14 % (1597221)Time elapsed: 1.521 s % 44.98/7.14 % (1597221)Peak memory usage: 141 MB % 44.98/7.14 % (1597221)Instructions burned: 2350 (million) % 44.98/7.14 % (1597252)lrs+10_16_anc=all:slsqr=32,1:sil=8000:avsql=on:sp=unary_frequency:lcm=predicate:urr=full:rp=on:br=off:slsqc=4:flr=on:sac=on:slsq=on:avsqc=1:random_seed=4189369891:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2976 on theBenchmark for (2976ds/150Mi) % 44.98/7.14 % (1597253)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=3840325977:i=14155:bd=all_2976 on theBenchmark for (2976ds/14155Mi) % 44.98/7.14 % (1597252)Instruction limit reached! % 44.98/7.14 % (1597252)------------------------------ % 44.98/7.14 % (1597252)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 44.98/7.14 % (1597252)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 44.98/7.14 % (1597252)CaDiCaL version: 2.1.3 % 44.98/7.14 % (1597252)Termination reason: Instruction limit % 44.98/7.14 % (1597252)Termination phase: Saturation % 44.98/7.14 % (1597252)Time elapsed: 0.078 s % 44.98/7.14 % (1597252)Peak memory usage: 90 MB % 44.98/7.14 % (1597252)Instructions burned: 151 (million) % 44.98/7.14 % (1597256)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=3076946680:i=667:av=off:fsr=off_2974 on theBenchmark for (2974ds/667Mi) % 44.98/7.14 % (1597256)Instruction limit reached! % 44.98/7.14 % (1597256)------------------------------ % 44.98/7.14 % (1597256)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 44.98/7.14 % (1597256)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 44.98/7.14 % (1597256)CaDiCaL version: 2.1.3 % 44.98/7.14 % (1597256)Termination reason: Instruction limit % 44.98/7.14 % (1597256)Termination phase: Saturation % 52.54/8.23 % (1597256)Time elapsed: 0.283 s % 52.54/8.23 % (1597256)Peak memory usage: 103 MB % 52.54/8.23 % (1597256)Instructions burned: 668 (million) % 52.54/8.23 % (1597258)ott-1011_3:1_anc=all_dependent:to=lpo:sil=8000:drc=ordering:sas=cadical:fdtod=off:sp=reverse_frequency:spb=goal_then_units:urr=full:lftc=20:newcnf=on:random_seed=100297846:s2a=on:i=185:s2at=1.8:fdi=4_2969 on theBenchmark for (2969ds/185Mi) % 52.54/8.23 % (1597258)Instruction limit reached! % 52.54/8.23 % (1597258)------------------------------ % 52.54/8.23 % (1597258)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 52.54/8.23 % (1597258)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 52.54/8.23 % (1597258)CaDiCaL version: 2.1.3 % 52.54/8.23 % (1597258)Termination reason: Instruction limit % 52.54/8.23 % (1597258)Termination phase: Saturation % 52.54/8.23 % (1597258)Time elapsed: 0.094 s % 52.54/8.23 % (1597258)Peak memory usage: 90 MB % 52.54/8.23 % (1597258)Instructions burned: 187 (million) % 52.54/8.23 % (1597260)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=2258299947:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2967 on theBenchmark for (2967ds/193Mi) % 52.54/8.23 % (1597260)Refutation not found, incomplete strategy % 52.54/8.23 % (1597260)------------------------------ % 52.54/8.23 % (1597260)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 52.54/8.23 % (1597260)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 52.54/8.23 % (1597260)CaDiCaL version: 2.1.3 % 52.54/8.23 % (1597260)Termination reason: Refutation not found, incomplete strategy % 52.54/8.23 % (1597260)Time elapsed: 0.001 s % 52.54/8.23 % (1597260)Peak memory usage: 86 MB % 52.54/8.23 % (1597260)Instructions burned: 1 (million) % 52.54/8.23 % (1597260)------------------------------ % 52.54/8.23 % (1597260)------------------------------ % 52.54/8.23 % (1597262)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=1608427860:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2962 on theBenchmark for (2962ds/4850Mi) % 52.54/8.23 % (1597232)Instruction limit reached! % 52.54/8.23 % (1597232)------------------------------ % 52.54/8.23 % (1597232)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 52.54/8.23 % (1597232)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 52.54/8.23 % (1597232)CaDiCaL version: 2.1.3 % 52.54/8.23 % (1597232)Termination reason: Instruction limit % 52.54/8.23 % (1597232)Termination phase: Saturation % 52.54/8.23 % (1597232)Time elapsed: 2.914 s % 52.54/8.23 % (1597232)Peak memory usage: 141 MB % 52.54/8.23 % (1597232)Instructions burned: 5204 (million) % 52.54/8.23 % (1597249)Instruction limit reached! % 52.54/8.23 % (1597249)------------------------------ % 52.54/8.23 % (1597249)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 52.54/8.23 % (1597249)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 52.54/8.23 % (1597249)CaDiCaL version: 2.1.3 % 52.54/8.23 % (1597249)Termination reason: Instruction limit % 52.54/8.23 % (1597249)Termination phase: Saturation % 52.54/8.23 % (1597249)Time elapsed: 2.025 s % 52.54/8.23 % (1597249)Peak memory usage: 157 MB % 52.54/8.23 % (1597249)Instructions burned: 6062 (million) % 52.54/8.23 % (1597264)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=3038069737:i=12111:sd=1:ss=included_2958 on theBenchmark for (2958ds/12111Mi) % 52.54/8.23 % (1597265)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=215917943:i=319:kws=precedence:fsr=off_2957 on theBenchmark for (2957ds/319Mi) % 52.54/8.23 % (1597265)Instruction limit reached! % 52.54/8.23 % (1597265)------------------------------ % 52.54/8.23 % (1597265)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 52.54/8.23 % (1597265)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 52.54/8.23 % (1597265)CaDiCaL version: 2.1.3 % 52.54/8.23 % (1597265)Termination reason: Instruction limit % 52.54/8.23 % (1597265)Termination phase: Saturation % 52.54/8.23 % (1597265)Time elapsed: 0.096 s % 52.54/8.23 % (1597265)Peak memory usage: 92 MB % 52.54/8.23 % (1597265)Instructions burned: 321 (million) % 52.54/8.23 % (1597268)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=2714158852:i=2064:ep=RST_2955 on theBenchmark for (2955ds/2064Mi) % 52.54/8.23 [W928 07:05:36.961078725 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 56.65/8.87 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 56.65/8.87 [W928 07:05:36.961110962 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 56.65/8.87 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 56.65/8.87 [W928 07:05:36.961169002 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 56.65/8.87 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 56.65/8.87 [W928 07:05:36.961180509 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 56.65/8.87 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 56.65/8.87 [W928 07:05:36.961206012 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 56.65/8.87 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 56.65/8.87 [W928 07:05:36.961227052 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 56.65/8.87 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 56.65/8.87 % (1597264)Refutation not found, incomplete strategy % 56.65/8.87 % (1597264)------------------------------ % 56.65/8.87 % (1597264)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 56.65/8.87 % (1597264)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 56.65/8.87 % (1597264)CaDiCaL version: 2.1.3 % 56.65/8.87 % (1597264)Termination reason: Refutation not found, incomplete strategy % 56.65/8.87 % (1597264)Time elapsed: 0.572 s % 56.65/8.87 % (1597264)Peak memory usage: 128 MB % 56.65/8.87 % (1597264)Instructions burned: 862 (million) % 56.65/8.87 % (1597268)Instruction limit reached! % 56.65/8.87 % (1597268)------------------------------ % 56.65/8.87 % (1597268)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 56.65/8.87 % (1597268)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 56.65/8.87 % (1597268)CaDiCaL version: 2.1.3 % 56.65/8.87 % (1597268)Termination reason: Instruction limit % 56.65/8.87 % (1597268)Termination phase: Saturation % 56.65/8.87 % (1597268)Time elapsed: 0.423 s % 56.65/8.87 % (1597268)Peak memory usage: 90 MB % 56.65/8.87 % (1597268)Instructions burned: 2069 (million) % 56.65/8.87 % (1597264)------------------------------ % 56.65/8.87 % (1597264)------------------------------ % 56.65/8.87 % (1597270)dis-1011_128_sil=32000:random_seed=4227970599:i=3706:ep=RST:av=off_2949 on theBenchmark for (2949ds/3706Mi) % 56.65/8.87 % (1597271)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=720753348:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2948 on theBenchmark for (2948ds/757Mi) % 56.65/8.87 % (1597271)Refutation not found, incomplete strategy % 56.65/8.87 % (1597271)------------------------------ % 56.65/8.87 % (1597271)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 56.65/8.87 % (1597271)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 56.65/8.87 % (1597271)CaDiCaL version: 2.1.3 % 56.65/8.87 % (1597271)Termination reason: Refutation not found, incomplete strategy % 56.65/8.87 % (1597271)Time elapsed: 0.003 s % 56.65/8.87 % (1597271)Peak memory usage: 88 MB % 56.65/8.87 % (1597271)Instructions burned: 3 (million) % 56.65/8.87 % (1597271)------------------------------ % 56.65/8.87 % (1597271)------------------------------ % 56.65/8.87 % (1597274)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=occurrence:random_seed=2627331737:i=13913:ss=axioms:sgt=8_2944 on theBenchmark for (2944ds/13913Mi) % 56.65/8.87 % (1597270)Instruction limit reached! % 56.65/8.87 % (1597270)------------------------------ % 56.65/8.87 % (1597270)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 56.65/8.87 % (1597270)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 70.45/10.85 % (1597270)CaDiCaL version: 2.1.3 % 70.45/10.85 % (1597270)Termination reason: Instruction limit % 70.45/10.85 % (1597270)Termination phase: Saturation % 70.45/10.85 % (1597270)Time elapsed: 1.177 s % 70.45/10.85 % (1597270)Peak memory usage: 107 MB % 70.45/10.85 % (1597270)Instructions burned: 3708 (million) % 70.45/10.85 % (1597274)Refutation not found, incomplete strategy % 70.45/10.85 % (1597274)------------------------------ % 70.45/10.85 % (1597274)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 70.45/10.85 % (1597274)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 70.45/10.85 % (1597274)CaDiCaL version: 2.1.3 % 70.45/10.85 % (1597274)Termination reason: Refutation not found, incomplete strategy % 70.45/10.85 % (1597274)Time elapsed: 0.635 s % 70.45/10.85 % (1597274)Peak memory usage: 128 MB % 70.45/10.85 % (1597274)Instructions burned: 963 (million) % 70.45/10.85 % (1597262)Instruction limit reached! % 70.45/10.85 % (1597262)------------------------------ % 70.45/10.85 % (1597262)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 70.45/10.85 % (1597262)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 70.45/10.85 % (1597262)CaDiCaL version: 2.1.3 % 70.45/10.85 % (1597262)Termination reason: Instruction limit % 70.45/10.85 % (1597262)Termination phase: Saturation % 70.45/10.85 % (1597262)Time elapsed: 2.552 s % 70.45/10.85 % (1597262)Peak memory usage: 105 MB % 70.45/10.85 % (1597262)Instructions burned: 4852 (million) % 70.45/10.85 % (1597276)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_frequency:sos=all:lma=off:random_seed=633081732:i=9925:aac=none_2936 on theBenchmark for (2936ds/9925Mi) % 70.45/10.85 % (1597274)------------------------------ % 70.45/10.85 % (1597274)------------------------------ % 70.45/10.85 % (1597278)dis-1010_50_to=lpo:sil=32000:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=3896035006:i=2479:sd=2:nm=16:fsr=off:ss=axioms_2935 on theBenchmark for (2935ds/2479Mi) % 70.45/10.85 % (1597278)Refutation not found, incomplete strategy % 70.45/10.85 % (1597278)------------------------------ % 70.45/10.85 % (1597278)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 70.45/10.85 % (1597278)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 70.45/10.85 % (1597278)CaDiCaL version: 2.1.3 % 70.45/10.85 % (1597278)Termination reason: Refutation not found, incomplete strategy % 70.45/10.85 % (1597278)Time elapsed: 0.001 s % 70.45/10.85 % (1597278)Peak memory usage: 86 MB % 70.45/10.85 % (1597279)ott+1002_64_sil=16000:sp=const_min:nwc=0.5:random_seed=4059140670:i=440:nm=2:av=off:gtg=exists_all:fdi=8:gsp=on_2934 on theBenchmark for (2934ds/440Mi) % 70.45/10.85 % (1597278)------------------------------ % 70.45/10.85 % (1597278)------------------------------ % 70.45/10.85 % (1597279)Instruction limit reached! % 70.45/10.85 % (1597279)------------------------------ % 70.45/10.85 % (1597279)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 70.45/10.85 % (1597279)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 70.45/10.85 % (1597279)CaDiCaL version: 2.1.3 % 70.45/10.85 % (1597279)Termination reason: Instruction limit % 70.45/10.85 % (1597279)Termination phase: Saturation % 70.45/10.85 % (1597279)Time elapsed: 0.206 s % 70.45/10.85 % (1597279)Peak memory usage: 92 MB % 70.45/10.85 % (1597279)Instructions burned: 442 (million) % 70.45/10.85 % (1597282)dis-1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=693877698:st=1.5:i=11145:s2at=3:sd=3:fsr=off:ss=axioms_2931 on theBenchmark for (2931ds/11145Mi) % 70.45/10.85 % (1597283)lrs+1002_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=unary_frequency:lcm=reverse:urr=on:bsr=on:random_seed=3530575853:cts=off:i=3034:av=off:er=known:fsd=on_2930 on theBenchmark for (2930ds/3034Mi) % 70.45/10.85 [W928 07:05:39.707642537 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 70.45/10.85 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 70.45/10.85 [W928 07:05:39.707676080 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 70.45/10.85 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 77.74/11.81 [W928 07:05:39.707713870 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 77.74/11.81 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 77.74/11.81 [W928 07:05:39.707725083 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 77.74/11.81 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 77.74/11.81 [W928 07:05:39.707749543 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 77.74/11.81 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 77.74/11.81 [W928 07:05:39.707759527 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 77.74/11.81 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 77.74/11.81 [W928 07:05:39.707801714 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 77.74/11.81 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 77.74/11.81 [W928 07:05:39.707811847 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 77.74/11.81 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 77.74/11.81 [W928 07:05:39.707835010 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 77.74/11.81 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 77.74/11.81 [W928 07:05:39.707844864 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 77.74/11.81 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 77.74/11.81 [W928 07:05:39.707869144 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 77.74/11.81 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 77.74/11.81 [W928 07:05:39.707879244 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 77.74/11.81 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 77.74/11.81 % (1597282)Refutation not found, incomplete strategy % 77.74/11.81 % (1597282)------------------------------ % 77.74/11.81 % (1597282)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 77.74/11.81 % (1597282)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 77.74/11.81 % (1597282)CaDiCaL version: 2.1.3 % 77.74/11.81 % (1597282)Termination reason: Refutation not found, incomplete strategy % 77.74/11.81 % (1597282)Time elapsed: 0.549 s % 77.74/11.81 % (1597282)Peak memory usage: 125 MB % 77.74/11.81 % (1597282)Instructions burned: 828 (million) % 77.74/11.81 % (1597282)------------------------------ % 77.74/11.81 % (1597282)------------------------------ % 77.74/11.81 % (1597286)lrs-1011_64:1_sil=8000:erd=off:urr=on:nwc=0.7:br=off:random_seed=3452267913:st=2:s2a=on:i=524:s2at=2:ss=axioms_2921 on theBenchmark for (2921ds/524Mi) % 77.74/11.81 % (1597286)Refutation not found, incomplete strategy % 77.74/11.81 % (1597286)------------------------------ % 77.74/11.81 % (1597286)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 81.76/12.42 % (1597286)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 81.76/12.42 % (1597286)CaDiCaL version: 2.1.3 % 81.76/12.42 % (1597286)Termination reason: Refutation not found, incomplete strategy % 81.76/12.42 % (1597286)Time elapsed: 0.048 s % 81.76/12.42 % (1597286)Peak memory usage: 89 MB % 81.76/12.42 % (1597286)Instructions burned: 98 (million) % 81.76/12.42 % (1597286)------------------------------ % 81.76/12.42 % (1597286)------------------------------ % 81.76/12.42 % (1597288)lrs+1011_16:1_sil=8000:acc=on:urr=on:fd=preordered:flr=on:random_seed=1577786777:avsq=on:i=1016:avsqr=676809,524288:sd=1:ss=axioms_2917 on theBenchmark for (2917ds/1016Mi) % 81.76/12.42 % (1597288)Refutation not found, incomplete strategy % 81.76/12.42 % (1597288)------------------------------ % 81.76/12.42 % (1597288)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 81.76/12.42 % (1597288)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 81.76/12.42 % (1597288)CaDiCaL version: 2.1.3 % 81.76/12.42 % (1597288)Termination reason: Refutation not found, incomplete strategy % 81.76/12.42 % (1597288)Time elapsed: 0.001 s % 81.76/12.42 % (1597288)Peak memory usage: 87 MB % 81.76/12.42 % (1597288)------------------------------ % 81.76/12.42 % (1597288)------------------------------ % 81.76/12.42 % (1597290)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:fde=none:s2agt=16:random_seed=578761958:i=14123:bd=preordered:ins=4_2913 on theBenchmark for (2913ds/14123Mi) % 81.76/12.42 % (1597283)Instruction limit reached! % 81.76/12.42 % (1597283)------------------------------ % 81.76/12.42 % (1597283)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 81.76/12.42 % (1597283)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 81.76/12.42 % (1597283)CaDiCaL version: 2.1.3 % 81.76/12.42 % (1597283)Termination reason: Instruction limit % 81.76/12.42 % (1597283)Termination phase: Saturation % 81.76/12.42 % (1597283)Time elapsed: 1.798 s % 81.76/12.42 % (1597283)Peak memory usage: 141 MB % 81.76/12.42 % (1597283)Instructions burned: 3035 (million) % 81.76/12.42 % (1597292)dis+10_4096_slsqr=16,1:sil=32000:tgt=full:plsq=on:bsr=unit_only:slsqc=1:slsq=on:random_seed=1746911062:i=5781:kws=precedence:bd=all:rawr=on_2910 on theBenchmark for (2910ds/5781Mi) % 81.76/12.42 % (1597276)Instruction limit reached! % 81.76/12.42 % (1597276)------------------------------ % 81.76/12.42 % (1597276)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 81.76/12.42 % (1597276)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 81.76/12.42 % (1597276)CaDiCaL version: 2.1.3 % 81.76/12.42 % (1597276)Termination reason: Instruction limit % 81.76/12.42 % (1597276)Termination phase: Saturation % 81.76/12.42 % (1597276)Time elapsed: 3.251 s % 81.76/12.42 % (1597276)Peak memory usage: 182 MB % 81.76/12.42 % (1597276)Instructions burned: 9928 (million) % 81.76/12.42 % (1597240)Instruction limit reached! % 81.76/12.42 % (1597240)------------------------------ % 81.76/12.42 % (1597240)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 81.76/12.42 % (1597240)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 81.76/12.42 % (1597240)CaDiCaL version: 2.1.3 % 81.76/12.42 % (1597240)Termination reason: Instruction limit % 81.76/12.42 % (1597240)Termination phase: Saturation % 81.76/12.42 % (1597240)Time elapsed: 8.128 s % 81.76/12.42 % (1597240)Peak memory usage: 215 MB % 81.76/12.42 % (1597240)Instructions burned: 13195 (million) % 81.76/12.42 % (1597294)lrs-1011_1_to=lpo:ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:drc=off:sp=reverse_frequency:erd=off:urr=on:br=off:random_seed=2657580499:i=2448:gtgl=5:bd=preordered:gtg=all_2903 on theBenchmark for (2903ds/2448Mi) % 81.76/12.42 % (1597253)Instruction limit reached! % 81.76/12.42 % (1597253)------------------------------ % 81.76/12.42 % (1597253)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 81.76/12.42 % (1597253)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 81.76/12.42 % (1597253)CaDiCaL version: 2.1.3 % 81.76/12.42 % (1597253)Termination reason: Instruction limit % 81.76/12.42 % (1597253)Termination phase: Saturation % 81.76/12.42 % (1597253)Time elapsed: 7.339 s % 81.76/12.42 % (1597253)Peak memory usage: 205 MB % 81.76/12.42 % (1597253)Instructions burned: 14155 (million) % 81.76/12.42 % (1597295)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:lcm=reverse:random_seed=696369629:i=3223:kws=precedence:fgj=on:av=off_2902 on theBenchmark for (2902ds/3223Mi) % 81.76/12.42 % (1597297)lrs+1002_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:sp=occurrence:sos=on:random_seed=3939791544:st=5.6:i=2033:sd=3:ss=axioms_2901 on theBenchmark for (2901ds/2033Mi) % 84.82/12.97 % (1597294)Instruction limit reached! % 84.82/12.97 % (1597294)------------------------------ % 84.82/12.97 % (1597294)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 84.82/12.97 % (1597294)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 84.82/12.97 % (1597294)CaDiCaL version: 2.1.3 % 84.82/12.97 % (1597294)Termination reason: Instruction limit % 84.82/12.97 % (1597294)Termination phase: Saturation % 84.82/12.97 % (1597294)Time elapsed: 0.831 s % 84.82/12.97 % (1597294)Peak memory usage: 144 MB % 84.82/12.97 % (1597294)Instructions burned: 2453 (million) % 84.82/12.97 % (1597300)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:bsd=on:random_seed=3956009609:i=2055:nm=16:gtg=position:ss=axioms:fsd=on_2893 on theBenchmark for (2893ds/2055Mi) % 84.82/12.97 [W928 07:05:42.285055551 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 84.82/12.97 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 84.82/12.97 [W928 07:05:42.285078878 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 84.82/12.97 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 84.82/12.97 [W928 07:05:42.285100799 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 84.82/12.97 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 84.82/12.97 [W928 07:05:42.285108378 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 84.82/12.97 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 84.82/12.97 [W928 07:05:42.285122941 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 84.82/12.97 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 84.82/12.97 [W928 07:05:42.285129674 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 84.82/12.97 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 84.82/12.97 [W928 07:05:42.285143101 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 84.82/12.97 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 84.82/12.97 [W928 07:05:42.285149967 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 84.82/12.97 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 84.82/12.97 [W928 07:05:42.285162742 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 84.82/12.97 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 84.82/12.97 [W928 07:05:42.285169300 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 84.82/12.97 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 84.82/12.97 [W928 07:05:42.285182312 register_special_ops.cpp:225] Warning: Creating a tensor from 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.19/14.82 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 99.19/14.82 [W928 07:05:42.285188857 register_special_ops.cpp:225] Warning: Creating a tensor from 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.19/14.82 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 99.19/14.82 % (1597300)Refutation not found, incomplete strategy % 99.19/14.82 % (1597300)------------------------------ % 99.19/14.82 % (1597300)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 99.19/14.82 % (1597300)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 99.19/14.82 % (1597300)CaDiCaL version: 2.1.3 % 99.19/14.82 % (1597300)Termination reason: Refutation not found, incomplete strategy % 99.19/14.82 % (1597300)Time elapsed: 0.306 s % 99.19/14.82 % (1597300)Peak memory usage: 126 MB % 99.19/14.82 % (1597300)Instructions burned: 827 (million) % 99.19/14.82 % (1597300)------------------------------ % 99.19/14.82 % (1597300)------------------------------ % 99.19/14.82 % (1597297)Instruction limit reached! % 99.19/14.82 % (1597297)------------------------------ % 99.19/14.82 % (1597297)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 99.19/14.82 % (1597297)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 99.19/14.82 % (1597297)CaDiCaL version: 2.1.3 % 99.19/14.82 % (1597297)Termination reason: Instruction limit % 99.19/14.82 % (1597297)Termination phase: Saturation % 99.19/14.82 % (1597297)Time elapsed: 1.310 s % 99.19/14.82 % (1597297)Peak memory usage: 132 MB % 99.19/14.82 % (1597297)Instructions burned: 2034 (million) % 99.19/14.82 % (1597302)dis+1010_1_ncem=casc2026/models/loop7.pt:sil=64000:tgt=full:npcc=on:fde=unused:sp=const_frequency:spb=goal:acc=on:random_seed=634756350:i=21611:sd=3:ss=axioms_2887 on theBenchmark for (2887ds/21611Mi) % 99.19/14.82 % (1597303)lrs+10_1_sil=8000:sp=occurrence:sos=all:lma=off:random_seed=1873890515:i=4835:sd=13:ss=axioms:sgt=23_2886 on theBenchmark for (2886ds/4835Mi) % 99.19/14.82 [W928 07:05:43.891548047 register_special_ops.cpp:225] Warning: Creating a tensor from 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.19/14.82 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 99.19/14.82 [W928 07:05:43.891571854 register_special_ops.cpp:225] Warning: Creating a tensor from 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.19/14.82 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 99.19/14.82 [W928 07:05:43.891592306 register_special_ops.cpp:225] Warning: Creating a tensor from 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.19/14.82 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 99.19/14.82 [W928 07:05:43.891602330 register_special_ops.cpp:225] Warning: Creating a tensor from 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.19/14.82 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 99.19/14.82 [W928 07:05:43.891615883 register_special_ops.cpp:225] Warning: Creating a tensor from 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.19/14.82 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 99.19/14.82 [W928 07:05:43.891622586 register_special_ops.cpp:225] Warning: Creating a tensor from 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.19/14.82 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 99.19/14.82 [W928 07:05:43.891636241 register_special_ops.cpp:225] Warning: Creating a tensor from 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.19/14.82 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 108.77/16.16 [W928 07:05:43.891642847 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 108.77/16.16 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 108.77/16.16 [W928 07:05:43.891667230 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 108.77/16.16 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 108.77/16.16 [W928 07:05:43.891673026 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 108.77/16.16 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 108.77/16.16 [W928 07:05:43.891685853 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 108.77/16.16 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 108.77/16.16 [W928 07:05:43.891691480 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 108.77/16.16 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 108.77/16.16 % (1597302)Refutation not found, incomplete strategy % 108.77/16.16 % (1597302)------------------------------ % 108.77/16.16 % (1597302)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 108.77/16.16 % (1597302)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 108.77/16.16 % (1597302)CaDiCaL version: 2.1.3 % 108.77/16.16 % (1597302)Termination reason: Refutation not found, incomplete strategy % 108.77/16.16 % (1597302)Time elapsed: 0.304 s % 108.77/16.16 % (1597302)Peak memory usage: 126 MB % 108.77/16.16 % (1597302)Instructions burned: 827 (million) % 108.77/16.16 % (1597302)------------------------------ % 108.77/16.16 % (1597302)------------------------------ % 108.77/16.16 % (1597306)lrs+10_1_to=lpo:sil=32000:plsq=on:plsqc=1:bsd=on:plsqr=64,1:sp=reverse_frequency:bsr=unit_only:plsql=on:fd=off:slsqc=4:newcnf=on:slsq=on:random_seed=2969136403:st=5:i=797:s2at=3:sd=4:bs=unit_only:av=off:sup=off:ss=included_2881 on theBenchmark for (2881ds/797Mi) % 108.77/16.16 % (1597292)Instruction limit reached! % 108.77/16.16 % (1597292)------------------------------ % 108.77/16.16 % (1597292)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 108.77/16.16 % (1597292)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 108.77/16.16 % (1597292)CaDiCaL version: 2.1.3 % 108.77/16.16 % (1597292)Termination reason: Instruction limit % 108.77/16.16 % (1597292)Termination phase: Saturation % 108.77/16.16 % (1597292)Time elapsed: 2.878 s % 108.77/16.16 % (1597292)Peak memory usage: 130 MB % 108.77/16.16 % (1597292)Instructions burned: 5782 (million) % 108.77/16.16 % (1597308)lrs-1011_5_sil=8000:sp=const_max:sos=on:lsd=50:rnwc=on:rp=on:nwc=2.6:alpa=false:random_seed=2651948462:i=2326:kws=inv_precedence:aac=none:nicw=on:bs=unit_only:nm=16:ins=2:fsd=on_2880 on theBenchmark for (2880ds/2326Mi) % 108.77/16.16 % (1597308)Refutation not found, incomplete strategy % 108.77/16.16 % (1597308)------------------------------ % 108.77/16.16 % (1597308)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 108.77/16.16 % (1597308)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 108.77/16.16 % (1597308)CaDiCaL version: 2.1.3 % 108.77/16.16 % (1597308)Termination reason: Refutation not found, incomplete strategy % 108.77/16.16 % (1597308)Time elapsed: 0.008 s % 108.77/16.16 % (1597308)Peak memory usage: 88 MB % 108.77/16.16 % (1597308)Instructions burned: 13 (million) % 108.77/16.16 % (1597295)Instruction limit reached! % 108.77/16.16 % (1597295)------------------------------ % 108.77/16.16 % (1597295)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 108.77/16.16 % (1597295)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 108.77/16.16 % (1597295)CaDiCaL version: 2.1.3 % 108.77/16.16 % (1597295)Termination reason: Instruction limit % 131.96/19.50 % (1597295)Termination phase: Saturation % 131.96/19.50 % (1597295)Time elapsed: 2.191 s % 131.96/19.50 % (1597295)Peak memory usage: 147 MB % 131.96/19.50 % (1597295)Instructions burned: 3223 (million) % 131.96/19.50 % (1597306)Instruction limit reached! % 131.96/19.50 % (1597306)------------------------------ % 131.96/19.50 % (1597306)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 131.96/19.50 % (1597306)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 131.96/19.50 % (1597306)CaDiCaL version: 2.1.3 % 131.96/19.50 % (1597306)Termination reason: Instruction limit % 131.96/19.50 % (1597306)Termination phase: Saturation % 131.96/19.50 % (1597306)Time elapsed: 0.240 s % 131.96/19.50 % (1597306)Peak memory usage: 95 MB % 131.96/19.50 % (1597306)Instructions burned: 799 (million) % 131.96/19.50 % (1597310)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=8000:npcc=on:sos=all:urr=on:br=off:random_seed=303900288:i=6038:nm=6_2878 on theBenchmark for (2878ds/6038Mi) % 131.96/19.50 % (1597311)lrs+10_1_sil=32000:sp=occurrence:random_seed=1643967960:st=2:i=33334:sd=3:ss=included:sgt=32_2877 on theBenchmark for (2877ds/33334Mi) % 131.96/19.50 % (1597308)------------------------------ % 131.96/19.50 % (1597308)------------------------------ % 131.96/19.50 % (1597314)lrs+10_4_sil=8000:plsq=on:plsqr=1,64:sp=occurrence:urr=on:bsr=on:br=off:random_seed=3199743082:st=3.7:s2a=on:i=1008:s2at=1.2:sd=3:bd=all:av=off:fdi=8:sup=off:ss=axioms_2876 on theBenchmark for (2876ds/1008Mi) % 131.96/19.50 % (1597314)Refutation not found, incomplete strategy % 131.96/19.50 % (1597314)------------------------------ % 131.96/19.50 % (1597314)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 131.96/19.50 % (1597314)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 131.96/19.50 % (1597314)CaDiCaL version: 2.1.3 % 131.96/19.50 % (1597314)Termination reason: Refutation not found, incomplete strategy % 131.96/19.50 % (1597314)Time elapsed: 0.040 s % 131.96/19.50 % (1597314)Peak memory usage: 89 MB % 131.96/19.50 % (1597314)Instructions burned: 73 (million) % 131.96/19.50 % (1597314)------------------------------ % 131.96/19.50 % (1597314)------------------------------ % 131.96/19.50 % (1597310)Refutation not found, incomplete strategy % 131.96/19.50 % (1597310)------------------------------ % 131.96/19.50 % (1597310)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 131.96/19.50 % (1597310)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 131.96/19.50 % (1597310)CaDiCaL version: 2.1.3 % 131.96/19.50 % (1597310)Termination reason: Refutation not found, incomplete strategy % 131.96/19.50 % (1597310)Time elapsed: 0.594 s % 131.96/19.50 % (1597310)Peak memory usage: 130 MB % 131.96/19.50 % (1597310)Instructions burned: 889 (million) % 131.96/19.50 % (1597316)lrs+10_1_to=lpo:ncem=casc2026/models/loop6.pt:sil=128000:tgt=ground:npcc=on:fde=none:sp=const_frequency:spb=intro:gs=on:random_seed=2687447649:i=8327:s2at=5:bd=preordered_2871 on theBenchmark for (2871ds/8327Mi) % 131.96/19.50 % (1597310)------------------------------ % 131.96/19.50 % (1597310)------------------------------ % 131.96/19.50 % (1597318)lrs+1002_1_slsqr=3,2:sil=8000:tgt=full:plsq=on:fde=unused:plsqc=1:plsqr=3,2:sp=reverse_arity:spb=intro:urr=on:plsql=on:s2agt=16:br=off:slsqc=2:slsq=on:random_seed=1669117537:s2a=on:i=1083:s2at=1.87328:slsql=off:ep=RSTC:fdi=16_2868 on theBenchmark for (2868ds/1083Mi) % 131.96/19.50 % (1597318)Instruction limit reached! % 131.96/19.50 % (1597318)------------------------------ % 131.96/19.50 % (1597318)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 131.96/19.50 % (1597318)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 131.96/19.50 % (1597318)CaDiCaL version: 2.1.3 % 131.96/19.50 % (1597318)Termination reason: Instruction limit % 131.96/19.50 % (1597318)Termination phase: Saturation % 131.96/19.50 % (1597318)Time elapsed: 0.506 s % 131.96/19.50 % (1597318)Peak memory usage: 99 MB % 131.96/19.50 % (1597318)Instructions burned: 1085 (million) % 131.96/19.50 % (1597320)lrs-1004_3_to=lpo:sil=16000:drc=off:sims=off:spb=goal:fd=preordered:random_seed=3211048987:i=1084:sd=1:bd=preordered:av=off:fsr=off:ss=axioms:sgt=14_2861 on theBenchmark for (2861ds/1084Mi) % 131.96/19.50 % (1597320)Refutation not found, incomplete strategy % 131.96/19.50 % (1597320)------------------------------ % 131.96/19.50 % (1597320)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 131.96/19.50 % (1597320)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 131.96/19.50 % (1597320)CaDiCaL version: 2.1.3 % 131.96/19.50 % (1597320)Termination reason: Refutation not found, incomplete strategy % 136.43/20.04 % (1597320)Time elapsed: 0.001 s % 136.43/20.04 % (1597320)Peak memory usage: 87 MB % 136.43/20.04 % (1597320)Instructions burned: 1 (million) % 136.43/20.04 % (1597320)------------------------------ % 136.43/20.04 % (1597320)------------------------------ % 136.43/20.04 % (1597303)Instruction limit reached! % 136.43/20.04 % (1597303)------------------------------ % 136.43/20.04 % (1597303)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 136.43/20.04 % (1597303)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 136.43/20.04 % (1597303)CaDiCaL version: 2.1.3 % 136.43/20.04 % (1597303)Termination reason: Instruction limit % 136.43/20.04 % (1597303)Termination phase: Saturation % 136.43/20.04 % (1597303)Time elapsed: 2.850 s % 136.43/20.04 % (1597303)Peak memory usage: 142 MB % 136.43/20.04 % (1597303)Instructions burned: 4836 (million) % 136.43/20.04 % (1597322)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=full:npcc=on:erd=off:spb=goal:sac=on:newcnf=on:random_seed=3771130432:i=6995:s2at=5:gtg=all_2857 on theBenchmark for (2857ds/6995Mi) % 136.43/20.04 % (1597323)lrs+10_1_sil=32000:sp=occurrence:sos=on:urr=on:rnwc=on:random_seed=3615490213:st=2:i=6225:sd=15:ss=axioms_2856 on theBenchmark for (2856ds/6225Mi) % 136.43/20.04 % (1597323)Refutation not found, incomplete strategy % 136.43/20.04 % (1597323)------------------------------ % 136.43/20.04 % (1597323)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 136.43/20.04 % (1597323)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 136.43/20.04 % (1597323)CaDiCaL version: 2.1.3 % 136.43/20.04 % (1597323)Termination reason: Refutation not found, incomplete strategy % 136.43/20.04 % (1597323)Time elapsed: 0.005 s % 136.43/20.04 % (1597323)Peak memory usage: 88 MB % 136.43/20.04 % (1597323)Instructions burned: 7 (million) % 136.43/20.04 % (1597323)------------------------------ % 136.43/20.04 % (1597323)------------------------------ % 136.43/20.04 % (1597326)dis-1011_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:lcm=reverse:random_seed=3217316403:cond=fast:i=3372:sd=1:nm=16:gtg=position:ss=axioms_2852 on theBenchmark for (2852ds/3372Mi) % 136.43/20.04 [W928 07:05:47.635604865 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 136.43/20.04 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 136.43/20.04 [W928 07:05:47.635650905 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 136.43/20.04 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 136.43/20.04 [W928 07:05:47.635689189 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 136.43/20.04 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 136.43/20.04 [W928 07:05:47.635701009 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 136.43/20.04 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 136.43/20.04 [W928 07:05:47.635730029 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 136.43/20.04 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 136.43/20.04 [W928 07:05:47.635741795 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 136.43/20.04 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 136.43/20.04 [W928 07:05:47.635768935 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 136.43/20.04 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 160.04/23.43 [W928 07:05:47.635780909 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 160.04/23.43 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 160.04/23.43 [W928 07:05:47.635812926 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 160.04/23.43 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 160.04/23.43 [W928 07:05:47.635823839 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 160.04/23.43 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 160.04/23.43 [W928 07:05:47.635848329 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 160.04/23.43 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 160.04/23.43 [W928 07:05:47.635858546 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 160.04/23.43 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 160.04/23.43 % (1597326)Refutation not found, incomplete strategy % 160.04/23.43 % (1597326)------------------------------ % 160.04/23.43 % (1597326)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 160.04/23.43 % (1597326)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 160.04/23.43 % (1597326)CaDiCaL version: 2.1.3 % 160.04/23.43 % (1597326)Termination reason: Refutation not found, incomplete strategy % 160.04/23.43 % (1597326)Time elapsed: 0.551 s % 160.04/23.43 % (1597326)Peak memory usage: 126 MB % 160.04/23.43 % (1597326)Instructions burned: 828 (million) % 160.04/23.43 % (1597326)------------------------------ % 160.04/23.43 % (1597326)------------------------------ % 160.04/23.43 % (1597328)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sos=all:random_seed=3126388955:st=2.3:i=26457:sd=10:ss=included:sgt=8_2842 on theBenchmark for (2842ds/26457Mi) % 160.04/23.43 % (1597290)Instruction limit reached! % 160.04/23.43 % (1597290)------------------------------ % 160.04/23.43 % (1597290)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 160.04/23.43 % (1597290)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 160.04/23.43 % (1597290)CaDiCaL version: 2.1.3 % 160.04/23.43 % (1597290)Termination reason: Instruction limit % 160.04/23.43 % (1597290)Termination phase: Saturation % 160.04/23.43 % (1597290)Time elapsed: 8.768 s % 160.04/23.43 % (1597290)Peak memory usage: 250 MB % 160.04/23.43 % (1597290)Instructions burned: 14123 (million) % 160.04/23.43 % (1597330)lrs+10_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:foolp=on:s2agt=20:sac=on:random_seed=135706295:i=13494:s2at=1.31:bd=all:ins=10:gtg=exists_top_2823 on theBenchmark for (2823ds/13494Mi) % 160.04/23.43 % (1597316)Instruction limit reached! % 160.04/23.43 % (1597316)------------------------------ % 160.04/23.43 % (1597316)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 160.04/23.43 % (1597316)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 160.04/23.43 % (1597316)CaDiCaL version: 2.1.3 % 160.04/23.43 % (1597316)Termination reason: Instruction limit % 160.04/23.43 % (1597316)Termination phase: Saturation % 160.04/23.43 % (1597316)Time elapsed: 4.868 s % 160.04/23.43 % (1597316)Peak memory usage: 179 MB % 160.04/23.43 % (1597316)Instructions burned: 8328 (million) % 160.04/23.43 % (1597332)dis-1010_1_ncem=casc2026/models/loop5.pt:sil=32000:npcc=on:fde=unused:sp=const_min:spb=goal_then_units:lcm=predicate:acc=on:flr=on:random_seed=847665584:i=2503:nm=4:gsp=on:ss=axioms:sgt=15_2821 on theBenchmark for (2821ds/2503Mi) % 160.04/23.43 % (1597322)Instruction limit reached! % 160.04/23.43 % (1597322)------------------------------ % 160.04/23.43 % (1597322)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 160.04/23.43 % (1597322)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 164.80/24.05 % (1597322)CaDiCaL version: 2.1.3 % 164.80/24.05 % (1597322)Termination reason: Instruction limit % 164.80/24.05 % (1597322)Termination phase: Saturation % 164.80/24.05 % (1597322)Time elapsed: 4.272 s % 164.80/24.05 % (1597322)Peak memory usage: 167 MB % 164.80/24.05 % (1597322)Instructions burned: 6996 (million) % 164.80/24.05 % (1597334)lrs+1011_1_ncem=casc2026/models/loop1.pt:sil=16000:npcc=on:sos=on:lsd=10:random_seed=741849140:i=2559:sd=1:ep=RSTC:ss=axioms_2813 on theBenchmark for (2813ds/2559Mi) % 164.80/24.05 [W928 07:05:51.515503738 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 164.80/24.05 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 164.80/24.05 [W928 07:05:51.515537994 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 164.80/24.05 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 164.80/24.05 [W928 07:05:51.515575931 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 164.80/24.05 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 164.80/24.05 [W928 07:05:51.515588588 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 164.80/24.05 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 164.80/24.05 [W928 07:05:51.515615305 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 164.80/24.05 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 164.80/24.05 [W928 07:05:51.515637008 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 164.80/24.05 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 164.80/24.05 [W928 07:05:51.515664015 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 164.80/24.05 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 164.80/24.05 [W928 07:05:51.515674248 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 164.80/24.05 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 164.80/24.05 [W928 07:05:51.515697428 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 164.80/24.05 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 164.80/24.05 [W928 07:05:51.515707322 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 164.80/24.05 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 164.80/24.05 [W928 07:05:51.515731412 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 164.80/24.05 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 164.80/24.05 [W928 07:05:51.515741418 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 167.33/24.43 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 167.33/24.43 % (1597334)Refutation not found, incomplete strategy % 167.33/24.43 % (1597334)------------------------------ % 167.33/24.43 % (1597334)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 167.33/24.43 % (1597334)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 167.33/24.43 % (1597334)CaDiCaL version: 2.1.3 % 167.33/24.43 % (1597334)Termination reason: Refutation not found, incomplete strategy % 167.33/24.43 % (1597334)Time elapsed: 0.549 s % 167.33/24.43 % (1597334)Peak memory usage: 125 MB % 167.33/24.43 % (1597334)Instructions burned: 823 (million) % 167.33/24.43 % (1597334)------------------------------ % 167.33/24.43 % (1597334)------------------------------ % 167.33/24.43 % (1597332)Instruction limit reached! % 167.33/24.43 % (1597332)------------------------------ % 167.33/24.43 % (1597332)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 167.33/24.43 % (1597332)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 167.33/24.43 % (1597332)CaDiCaL version: 2.1.3 % 167.33/24.43 % (1597332)Termination reason: Instruction limit % 167.33/24.43 % (1597332)Termination phase: Saturation % 167.33/24.43 % (1597332)Time elapsed: 1.589 s % 167.33/24.43 % (1597332)Peak memory usage: 141 MB % 167.33/24.43 % (1597332)Instructions burned: 2504 (million) % 167.33/24.43 % (1597336)ott+1_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:fdtod=off:random_seed=3894777364:i=30753:av=off:ss=included_2803 on theBenchmark for (2803ds/30753Mi) % 167.33/24.43 % (1597337)lrs+10_1024_sil=64000:plsq=on:plsqc=4:plsqr=128,1:urr=on:plsql=on:br=off:random_seed=2930435255:i=26473:ep=RSTC_2803 on theBenchmark for (2803ds/26473Mi) % 167.33/24.43 % (1597311)Instruction limit reached! % 167.33/24.43 % (1597311)------------------------------ % 167.33/24.43 % (1597311)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 167.33/24.43 % (1597311)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 167.33/24.43 % (1597311)CaDiCaL version: 2.1.3 % 167.33/24.43 % (1597311)Termination reason: Instruction limit % 167.33/24.43 % (1597311)Termination phase: Saturation % 167.33/24.43 % (1597311)Time elapsed: 9.257 s % 167.33/24.43 % (1597311)Peak memory usage: 368 MB % 167.33/24.43 % (1597311)Instructions burned: 33336 (million) % 167.33/24.43 % (1597340)dis-1011_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=32000:tgt=ground:npcc=on:sp=arity:sos=on:erd=off:rp=on:gs=on:kmz=on:random_seed=1444939456:cts=off:i=2759:kws=inv_arity:fgj=on_2783 on theBenchmark for (2783ds/2759Mi) % 167.33/24.43 % (1597340)Refutation not found, incomplete strategy % 167.33/24.43 % (1597340)------------------------------ % 167.33/24.43 % (1597340)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 167.33/24.43 % (1597340)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 167.33/24.43 % (1597340)CaDiCaL version: 2.1.3 % 167.33/24.43 % (1597340)Termination reason: Refutation not found, incomplete strategy % 167.33/24.43 % (1597340)Time elapsed: 0.351 s % 167.33/24.43 % (1597340)Peak memory usage: 130 MB % 167.33/24.43 % (1597340)Instructions burned: 889 (million) % 167.33/24.43 % (1597340)------------------------------ % 167.33/24.43 % (1597340)------------------------------ % 167.33/24.43 % (1597342)lrs-1011_1_anc=all_dependent:ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:fde=unused:sp=weighted_frequency:sos=all:spb=goal_then_units:urr=ec_only:sac=on:random_seed=3159990545:st=1.2:i=5665:sd=2:ep=RSTC:gsp=on:ss=axioms_2777 on theBenchmark for (2777ds/5665Mi) % 167.33/24.43 [W928 07:05:54.905092747 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 167.33/24.43 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 167.33/24.43 [W928 07:05:54.905115987 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 167.33/24.43 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 167.33/24.43 [W928 07:05:54.905136539 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 188.93/27.56 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 188.93/27.56 [W928 07:05:54.905143010 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 188.93/27.56 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 188.93/27.56 [W928 07:05:54.905155850 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 188.93/27.56 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 188.93/27.56 [W928 07:05:54.905175885 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 188.93/27.56 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 188.93/27.56 [W928 07:05:54.905188606 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 188.93/27.56 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 188.93/27.56 [W928 07:05:54.905193870 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 188.93/27.56 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 188.93/27.56 [W928 07:05:54.905205898 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 188.93/27.56 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 188.93/27.56 [W928 07:05:54.905211343 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 188.93/27.56 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 188.93/27.56 [W928 07:05:54.905223688 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 188.93/27.56 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 188.93/27.56 [W928 07:05:54.905238091 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 188.93/27.56 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 188.93/27.56 % (1597342)Refutation not found, incomplete strategy % 188.93/27.56 % (1597342)------------------------------ % 188.93/27.56 % (1597342)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 188.93/27.56 % (1597342)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 188.93/27.56 % (1597342)CaDiCaL version: 2.1.3 % 188.93/27.56 % (1597342)Termination reason: Refutation not found, incomplete strategy % 188.93/27.56 % (1597342)Time elapsed: 0.312 s % 188.93/27.56 % (1597342)Peak memory usage: 126 MB % 188.93/27.56 % (1597342)Instructions burned: 826 (million) % 188.93/27.56 % (1597342)------------------------------ % 188.93/27.56 % (1597342)------------------------------ % 188.93/27.56 % (1597344)dis+1011_1_anc=none:ncem=casc2026/models/loop3.pt:sil=16000:npcc=on:sos=on:lsd=20:urr=full:alpa=true:sac=on:random_seed=4060257559:i=1532:ep=RS:ss=axioms_2771 on theBenchmark for (2771ds/1532Mi) % 188.93/27.56 [W928 07:05:55.522952354 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 188.93/27.56 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 188.93/27.56 [W928 07:05:55.522975061 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 203.10/29.55 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 203.10/29.55 [W928 07:05:55.522995970 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 203.10/29.55 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 203.10/29.55 [W928 07:05:55.523007817 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 203.10/29.55 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 203.10/29.55 [W928 07:05:55.523030363 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 203.10/29.55 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 203.10/29.55 [W928 07:05:55.523035799 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 203.10/29.55 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 203.10/29.55 [W928 07:05:55.523048436 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 203.10/29.55 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 203.10/29.55 [W928 07:05:55.523061140 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 203.10/29.55 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 203.10/29.55 [W928 07:05:55.523074527 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 203.10/29.55 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 203.10/29.55 [W928 07:05:55.523080209 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 203.10/29.55 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 203.10/29.55 [W928 07:05:55.523092807 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 203.10/29.55 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 203.10/29.55 [W928 07:05:55.523098259 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 203.10/29.55 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 203.10/29.55 % (1597344)Refutation not found, incomplete strategy % 203.10/29.55 % (1597344)------------------------------ % 203.10/29.55 % (1597344)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 203.10/29.55 % (1597344)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 203.10/29.55 % (1597344)CaDiCaL version: 2.1.3 % 203.10/29.55 % (1597344)Termination reason: Refutation not found, incomplete strategy % 203.10/29.55 % (1597344)Time elapsed: 0.304 s % 203.10/29.55 % (1597344)Peak memory usage: 126 MB % 203.10/29.55 % (1597344)Instructions burned: 827 (million) % 203.10/29.55 % (1597344)------------------------------ % 203.10/29.55 % (1597344)------------------------------ % 203.10/29.55 % (1597346)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=unary_first:erd=off:flr=on:newcnf=on:random_seed=2465134046:i=1565:sd=2:ss=axioms:sgt=32_2765 on theBenchmark for (2765ds/1565Mi) % 228.68/33.05 % (1597346)Refutation not found, incomplete strategy % 228.68/33.05 % (1597346)------------------------------ % 228.68/33.05 % (1597346)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 228.68/33.05 % (1597346)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 228.68/33.05 % (1597346)CaDiCaL version: 2.1.3 % 228.68/33.05 % (1597346)Termination reason: Refutation not found, incomplete strategy % 228.68/33.05 % (1597346)Time elapsed: 0.352 s % 228.68/33.05 % (1597346)Peak memory usage: 129 MB % 228.68/33.05 % (1597346)Instructions burned: 898 (million) % 228.68/33.05 % (1597346)------------------------------ % 228.68/33.05 % (1597346)------------------------------ % 228.68/33.05 % (1597348)lrs-1011_1_to=lpo:ncem=casc2026/models/loop4.pt:sil=16000:npcc=on:sims=off:bsd=on:sp=unary_first:erd=off:spb=goal:lcm=reverse:gs=on:s2agt=8:random_seed=3717050485:i=1572:fgj=on:gsp=on_2758 on theBenchmark for (2758ds/1572Mi) % 228.68/33.05 % (1597348)Instruction limit reached! % 228.68/33.05 % (1597348)------------------------------ % 228.68/33.05 % (1597348)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 228.68/33.05 % (1597348)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 228.68/33.05 % (1597348)CaDiCaL version: 2.1.3 % 228.68/33.05 % (1597348)Termination reason: Instruction limit % 228.68/33.05 % (1597348)Termination phase: Saturation % 228.68/33.05 % (1597348)Time elapsed: 0.597 s % 228.68/33.05 % (1597348)Peak memory usage: 135 MB % 228.68/33.05 % (1597348)Instructions burned: 1572 (million) % 228.68/33.05 % (1597350)lrs-1002_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:fde=none:sp=occurrence:sos=on:newcnf=on:random_seed=2794459142:i=6052:sd=4:ss=axioms:sgt=24_2751 on theBenchmark for (2751ds/6052Mi) % 228.68/33.05 % (1597330)Instruction limit reached! % 228.68/33.05 % (1597330)------------------------------ % 228.68/33.05 % (1597330)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 228.68/33.05 % (1597330)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 228.68/33.05 % (1597330)CaDiCaL version: 2.1.3 % 228.68/33.05 % (1597330)Termination reason: Instruction limit % 228.68/33.05 % (1597330)Termination phase: Saturation % 228.68/33.05 % (1597330)Time elapsed: 8.372 s % 228.68/33.05 % (1597330)Peak memory usage: 229 MB % 228.68/33.05 % (1597330)Instructions burned: 13495 (million) % 228.68/33.05 % (1597352)lrs+21_1_to=lpo:ncem=casc2026/models/loop2.pt:sil=16000:npcc=on:sp=arity:sos=on:erd=off:lcm=predicate:alpa=false:sac=on:random_seed=2567410042:i=3500:sd=1:bd=preordered:sup=off:ss=included_2738 on theBenchmark for (2738ds/3500Mi) % 228.68/33.05 [W928 07:05:58.030659756 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 228.68/33.05 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 228.68/33.05 [W928 07:05:58.030695083 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 228.68/33.05 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 228.68/33.05 [W928 07:05:58.030731533 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 228.68/33.05 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 228.68/33.05 [W928 07:05:58.030743469 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 228.68/33.05 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 228.68/33.05 [W928 07:05:58.030768126 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 228.68/33.05 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 228.68/33.05 [W928 07:05:58.030780449 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 249.84/36.06 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 249.84/36.06 % (1597350)Instruction limit reached! % 249.84/36.06 % (1597350)------------------------------ % 249.84/36.06 % (1597350)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 249.84/36.06 % (1597350)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 249.84/36.06 % (1597350)CaDiCaL version: 2.1.3 % 249.84/36.06 % (1597350)Termination reason: Instruction limit % 249.84/36.06 % (1597350)Termination phase: Saturation % 249.84/36.06 % (1597350)Time elapsed: 1.881 s % 249.84/36.06 % (1597350)Peak memory usage: 138 MB % 249.84/36.06 % (1597350)Instructions burned: 6055 (million) % 249.84/36.06 % (1597352)Refutation not found, incomplete strategy % 249.84/36.06 % (1597352)------------------------------ % 249.84/36.06 % (1597352)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 249.84/36.06 % (1597352)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 249.84/36.06 % (1597352)CaDiCaL version: 2.1.3 % 249.84/36.06 % (1597352)Termination reason: Refutation not found, incomplete strategy % 249.84/36.06 % (1597352)Time elapsed: 0.553 s % 249.84/36.06 % (1597352)Peak memory usage: 127 MB % 249.84/36.06 % (1597352)Instructions burned: 891 (million) % 249.84/36.06 % (1597354)lrs+35_1_anc=all_dependent:ncem=casc2026/models/all5champsBiggishL14.pt:sil=32000:npcc=on:fde=none:sp=weighted_frequency:erd=off:spb=non_intro:updr=off:newcnf=on:random_seed=4117274821:i=1842:sd=3:fgj=on:gtg=position:gsp=on:ss=axioms:sgt=20_2731 on theBenchmark for (2731ds/1842Mi) % 249.84/36.06 % (1597352)------------------------------ % 249.84/36.06 % (1597352)------------------------------ % 249.84/36.06 % (1597356)lrs+11_1_anc=all_dependent:ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:bsr=unit_only:random_seed=944632410:i=66096:add=on_2729 on theBenchmark for (2729ds/66096Mi) % 249.84/36.06 % (1597354)Refutation not found, incomplete strategy % 249.84/36.06 % (1597354)------------------------------ % 249.84/36.06 % (1597354)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 249.84/36.06 % (1597354)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 249.84/36.06 % (1597354)CaDiCaL version: 2.1.3 % 249.84/36.06 % (1597354)Termination reason: Refutation not found, incomplete strategy % 249.84/36.06 % (1597354)Time elapsed: 0.895 s % 249.84/36.06 % (1597354)Peak memory usage: 134 MB % 249.84/36.06 % (1597354)Instructions burned: 1372 (million) % 249.84/36.06 % (1597354)------------------------------ % 249.84/36.06 % (1597354)------------------------------ % 249.84/36.06 % (1597358)lrs+1011_1_to=lpo:ncem=casc2026/models/loop3.pt:sil=64000:npcc=on:random_seed=44455854:i=1884:sd=1:nm=60:ss=axioms_2718 on theBenchmark for (2718ds/1884Mi) % 249.84/36.06 [W928 07:06:00.020324976 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 249.84/36.06 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 249.84/36.06 [W928 07:06:00.020360249 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 249.84/36.06 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 249.84/36.06 [W928 07:06:00.020398159 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 249.84/36.06 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 249.84/36.06 [W928 07:06:00.020409236 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 249.84/36.06 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 249.84/36.06 [W928 07:06:00.020434493 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 249.84/36.06 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 268.14/38.83 [W928 07:06:00.020445376 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 268.14/38.83 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 268.14/38.83 [W928 07:06:00.020476519 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 268.14/38.83 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 268.14/38.83 [W928 07:06:00.020487443 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 268.14/38.83 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 268.14/38.83 [W928 07:06:00.020516723 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 268.14/38.83 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 268.14/38.83 [W928 07:06:00.020527366 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 268.14/38.83 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 268.14/38.83 [W928 07:06:00.020551266 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 268.14/38.83 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 268.14/38.83 [W928 07:06:00.020573786 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 268.14/38.83 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 268.14/38.83 % (1597358)Refutation not found, incomplete strategy % 268.14/38.83 % (1597358)------------------------------ % 268.14/38.83 % (1597358)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 268.14/38.83 % (1597358)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 268.14/38.83 % (1597358)CaDiCaL version: 2.1.3 % 268.14/38.83 % (1597358)Termination reason: Refutation not found, incomplete strategy % 268.14/38.83 % (1597358)Time elapsed: 0.540 s % 268.14/38.83 % (1597358)Peak memory usage: 125 MB % 268.14/38.83 % (1597358)Instructions burned: 822 (million) % 268.14/38.83 % (1597358)------------------------------ % 268.14/38.83 % (1597358)------------------------------ % 268.14/38.83 % (1597360)lrs-1011_4:1_sil=16000:bsr=on:random_seed=1453334206:cts=off:i=5469:bs=on:fsr=off_2708 on theBenchmark for (2708ds/5469Mi) % 268.14/38.83 % (1597328)Instruction limit reached! % 268.14/38.83 % (1597328)------------------------------ % 268.14/38.83 % (1597328)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 268.14/38.83 % (1597328)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 268.14/38.83 % (1597328)CaDiCaL version: 2.1.3 % 268.14/38.83 % (1597328)Termination reason: Instruction limit % 268.14/38.83 % (1597328)Termination phase: Saturation % 268.14/38.83 % (1597328)Time elapsed: 14.850 s % 268.14/38.83 % (1597328)Peak memory usage: 276 MB % 268.14/38.83 % (1597328)Instructions burned: 26458 (million) % 268.14/38.83 % (1597362)lrs-1010_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=unary_frequency:urr=on:bce=on:alpa=false:sac=on:random_seed=3700918267:i=2037:s2at=10:gtgl=5:add=off:bd=preordered:ins=25:gtg=exists_all_2692 on theBenchmark for (2692ds/2037Mi) % 268.14/38.83 % (1597362)Instruction limit reached! % 268.14/38.83 % (1597362)------------------------------ % 268.14/38.83 % (1597362)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 268.14/38.83 % (1597362)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 268.14/38.83 % (1597362)CaDiCaL version: 2.1.3 % 268.14/38.83 % (1597362)Termination reason: Instruction limit % 274.66/39.64 % (1597362)Termination phase: Saturation % 274.66/39.64 % (1597362)Time elapsed: 1.250 s % 274.66/39.64 % (1597362)Peak memory usage: 139 MB % 274.66/39.64 % (1597362)Instructions burned: 2038 (million) % 274.66/39.64 % (1597360)Instruction limit reached! % 274.66/39.64 % (1597360)------------------------------ % 274.66/39.64 % (1597360)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 274.66/39.64 % (1597360)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 274.66/39.64 % (1597360)CaDiCaL version: 2.1.3 % 274.66/39.64 % (1597360)Termination reason: Instruction limit % 274.66/39.64 % (1597360)Termination phase: Saturation % 274.66/39.64 % (1597360)Time elapsed: 2.945 s % 274.66/39.64 % (1597360)Peak memory usage: 112 MB % 274.66/39.64 % (1597360)Instructions burned: 5469 (million) % 274.66/39.64 % (1597364)lrs-30_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:urr=on:bce=on:rp=on:br=off:flr=on:random_seed=3982166476:st=-1:i=2110:kws=precedence:av=off:ss=axioms:er=known_2677 on theBenchmark for (2677ds/2110Mi) % 274.66/39.64 % (1597365)dis-1010_1_anc=all_dependent:ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:sp=unary_first:spb=goal:lcm=reverse:fd=off:flr=on:random_seed=264829613:i=2430:add=off:aac=none:nm=16_2677 on theBenchmark for (2677ds/2430Mi) % 274.66/39.64 % (1597364)Instruction limit reached! % 274.66/39.64 % (1597364)------------------------------ % 274.66/39.64 % (1597364)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 274.66/39.64 % (1597364)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 274.66/39.64 % (1597364)CaDiCaL version: 2.1.3 % 274.66/39.64 % (1597364)Termination reason: Instruction limit % 274.66/39.64 % (1597364)Termination phase: Saturation % 274.66/39.64 % (1597364)Time elapsed: 1.315 s % 274.66/39.64 % (1597364)Peak memory usage: 135 MB % 274.66/39.64 % (1597364)Instructions burned: 2110 (million) % 274.66/39.64 % (1597368)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=unary_first:spb=units:acc=on:bsr=unit_only:gs=on:sac=on:random_seed=1105577499:cond=fast:i=4891_2662 on theBenchmark for (2662ds/4891Mi) % 274.66/39.64 % (1597365)Instruction limit reached! % 274.66/39.64 % (1597365)------------------------------ % 274.66/39.64 % (1597365)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 274.66/39.64 % (1597365)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 274.66/39.64 % (1597365)CaDiCaL version: 2.1.3 % 274.66/39.64 % (1597365)Termination reason: Instruction limit % 274.66/39.64 % (1597365)Termination phase: Saturation % 274.66/39.64 % (1597365)Time elapsed: 1.569 s % 274.66/39.64 % (1597365)Peak memory usage: 139 MB % 274.66/39.64 % (1597365)Instructions burned: 2430 (million) % 274.66/39.64 % (1597370)lrs+4_1_anc=all:ncem=casc2026/models/loop8.pt:sil=32000:tgt=full:npcc=on:sos=on:spb=goal_then_units:lcm=reverse:gs=on:s2agt=16:sac=on:newcnf=on:random_seed=2619247086:st=2:i=14845:sd=2:ss=included:fsd=on_2659 on theBenchmark for (2659ds/14845Mi) % 274.66/39.64 % (1597337)Instruction limit reached! % 274.66/39.64 % (1597337)------------------------------ % 274.66/39.64 % (1597337)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 274.66/39.64 % (1597337)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 274.66/39.64 % (1597337)CaDiCaL version: 2.1.3 % 274.66/39.64 % (1597337)Termination reason: Instruction limit % 274.66/39.64 % (1597337)Termination phase: Saturation % 274.66/39.64 % (1597337)Time elapsed: 14.777 s % 274.66/39.64 % (1597337)Peak memory usage: 1237 MB % 274.66/39.64 % (1597337)Instructions burned: 26474 (million) % 274.66/39.64 % (1597370)Refutation not found, incomplete strategy % 274.66/39.64 % (1597370)------------------------------ % 274.66/39.64 % (1597370)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 274.66/39.64 % (1597370)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 274.66/39.64 % (1597370)CaDiCaL version: 2.1.3 % 274.66/39.64 % (1597370)Termination reason: Refutation not found, incomplete strategy % 274.66/39.64 % (1597370)Time elapsed: 0.615 s % 274.66/39.64 % (1597370)Peak memory usage: 129 MB % 274.66/39.64 % (1597370)Instructions burned: 906 (million) % 274.66/39.64 % (1597373)lrs-1010_1_to=lpo:ncem=casc2026/models/loop4.pt:sil=32000:npcc=on:urr=ec_only:br=off:random_seed=3115084333:i=7534:sd=3:ins=1:gtg=exists_top:ss=included:sgt=8_2652 on theBenchmark for (2652ds/7534Mi) % 274.66/39.64 % (1597370)------------------------------ % 274.66/39.64 % (1597370)------------------------------ % 274.66/39.64 % (1597375)lrs-1002_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=ground:npcc=on:prc=on:fde=none:sims=off:spb=goal:bsr=unit_only:s2agt=32:random_seed=59703279:cond=fast:i=10353:bs=on:av=off:ss=axioms:fsd=on:sgt=64:fsdmm=10_2649 on theBenchmark for (2649ds/10353Mi) % 288.98/41.73 % (1597373)Refutation not found, incomplete strategy % 288.98/41.73 % (1597373)------------------------------ % 288.98/41.73 % (1597373)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 288.98/41.73 % (1597373)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 288.98/41.73 % (1597373)CaDiCaL version: 2.1.3 % 288.98/41.73 % (1597373)Termination reason: Refutation not found, incomplete strategy % 288.98/41.73 % (1597373)Time elapsed: 0.611 s % 288.98/41.73 % (1597373)Peak memory usage: 128 MB % 288.98/41.73 % (1597373)Instructions burned: 908 (million) % 288.98/41.73 % (1597373)------------------------------ % 288.98/41.73 % (1597373)------------------------------ % 288.98/41.73 % (1597377)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=2447968047:i=7860_2642 on theBenchmark for (2642ds/7860Mi) % 288.98/41.73 % (1597377)Refutation not found, incomplete strategy % 288.98/41.73 % (1597377)------------------------------ % 288.98/41.73 % (1597377)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 288.98/41.73 % (1597377)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 288.98/41.73 % (1597377)CaDiCaL version: 2.1.3 % 288.98/41.73 % (1597377)Termination reason: Refutation not found, incomplete strategy % 288.98/41.73 % (1597377)Time elapsed: 0.006 s % 288.98/41.73 % (1597377)Peak memory usage: 88 MB % 288.98/41.73 % (1597377)Instructions burned: 8 (million) % 288.98/41.73 % (1597377)------------------------------ % 288.98/41.73 % (1597377)------------------------------ % 288.98/41.73 % (1597379)ott+1011_1_anc=all_dependent:to=lpo:ncem=casc2026/models/loop5.pt:sil=8000:npcc=on:fde=unused:spb=goal:lsd=30:lcm=predicate:fd=off:gs=on:sac=on:random_seed=3412957662:i=7896:sd=2:bs=on:ss=included:sgt=20_2638 on theBenchmark for (2638ds/7896Mi) % 288.98/41.73 % (1597336)Instruction limit reached! % 288.98/41.73 % (1597336)------------------------------ % 288.98/41.73 % (1597336)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 288.98/41.73 % (1597336)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 288.98/41.73 % (1597336)CaDiCaL version: 2.1.3 % 288.98/41.73 % (1597336)Termination reason: Instruction limit % 288.98/41.73 % (1597336)Termination phase: Saturation % 288.98/41.73 % (1597336)Time elapsed: 17.180 s % 288.98/41.73 % (1597336)Peak memory usage: 401 MB % 288.98/41.73 % (1597336)Instructions burned: 30755 (million) % 288.98/41.73 % (1597379)Refutation not found, incomplete strategy % 288.98/41.73 % (1597379)------------------------------ % 288.98/41.73 % (1597379)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 288.98/41.73 % (1597379)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 288.98/41.73 % (1597379)CaDiCaL version: 2.1.3 % 288.98/41.73 % (1597379)Termination reason: Refutation not found, incomplete strategy % 288.98/41.73 % (1597379)Time elapsed: 0.650 s % 288.98/41.73 % (1597379)Peak memory usage: 130 MB % 288.98/41.73 % (1597379)Instructions burned: 974 (million) % 288.98/41.73 % (1597381)lrs+10_1_ncem=casc2026/models/loop2.pt:sil=16000:tgt=ground:npcc=on:prc=on:random_seed=2187323946:i=5812:gtgl=2:gtg=all_2629 on theBenchmark for (2629ds/5812Mi) % 288.98/41.73 % (1597379)------------------------------ % 288.98/41.73 % (1597379)------------------------------ % 288.98/41.73 % (1597368)Instruction limit reached! % 288.98/41.73 % (1597368)------------------------------ % 288.98/41.73 % (1597368)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 288.98/41.73 % (1597368)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 288.98/41.73 % (1597368)CaDiCaL version: 2.1.3 % 288.98/41.73 % (1597368)Termination reason: Instruction limit % 288.98/41.73 % (1597368)Termination phase: Saturation % 288.98/41.73 % (1597368)Time elapsed: 3.344 s % 288.98/41.73 % (1597368)Peak memory usage: 153 MB % 288.98/41.73 % (1597368)Instructions burned: 4891 (million) % 288.98/41.73 % (1597383)ott-1011_1_anc=none:ncem=casc2026/models/loop1.pt:sil=16000:npcc=on:prc=on:sp=const_frequency:sos=on:lsd=100:random_seed=4174947936:i=2965:s2at=3.7:aac=none:fgj=on:fdi=2:er=known_2627 on theBenchmark for (2627ds/2965Mi) % 288.98/41.73 % (1597384)lrs-1010_1_ncem=casc2026/models/loop5.pt:sil=16000:npcc=on:sp=reverse_frequency:spb=units:lcm=predicate:urr=on:s2agt=8:updr=off:random_seed=2799516709:i=2967:kws=precedence:bd=preordered:av=off_2627 on theBenchmark for (2627ds/2967Mi) % 288.98/41.73 % (1597383)Refutation not found, iTerminated %------------------------------------------------------------------------------