%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LAT056-1 : 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 : n006.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 11:45:55 AM UTC 2026
% Result : Satisfiable 0.18s 21.90s
% Output : Saturation 0.18s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u2731,axiom,
n0 = n1 ).
cnf(u2735,axiom,
n1 = X0 ).
cnf(u5591,axiom,
join(X1,X0) = n1 ).
cnf(u209,axiom,
join(X1,X0) = join(X0,join(X1,X0)) ).
cnf(u210,axiom,
meet(X1,X0) = meet(X0,meet(X1,X0)) ).
cnf(u114,axiom,
( meet(X2,join(X3,meet(X0,X1))) = join(X3,meet(X0,meet(X1,X2)))
| meet(X3,X2) != X3 ) ).
cnf(u205,axiom,
meet(X0,X2) = meet(X0,meet(join(X1,X0),X2)) ).
cnf(u100,axiom,
join(X0,X1) = meet(join(X0,X1),join(X0,join(X1,X2))) ).
cnf(x_meet_1,axiom,
meet(X0,n1) = X0 ).
cnf(u129,axiom,
( join(X1,join(X2,meet(X3,X0))) = meet(X0,join(X1,join(X2,X3)))
| join(X1,X2) != meet(join(X1,X2),X0) ) ).
cnf(u178,axiom,
join(X2,meet(X0,meet(X1,X2))) = X2 ).
cnf(u111,axiom,
( join(X2,X0) = meet(join(X0,X1),join(X2,X0))
| meet(X2,join(X0,X1)) != X2 ) ).
cnf(u24,axiom,
n0 = meet(n0,X0) ).
cnf(u2669,axiom,
( join(X0,join(X1,X2)) = n1
| n1 != X1 ) ).
cnf(u34,axiom,
join(n0,X0) = X0 ).
cnf(u3057,axiom,
( meet(X1,X0) != n1
| n1 = X0 ) ).
cnf(u510,axiom,
meet(X0,join(X2,join(X0,X1))) = X0 ).
cnf(u109,axiom,
( meet(X0,join(X2,X1)) = join(X2,meet(X0,X1))
| meet(X2,X0) != X2 ) ).
cnf(u119,axiom,
( join(meet(X0,X1),X2) = meet(X1,join(X2,X0))
| meet(X2,X1) != X2 ) ).
cnf(u2658,axiom,
( join(X0,X1) = n1
| n1 != X1 ) ).
cnf(absorption1,axiom,
meet(X0,join(X0,X1)) = X0 ).
cnf(u60,axiom,
meet(X0,X1) = meet(X0,meet(X1,join(meet(X0,X1),X2))) ).
cnf(u1632,axiom,
( join(X0,X1) = X0
| meet(X1,X0) != X1 ) ).
cnf(u2977,axiom,
( meet(X1,X0) = X0
| n0 != X0 ) ).
cnf(u84,axiom,
join(X0,X1) = join(X0,join(X0,X1)) ).
cnf(u94,axiom,
join(X0,X1) = join(X0,join(X1,meet(join(X0,X1),X2))) ).
cnf(x_join_0,axiom,
join(X0,n0) = X0 ).
cnf(u185,axiom,
join(X0,X2) = join(X0,join(meet(X1,X0),X2)) ).
cnf(u124,axiom,
( join(X1,join(meet(X2,X0),X3)) = join(meet(X0,join(X1,X2)),X3)
| meet(X1,X0) != X1 ) ).
cnf(u85,axiom,
join(join(X0,X1),X2) = join(X1,join(X0,X2)) ).
cnf(commutativity_of_join,axiom,
join(X0,X1) = join(X1,X0) ).
cnf(u35,axiom,
n1 = join(n1,X0) ).
cnf(associativity_of_join,axiom,
join(join(X0,X1),X2) = join(X0,join(X1,X2)) ).
cnf(u87,axiom,
join(X0,X2) = join(X0,join(meet(X0,X1),X2)) ).
cnf(u3054,axiom,
( meet(X0,X1) != n1
| n1 = X0 ) ).
cnf(absorption2,axiom,
join(X0,meet(X0,X1)) = X0 ).
cnf(u49,axiom,
meet(X0,X1) = meet(X0,meet(X0,X1)) ).
cnf(u14,axiom,
n1 = join(X0,n1) ).
cnf(u131,axiom,
( meet(X1,X0) != X1
| meet(X0,X1) = X1 ) ).
cnf(commutativity_of_meet,axiom,
meet(X0,X1) = meet(X1,X0) ).
cnf(u2670,axiom,
( join(X0,join(X1,X2)) = n1
| n1 != X2 ) ).
cnf(modular,axiom,
( meet(X1,join(X0,X2)) = join(X0,meet(X2,X1))
| meet(X0,X1) != X0 ) ).
cnf(u66,axiom,
meet(X0,X1) = join(meet(X0,X1),meet(X0,meet(X1,X2))) ).
cnf(u2974,axiom,
( meet(X0,X1) = X0
| n0 != X0 ) ).
cnf(u52,axiom,
meet(X0,X2) = meet(X0,meet(join(X0,X1),X2)) ).
cnf(u25,axiom,
meet(n1,X0) = X0 ).
cnf(idempotence_of_join,axiom,
join(X0,X0) = X0 ).
cnf(u58,axiom,
meet(X0,meet(X1,X2)) = meet(X1,meet(X2,X0)) ).
cnf(u3508,axiom,
( n0 != X1
| n0 != X0
| X0 = X1 ) ).
cnf(u2972,axiom,
( join(X0,X1) = X0
| n0 != X1 ) ).
cnf(u650,axiom,
join(X1,meet(X0,meet(X1,X2))) = X1 ).
cnf(u889,axiom,
join(X1,X0) = join(X1,join(X0,meet(X1,X2))) ).
cnf(u198,axiom,
meet(X2,join(X0,join(X1,X2))) = X2 ).
cnf(u10,axiom,
n0 = meet(X0,n0) ).
cnf(u1631,axiom,
( join(X1,X0) = X0
| meet(X1,X0) != X1 ) ).
cnf(u475,axiom,
meet(X1,X0) = meet(X1,meet(X0,join(X1,X2))) ).
cnf(u28,axiom,
join(X1,meet(X0,X1)) = X1 ).
cnf(u38,axiom,
meet(X1,join(X0,X1)) = X1 ).
cnf(u2654,axiom,
( join(X0,X2) = X2
| n0 != X0 ) ).
cnf(u127,axiom,
( meet(X1,meet(X0,join(X1,X2))) = X1
| meet(X1,X0) != X1 ) ).
cnf(idempotence_of_meet,axiom,
meet(X0,X0) = X0 ).
cnf(u50,axiom,
meet(meet(X0,X1),X2) = meet(X1,meet(X0,X2)) ).
cnf(u4217,axiom,
X0 = X1 ).
cnf(u2652,axiom,
( join(X1,X2) = n1
| n1 != X1 ) ).
cnf(associativity_of_meet,axiom,
meet(meet(X0,X1),X2) = meet(X0,meet(X1,X2)) ).
cnf(u92,axiom,
join(X0,join(X1,X2)) = join(X1,join(X2,X0)) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LAT056-1 : TPTP v9.3.1. Released v2.5.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.13/0.38 % Computer : n006.cluster.edu
% 0.13/0.38 % Model : x86_64 x86_64
% 0.13/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.38 % Memory : 8046.5625MB
% 0.13/0.38 % OS : Linux 6.8.0-71-generic
% 0.13/0.38 % CPULimit : 300
% 0.13/0.38 % WCLimit : 300
% 0.13/0.38 % DateTime : Sun Sep 27 13:57:55 UTC 2026
% 0.13/0.38 % CPUTime :
% 0.13/0.38 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.13/0.42 Running first-order theorem proving
% 0.13/0.42 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
% 8.61/2.06 % (2991932)Input is clausal, will run a generic CNF schedule.
% 8.61/2.06 % (2992021)lrs+10_1_sil=8000:sp=occurrence:random_seed=874324085:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 8.61/2.06 % (2992021)Refutation not found, incomplete strategy
% 8.61/2.06 % (2992021)------------------------------
% 8.61/2.06 % (2992021)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.61/2.06 % (2992021)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.61/2.06 % (2992021)CaDiCaL version: 2.1.3
% 8.61/2.06 % (2992021)Termination reason: Refutation not found, incomplete strategy
% 8.61/2.06 % (2992021)Time elapsed: 0.0000 s
% 8.61/2.06 % (2992021)Peak memory usage: 86 MB
% 8.61/2.06 % (2992024)dis-21_1_sil=8000:lcm=predicate:random_seed=3748760224:st=5:avsq=on:i=117:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/117Mi)
% 8.61/2.06 % (2992018)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=4138565825:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 8.61/2.06 % (2992022)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=4045341275:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 8.61/2.06 % (2992020)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=2803095012:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 8.61/2.06 % (2992023)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1476267931:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 8.61/2.06 % (2992019)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=2294689496:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 8.61/2.06 % (2992022)Refutation not found, incomplete strategy
% 8.61/2.06 % (2992022)------------------------------
% 8.61/2.06 % (2992022)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.61/2.06 % (2992024)Refutation not found, incomplete strategy
% 8.61/2.06 % (2992024)------------------------------
% 8.61/2.06 % (2992024)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.61/2.06 % (2992022)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.61/2.06 % (2992024)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.61/2.06 % (2992022)CaDiCaL version: 2.1.3
% 8.61/2.06 % (2992022)Termination reason: Refutation not found, incomplete strategy
% 8.61/2.06 % (2992022)Time elapsed: 0.0000 s
% 8.61/2.06 % (2992024)CaDiCaL version: 2.1.3
% 8.61/2.06 % (2992022)Peak memory usage: 86 MB
% 8.61/2.06 % (2992024)Termination reason: Refutation not found, incomplete strategy
% 8.61/2.06 % (2992024)Time elapsed: 0.001 s
% 8.61/2.06 % (2992024)Peak memory usage: 86 MB
% 8.61/2.06 % (2992023)Instruction limit reached!
% 8.61/2.06 % (2992023)------------------------------
% 8.61/2.06 % (2992023)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.61/2.06 % (2992023)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.61/2.06 % (2992023)CaDiCaL version: 2.1.3
% 8.61/2.06 % (2992023)Termination reason: Instruction limit
% 8.61/2.06 % (2992023)Termination phase: Saturation
% 8.61/2.06 % (2992023)Time elapsed: 0.098 s
% 8.61/2.06 % (2992023)Peak memory usage: 89 MB
% 8.61/2.06 % (2992023)Instructions burned: 181 (million)
% 8.61/2.06 % (2992021)------------------------------
% 8.61/2.06 % (2992021)------------------------------
% 8.61/2.06 % (2992064)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=1792513294:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2997 on theBenchmark for (2997ds/189Mi)
% 8.61/2.06 % (2992064)Refutation not found, incomplete strategy
% 8.61/2.06 % (2992064)------------------------------
% 8.61/2.06 % (2992064)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.61/2.06 % (2992064)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.61/2.06 % (2992064)CaDiCaL version: 2.1.3
% 8.61/2.06 % (2992064)Termination reason: Refutation not found, incomplete strategy
% 8.61/2.06 % (2992064)Time elapsed: 0.0000 s
% 8.61/2.06 % (2992064)Peak memory usage: 86 MB
% 8.61/2.06 % (2992060)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=1957862662:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi)
% 12.02/2.65 % (2992060)Refutation not found, incomplete strategy
% 12.02/2.65 % (2992060)------------------------------
% 12.02/2.65 % (2992060)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.02/2.65 % (2992060)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.02/2.65 % (2992060)CaDiCaL version: 2.1.3
% 12.02/2.65 % (2992060)Termination reason: Refutation not found, incomplete strategy
% 12.02/2.65 % (2992060)Time elapsed: 0.0000 s
% 12.02/2.65 % (2992060)Peak memory usage: 86 MB
% 12.02/2.65 % (2992022)------------------------------
% 12.02/2.65 % (2992022)------------------------------
% 12.02/2.65 % (2992024)------------------------------
% 12.02/2.65 % (2992024)------------------------------
% 12.02/2.65 % (2992064)------------------------------
% 12.02/2.65 % (2992064)------------------------------
% 12.02/2.65 % (2992129)lrs+10_64_to=lpo:sil=8000:random_seed=292212650:i=126:bd=preordered_2995 on theBenchmark for (2995ds/126Mi)
% 12.02/2.65 % (2992127)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=637515136:st=4:i=219:sd=3:ss=axioms_2995 on theBenchmark for (2995ds/219Mi)
% 12.02/2.65 % (2992127)Refutation not found, incomplete strategy
% 12.02/2.65 % (2992127)------------------------------
% 12.02/2.65 % (2992127)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.02/2.65 % (2992127)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.02/2.65 % (2992127)CaDiCaL version: 2.1.3
% 12.02/2.65 % (2992127)Termination reason: Refutation not found, incomplete strategy
% 12.02/2.65 % (2992127)Time elapsed: 0.0000 s
% 12.02/2.65 % (2992127)Peak memory usage: 86 MB
% 12.02/2.65 % (2992129)Instruction limit reached!
% 12.02/2.65 % (2992129)------------------------------
% 12.02/2.65 % (2992129)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.02/2.65 % (2992129)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.02/2.65 % (2992129)CaDiCaL version: 2.1.3
% 12.02/2.65 % (2992129)Termination reason: Instruction limit
% 12.02/2.65 % (2992129)Termination phase: Saturation
% 12.02/2.65 % (2992129)Time elapsed: 0.074 s
% 12.02/2.65 % (2992129)Peak memory usage: 88 MB
% 12.02/2.65 % (2992129)Instructions burned: 127 (million)
% 12.02/2.65 % (2992060)------------------------------
% 12.02/2.65 % (2992060)------------------------------
% 12.02/2.65 % (2992171)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=554734578:avsq=on:i=194:fgj=on:bd=preordered_2994 on theBenchmark for (2994ds/194Mi)
% 12.02/2.65 % (2992171)Instruction limit reached!
% 12.02/2.65 % (2992171)------------------------------
% 12.02/2.65 % (2992171)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.02/2.65 % (2992171)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.02/2.65 % (2992171)CaDiCaL version: 2.1.3
% 12.02/2.65 % (2992171)Termination reason: Instruction limit
% 12.02/2.65 % (2992171)Termination phase: Saturation
% 12.02/2.65 % (2992171)Time elapsed: 0.065 s
% 12.02/2.65 % (2992171)Peak memory usage: 90 MB
% 12.02/2.65 % (2992171)Instructions burned: 195 (million)
% 12.02/2.65 % (2992175)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=3330007234:i=3394:sd=4:ss=included:sgt=64_2993 on theBenchmark for (2993ds/3394Mi)
% 12.02/2.65 % (2992174)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=3684285743:i=157:gtg=all_2993 on theBenchmark for (2993ds/157Mi)
% 12.02/2.65 % (2992127)------------------------------
% 12.02/2.65 % (2992127)------------------------------
% 12.02/2.65 % (2992197)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=3870187383:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2992 on theBenchmark for (2992ds/106Mi)
% 12.02/2.65 % (2992197)Refutation not found, incomplete strategy
% 12.02/2.65 % (2992197)------------------------------
% 12.02/2.65 % (2992197)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.02/2.65 % (2992197)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.02/2.65 % (2992197)CaDiCaL version: 2.1.3
% 12.02/2.65 % (2992197)Termination reason: Refutation not found, incomplete strategy
% 12.02/2.65 % (2992197)Time elapsed: 0.0000 s
% 12.02/2.65 % (2992197)Peak memory usage: 86 MB
% 12.02/2.65 % (2992174)Instruction limit reached!
% 12.02/2.65 % (2992174)------------------------------
% 12.02/2.65 % (2992174)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.37/3.56 % (2992174)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.37/3.56 % (2992174)CaDiCaL version: 2.1.3
% 18.37/3.56 % (2992174)Termination reason: Instruction limit
% 18.37/3.56 % (2992174)Termination phase: Saturation
% 18.37/3.56 % (2992174)Time elapsed: 0.092 s
% 18.37/3.56 % (2992174)Peak memory usage: 89 MB
% 18.37/3.56 % (2992174)Instructions burned: 159 (million)
% 18.37/3.56 % (2992227)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=342897742:i=107_2991 on theBenchmark for (2991ds/107Mi)
% 18.37/3.56 % (2992227)Refutation not found, incomplete strategy
% 18.37/3.56 % (2992227)------------------------------
% 18.37/3.56 % (2992227)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.37/3.56 % (2992227)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.37/3.56 % (2992227)CaDiCaL version: 2.1.3
% 18.37/3.56 % (2992227)Termination reason: Refutation not found, incomplete strategy
% 18.37/3.56 % (2992227)Time elapsed: 0.001 s
% 18.37/3.56 % (2992227)Peak memory usage: 87 MB
% 18.37/3.56 % (2992197)------------------------------
% 18.37/3.56 % (2992197)------------------------------
% 18.37/3.56 % (2992229)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=3770129678:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2990 on theBenchmark for (2990ds/242Mi)
% 18.37/3.56 % (2992229)Refutation not found, incomplete strategy
% 18.37/3.56 % (2992229)------------------------------
% 18.37/3.56 % (2992229)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.37/3.56 % (2992229)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.37/3.56 % (2992229)CaDiCaL version: 2.1.3
% 18.37/3.56 % (2992229)Termination reason: Refutation not found, incomplete strategy
% 18.37/3.56 % (2992229)Time elapsed: 0.001 s
% 18.37/3.56 % (2992229)Peak memory usage: 86 MB
% 18.37/3.56 % (2992231)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=2768568300:cond=fast:i=5208:av=off_2990 on theBenchmark for (2990ds/5208Mi)
% 18.37/3.56 [W927 13:57:57.834188548 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 18.37/3.56 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 18.37/3.56 [W927 13:57:57.834221688 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 18.37/3.56 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 18.37/3.56 [W927 13:57:57.834259908 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 18.37/3.56 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 18.37/3.56 [W927 13:57:57.834272662 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 18.37/3.56 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 18.37/3.56 [W927 13:57:57.834298558 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 18.37/3.56 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 18.37/3.56 [W927 13:57:57.834309752 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 18.37/3.56 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 18.37/3.56 [W927 13:57:57.834336235 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 18.37/3.56 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 27.27/4.79 [W927 13:57:57.834347542 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 27.27/4.79 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 27.27/4.79 [W927 13:57:57.834378888 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 27.27/4.79 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 27.27/4.79 [W927 13:57:57.834443798 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 27.27/4.79 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 27.27/4.79 [W927 13:57:57.834481649 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 27.27/4.79 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 27.27/4.79 [W927 13:57:57.834493025 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 27.27/4.79 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 27.27/4.79 % (2992227)------------------------------
% 27.27/4.79 % (2992227)------------------------------
% 27.27/4.79 % (2992229)------------------------------
% 27.27/4.79 % (2992229)------------------------------
% 27.27/4.79 % (2992175)Refutation not found, incomplete strategy
% 27.27/4.79 % (2992175)------------------------------
% 27.27/4.79 % (2992175)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.27/4.79 % (2992175)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.27/4.79 % (2992175)CaDiCaL version: 2.1.3
% 27.27/4.79 % (2992175)Termination reason: Refutation not found, incomplete strategy
% 27.27/4.79 % (2992175)Time elapsed: 0.559 s
% 27.27/4.79 % (2992175)Peak memory usage: 125 MB
% 27.27/4.79 % (2992175)Instructions burned: 825 (million)
% 27.27/4.79 % (2992234)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=1854426851:i=134:sd=2:doe=on:ss=axioms:sgt=14_2987 on theBenchmark for (2987ds/134Mi)
% 27.27/4.79 % (2992234)Refutation not found, incomplete strategy
% 27.27/4.79 % (2992234)------------------------------
% 27.27/4.79 % (2992234)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.27/4.79 % (2992234)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.27/4.79 % (2992234)CaDiCaL version: 2.1.3
% 27.27/4.79 % (2992234)Termination reason: Refutation not found, incomplete strategy
% 27.27/4.79 % (2992234)Time elapsed: 0.001 s
% 27.27/4.79 % (2992234)Peak memory usage: 86 MB
% 27.27/4.79 % (2992235)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=2630803353:i=499:bd=all_2986 on theBenchmark for (2986ds/499Mi)
% 27.27/4.79 % (2992175)------------------------------
% 27.27/4.79 % (2992175)------------------------------
% 27.27/4.79 % (2992234)------------------------------
% 27.27/4.79 % (2992234)------------------------------
% 27.27/4.79 % (2992239)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=539137486:i=264:kws=precedence:fsr=off_2983 on theBenchmark for (2983ds/264Mi)
% 27.27/4.79 % (2992238)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=3545010851:i=191:fgj=on:bd=all_2983 on theBenchmark for (2983ds/191Mi)
% 27.27/4.79 % (2992235)Instruction limit reached!
% 27.27/4.79 % (2992235)------------------------------
% 27.27/4.79 % (2992235)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.27/4.79 % (2992235)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.27/4.79 % (2992235)CaDiCaL version: 2.1.3
% 27.27/4.79 % (2992235)Termination reason: Instruction limit
% 27.27/4.79 % (2992235)Termination phase: Saturation
% 27.27/4.79 % (2992235)Time elapsed: 0.303 s
% 27.27/4.79 % (2992235)Peak memory usage: 93 MB
% 27.27/4.79 % (2992235)Instructions burned: 500 (million)
% 28.49/4.92 % (2992238)Instruction limit reached!
% 28.49/4.92 % (2992238)------------------------------
% 28.49/4.92 % (2992238)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.49/4.92 % (2992238)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.49/4.92 % (2992238)CaDiCaL version: 2.1.3
% 28.49/4.92 % (2992238)Termination reason: Instruction limit
% 28.49/4.92 % (2992238)Termination phase: Saturation
% 28.49/4.92 % (2992238)Time elapsed: 0.119 s
% 28.49/4.92 % (2992238)Peak memory usage: 90 MB
% 28.49/4.92 % (2992238)Instructions burned: 191 (million)
% 28.49/4.92 % (2992239)Instruction limit reached!
% 28.49/4.92 % (2992239)------------------------------
% 28.49/4.92 % (2992239)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.49/4.92 % (2992239)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.49/4.92 % (2992239)CaDiCaL version: 2.1.3
% 28.49/4.92 % (2992239)Termination reason: Instruction limit
% 28.49/4.92 % (2992239)Termination phase: Saturation
% 28.49/4.92 % (2992239)Time elapsed: 0.151 s
% 28.49/4.92 % (2992239)Peak memory usage: 91 MB
% 28.49/4.92 % (2992239)Instructions burned: 264 (million)
% 28.49/4.92 % (2992242)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=838351963:cond=on:i=156:bs=on:gtg=exists_all:er=known_2982 on theBenchmark for (2982ds/156Mi)
% 28.49/4.92 % (2992242)Instruction limit reached!
% 28.49/4.92 % (2992242)------------------------------
% 28.49/4.92 % (2992242)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.49/4.92 % (2992242)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.49/4.92 % (2992242)CaDiCaL version: 2.1.3
% 28.49/4.92 % (2992242)Termination reason: Instruction limit
% 28.49/4.92 % (2992242)Termination phase: Saturation
% 28.49/4.92 % (2992242)Time elapsed: 0.090 s
% 28.49/4.92 % (2992242)Peak memory usage: 88 MB
% 28.49/4.92 % (2992242)Instructions burned: 157 (million)
% 28.49/4.92 % (2992243)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=1935052979:i=3256:kws=precedence:bd=preordered:av=off_2980 on theBenchmark for (2980ds/3256Mi)
% 28.49/4.92 % (2992244)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=1807033802:i=537:av=off:ss=included_2980 on theBenchmark for (2980ds/537Mi)
% 28.49/4.92 % (2992244)Refutation not found, incomplete strategy
% 28.49/4.92 % (2992244)------------------------------
% 28.49/4.92 % (2992244)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.49/4.92 % (2992244)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.49/4.92 % (2992244)CaDiCaL version: 2.1.3
% 28.49/4.92 % (2992244)Termination reason: Refutation not found, incomplete strategy
% 28.49/4.92 % (2992244)Time elapsed: 0.0000 s
% 28.49/4.92 % (2992244)Peak memory usage: 86 MB
% 28.49/4.92 % (2992246)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=1998760982:i=180:bd=preordered:av=off_2979 on theBenchmark for (2979ds/180Mi)
% 28.49/4.92 % (2992246)Instruction limit reached!
% 28.49/4.92 % (2992246)------------------------------
% 28.49/4.92 % (2992246)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.49/4.92 % (2992246)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.49/4.92 % (2992246)CaDiCaL version: 2.1.3
% 28.49/4.92 % (2992246)Termination reason: Instruction limit
% 28.49/4.92 % (2992246)Termination phase: Saturation
% 28.49/4.92 % (2992246)Time elapsed: 0.101 s
% 28.49/4.92 % (2992246)Peak memory usage: 88 MB
% 28.49/4.92 % (2992246)Instructions burned: 180 (million)
% 28.49/4.92 % (2992244)------------------------------
% 28.49/4.92 % (2992244)------------------------------
% 28.49/4.92 % (2992250)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=1974849715:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2977 on theBenchmark for (2977ds/10307Mi)
% 28.49/4.92 % (2992251)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=3683028181:i=412:gtgl=4:gtg=exists_all_2976 on theBenchmark for (2976ds/412Mi)
% 28.49/4.92 % (2992251)Instruction limit reached!
% 28.49/4.92 % (2992251)------------------------------
% 28.49/4.92 % (2992251)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.49/4.92 % (2992251)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.97/6.71 % (2992251)CaDiCaL version: 2.1.3
% 40.97/6.71 % (2992251)Termination reason: Instruction limit
% 40.97/6.71 % (2992251)Termination phase: Saturation
% 40.97/6.71 % (2992251)Time elapsed: 0.216 s
% 40.97/6.71 % (2992251)Peak memory usage: 90 MB
% 40.97/6.71 % (2992251)Instructions burned: 413 (million)
% 40.97/6.71 % (2992231)Instruction limit reached!
% 40.97/6.71 % (2992231)------------------------------
% 40.97/6.71 % (2992231)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.97/6.71 % (2992231)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.97/6.71 % (2992231)CaDiCaL version: 2.1.3
% 40.97/6.71 % (2992231)Termination reason: Instruction limit
% 40.97/6.71 % (2992231)Termination phase: Saturation
% 40.97/6.71 % (2992231)Time elapsed: 1.663 s
% 40.97/6.71 % (2992231)Peak memory usage: 163 MB
% 40.97/6.71 % (2992231)Instructions burned: 5210 (million)
% 40.97/6.71 % (2992254)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=1753371108:s2pl=no:i=8478:s2at=4:nm=6_2973 on theBenchmark for (2973ds/8478Mi)
% 40.97/6.71 % (2992255)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=3188467667:s2a=on:i=303:s2at=2:sd=1:kws=inv_arity:bs=on:ins=10:fdi=1024:sup=off:ss=included_2972 on theBenchmark for (2972ds/303Mi)
% 40.97/6.71 % (2992255)Refutation not found, incomplete strategy
% 40.97/6.71 % (2992255)------------------------------
% 40.97/6.71 % (2992255)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.97/6.71 % (2992255)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.97/6.71 % (2992255)CaDiCaL version: 2.1.3
% 40.97/6.71 % (2992255)Termination reason: Refutation not found, incomplete strategy
% 40.97/6.71 % (2992255)Time elapsed: 0.0000 s
% 40.97/6.71 % (2992255)Peak memory usage: 87 MB
% 40.97/6.71 % (2992255)------------------------------
% 40.97/6.71 % (2992255)------------------------------
% 40.97/6.71 % (2992258)lrs+10_1_to=lpo:sil=16000:fde=none:sos=on:urr=on:bsr=on:random_seed=1475989093:st=4:i=720:sd=3:fsr=off:ss=axioms_2969 on theBenchmark for (2969ds/720Mi)
% 40.97/6.71 % (2992258)Refutation not found, incomplete strategy
% 40.97/6.71 % (2992258)------------------------------
% 40.97/6.71 % (2992258)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.97/6.71 % (2992258)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.97/6.71 % (2992258)CaDiCaL version: 2.1.3
% 40.97/6.71 % (2992258)Termination reason: Refutation not found, incomplete strategy
% 40.97/6.71 % (2992258)Time elapsed: 0.0000 s
% 40.97/6.71 % (2992258)Peak memory usage: 86 MB
% 40.97/6.71 % (2992258)------------------------------
% 40.97/6.71 % (2992258)------------------------------
% 40.97/6.71 % (2992260)lrs-20_1_to=lpo:sil=32000:tgt=ground:sp=reverse_frequency:spb=goal:urr=on:bsr=unit_only:nwc=1.5:random_seed=494921685:i=598:bs=on:bd=preordered:av=off:ss=axioms_2966 on theBenchmark for (2966ds/598Mi)
% 40.97/6.71 % (2992260)Refutation not found, incomplete strategy
% 40.97/6.71 % (2992260)------------------------------
% 40.97/6.71 % (2992260)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.97/6.71 % (2992260)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.97/6.71 % (2992260)CaDiCaL version: 2.1.3
% 40.97/6.71 % (2992260)Termination reason: Refutation not found, incomplete strategy
% 40.97/6.71 % (2992260)Time elapsed: 0.0000 s
% 40.97/6.71 % (2992260)Peak memory usage: 86 MB
% 40.97/6.71 % (2992260)------------------------------
% 40.97/6.71 % (2992260)------------------------------
% 40.97/6.71 % (2992262)dis-1010_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=occurrence:random_seed=53167177:i=2989:sd=3:ss=axioms:sgt=60_2964 on theBenchmark for (2964ds/2989Mi)
% 40.97/6.71 [W927 13:58:00.566886269 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 40.97/6.71 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 40.97/6.71 [W927 13:58:00.566923405 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 40.97/6.71 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 44.03/7.09 [W927 13:58:00.566945159 register_special_ops.cpp:225] Warning: Creating a tensor from 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.03/7.09 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 44.03/7.09 [W927 13:58:00.566951882 register_special_ops.cpp:225] Warning: Creating a tensor from 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.03/7.09 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 44.03/7.09 [W927 13:58:00.566964785 register_special_ops.cpp:225] Warning: Creating a tensor from 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.03/7.09 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 44.03/7.09 [W927 13:58:00.566970688 register_special_ops.cpp:225] Warning: Creating a tensor from 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.03/7.09 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 44.03/7.09 [W927 13:58:00.566983829 register_special_ops.cpp:225] Warning: Creating a tensor from 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.03/7.09 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 44.03/7.09 [W927 13:58:00.566989794 register_special_ops.cpp:225] Warning: Creating a tensor from 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.03/7.09 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 44.03/7.09 [W927 13:58:00.567008751 register_special_ops.cpp:225] Warning: Creating a tensor from 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.03/7.09 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 44.03/7.09 [W927 13:58:00.567015314 register_special_ops.cpp:225] Warning: Creating a tensor from 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.03/7.09 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 44.03/7.09 [W927 13:58:00.567028712 register_special_ops.cpp:225] Warning: Creating a tensor from 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.03/7.09 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 44.03/7.09 [W927 13:58:00.567039155 register_special_ops.cpp:225] Warning: Creating a tensor from 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.03/7.09 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 44.03/7.09 % (2992262)Refutation not found, incomplete strategy
% 44.03/7.09 % (2992262)------------------------------
% 44.03/7.09 % (2992262)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 44.03/7.09 % (2992262)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.03/7.09 % (2992262)CaDiCaL version: 2.1.3
% 44.03/7.09 % (2992262)Termination reason: Refutation not found, incomplete strategy
% 44.03/7.09 % (2992262)Time elapsed: 0.309 s
% 44.03/7.09 % (2992262)Peak memory usage: 125 MB
% 44.03/7.09 % (2992262)Instructions burned: 825 (million)
% 44.03/7.09 % (2992243)Instruction limit reached!
% 44.03/7.09 % (2992243)------------------------------
% 44.03/7.09 % (2992243)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 44.03/7.09 % (2992243)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.03/7.09 % (2992243)CaDiCaL version: 2.1.3
% 44.03/7.09 % (2992243)Termination reason: Instruction limit
% 44.03/7.09 % (2992243)Termination phase: Saturation
% 44.03/7.09 % (2992243)Time elapsed: 2.005 s
% 45.21/7.25 % (2992243)Peak memory usage: 148 MB
% 45.21/7.25 % (2992243)Instructions burned: 3258 (million)
% 45.21/7.25 % (2992262)------------------------------
% 45.21/7.25 % (2992262)------------------------------
% 45.21/7.25 % (2992264)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=2692227031:i=1997:bd=preordered:av=off:gtg=all:gsp=on_2959 on theBenchmark for (2959ds/1997Mi)
% 45.21/7.25 % (2992265)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=63855792:i=2088:bd=preordered:av=off_2958 on theBenchmark for (2958ds/2088Mi)
% 45.21/7.25 % (2992265)Instruction limit reached!
% 45.21/7.25 % (2992265)------------------------------
% 45.21/7.25 % (2992265)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 45.21/7.25 % (2992265)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.21/7.25 % (2992265)CaDiCaL version: 2.1.3
% 45.21/7.25 % (2992265)Termination reason: Instruction limit
% 45.21/7.25 % (2992265)Termination phase: Saturation
% 45.21/7.25 % (2992265)Time elapsed: 0.752 s
% 45.21/7.25 % (2992265)Peak memory usage: 138 MB
% 45.21/7.25 % (2992265)Instructions burned: 2090 (million)
% 45.21/7.25 % (2992268)lrs+1010_64:1_anc=all:to=lpo:sil=16000:fde=none:sp=const_frequency:urr=full:sac=on:random_seed=407758539:i=1098:nicw=on_2949 on theBenchmark for (2949ds/1098Mi)
% 45.21/7.25 % (2992264)Instruction limit reached!
% 45.21/7.25 % (2992264)------------------------------
% 45.21/7.25 % (2992264)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 45.21/7.25 % (2992264)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.21/7.25 % (2992264)CaDiCaL version: 2.1.3
% 45.21/7.25 % (2992264)Termination reason: Instruction limit
% 45.21/7.25 % (2992264)Termination phase: Saturation
% 45.21/7.25 % (2992264)Time elapsed: 1.182 s
% 45.21/7.25 % (2992264)Peak memory usage: 138 MB
% 45.21/7.25 % (2992264)Instructions burned: 1999 (million)
% 45.21/7.25 % (2992268)Instruction limit reached!
% 45.21/7.25 % (2992268)------------------------------
% 45.21/7.25 % (2992268)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 45.21/7.25 % (2992268)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.21/7.25 % (2992268)CaDiCaL version: 2.1.3
% 45.21/7.25 % (2992268)Termination reason: Instruction limit
% 45.21/7.25 % (2992268)Termination phase: Saturation
% 45.21/7.25 % (2992268)Time elapsed: 0.326 s
% 45.21/7.25 % (2992268)Peak memory usage: 98 MB
% 45.21/7.25 % (2992268)Instructions burned: 1102 (million)
% 45.21/7.25 % (2992270)lrs-1011_32:1_to=lpo:sil=32000:tgt=ground:sos=on:spb=goal_then_units:acc=on:random_seed=1118877888:i=433:bd=preordered_2945 on theBenchmark for (2945ds/433Mi)
% 45.21/7.25 % (2992270)Refutation not found, incomplete strategy
% 45.21/7.25 % (2992270)------------------------------
% 45.21/7.25 % (2992270)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 45.21/7.25 % (2992270)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.21/7.25 % (2992270)CaDiCaL version: 2.1.3
% 45.21/7.25 % (2992270)Termination reason: Refutation not found, incomplete strategy
% 45.21/7.25 % (2992270)Time elapsed: 0.001 s
% 45.21/7.25 % (2992270)Peak memory usage: 87 MB
% 45.21/7.25 % (2992271)lrs+1002_1_ncem=casc2026/models/loop3.pt:sil=32000:npcc=on:prc=on:etr=on:spb=goal:flr=on:random_seed=3619820545:st=5.37:cond=on:i=2942:s2at=20:aac=none:fgj=on:bs=on:gtg=exists_sym:ss=axioms:er=filter:sgt=16_2944 on theBenchmark for (2944ds/2942Mi)
% 45.21/7.25 % (2992270)------------------------------
% 45.21/7.25 % (2992270)------------------------------
% 45.21/7.25 [W927 13:58:02.481876917 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 45.21/7.25 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 45.21/7.25 [W927 13:58:02.481911720 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 45.21/7.25 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 45.21/7.25 [W927 13:58:02.481933467 register_special_ops.cpp:225] Warning: Creating a tensor from 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.29/8.21 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 52.29/8.21 [W927 13:58:02.481940011 register_special_ops.cpp:225] Warning: Creating a tensor from 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.29/8.21 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 52.29/8.21 [W927 13:58:02.481954120 register_special_ops.cpp:225] Warning: Creating a tensor from 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.29/8.21 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 52.29/8.21 [W927 13:58:02.481960027 register_special_ops.cpp:225] Warning: Creating a tensor from 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.29/8.21 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 52.29/8.21 [W927 13:58:02.481973519 register_special_ops.cpp:225] Warning: Creating a tensor from 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.29/8.21 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 52.29/8.21 [W927 13:58:02.481989517 register_special_ops.cpp:225] Warning: Creating a tensor from 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.29/8.21 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 52.29/8.21 [W927 13:58:02.482010930 register_special_ops.cpp:225] Warning: Creating a tensor from 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.29/8.21 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 52.29/8.21 [W927 13:58:02.482017256 register_special_ops.cpp:225] Warning: Creating a tensor from 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.29/8.21 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 52.29/8.21 [W927 13:58:02.482031210 register_special_ops.cpp:225] Warning: Creating a tensor from 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.29/8.21 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 52.29/8.21 [W927 13:58:02.482037604 register_special_ops.cpp:225] Warning: Creating a tensor from 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.29/8.21 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 52.29/8.21 % (2992271)Refutation not found, incomplete strategy
% 52.29/8.21 % (2992271)------------------------------
% 52.29/8.21 % (2992271)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 52.29/8.21 % (2992271)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.29/8.21 % (2992271)CaDiCaL version: 2.1.3
% 52.29/8.21 % (2992271)Termination reason: Refutation not found, incomplete strategy
% 52.29/8.21 % (2992271)Time elapsed: 0.300 s
% 52.29/8.21 % (2992271)Peak memory usage: 126 MB
% 52.29/8.21 % (2992271)Instructions burned: 821 (million)
% 52.29/8.21 % (2992274)lrs+35_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=reverse_arity:urr=full:rp=on:br=off:random_seed=359368689:i=6922:s2at=5:sd=3:bd=all:ss=axioms:er=known:sgt=32_2941 on theBenchmark for (2941ds/6922Mi)
% 52.29/8.21 % (2992271)------------------------------
% 52.29/8.21 % (2992271)------------------------------
% 52.29/8.21 % (2992276)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=1434984447:s2a=on:i=596:s2at=2.3:gtgl=5:gtg=all:sup=off_2939 on theBenchmark for (2939ds/596Mi)
% 52.29/8.21 % (2992276)Refutation not found, incomplete strategy
% 58.19/9.04 % (2992276)------------------------------
% 58.19/9.04 % (2992276)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 58.19/9.04 % (2992276)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 58.19/9.04 % (2992276)CaDiCaL version: 2.1.3
% 58.19/9.04 % (2992276)Termination reason: Refutation not found, incomplete strategy
% 58.19/9.04 % (2992276)Time elapsed: 0.001 s
% 58.19/9.04 % (2992276)Peak memory usage: 88 MB
% 58.19/9.04 % (2992276)Instructions burned: 1 (million)
% 58.19/9.04 % (2992276)------------------------------
% 58.19/9.04 % (2992276)------------------------------
% 58.19/9.04 [W927 13:58:02.030596289 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 58.19/9.04 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 58.19/9.04 [W927 13:58:02.030642745 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 58.19/9.04 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 58.19/9.04 [W927 13:58:02.030681249 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 58.19/9.04 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 58.19/9.04 [W927 13:58:02.030699692 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 58.19/9.04 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 58.19/9.04 [W927 13:58:02.030725362 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 58.19/9.04 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 58.19/9.04 [W927 13:58:02.030737535 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 58.19/9.04 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 58.19/9.04 [W927 13:58:02.030762879 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 58.19/9.04 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 58.19/9.04 [W927 13:58:02.030786722 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 58.19/9.04 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 58.19/9.04 [W927 13:58:02.030813049 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 58.19/9.04 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 58.19/9.04 [W927 13:58:02.030823379 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 58.19/9.04 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 58.19/9.04 [W927 13:58:02.030851866 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 58.19/9.04 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 58.19/9.04 [W927 13:58:02.030862296 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 63.08/9.83 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 63.08/9.83 % (2992278)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=3318523152:i=4123:kws=inv_frequency:bd=preordered:av=off:er=known_2936 on theBenchmark for (2936ds/4123Mi)
% 63.08/9.83 % (2992274)Refutation not found, incomplete strategy
% 63.08/9.83 % (2992274)------------------------------
% 63.08/9.83 % (2992274)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 63.08/9.83 % (2992274)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 63.08/9.83 % (2992274)CaDiCaL version: 2.1.3
% 63.08/9.83 % (2992274)Termination reason: Refutation not found, incomplete strategy
% 63.08/9.83 % (2992274)Time elapsed: 0.554 s
% 63.08/9.83 % (2992274)Peak memory usage: 125 MB
% 63.08/9.83 % (2992274)Instructions burned: 825 (million)
% 63.08/9.83 % (2992274)------------------------------
% 63.08/9.83 % (2992274)------------------------------
% 63.08/9.83 % (2992280)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=341994309:i=16411:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2931 on theBenchmark for (2931ds/16411Mi)
% 63.08/9.83 [W927 13:58:03.990561876 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 63.08/9.83 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 63.08/9.83 [W927 13:58:03.990606296 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 63.08/9.83 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 63.08/9.83 [W927 13:58:03.990644336 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 63.08/9.83 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 63.08/9.83 [W927 13:58:03.990661639 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 63.08/9.83 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 63.08/9.83 [W927 13:58:03.990686423 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 63.08/9.83 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 63.08/9.83 [W927 13:58:03.990698033 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 63.08/9.83 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 63.08/9.83 [W927 13:58:03.990724250 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 63.08/9.83 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 63.08/9.83 [W927 13:58:03.990735610 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 63.08/9.83 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 63.08/9.83 [W927 13:58:03.990760600 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 63.08/9.83 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 66.46/10.25 [W927 13:58:03.990772053 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 66.46/10.25 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 66.46/10.25 [W927 13:58:03.990803050 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 66.46/10.25 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 66.46/10.25 [W927 13:58:03.990824740 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 66.46/10.25 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 66.46/10.25 % (2992280)Refutation not found, incomplete strategy
% 66.46/10.25 % (2992280)------------------------------
% 66.46/10.25 % (2992280)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 66.46/10.25 % (2992280)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 66.46/10.25 % (2992280)CaDiCaL version: 2.1.3
% 66.46/10.25 % (2992280)Termination reason: Refutation not found, incomplete strategy
% 66.46/10.25 % (2992280)Time elapsed: 0.541 s
% 66.46/10.25 % (2992280)Peak memory usage: 125 MB
% 66.46/10.25 % (2992280)Instructions burned: 825 (million)
% 66.46/10.25 % (2992280)------------------------------
% 66.46/10.25 % (2992280)------------------------------
% 66.46/10.25 % (2992278)Instruction limit reached!
% 66.46/10.25 % (2992278)------------------------------
% 66.46/10.25 % (2992278)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 66.46/10.25 % (2992278)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 66.46/10.25 % (2992278)CaDiCaL version: 2.1.3
% 66.46/10.25 % (2992278)Termination reason: Instruction limit
% 66.46/10.25 % (2992278)Termination phase: Saturation
% 66.46/10.25 % (2992278)Time elapsed: 1.342 s
% 66.46/10.25 % (2992278)Peak memory usage: 156 MB
% 66.46/10.25 % (2992278)Instructions burned: 4124 (million)
% 66.46/10.25 % (2992282)lrs+0_1_ncem=casc2026/models/loop1.pt:sil=8000:tgt=full:npcc=on:sp=reverse_frequency:gs=on:random_seed=1816702102:i=1670:kws=inv_precedence:bd=all:av=off:gtg=exists_all_2922 on theBenchmark for (2922ds/1670Mi)
% 66.46/10.25 % (2992283)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=228781424:st=3:cond=fast:i=1722:sd=2:ss=included:fsd=on_2921 on theBenchmark for (2921ds/1722Mi)
% 66.46/10.25 [W927 13:58:04.818431922 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 66.46/10.25 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 66.46/10.25 [W927 13:58:04.818468448 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 66.46/10.25 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 66.46/10.25 [W927 13:58:04.818490069 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 66.46/10.25 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 66.46/10.25 [W927 13:58:04.818496178 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 66.46/10.25 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 66.46/10.25 [W927 13:58:04.818509211 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 66.46/10.25 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 82.75/12.69 [W927 13:58:04.818514792 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 82.75/12.69 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 82.75/12.69 [W927 13:58:04.818536156 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 82.75/12.69 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 82.75/12.69 [W927 13:58:04.818541473 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 82.75/12.69 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 82.75/12.69 [W927 13:58:04.818554233 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 82.75/12.69 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 82.75/12.69 [W927 13:58:04.818559483 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 82.75/12.69 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 82.75/12.69 [W927 13:58:04.818572238 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 82.75/12.69 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 82.75/12.69 [W927 13:58:04.818577802 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 82.75/12.69 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 82.75/12.69 % (2992283)Refutation not found, incomplete strategy
% 82.75/12.69 % (2992283)------------------------------
% 82.75/12.69 % (2992283)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 82.75/12.69 % (2992283)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 82.75/12.69 % (2992283)CaDiCaL version: 2.1.3
% 82.75/12.69 % (2992283)Termination reason: Refutation not found, incomplete strategy
% 82.75/12.69 % (2992283)Time elapsed: 0.307 s
% 82.75/12.69 % (2992283)Peak memory usage: 125 MB
% 82.75/12.69 % (2992283)Instructions burned: 825 (million)
% 82.75/12.69 % (2992283)------------------------------
% 82.75/12.69 % (2992283)------------------------------
% 82.75/12.69 % (2992286)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=2180750994:cts=off:cond=on:i=9530:bs=on:fsd=on_2915 on theBenchmark for (2915ds/9530Mi)
% 82.75/12.69 % (2992250)Instruction limit reached!
% 82.75/12.69 % (2992250)------------------------------
% 82.75/12.69 % (2992250)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 82.75/12.69 % (2992250)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 82.75/12.69 % (2992250)CaDiCaL version: 2.1.3
% 82.75/12.69 % (2992250)Termination reason: Instruction limit
% 82.75/12.69 % (2992250)Termination phase: Saturation
% 82.75/12.69 % (2992250)Time elapsed: 6.391 s
% 82.75/12.69 % (2992250)Peak memory usage: 198 MB
% 82.75/12.69 % (2992250)Instructions burned: 10307 (million)
% 82.75/12.69 % (2992282)Instruction limit reached!
% 82.75/12.69 % (2992282)------------------------------
% 82.75/12.69 % (2992282)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 82.75/12.69 % (2992282)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 82.75/12.69 % (2992282)CaDiCaL version: 2.1.3
% 82.75/12.69 % (2992282)Termination reason: Instruction limit
% 82.75/12.69 % (2992282)Termination phase: Saturation
% 82.75/12.69 % (2992282)Time elapsed: 1.043 s
% 82.75/12.69 % (2992282)Peak memory usage: 135 MB
% 83.57/12.82 % (2992282)Instructions burned: 1670 (million)
% 83.57/12.82 % (2992288)lrs+10_1_ncem=casc2026/models/loop4.pt:sil=64000:npcc=on:sp=occurrence:random_seed=1131180321:st=2:i=4495:sd=10:ss=included_2911 on theBenchmark for (2911ds/4495Mi)
% 83.57/12.82 % (2992289)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=4173935787:cond=fast:i=4920:s2at=1.9:kws=inv_frequency:av=off:er=filter_2910 on theBenchmark for (2910ds/4920Mi)
% 83.57/12.82 [W927 13:58:05.026201840 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 83.57/12.82 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 83.57/12.82 [W927 13:58:05.026234263 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 83.57/12.82 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 83.57/12.82 [W927 13:58:05.026272400 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 83.57/12.82 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 83.57/12.82 [W927 13:58:05.026284837 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 83.57/12.82 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 83.57/12.82 [W927 13:58:05.026312033 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 83.57/12.82 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 83.57/12.82 [W927 13:58:05.026323777 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 83.57/12.82 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 83.57/12.82 [W927 13:58:05.026349600 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 83.57/12.82 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 83.57/12.82 [W927 13:58:05.026361010 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 83.57/12.82 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 83.57/12.82 [W927 13:58:05.026384730 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 83.57/12.82 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 83.57/12.82 [W927 13:58:05.026394843 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 83.57/12.82 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 83.57/12.82 [W927 13:58:05.026434437 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 83.57/12.82 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 83.57/12.82 [W927 13:58:05.026444680 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 88.20/13.36 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 88.20/13.36 % (2992288)Refutation not found, incomplete strategy
% 88.20/13.36 % (2992288)------------------------------
% 88.20/13.36 % (2992288)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 88.20/13.36 % (2992288)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 88.20/13.36 % (2992288)CaDiCaL version: 2.1.3
% 88.20/13.36 % (2992288)Termination reason: Refutation not found, incomplete strategy
% 88.20/13.36 % (2992288)Time elapsed: 0.543 s
% 88.20/13.36 % (2992288)Peak memory usage: 125 MB
% 88.20/13.36 % (2992288)Instructions burned: 824 (million)
% 88.20/13.36 % (2992288)------------------------------
% 88.20/13.36 % (2992288)------------------------------
% 88.20/13.36 % (2992292)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=55311311:cts=off:cond=on:i=2083:s2at=-1:fgj=on:av=off_2901 on theBenchmark for (2901ds/2083Mi)
% 88.20/13.36 % (2992254)Instruction limit reached!
% 88.20/13.36 % (2992254)------------------------------
% 88.20/13.36 % (2992254)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 88.20/13.36 % (2992254)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 88.20/13.36 % (2992254)CaDiCaL version: 2.1.3
% 88.20/13.36 % (2992254)Termination reason: Instruction limit
% 88.20/13.36 % (2992254)Termination phase: Saturation
% 88.20/13.36 % (2992254)Time elapsed: 7.836 s
% 88.20/13.36 % (2992254)Peak memory usage: 151 MB
% 88.20/13.36 % (2992254)Instructions burned: 8479 (million)
% 88.20/13.36 % (2992294)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=4291700853:i=4629:av=off:gsp=on_2893 on theBenchmark for (2893ds/4629Mi)
% 88.20/13.36 % (2992292)Instruction limit reached!
% 88.20/13.36 % (2992292)------------------------------
% 88.20/13.36 % (2992292)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 88.20/13.36 % (2992292)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 88.20/13.36 % (2992292)CaDiCaL version: 2.1.3
% 88.20/13.36 % (2992292)Termination reason: Instruction limit
% 88.20/13.36 % (2992292)Termination phase: Saturation
% 88.20/13.36 % (2992292)Time elapsed: 1.267 s
% 88.20/13.36 % (2992292)Peak memory usage: 140 MB
% 88.20/13.36 % (2992292)Instructions burned: 2084 (million)
% 88.20/13.36 % (2992294)Refutation not found, incomplete strategy
% 88.20/13.36 % (2992294)------------------------------
% 88.20/13.36 % (2992294)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 88.20/13.36 % (2992294)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 88.20/13.36 % (2992294)CaDiCaL version: 2.1.3
% 88.20/13.36 % (2992294)Termination reason: Refutation not found, incomplete strategy
% 88.20/13.36 % (2992294)Time elapsed: 0.556 s
% 88.20/13.36 % (2992294)Peak memory usage: 127 MB
% 88.20/13.36 % (2992294)Instructions burned: 829 (million)
% 88.20/13.36 % (2992296)dis+10_64_sil=16000:tgt=full:plsq=on:prc=on:drc=off:plsqc=2:plsqr=32,1:spb=goal:random_seed=4210353458:i=1258:av=off_2887 on theBenchmark for (2887ds/1258Mi)
% 88.20/13.36 % (2992286)Instruction limit reached!
% 88.20/13.36 % (2992286)------------------------------
% 88.20/13.36 % (2992286)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 88.20/13.36 % (2992286)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 88.20/13.36 % (2992286)CaDiCaL version: 2.1.3
% 88.20/13.36 % (2992286)Termination reason: Instruction limit
% 88.20/13.36 % (2992286)Termination phase: Saturation
% 88.20/13.36 % (2992286)Time elapsed: 2.952 s
% 88.20/13.36 % (2992286)Peak memory usage: 174 MB
% 88.20/13.36 % (2992286)Instructions burned: 9532 (million)
% 88.20/13.36 % (2992298)ott+1_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:fdtod=off:random_seed=1235047166:i=7343:av=off:ss=included_2884 on theBenchmark for (2884ds/7343Mi)
% 88.20/13.36 % (2992294)------------------------------
% 88.20/13.36 % (2992294)------------------------------
% 88.20/13.36 % (2992300)lrs-1002_1_to=lpo:sil=16000:sp=reverse_arity:sos=on:random_seed=4279233564:i=1325:sd=2:ss=axioms:sgt=16_2883 on theBenchmark for (2883ds/1325Mi)
% 88.20/13.36 % (2992300)Refutation not found, incomplete strategy
% 88.20/13.36 % (2992300)------------------------------
% 88.20/13.36 % (2992300)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 88.20/13.36 % (2992300)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 88.80/13.43 % (2992300)CaDiCaL version: 2.1.3
% 88.80/13.43 % (2992300)Termination reason: Refutation not found, incomplete strategy
% 88.80/13.43 % (2992300)Time elapsed: 0.001 s
% 88.80/13.43 % (2992300)Peak memory usage: 86 MB
% 88.80/13.43 [W927 13:58:08.492510129 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 88.80/13.43 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 88.80/13.43 [W927 13:58:08.492548669 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 88.80/13.43 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 88.80/13.43 [W927 13:58:08.492569949 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 88.80/13.43 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 88.80/13.43 [W927 13:58:08.492576781 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 88.80/13.43 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 88.80/13.43 [W927 13:58:08.492591372 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 88.80/13.43 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 88.80/13.43 [W927 13:58:08.492597501 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 88.80/13.43 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 88.80/13.43 [W927 13:58:08.492611172 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 88.80/13.43 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 88.80/13.43 [W927 13:58:08.492618221 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 88.80/13.43 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 88.80/13.43 [W927 13:58:08.492631279 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 88.80/13.43 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 88.80/13.43 [W927 13:58:08.492638128 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 88.80/13.43 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 88.80/13.43 [W927 13:58:08.492651256 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 88.80/13.43 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 88.80/13.43 [W927 13:58:08.492657836 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 88.80/13.43 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 88.80/13.43 % (2992296)Instruction limit reached!
% 88.80/13.43 % (2992296)------------------------------
% 88.80/13.43 % (2992296)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 93.60/14.06 % (2992296)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 93.60/14.06 % (2992296)CaDiCaL version: 2.1.3
% 93.60/14.06 % (2992296)Termination reason: Instruction limit
% 93.60/14.06 % (2992296)Termination phase: Saturation
% 93.60/14.06 % (2992296)Time elapsed: 0.530 s
% 93.60/14.06 % (2992296)Peak memory usage: 91 MB
% 93.60/14.06 % (2992296)Instructions burned: 1260 (million)
% 93.60/14.06 % (2992298)Refutation not found, incomplete strategy
% 93.60/14.06 % (2992298)------------------------------
% 93.60/14.06 % (2992298)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 93.60/14.06 % (2992298)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 93.60/14.06 % (2992298)CaDiCaL version: 2.1.3
% 93.60/14.06 % (2992298)Termination reason: Refutation not found, incomplete strategy
% 93.60/14.06 % (2992298)Time elapsed: 0.316 s
% 93.60/14.06 % (2992298)Peak memory usage: 125 MB
% 93.60/14.06 % (2992298)Instructions burned: 824 (million)
% 93.60/14.06 % (2992289)Instruction limit reached!
% 93.60/14.06 % (2992289)------------------------------
% 93.60/14.06 % (2992289)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 93.60/14.06 % (2992289)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 93.60/14.06 % (2992289)CaDiCaL version: 2.1.3
% 93.60/14.06 % (2992289)Termination reason: Instruction limit
% 93.60/14.06 % (2992289)Termination phase: Saturation
% 93.60/14.06 % (2992289)Time elapsed: 2.888 s
% 93.60/14.06 % (2992289)Peak memory usage: 161 MB
% 93.60/14.06 % (2992289)Instructions burned: 4921 (million)
% 93.60/14.06 % (2992300)------------------------------
% 93.60/14.06 % (2992300)------------------------------
% 93.60/14.06 % (2992302)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=820559371:st=3.9:cond=fast:i=2646:s2at=1.8:sd=5:amm=off:gtg=position:ss=axioms:fsd=on_2880 on theBenchmark for (2880ds/2646Mi)
% 93.60/14.06 % (2992298)------------------------------
% 93.60/14.06 % (2992298)------------------------------
% 93.60/14.06 % (2992303)dis-1003_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:sp=arity:sos=on:urr=on:random_seed=1271286958:i=1489:sd=2:ep=R:ss=axioms_2879 on theBenchmark for (2879ds/1489Mi)
% 93.60/14.06 % (2992304)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=1835840685:i=1503_2879 on theBenchmark for (2879ds/1503Mi)
% 93.60/14.06 % (2992307)lrs+10_1_ncem=casc2026/models/loop3.pt:sil=16000:tgt=ground:npcc=on:random_seed=2361143490:i=13942:kws=frequency_2878 on theBenchmark for (2878ds/13942Mi)
% 93.60/14.06 [W927 13:58:08.139675572 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 93.60/14.06 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 93.60/14.06 [W927 13:58:08.139719299 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 93.60/14.06 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 93.60/14.06 [W927 13:58:08.139756472 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 93.60/14.06 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 93.60/14.06 [W927 13:58:08.139767722 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 93.60/14.06 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 93.60/14.06 [W927 13:58:08.139794362 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 93.60/14.06 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 93.60/14.06 [W927 13:58:08.139805932 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 96.24/14.43 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 96.24/14.43 [W927 13:58:08.139831875 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 96.24/14.43 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 96.24/14.43 [W927 13:58:08.139842389 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 96.24/14.43 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 96.24/14.43 [W927 13:58:08.139866275 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 96.24/14.43 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 96.24/14.43 [W927 13:58:08.139877059 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 96.24/14.43 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 96.24/14.43 [W927 13:58:08.139900625 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 96.24/14.43 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 96.24/14.43 [W927 13:58:08.139910992 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 96.24/14.43 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 96.24/14.43 [W927 13:58:08.205030323 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 96.24/14.43 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 96.24/14.43 [W927 13:58:08.205130157 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 96.24/14.43 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 96.24/14.43 [W927 13:58:08.205173997 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 96.24/14.43 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 96.24/14.43 [W927 13:58:08.205186527 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 96.24/14.43 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 96.24/14.43 [W927 13:58:08.205215364 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 96.24/14.43 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 96.24/14.43 [W927 13:58:08.205226794 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 96.24/14.43 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 96.24/14.43 [W927 13:58:08.205252300 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 96.92/14.60 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 96.92/14.60 [W927 13:58:08.205263577 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 96.92/14.60 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 96.92/14.60 [W927 13:58:08.205294144 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 96.92/14.60 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 96.92/14.60 [W927 13:58:08.205304507 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 96.92/14.60 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 96.92/14.60 [W927 13:58:08.205329387 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 96.92/14.60 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 96.92/14.60 [W927 13:58:08.205339810 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 96.92/14.60 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 96.92/14.60 % (2992302)Refutation not found, incomplete strategy
% 96.92/14.60 % (2992302)------------------------------
% 96.92/14.60 % (2992302)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 96.92/14.60 % (2992302)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 96.92/14.60 % (2992302)CaDiCaL version: 2.1.3
% 96.92/14.60 % (2992302)Termination reason: Refutation not found, incomplete strategy
% 96.92/14.60 % (2992302)Time elapsed: 0.533 s
% 96.92/14.60 % (2992302)Peak memory usage: 125 MB
% 96.92/14.60 % (2992302)Instructions burned: 824 (million)
% 96.92/14.60 % (2992303)Refutation not found, incomplete strategy
% 96.92/14.60 % (2992303)------------------------------
% 96.92/14.60 % (2992303)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 96.92/14.60 % (2992303)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 96.92/14.60 % (2992303)CaDiCaL version: 2.1.3
% 96.92/14.60 % (2992303)Termination reason: Refutation not found, incomplete strategy
% 96.92/14.60 % (2992303)Time elapsed: 0.546 s
% 96.92/14.60 % (2992303)Peak memory usage: 125 MB
% 96.92/14.60 % (2992303)Instructions burned: 821 (million)
% 96.92/14.60 % (2992304)Refutation not found, incomplete strategy
% 96.92/14.60 % (2992304)------------------------------
% 96.92/14.60 % (2992304)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 96.92/14.60 % (2992304)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 96.92/14.60 % (2992304)CaDiCaL version: 2.1.3
% 96.92/14.60 % (2992304)Termination reason: Refutation not found, incomplete strategy
% 96.92/14.60 % (2992304)Time elapsed: 0.551 s
% 96.92/14.60 % (2992304)Peak memory usage: 127 MB
% 96.92/14.60 % (2992304)Instructions burned: 828 (million)
% 96.92/14.60 % (2992302)------------------------------
% 96.92/14.60 % (2992302)------------------------------
% 96.92/14.60 % (2992310)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=3085909706:i=3604:fsr=off:er=filter_2871 on theBenchmark for (2871ds/3604Mi)
% 96.92/14.60 % (2992303)------------------------------
% 96.92/14.60 % (2992303)------------------------------
% 96.92/14.60 % (2992304)------------------------------
% 96.92/14.60 % (2992304)------------------------------
% 96.92/14.60 % (2992312)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=32000:npcc=on:random_seed=3318427852:i=1876:sd=1:ss=included:sgt=32_2870 on theBenchmark for (2870ds/1876Mi)
% 96.92/14.60 % (2992313)lrs+10_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:fde=none:sp=arity:urr=on:br=off:random_seed=992431166:i=1932:bd=preordered:ins=10:sup=off:ss=axioms_2869 on theBenchmark for (2869ds/1932Mi)
% 104.04/15.58 [W927 13:58:09.180969163 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 104.04/15.58 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 104.04/15.58 [W927 13:58:09.181017183 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 104.04/15.58 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 104.04/15.58 [W927 13:58:09.181059626 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 104.04/15.58 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 104.04/15.58 [W927 13:58:09.181072536 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 104.04/15.58 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 104.04/15.58 [W927 13:58:09.181099099 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 104.04/15.58 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 104.04/15.58 [W927 13:58:09.181109839 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 104.04/15.58 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 104.04/15.58 [W927 13:58:09.181134229 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 104.04/15.58 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 104.04/15.58 [W927 13:58:09.181154879 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 104.04/15.58 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 104.04/15.58 [W927 13:58:09.181184613 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 104.04/15.58 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 104.04/15.58 [W927 13:58:09.181195029 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 104.04/15.58 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 104.04/15.58 [W927 13:58:09.181221189 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 104.04/15.58 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 104.04/15.58 [W927 13:58:09.181231496 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 104.04/15.58 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 104.04/15.58 [W927 13:58:09.209595923 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 130.37/19.30 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 130.37/19.30 [W927 13:58:09.209636756 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 130.37/19.30 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 130.37/19.30 [W927 13:58:09.209674160 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 130.37/19.30 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 130.37/19.30 [W927 13:58:09.209689953 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 130.37/19.30 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 130.37/19.30 [W927 13:58:09.209715070 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 130.37/19.30 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 130.37/19.30 [W927 13:58:09.209725126 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 130.37/19.30 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 130.37/19.30 [W927 13:58:09.209749573 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 130.37/19.30 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 130.37/19.30 [W927 13:58:09.209773926 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 130.37/19.30 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 130.37/19.30 [W927 13:58:09.209797926 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 130.37/19.30 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 130.37/19.30 [W927 13:58:09.209808493 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 130.37/19.30 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 130.37/19.30 [W927 13:58:09.209832056 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 130.37/19.30 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 130.37/19.30 [W927 13:58:09.209842536 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 130.37/19.30 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 130.37/19.30 % (2992312)Refutation not found, incomplete strategy
% 130.37/19.30 % (2992312)------------------------------
% 130.37/19.30 % (2992312)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 130.37/19.30 % (2992312)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 130.37/19.30 % (2992312)CaDiCaL version: 2.1.3
% 130.37/19.30 % (2992312)Termination reason: Refutation not found, incomplete strategy
% 130.37/19.30 % (2992312)Time elapsed: 0.550 s
% 130.37/19.30 % (2992312)Peak memory usage: 125 MB
% 130.37/19.30 % (2992312)Instructions burned: 821 (million)
% 130.37/19.30 % (2992313)Refutation not found, incomplete strategy
% 139.59/20.50 % (2992313)------------------------------
% 139.59/20.50 % (2992313)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 139.59/20.50 % (2992313)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 139.59/20.50 % (2992313)CaDiCaL version: 2.1.3
% 139.59/20.50 % (2992313)Termination reason: Refutation not found, incomplete strategy
% 139.59/20.50 % (2992313)Time elapsed: 0.542 s
% 139.59/20.50 % (2992313)Peak memory usage: 125 MB
% 139.59/20.50 % (2992313)Instructions burned: 821 (million)
% 139.59/20.50 % (2992312)------------------------------
% 139.59/20.50 % (2992312)------------------------------
% 139.59/20.50 % (2992313)------------------------------
% 139.59/20.50 % (2992313)------------------------------
% 139.59/20.50 % (2992310)Instruction limit reached!
% 139.59/20.50 % (2992310)------------------------------
% 139.59/20.50 % (2992310)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 139.59/20.50 % (2992310)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 139.59/20.50 % (2992310)CaDiCaL version: 2.1.3
% 139.59/20.50 % (2992310)Termination reason: Instruction limit
% 139.59/20.50 % (2992310)Termination phase: Saturation
% 139.59/20.50 % (2992310)Time elapsed: 1.067 s
% 139.59/20.50 % (2992310)Peak memory usage: 137 MB
% 139.59/20.50 % (2992310)Instructions burned: 3608 (million)
% 139.59/20.50 % (2992550)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=4169232173:s2pl=on:cond=fast:i=1980:s2at=2:kws=inv_precedence:doe=on:ins=1:av=off:gsp=on_2860 on theBenchmark for (2860ds/1980Mi)
% 139.59/20.50 % (2992551)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=666110845:i=3902:kws=inv_arity_squared:fgj=on:ss=axioms:sgt=11_2860 on theBenchmark for (2860ds/3902Mi)
% 139.59/20.50 % (2992552)dis+10_32_sil=16000:tgt=ground:drc=off:sas=cadical:acc=on:alpa=false:avsqc=3:random_seed=497002319:avsq=on:i=3916:aac=none:amm=off_2859 on theBenchmark for (2859ds/3916Mi)
% 139.59/20.50 [W927 13:58:10.354200234 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 139.59/20.50 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 139.59/20.50 [W927 13:58:10.354248714 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 139.59/20.50 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 139.59/20.50 [W927 13:58:10.354310324 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 139.59/20.50 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 139.59/20.50 [W927 13:58:10.354331878 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 139.59/20.50 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 139.59/20.50 [W927 13:58:10.354379781 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 139.59/20.50 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 139.59/20.50 [W927 13:58:10.354398801 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 139.59/20.50 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 139.59/20.50 [W927 13:58:10.354445491 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 139.59/20.50 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 139.59/20.50 [W927 13:58:10.354464968 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 73.11/21.70 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 73.11/21.70 [W927 13:58:10.354509838 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 73.11/21.70 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 73.11/21.70 [W927 13:58:10.354527138 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 73.11/21.70 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 73.11/21.70 [W927 13:58:10.354569411 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 73.11/21.70 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 73.11/21.70 [W927 13:58:10.354586674 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 73.11/21.70 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 73.11/21.70 % (2992551)Refutation not found, incomplete strategy
% 73.11/21.70 % (2992551)------------------------------
% 73.11/21.70 % (2992551)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 73.11/21.70 % (2992551)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 73.11/21.70 % (2992551)CaDiCaL version: 2.1.3
% 73.11/21.70 % (2992551)Termination reason: Refutation not found, incomplete strategy
% 73.11/21.70 % (2992551)Time elapsed: 0.877 s
% 73.11/21.70 % (2992551)Peak memory usage: 125 MB
% 73.11/21.70 % (2992551)Instructions burned: 824 (million)
% 73.11/21.70 % (2992551)------------------------------
% 73.11/21.70 % (2992551)------------------------------
% 73.11/21.70 % (2992587)dis+10_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=full:npcc=on:drc=ordering:lcm=predicate:random_seed=252847118:cond=on:i=3940:av=off:er=known_2845 on theBenchmark for (2845ds/3940Mi)
% 73.11/21.70 % (2992552)Instruction limit reached!
% 73.11/21.70 % (2992552)------------------------------
% 73.11/21.70 % (2992552)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 73.11/21.70 % (2992552)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 73.11/21.70 % (2992552)CaDiCaL version: 2.1.3
% 73.11/21.70 % (2992552)Termination reason: Instruction limit
% 73.11/21.70 % (2992552)Termination phase: Saturation
% 73.11/21.70 % (2992552)Time elapsed: 1.795 s
% 73.11/21.70 % (2992552)Peak memory usage: 113 MB
% 73.11/21.70 % (2992552)Instructions burned: 3917 (million)
% 73.11/21.70 % (2992550)Instruction limit reached!
% 73.11/21.70 % (2992550)------------------------------
% 73.11/21.70 % (2992550)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 73.11/21.70 % (2992550)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 73.11/21.70 % (2992550)CaDiCaL version: 2.1.3
% 73.11/21.70 % (2992550)Termination reason: Instruction limit
% 73.11/21.70 % (2992550)Termination phase: Saturation
% 73.11/21.70 % (2992550)Time elapsed: 2.041 s
% 73.11/21.70 % (2992550)Peak memory usage: 138 MB
% 73.11/21.70 % (2992550)Instructions burned: 1980 (million)
% 73.11/21.70 % (2992589)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=reverse_frequency:bce=on:random_seed=3060402402:s2pl=on:i=3980:gtgl=3:kws=precedence:fgj=on:gtg=all_2840 on theBenchmark for (2840ds/3980Mi)
% 73.11/21.70 % (2992590)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=1875786534:i=2087:s2at=3:kws=frequency:av=off:fsr=off_2838 on theBenchmark for (2838ds/2087Mi)
% 73.11/21.70 % (2992589)Instruction limit reached!
% 73.11/21.70 % (2992589)------------------------------
% 73.11/21.70 % (2992589)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 73.11/21.70 % (2992589)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.18/21.90 % (2992589)CaDiCaL version: 2.1.3
% 0.18/21.90 % (2992589)Termination reason: Instruction limit
% 0.18/21.90 % (2992589)Termination phase: Saturation
% 0.18/21.90 % (2992589)Time elapsed: 2.259 s
% 0.18/21.90 % (2992589)Peak memory usage: 158 MB
% 0.18/21.90 % (2992589)Instructions burned: 3983 (million)
% 0.18/21.90 % (2992593)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=382931891:cts=off:cond=on:i=4272:bs=on:fsd=on_2815 on theBenchmark for (2815ds/4272Mi)
% 0.18/21.90 % (2992590)Instruction limit reached!
% 0.18/21.90 % (2992590)------------------------------
% 0.18/21.90 % (2992590)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.18/21.90 % (2992590)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.18/21.90 % (2992590)CaDiCaL version: 2.1.3
% 0.18/21.90 % (2992590)Termination reason: Instruction limit
% 0.18/21.90 % (2992590)Termination phase: Saturation
% 0.18/21.90 % (2992590)Time elapsed: 2.244 s
% 0.18/21.90 % (2992590)Peak memory usage: 141 MB
% 0.18/21.90 % (2992590)Instructions burned: 2087 (million)
% 0.18/21.90 % (2992595)lrs-30_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:urr=on:bce=on:rp=on:br=off:flr=on:random_seed=2767662912:st=-1:i=2197:kws=precedence:av=off:ss=axioms:er=known_2812 on theBenchmark for (2812ds/2197Mi)
% 0.18/21.90 [W927 13:58:15.276076766 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 0.18/21.90 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 0.18/21.90 [W927 13:58:15.276136383 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 0.18/21.90 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 0.18/21.90 [W927 13:58:15.276199579 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 0.18/21.90 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 0.18/21.90 [W927 13:58:15.276218243 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 0.18/21.90 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 0.18/21.90 [W927 13:58:15.276262519 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 0.18/21.90 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 0.18/21.90 [W927 13:58:15.276280026 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 0.18/21.90 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 0.18/21.90 [W927 13:58:15.276323786 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 0.18/21.90 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 0.18/21.90 [W927 13:58:15.276341193 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 0.18/21.90 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 0.18/21.90 [W927 13:58:15.276383626 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 0.18/21.90 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 0.18/21.90 [W927 13:58:15.276401296 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 0.18/21.90 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 0.18/21.90 [W927 13:58:15.276445040 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 0.18/21.90 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 0.18/21.90 [W927 13:58:15.276462823 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 0.18/21.90 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 0.18/21.90 % (2992587)Instruction limit reached!
% 0.18/21.90 % (2992587)------------------------------
% 0.18/21.90 % (2992587)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.18/21.90 % (2992587)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.18/21.90 % (2992587)CaDiCaL version: 2.1.3
% 0.18/21.90 % (2992587)Termination reason: Instruction limit
% 0.18/21.90 % (2992587)Termination phase: Saturation
% 0.18/21.90 % (2992587)Time elapsed: 3.972 s
% 0.18/21.90 % (2992587)Peak memory usage: 157 MB
% 0.18/21.90 % (2992587)Instructions burned: 3940 (million)
% 0.18/21.90 % (2992595)Refutation not found, incomplete strategy
% 0.18/21.90 % (2992595)------------------------------
% 0.18/21.90 % (2992595)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.18/21.90 % (2992595)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.18/21.90 % (2992595)CaDiCaL version: 2.1.3
% 0.18/21.90 % (2992595)Termination reason: Refutation not found, incomplete strategy
% 0.18/21.90 % (2992595)Time elapsed: 0.907 s
% 0.18/21.90 % (2992595)Peak memory usage: 125 MB
% 0.18/21.90 % (2992595)Instructions burned: 825 (million)
% 0.18/21.90 % (2992597)dis+21_1_sil=8000:spb=goal_then_units:random_seed=327860976:avsq=on:i=6508:avsqr=1,16:kws=arity_squared:fgj=on_2802 on theBenchmark for (2802ds/6508Mi)
% 0.18/21.90 % (2992595)------------------------------
% 0.18/21.90 % (2992595)------------------------------
% 0.18/21.90 % (2992597)First to succeed.
% 0.18/21.90 % (2992597)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-2991932"
% 0.18/21.90 % (2992599)dis-1002_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=occurrence:random_seed=402008824:i=2330:fgj=on:av=off:fsr=off_2796 on theBenchmark for (2796ds/2330Mi)
% 0.18/21.90 % SZS status Satisfiable for theBenchmark
% 0.18/21.90 % SZS output start Saturation.
% See solution above
% 0.18/21.90 % SZS output start Definitions and Model Updates.
% 0.18/21.90 % SZS output end Definitions and Model Updates.
% 0.18/21.90 % (2992597)------------------------------
% 0.18/21.90 % (2992597)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.18/21.90 % (2992597)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.18/21.90 % (2992597)CaDiCaL version: 2.1.3
% 0.18/21.90 % (2992597)Termination reason: Satisfiable
% 0.18/21.90 % (2992597)Time elapsed: 0.310 s
% 0.18/21.90 % (2992597)Peak memory usage: 90 MB
% 0.18/21.90 % (2992597)Instructions burned: 342 (million)
% 0.18/21.90 % (2992597)------------------------------
% 0.18/21.90 % (2992597)------------------------------
% 0.18/21.90 % (2991932)Success in time 20.831 s
% 0.18/21.90 % Vampire exiting
%------------------------------------------------------------------------------