%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : HEN013-2 : TPTP v9.3.1. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n015.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 10:19:11 AM UTC 2026
% Result : Satisfiable 146.29s 21.85s
% Output : Saturation 146.29s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u720,axiom,
less_equal(identity,zero) ).
cnf(u880,axiom,
less_equal(X0,X1) ).
cnf(u944,axiom,
X0 = X1 ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : HEN013-2 : TPTP v9.3.1. Released v2.5.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.57 % Computer : n015.cluster.edu
% 0.11/0.57 % Model : x86_64 x86_64
% 0.11/0.57 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.57 % Memory : 8046.5625MB
% 0.11/0.57 % OS : Linux 6.8.0-71-generic
% 0.11/0.57 % CPULimit : 300
% 0.11/0.57 % WCLimit : 300
% 0.11/0.57 % DateTime : Sun Sep 27 10:54:46 UTC 2026
% 0.11/0.57 % CPUTime :
% 0.11/0.57 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.60 Running first-order theorem proving
% 0.11/0.60 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
% 7.94/2.15 % (1482185)Input is clausal, will run a generic CNF schedule.
% 7.94/2.15 % (1482278)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=1812747832:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 7.94/2.15 % (1482283)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1820180421:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 7.94/2.15 % (1482276)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=3404005222:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 7.94/2.15 % (1482285)dis-21_1_sil=8000:lcm=predicate:random_seed=2847654739:st=5:avsq=on:i=117:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/117Mi)
% 7.94/2.15 % (1482282)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=2487405910:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 7.94/2.15 % (1482281)lrs+10_1_sil=8000:sp=occurrence:random_seed=477127659:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 7.94/2.15 % (1482279)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=2661157675:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 7.94/2.15 % (1482282)Refutation not found, incomplete strategy
% 7.94/2.15 % (1482282)------------------------------
% 7.94/2.15 % (1482282)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.94/2.15 % (1482285)Refutation not found, incomplete strategy
% 7.94/2.15 % (1482285)------------------------------
% 7.94/2.15 % (1482285)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.94/2.15 % (1482281)Refutation not found, incomplete strategy
% 7.94/2.15 % (1482281)------------------------------
% 7.94/2.15 % (1482281)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.94/2.15 % (1482281)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.94/2.15 % (1482285)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.94/2.15 % (1482282)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.94/2.15 % (1482282)CaDiCaL version: 2.1.3
% 7.94/2.15 % (1482285)CaDiCaL version: 2.1.3
% 7.94/2.15 % (1482281)CaDiCaL version: 2.1.3
% 7.94/2.15 % (1482285)Termination reason: Refutation not found, incomplete strategy
% 7.94/2.15 % (1482285)Time elapsed: 0.001 s
% 7.94/2.15 % (1482281)Termination reason: Refutation not found, incomplete strategy
% 7.94/2.15 % (1482281)Time elapsed: 0.001 s
% 7.94/2.15 % (1482282)Termination reason: Refutation not found, incomplete strategy
% 7.94/2.15 % (1482282)Time elapsed: 0.001 s
% 7.94/2.15 % (1482285)Peak memory usage: 86 MB
% 7.94/2.15 % (1482282)Peak memory usage: 85 MB
% 7.94/2.15 % (1482281)Peak memory usage: 86 MB
% 7.94/2.15 % (1482283)Instruction limit reached!
% 7.94/2.15 % (1482283)------------------------------
% 7.94/2.15 % (1482283)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.94/2.15 % (1482283)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.94/2.15 % (1482283)CaDiCaL version: 2.1.3
% 7.94/2.15 % (1482283)Termination reason: Instruction limit
% 7.94/2.15 % (1482283)Termination phase: Saturation
% 7.94/2.15 % (1482283)Time elapsed: 0.104 s
% 7.94/2.15 % (1482283)Peak memory usage: 89 MB
% 7.94/2.15 % (1482283)Instructions burned: 181 (million)
% 7.94/2.15 % (1482281)------------------------------
% 7.94/2.15 % (1482281)------------------------------
% 7.94/2.15 % (1482285)------------------------------
% 7.94/2.15 % (1482285)------------------------------
% 7.94/2.15 % (1482282)------------------------------
% 7.94/2.15 % (1482282)------------------------------
% 7.94/2.15 % (1482303)dis+1010_3_sil=8000:plsq=on:drc=off:fde=none:plsqc=1:bsd=on:plsqr=7,2:sos=on:spb=goal_then_units:random_seed=1177835497:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi)
% 7.94/2.15 % (1482303)Refutation not found, incomplete strategy
% 7.94/2.15 % (1482303)------------------------------
% 7.94/2.15 % (1482303)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.94/2.15 % (1482303)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.94/2.15 % (1482303)CaDiCaL version: 2.1.3
% 7.94/2.15 % (1482303)Termination reason: Refutation not found, incomplete strategy
% 7.94/2.15 % (1482303)Time elapsed: 0.001 s
% 11.37/2.76 % (1482303)Peak memory usage: 86 MB
% 11.37/2.76 % (1482306)lrs+10_64_to=lpo:sil=8000:random_seed=1930368408:i=126:bd=preordered_2995 on theBenchmark for (2995ds/126Mi)
% 11.37/2.76 % (1482305)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=920772913:st=4:i=219:sd=3:ss=axioms_2995 on theBenchmark for (2995ds/219Mi)
% 11.37/2.76 % (1482304)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=1769671314:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2995 on theBenchmark for (2995ds/189Mi)
% 11.37/2.76 % (1482306)Instruction limit reached!
% 11.37/2.76 % (1482306)------------------------------
% 11.37/2.76 % (1482306)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.37/2.76 % (1482306)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.37/2.76 % (1482306)CaDiCaL version: 2.1.3
% 11.37/2.76 % (1482306)Termination reason: Instruction limit
% 11.37/2.76 % (1482306)Termination phase: Saturation
% 11.37/2.76 % (1482306)Time elapsed: 0.040 s
% 11.37/2.76 % (1482306)Peak memory usage: 88 MB
% 11.37/2.76 % (1482306)Instructions burned: 128 (million)
% 11.37/2.76 % (1482305)Refutation not found, incomplete strategy
% 11.37/2.76 % (1482305)------------------------------
% 11.37/2.76 % (1482305)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.37/2.76 % (1482304)Refutation not found, incomplete strategy
% 11.37/2.76 % (1482304)------------------------------
% 11.37/2.76 % (1482304)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.37/2.76 % (1482305)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.37/2.76 % (1482304)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.37/2.76 % (1482305)CaDiCaL version: 2.1.3
% 11.37/2.76 % (1482305)Termination reason: Refutation not found, incomplete strategy
% 11.37/2.76 % (1482305)Time elapsed: 0.0000 s
% 11.37/2.76 % (1482304)CaDiCaL version: 2.1.3
% 11.37/2.76 % (1482305)Peak memory usage: 86 MB
% 11.37/2.76 % (1482304)Termination reason: Refutation not found, incomplete strategy
% 11.37/2.76 % (1482304)Time elapsed: 0.001 s
% 11.37/2.76 % (1482304)Peak memory usage: 86 MB
% 11.37/2.76 % (1482303)------------------------------
% 11.37/2.76 % (1482303)------------------------------
% 11.37/2.76 % (1482311)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=794021917:avsq=on:i=194:fgj=on:bd=preordered_2994 on theBenchmark for (2994ds/194Mi)
% 11.37/2.76 % (1482311)Instruction limit reached!
% 11.37/2.76 % (1482311)------------------------------
% 11.37/2.76 % (1482311)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.37/2.76 % (1482311)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.37/2.76 % (1482311)CaDiCaL version: 2.1.3
% 11.37/2.76 % (1482311)Termination reason: Instruction limit
% 11.37/2.76 % (1482311)Termination phase: Saturation
% 11.37/2.76 % (1482311)Time elapsed: 0.063 s
% 11.37/2.76 % (1482311)Peak memory usage: 89 MB
% 11.37/2.76 % (1482311)Instructions burned: 197 (million)
% 11.37/2.76 % (1482304)------------------------------
% 11.37/2.76 % (1482304)------------------------------
% 11.37/2.76 % (1482305)------------------------------
% 11.37/2.76 % (1482305)------------------------------
% 11.37/2.76 % (1482312)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=2740403034:i=157:gtg=all_2993 on theBenchmark for (2993ds/157Mi)
% 11.37/2.76 % (1482314)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=62168088:i=3394:sd=4:ss=included:sgt=64_2992 on theBenchmark for (2992ds/3394Mi)
% 11.37/2.76 % (1482312)Instruction limit reached!
% 11.37/2.76 % (1482312)------------------------------
% 11.37/2.76 % (1482312)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.37/2.76 % (1482312)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.37/2.76 % (1482312)CaDiCaL version: 2.1.3
% 11.37/2.76 % (1482312)Termination reason: Instruction limit
% 11.37/2.76 % (1482312)Termination phase: Saturation
% 11.37/2.76 % (1482312)Time elapsed: 0.092 s
% 11.37/2.76 % (1482312)Peak memory usage: 89 MB
% 11.37/2.76 % (1482312)Instructions burned: 158 (million)
% 11.37/2.76 % (1482316)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=4055872899:i=107_2991 on theBenchmark for (2991ds/107Mi)
% 11.37/2.76 % (1482315)lrs+1011_5_to=lpo:sil=8000:tgt=full:plsq=on:prc=on:drc=off:plsqr=31,4:sp=occurrence:urr=on:nwc=0.8:s2agt=16:br=off:random_seed=2601606328:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2991 on theBenchmark for (2991ds/106Mi)
% 17.75/3.64 % (1482315)Refutation not found, incomplete strategy
% 17.75/3.64 % (1482315)------------------------------
% 17.75/3.64 % (1482315)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.75/3.64 % (1482315)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.75/3.64 % (1482315)CaDiCaL version: 2.1.3
% 17.75/3.64 % (1482315)Termination reason: Refutation not found, incomplete strategy
% 17.75/3.64 % (1482315)Time elapsed: 0.001 s
% 17.75/3.64 % (1482315)Peak memory usage: 86 MB
% 17.75/3.64 % (1482316)Refutation not found, incomplete strategy
% 17.75/3.64 % (1482316)------------------------------
% 17.75/3.64 % (1482316)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.75/3.64 % (1482316)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.75/3.64 % (1482316)CaDiCaL version: 2.1.3
% 17.75/3.64 % (1482316)Termination reason: Refutation not found, incomplete strategy
% 17.75/3.64 % (1482316)Time elapsed: 0.001 s
% 17.75/3.64 % (1482316)Peak memory usage: 87 MB
% 17.75/3.64 [W927 10:54:47.905562371 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 17.75/3.64 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 17.75/3.64 [W927 10:54:47.905585784 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 17.75/3.64 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 17.75/3.64 [W927 10:54:47.905607014 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 17.75/3.64 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 17.75/3.64 [W927 10:54:47.905614147 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 17.75/3.64 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 17.75/3.64 [W927 10:54:47.905627854 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 17.75/3.64 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 17.75/3.64 [W927 10:54:47.905634355 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 17.75/3.64 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 17.75/3.64 [W927 10:54:47.905648714 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 17.75/3.64 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 17.75/3.64 [W927 10:54:47.905655008 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 17.75/3.64 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 17.75/3.64 [W927 10:54:47.905668150 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 17.75/3.64 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 17.75/3.64 [W927 10:54:47.905674424 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 17.75/3.64 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 29.33/5.16 [W927 10:54:47.905687329 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 29.33/5.16 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 29.33/5.16 [W927 10:54:47.905694513 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 29.33/5.16 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 29.33/5.16 % (1482319)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=384310443:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2990 on theBenchmark for (2990ds/242Mi)
% 29.33/5.16 % (1482319)Refutation not found, incomplete strategy
% 29.33/5.16 % (1482319)------------------------------
% 29.33/5.16 % (1482319)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.33/5.16 % (1482319)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.33/5.16 % (1482319)CaDiCaL version: 2.1.3
% 29.33/5.16 % (1482319)Termination reason: Refutation not found, incomplete strategy
% 29.33/5.16 % (1482319)Time elapsed: 0.001 s
% 29.33/5.16 % (1482319)Peak memory usage: 86 MB
% 29.33/5.16 % (1482314)Refutation not found, incomplete strategy
% 29.33/5.16 % (1482314)------------------------------
% 29.33/5.16 % (1482314)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.33/5.16 % (1482314)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.33/5.16 % (1482314)CaDiCaL version: 2.1.3
% 29.33/5.16 % (1482314)Termination reason: Refutation not found, incomplete strategy
% 29.33/5.16 % (1482314)Time elapsed: 0.319 s
% 29.33/5.16 % (1482314)Peak memory usage: 125 MB
% 29.33/5.16 % (1482314)Instructions burned: 825 (million)
% 29.33/5.16 % (1482316)------------------------------
% 29.33/5.16 % (1482316)------------------------------
% 29.33/5.16 % (1482315)------------------------------
% 29.33/5.16 % (1482315)------------------------------
% 29.33/5.16 % (1482319)------------------------------
% 29.33/5.16 % (1482319)------------------------------
% 29.33/5.16 % (1482314)------------------------------
% 29.33/5.16 % (1482314)------------------------------
% 29.33/5.16 % (1482323)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=4223791163:cond=fast:i=5208:av=off_2987 on theBenchmark for (2987ds/5208Mi)
% 29.33/5.16 % (1482324)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=2116421616:i=134:sd=2:doe=on:ss=axioms:sgt=14_2987 on theBenchmark for (2987ds/134Mi)
% 29.33/5.16 % (1482324)Refutation not found, incomplete strategy
% 29.33/5.16 % (1482324)------------------------------
% 29.33/5.16 % (1482324)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.33/5.16 % (1482324)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.33/5.16 % (1482324)CaDiCaL version: 2.1.3
% 29.33/5.16 % (1482324)Termination reason: Refutation not found, incomplete strategy
% 29.33/5.16 % (1482324)Time elapsed: 0.001 s
% 29.33/5.16 % (1482324)Peak memory usage: 86 MB
% 29.33/5.16 % (1482328)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=1116365351:i=191:fgj=on:bd=all_2985 on theBenchmark for (2985ds/191Mi)
% 29.33/5.16 % (1482325)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=2403885273:i=499:bd=all_2986 on theBenchmark for (2986ds/499Mi)
% 29.33/5.16 % (1482328)Instruction limit reached!
% 29.33/5.16 % (1482328)------------------------------
% 29.33/5.16 % (1482328)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.33/5.16 % (1482328)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.33/5.16 % (1482328)CaDiCaL version: 2.1.3
% 29.33/5.16 % (1482328)Termination reason: Instruction limit
% 29.33/5.16 % (1482328)Termination phase: Saturation
% 29.33/5.16 % (1482328)Time elapsed: 0.065 s
% 29.33/5.16 % (1482328)Peak memory usage: 91 MB
% 29.33/5.16 % (1482328)Instructions burned: 195 (million)
% 29.33/5.16 % (1482324)------------------------------
% 29.33/5.16 % (1482324)------------------------------
% 29.33/5.16 % (1482331)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=3370644586:i=264:kws=precedence:fsr=off_2984 on theBenchmark for (2984ds/264Mi)
% 31.88/5.55 % (1482331)Instruction limit reached!
% 31.88/5.55 % (1482331)------------------------------
% 31.88/5.55 % (1482331)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.88/5.55 % (1482331)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.88/5.55 % (1482331)CaDiCaL version: 2.1.3
% 31.88/5.55 % (1482331)Termination reason: Instruction limit
% 31.88/5.55 % (1482331)Termination phase: Saturation
% 31.88/5.55 % (1482331)Time elapsed: 0.082 s
% 31.88/5.55 % (1482331)Peak memory usage: 91 MB
% 31.88/5.55 % (1482331)Instructions burned: 264 (million)
% 31.88/5.55 % (1482332)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=3100482683:cond=on:i=156:bs=on:gtg=exists_all:er=known_2983 on theBenchmark for (2983ds/156Mi)
% 31.88/5.55 % (1482325)Instruction limit reached!
% 31.88/5.55 % (1482325)------------------------------
% 31.88/5.55 % (1482325)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.88/5.55 % (1482325)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.88/5.55 % (1482325)CaDiCaL version: 2.1.3
% 31.88/5.55 % (1482325)Termination reason: Instruction limit
% 31.88/5.55 % (1482325)Termination phase: Saturation
% 31.88/5.55 % (1482325)Time elapsed: 0.303 s
% 31.88/5.55 % (1482325)Peak memory usage: 93 MB
% 31.88/5.55 % (1482325)Instructions burned: 500 (million)
% 31.88/5.55 % (1482332)Instruction limit reached!
% 31.88/5.55 % (1482332)------------------------------
% 31.88/5.55 % (1482332)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.88/5.55 % (1482332)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.88/5.55 % (1482332)CaDiCaL version: 2.1.3
% 31.88/5.55 % (1482332)Termination reason: Instruction limit
% 31.88/5.55 % (1482332)Termination phase: Saturation
% 31.88/5.55 % (1482332)Time elapsed: 0.090 s
% 31.88/5.55 % (1482332)Peak memory usage: 89 MB
% 31.88/5.55 % (1482332)Instructions burned: 157 (million)
% 31.88/5.55 % (1482334)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=reverse_frequency:spb=units:lcm=predicate:urr=on:s2agt=8:updr=off:random_seed=762795690:i=3256:kws=precedence:bd=preordered:av=off_2981 on theBenchmark for (2981ds/3256Mi)
% 31.88/5.55 % (1482336)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=2391997603:i=537:av=off:ss=included_2981 on theBenchmark for (2981ds/537Mi)
% 31.88/5.55 % (1482336)Refutation not found, incomplete strategy
% 31.88/5.55 % (1482336)------------------------------
% 31.88/5.55 % (1482336)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.88/5.55 % (1482336)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.88/5.55 % (1482336)CaDiCaL version: 2.1.3
% 31.88/5.55 % (1482336)Termination reason: Refutation not found, incomplete strategy
% 31.88/5.55 % (1482336)Time elapsed: 0.0000 s
% 31.88/5.55 % (1482336)Peak memory usage: 86 MB
% 31.88/5.55 % (1482337)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=2217384533:i=180:bd=preordered:av=off_2980 on theBenchmark for (2980ds/180Mi)
% 31.88/5.55 % (1482337)Instruction limit reached!
% 31.88/5.55 % (1482337)------------------------------
% 31.88/5.55 % (1482337)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.88/5.55 % (1482337)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.88/5.55 % (1482337)CaDiCaL version: 2.1.3
% 31.88/5.55 % (1482337)Termination reason: Instruction limit
% 31.88/5.55 % (1482337)Termination phase: Saturation
% 31.88/5.55 % (1482337)Time elapsed: 0.099 s
% 31.88/5.55 % (1482337)Peak memory usage: 88 MB
% 31.88/5.55 % (1482337)Instructions burned: 182 (million)
% 31.88/5.55 % (1482336)------------------------------
% 31.88/5.55 % (1482336)------------------------------
% 31.88/5.55 % (1482341)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:sas=cadical:sp=reverse_frequency:bsr=on:alpa=false:sac=on:random_seed=1370924368:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2978 on theBenchmark for (2978ds/10307Mi)
% 31.88/5.55 % (1482342)lrs-1010_1024_to=lpo:sil=8000:tgt=ground:plsq=on:plsqc=1:sas=cadical:plsqr=1,32:sp=arity:lma=off:spb=goal:acc=on:bce=on:nwc=1.2:alpa=false:random_seed=1448931439:i=412:gtgl=4:gtg=exists_all_2977 on theBenchmark for (2977ds/412Mi)
% 31.88/5.55 % (1482342)Instruction limit reached!
% 31.88/5.55 % (1482342)------------------------------
% 31.88/5.55 % (1482342)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.88/5.55 % (1482342)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.16/7.38 % (1482342)CaDiCaL version: 2.1.3
% 44.16/7.38 % (1482342)Termination reason: Instruction limit
% 44.16/7.38 % (1482342)Termination phase: Saturation
% 44.16/7.38 % (1482342)Time elapsed: 0.219 s
% 44.16/7.38 % (1482342)Peak memory usage: 91 MB
% 44.16/7.38 % (1482342)Instructions burned: 414 (million)
% 44.16/7.38 % (1482345)ott+1002_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:etr=on:spb=units:urr=on:bsr=unit_only:gs=on:s2agt=16:br=off:random_seed=3634101210:s2pl=no:i=8478:s2at=4:nm=6_2973 on theBenchmark for (2973ds/8478Mi)
% 44.16/7.38 % (1482334)Instruction limit reached!
% 44.16/7.38 % (1482334)------------------------------
% 44.16/7.38 % (1482334)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 44.16/7.38 % (1482334)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.16/7.38 % (1482334)CaDiCaL version: 2.1.3
% 44.16/7.38 % (1482334)Termination reason: Instruction limit
% 44.16/7.38 % (1482334)Termination phase: Saturation
% 44.16/7.38 % (1482334)Time elapsed: 1.034 s
% 44.16/7.38 % (1482334)Peak memory usage: 138 MB
% 44.16/7.38 % (1482334)Instructions burned: 3261 (million)
% 44.16/7.38 % (1482347)ott-1011_2_sil=32000:bsd=on:sp=reverse_frequency:erd=off:urr=on:rnwc=on:gs=on:s2agt=70:updr=off:lftc=20:random_seed=276365795:s2a=on:i=303:s2at=2:sd=1:kws=inv_arity:bs=on:ins=10:fdi=1024:sup=off:ss=included_2970 on theBenchmark for (2970ds/303Mi)
% 44.16/7.38 % (1482347)Refutation not found, incomplete strategy
% 44.16/7.38 % (1482347)------------------------------
% 44.16/7.38 % (1482347)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 44.16/7.38 % (1482347)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.16/7.38 % (1482347)CaDiCaL version: 2.1.3
% 44.16/7.38 % (1482347)Termination reason: Refutation not found, incomplete strategy
% 44.16/7.38 % (1482347)Time elapsed: 0.0000 s
% 44.16/7.38 % (1482347)Peak memory usage: 86 MB
% 44.16/7.38 % (1482347)------------------------------
% 44.16/7.38 % (1482347)------------------------------
% 44.16/7.38 % (1482349)lrs+10_1_to=lpo:sil=16000:fde=none:sos=on:urr=on:bsr=on:random_seed=2037975062:st=4:i=720:sd=3:fsr=off:ss=axioms_2967 on theBenchmark for (2967ds/720Mi)
% 44.16/7.38 % (1482349)Refutation not found, incomplete strategy
% 44.16/7.38 % (1482349)------------------------------
% 44.16/7.38 % (1482349)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 44.16/7.38 % (1482349)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.16/7.38 % (1482349)CaDiCaL version: 2.1.3
% 44.16/7.38 % (1482349)Termination reason: Refutation not found, incomplete strategy
% 44.16/7.38 % (1482349)Time elapsed: 0.0000 s
% 44.16/7.38 % (1482349)Peak memory usage: 86 MB
% 44.16/7.38 % (1482349)------------------------------
% 44.16/7.38 % (1482349)------------------------------
% 44.16/7.38 % (1482351)lrs-20_1_to=lpo:sil=32000:tgt=ground:sp=reverse_frequency:spb=goal:urr=on:bsr=unit_only:nwc=1.5:random_seed=853120685:i=598:bs=on:bd=preordered:av=off:ss=axioms_2964 on theBenchmark for (2964ds/598Mi)
% 44.16/7.38 % (1482351)Refutation not found, incomplete strategy
% 44.16/7.38 % (1482351)------------------------------
% 44.16/7.38 % (1482351)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 44.16/7.38 % (1482351)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.16/7.38 % (1482351)CaDiCaL version: 2.1.3
% 44.16/7.38 % (1482351)Termination reason: Refutation not found, incomplete strategy
% 44.16/7.38 % (1482351)Time elapsed: 0.0000 s
% 44.16/7.38 % (1482351)Peak memory usage: 86 MB
% 44.16/7.38 % (1482351)------------------------------
% 44.16/7.38 % (1482351)------------------------------
% 44.16/7.38 % (1482353)dis-1010_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=occurrence:random_seed=1348401318:i=2989:sd=3:ss=axioms:sgt=60_2962 on theBenchmark for (2962ds/2989Mi)
% 44.16/7.38 [W927 10:54:50.916604199 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 44.16/7.38 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 44.16/7.38 [W927 10:54:50.916655842 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 44.16/7.38 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 46.80/7.79 [W927 10:54:50.916676104 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 46.80/7.79 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 46.80/7.79 [W927 10:54:50.916694824 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 46.80/7.79 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 46.80/7.79 [W927 10:54:50.916707404 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 46.80/7.79 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 46.80/7.79 [W927 10:54:50.916713141 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 46.80/7.79 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 46.80/7.79 [W927 10:54:50.916726185 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 46.80/7.79 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 46.80/7.79 [W927 10:54:50.916731687 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 46.80/7.79 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 46.80/7.79 [W927 10:54:50.916784557 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 46.80/7.79 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 46.80/7.79 [W927 10:54:50.916803620 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 46.80/7.79 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 46.80/7.79 [W927 10:54:50.916827963 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 46.80/7.79 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 46.80/7.79 [W927 10:54:50.916844423 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 46.80/7.79 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 46.80/7.79 % (1482353)Refutation not found, incomplete strategy
% 46.80/7.79 % (1482353)------------------------------
% 46.80/7.79 % (1482353)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 46.80/7.79 % (1482353)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.80/7.79 % (1482353)CaDiCaL version: 2.1.3
% 46.80/7.79 % (1482353)Termination reason: Refutation not found, incomplete strategy
% 46.80/7.79 % (1482353)Time elapsed: 0.311 s
% 46.80/7.79 % (1482353)Peak memory usage: 125 MB
% 46.80/7.79 % (1482353)Instructions burned: 826 (million)
% 46.80/7.79 % (1482353)------------------------------
% 46.80/7.79 % (1482353)------------------------------
% 46.80/7.79 % (1482323)Instruction limit reached!
% 46.80/7.79 % (1482323)------------------------------
% 46.80/7.79 % (1482323)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 46.80/7.79 % (1482323)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.80/7.79 % (1482323)CaDiCaL version: 2.1.3
% 46.80/7.79 % (1482323)Termination reason: Instruction limit
% 52.97/8.61 % (1482323)Termination phase: Saturation
% 52.97/8.61 % (1482323)Time elapsed: 3.110 s
% 52.97/8.61 % (1482323)Peak memory usage: 144 MB
% 52.97/8.61 % (1482323)Instructions burned: 5208 (million)
% 52.97/8.61 % (1482355)dis+1011_1_ncem=casc2026/models/loop5.pt:sil=8000:tgt=full:npcc=on:bsd=on:sp=const_min:spb=goal_then_units:lcm=predicate:urr=ec_only:s2agt=16:random_seed=3293006835:i=1997:bd=preordered:av=off:gtg=all:gsp=on_2955 on theBenchmark for (2955ds/1997Mi)
% 52.97/8.61 % (1482357)lrs-1010_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:drc=off:sp=unary_frequency:urr=ec_only:fd=preordered:random_seed=1564404597:i=2088:bd=preordered:av=off_2954 on theBenchmark for (2954ds/2088Mi)
% 52.97/8.61 % (1482355)Instruction limit reached!
% 52.97/8.61 % (1482355)------------------------------
% 52.97/8.61 % (1482355)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 52.97/8.61 % (1482355)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.97/8.61 % (1482355)CaDiCaL version: 2.1.3
% 52.97/8.61 % (1482355)Termination reason: Instruction limit
% 52.97/8.61 % (1482355)Termination phase: Saturation
% 52.97/8.61 % (1482355)Time elapsed: 0.725 s
% 52.97/8.61 % (1482355)Peak memory usage: 138 MB
% 52.97/8.61 % (1482355)Instructions burned: 1997 (million)
% 52.97/8.61 % (1482359)lrs+1010_64:1_anc=all:to=lpo:sil=16000:fde=none:sp=const_frequency:urr=full:sac=on:random_seed=1499971170:i=1098:nicw=on_2947 on theBenchmark for (2947ds/1098Mi)
% 52.97/8.61 % (1482359)Instruction limit reached!
% 52.97/8.61 % (1482359)------------------------------
% 52.97/8.61 % (1482359)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 52.97/8.61 % (1482359)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.97/8.61 % (1482359)CaDiCaL version: 2.1.3
% 52.97/8.61 % (1482359)Termination reason: Instruction limit
% 52.97/8.61 % (1482359)Termination phase: Saturation
% 52.97/8.61 % (1482359)Time elapsed: 0.350 s
% 52.97/8.61 % (1482359)Peak memory usage: 99 MB
% 52.97/8.61 % (1482359)Instructions burned: 1100 (million)
% 52.97/8.61 % (1482361)lrs-1011_32:1_to=lpo:sil=32000:tgt=ground:sos=on:spb=goal_then_units:acc=on:random_seed=3860672603:i=433:bd=preordered_2942 on theBenchmark for (2942ds/433Mi)
% 52.97/8.61 % (1482361)Refutation not found, incomplete strategy
% 52.97/8.61 % (1482361)------------------------------
% 52.97/8.61 % (1482361)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 52.97/8.61 % (1482361)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.97/8.61 % (1482361)CaDiCaL version: 2.1.3
% 52.97/8.61 % (1482361)Termination reason: Refutation not found, incomplete strategy
% 52.97/8.61 % (1482361)Time elapsed: 0.0000 s
% 52.97/8.61 % (1482361)Peak memory usage: 87 MB
% 52.97/8.61 % (1482357)Instruction limit reached!
% 52.97/8.61 % (1482357)------------------------------
% 52.97/8.61 % (1482357)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 52.97/8.61 % (1482357)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.97/8.61 % (1482357)CaDiCaL version: 2.1.3
% 52.97/8.61 % (1482357)Termination reason: Instruction limit
% 52.97/8.61 % (1482357)Termination phase: Saturation
% 52.97/8.61 % (1482357)Time elapsed: 1.266 s
% 52.97/8.61 % (1482357)Peak memory usage: 133 MB
% 52.97/8.61 % (1482357)Instructions burned: 2096 (million)
% 52.97/8.61 % (1482361)------------------------------
% 52.97/8.61 % (1482361)------------------------------
% 52.97/8.61 % (1482363)lrs+1002_1_ncem=casc2026/models/loop3.pt:sil=32000:npcc=on:prc=on:etr=on:spb=goal:flr=on:random_seed=3776754512:st=5.37:cond=on:i=2942:s2at=20:aac=none:fgj=on:bs=on:gtg=exists_sym:ss=axioms:er=filter:sgt=16_2940 on theBenchmark for (2940ds/2942Mi)
% 52.97/8.61 % (1482364)lrs+35_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=reverse_arity:urr=full:rp=on:br=off:random_seed=3517090200:i=6922:s2at=5:sd=3:bd=all:ss=axioms:er=known:sgt=32_2939 on theBenchmark for (2939ds/6922Mi)
% 52.97/8.61 [W927 10:54:53.140722588 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 52.97/8.61 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 52.97/8.61 [W927 10:54:53.140750168 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 59.62/9.53 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 59.62/9.53 [W927 10:54:53.140773935 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 59.62/9.53 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 59.62/9.53 [W927 10:54:53.140780287 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 59.62/9.53 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 59.62/9.53 [W927 10:54:53.140802248 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 59.62/9.53 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 59.62/9.53 [W927 10:54:53.140807976 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 59.62/9.53 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 59.62/9.53 [W927 10:54:53.140821909 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 59.62/9.53 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 59.62/9.53 [W927 10:54:53.140827857 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 59.62/9.53 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 59.62/9.53 [W927 10:54:53.140840814 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 59.62/9.53 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 59.62/9.53 [W927 10:54:53.140846734 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 59.62/9.53 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 59.62/9.53 [W927 10:54:53.140860019 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 59.62/9.53 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 59.62/9.53 [W927 10:54:53.140865945 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 59.62/9.53 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 59.62/9.53 % (1482364)Refutation not found, incomplete strategy
% 59.62/9.53 % (1482364)------------------------------
% 59.62/9.53 % (1482364)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 59.62/9.53 % (1482364)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.62/9.53 % (1482364)CaDiCaL version: 2.1.3
% 59.62/9.53 % (1482364)Termination reason: Refutation not found, incomplete strategy
% 59.62/9.53 % (1482364)Time elapsed: 0.308 s
% 59.62/9.53 % (1482364)Peak memory usage: 125 MB
% 59.62/9.53 % (1482364)Instructions burned: 822 (million)
% 59.62/9.53 % (1482364)------------------------------
% 59.62/9.53 % (1482364)------------------------------
% 59.62/9.53 % (1482367)dis+10_5:1_sil=8000:tgt=full:plsq=on:plsqc=1:plsqr=32,1:urr=on:fd=off:nwc=0.5:br=off:slsqc=3:slsq=on:random_seed=2544630733:s2a=on:i=596:s2at=2.3:gtgl=5:gtg=all:sup=off_2933 on theBenchmark for (2933ds/596Mi)
% 59.62/9.53 % (1482367)Refutation not found, incomplete strategy
% 60.43/9.73 % (1482367)------------------------------
% 60.43/9.73 % (1482367)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 60.43/9.73 % (1482367)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 60.43/9.73 % (1482367)CaDiCaL version: 2.1.3
% 60.43/9.73 % (1482367)Termination reason: Refutation not found, incomplete strategy
% 60.43/9.73 % (1482367)Time elapsed: 0.001 s
% 60.43/9.73 % (1482367)Peak memory usage: 88 MB
% 60.43/9.73 % (1482367)Instructions burned: 1 (million)
% 60.43/9.73 % (1482363)Refutation not found, incomplete strategy
% 60.43/9.73 % (1482363)------------------------------
% 60.43/9.73 % (1482363)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 60.43/9.73 % (1482363)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 60.43/9.73 % (1482363)CaDiCaL version: 2.1.3
% 60.43/9.73 % (1482363)Termination reason: Refutation not found, incomplete strategy
% 60.43/9.73 % (1482363)Time elapsed: 0.649 s
% 60.43/9.73 % (1482363)Peak memory usage: 129 MB
% 60.43/9.73 % (1482363)Instructions burned: 967 (million)
% 60.43/9.73 % (1482367)------------------------------
% 60.43/9.73 % (1482367)------------------------------
% 60.43/9.73 % (1482363)------------------------------
% 60.43/9.73 % (1482363)------------------------------
% 60.43/9.73 % (1482369)lrs+21_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=non_intro:urr=on:fd=preordered:random_seed=2461053088:i=4123:kws=inv_frequency:bd=preordered:av=off:er=known_2930 on theBenchmark for (2930ds/4123Mi)
% 60.43/9.73 % (1482345)Instruction limit reached!
% 60.43/9.73 % (1482345)------------------------------
% 60.43/9.73 % (1482345)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 60.43/9.73 % (1482345)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 60.43/9.73 % (1482345)CaDiCaL version: 2.1.3
% 60.43/9.73 % (1482345)Termination reason: Instruction limit
% 60.43/9.73 % (1482345)Termination phase: Saturation
% 60.43/9.73 % (1482345)Time elapsed: 4.364 s
% 60.43/9.73 % (1482345)Peak memory usage: 159 MB
% 60.43/9.73 % (1482345)Instructions burned: 8479 (million)
% 60.43/9.73 % (1482371)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=1446647967:i=16411:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2929 on theBenchmark for (2929ds/16411Mi)
% 60.43/9.73 % (1482372)lrs+0_1_ncem=casc2026/models/loop1.pt:sil=8000:tgt=full:npcc=on:sp=reverse_frequency:gs=on:random_seed=209912625:i=1670:kws=inv_precedence:bd=all:av=off:gtg=exists_all_2928 on theBenchmark for (2928ds/1670Mi)
% 60.43/9.73 [W927 10:54:54.362079709 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 60.43/9.73 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 60.43/9.73 [W927 10:54:54.362111875 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 60.43/9.73 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 60.43/9.73 [W927 10:54:54.362150612 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 60.43/9.73 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 60.43/9.73 [W927 10:54:54.362164312 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 60.43/9.73 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 60.43/9.73 [W927 10:54:54.362192409 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 60.43/9.73 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 60.43/9.73 [W927 10:54:54.362204553 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 60.43/9.74 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 60.43/9.74 [W927 10:54:54.362230723 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 60.43/9.74 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 60.43/9.74 [W927 10:54:54.362241603 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 60.43/9.74 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 60.43/9.74 [W927 10:54:54.362265013 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 60.43/9.74 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 60.43/9.74 [W927 10:54:54.362275613 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 60.43/9.74 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 60.43/9.74 [W927 10:54:54.362298727 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 60.43/9.74 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 60.43/9.74 [W927 10:54:54.362362307 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 60.43/9.74 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 60.43/9.74 % (1482371)Refutation not found, incomplete strategy
% 60.43/9.74 % (1482371)------------------------------
% 60.43/9.74 % (1482371)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 60.43/9.74 % (1482371)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 60.43/9.74 % (1482371)CaDiCaL version: 2.1.3
% 60.43/9.74 % (1482371)Termination reason: Refutation not found, incomplete strategy
% 60.43/9.74 % (1482371)Time elapsed: 0.540 s
% 60.43/9.74 % (1482371)Peak memory usage: 125 MB
% 60.43/9.74 % (1482371)Instructions burned: 825 (million)
% 60.43/9.74 % (1482371)------------------------------
% 60.43/9.74 % (1482371)------------------------------
% 60.43/9.74 % (1482375)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:prc=on:drc=off:fde=unused:sp=reverse_frequency:updr=off:random_seed=4199064644:st=3:cond=fast:i=1722:sd=2:ss=included:fsd=on_2920 on theBenchmark for (2920ds/1722Mi)
% 60.43/9.74 % (1482372)Instruction limit reached!
% 60.43/9.74 % (1482372)------------------------------
% 60.43/9.74 % (1482372)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 60.43/9.74 % (1482372)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 60.43/9.74 % (1482372)CaDiCaL version: 2.1.3
% 60.43/9.74 % (1482372)Termination reason: Instruction limit
% 60.43/9.74 % (1482372)Termination phase: Saturation
% 60.43/9.74 % (1482372)Time elapsed: 1.026 s
% 60.43/9.74 % (1482372)Peak memory usage: 130 MB
% 60.43/9.74 % (1482372)Instructions burned: 1672 (million)
% 60.43/9.74 % (1482369)Instruction limit reached!
% 60.43/9.74 % (1482369)------------------------------
% 60.43/9.74 % (1482369)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 60.43/9.74 % (1482369)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 60.43/9.74 % (1482369)CaDiCaL version: 2.1.3
% 60.43/9.74 % (1482369)Termination reason: Instruction limit
% 60.43/9.74 % (1482369)Termination phase: Saturation
% 60.43/9.74 % (1482369)Time elapsed: 1.335 s
% 60.43/9.74 % (1482369)Peak memory usage: 147 MB
% 60.43/9.74 % (1482369)Instructions burned: 4123 (million)
% 60.43/9.74 % (1482377)ott-1004_1_anc=all_dependent:to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:tgt=full:npcc=on:sas=cadical:sp=const_frequency:acc=on:urr=ec_only:gs=on:s2agt=40:alpa=false:sac=on:random_seed=74951456:cts=off:cond=on:i=9530:bs=on:fsd=on_2916 on theBenchmark for (2916ds/9530Mi)
% 75.46/11.73 % (1482378)lrs+10_1_ncem=casc2026/models/loop4.pt:sil=64000:npcc=on:sp=occurrence:random_seed=3652077616:st=2:i=4495:sd=10:ss=included_2916 on theBenchmark for (2916ds/4495Mi)
% 75.46/11.73 [W927 10:54:55.318088920 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 75.46/11.73 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 75.46/11.73 [W927 10:54:55.318122680 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 75.46/11.73 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 75.46/11.73 [W927 10:54:55.318161400 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 75.46/11.73 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 75.46/11.73 [W927 10:54:55.318174181 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 75.46/11.73 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 75.46/11.73 [W927 10:54:55.318200574 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 75.46/11.73 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 75.46/11.73 [W927 10:54:55.318212684 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 75.46/11.73 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 75.46/11.73 [W927 10:54:55.318239471 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 75.46/11.73 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 75.46/11.73 [W927 10:54:55.318250338 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 75.46/11.73 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 75.46/11.73 [W927 10:54:55.318275775 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 75.46/11.73 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 75.46/11.73 [W927 10:54:55.318300061 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 75.46/11.73 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 75.46/11.73 [W927 10:54:55.318325872 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 75.46/11.73 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 75.46/11.73 [W927 10:54:55.318336572 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 75.46/11.73 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 75.46/11.73 % (1482375)Refutation not found, incomplete strategy
% 76.72/11.98 % (1482375)------------------------------
% 76.72/11.98 % (1482375)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 76.72/11.98 % (1482375)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 76.72/11.98 % (1482375)CaDiCaL version: 2.1.3
% 76.72/11.98 % (1482375)Termination reason: Refutation not found, incomplete strategy
% 76.72/11.98 % (1482375)Time elapsed: 0.553 s
% 76.72/11.98 % (1482375)Peak memory usage: 125 MB
% 76.72/11.98 % (1482375)Instructions burned: 825 (million)
% 76.72/11.98 [W927 10:54:55.492944325 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 76.72/11.98 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 76.72/11.98 [W927 10:54:55.492977085 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 76.72/11.98 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 76.72/11.98 [W927 10:54:55.492998204 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 76.72/11.98 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 76.72/11.98 [W927 10:54:55.493011606 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 76.72/11.98 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 76.72/11.98 [W927 10:54:55.493026483 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 76.72/11.98 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 76.72/11.98 [W927 10:54:55.493032500 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 76.72/11.98 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 76.72/11.98 [W927 10:54:55.493047545 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 76.72/11.98 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 76.72/11.98 [W927 10:54:55.493054306 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 76.72/11.98 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 76.72/11.98 [W927 10:54:55.493067575 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 76.72/11.98 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 76.72/11.98 [W927 10:54:55.493074132 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 76.72/11.98 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 76.72/11.98 [W927 10:54:55.493087296 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 76.72/11.98 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 76.72/11.98 [W927 10:54:55.493093829 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 79.38/12.22 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 79.38/12.22 % (1482341)Instruction limit reached!
% 79.38/12.22 % (1482341)------------------------------
% 79.38/12.22 % (1482341)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 79.38/12.22 % (1482341)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 79.38/12.22 % (1482341)CaDiCaL version: 2.1.3
% 79.38/12.22 % (1482341)Termination reason: Instruction limit
% 79.38/12.22 % (1482341)Termination phase: Saturation
% 79.38/12.22 % (1482341)Time elapsed: 6.451 s
% 79.38/12.22 % (1482341)Peak memory usage: 188 MB
% 79.38/12.22 % (1482341)Instructions burned: 10308 (million)
% 79.38/12.22 % (1482378)Refutation not found, incomplete strategy
% 79.38/12.22 % (1482378)------------------------------
% 79.38/12.22 % (1482378)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 79.38/12.22 % (1482378)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 79.38/12.22 % (1482378)CaDiCaL version: 2.1.3
% 79.38/12.22 % (1482378)Termination reason: Refutation not found, incomplete strategy
% 79.38/12.22 % (1482378)Time elapsed: 0.301 s
% 79.38/12.22 % (1482378)Peak memory usage: 125 MB
% 79.38/12.22 % (1482378)Instructions burned: 825 (million)
% 79.38/12.22 % (1482375)------------------------------
% 79.38/12.22 % (1482375)------------------------------
% 79.38/12.22 % (1482378)------------------------------
% 79.38/12.22 % (1482378)------------------------------
% 79.38/12.22 % (1482381)lrs+1002_1_sfv=off:ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=reverse_arity:spb=non_intro:s2agt=16:random_seed=2569269306:cond=fast:i=4920:s2at=1.9:kws=inv_frequency:av=off:er=filter_2912 on theBenchmark for (2912ds/4920Mi)
% 79.38/12.22 % (1482382)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:lcm=reverse:bce=on:bsr=unit_only:random_seed=185456385:cts=off:cond=on:i=2083:s2at=-1:fgj=on:av=off_2910 on theBenchmark for (2910ds/2083Mi)
% 79.38/12.22 % (1482384)lrs+31_1_to=lpo:ncem=casc2026/models/loop2.pt:sil=16000:npcc=on:sp=weighted_frequency:sos=all:spb=units:lcm=predicate:bsr=on:gs=on:random_seed=1449675719:i=4629:av=off:gsp=on_2910 on theBenchmark for (2910ds/4629Mi)
% 79.38/12.22 % (1482384)Refutation not found, incomplete strategy
% 79.38/12.22 % (1482384)------------------------------
% 79.38/12.22 % (1482384)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 79.38/12.22 % (1482384)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 79.38/12.22 % (1482384)CaDiCaL version: 2.1.3
% 79.38/12.22 % (1482384)Termination reason: Refutation not found, incomplete strategy
% 79.38/12.22 % (1482384)Time elapsed: 0.550 s
% 79.38/12.22 % (1482384)Peak memory usage: 126 MB
% 79.38/12.22 % (1482384)Instructions burned: 827 (million)
% 79.38/12.22 % (1482384)------------------------------
% 79.38/12.22 % (1482384)------------------------------
% 79.38/12.22 % (1482387)dis+10_64_sil=16000:tgt=full:plsq=on:prc=on:drc=off:plsqc=2:plsqr=32,1:spb=goal:random_seed=80466017:i=1258:av=off_2900 on theBenchmark for (2900ds/1258Mi)
% 79.38/12.22 % (1482382)Instruction limit reached!
% 79.38/12.22 % (1482382)------------------------------
% 79.38/12.22 % (1482382)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 79.38/12.22 % (1482382)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 79.38/12.22 % (1482382)CaDiCaL version: 2.1.3
% 79.38/12.22 % (1482382)Termination reason: Instruction limit
% 79.38/12.22 % (1482382)Termination phase: Saturation
% 79.38/12.22 % (1482382)Time elapsed: 1.259 s
% 79.38/12.22 % (1482382)Peak memory usage: 134 MB
% 79.38/12.22 % (1482382)Instructions burned: 2083 (million)
% 79.38/12.22 % (1482381)Instruction limit reached!
% 79.38/12.22 % (1482381)------------------------------
% 79.38/12.22 % (1482381)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 79.38/12.22 % (1482381)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 79.38/12.22 % (1482381)CaDiCaL version: 2.1.3
% 79.38/12.22 % (1482381)Termination reason: Instruction limit
% 79.38/12.22 % (1482381)Termination phase: Saturation
% 79.38/12.22 % (1482381)Time elapsed: 1.595 s
% 79.38/12.22 % (1482381)Peak memory usage: 141 MB
% 79.38/12.22 % (1482381)Instructions burned: 4922 (million)
% 79.38/12.22 % (1482389)ott+1_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:fdtod=off:random_seed=2570457604:i=7343:av=off:ss=included_2896 on theBenchmark for (2896ds/7343Mi)
% 79.38/12.22 % (1482391)lrs-1002_1_to=lpo:sil=16000:sp=reverse_arity:sos=on:random_seed=3390031928:i=1325:sd=2:ss=axioms:sgt=16_2894 on theBenchmark for (2894ds/1325Mi)
% 80.09/12.38 % (1482391)Refutation not found, incomplete strategy
% 80.09/12.38 % (1482391)------------------------------
% 80.09/12.38 % (1482391)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 80.09/12.38 % (1482391)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 80.09/12.38 % (1482391)CaDiCaL version: 2.1.3
% 80.09/12.38 % (1482391)Termination reason: Refutation not found, incomplete strategy
% 80.09/12.38 % (1482391)Time elapsed: 0.0000 s
% 80.09/12.38 % (1482391)Peak memory usage: 86 MB
% 80.09/12.38 % (1482387)Instruction limit reached!
% 80.09/12.38 % (1482387)------------------------------
% 80.09/12.38 % (1482387)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 80.09/12.38 % (1482387)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 80.09/12.38 % (1482387)CaDiCaL version: 2.1.3
% 80.09/12.38 % (1482387)Termination reason: Instruction limit
% 80.09/12.38 % (1482387)Termination phase: Saturation
% 80.09/12.38 % (1482387)Time elapsed: 0.716 s
% 80.09/12.38 % (1482387)Peak memory usage: 92 MB
% 80.09/12.38 % (1482387)Instructions burned: 1259 (million)
% 80.09/12.38 % (1482391)------------------------------
% 80.09/12.38 % (1482391)------------------------------
% 80.09/12.38 [W927 10:54:57.731675530 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 80.09/12.38 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 80.09/12.38 [W927 10:54:57.731731487 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 80.09/12.38 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 80.09/12.38 [W927 10:54:57.731769000 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 80.09/12.38 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 80.09/12.38 [W927 10:54:57.731786827 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 80.09/12.38 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 80.09/12.38 [W927 10:54:57.731812154 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 80.09/12.38 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 80.09/12.38 [W927 10:54:57.731823964 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 80.09/12.38 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 80.09/12.38 [W927 10:54:57.731849611 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 80.09/12.38 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 80.09/12.38 [W927 10:54:57.731861488 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 80.09/12.38 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 80.09/12.38 [W927 10:54:57.731887271 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 80.09/12.38 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 80.09/12.38 [W927 10:54:57.731899138 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 90.89/13.90 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 90.89/13.90 [W927 10:54:57.731924602 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 90.89/13.90 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 90.89/13.90 [W927 10:54:57.731935378 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 90.89/13.90 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 90.89/13.90 % (1482393)dis+1011_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:prc=on:sp=arity:lma=off:spb=intro:urr=ec_only:sac=on:random_seed=3580007441:st=3.9:cond=fast:i=2646:s2at=1.8:sd=5:amm=off:gtg=position:ss=axioms:fsd=on_2892 on theBenchmark for (2892ds/2646Mi)
% 90.89/13.90 % (1482394)dis-1003_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:sp=arity:sos=on:urr=on:random_seed=1468042291:i=1489:sd=2:ep=R:ss=axioms_2891 on theBenchmark for (2891ds/1489Mi)
% 90.89/13.90 % (1482389)Refutation not found, incomplete strategy
% 90.89/13.90 % (1482389)------------------------------
% 90.89/13.90 % (1482389)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 90.89/13.90 % (1482389)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 90.89/13.90 % (1482389)CaDiCaL version: 2.1.3
% 90.89/13.90 % (1482389)Termination reason: Refutation not found, incomplete strategy
% 90.89/13.90 % (1482389)Time elapsed: 0.553 s
% 90.89/13.90 % (1482389)Peak memory usage: 125 MB
% 90.89/13.90 % (1482389)Instructions burned: 822 (million)
% 90.89/13.90 [W927 10:54:57.981515365 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 90.89/13.90 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 90.89/13.90 [W927 10:54:57.981537170 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 90.89/13.90 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 90.89/13.90 [W927 10:54:57.981558565 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 90.89/13.90 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 90.89/13.90 [W927 10:54:57.981567216 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 90.89/13.90 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 90.89/13.90 [W927 10:54:57.981580482 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 90.89/13.90 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 90.89/13.90 [W927 10:54:57.981586917 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 90.89/13.90 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 90.89/13.90 [W927 10:54:57.981600292 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 90.89/13.90 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 90.89/13.90 [W927 10:54:57.981606551 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 94.89/14.48 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 94.89/14.48 [W927 10:54:57.981619407 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 94.89/14.48 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 94.89/14.48 [W927 10:54:57.981626523 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 94.89/14.48 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 94.89/14.48 [W927 10:54:57.981639258 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 94.89/14.48 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 94.89/14.48 [W927 10:54:57.981644931 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 94.89/14.48 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 94.89/14.48 % (1482394)Refutation not found, incomplete strategy
% 94.89/14.48 % (1482394)------------------------------
% 94.89/14.48 % (1482394)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 94.89/14.48 % (1482394)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 94.89/14.48 % (1482394)CaDiCaL version: 2.1.3
% 94.89/14.48 % (1482394)Termination reason: Refutation not found, incomplete strategy
% 94.89/14.48 % (1482394)Time elapsed: 0.298 s
% 94.89/14.48 % (1482394)Peak memory usage: 125 MB
% 94.89/14.48 % (1482394)Instructions burned: 821 (million)
% 94.89/14.48 [W927 10:54:58.132796544 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 94.89/14.48 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 94.89/14.48 [W927 10:54:58.132851281 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 94.89/14.48 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 94.89/14.48 [W927 10:54:58.132888861 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 94.89/14.48 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 94.89/14.48 [W927 10:54:58.132906251 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 94.89/14.48 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 94.89/14.48 [W927 10:54:58.132932188 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 94.89/14.48 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 94.89/14.48 [W927 10:54:58.132944285 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 94.89/14.48 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 94.89/14.48 [W927 10:54:58.132971152 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 97.92/15.03 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 97.92/15.03 [W927 10:54:58.132983092 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 97.92/15.03 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 97.92/15.03 [W927 10:54:58.133027149 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 97.92/15.03 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 97.92/15.03 [W927 10:54:58.133048939 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 97.92/15.03 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 97.92/15.03 [W927 10:54:58.133075619 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 97.92/15.03 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 97.92/15.03 [W927 10:54:58.133086476 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 97.92/15.03 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 97.92/15.03 % (1482389)------------------------------
% 97.92/15.03 % (1482389)------------------------------
% 97.92/15.03 % (1482394)------------------------------
% 97.92/15.03 % (1482394)------------------------------
% 97.92/15.03 % (1482393)Refutation not found, incomplete strategy
% 97.92/15.03 % (1482393)------------------------------
% 97.92/15.03 % (1482393)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 97.92/15.03 % (1482393)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 97.92/15.03 % (1482393)CaDiCaL version: 2.1.3
% 97.92/15.03 % (1482393)Termination reason: Refutation not found, incomplete strategy
% 97.92/15.03 % (1482393)Time elapsed: 0.551 s
% 97.92/15.03 % (1482393)Peak memory usage: 125 MB
% 97.92/15.03 % (1482393)Instructions burned: 825 (million)
% 97.92/15.03 % (1482397)lrs+20_1_ncem=casc2026/models/loop3.pt:sil=32000:npcc=on:fde=unused:sp=occurrence:sos=on:lcm=predicate:urr=full:sac=on:random_seed=3976150457:i=1503_2886 on theBenchmark for (2886ds/1503Mi)
% 97.92/15.03 % (1482398)lrs+10_1_ncem=casc2026/models/loop3.pt:sil=16000:tgt=ground:npcc=on:random_seed=4255765449:i=13942:kws=frequency_2885 on theBenchmark for (2885ds/13942Mi)
% 97.92/15.03 % (1482393)------------------------------
% 97.92/15.03 % (1482393)------------------------------
% 97.92/15.03 % (1482401)lrs-1002_1_to=lpo:ncem=casc2026/models/loop4.pt:sil=16000:npcc=on:bsd=on:sp=unary_frequency:spb=goal:lcm=predicate:acc=on:urr=full:bce=on:bsr=unit_only:s2agt=64:sac=on:random_seed=4220670541:i=3604:fsr=off:er=filter_2882 on theBenchmark for (2882ds/3604Mi)
% 97.92/15.03 % (1482397)Refutation not found, incomplete strategy
% 97.92/15.03 % (1482397)------------------------------
% 97.92/15.03 % (1482397)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 97.92/15.03 % (1482397)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 97.92/15.03 % (1482397)CaDiCaL version: 2.1.3
% 97.92/15.03 % (1482397)Termination reason: Refutation not found, incomplete strategy
% 97.92/15.03 % (1482397)Time elapsed: 0.552 s
% 97.92/15.03 % (1482397)Peak memory usage: 127 MB
% 97.92/15.03 % (1482397)Instructions burned: 828 (million)
% 97.92/15.03 % (1482397)------------------------------
% 97.92/15.03 % (1482397)------------------------------
% 97.92/15.03 % (1482447)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=32000:npcc=on:random_seed=65731174:i=1876:sd=1:ss=included:sgt=32_2876 on theBenchmark for (2876ds/1876Mi)
% 97.92/15.03 [W927 10:54:59.657577406 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 97.92/15.03 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 102.71/15.79 [W927 10:54:59.657611009 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 102.71/15.79 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 102.71/15.79 [W927 10:54:59.657649016 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 102.71/15.79 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 102.71/15.79 [W927 10:54:59.657660820 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 102.71/15.79 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 102.71/15.79 [W927 10:54:59.657685337 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 102.71/15.79 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 102.71/15.79 [W927 10:54:59.657696297 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 102.71/15.79 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 102.71/15.79 [W927 10:54:59.657721007 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 102.71/15.79 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 102.71/15.79 [W927 10:54:59.657731717 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 102.71/15.79 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 102.71/15.79 [W927 10:54:59.657755640 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 102.71/15.79 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 102.71/15.79 [W927 10:54:59.657766724 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 102.71/15.79 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 102.71/15.79 [W927 10:54:59.657791361 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 102.71/15.79 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 102.71/15.79 [W927 10:54:59.657802214 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 102.71/15.79 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 102.71/15.79 % (1482447)Refutation not found, incomplete strategy
% 102.71/15.79 % (1482447)------------------------------
% 102.71/15.79 % (1482447)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 102.71/15.79 % (1482447)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 102.71/15.79 % (1482447)CaDiCaL version: 2.1.3
% 102.71/15.79 % (1482447)Termination reason: Refutation not found, incomplete strategy
% 102.71/15.79 % (1482447)Time elapsed: 0.544 s
% 102.71/15.79 % (1482447)Peak memory usage: 125 MB
% 102.71/15.79 % (1482447)Instructions burned: 825 (million)
% 102.71/15.79 % (1482447)------------------------------
% 102.71/15.79 % (1482447)------------------------------
% 102.71/15.79 % (1482543)lrs+10_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:fde=none:sp=arity:urr=on:br=off:random_seed=3482183836:i=1932:bd=preordered:ins=10:sup=off:ss=axioms_2867 on theBenchmark for (2867ds/1932Mi)
% 117.56/17.64 [W927 10:55:00.609602161 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 117.56/17.64 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 117.56/17.64 [W927 10:55:00.609646421 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 117.56/17.64 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 117.56/17.64 [W927 10:55:00.609683411 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 117.56/17.64 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 117.56/17.64 [W927 10:55:00.609695391 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 117.56/17.64 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 117.56/17.64 [W927 10:55:00.609721761 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 117.56/17.64 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 117.56/17.64 [W927 10:55:00.609733875 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 117.56/17.64 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 117.56/17.64 [W927 10:55:00.609760185 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 117.56/17.64 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 117.56/17.64 [W927 10:55:00.609772272 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 117.56/17.64 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 117.56/17.64 [W927 10:55:00.609797539 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 117.56/17.64 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 117.56/17.64 [W927 10:55:00.609809535 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 117.56/17.64 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 117.56/17.64 [W927 10:55:00.609835152 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 117.56/17.64 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 117.56/17.64 [W927 10:55:00.609847129 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 117.56/17.64 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 117.56/17.64 % (1482543)Refutation not found, incomplete strategy
% 117.56/17.64 % (1482543)------------------------------
% 117.56/17.64 % (1482543)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 131.87/19.64 % (1482543)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 131.87/19.64 % (1482543)CaDiCaL version: 2.1.3
% 131.87/19.64 % (1482543)Termination reason: Refutation not found, incomplete strategy
% 131.87/19.64 % (1482543)Time elapsed: 0.547 s
% 131.87/19.64 % (1482543)Peak memory usage: 125 MB
% 131.87/19.64 % (1482543)Instructions burned: 825 (million)
% 131.87/19.64 % (1482401)Instruction limit reached!
% 131.87/19.64 % (1482401)------------------------------
% 131.87/19.64 % (1482401)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 131.87/19.64 % (1482401)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 131.87/19.64 % (1482401)CaDiCaL version: 2.1.3
% 131.87/19.64 % (1482401)Termination reason: Instruction limit
% 131.87/19.64 % (1482401)Termination phase: Saturation
% 131.87/19.64 % (1482401)Time elapsed: 2.093 s
% 131.87/19.64 % (1482401)Peak memory usage: 138 MB
% 131.87/19.64 % (1482401)Instructions burned: 3606 (million)
% 131.87/19.64 % (1482604)dis-1010_1_ncem=casc2026/models/loop1.pt:sil=8000:npcc=on:fde=unused:etr=on:sp=weighted_frequency:spb=goal_then_units:urr=ec_only:fd=preordered:kmz=on:random_seed=1989184745:s2pl=on:cond=fast:i=1980:s2at=2:kws=inv_precedence:doe=on:ins=1:av=off:gsp=on_2859 on theBenchmark for (2859ds/1980Mi)
% 131.87/19.64 % (1482377)Instruction limit reached!
% 131.87/19.64 % (1482377)------------------------------
% 131.87/19.64 % (1482377)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 131.87/19.64 % (1482377)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 131.87/19.64 % (1482377)CaDiCaL version: 2.1.3
% 131.87/19.64 % (1482377)Termination reason: Instruction limit
% 131.87/19.64 % (1482377)Termination phase: Saturation
% 131.87/19.64 % (1482377)Time elapsed: 5.713 s
% 131.87/19.64 % (1482377)Peak memory usage: 170 MB
% 131.87/19.64 % (1482377)Instructions burned: 9530 (million)
% 131.87/19.64 % (1482543)------------------------------
% 131.87/19.64 % (1482543)------------------------------
% 131.87/19.64 % (1482638)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=unary_first:sos=all:spb=units:urr=on:br=off:random_seed=1732399404:i=3902:kws=inv_arity_squared:fgj=on:ss=axioms:sgt=11_2857 on theBenchmark for (2857ds/3902Mi)
% 131.87/19.64 % (1482643)dis+10_32_sil=16000:tgt=ground:drc=off:sas=cadical:acc=on:alpa=false:avsqc=3:random_seed=988795775:avsq=on:i=3916:aac=none:amm=off_2857 on theBenchmark for (2857ds/3916Mi)
% 131.87/19.64 [W927 10:55:01.545662135 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 131.87/19.64 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 131.87/19.64 [W927 10:55:01.545699502 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 131.87/19.64 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 131.87/19.64 [W927 10:55:01.545737106 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 131.87/19.64 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 131.87/19.64 [W927 10:55:01.545749706 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 131.87/19.64 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 131.87/19.64 [W927 10:55:01.545774896 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 131.87/19.64 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 131.87/19.64 [W927 10:55:01.545787026 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 131.87/19.64 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 101.19/21.65 [W927 10:55:01.545812126 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 101.19/21.65 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 101.19/21.65 [W927 10:55:01.545822506 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 101.19/21.65 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 101.19/21.65 [W927 10:55:01.545846533 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 101.19/21.65 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 101.19/21.65 [W927 10:55:01.545856653 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 101.19/21.65 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 101.19/21.65 [W927 10:55:01.545879843 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 101.19/21.65 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 101.19/21.65 [W927 10:55:01.545889923 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 101.19/21.65 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 101.19/21.65 % (1482638)Refutation not found, incomplete strategy
% 101.19/21.65 % (1482638)------------------------------
% 101.19/21.65 % (1482638)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 101.19/21.65 % (1482638)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 101.19/21.65 % (1482638)CaDiCaL version: 2.1.3
% 101.19/21.65 % (1482638)Termination reason: Refutation not found, incomplete strategy
% 101.19/21.65 % (1482638)Time elapsed: 0.547 s
% 101.19/21.65 % (1482638)Peak memory usage: 125 MB
% 101.19/21.65 % (1482638)Instructions burned: 825 (million)
% 101.19/21.65 % (1482638)------------------------------
% 101.19/21.65 % (1482638)------------------------------
% 101.19/21.65 % (1482673)dis+10_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=full:npcc=on:drc=ordering:lcm=predicate:random_seed=3987916767:cond=on:i=3940:av=off:er=known_2848 on theBenchmark for (2848ds/3940Mi)
% 101.19/21.65 % (1482604)Instruction limit reached!
% 101.19/21.65 % (1482604)------------------------------
% 101.19/21.65 % (1482604)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 101.19/21.65 % (1482604)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 101.19/21.65 % (1482604)CaDiCaL version: 2.1.3
% 101.19/21.65 % (1482604)Termination reason: Instruction limit
% 101.19/21.65 % (1482604)Termination phase: Saturation
% 101.19/21.65 % (1482604)Time elapsed: 1.526 s
% 101.19/21.65 % (1482604)Peak memory usage: 134 MB
% 101.19/21.65 % (1482604)Instructions burned: 1980 (million)
% 101.19/21.65 % (1482688)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=reverse_frequency:bce=on:random_seed=401436650:s2pl=on:i=3980:gtgl=3:kws=precedence:fgj=on:gtg=all_2842 on theBenchmark for (2842ds/3980Mi)
% 101.19/21.65 % (1482398)Instruction limit reached!
% 101.19/21.65 % (1482398)------------------------------
% 101.19/21.65 % (1482398)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 101.19/21.65 % (1482398)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 101.19/21.65 % (1482398)CaDiCaL version: 2.1.3
% 101.19/21.65 % (1482398)Termination reason: Instruction limit
% 101.19/21.65 % (1482398)Termination phase: Saturation
% 101.19/21.65 % (1482398)Time elapsed: 4.824 s
% 101.19/21.65 % (1482398)Peak memory usage: 208 MB
% 101.19/21.65 % (1482398)Instructions burned: 13942 (million)
% 101.19/21.65 % (1482704)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:prc=on:sp=reverse_frequency:spb=units:lsd=20:urr=ec_only:bce=on:fd=off:kmz=on:random_seed=114477543:i=2087:s2at=3:kws=frequency:av=off:fsr=off_2835 on theBenchmark for (2835ds/2087Mi)
% 146.29/21.85 % (1482643)Instruction limit reached!
% 146.29/21.85 % (1482643)------------------------------
% 146.29/21.85 % (1482643)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 146.29/21.85 % (1482643)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 146.29/21.85 % (1482643)CaDiCaL version: 2.1.3
% 146.29/21.85 % (1482643)Termination reason: Instruction limit
% 146.29/21.85 % (1482643)Termination phase: Saturation
% 146.29/21.85 % (1482643)Time elapsed: 2.906 s
% 146.29/21.85 % (1482643)Peak memory usage: 115 MB
% 146.29/21.85 % (1482643)Instructions burned: 3917 (million)
% 146.29/21.85 % (1482716)ott-1004_1_anc=all_dependent:to=lpo:ncem=casc2026/models/loop5.pt:sil=8000:tgt=full:npcc=on:sas=cadical:sp=const_frequency:acc=on:urr=ec_only:gs=on:s2agt=40:alpa=false:sac=on:random_seed=4248944804:cts=off:cond=on:i=4272:bs=on:fsd=on_2826 on theBenchmark for (2826ds/4272Mi)
% 146.29/21.85 % (1482704)Instruction limit reached!
% 146.29/21.85 % (1482704)------------------------------
% 146.29/21.85 % (1482704)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 146.29/21.85 % (1482704)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 146.29/21.85 % (1482704)CaDiCaL version: 2.1.3
% 146.29/21.85 % (1482704)Termination reason: Instruction limit
% 146.29/21.85 % (1482704)Termination phase: Saturation
% 146.29/21.85 % (1482704)Time elapsed: 1.118 s
% 146.29/21.85 % (1482704)Peak memory usage: 138 MB
% 146.29/21.85 % (1482704)Instructions burned: 2087 (million)
% 146.29/21.85 % (1482722)lrs-30_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:urr=on:bce=on:rp=on:br=off:flr=on:random_seed=3654118752:st=-1:i=2197:kws=precedence:av=off:ss=axioms:er=known_2822 on theBenchmark for (2822ds/2197Mi)
% 146.29/21.85 [W927 10:55:05.400272972 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 146.29/21.85 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 146.29/21.85 [W927 10:55:05.400319869 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 146.29/21.85 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 146.29/21.85 [W927 10:55:05.400380036 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 146.29/21.85 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 146.29/21.85 [W927 10:55:05.400399580 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 146.29/21.85 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 146.29/21.85 [W927 10:55:05.400443380 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 146.29/21.85 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 146.29/21.85 [W927 10:55:05.400462077 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 146.29/21.85 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 146.29/21.85 [W927 10:55:05.400506721 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 146.29/21.85 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 146.29/21.85 [W927 10:55:05.400525634 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 146.29/21.85 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 146.29/21.85 [W927 10:55:05.400569684 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 146.29/21.85 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 146.29/21.85 [W927 10:55:05.400586901 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 146.29/21.85 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 146.29/21.85 [W927 10:55:05.400629451 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 146.29/21.85 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 146.29/21.85 [W927 10:55:05.400646482 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 146.29/21.85 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 146.29/21.85 % (1482722)Refutation not found, incomplete strategy
% 146.29/21.85 % (1482722)------------------------------
% 146.29/21.85 % (1482722)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 146.29/21.85 % (1482722)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 146.29/21.85 % (1482722)CaDiCaL version: 2.1.3
% 146.29/21.85 % (1482722)Termination reason: Refutation not found, incomplete strategy
% 146.29/21.85 % (1482722)Time elapsed: 0.845 s
% 146.29/21.85 % (1482722)Peak memory usage: 125 MB
% 146.29/21.85 % (1482722)Instructions burned: 820 (million)
% 146.29/21.85 % (1482722)------------------------------
% 146.29/21.85 % (1482722)------------------------------
% 146.29/21.85 % (1482673)Instruction limit reached!
% 146.29/21.85 % (1482673)------------------------------
% 146.29/21.85 % (1482673)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 146.29/21.85 % (1482673)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 146.29/21.85 % (1482673)CaDiCaL version: 2.1.3
% 146.29/21.85 % (1482673)Termination reason: Instruction limit
% 146.29/21.85 % (1482673)Termination phase: Saturation
% 146.29/21.85 % (1482673)Time elapsed: 3.969 s
% 146.29/21.85 % (1482673)Peak memory usage: 154 MB
% 146.29/21.85 % (1482673)Instructions burned: 3940 (million)
% 146.29/21.85 % (1482732)dis+21_1_sil=8000:spb=goal_then_units:random_seed=4291171127:avsq=on:i=6508:avsqr=1,16:kws=arity_squared:fgj=on_2807 on theBenchmark for (2807ds/6508Mi)
% 146.29/21.85 % (1482733)dis-1002_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=occurrence:random_seed=43884519:i=2330:fgj=on:av=off:fsr=off_2805 on theBenchmark for (2805ds/2330Mi)
% 146.29/21.85 % (1482688)Instruction limit reached!
% 146.29/21.85 % (1482688)------------------------------
% 146.29/21.85 % (1482688)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 146.29/21.85 % (1482688)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 146.29/21.85 % (1482688)CaDiCaL version: 2.1.3
% 146.29/21.85 % (1482688)Termination reason: Instruction limit
% 146.29/21.85 % (1482688)Termination phase: Saturation
% 146.29/21.85 % (1482688)Time elapsed: 3.835 s
% 146.29/21.85 % (1482688)Peak memory usage: 152 MB
% 146.29/21.85 % (1482688)Instructions burned: 3980 (million)
% 146.29/21.85 % (1482737)dis+10_2_anc=none:sil=64000:bsr=on:rp=on:alpa=true:avsqc=1:random_seed=3774484340:avsq=on:i=7592:avsqr=1,16:bs=on:gsp=on_2802 on theBenchmark for (2802ds/7592Mi)
% 146.29/21.85 % (1482737)First to succeed.
% 146.29/21.85 % (1482737)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-1482185"
% 146.29/21.85 % SZS status Satisfiable for theBenchmark
% 146.29/21.85 % SZS output start Saturation.
% See solution above
% 146.29/21.85 % SZS output start Definitions and Model Updates.
% 146.29/21.85 % SZS output end Definitions and Model Updates.
% 146.29/21.85 % (1482737)------------------------------
% 146.29/21.85 % (1482737)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 146.29/21.85 % (1482737)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 146.29/21.85 % (1482737)CaDiCaL version: 2.1.3
% 146.29/21.85 % (1482737)Termination reason: Satisfiable
% 146.29/21.85 % (1482737)Time elapsed: 0.027 s
% 146.29/21.85 % (1482737)Peak memory usage: 88 MB
% 146.29/21.85 % (1482737)Instructions burned: 25 (million)
% 146.29/21.85 % (1482737)------------------------------
% 146.29/21.85 % (1482737)------------------------------
% 146.29/21.85 % (1482185)Success in time 20.616 s
% 146.29/21.85 % Vampire exiting
%------------------------------------------------------------------------------