%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWV352-1 : TPTP v9.3.1. Released v3.2.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % Computer : n005.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:21:02 PM UTC 2026 % Result : Timeout 300.50s 42.73s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWV352-1 : TPTP v9.3.1. Released v3.2.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.07/0.19 % Computer : n005.cluster.edu % 0.07/0.19 % Model : x86_64 x86_64 % 0.07/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.07/0.19 % Memory : 8046.5625MB % 0.07/0.19 % OS : Linux 6.8.0-71-generic % 0.07/0.19 % CPULimit : 300 % 0.07/0.19 % WCLimit : 300 % 0.07/0.19 % DateTime : Mon Sep 28 10:41:32 UTC 2026 % 0.07/0.19 % CPUTime : % 0.07/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.07/0.22 Running first-order model finding % 0.07/0.22 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 13.27/2.15 % (706356)Will run a generic schedule for satisfiability detection. % 13.27/2.15 % (706362)% WARNING: option uhcvi not known. % 13.27/2.15 % (706361)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2603662276_2999 on theBenchmark for (2999ds/0Mi) % 13.27/2.15 % (706362)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=33143816:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 13.27/2.15 % (706363)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1901121186:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 13.27/2.15 % (706364)dis+10_1_sil=32000:sp=arity:random_seed=1820575617:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 13.27/2.15 % (706365)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2047753452:i=116_2999 on theBenchmark for (2999ds/116Mi) % 13.27/2.15 % (706366)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1442705595:i=131_2999 on theBenchmark for (2999ds/131Mi) % 13.27/2.15 % (706367)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=143398136:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 13.27/2.15 % (706364)Instruction limit reached! % 13.27/2.15 % (706364)------------------------------ % 13.27/2.15 % (706364)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 13.27/2.15 % (706364)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.27/2.15 % (706364)CaDiCaL version: 2.1.3 % 13.27/2.15 % (706364)Termination reason: Instruction limit % 13.27/2.15 % (706364)Termination phase: Saturation % 13.27/2.15 % (706364)Time elapsed: 0.059 s % 13.27/2.15 % (706364)Peak memory usage: 15 MB % 13.27/2.15 % (706364)Instructions burned: 104 (million) % 13.27/2.15 % (706365)Instruction limit reached! % 13.27/2.15 % (706365)------------------------------ % 13.27/2.15 % (706365)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 13.27/2.15 % (706365)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.27/2.15 % (706365)CaDiCaL version: 2.1.3 % 13.27/2.15 % (706365)Termination reason: Instruction limit % 13.27/2.15 % (706365)Termination phase: Saturation % 13.27/2.15 % (706365)Time elapsed: 0.061 s % 13.27/2.15 % (706365)Peak memory usage: 16 MB % 13.27/2.15 % (706365)Instructions burned: 116 (million) % 13.27/2.15 % (706366)Instruction limit reached! % 13.27/2.15 % (706366)------------------------------ % 13.27/2.15 % (706366)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 13.27/2.15 % (706366)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.27/2.15 % (706366)CaDiCaL version: 2.1.3 % 13.27/2.15 % (706366)Termination reason: Instruction limit % 13.27/2.15 % (706366)Termination phase: Saturation % 13.27/2.15 % (706366)Time elapsed: 0.073 s % 13.27/2.15 % (706366)Peak memory usage: 16 MB % 13.27/2.15 % (706366)Instructions burned: 131 (million) % 13.27/2.15 % (706375)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2022945877:i=714:nm=2_2998 on theBenchmark for (2998ds/714Mi) % 13.27/2.15 % (706376)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3950909367:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi) % 13.27/2.15 % (706377)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=627375830:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi) % 13.27/2.15 % (706367)Instruction limit reached! % 13.27/2.15 % (706367)------------------------------ % 13.27/2.15 % (706367)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 13.27/2.15 % (706367)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.27/2.15 % (706367)CaDiCaL version: 2.1.3 % 13.27/2.15 % (706367)Termination reason: Instruction limit % 13.27/2.15 % (706367)Termination phase: Saturation % 13.27/2.15 % (706367)Time elapsed: 0.096 s % 13.27/2.15 % (706367)Peak memory usage: 17 MB % 13.27/2.15 % (706367)Instructions burned: 160 (million) % 13.27/2.15 % (706381)ott-21_1_sil=16000:fs=off:random_seed=1697424039:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 13.27/2.15 % (706376)Instruction limit reached! % 13.27/2.15 % (706376)------------------------------ % 13.27/2.15 % (706376)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 13.27/2.15 % (706376)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.27/2.15 % (706376)CaDiCaL version: 2.1.3 % 13.27/2.15 % (706376)Termination reason: Instruction limit % 46.53/6.94 % (706376)Termination phase: Saturation % 46.53/6.94 % (706376)Time elapsed: 0.075 s % 46.53/6.94 % (706376)Peak memory usage: 17 MB % 46.53/6.94 % (706376)Instructions burned: 132 (million) % 46.53/6.94 % (706383)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2114199266:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi) % 46.53/6.94 % (706381)Instruction limit reached! % 46.53/6.94 % (706381)------------------------------ % 46.53/6.94 % (706381)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 46.53/6.94 % (706381)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 46.53/6.94 % (706381)CaDiCaL version: 2.1.3 % 46.53/6.94 % (706381)Termination reason: Instruction limit % 46.53/6.94 % (706381)Termination phase: Saturation % 46.53/6.94 % (706381)Time elapsed: 0.102 s % 46.53/6.94 % (706381)Peak memory usage: 16 MB % 46.53/6.94 % (706381)Instructions burned: 181 (million) % 46.53/6.94 % (706385)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1581980860:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi) % 46.53/6.94 % TRYING [1] % 46.53/6.94 % TRYING [2] % 46.53/6.94 % (706377)Instruction limit reached! % 46.53/6.94 % (706377)------------------------------ % 46.53/6.94 % (706377)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 46.53/6.94 % (706377)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 46.53/6.94 % (706377)CaDiCaL version: 2.1.3 % 46.53/6.94 % (706377)Termination reason: Instruction limit % 46.53/6.94 % (706377)Termination phase: Saturation % 46.53/6.94 % (706377)Time elapsed: 0.331 s % 46.53/6.94 % (706377)Peak memory usage: 19 MB % 46.53/6.94 % (706377)Instructions burned: 685 (million) % 46.53/6.94 % (706375)Instruction limit reached! % 46.53/6.94 % (706375)------------------------------ % 46.53/6.94 % (706375)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 46.53/6.94 % (706375)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 46.53/6.94 % (706375)CaDiCaL version: 2.1.3 % 46.53/6.94 % (706375)Termination reason: Instruction limit % 46.53/6.94 % (706375)Termination phase: Finite model building preprocessing % 46.53/6.94 % (706375)Time elapsed: 0.346 s % 46.53/6.94 % (706375)Peak memory usage: 24 MB % 46.53/6.94 % (706375)Instructions burned: 714 (million) % 46.53/6.94 % (706387)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2492359661:i=1179_2995 on theBenchmark for (2995ds/1179Mi) % 46.53/6.94 % (706388)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2780267574:i=889:ins=1_2995 on theBenchmark for (2995ds/889Mi) % 46.53/6.94 % (706383)Instruction limit reached! % 46.53/6.94 % (706383)------------------------------ % 46.53/6.94 % (706383)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 46.53/6.94 % (706383)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 46.53/6.94 % (706383)CaDiCaL version: 2.1.3 % 46.53/6.94 % (706383)Termination reason: Instruction limit % 46.53/6.94 % (706383)Termination phase: Saturation % 46.53/6.94 % (706383)Time elapsed: 0.289 s % 46.53/6.94 % (706383)Peak memory usage: 18 MB % 46.53/6.94 % (706383)Instructions burned: 477 (million) % 46.53/6.94 % (706391)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=749094847:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2994 on theBenchmark for (2994ds/692Mi) % 46.53/6.94 % TRYING [1] % 46.53/6.94 % (706385)Instruction limit reached! % 46.53/6.94 % (706385)------------------------------ % 46.53/6.94 % (706385)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 46.53/6.94 % (706385)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 46.53/6.94 % (706385)CaDiCaL version: 2.1.3 % 46.53/6.94 % (706385)Termination reason: Instruction limit % 46.53/6.94 % (706385)Termination phase: Finite model building constraint generation % 46.53/6.94 % (706385)Time elapsed: 0.423 s % 46.53/6.94 % (706385)Peak memory usage: 30 MB % 46.53/6.94 % (706385)Instructions burned: 866 (million) % 46.53/6.94 % (706393)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=254185185:i=879:kws=inv_precedence:fsr=off_2992 on theBenchmark for (2992ds/879Mi) % 46.53/6.94 % (706388)Cannot represent all propositional literals internally % 46.53/6.94 % (706388)Refutation not found, incomplete strategy % 46.53/6.94 % (706388)------------------------------ % 46.53/6.94 % (706388)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 46.53/6.94 % (706388)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 74.06/10.78 % (706388)CaDiCaL version: 2.1.3 % 74.06/10.78 % (706388)Termination reason: Refutation not found, incomplete strategy % 74.06/10.78 % (706388)Time elapsed: 0.344 s % 74.06/10.78 % (706388)Peak memory usage: 26 MB % 74.06/10.78 % (706388)Instructions burned: 697 (million) % 74.06/10.78 % (706388)------------------------------ % 74.06/10.78 % (706388)------------------------------ % 74.06/10.78 % (706395)fmb+10_1_sil=64000:random_seed=4235129997:i=22061:nm=2:gsp=on_2991 on theBenchmark for (2991ds/22061Mi) % 74.06/10.78 % (706391)Instruction limit reached! % 74.06/10.78 % (706391)------------------------------ % 74.06/10.78 % (706391)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 74.06/10.78 % (706391)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 74.06/10.78 % (706391)CaDiCaL version: 2.1.3 % 74.06/10.78 % (706391)Termination reason: Instruction limit % 74.06/10.78 % (706391)Termination phase: Saturation % 74.06/10.78 % (706391)Time elapsed: 0.406 s % 74.06/10.78 % (706391)Peak memory usage: 23 MB % 74.06/10.78 % (706391)Instructions burned: 692 (million) % 74.06/10.78 % (706397)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=4051601533:i=9515:nm=5_2990 on theBenchmark for (2990ds/9515Mi) % 74.06/10.78 % (706393)Instruction limit reached! % 74.06/10.78 % (706393)------------------------------ % 74.06/10.78 % (706393)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 74.06/10.78 % (706393)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 74.06/10.78 % (706393)CaDiCaL version: 2.1.3 % 74.06/10.78 % (706393)Termination reason: Instruction limit % 74.06/10.78 % (706393)Termination phase: Saturation % 74.06/10.78 % (706393)Time elapsed: 0.421 s % 74.06/10.78 % (706393)Peak memory usage: 21 MB % 74.06/10.78 % (706393)Instructions burned: 879 (million) % 74.06/10.78 % (706399)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1099887709:fmbsr=1.7:i=920_2988 on theBenchmark for (2988ds/920Mi) % 74.06/10.78 % TRYING [1] % 74.06/10.78 % (706387)Instruction limit reached! % 74.06/10.78 % (706387)------------------------------ % 74.06/10.78 % (706387)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 74.06/10.78 % (706387)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 74.06/10.78 % (706387)CaDiCaL version: 2.1.3 % 74.06/10.78 % (706387)Termination reason: Instruction limit % 74.06/10.78 % (706387)Termination phase: Saturation % 74.06/10.78 % (706387)Time elapsed: 0.767 s % 74.06/10.78 % (706387)Peak memory usage: 29 MB % 74.06/10.78 % (706387)Instructions burned: 1180 (million) % 74.06/10.78 % (706401)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=3591524817:i=5131_2987 on theBenchmark for (2987ds/5131Mi) % 74.06/10.78 % (706397)Cannot represent all propositional literals internally % 74.06/10.78 % (706397)Refutation not found, incomplete strategy % 74.06/10.78 % (706397)------------------------------ % 74.06/10.78 % (706397)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 74.06/10.78 % (706397)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 74.06/10.78 % (706397)CaDiCaL version: 2.1.3 % 74.06/10.78 % (706397)Termination reason: Refutation not found, incomplete strategy % 74.06/10.78 % (706397)Time elapsed: 0.348 s % 74.06/10.78 % (706397)Peak memory usage: 25 MB % 74.06/10.78 % (706397)Instructions burned: 696 (million) % 74.06/10.78 % (706397)------------------------------ % 74.06/10.78 % (706397)------------------------------ % 74.06/10.78 % (706403)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3279494613:i=1472:ins=7:fdi=8:gsp=on_2986 on theBenchmark for (2986ds/1472Mi) % 74.06/10.78 % (706399)Cannot represent all propositional literals internally % 74.06/10.78 % (706399)Refutation not found, incomplete strategy % 74.06/10.78 % (706399)------------------------------ % 74.06/10.78 % (706399)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 74.06/10.78 % (706399)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 74.06/10.78 % (706399)CaDiCaL version: 2.1.3 % 74.06/10.78 % (706399)Termination reason: Refutation not found, incomplete strategy % 74.06/10.78 % (706399)Time elapsed: 0.345 s % 74.06/10.78 % (706399)Peak memory usage: 25 MB % 74.06/10.78 % (706399)Instructions burned: 696 (million) % 74.06/10.78 % (706399)------------------------------ % 74.06/10.78 % (706399)------------------------------ % 74.06/10.78 % (706405)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=2487456232:i=6324_2984 on theBenchmark for (2984ds/6324Mi) % 74.06/10.78 % TRYING [2] % 74.06/10.78 % (706405)Cannot represent all propositional literals internally % 74.06/10.78 % (706405)Refutation not found, incomplete strategy % 101.74/14.66 % (706405)------------------------------ % 101.74/14.66 % (706405)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 101.74/14.66 % (706405)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 101.74/14.66 % (706405)CaDiCaL version: 2.1.3 % 101.74/14.66 % (706405)Termination reason: Refutation not found, incomplete strategy % 101.74/14.66 % (706405)Time elapsed: 0.356 s % 101.74/14.66 % (706405)Peak memory usage: 26 MB % 101.74/14.66 % (706405)Instructions burned: 717 (million) % 101.74/14.66 % (706405)------------------------------ % 101.74/14.66 % (706405)------------------------------ % 101.74/14.66 % (706407)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1375500345:fmbsr=2.30978:i=2174_2980 on theBenchmark for (2980ds/2174Mi) % 101.74/14.66 % (706403)Instruction limit reached! % 101.74/14.66 % (706403)------------------------------ % 101.74/14.66 % (706403)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 101.74/14.66 % (706403)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 101.74/14.66 % (706403)CaDiCaL version: 2.1.3 % 101.74/14.66 % (706403)Termination reason: Instruction limit % 101.74/14.66 % (706403)Termination phase: Saturation % 101.74/14.66 % (706403)Time elapsed: 0.874 s % 101.74/14.66 % (706403)Peak memory usage: 35 MB % 101.74/14.66 % (706403)Instructions burned: 1473 (million) % 101.74/14.66 % (706409)ott-2_1_sil=16000:newcnf=on:random_seed=3616751823:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2977 on theBenchmark for (2977ds/869Mi) % 101.74/14.66 % (706409)Instruction limit reached! % 101.74/14.66 % (706409)------------------------------ % 101.74/14.66 % (706409)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 101.74/14.66 % (706409)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 101.74/14.66 % (706409)CaDiCaL version: 2.1.3 % 101.74/14.66 % (706409)Termination reason: Instruction limit % 101.74/14.66 % (706409)Termination phase: Saturation % 101.74/14.66 % (706409)Time elapsed: 0.441 s % 101.74/14.66 % (706409)Peak memory usage: 19 MB % 101.74/14.66 % (706409)Instructions burned: 870 (million) % 101.74/14.66 % (706411)ott+10_1_sil=32000:tgt=ground:random_seed=2179278320:i=5114:av=off_2972 on theBenchmark for (2972ds/5114Mi) % 101.74/14.66 % (706407)Instruction limit reached! % 101.74/14.66 % (706407)------------------------------ % 101.74/14.66 % (706407)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 101.74/14.66 % (706407)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 101.74/14.66 % (706407)CaDiCaL version: 2.1.3 % 101.74/14.66 % (706407)Termination reason: Instruction limit % 101.74/14.66 % (706407)Termination phase: Finite model building preprocessing % 101.74/14.66 % (706407)Time elapsed: 1.088 s % 101.74/14.66 % (706407)Peak memory usage: 42 MB % 101.74/14.66 % (706407)Instructions burned: 2174 (million) % 101.74/14.66 % (706413)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2484509890:i=54282_2969 on theBenchmark for (2969ds/54282Mi) % 101.74/14.66 % TRYING [1] % 101.74/14.66 % TRYING [2] % 101.74/14.66 % (706401)Instruction limit reached! % 101.74/14.66 % (706401)------------------------------ % 101.74/14.66 % (706401)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 101.74/14.66 % (706401)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 101.74/14.66 % (706401)CaDiCaL version: 2.1.3 % 101.74/14.66 % (706401)Termination reason: Instruction limit % 101.74/14.66 % (706401)Termination phase: Saturation % 101.74/14.66 % (706401)Time elapsed: 3.170 s % 101.74/14.66 % (706401)Peak memory usage: 53 MB % 101.74/14.66 % (706401)Instructions burned: 5133 (million) % 101.74/14.66 % (706415)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3047040063:i=3512:aac=none_2955 on theBenchmark for (2955ds/3512Mi) % 101.74/14.66 % (706411)Instruction limit reached! % 101.74/14.66 % (706411)------------------------------ % 101.74/14.66 % (706411)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 101.74/14.66 % (706411)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 101.74/14.66 % (706411)CaDiCaL version: 2.1.3 % 101.74/14.66 % (706411)Termination reason: Instruction limit % 101.74/14.66 % (706411)Termination phase: Saturation % 101.74/14.66 % (706411)Time elapsed: 3.379 s % 101.74/14.66 % (706411)Peak memory usage: 68 MB % 101.74/14.66 % (706411)Instructions burned: 5114 (million) % 101.74/14.66 % (706417)dis+21_1_sil=32000:sas=cadical:random_seed=4163672813:i=3773:amm=off_2938 on theBenchmark for (2938ds/3773Mi) % 101.74/14.66 % (706415)Instruction limit reached! % 101.74/14.66 % (706415)------------------------------ % 101.74/14.66 % (706415)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 174.85/25.00 % (706415)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 174.85/25.00 % (706415)CaDiCaL version: 2.1.3 % 174.85/25.00 % (706415)Termination reason: Instruction limit % 174.85/25.00 % (706415)Termination phase: Saturation % 174.85/25.00 % (706415)Time elapsed: 2.219 s % 174.85/25.00 % (706415)Peak memory usage: 48 MB % 174.85/25.00 % (706415)Instructions burned: 3512 (million) % 174.85/25.00 % (706419)ott+11_1_sil=16000:gs=on:random_seed=602717087:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2932 on theBenchmark for (2932ds/2251Mi) % 174.85/25.00 % (706361)Cannot represent all propositional literals internally % 174.85/25.00 % (706419)Instruction limit reached! % 174.85/25.00 % (706419)------------------------------ % 174.85/25.00 % (706419)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 174.85/25.00 % (706419)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 174.85/25.00 % (706419)CaDiCaL version: 2.1.3 % 174.85/25.00 % (706419)Termination reason: Instruction limit % 174.85/25.00 % (706419)Termination phase: Saturation % 174.85/25.00 % (706419)Time elapsed: 1.425 s % 174.85/25.00 % (706419)Peak memory usage: 61 MB % 174.85/25.00 % (706419)Instructions burned: 2251 (million) % 174.85/25.00 % (706421)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=117210951:fmbsr=1.6:i=67534_2918 on theBenchmark for (2918ds/67534Mi) % 174.85/25.00 % (706417)Instruction limit reached! % 174.85/25.00 % (706417)------------------------------ % 174.85/25.00 % (706417)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 174.85/25.00 % (706417)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 174.85/25.00 % (706417)CaDiCaL version: 2.1.3 % 174.85/25.00 % (706417)Termination reason: Instruction limit % 174.85/25.00 % (706417)Termination phase: Saturation % 174.85/25.00 % (706417)Time elapsed: 2.337 s % 174.85/25.00 % (706417)Peak memory usage: 43 MB % 174.85/25.00 % (706417)Instructions burned: 3773 (million) % 174.85/25.00 % (706423)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=3172609199:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2915 on theBenchmark for (2915ds/4591Mi) % 174.85/25.00 % (706421)Cannot represent all propositional literals internally % 174.85/25.00 % (706421)Refutation not found, incomplete strategy % 174.85/25.00 % (706421)------------------------------ % 174.85/25.00 % (706421)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 174.85/25.00 % (706421)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 174.85/25.00 % (706421)CaDiCaL version: 2.1.3 % 174.85/25.00 % (706421)Termination reason: Refutation not found, incomplete strategy % 174.85/25.00 % (706421)Time elapsed: 0.362 s % 174.85/25.00 % (706421)Peak memory usage: 24 MB % 174.85/25.00 % (706421)Instructions burned: 727 (million) % 174.85/25.00 % (706421)------------------------------ % 174.85/25.00 % (706421)------------------------------ % 174.85/25.00 % (706425)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=1441874688:i=29340_2914 on theBenchmark for (2914ds/29340Mi) % 174.85/25.00 % (706361)Refutation not found, incomplete strategy % 174.85/25.00 % (706361)------------------------------ % 174.85/25.00 % (706361)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 174.85/25.00 % (706361)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 174.85/25.00 % (706361)CaDiCaL version: 2.1.3 % 174.85/25.00 % (706361)Termination reason: Refutation not found, incomplete strategy % 174.85/25.00 % (706361)Time elapsed: 8.836 s % 174.85/25.00 % (706361)Peak memory usage: 983 MB % 174.85/25.00 % (706361)Instructions burned: 14877 (million) % 174.85/25.00 % (706361)------------------------------ % 174.85/25.00 % (706361)------------------------------ % 174.85/25.00 % (706427)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=2363749495:i=5211_2909 on theBenchmark for (2909ds/5211Mi) % 174.85/25.00 % (706423)Instruction limit reached! % 174.85/25.00 % (706423)------------------------------ % 174.85/25.00 % (706423)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 174.85/25.00 % (706423)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 174.85/25.00 % (706423)CaDiCaL version: 2.1.3 % 174.85/25.00 % (706423)Termination reason: Instruction limit % 174.85/25.00 % (706423)Termination phase: Saturation % 174.85/25.00 % (706423)Time elapsed: 2.038 s % 174.85/25.00 % (706423)Peak memory usage: 43 MB % 174.85/25.00 % (706423)Instructions burned: 4591 (million) % 174.85/25.00 % (706429)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=2903966778:i=5497:nm=2_2894 on theBenchmark for (2894ds/5497Mi) % 190.81/27.21 % (706429)Cannot represent all propositional literals internally % 190.81/27.21 % (706429)Refutation not found, incomplete strategy % 190.81/27.21 % (706429)------------------------------ % 190.81/27.21 % (706429)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 190.81/27.21 % (706429)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 190.81/27.21 % (706429)CaDiCaL version: 2.1.3 % 190.81/27.21 % (706429)Termination reason: Refutation not found, incomplete strategy % 190.81/27.21 % (706429)Time elapsed: 0.357 s % 190.81/27.21 % (706429)Peak memory usage: 26 MB % 190.81/27.21 % (706429)Instructions burned: 717 (million) % 190.81/27.21 % (706429)------------------------------ % 190.81/27.21 % (706429)------------------------------ % 190.81/27.21 % (706431)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=128517879:fmbsr=2:i=46332_2890 on theBenchmark for (2890ds/46332Mi) % 190.81/27.21 % (706413)Cannot represent all propositional literals internally % 190.81/27.21 % (706431)Cannot represent all propositional literals internally % 190.81/27.21 % (706431)Refutation not found, incomplete strategy % 190.81/27.21 % (706431)------------------------------ % 190.81/27.21 % (706431)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 190.81/27.21 % (706431)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 190.81/27.21 % (706431)CaDiCaL version: 2.1.3 % 190.81/27.21 % (706431)Termination reason: Refutation not found, incomplete strategy % 190.81/27.21 % (706431)Time elapsed: 0.354 s % 190.81/27.21 % (706431)Peak memory usage: 24 MB % 190.81/27.21 % (706431)Instructions burned: 726 (million) % 190.81/27.21 % (706431)------------------------------ % 190.81/27.21 % (706431)------------------------------ % 190.81/27.21 % (706433)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=277402605:i=14071_2887 on theBenchmark for (2887ds/14071Mi) % 190.81/27.21 % (706427)Instruction limit reached! % 190.81/27.21 % (706427)------------------------------ % 190.81/27.21 % (706427)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 190.81/27.21 % (706427)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 190.81/27.21 % (706427)CaDiCaL version: 2.1.3 % 190.81/27.21 % (706427)Termination reason: Instruction limit % 190.81/27.21 % (706427)Termination phase: Saturation % 190.81/27.21 % (706427)Time elapsed: 2.507 s % 190.81/27.21 % (706427)Peak memory usage: 44 MB % 190.81/27.21 % (706427)Instructions burned: 5212 (million) % 190.81/27.21 % (706435)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=4017455979:i=22565:add=on:rawr=on_2884 on theBenchmark for (2884ds/22565Mi) % 190.81/27.21 % (706433)Cannot represent all propositional literals internally % 190.81/27.21 % (706433)Refutation not found, incomplete strategy % 190.81/27.21 % (706433)------------------------------ % 190.81/27.21 % (706433)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 190.81/27.21 % (706433)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 190.81/27.21 % (706433)CaDiCaL version: 2.1.3 % 190.81/27.21 % (706433)Termination reason: Refutation not found, incomplete strategy % 190.81/27.21 % (706433)Time elapsed: 0.356 s % 190.81/27.21 % (706433)Peak memory usage: 26 MB % 190.81/27.21 % (706433)Instructions burned: 696 (million) % 190.81/27.21 % (706433)------------------------------ % 190.81/27.21 % (706433)------------------------------ % 190.81/27.21 % (706437)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=1928425110:i=8173:av=off_2883 on theBenchmark for (2883ds/8173Mi) % 190.81/27.21 % (706413)Refutation not found, incomplete strategy % 190.81/27.21 % (706413)------------------------------ % 190.81/27.21 % (706413)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 190.81/27.21 % (706413)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 190.81/27.21 % (706413)CaDiCaL version: 2.1.3 % 190.81/27.21 % (706413)Termination reason: Refutation not found, incomplete strategy % 190.81/27.21 % (706413)Time elapsed: 8.911 s % 190.81/27.21 % (706413)Peak memory usage: 983 MB % 190.81/27.21 % (706413)Instructions burned: 14878 (million) % 190.81/27.21 % (706413)------------------------------ % 190.81/27.21 % (706413)------------------------------ % 190.81/27.21 % (706439)dis+10_16:1_sil=16000:random_seed=316366067:i=9155:fsr=off_2879 on theBenchmark for (2879ds/9155Mi) % 190.81/27.21 % (706395)Instruction limit reached! % 190.81/27.21 % (706395)------------------------------ % 190.81/27.21 % (706395)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 190.81/27.21 % (706395)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 220.28/31.40 % (706395)CaDiCaL version: 2.1.3 % 220.28/31.40 % (706395)Termination reason: Instruction limit % 220.28/31.40 % (706395)Termination phase: Finite model building SAT solving % 220.28/31.40 % (706395)Time elapsed: 13.551 s % 220.28/31.40 % (706395)Peak memory usage: 743 MB % 220.28/31.40 % (706395)Instructions burned: 22064 (million) % 220.28/31.40 % (706441)ott-3_8_sil=64000:random_seed=2487851075:i=20139:bs=on_2854 on theBenchmark for (2854ds/20139Mi) % 220.28/31.40 % (706437)Instruction limit reached! % 220.28/31.40 % (706437)------------------------------ % 220.28/31.40 % (706437)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 220.28/31.40 % (706437)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 220.28/31.40 % (706437)CaDiCaL version: 2.1.3 % 220.28/31.40 % (706437)Termination reason: Instruction limit % 220.28/31.40 % (706437)Termination phase: Saturation % 220.28/31.40 % (706437)Time elapsed: 5.440 s % 220.28/31.40 % (706437)Peak memory usage: 107 MB % 220.28/31.40 % (706437)Instructions burned: 8173 (million) % 220.28/31.40 % (706443)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=490600369:fmbsr=2:i=32576_2828 on theBenchmark for (2828ds/32576Mi) % 220.28/31.40 % (706439)Instruction limit reached! % 220.28/31.40 % (706439)------------------------------ % 220.28/31.40 % (706439)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 220.28/31.40 % (706439)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 220.28/31.40 % (706439)CaDiCaL version: 2.1.3 % 220.28/31.40 % (706439)Termination reason: Instruction limit % 220.28/31.40 % (706439)Termination phase: Saturation % 220.28/31.40 % (706439)Time elapsed: 5.176 s % 220.28/31.40 % (706439)Peak memory usage: 90 MB % 220.28/31.40 % (706439)Instructions burned: 9156 (million) % 220.28/31.40 % (706445)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=3468578688:i=11404_2827 on theBenchmark for (2827ds/11404Mi) % 220.28/31.40 % (706443)Cannot represent all propositional literals internally % 220.28/31.40 % (706443)Refutation not found, incomplete strategy % 220.28/31.40 % (706443)------------------------------ % 220.28/31.40 % (706443)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 220.28/31.40 % (706443)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 220.28/31.40 % (706443)CaDiCaL version: 2.1.3 % 220.28/31.40 % (706443)Termination reason: Refutation not found, incomplete strategy % 220.28/31.40 % (706443)Time elapsed: 0.354 s % 220.28/31.40 % (706443)Peak memory usage: 26 MB % 220.28/31.40 % (706443)Instructions burned: 718 (million) % 220.28/31.40 % (706443)------------------------------ % 220.28/31.40 % (706443)------------------------------ % 220.28/31.40 % (706447)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=2444980850:i=14134_2824 on theBenchmark for (2824ds/14134Mi) % 220.28/31.40 % (706363)Instruction limit reached! % 220.28/31.40 % (706363)------------------------------ % 220.28/31.40 % (706363)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 220.28/31.40 % (706363)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 220.28/31.40 % (706363)CaDiCaL version: 2.1.3 % 220.28/31.40 % (706363)Termination reason: Instruction limit % 220.28/31.40 % (706363)Termination phase: Saturation % 220.28/31.40 % (706363)Time elapsed: 21.664 s % 220.28/31.40 % (706363)Peak memory usage: 476 MB % 220.28/31.40 % (706363)Instructions burned: 88026 (million) % 220.28/31.40 % (706449)dis+33_16_sil=32000:sac=on:random_seed=461838557:i=15851:nm=0_2782 on theBenchmark for (2782ds/15851Mi) % 220.28/31.40 % (706425)Instruction limit reached! % 220.28/31.40 % (706425)------------------------------ % 220.28/31.40 % (706425)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 220.28/31.40 % (706425)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 220.28/31.40 % (706425)CaDiCaL version: 2.1.3 % 220.28/31.40 % (706425)Termination reason: Instruction limit % 220.28/31.40 % (706425)Termination phase: Saturation % 220.28/31.40 % (706425)Time elapsed: 13.382 s % 220.28/31.40 % (706425)Peak memory usage: 447 MB % 220.28/31.40 % (706425)Instructions burned: 29341 (million) % 220.28/31.40 % (706451)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=316029909:avsq=on:i=17627:add=on:amm=off_2779 on theBenchmark for (2779ds/17627Mi) % 220.28/31.40 % (706445)Instruction limit reached! % 220.28/31.40 % (706445)------------------------------ % 220.28/31.40 % (706445)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 220.28/31.40 % (706445)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 220.28/31.40 % (706445)CaDiCaL version: 2.1.3 % 220.28/31.40 % (706445)Termination reason: Instruction limit % 232.56/33.04 % (706445)Termination phase: Saturation % 232.56/33.04 % (706445)Time elapsed: 7.467 s % 232.56/33.04 % (706445)Peak memory usage: 169 MB % 232.56/33.04 % (706445)Instructions burned: 11408 (million) % 232.56/33.04 % (706453)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=2313306655:s2a=on:i=53295_2752 on theBenchmark for (2752ds/53295Mi) % 232.56/33.04 % (706449)Instruction limit reached! % 232.56/33.04 % (706449)------------------------------ % 232.56/33.04 % (706449)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 232.56/33.04 % (706449)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 232.56/33.04 % (706449)CaDiCaL version: 2.1.3 % 232.56/33.04 % (706449)Termination reason: Instruction limit % 232.56/33.04 % (706449)Termination phase: Saturation % 232.56/33.04 % (706449)Time elapsed: 4.186 s % 232.56/33.04 % (706449)Peak memory usage: 225 MB % 232.56/33.04 % (706449)Instructions burned: 15852 (million) % 232.56/33.04 % (706455)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=3270919269:i=26857:ins=20_2740 on theBenchmark for (2740ds/26857Mi) % 232.56/33.04 % (706435)Instruction limit reached! % 232.56/33.04 % (706435)------------------------------ % 232.56/33.04 % (706435)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 232.56/33.04 % (706435)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 232.56/33.04 % (706435)CaDiCaL version: 2.1.3 % 232.56/33.04 % (706435)Termination reason: Instruction limit % 232.56/33.04 % (706435)Termination phase: Saturation % 232.56/33.04 % (706435)Time elapsed: 14.602 s % 232.56/33.04 % (706435)Peak memory usage: 467 MB % 232.56/33.04 % (706435)Instructions burned: 22565 (million) % 232.56/33.04 % (706455)Cannot represent all propositional literals internally % 232.56/33.04 % (706455)Refutation not found, incomplete strategy % 232.56/33.04 % (706455)------------------------------ % 232.56/33.04 % (706455)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 232.56/33.04 % (706455)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 232.56/33.04 % (706455)CaDiCaL version: 2.1.3 % 232.56/33.04 % (706455)Termination reason: Refutation not found, incomplete strategy % 232.56/33.04 % (706455)Time elapsed: 0.184 s % 232.56/33.04 % (706455)Peak memory usage: 25 MB % 232.56/33.04 % (706455)Instructions burned: 696 (million) % 232.56/33.04 % (706455)------------------------------ % 232.56/33.04 % (706455)------------------------------ % 232.56/33.04 % (706457)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=1546745044:i=28120:bs=on:fsr=off_2738 on theBenchmark for (2738ds/28120Mi) % 232.56/33.04 % (706459)fmb+10_1_sil=256000:fmbss=7:random_seed=246041706:fmbsr=1.6:i=182295_2737 on theBenchmark for (2737ds/182295Mi) % 232.56/33.04 % (706459)Cannot represent all propositional literals internally % 232.56/33.04 % (706459)Refutation not found, incomplete strategy % 232.56/33.04 % (706459)------------------------------ % 232.56/33.04 % (706459)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 232.56/33.04 % (706459)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 232.56/33.04 % (706459)CaDiCaL version: 2.1.3 % 232.56/33.04 % (706459)Termination reason: Refutation not found, incomplete strategy % 232.56/33.04 % (706459)Time elapsed: 0.345 s % 232.56/33.04 % (706459)Peak memory usage: 25 MB % 232.56/33.04 % (706459)Instructions burned: 696 (million) % 232.56/33.04 % (706459)------------------------------ % 232.56/33.04 % (706459)------------------------------ % 232.56/33.04 % (706461)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=2052407357:i=44625:gsp=on_2733 on theBenchmark for (2733ds/44625Mi) % 232.56/33.04 % (706461)Cannot represent all propositional literals internally % 232.56/33.04 % (706461)Refutation not found, incomplete strategy % 232.56/33.04 % (706461)------------------------------ % 232.56/33.04 % (706461)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 232.56/33.04 % (706461)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 232.56/33.04 % (706461)CaDiCaL version: 2.1.3 % 232.56/33.04 % (706461)Termination reason: Refutation not found, incomplete strategy % 232.56/33.04 % (706461)Time elapsed: 0.344 s % 232.56/33.04 % (706461)Peak memory usage: 26 MB % 232.56/33.04 % (706461)Instructions burned: 694 (million) % 232.56/33.04 % (706461)------------------------------ % 232.56/33.04 % (706461)------------------------------ % 232.56/33.04 % (706447)Instruction limit reached! % 232.56/33.04 % (706447)------------------------------ % 232.56/33.04 % (706447)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 232.56/33.04 % (706447)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 263.17/37.41 % (706447)CaDiCaL version: 2.1.3 % 263.17/37.41 % (706447)Termination reason: Instruction limit % 263.17/37.41 % (706447)Termination phase: Saturation % 263.17/37.41 % (706447)Time elapsed: 9.428 s % 263.17/37.41 % (706447)Peak memory usage: 129 MB % 263.17/37.41 % (706447)Instructions burned: 14136 (million) % 263.17/37.41 % (706463)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=3182607857:i=160505_2730 on theBenchmark for (2730ds/160505Mi) % 263.17/37.41 % (706465)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=2781161361:fmbsr=1.3:i=225729_2729 on theBenchmark for (2729ds/225729Mi) % 263.17/37.41 % (706463)Cannot represent all propositional literals internally % 263.17/37.41 % (706463)Refutation not found, incomplete strategy % 263.17/37.41 % (706463)------------------------------ % 263.17/37.41 % (706463)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 263.17/37.41 % (706463)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 263.17/37.41 % (706463)CaDiCaL version: 2.1.3 % 263.17/37.41 % (706463)Termination reason: Refutation not found, incomplete strategy % 263.17/37.41 % (706463)Time elapsed: 0.348 s % 263.17/37.41 % (706463)Peak memory usage: 25 MB % 263.17/37.41 % (706463)Instructions burned: 696 (million) % 263.17/37.41 % (706463)------------------------------ % 263.17/37.41 % (706463)------------------------------ % 263.17/37.41 % (706465)Cannot represent all propositional literals internally % 263.17/37.41 % (706465)Refutation not found, incomplete strategy % 263.17/37.41 % (706465)------------------------------ % 263.17/37.41 % (706465)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 263.17/37.41 % (706465)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 263.17/37.41 % (706465)CaDiCaL version: 2.1.3 % 263.17/37.41 % (706465)Termination reason: Refutation not found, incomplete strategy % 263.17/37.41 % (706465)Time elapsed: 0.347 s % 263.17/37.41 % (706465)Peak memory usage: 26 MB % 263.17/37.41 % (706465)Instructions burned: 696 (million) % 263.17/37.41 % (706467)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=2800821036:fmbsr=2:i=185024:ins=7_2726 on theBenchmark for (2726ds/185024Mi) % 263.17/37.41 % (706465)------------------------------ % 263.17/37.41 % (706465)------------------------------ % 263.17/37.41 % (706469)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=1901490234:rtra=on_2726 on theBenchmark for (2726ds/0Mi) % 263.17/37.41 % (706441)Instruction limit reached! % 263.17/37.41 % (706441)------------------------------ % 263.17/37.41 % (706441)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 263.17/37.41 % (706441)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 263.17/37.41 % (706441)CaDiCaL version: 2.1.3 % 263.17/37.41 % (706441)Termination reason: Instruction limit % 263.17/37.41 % (706441)Termination phase: Saturation % 263.17/37.41 % (706441)Time elapsed: 13.073 s % 263.17/37.41 % (706441)Peak memory usage: 124 MB % 263.17/37.41 % (706441)Instructions burned: 20140 (million) % 263.17/37.41 % (706471)% WARNING: option uhcvi not known. % 263.17/37.41 % (706471)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1014140956:i=271062:add=off:rtra=on:rawr=on_2723 on theBenchmark for (2723ds/271062Mi) % 263.17/37.41 % (706467)Cannot represent all propositional literals internally % 263.17/37.41 % (706467)Refutation not found, incomplete strategy % 263.17/37.41 % (706467)------------------------------ % 263.17/37.41 % (706467)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 263.17/37.41 % (706467)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 263.17/37.41 % (706467)CaDiCaL version: 2.1.3 % 263.17/37.41 % (706467)Termination reason: Refutation not found, incomplete strategy % 263.17/37.41 % (706467)Time elapsed: 0.350 s % 263.17/37.41 % (706467)Peak memory usage: 26 MB % 263.17/37.41 % (706467)Instructions burned: 696 (million) % 263.17/37.41 % (706467)------------------------------ % 263.17/37.41 % (706467)------------------------------ % 263.17/37.41 % (706473)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2496800464:i=176048:add=on:rtra=on:rawr=on_2722 on theBenchmark for (2722ds/176048Mi) % 263.17/37.41 % TRYING [1] % 263.17/37.41 % TRYING [2] % 263.17/37.41 % (706451)Instruction limit reached! % 263.17/37.41 % (706451)------------------------------ % 263.17/37.41 % (706451)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 263.17/37.41 % (706451)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 263.17/37.41 % (706451)CaDiCaL version: 2.1.3 % 263.17/37.41 % (706451)Termination reason: Instruction limit % 263.17/37.41 % (706451)Termination phase: Saturation % 279.38/39.83 % (706451)Time elapsed: 9.122 s % 279.38/39.83 % (706451)Peak memory usage: 120 MB % 279.38/39.83 % (706451)Instructions burned: 17629 (million) % 279.38/39.83 % (706475)dis+10_1_sil=32000:si=on:sp=arity:random_seed=2360953238:i=206:fgj=on:rtra=on_2688 on theBenchmark for (2688ds/206Mi) % 279.38/39.83 % (706475)Instruction limit reached! % 279.38/39.83 % (706475)------------------------------ % 279.38/39.83 % (706475)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 279.38/39.83 % (706475)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 279.38/39.83 % (706475)CaDiCaL version: 2.1.3 % 279.38/39.83 % (706475)Termination reason: Instruction limit % 279.38/39.83 % (706475)Termination phase: Saturation % 279.38/39.83 % (706475)Time elapsed: 0.137 s % 279.38/39.83 % (706475)Peak memory usage: 17 MB % 279.38/39.83 % (706475)Instructions burned: 207 (million) % 279.38/39.83 % (706477)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=1811797421:i=232:rtra=on_2686 on theBenchmark for (2686ds/232Mi) % 279.38/39.83 % (706477)Instruction limit reached! % 279.38/39.83 % (706477)------------------------------ % 279.38/39.83 % (706477)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 279.38/39.83 % (706477)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 279.38/39.83 % (706477)CaDiCaL version: 2.1.3 % 279.38/39.83 % (706477)Termination reason: Instruction limit % 279.38/39.83 % (706477)Termination phase: Saturation % 279.38/39.83 % (706477)Time elapsed: 0.145 s % 279.38/39.83 % (706477)Peak memory usage: 17 MB % 279.38/39.83 % (706477)Instructions burned: 232 (million) % 279.38/39.83 % (706479)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=1034945235:i=262:rtra=on_2684 on theBenchmark for (2684ds/262Mi) % 279.38/39.83 % (706479)Instruction limit reached! % 279.38/39.83 % (706479)------------------------------ % 279.38/39.83 % (706479)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 279.38/39.83 % (706479)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 279.38/39.83 % (706479)CaDiCaL version: 2.1.3 % 279.38/39.83 % (706479)Termination reason: Instruction limit % 279.38/39.83 % (706479)Termination phase: Saturation % 279.38/39.83 % (706479)Time elapsed: 0.166 s % 279.38/39.83 % (706479)Peak memory usage: 19 MB % 279.38/39.83 % (706479)Instructions burned: 262 (million) % 279.38/39.83 % (706481)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=1589182463:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2682 on theBenchmark for (2682ds/318Mi) % 279.38/39.83 % (706481)Instruction limit reached! % 279.38/39.83 % (706481)------------------------------ % 279.38/39.83 % (706481)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 279.38/39.83 % (706481)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 279.38/39.83 % (706481)CaDiCaL version: 2.1.3 % 279.38/39.83 % (706481)Termination reason: Instruction limit % 279.38/39.83 % (706481)Termination phase: Saturation % 279.38/39.83 % (706481)Time elapsed: 0.213 s % 279.38/39.83 % (706481)Peak memory usage: 19 MB % 279.38/39.83 % (706481)Instructions burned: 318 (million) % 279.38/39.83 % (706483)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=34806262:i=1428:nm=2:rtra=on_2680 on theBenchmark for (2680ds/1428Mi) % 279.38/39.83 % TRYING [1] % 279.38/39.83 % TRYING [2] % 279.38/39.83 % (706483)Instruction limit reached! % 279.38/39.83 % (706483)------------------------------ % 279.38/39.83 % (706483)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 279.38/39.83 % (706483)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 279.38/39.83 % (706483)CaDiCaL version: 2.1.3 % 279.38/39.83 % (706483)Termination reason: Instruction limit % 279.38/39.83 % (706483)Termination phase: Finite model building constraint generation % 279.38/39.83 % (706483)Time elapsed: 0.645 s % 279.38/39.83 % (706483)Peak memory usage: 58 MB % 279.38/39.83 % (706483)Instructions burned: 1429 (million) % 279.38/39.83 % (706485)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=525621536:i=262:bd=preordered:rtra=on:fsd=on_2673 on theBenchmark for (2673ds/262Mi) % 279.38/39.83 % (706485)Instruction limit reached! % 279.38/39.83 % (706485)------------------------------ % 279.38/39.83 % (706485)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 279.38/39.83 % (706485)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 279.38/39.83 % (706485)CaDiCaL version: 2.1.3 % 279.38/39.83 % (706485)Termination reason: Instruction limit % 279.38/39.83 % (706485)Termination phase: Saturation % 279.38/39.83 % (706485)Time elapsed: 0.181 s % 279.38/39.83 % (706485)Peak memory usage: 18 MB % 279.38/39.83 % (706485)Instructions burned: 262 (million) % 300.50/42.73 % (706487)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:si=on:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=3144178264:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2671 on theBenchmark for (2671ds/1368Mi) % 300.50/42.73 % (706487)Instruction limit reached! % 300.50/42.73 % (706487)------------------------------ % 300.50/42.73 % (706487)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.50/42.73 % (706487)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.50/42.73 % (706487)CaDiCaL version: 2.1.3 % 300.50/42.73 % (706487)Termination reason: Instruction limit % 300.50/42.73 % (706487)Termination phase: Saturation % 300.50/42.73 % (706487)Time elapsed: 0.679 s % 300.50/42.73 % (706487)Peak memory usage: 23 MB % 300.50/42.73 % (706487)Instructions burned: 1369 (million) % 300.50/42.73 % (706489)ott-21_1_sil=16000:si=on:fs=off:random_seed=567138089:i=360:av=off:fsr=off:rtra=on_2664 on theBenchmark for (2664ds/360Mi) % 300.50/42.73 % (706489)Instruction limit reached! % 300.50/42.73 % (706489)------------------------------ % 300.50/42.73 % (706489)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.50/42.73 % (706489)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.50/42.73 % (706489)CaDiCaL version: 2.1.3 % 300.50/42.73 % (706489)Termination reason: Instruction limit % 300.50/42.73 % (706489)Termination phase: Saturation % 300.50/42.73 % (706489)Time elapsed: 0.211 s % 300.50/42.73 % (706489)Peak memory usage: 18 MB % 300.50/42.73 % (706489)Instructions burned: 361 (million) % 300.50/42.73 % (706491)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2944453410:i=954:bd=all:rtra=on_2662 on theBenchmark for (2662ds/954Mi) % 300.50/42.73 % (706491)Instruction limit reached! % 300.50/42.73 % (706491)------------------------------ % 300.50/42.73 % (706491)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.50/42.73 % (706491)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.50/42.73 % (706491)CaDiCaL version: 2.1.3 % 300.50/42.73 % (706491)Termination reason: Instruction limit % 300.50/42.73 % (706491)Termination phase: Saturation % 300.50/42.73 % (706491)Time elapsed: 0.612 s % 300.50/42.73 % (706491)Peak memory usage: 19 MB % 300.50/42.73 % (706491)Instructions burned: 955 (million) % 300.50/42.73 % (706493)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=969214658:fmbsr=1.3:i=1730:ins=25:rtra=on_2656 on theBenchmark for (2656ds/1730Mi) % 300.50/42.73 % TRYING [1] % 300.50/42.73 % (706493)Instruction limit reached! % 300.50/42.73 % (706493)------------------------------ % 300.50/42.73 % (706493)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.50/42.73 % (706493)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.50/42.73 % (706493)CaDiCaL version: 2.1.3 % 300.50/42.73 % (706493)Termination reason: Instruction limit % 300.50/42.73 % (706493)Termination phase: Finite model building constraint generation % 300.50/42.73 % (706493)Time elapsed: 0.852 s % 300.50/42.73 % (706493)Peak memory usage: 124 MB % 300.50/42.73 % (706493)Instructions burned: 1732 (million) % 300.50/42.73 % (706495)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=189318229:i=2358:rtra=on_2647 on theBenchmark for (2647ds/2358Mi) % 300.50/42.73 % (706495)Instruction limit reached! % 300.50/42.73 % (706495)------------------------------ % 300.50/42.73 % (706495)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.50/42.73 % (706495)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.50/42.73 % (706495)CaDiCaL version: 2.1.3 % 300.50/42.73 % (706495)Termination reason: Instruction limit % 300.50/42.73 % (706495)Termination phase: Saturation % 300.50/42.73 % (706495)Time elapsed: 1.493 s % 300.50/42.73 % (706495)Peak memory usage: 42 MB % 300.50/42.73 % (706495)Instructions burned: 2358 (million) % 300.50/42.73 % (706497)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=4259370509:i=1778:ins=1:rtra=on_2632 on theBenchmark for (2632ds/1778Mi) % 300.50/42.73 % (706497)Cannot represent all propositional literals internally % 300.50/42.73 % (706497)Refutation not found, incomplete strategy % 300.50/42.73 % (706497)------------------------------ % 300.50/42.73 % (706497)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.50/42.73 % (706497)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.50/42.73 % (706497)CaDiCaL version: 2.1.3 % 300.50/42.73 % (706497)Termination reason: Refutation not found, incomplete strategy % 300.50/42.73 % (706497)Time elapsed: 0.377 s % 300.50/42.73 % (70 % 300.50/42.73 Terminated % 300.50/42.73 % Vampire exiting % 300.50/42.74 Terminated %------------------------------------------------------------------------------