%------------------------------------------------------------------------------ % File : Vampire---5.0.1 % Problem : SWV420-1.045 : TPTP v9.3.1. Released v3.5.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % Computer : n015.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 29 01:10:36 PM UTC 2026 % Result : Timeout 300.12s 43.08s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : SWV420-1.045 : TPTP v9.3.1. Released v3.5.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.07/0.17 % Computer : n015.cluster.edu % 0.07/0.17 % Model : x86_64 x86_64 % 0.07/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.07/0.17 % Memory : 8046.5625MB % 0.07/0.17 % OS : Linux 6.8.0-71-generic % 0.07/0.17 % CPULimit : 300 % 0.07/0.17 % WCLimit : 300 % 0.07/0.17 % DateTime : Mon Sep 28 11:00:47 UTC 2026 % 0.07/0.18 % CPUTime : % 0.07/0.18 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.07/0.21 Running first-order theorem proving % 0.07/0.21 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.19/1.80 % (2544728)Input is clausal, will run a generic CNF schedule. % 8.19/1.80 % (2544738)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3026925974:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi) % 8.19/1.80 % (2544736)lrs+10_1_sil=8000:sp=occurrence:random_seed=2597603959:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi) % 8.19/1.80 % (2544734)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=3745466667:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi) % 8.19/1.80 % (2544733)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=2817208361:i=140167_2999 on theBenchmark for (2999ds/140167Mi) % 8.19/1.80 % (2544735)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=152650003:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi) % 8.19/1.80 % (2544739)dis-21_1_sil=8000:lcm=predicate:random_seed=1329009458: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.19/1.80 % (2544737)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=4063811319:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi) % 8.19/1.80 % (2544737)Refutation not found, incomplete strategy % 8.19/1.80 % (2544737)------------------------------ % 8.19/1.80 % (2544737)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.19/1.80 % (2544737)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.19/1.80 % (2544737)CaDiCaL version: 2.1.3 % 8.19/1.80 % (2544737)Termination reason: Refutation not found, incomplete strategy % 8.19/1.80 % (2544737)Time elapsed: 0.015 s % 8.19/1.80 % (2544737)Peak memory usage: 88 MB % 8.19/1.80 % (2544737)Instructions burned: 25 (million) % 8.19/1.80 % (2544738)Instruction limit reached! % 8.19/1.80 % (2544738)------------------------------ % 8.19/1.80 % (2544738)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.19/1.80 % (2544738)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.19/1.80 % (2544738)CaDiCaL version: 2.1.3 % 8.19/1.80 % (2544738)Termination reason: Instruction limit % 8.19/1.80 % (2544738)Termination phase: Saturation % 8.19/1.80 % (2544738)Time elapsed: 0.057 s % 8.19/1.80 % (2544738)Peak memory usage: 90 MB % 8.19/1.80 % (2544738)Instructions burned: 181 (million) % 8.19/1.80 % (2544736)Instruction limit reached! % 8.19/1.80 % (2544736)------------------------------ % 8.19/1.80 % (2544736)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.19/1.80 % (2544736)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.19/1.80 % (2544736)CaDiCaL version: 2.1.3 % 8.19/1.80 % (2544736)Termination reason: Instruction limit % 8.19/1.80 % (2544736)Termination phase: Saturation % 8.19/1.80 % (2544736)Time elapsed: 0.057 s % 8.19/1.80 % (2544736)Peak memory usage: 90 MB % 8.19/1.80 % (2544736)Instructions burned: 108 (million) % 8.19/1.80 % (2544739)Instruction limit reached! % 8.19/1.80 % (2544739)------------------------------ % 8.19/1.80 % (2544739)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.19/1.80 % (2544739)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.19/1.80 % (2544739)CaDiCaL version: 2.1.3 % 8.19/1.80 % (2544739)Termination reason: Instruction limit % 8.19/1.80 % (2544739)Termination phase: Saturation % 8.19/1.80 % (2544739)Time elapsed: 0.061 s % 8.19/1.80 % (2544739)Peak memory usage: 88 MB % 8.19/1.80 % (2544739)Instructions burned: 118 (million) % 8.19/1.80 % (2544747)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=2858254286:i=143:sd=2:aac=none:ss=axioms:sgt=16_2998 on theBenchmark for (2998ds/143Mi) % 8.19/1.80 % (2544747)Refutation not found, incomplete strategy % 8.19/1.80 % (2544747)------------------------------ % 8.19/1.80 % (2544747)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.19/1.80 % (2544747)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.19/1.80 % (2544747)CaDiCaL version: 2.1.3 % 8.19/1.80 % (2544747)Termination reason: Refutation not found, incomplete strategy % 8.19/1.80 % (2544747)Time elapsed: 0.003 s % 8.19/1.80 % (2544747)Peak memory usage: 88 MB % 8.19/1.80 % (2544747)Instructions burned: 9 (million) % 8.19/1.80 % (2544749)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=285941210:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi) % 13.19/2.38 % (2544748)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=257536654: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) % 13.19/2.38 % (2544748)Refutation not found, incomplete strategy % 13.19/2.38 % (2544748)------------------------------ % 13.19/2.38 % (2544748)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.19/2.38 % (2544748)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.19/2.38 % (2544748)CaDiCaL version: 2.1.3 % 13.19/2.38 % (2544748)Termination reason: Refutation not found, incomplete strategy % 13.19/2.38 % (2544748)Time elapsed: 0.011 s % 13.19/2.38 % (2544748)Peak memory usage: 88 MB % 13.19/2.38 % (2544748)Instructions burned: 22 (million) % 13.19/2.38 % (2544749)Refutation not found, incomplete strategy % 13.19/2.38 % (2544749)------------------------------ % 13.19/2.38 % (2544749)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.19/2.38 % (2544749)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.19/2.38 % (2544749)CaDiCaL version: 2.1.3 % 13.19/2.38 % (2544749)Termination reason: Refutation not found, incomplete strategy % 13.19/2.38 % (2544749)Time elapsed: 0.012 s % 13.19/2.38 % (2544749)Peak memory usage: 89 MB % 13.19/2.38 % (2544749)Instructions burned: 23 (million) % 13.19/2.38 % (2544737)------------------------------ % 13.19/2.38 % (2544737)------------------------------ % 13.19/2.38 % (2544747)------------------------------ % 13.19/2.38 % (2544747)------------------------------ % 13.19/2.38 % (2544753)lrs+10_64_to=lpo:sil=8000:random_seed=1791030309:i=126:bd=preordered_2995 on theBenchmark for (2995ds/126Mi) % 13.19/2.38 % (2544754)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=3555270286:avsq=on:i=194:fgj=on:bd=preordered_2995 on theBenchmark for (2995ds/194Mi) % 13.19/2.38 % (2544749)------------------------------ % 13.19/2.38 % (2544749)------------------------------ % 13.19/2.38 % (2544748)------------------------------ % 13.19/2.38 % (2544748)------------------------------ % 13.19/2.38 % (2544753)Instruction limit reached! % 13.19/2.38 % (2544753)------------------------------ % 13.19/2.38 % (2544753)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.19/2.38 % (2544753)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.19/2.38 % (2544753)CaDiCaL version: 2.1.3 % 13.19/2.38 % (2544753)Termination reason: Instruction limit % 13.19/2.38 % (2544753)Termination phase: Saturation % 13.19/2.38 % (2544753)Time elapsed: 0.071 s % 13.19/2.38 % (2544753)Peak memory usage: 90 MB % 13.19/2.38 % (2544753)Instructions burned: 127 (million) % 13.19/2.38 % (2544754)Instruction limit reached! % 13.19/2.38 % (2544754)------------------------------ % 13.19/2.38 % (2544754)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.19/2.38 % (2544754)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.19/2.38 % (2544754)CaDiCaL version: 2.1.3 % 13.19/2.38 % (2544754)Termination reason: Instruction limit % 13.19/2.38 % (2544754)Termination phase: Saturation % 13.19/2.38 % (2544754)Time elapsed: 0.066 s % 13.19/2.38 % (2544754)Peak memory usage: 90 MB % 13.19/2.38 % (2544754)Instructions burned: 196 (million) % 13.19/2.38 % (2544760)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=2944573254:i=107_2993 on theBenchmark for (2993ds/107Mi) % 13.19/2.38 % (2544758)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=4029663105:i=3394:sd=4:ss=included:sgt=64_2994 on theBenchmark for (2994ds/3394Mi) % 13.19/2.38 % (2544757)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=3074061645:i=157:gtg=all_2994 on theBenchmark for (2994ds/157Mi) % 13.19/2.38 % (2544759)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=464756299:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2993 on theBenchmark for (2993ds/106Mi) % 13.19/2.38 % (2544760)Refutation not found, incomplete strategy % 13.19/2.38 % (2544760)------------------------------ % 13.19/2.38 % (2544760)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.19/2.38 % (2544760)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.19/2.38 % (2544760)CaDiCaL version: 2.1.3 % 13.19/2.38 % (2544760)Termination reason: Refutation not found, incomplete strategy % 21.10/3.49 % (2544760)Time elapsed: 0.020 s % 21.10/3.49 % (2544760)Peak memory usage: 90 MB % 21.10/3.49 % (2544760)Instructions burned: 67 (million) % 21.10/3.49 % (2544759)Refutation not found, incomplete strategy % 21.10/3.49 % (2544759)------------------------------ % 21.10/3.49 % (2544759)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 21.10/3.49 % (2544759)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.10/3.49 % (2544759)CaDiCaL version: 2.1.3 % 21.10/3.49 % (2544759)Termination reason: Refutation not found, incomplete strategy % 21.10/3.49 % (2544759)Time elapsed: 0.014 s % 21.10/3.49 % (2544759)Peak memory usage: 89 MB % 21.10/3.49 % (2544759)Instructions burned: 27 (million) % 21.10/3.49 % (2544757)Instruction limit reached! % 21.10/3.49 % (2544757)------------------------------ % 21.10/3.49 % (2544757)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 21.10/3.49 % (2544757)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.10/3.49 % (2544757)CaDiCaL version: 2.1.3 % 21.10/3.49 % (2544757)Termination reason: Instruction limit % 21.10/3.49 % (2544757)Termination phase: Saturation % 21.10/3.49 % (2544757)Time elapsed: 0.106 s % 21.10/3.49 % (2544757)Peak memory usage: 91 MB % 21.10/3.49 % (2544757)Instructions burned: 194 (million) % 21.10/3.49 % (2544760)------------------------------ % 21.10/3.49 % (2544760)------------------------------ % 21.10/3.49 % (2544734)Refutation not found, incomplete strategy % 21.10/3.49 % (2544734)------------------------------ % 21.10/3.49 % (2544734)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 21.10/3.49 % (2544734)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.10/3.49 % (2544734)CaDiCaL version: 2.1.3 % 21.10/3.49 % (2544734)Termination reason: Refutation not found, incomplete strategy % 21.10/3.49 % (2544734)Time elapsed: 0.743 s % 21.10/3.49 % (2544734)Peak memory usage: 131 MB % 21.10/3.49 % (2544734)Instructions burned: 1113 (million) % 21.10/3.49 % (2544766)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=3078591735:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2991 on theBenchmark for (2991ds/242Mi) % 21.10/3.49 % (2544759)------------------------------ % 21.10/3.49 % (2544759)------------------------------ % 21.10/3.49 % (2544767)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=2195482374:cond=fast:i=5208:av=off_2991 on theBenchmark for (2991ds/5208Mi) % 21.10/3.49 % (2544766)Instruction limit reached! % 21.10/3.49 % (2544766)------------------------------ % 21.10/3.49 % (2544766)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 21.10/3.49 % (2544766)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.10/3.49 % (2544766)CaDiCaL version: 2.1.3 % 21.10/3.49 % (2544766)Termination reason: Instruction limit % 21.10/3.49 % (2544766)Termination phase: Saturation % 21.10/3.49 % (2544766)Time elapsed: 0.122 s % 21.10/3.49 % (2544766)Peak memory usage: 90 MB % 21.10/3.49 % (2544766)Instructions burned: 242 (million) % 21.10/3.49 % (2544770)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=3965498713:i=134:sd=2:doe=on:ss=axioms:sgt=14_2990 on theBenchmark for (2990ds/134Mi) % 21.10/3.49 % (2544770)Refutation not found, incomplete strategy % 21.10/3.49 % (2544770)------------------------------ % 21.10/3.49 % (2544770)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 21.10/3.49 % (2544770)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.10/3.49 % (2544770)CaDiCaL version: 2.1.3 % 21.10/3.49 % (2544770)Termination reason: Refutation not found, incomplete strategy % 21.10/3.49 % (2544770)Time elapsed: 0.013 s % 21.10/3.49 % (2544770)Peak memory usage: 89 MB % 21.10/3.49 % (2544770)Instructions burned: 22 (million) % 21.10/3.49 % (2544734)------------------------------ % 21.10/3.49 % (2544734)------------------------------ % 21.10/3.49 % (2544771)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=2379762553:i=499:bd=all_2988 on theBenchmark for (2988ds/499Mi) % 21.10/3.49 % (2544773)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=3471728150:i=191:fgj=on:bd=all_2988 on theBenchmark for (2988ds/191Mi) % 21.10/3.49 % (2544770)------------------------------ % 21.10/3.49 % (2544770)------------------------------ % 21.10/3.49 % (2544773)Instruction limit reached! % 21.10/3.49 % (2544773)------------------------------ % 21.10/3.49 % (2544773)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 31.77/5.01 % (2544773)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.77/5.01 % (2544773)CaDiCaL version: 2.1.3 % 31.77/5.01 % (2544773)Termination reason: Instruction limit % 31.77/5.01 % (2544773)Termination phase: Saturation % 31.77/5.01 % (2544773)Time elapsed: 0.104 s % 31.77/5.01 % (2544773)Peak memory usage: 92 MB % 31.77/5.01 % (2544773)Instructions burned: 192 (million) % 31.77/5.01 % (2544777)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=42205732:cond=on:i=156:bs=on:gtg=exists_all:er=known_2986 on theBenchmark for (2986ds/156Mi) % 31.77/5.01 % (2544776)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=4183614916:i=264:kws=precedence:fsr=off_2986 on theBenchmark for (2986ds/264Mi) % 31.77/5.01 % (2544771)Instruction limit reached! % 31.77/5.01 % (2544771)------------------------------ % 31.77/5.01 % (2544771)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 31.77/5.01 % (2544771)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.77/5.01 % (2544771)CaDiCaL version: 2.1.3 % 31.77/5.01 % (2544771)Termination reason: Instruction limit % 31.77/5.01 % (2544771)Termination phase: Saturation % 31.77/5.01 % (2544771)Time elapsed: 0.269 s % 31.77/5.01 % (2544771)Peak memory usage: 96 MB % 31.77/5.01 % (2544771)Instructions burned: 500 (million) % 31.77/5.01 % (2544777)Instruction limit reached! % 31.77/5.01 % (2544777)------------------------------ % 31.77/5.01 % (2544777)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 31.77/5.01 % (2544777)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.77/5.01 % (2544777)CaDiCaL version: 2.1.3 % 31.77/5.01 % (2544777)Termination reason: Instruction limit % 31.77/5.01 % (2544777)Termination phase: Saturation % 31.77/5.01 % (2544777)Time elapsed: 0.081 s % 31.77/5.01 % (2544777)Peak memory usage: 89 MB % 31.77/5.01 % (2544777)Instructions burned: 156 (million) % 31.77/5.01 % (2544776)Instruction limit reached! % 31.77/5.01 % (2544776)------------------------------ % 31.77/5.01 % (2544776)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 31.77/5.01 % (2544776)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.77/5.01 % (2544776)CaDiCaL version: 2.1.3 % 31.77/5.01 % (2544776)Termination reason: Instruction limit % 31.77/5.01 % (2544776)Termination phase: Saturation % 31.77/5.01 % (2544776)Time elapsed: 0.121 s % 31.77/5.01 % (2544776)Peak memory usage: 91 MB % 31.77/5.01 % (2544776)Instructions burned: 265 (million) % 31.77/5.01 % (2544780)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=1406997120:i=3256:kws=precedence:bd=preordered:av=off_2984 on theBenchmark for (2984ds/3256Mi) % 31.77/5.01 % (2544781)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=2946178229:i=537:av=off:ss=included_2984 on theBenchmark for (2984ds/537Mi) % 31.77/5.01 % (2544782)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=3943683350:i=180:bd=preordered:av=off_2983 on theBenchmark for (2983ds/180Mi) % 31.77/5.01 % (2544782)Instruction limit reached! % 31.77/5.01 % (2544782)------------------------------ % 31.77/5.01 % (2544782)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 31.77/5.01 % (2544782)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.77/5.01 % (2544782)CaDiCaL version: 2.1.3 % 31.77/5.01 % (2544782)Termination reason: Instruction limit % 31.77/5.01 % (2544782)Termination phase: Saturation % 31.77/5.01 % (2544782)Time elapsed: 0.088 s % 31.77/5.01 % (2544782)Peak memory usage: 90 MB % 31.77/5.01 % (2544782)Instructions burned: 180 (million) % 31.77/5.01 % (2544781)Instruction limit reached! % 31.77/5.01 % (2544781)------------------------------ % 31.77/5.01 % (2544781)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 31.77/5.01 % (2544781)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.77/5.01 % (2544781)CaDiCaL version: 2.1.3 % 31.77/5.01 % (2544781)Termination reason: Instruction limit % 31.77/5.01 % (2544781)Termination phase: Saturation % 31.77/5.01 % (2544781)Time elapsed: 0.211 s % 31.77/5.01 % (2544781)Peak memory usage: 88 MB % 31.77/5.01 % (2544781)Instructions burned: 539 (million) % 31.77/5.01 % (2544786)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=133139352:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2981 on theBenchmark for (2981ds/10307Mi) % 41.14/6.30 % (2544787)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=506903351:i=412:gtgl=4:gtg=exists_all_2980 on theBenchmark for (2980ds/412Mi) % 41.14/6.30 % (2544787)Instruction limit reached! % 41.14/6.30 % (2544787)------------------------------ % 41.14/6.30 % (2544787)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 41.14/6.30 % (2544787)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 41.14/6.30 % (2544787)CaDiCaL version: 2.1.3 % 41.14/6.30 % (2544787)Termination reason: Instruction limit % 41.14/6.30 % (2544787)Termination phase: Saturation % 41.14/6.30 % (2544787)Time elapsed: 0.178 s % 41.14/6.30 % (2544787)Peak memory usage: 91 MB % 41.14/6.30 % (2544787)Instructions burned: 414 (million) % 41.14/6.30 % (2544790)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=2842560298:s2pl=no:i=8478:s2at=4:nm=6_2977 on theBenchmark for (2977ds/8478Mi) % 41.14/6.30 % (2544767)Instruction limit reached! % 41.14/6.30 % (2544767)------------------------------ % 41.14/6.30 % (2544767)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 41.14/6.30 % (2544767)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 41.14/6.30 % (2544767)CaDiCaL version: 2.1.3 % 41.14/6.30 % (2544767)Termination reason: Instruction limit % 41.14/6.30 % (2544767)Termination phase: Saturation % 41.14/6.30 % (2544767)Time elapsed: 1.653 s % 41.14/6.30 % (2544767)Peak memory usage: 150 MB % 41.14/6.30 % (2544767)Instructions burned: 5209 (million) % 41.14/6.30 % (2544792)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=3915206579:s2a=on:i=303:s2at=2:sd=1:kws=inv_arity:bs=on:ins=10:fdi=1024:sup=off:ss=included_2973 on theBenchmark for (2973ds/303Mi) % 41.14/6.30 % (2544792)Instruction limit reached! % 41.14/6.30 % (2544792)------------------------------ % 41.14/6.30 % (2544792)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 41.14/6.30 % (2544792)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 41.14/6.30 % (2544792)CaDiCaL version: 2.1.3 % 41.14/6.30 % (2544792)Termination reason: Instruction limit % 41.14/6.30 % (2544792)Termination phase: Saturation % 41.14/6.30 % (2544792)Time elapsed: 0.124 s % 41.14/6.30 % (2544792)Peak memory usage: 92 MB % 41.14/6.30 % (2544792)Instructions burned: 303 (million) % 41.14/6.30 % (2544758)Instruction limit reached! % 41.14/6.30 % (2544758)------------------------------ % 41.14/6.30 % (2544758)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 41.14/6.30 % (2544758)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 41.14/6.30 % (2544758)CaDiCaL version: 2.1.3 % 41.14/6.30 % (2544758)Termination reason: Instruction limit % 41.14/6.30 % (2544758)Termination phase: Saturation % 41.14/6.30 % (2544758)Time elapsed: 2.157 s % 41.14/6.30 % (2544758)Peak memory usage: 150 MB % 41.14/6.30 % (2544758)Instructions burned: 3394 (million) % 41.14/6.30 % (2544794)lrs+10_1_to=lpo:sil=16000:fde=none:sos=on:urr=on:bsr=on:random_seed=1746572770:st=4:i=720:sd=3:fsr=off:ss=axioms_2971 on theBenchmark for (2971ds/720Mi) % 41.14/6.30 % (2544795)lrs-20_1_to=lpo:sil=32000:tgt=ground:sp=reverse_frequency:spb=goal:urr=on:bsr=unit_only:nwc=1.5:random_seed=236550476:i=598:bs=on:bd=preordered:av=off:ss=axioms_2971 on theBenchmark for (2971ds/598Mi) % 41.14/6.30 % (2544795)Refutation not found, incomplete strategy % 41.14/6.30 % (2544795)------------------------------ % 41.14/6.30 % (2544795)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 41.14/6.30 % (2544795)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 41.14/6.30 % (2544795)CaDiCaL version: 2.1.3 % 41.14/6.30 % (2544795)Termination reason: Refutation not found, incomplete strategy % 41.14/6.30 % (2544795)Time elapsed: 0.002 s % 41.14/6.30 % (2544795)Peak memory usage: 88 MB % 41.14/6.30 % (2544795)Instructions burned: 3 (million) % 41.14/6.30 % (2544794)Refutation not found, incomplete strategy % 41.14/6.30 % (2544794)------------------------------ % 41.14/6.30 % (2544794)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 41.14/6.30 % (2544794)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 41.14/6.30 % (2544794)CaDiCaL version: 2.1.3 % 41.14/6.30 % (2544794)Termination reason: Refutation not found, incomplete strategy % 71.65/10.92 % (2544794)Time elapsed: 0.122 s % 71.65/10.92 % (2544794)Peak memory usage: 94 MB % 71.65/10.92 % (2544794)Instructions burned: 426 (million) % 71.65/10.92 % (2544790)Refutation not found, incomplete strategy % 71.65/10.92 % (2544790)------------------------------ % 71.65/10.92 % (2544790)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 71.65/10.92 % (2544790)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 71.65/10.92 % (2544790)CaDiCaL version: 2.1.3 % 71.65/10.92 % (2544790)Termination reason: Refutation not found, incomplete strategy % 71.65/10.92 % (2544790)Time elapsed: 0.745 s % 71.65/10.92 % (2544790)Peak memory usage: 133 MB % 71.65/10.92 % (2544790)Instructions burned: 1132 (million) % 71.65/10.92 % (2544794)------------------------------ % 71.65/10.92 % (2544794)------------------------------ % 71.65/10.92 % (2544795)------------------------------ % 71.65/10.92 % (2544795)------------------------------ % 71.65/10.92 % (2544798)dis-1010_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=occurrence:random_seed=4103645485:i=2989:sd=3:ss=axioms:sgt=60_2967 on theBenchmark for (2967ds/2989Mi) % 71.65/10.92 % (2544790)------------------------------ % 71.65/10.92 % (2544790)------------------------------ % 71.65/10.92 % (2544799)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=3750768947:i=1997:bd=preordered:av=off:gtg=all:gsp=on_2967 on theBenchmark for (2967ds/1997Mi) % 71.65/10.92 % (2544801)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=2758428889:i=2088:bd=preordered:av=off_2966 on theBenchmark for (2966ds/2088Mi) % 71.65/10.92 % (2544780)Instruction limit reached! % 71.65/10.92 % (2544780)------------------------------ % 71.65/10.92 % (2544780)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 71.65/10.92 % (2544780)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 71.65/10.92 % (2544780)CaDiCaL version: 2.1.3 % 71.65/10.92 % (2544780)Termination reason: Instruction limit % 71.65/10.92 % (2544780)Termination phase: Saturation % 71.65/10.92 % (2544780)Time elapsed: 2.156 s % 71.65/10.92 % (2544780)Peak memory usage: 149 MB % 71.65/10.92 % (2544780)Instructions burned: 3256 (million) % 71.65/10.92 % (2544804)lrs+1010_64:1_anc=all:to=lpo:sil=16000:fde=none:sp=const_frequency:urr=full:sac=on:random_seed=2824651520:i=1098:nicw=on_2961 on theBenchmark for (2961ds/1098Mi) % 71.65/10.92 % (2544804)Instruction limit reached! % 71.65/10.92 % (2544804)------------------------------ % 71.65/10.92 % (2544804)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 71.65/10.92 % (2544804)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 71.65/10.92 % (2544804)CaDiCaL version: 2.1.3 % 71.65/10.92 % (2544804)Termination reason: Instruction limit % 71.65/10.92 % (2544804)Termination phase: Saturation % 71.65/10.92 % (2544804)Time elapsed: 0.439 s % 71.65/10.92 % (2544804)Peak memory usage: 97 MB % 71.65/10.92 % (2544804)Instructions burned: 1100 (million) % 71.65/10.92 % (2544798)Instruction limit reached! % 71.65/10.92 % (2544798)------------------------------ % 71.65/10.92 % (2544798)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 71.65/10.92 % (2544798)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 71.65/10.92 % (2544798)CaDiCaL version: 2.1.3 % 71.65/10.92 % (2544798)Termination reason: Instruction limit % 71.65/10.92 % (2544798)Termination phase: Saturation % 71.65/10.92 % (2544798)Time elapsed: 1.080 s % 71.65/10.92 % (2544798)Peak memory usage: 145 MB % 71.65/10.92 % (2544798)Instructions burned: 2989 (million) % 71.65/10.92 % (2544807)lrs+1002_1_ncem=casc2026/models/loop3.pt:sil=32000:npcc=on:prc=on:etr=on:spb=goal:flr=on:random_seed=1397898128:st=5.37:cond=on:i=2942:s2at=20:aac=none:fgj=on:bs=on:gtg=exists_sym:ss=axioms:er=filter:sgt=16_2955 on theBenchmark for (2955ds/2942Mi) % 71.65/10.92 % (2544806)lrs-1011_32:1_to=lpo:sil=32000:tgt=ground:sos=on:spb=goal_then_units:acc=on:random_seed=16011932:i=433:bd=preordered_2956 on theBenchmark for (2956ds/433Mi) % 71.65/10.92 % (2544806)Refutation not found, incomplete strategy % 71.65/10.92 % (2544806)------------------------------ % 71.65/10.92 % (2544806)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 71.65/10.92 % (2544806)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 71.65/10.92 % (2544806)CaDiCaL version: 2.1.3 % 71.65/10.92 % (2544806)Termination reason: Refutation not found, incomplete strategy % 82.73/12.41 % (2544806)Time elapsed: 0.094 s % 82.73/12.41 % (2544806)Peak memory usage: 90 MB % 82.73/12.41 % (2544806)Instructions burned: 164 (million) % 82.73/12.41 % (2544799)Instruction limit reached! % 82.73/12.41 % (2544799)------------------------------ % 82.73/12.41 % (2544799)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 82.73/12.41 % (2544799)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 82.73/12.41 % (2544799)CaDiCaL version: 2.1.3 % 82.73/12.41 % (2544799)Termination reason: Instruction limit % 82.73/12.41 % (2544799)Termination phase: Saturation % 82.73/12.41 % (2544799)Time elapsed: 1.364 s % 82.73/12.41 % (2544799)Peak memory usage: 136 MB % 82.73/12.41 % (2544799)Instructions burned: 1998 (million) % 82.73/12.41 % (2544806)------------------------------ % 82.73/12.41 % (2544806)------------------------------ % 82.73/12.41 % (2544801)Instruction limit reached! % 82.73/12.41 % (2544801)------------------------------ % 82.73/12.41 % (2544801)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 82.73/12.41 % (2544801)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 82.73/12.41 % (2544801)CaDiCaL version: 2.1.3 % 82.73/12.41 % (2544801)Termination reason: Instruction limit % 82.73/12.41 % (2544801)Termination phase: Saturation % 82.73/12.41 % (2544801)Time elapsed: 1.380 s % 82.73/12.41 % (2544801)Peak memory usage: 138 MB % 82.73/12.41 % (2544801)Instructions burned: 2088 (million) % 82.73/12.41 % (2544810)lrs+35_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=reverse_arity:urr=full:rp=on:br=off:random_seed=893664727:i=6922:s2at=5:sd=3:bd=all:ss=axioms:er=known:sgt=32_2952 on theBenchmark for (2952ds/6922Mi) % 82.73/12.41 % (2544811)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=1025228046:s2a=on:i=596:s2at=2.3:gtgl=5:gtg=all:sup=off_2951 on theBenchmark for (2951ds/596Mi) % 82.73/12.41 % (2544811)Refutation not found, incomplete strategy % 82.73/12.41 % (2544811)------------------------------ % 82.73/12.41 % (2544811)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 82.73/12.41 % (2544811)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 82.73/12.41 % (2544811)CaDiCaL version: 2.1.3 % 82.73/12.41 % (2544811)Termination reason: Refutation not found, incomplete strategy % 82.73/12.41 % (2544811)Time elapsed: 0.023 s % 82.73/12.41 % (2544811)Peak memory usage: 89 MB % 82.73/12.41 % (2544811)Instructions burned: 43 (million) % 82.73/12.41 % (2544812)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=969707000:i=4123:kws=inv_frequency:bd=preordered:av=off:er=known_2951 on theBenchmark for (2951ds/4123Mi) % 82.73/12.41 % (2544811)------------------------------ % 82.73/12.41 % (2544811)------------------------------ % 82.73/12.41 % (2544816)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=1726516220:i=16411:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2947 on theBenchmark for (2947ds/16411Mi) % 82.73/12.41 % (2544807)Instruction limit reached! % 82.73/12.41 % (2544807)------------------------------ % 82.73/12.41 % (2544807)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 82.73/12.41 % (2544807)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 82.73/12.41 % (2544807)CaDiCaL version: 2.1.3 % 82.73/12.41 % (2544807)Termination reason: Instruction limit % 82.73/12.41 % (2544807)Termination phase: Saturation % 82.73/12.41 % (2544807)Time elapsed: 1.023 s % 82.73/12.41 % (2544807)Peak memory usage: 141 MB % 82.73/12.41 % (2544807)Instructions burned: 2943 (million) % 82.73/12.41 % (2544818)lrs+0_1_ncem=casc2026/models/loop1.pt:sil=8000:tgt=full:npcc=on:sp=reverse_frequency:gs=on:random_seed=3358694800:i=1670:kws=inv_precedence:bd=all:av=off:gtg=exists_all_2944 on theBenchmark for (2944ds/1670Mi) % 82.73/12.41 % (2544810)Refutation not found, incomplete strategy % 82.73/12.41 % (2544810)------------------------------ % 82.73/12.41 % (2544810)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 82.73/12.41 % (2544810)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 82.73/12.41 % (2544810)CaDiCaL version: 2.1.3 % 82.73/12.41 % (2544810)Termination reason: Refutation not found, incomplete strategy % 82.73/12.41 % (2544810)Time elapsed: 0.743 s % 82.73/12.41 % (2544810)Peak memory usage: 131 MB % 82.73/12.41 % (2544810)Instructions burned: 1131 (million) % 82.73/12.41 % (2544810)------------------------------ % 82.73/12.41 % (2544810)------------------------------ % 98.51/14.71 % (2544820)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=4047461218:st=3:cond=fast:i=1722:sd=2:ss=included:fsd=on_2941 on theBenchmark for (2941ds/1722Mi) % 98.51/14.71 % (2544818)Instruction limit reached! % 98.51/14.71 % (2544818)------------------------------ % 98.51/14.71 % (2544818)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 98.51/14.71 % (2544818)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 98.51/14.71 % (2544818)CaDiCaL version: 2.1.3 % 98.51/14.71 % (2544818)Termination reason: Instruction limit % 98.51/14.71 % (2544818)Termination phase: Saturation % 98.51/14.71 % (2544818)Time elapsed: 0.621 s % 98.51/14.71 % (2544818)Peak memory usage: 137 MB % 98.51/14.71 % (2544818)Instructions burned: 1672 (million) % 98.51/14.71 % (2544822)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=3375869583:cts=off:cond=on:i=9530:bs=on:fsd=on_2937 on theBenchmark for (2937ds/9530Mi) % 98.51/14.71 % (2544820)Instruction limit reached! % 98.51/14.71 % (2544820)------------------------------ % 98.51/14.71 % (2544820)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 98.51/14.71 % (2544820)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 98.51/14.71 % (2544820)CaDiCaL version: 2.1.3 % 98.51/14.71 % (2544820)Termination reason: Instruction limit % 98.51/14.71 % (2544820)Termination phase: Saturation % 98.51/14.71 % (2544820)Time elapsed: 1.453 s % 98.51/14.71 % (2544820)Peak memory usage: 136 MB % 98.51/14.71 % (2544820)Instructions burned: 1723 (million) % 98.51/14.71 % (2544824)lrs+10_1_ncem=casc2026/models/loop4.pt:sil=64000:npcc=on:sp=occurrence:random_seed=1441511761:st=2:i=4495:sd=10:ss=included_2925 on theBenchmark for (2925ds/4495Mi) % 98.51/14.71 % (2544812)Instruction limit reached! % 98.51/14.71 % (2544812)------------------------------ % 98.51/14.71 % (2544812)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 98.51/14.71 % (2544812)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 98.51/14.71 % (2544812)CaDiCaL version: 2.1.3 % 98.51/14.71 % (2544812)Termination reason: Instruction limit % 98.51/14.71 % (2544812)Termination phase: Saturation % 98.51/14.71 % (2544812)Time elapsed: 2.726 s % 98.51/14.71 % (2544812)Peak memory usage: 155 MB % 98.51/14.71 % (2544812)Instructions burned: 4123 (million) % 98.51/14.71 % (2544826)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=1255419184:cond=fast:i=4920:s2at=1.9:kws=inv_frequency:av=off:er=filter_2922 on theBenchmark for (2922ds/4920Mi) % 98.51/14.71 % (2544786)Instruction limit reached! % 98.51/14.71 % (2544786)------------------------------ % 98.51/14.71 % (2544786)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 98.51/14.71 % (2544786)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 98.51/14.71 % (2544786)CaDiCaL version: 2.1.3 % 98.51/14.71 % (2544786)Termination reason: Instruction limit % 98.51/14.71 % (2544786)Termination phase: Saturation % 98.51/14.71 % (2544786)Time elapsed: 6.563 s % 98.51/14.71 % (2544786)Peak memory usage: 186 MB % 98.51/14.71 % (2544786)Instructions burned: 10308 (million) % 98.51/14.71 % (2544828)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=2957126117:cts=off:cond=on:i=2083:s2at=-1:fgj=on:av=off_2914 on theBenchmark for (2914ds/2083Mi) % 98.51/14.71 % (2544828)Instruction limit reached! % 98.51/14.71 % (2544828)------------------------------ % 98.51/14.71 % (2544828)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 98.51/14.71 % (2544828)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 98.51/14.71 % (2544828)CaDiCaL version: 2.1.3 % 98.51/14.71 % (2544828)Termination reason: Instruction limit % 98.51/14.71 % (2544828)Termination phase: Saturation % 98.51/14.71 % (2544828)Time elapsed: 1.367 s % 98.51/14.71 % (2544828)Peak memory usage: 136 MB % 98.51/14.71 % (2544828)Instructions burned: 2084 (million) % 98.51/14.71 % (2544830)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=1972237520:i=4629:av=off:gsp=on_2899 on theBenchmark for (2899ds/4629Mi) % 98.51/14.71 % (2544822)Instruction limit reached! % 116.12/17.14 % (2544822)------------------------------ % 116.12/17.14 % (2544822)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 116.12/17.14 % (2544822)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 116.12/17.14 % (2544822)CaDiCaL version: 2.1.3 % 116.12/17.14 % (2544822)Termination reason: Instruction limit % 116.12/17.14 % (2544822)Termination phase: Saturation % 116.12/17.14 % (2544822)Time elapsed: 4.171 s % 116.12/17.14 % (2544822)Peak memory usage: 155 MB % 116.12/17.14 % (2544822)Instructions burned: 9530 (million) % 116.12/17.14 % (2544832)dis+10_64_sil=16000:tgt=full:plsq=on:prc=on:drc=off:plsqc=2:plsqr=32,1:spb=goal:random_seed=107819488:i=1258:av=off_2894 on theBenchmark for (2894ds/1258Mi) % 116.12/17.14 % (2544824)Instruction limit reached! % 116.12/17.14 % (2544824)------------------------------ % 116.12/17.14 % (2544824)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 116.12/17.14 % (2544824)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 116.12/17.14 % (2544824)CaDiCaL version: 2.1.3 % 116.12/17.14 % (2544824)Termination reason: Instruction limit % 116.12/17.14 % (2544824)Termination phase: Saturation % 116.12/17.14 % (2544824)Time elapsed: 3.280 s % 116.12/17.14 % (2544824)Peak memory usage: 156 MB % 116.12/17.14 % (2544824)Instructions burned: 4495 (million) % 116.12/17.14 % (2544832)Instruction limit reached! % 116.12/17.14 % (2544832)------------------------------ % 116.12/17.14 % (2544832)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 116.12/17.14 % (2544832)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 116.12/17.14 % (2544832)CaDiCaL version: 2.1.3 % 116.12/17.14 % (2544832)Termination reason: Instruction limit % 116.12/17.14 % (2544832)Termination phase: Saturation % 116.12/17.14 % (2544832)Time elapsed: 0.334 s % 116.12/17.14 % (2544832)Peak memory usage: 100 MB % 116.12/17.14 % (2544832)Instructions burned: 1260 (million) % 116.12/17.14 % (2544834)ott+1_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:fdtod=off:random_seed=575682338:i=7343:av=off:ss=included_2890 on theBenchmark for (2890ds/7343Mi) % 116.12/17.14 % (2544835)lrs-1002_1_to=lpo:sil=16000:sp=reverse_arity:sos=on:random_seed=619563633:i=1325:sd=2:ss=axioms:sgt=16_2890 on theBenchmark for (2890ds/1325Mi) % 116.12/17.14 % (2544835)Refutation not found, incomplete strategy % 116.12/17.14 % (2544835)------------------------------ % 116.12/17.14 % (2544835)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 116.12/17.14 % (2544835)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 116.12/17.14 % (2544835)CaDiCaL version: 2.1.3 % 116.12/17.14 % (2544835)Termination reason: Refutation not found, incomplete strategy % 116.12/17.14 % (2544835)Time elapsed: 0.005 s % 116.12/17.14 % (2544835)Peak memory usage: 89 MB % 116.12/17.14 % (2544835)Instructions burned: 16 (million) % 116.12/17.14 % (2544835)------------------------------ % 116.12/17.14 % (2544835)------------------------------ % 116.12/17.14 % (2544826)Instruction limit reached! % 116.12/17.14 % (2544826)------------------------------ % 116.12/17.14 % (2544826)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 116.12/17.14 % (2544826)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 116.12/17.14 % (2544826)CaDiCaL version: 2.1.3 % 116.12/17.14 % (2544826)Termination reason: Instruction limit % 116.12/17.14 % (2544826)Termination phase: Saturation % 116.12/17.14 % (2544826)Time elapsed: 3.434 s % 116.12/17.14 % (2544826)Peak memory usage: 156 MB % 116.12/17.14 % (2544826)Instructions burned: 4920 (million) % 116.12/17.14 % (2544838)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=2613976845:st=3.9:cond=fast:i=2646:s2at=1.8:sd=5:amm=off:gtg=position:ss=axioms:fsd=on_2887 on theBenchmark for (2887ds/2646Mi) % 116.12/17.14 % (2544840)dis-1003_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:sp=arity:sos=on:urr=on:random_seed=2042966985:i=1489:sd=2:ep=R:ss=axioms_2886 on theBenchmark for (2886ds/1489Mi) % 116.12/17.14 % (2544840)Refutation not found, incomplete strategy % 116.12/17.14 % (2544840)------------------------------ % 116.12/17.14 % (2544840)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 116.12/17.14 % (2544840)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 116.12/17.14 % (2544840)CaDiCaL version: 2.1.3 % 116.12/17.14 % (2544840)Termination reason: Refutation not found, incomplete strategy % 116.12/17.14 % (2544840)Time elapsed: 0.547 s % 116.12/17.14 % (2544840)Peak memory usage: 127 MB % 116.12/17.14 % (2544840)Instructions burned: 837 (million) % 133.03/19.56 % (2544830)Instruction limit reached! % 133.03/19.56 % (2544830)------------------------------ % 133.03/19.56 % (2544830)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 133.03/19.56 % (2544830)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 133.03/19.56 % (2544830)CaDiCaL version: 2.1.3 % 133.03/19.56 % (2544830)Termination reason: Instruction limit % 133.03/19.56 % (2544830)Termination phase: Saturation % 133.03/19.56 % (2544830)Time elapsed: 1.918 s % 133.03/19.56 % (2544830)Peak memory usage: 135 MB % 133.03/19.56 % (2544830)Instructions burned: 4631 (million) % 133.03/19.56 % (2544840)------------------------------ % 133.03/19.56 % (2544840)------------------------------ % 133.03/19.56 % (2544842)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=4103078158:i=1503_2878 on theBenchmark for (2878ds/1503Mi) % 133.03/19.56 % (2544844)lrs+10_1_ncem=casc2026/models/loop3.pt:sil=16000:tgt=ground:npcc=on:random_seed=3342189886:i=13942:kws=frequency_2877 on theBenchmark for (2877ds/13942Mi) % 133.03/19.56 % (2544838)Instruction limit reached! % 133.03/19.56 % (2544838)------------------------------ % 133.03/19.56 % (2544838)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 133.03/19.56 % (2544838)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 133.03/19.56 % (2544838)CaDiCaL version: 2.1.3 % 133.03/19.56 % (2544838)Termination reason: Instruction limit % 133.03/19.56 % (2544838)Termination phase: Saturation % 133.03/19.56 % (2544838)Time elapsed: 1.059 s % 133.03/19.56 % (2544838)Peak memory usage: 143 MB % 133.03/19.56 % (2544838)Instructions burned: 2647 (million) % 133.03/19.56 % (2544846)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=2094656114:i=3604:fsr=off:er=filter_2876 on theBenchmark for (2876ds/3604Mi) % 133.03/19.56 % (2544842)Instruction limit reached! % 133.03/19.56 % (2544842)------------------------------ % 133.03/19.56 % (2544842)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 133.03/19.56 % (2544842)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 133.03/19.56 % (2544842)CaDiCaL version: 2.1.3 % 133.03/19.56 % (2544842)Termination reason: Instruction limit % 133.03/19.56 % (2544842)Termination phase: Saturation % 133.03/19.56 % (2544842)Time elapsed: 1.031 s % 133.03/19.56 % (2544842)Peak memory usage: 133 MB % 133.03/19.56 % (2544842)Instructions burned: 1504 (million) % 133.03/19.56 % (2544848)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=32000:npcc=on:random_seed=812968555:i=1876:sd=1:ss=included:sgt=32_2867 on theBenchmark for (2867ds/1876Mi) % 133.03/19.56 % (2544846)Instruction limit reached! % 133.03/19.56 % (2544846)------------------------------ % 133.03/19.56 % (2544846)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 133.03/19.56 % (2544846)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 133.03/19.56 % (2544846)CaDiCaL version: 2.1.3 % 133.03/19.56 % (2544846)Termination reason: Instruction limit % 133.03/19.56 % (2544846)Termination phase: Saturation % 133.03/19.56 % (2544846)Time elapsed: 1.357 s % 133.03/19.56 % (2544846)Peak memory usage: 148 MB % 133.03/19.56 % (2544846)Instructions burned: 3606 (million) % 133.03/19.56 % (2544850)lrs+10_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:fde=none:sp=arity:urr=on:br=off:random_seed=2772060751:i=1932:bd=preordered:ins=10:sup=off:ss=axioms_2861 on theBenchmark for (2861ds/1932Mi) % 133.03/19.56 % (2544834)Instruction limit reached! % 133.03/19.56 % (2544834)------------------------------ % 133.03/19.56 % (2544834)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 133.03/19.56 % (2544834)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 133.03/19.56 % (2544834)CaDiCaL version: 2.1.3 % 133.03/19.56 % (2544834)Termination reason: Instruction limit % 133.03/19.56 % (2544834)Termination phase: Saturation % 133.03/19.56 % (2544834)Time elapsed: 3.157 s % 133.03/19.56 % (2544834)Peak memory usage: 145 MB % 133.03/19.56 % (2544834)Instructions burned: 7346 (million) % 133.03/19.56 % (2544850)Refutation not found, incomplete strategy % 133.03/19.56 % (2544850)------------------------------ % 133.03/19.56 % (2544850)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 133.03/19.56 % (2544850)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 133.03/19.56 % (2544850)CaDiCaL version: 2.1.3 % 133.03/19.56 % (2544850)Termination reason: Refutation not found, incomplete strategy % 149.18/21.95 % (2544850)Time elapsed: 0.360 s % 149.18/21.95 % (2544850)Peak memory usage: 128 MB % 149.18/21.95 % (2544850)Instructions burned: 907 (million) % 149.18/21.95 % (2544852)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=1934844524:s2pl=on:cond=fast:i=1980:s2at=2:kws=inv_precedence:doe=on:ins=1:av=off:gsp=on_2857 on theBenchmark for (2857ds/1980Mi) % 149.18/21.95 % (2544850)------------------------------ % 149.18/21.95 % (2544850)------------------------------ % 149.18/21.95 % (2544854)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=2735582783:i=3902:kws=inv_arity_squared:fgj=on:ss=axioms:sgt=11_2855 on theBenchmark for (2855ds/3902Mi) % 149.18/21.95 % (2544848)Instruction limit reached! % 149.18/21.95 % (2544848)------------------------------ % 149.18/21.95 % (2544848)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 149.18/21.95 % (2544848)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 149.18/21.95 % (2544848)CaDiCaL version: 2.1.3 % 149.18/21.95 % (2544848)Termination reason: Instruction limit % 149.18/21.95 % (2544848)Termination phase: Saturation % 149.18/21.95 % (2544848)Time elapsed: 1.237 s % 149.18/21.95 % (2544848)Peak memory usage: 137 MB % 149.18/21.95 % (2544848)Instructions burned: 1876 (million) % 149.18/21.95 % (2544856)dis+10_32_sil=16000:tgt=ground:drc=off:sas=cadical:acc=on:alpa=false:avsqc=3:random_seed=134995745:avsq=on:i=3916:aac=none:amm=off_2853 on theBenchmark for (2853ds/3916Mi) % 149.18/21.95 % (2544854)Refutation not found, incomplete strategy % 149.18/21.95 % (2544854)------------------------------ % 149.18/21.95 % (2544854)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 149.18/21.95 % (2544854)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 149.18/21.95 % (2544854)CaDiCaL version: 2.1.3 % 149.18/21.95 % (2544854)Termination reason: Refutation not found, incomplete strategy % 149.18/21.95 % (2544854)Time elapsed: 0.380 s % 149.18/21.95 % (2544854)Peak memory usage: 130 MB % 149.18/21.95 % (2544854)Instructions burned: 937 (million) % 149.18/21.95 % (2544854)------------------------------ % 149.18/21.95 % (2544854)------------------------------ % 149.18/21.95 % (2544858)dis+10_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=full:npcc=on:drc=ordering:lcm=predicate:random_seed=3640230216:cond=on:i=3940:av=off:er=known_2848 on theBenchmark for (2848ds/3940Mi) % 149.18/21.95 % (2544852)Instruction limit reached! % 149.18/21.95 % (2544852)------------------------------ % 149.18/21.95 % (2544852)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 149.18/21.95 % (2544852)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 149.18/21.95 % (2544852)CaDiCaL version: 2.1.3 % 149.18/21.95 % (2544852)Termination reason: Instruction limit % 149.18/21.95 % (2544852)Termination phase: Saturation % 149.18/21.95 % (2544852)Time elapsed: 0.971 s % 149.18/21.95 % (2544852)Peak memory usage: 138 MB % 149.18/21.95 % (2544852)Instructions burned: 1981 (million) % 149.18/21.95 % (2544860)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=reverse_frequency:bce=on:random_seed=1454725147:s2pl=on:i=3980:gtgl=3:kws=precedence:fgj=on:gtg=all_2846 on theBenchmark for (2846ds/3980Mi) % 149.18/21.95 % (2544816)Instruction limit reached! % 149.18/21.95 % (2544816)------------------------------ % 149.18/21.95 % (2544816)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 149.18/21.95 % (2544816)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 149.18/21.95 % (2544816)CaDiCaL version: 2.1.3 % 149.18/21.95 % (2544816)Termination reason: Instruction limit % 149.18/21.95 % (2544816)Termination phase: Saturation % 149.18/21.95 % (2544816)Time elapsed: 11.225 s % 149.18/21.95 % (2544816)Peak memory usage: 191 MB % 149.18/21.95 % (2544816)Instructions burned: 16412 (million) % 149.18/21.95 % (2544856)Instruction limit reached! % 149.18/21.95 % (2544856)------------------------------ % 149.18/21.95 % (2544856)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 149.18/21.95 % (2544856)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 149.18/21.95 % (2544856)CaDiCaL version: 2.1.3 % 149.18/21.95 % (2544856)Termination reason: Instruction limit % 149.18/21.95 % (2544856)Termination phase: Saturation % 149.18/21.95 % (2544856)Time elapsed: 1.898 s % 149.18/21.95 % (2544856)Peak memory usage: 103 MB % 149.18/21.95 % (2544856)Instructions burned: 3919 (million) % 149.18/21.95 % (2544862)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=390395609:i=2087:s2at=3:kws=frequency:av=off:fsr=off_2833 on theBenchmark for (2833ds/2087Mi) % 167.68/24.40 % (2544863)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=1425063577:cts=off:cond=on:i=4272:bs=on:fsd=on_2833 on theBenchmark for (2833ds/4272Mi) % 167.68/24.40 % (2544860)Instruction limit reached! % 167.68/24.40 % (2544860)------------------------------ % 167.68/24.40 % (2544860)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 167.68/24.40 % (2544860)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 167.68/24.40 % (2544860)CaDiCaL version: 2.1.3 % 167.68/24.40 % (2544860)Termination reason: Instruction limit % 167.68/24.40 % (2544860)Termination phase: Saturation % 167.68/24.40 % (2544860)Time elapsed: 1.459 s % 167.68/24.40 % (2544860)Peak memory usage: 154 MB % 167.68/24.40 % (2544860)Instructions burned: 3982 (million) % 167.68/24.41 % (2544866)lrs-30_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:urr=on:bce=on:rp=on:br=off:flr=on:random_seed=3211381884:st=-1:i=2197:kws=precedence:av=off:ss=axioms:er=known_2831 on theBenchmark for (2831ds/2197Mi) % 167.68/24.41 % (2544866)Refutation not found, incomplete strategy % 167.68/24.41 % (2544866)------------------------------ % 167.68/24.41 % (2544866)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 167.68/24.41 % (2544866)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 167.68/24.41 % (2544866)CaDiCaL version: 2.1.3 % 167.68/24.41 % (2544866)Termination reason: Refutation not found, incomplete strategy % 167.68/24.41 % (2544866)Time elapsed: 0.406 s % 167.68/24.41 % (2544866)Peak memory usage: 132 MB % 167.68/24.41 % (2544866)Instructions burned: 1138 (million) % 167.68/24.41 % (2544866)------------------------------ % 167.68/24.41 % (2544866)------------------------------ % 167.68/24.41 % (2544868)dis+21_1_sil=8000:spb=goal_then_units:random_seed=4023327776:avsq=on:i=6508:avsqr=1,16:kws=arity_squared:fgj=on_2824 on theBenchmark for (2824ds/6508Mi) % 167.68/24.41 % (2544858)Instruction limit reached! % 167.68/24.41 % (2544858)------------------------------ % 167.68/24.41 % (2544858)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 167.68/24.41 % (2544858)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 167.68/24.41 % (2544858)CaDiCaL version: 2.1.3 % 167.68/24.41 % (2544858)Termination reason: Instruction limit % 167.68/24.41 % (2544858)Termination phase: Saturation % 167.68/24.41 % (2544858)Time elapsed: 2.395 s % 167.68/24.41 % (2544858)Peak memory usage: 145 MB % 167.68/24.41 % (2544858)Instructions burned: 3940 (million) % 167.68/24.41 % (2544871)dis-1002_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=occurrence:random_seed=1093122173:i=2330:fgj=on:av=off:fsr=off_2823 on theBenchmark for (2823ds/2330Mi) % 167.68/24.41 % (2544862)Instruction limit reached! % 167.68/24.41 % (2544862)------------------------------ % 167.68/24.41 % (2544862)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 167.68/24.41 % (2544862)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 167.68/24.41 % (2544862)CaDiCaL version: 2.1.3 % 167.68/24.41 % (2544862)Termination reason: Instruction limit % 167.68/24.41 % (2544862)Termination phase: Saturation % 167.68/24.41 % (2544862)Time elapsed: 1.479 s % 167.68/24.41 % (2544862)Peak memory usage: 139 MB % 167.68/24.41 % (2544862)Instructions burned: 2087 (million) % 167.68/24.41 % (2544873)dis+10_2_anc=none:sil=64000:bsr=on:rp=on:alpa=true:avsqc=1:random_seed=11510776:avsq=on:i=7592:avsqr=1,16:bs=on:gsp=on_2817 on theBenchmark for (2817ds/7592Mi) % 167.68/24.41 % (2544868)Instruction limit reached! % 167.68/24.41 % (2544868)------------------------------ % 167.68/24.41 % (2544868)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 167.68/24.41 % (2544868)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 167.68/24.41 % (2544868)CaDiCaL version: 2.1.3 % 167.68/24.41 % (2544868)Termination reason: Instruction limit % 167.68/24.41 % (2544868)Termination phase: Saturation % 167.68/24.41 % (2544868)Time elapsed: 1.444 s % 167.68/24.41 % (2544868)Peak memory usage: 106 MB % 167.68/24.41 % (2544868)Instructions burned: 6510 (million) % 167.68/24.41 % (2544875)lrs-1002_1_ncem=casc2026/models/loop6.pt:sil=64000:tgt=ground:npcc=on:prc=on:sims=off:sp=reverse_frequency:spb=goal_then_units:bce=on:bsr=unit_only:gs=on:flr=on:random_seed=955110571:i=2693:kws=precedence:ins=1:av=off_2809 on theBenchmark for (2809ds/2693Mi) % 238.11/34.33 % (2544871)Instruction limit reached! % 238.11/34.33 % (2544871)------------------------------ % 238.11/34.33 % (2544871)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 238.11/34.33 % (2544871)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 238.11/34.33 % (2544871)CaDiCaL version: 2.1.3 % 238.11/34.33 % (2544871)Termination reason: Instruction limit % 238.11/34.33 % (2544871)Termination phase: Saturation % 238.11/34.33 % (2544871)Time elapsed: 1.578 s % 238.11/34.33 % (2544871)Peak memory usage: 139 MB % 238.11/34.33 % (2544871)Instructions burned: 2330 (million) % 238.11/34.33 % (2544863)Instruction limit reached! % 238.11/34.33 % (2544863)------------------------------ % 238.11/34.33 % (2544863)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 238.11/34.33 % (2544863)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 238.11/34.33 % (2544863)CaDiCaL version: 2.1.3 % 238.11/34.33 % (2544863)Termination reason: Instruction limit % 238.11/34.33 % (2544863)Termination phase: Saturation % 238.11/34.33 % (2544863)Time elapsed: 2.632 s % 238.11/34.33 % (2544863)Peak memory usage: 145 MB % 238.11/34.33 % (2544863)Instructions burned: 4272 (million) % 238.11/34.33 % (2544877)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:random_seed=2347769480:i=28651:sd=4:ss=included:sgt=64_2805 on theBenchmark for (2805ds/28651Mi) % 238.11/34.33 % (2544878)lrs-1010_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:sp=unary_frequency:random_seed=169354385:i=2700:kws=precedence:fgj=on:bd=preordered:ins=1_2805 on theBenchmark for (2805ds/2700Mi) % 238.11/34.33 % (2544875)Instruction limit reached! % 238.11/34.33 % (2544875)------------------------------ % 238.11/34.33 % (2544875)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 238.11/34.33 % (2544875)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 238.11/34.33 % (2544875)CaDiCaL version: 2.1.3 % 238.11/34.33 % (2544875)Termination reason: Instruction limit % 238.11/34.33 % (2544875)Termination phase: Saturation % 238.11/34.33 % (2544875)Time elapsed: 1.012 s % 238.11/34.33 % (2544875)Peak memory usage: 141 MB % 238.11/34.33 % (2544875)Instructions burned: 2693 (million) % 238.11/34.33 % (2544881)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_min:sos=on:erd=off:spb=goal:lsd=20:urr=full:sac=on:random_seed=2252856175:i=3196:nm=4_2798 on theBenchmark for (2798ds/3196Mi) % 238.11/34.33 % (2544844)Instruction limit reached! % 238.11/34.33 % (2544844)------------------------------ % 238.11/34.33 % (2544844)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 238.11/34.33 % (2544844)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 238.11/34.33 % (2544844)CaDiCaL version: 2.1.3 % 238.11/34.33 % (2544844)Termination reason: Instruction limit % 238.11/34.33 % (2544844)Termination phase: Saturation % 238.11/34.33 % (2544844)Time elapsed: 8.334 s % 238.11/34.33 % (2544844)Peak memory usage: 208 MB % 238.11/34.33 % (2544844)Instructions burned: 13942 (million) % 238.11/34.33 % (2544883)ott+11_1_ncem=casc2026/models/loop4.pt:sil=64000:tgt=full:irw=on:npcc=on:spb=units:flr=on:random_seed=4137771279:cts=off:i=3254:av=off_2792 on theBenchmark for (2792ds/3254Mi) % 238.11/34.33 % (2544878)Instruction limit reached! % 238.11/34.33 % (2544878)------------------------------ % 238.11/34.33 % (2544878)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 238.11/34.33 % (2544878)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 238.11/34.33 % (2544878)CaDiCaL version: 2.1.3 % 238.11/34.33 % (2544878)Termination reason: Instruction limit % 238.11/34.33 % (2544878)Termination phase: Saturation % 238.11/34.33 % (2544878)Time elapsed: 1.745 s % 238.11/34.33 % (2544878)Peak memory usage: 142 MB % 238.11/34.33 % (2544878)Instructions burned: 2701 (million) % 238.11/34.33 % (2544885)dis+1011_1_sfv=off:ncem=casc2026/models/loop2.pt:sil=32000:tgt=ground:npcc=on:lcm=predicate:bce=on:sac=on:random_seed=1311247769:i=3264:bd=all:gtg=exists_sym:ss=included:er=known_2786 on theBenchmark for (2786ds/3264Mi) % 238.11/34.33 % (2544881)Instruction limit reached! % 238.11/34.33 % (2544881)------------------------------ % 238.11/34.33 % (2544881)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 238.11/34.33 % (2544881)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 238.11/34.33 % (2544881)CaDiCaL version: 2.1.3 % 238.11/34.33 % (2544881)Termination reason: Instruction limit % 238.11/34.33 % (2544881)Termination phase: Saturation % 275.03/39.53 % (2544881)Time elapsed: 1.271 s % 275.03/39.53 % (2544881)Peak memory usage: 145 MB % 275.03/39.53 % (2544881)Instructions burned: 3197 (million) % 275.03/39.53 % (2544887)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:sp=unary_first:sos=on:lma=off:lsd=20:urr=on:kmz=on:sac=on:random_seed=2537190194:st=6:i=9708:kws=inv_frequency:doe=on:fgj=on:ss=axioms_2784 on theBenchmark for (2784ds/9708Mi) % 275.03/39.53 % (2544887)Refutation not found, incomplete strategy % 275.03/39.53 % (2544887)------------------------------ % 275.03/39.53 % (2544887)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 275.03/39.53 % (2544887)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 275.03/39.53 % (2544887)CaDiCaL version: 2.1.3 % 275.03/39.53 % (2544887)Termination reason: Refutation not found, incomplete strategy % 275.03/39.53 % (2544887)Time elapsed: 0.487 s % 275.03/39.53 % (2544887)Peak memory usage: 131 MB % 275.03/39.53 % (2544887)Instructions burned: 1221 (million) % 275.03/39.53 % (2544873)Instruction limit reached! % 275.03/39.53 % (2544873)------------------------------ % 275.03/39.53 % (2544873)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 275.03/39.53 % (2544873)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 275.03/39.53 % (2544873)CaDiCaL version: 2.1.3 % 275.03/39.53 % (2544873)Termination reason: Instruction limit % 275.03/39.53 % (2544873)Termination phase: Saturation % 275.03/39.53 % (2544873)Time elapsed: 3.829 s % 275.03/39.53 % (2544873)Peak memory usage: 139 MB % 275.03/39.53 % (2544873)Instructions burned: 7592 (million) % 275.03/39.53 % (2544887)------------------------------ % 275.03/39.53 % (2544887)------------------------------ % 275.03/39.53 % (2544889)lrs+1010_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=full:npcc=on:erd=off:spb=goal:sac=on:newcnf=on:random_seed=1569906473:i=21997:s2at=5:gtg=all_2778 on theBenchmark for (2778ds/21997Mi) % 275.03/39.53 % (2544890)dis+10_14_to=lpo:sil=8000:tgt=full:drc=off:sp=const_frequency:sos=all:random_seed=4076724461:i=7551:gtgl=5:bs=unit_only:fsr=off:gtg=exists_all_2777 on theBenchmark for (2777ds/7551Mi) % 275.03/39.53 % (2544890)Refutation not found, incomplete strategy % 275.03/39.53 % (2544890)------------------------------ % 275.03/39.53 % (2544890)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 275.03/39.53 % (2544890)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 275.03/39.53 % (2544890)CaDiCaL version: 2.1.3 % 275.03/39.53 % (2544890)Termination reason: Refutation not found, incomplete strategy % 275.03/39.53 % (2544890)Time elapsed: 0.007 s % 275.03/39.53 % (2544890)Peak memory usage: 89 MB % 275.03/39.53 % (2544890)Instructions burned: 23 (million) % 275.03/39.53 % (2544890)------------------------------ % 275.03/39.53 % (2544890)------------------------------ % 275.03/39.53 % (2544893)lrs+1011_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=826734661:i=8924:sd=1:ss=included_2774 on theBenchmark for (2774ds/8924Mi) % 275.03/39.53 % (2544883)Instruction limit reached! % 275.03/39.53 % (2544883)------------------------------ % 275.03/39.53 % (2544883)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 275.03/39.53 % (2544883)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 275.03/39.53 % (2544883)CaDiCaL version: 2.1.3 % 275.03/39.53 % (2544883)Termination reason: Instruction limit % 275.03/39.53 % (2544883)Termination phase: Saturation % 275.03/39.53 % (2544883)Time elapsed: 2.140 s % 275.03/39.53 % (2544883)Peak memory usage: 144 MB % 275.03/39.53 % (2544883)Instructions burned: 3255 (million) % 275.03/39.53 % (2544895)lrs+1011_1_ncem=casc2026/models/loop2.pt:sil=16000:npcc=on:sp=arity:fd=preordered:random_seed=2417036859:i=9638:kws=frequency:bd=preordered_2769 on theBenchmark for (2769ds/9638Mi) % 275.03/39.53 % (2544885)Instruction limit reached! % 275.03/39.53 % (2544885)------------------------------ % 275.03/39.53 % (2544885)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 275.03/39.53 % (2544885)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 275.03/39.53 % (2544885)CaDiCaL version: 2.1.3 % 275.03/39.53 % (2544885)Termination reason: Instruction limit % 275.03/39.53 % (2544885)Termination phase: Saturation % 275.03/39.53 % (2544885)Time elapsed: 2.388 s % 275.03/39.53 % (2544885)Peak memory usage: 146 MB % 275.03/39.53 % (2544885)Instructions burned: 3264 (million) % 275.03/39.53 % (2544897)lrs+1002_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:prc=on:drc=off:sp=const_min:sos=on:lcm=predicate:s2agt=20:br=off:flr=on:random_seed=4271282194:i=51Terminated %------------------------------------------------------------------------------