%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : CSR080+1 : TPTP v9.3.1. Bugfixed v7.3.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 09:45:01 AM UTC 2026 % Result : Timeout 300.49s 42.83s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : CSR080+1 : TPTP v9.3.1. Bugfixed v7.3.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.08/0.19 % Computer : n005.cluster.edu % 0.08/0.19 % Model : x86_64 x86_64 % 0.08/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.08/0.19 % Memory : 8046.5625MB % 0.08/0.19 % OS : Linux 6.8.0-71-generic % 0.08/0.19 % CPULimit : 300 % 0.08/0.19 % WCLimit : 300 % 0.08/0.19 % DateTime : Mon Sep 28 22:27:47 UTC 2026 % 0.08/0.19 % CPUTime : % 0.08/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.08/0.22 Running first-order model finding % 0.08/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 % 7.63/1.89 % (1257041)Will run a generic schedule for satisfiability detection. % 7.63/1.89 % (1257049)dis+10_1_sil=32000:sp=arity:random_seed=4182019127:i=103:fgj=on_2997 on theBenchmark for (2997ds/103Mi) % 7.63/1.89 % (1257047)% WARNING: option uhcvi not known. % 7.63/1.89 % (1257046)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=361018896_2997 on theBenchmark for (2997ds/0Mi) % 7.63/1.89 % (1257047)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3003497954:i=135531:add=off:rawr=on_2997 on theBenchmark for (2997ds/135531Mi) % 7.63/1.89 % (1257048)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=986002417:i=88024:add=on:rawr=on_2997 on theBenchmark for (2997ds/88024Mi) % 7.63/1.89 % (1257050)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1246705785:i=116_2997 on theBenchmark for (2997ds/116Mi) % 7.63/1.89 % (1257051)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3629285473:i=131_2997 on theBenchmark for (2997ds/131Mi) % 7.63/1.89 % (1257052)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2535520582:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2997 on theBenchmark for (2997ds/159Mi) % 7.63/1.89 % (1257049)Instruction limit reached! % 7.63/1.89 % (1257049)------------------------------ % 7.63/1.89 % (1257049)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.63/1.89 % (1257049)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.63/1.89 % (1257049)CaDiCaL version: 2.1.3 % 7.63/1.89 % (1257049)Termination reason: Instruction limit % 7.63/1.89 % (1257049)Termination phase: Preprocessing 3 % 7.63/1.89 % (1257049)Time elapsed: 0.040 s % 7.63/1.89 % (1257049)Peak memory usage: 29 MB % 7.63/1.89 % (1257049)Instructions burned: 103 (million) % 7.63/1.89 % (1257060)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2544210336:i=714:nm=2_2996 on theBenchmark for (2996ds/714Mi) % 7.63/1.89 % (1257050)Instruction limit reached! % 7.63/1.89 % (1257050)------------------------------ % 7.63/1.89 % (1257050)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.63/1.89 % (1257050)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.63/1.89 % (1257050)CaDiCaL version: 2.1.3 % 7.63/1.89 % (1257050)Termination reason: Instruction limit % 7.63/1.89 % (1257050)Termination phase: NewCNF % 7.63/1.89 % (1257050)Time elapsed: 0.078 s % 7.63/1.89 % (1257050)Peak memory usage: 32 MB % 7.63/1.89 % (1257050)Instructions burned: 117 (million) % 7.63/1.89 % (1257051)Instruction limit reached! % 7.63/1.89 % (1257051)------------------------------ % 7.63/1.89 % (1257051)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.63/1.89 % (1257051)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.63/1.89 % (1257051)CaDiCaL version: 2.1.3 % 7.63/1.89 % (1257051)Termination reason: Instruction limit % 7.63/1.89 % (1257051)Termination phase: Clausification % 7.63/1.89 % (1257051)Time elapsed: 0.081 s % 7.63/1.89 % (1257051)Peak memory usage: 31 MB % 7.63/1.89 % (1257051)Instructions burned: 131 (million) % 7.63/1.89 % (1257062)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1390411707:i=131:bd=preordered:fsd=on_2996 on theBenchmark for (2996ds/131Mi) % 7.63/1.89 % (1257052)Instruction limit reached! % 7.63/1.89 % (1257052)------------------------------ % 7.63/1.89 % (1257052)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.63/1.89 % (1257052)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.63/1.89 % (1257052)CaDiCaL version: 2.1.3 % 7.63/1.89 % (1257052)Termination reason: Instruction limit % 7.63/1.89 % (1257052)Termination phase: Property scanning % 7.63/1.89 % (1257052)Time elapsed: 0.099 s % 7.63/1.89 % (1257052)Peak memory usage: 31 MB % 7.63/1.89 % (1257052)Instructions burned: 162 (million) % 7.63/1.89 % (1257063)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=855631049:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2996 on theBenchmark for (2996ds/684Mi) % 7.63/1.89 % (1257065)ott-21_1_sil=16000:fs=off:random_seed=3765312353:i=180:av=off:fsr=off_2995 on theBenchmark for (2995ds/180Mi) % 7.63/1.89 % (1257062)Instruction limit reached! % 7.63/1.89 % (1257062)------------------------------ % 7.63/1.89 % (1257062)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.63/1.89 % (1257062)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.60/2.98 % (1257062)CaDiCaL version: 2.1.3 % 15.60/2.98 % (1257062)Termination reason: Instruction limit % 15.60/2.98 % (1257062)Termination phase: Clausification % 15.60/2.98 % (1257062)Time elapsed: 0.076 s % 15.60/2.98 % (1257062)Peak memory usage: 31 MB % 15.60/2.98 % (1257062)Instructions burned: 133 (million) % 15.60/2.98 % (1257068)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2942937879:i=477:bd=all_2995 on theBenchmark for (2995ds/477Mi) % 15.60/2.98 % (1257065)Instruction limit reached! % 15.60/2.98 % (1257065)------------------------------ % 15.60/2.98 % (1257065)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 15.60/2.98 % (1257065)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.60/2.98 % (1257065)CaDiCaL version: 2.1.3 % 15.60/2.98 % (1257065)Termination reason: Instruction limit % 15.60/2.98 % (1257065)Termination phase: Property scanning % 15.60/2.98 % (1257065)Time elapsed: 0.101 s % 15.60/2.98 % (1257065)Peak memory usage: 31 MB % 15.60/2.98 % (1257065)Instructions burned: 182 (million) % 15.60/2.98 % (1257070)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2975546571:fmbsr=1.3:i=865:ins=25_2994 on theBenchmark for (2994ds/865Mi) % 15.60/2.98 % (1257060)Instruction limit reached! % 15.60/2.98 % (1257060)------------------------------ % 15.60/2.98 % (1257060)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 15.60/2.98 % (1257060)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.60/2.98 % (1257060)CaDiCaL version: 2.1.3 % 15.60/2.98 % (1257060)Termination reason: Instruction limit % 15.60/2.98 % (1257060)Termination phase: Finite model building preprocessing % 15.60/2.98 % (1257060)Time elapsed: 0.200 s % 15.60/2.98 % (1257060)Peak memory usage: 42 MB % 15.60/2.98 % (1257060)Instructions burned: 718 (million) % 15.60/2.98 % (1257072)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=401203122:i=1179_2994 on theBenchmark for (2994ds/1179Mi) % 15.60/2.98 % (1257068)Instruction limit reached! % 15.60/2.98 % (1257068)------------------------------ % 15.60/2.98 % (1257068)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 15.60/2.98 % (1257068)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.60/2.98 % (1257068)CaDiCaL version: 2.1.3 % 15.60/2.98 % (1257068)Termination reason: Instruction limit % 15.60/2.98 % (1257068)Termination phase: Saturation % 15.60/2.98 % (1257068)Time elapsed: 0.233 s % 15.60/2.98 % (1257068)Peak memory usage: 35 MB % 15.60/2.98 % (1257068)Instructions burned: 478 (million) % 15.60/2.98 % (1257063)Instruction limit reached! % 15.60/2.98 % (1257063)------------------------------ % 15.60/2.98 % (1257063)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 15.60/2.98 % (1257063)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.60/2.98 % (1257063)CaDiCaL version: 2.1.3 % 15.60/2.98 % (1257063)Termination reason: Instruction limit % 15.60/2.98 % (1257063)Termination phase: Saturation % 15.60/2.98 % (1257063)Time elapsed: 0.338 s % 15.60/2.98 % (1257063)Peak memory usage: 40 MB % 15.60/2.98 % (1257063)Instructions burned: 685 (million) % 15.60/2.98 % (1257074)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2940730411:i=889:ins=1_2992 on theBenchmark for (2992ds/889Mi) % 15.60/2.98 % (1257075)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=287787378:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2992 on theBenchmark for (2992ds/692Mi) % 15.60/2.98 % (1257072)Instruction limit reached! % 15.60/2.98 % (1257072)------------------------------ % 15.60/2.98 % (1257072)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 15.60/2.98 % (1257072)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.60/2.98 % (1257072)CaDiCaL version: 2.1.3 % 15.60/2.98 % (1257072)Termination reason: Instruction limit % 15.60/2.98 % (1257072)Termination phase: Saturation % 15.60/2.98 % (1257072)Time elapsed: 0.336 s % 15.60/2.98 % (1257072)Peak memory usage: 44 MB % 15.60/2.98 % (1257072)Instructions burned: 1182 (million) % 15.60/2.98 % (1257078)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2007137057:i=879:kws=inv_precedence:fsr=off_2990 on theBenchmark for (2990ds/879Mi) % 15.60/2.98 % (1257070)Instruction limit reached! % 15.60/2.98 % (1257070)------------------------------ % 15.60/2.98 % (1257070)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 15.60/2.98 % (1257070)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.10/4.18 % (1257070)CaDiCaL version: 2.1.3 % 26.10/4.18 % (1257070)Termination reason: Instruction limit % 26.10/4.18 % (1257070)Termination phase: Finite model building preprocessing % 26.10/4.18 % (1257070)Time elapsed: 0.413 s % 26.10/4.18 % (1257070)Peak memory usage: 46 MB % 26.10/4.18 % (1257070)Instructions burned: 865 (million) % 26.10/4.18 % (1257080)fmb+10_1_sil=64000:random_seed=3173783342:i=22061:nm=2:gsp=on_2990 on theBenchmark for (2990ds/22061Mi) % 26.10/4.18 % (1257075)Instruction limit reached! % 26.10/4.18 % (1257075)------------------------------ % 26.10/4.18 % (1257075)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 26.10/4.18 % (1257075)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.10/4.18 % (1257075)CaDiCaL version: 2.1.3 % 26.10/4.18 % (1257075)Termination reason: Instruction limit % 26.10/4.18 % (1257075)Termination phase: Saturation % 26.10/4.18 % (1257075)Time elapsed: 0.351 s % 26.10/4.18 % (1257075)Peak memory usage: 43 MB % 26.10/4.18 % (1257075)Instructions burned: 692 (million) % 26.10/4.18 % (1257082)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1180335102:i=9515:nm=5_2988 on theBenchmark for (2988ds/9515Mi) % 26.10/4.18 % (1257078)Instruction limit reached! % 26.10/4.18 % (1257078)------------------------------ % 26.10/4.18 % (1257078)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 26.10/4.18 % (1257078)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.10/4.18 % (1257078)CaDiCaL version: 2.1.3 % 26.10/4.18 % (1257078)Termination reason: Instruction limit % 26.10/4.18 % (1257078)Termination phase: Saturation % 26.10/4.18 % (1257078)Time elapsed: 0.238 s % 26.10/4.18 % (1257078)Peak memory usage: 45 MB % 26.10/4.18 % (1257078)Instructions burned: 881 (million) % 26.10/4.18 % (1257084)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1911711348:fmbsr=1.7:i=920_2988 on theBenchmark for (2988ds/920Mi) % 26.10/4.18 % (1257074)Instruction limit reached! % 26.10/4.18 % (1257074)------------------------------ % 26.10/4.18 % (1257074)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 26.10/4.18 % (1257074)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.10/4.18 % (1257074)CaDiCaL version: 2.1.3 % 26.10/4.18 % (1257074)Termination reason: Instruction limit % 26.10/4.18 % (1257074)Termination phase: Finite model building preprocessing % 26.10/4.18 % (1257074)Time elapsed: 0.424 s % 26.10/4.18 % (1257074)Peak memory usage: 47 MB % 26.10/4.18 % (1257074)Instructions burned: 890 (million) % 26.10/4.18 % (1257086)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=3543973710:i=5131_2988 on theBenchmark for (2988ds/5131Mi) % 26.10/4.18 % Detected minimum model sizes of [51] % 26.10/4.18 % Detected maximum model sizes of [max] % 26.10/4.18 % (1257046)Cannot represent all propositional literals internally % 26.10/4.18 % (1257046)Refutation not found, incomplete strategy % 26.10/4.18 % (1257046)------------------------------ % 26.10/4.18 % (1257046)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 26.10/4.18 % (1257046)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.10/4.18 % (1257046)CaDiCaL version: 2.1.3 % 26.10/4.18 % (1257046)Termination reason: Refutation not found, incomplete strategy % 26.10/4.18 % (1257046)Time elapsed: 0.906 s % 26.10/4.18 % (1257046)Peak memory usage: 60 MB % 26.10/4.18 % (1257046)Instructions burned: 1874 (million) % 26.10/4.18 % (1257046)------------------------------ % 26.10/4.18 % (1257046)------------------------------ % 26.10/4.18 % (1257088)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3771373358:i=1472:ins=7:fdi=8:gsp=on_2987 on theBenchmark for (2987ds/1472Mi) % 26.10/4.18 % (1257084)Instruction limit reached! % 26.10/4.18 % (1257084)------------------------------ % 26.10/4.18 % (1257084)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 26.10/4.18 % (1257084)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.10/4.18 % (1257084)CaDiCaL version: 2.1.3 % 26.10/4.18 % (1257084)Termination reason: Instruction limit % 26.10/4.18 % (1257084)Termination phase: Finite model building preprocessing % 26.10/4.18 % (1257084)Time elapsed: 0.241 s % 26.10/4.18 % (1257084)Peak memory usage: 46 MB % 26.10/4.18 % (1257084)Instructions burned: 922 (million) % 26.10/4.18 % (1257090)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3317391780:i=6324_2985 on theBenchmark for (2985ds/6324Mi) % 26.10/4.18 % Detected minimum model sizes of [51] % 26.10/4.18 % Detected maximum model sizes of [max] % 26.10/4.18 % (1257080)Cannot represent all propositional literals internally % 36.77/5.87 % (1257080)Refutation not found, incomplete strategy % 36.77/5.87 % (1257080)------------------------------ % 36.77/5.87 % (1257080)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 36.77/5.87 % (1257080)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 36.77/5.87 % (1257080)CaDiCaL version: 2.1.3 % 36.77/5.87 % (1257080)Termination reason: Refutation not found, incomplete strategy % 36.77/5.87 % (1257080)Time elapsed: 0.671 s % 36.77/5.87 % (1257080)Peak memory usage: 51 MB % 36.77/5.87 % (1257080)Instructions burned: 1452 (million) % 36.77/5.87 % (1257080)------------------------------ % 36.77/5.87 % (1257080)------------------------------ % 36.77/5.87 % (1257092)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=773809540:fmbsr=2.30978:i=2174_2983 on theBenchmark for (2983ds/2174Mi) % 36.77/5.87 % Detected minimum model sizes of [51] % 36.77/5.87 % Detected maximum model sizes of [max] % 36.77/5.87 % (1257082)Cannot represent all propositional literals internally % 36.77/5.87 % (1257082)Refutation not found, incomplete strategy % 36.77/5.87 % (1257082)------------------------------ % 36.77/5.87 % (1257082)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 36.77/5.87 % (1257082)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 36.77/5.87 % (1257082)CaDiCaL version: 2.1.3 % 36.77/5.87 % (1257082)Termination reason: Refutation not found, incomplete strategy % 36.77/5.87 % (1257082)Time elapsed: 0.706 s % 36.77/5.87 % (1257082)Peak memory usage: 52 MB % 36.77/5.87 % (1257082)Instructions burned: 1527 (million) % 36.77/5.87 % (1257082)------------------------------ % 36.77/5.87 % (1257082)------------------------------ % 36.77/5.87 % (1257094)ott-2_1_sil=16000:newcnf=on:random_seed=4258034834:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2981 on theBenchmark for (2981ds/869Mi) % 36.77/5.87 % Detected minimum model sizes of [51] % 36.77/5.87 % Detected maximum model sizes of [max] % 36.77/5.87 % (1257090)Cannot represent all propositional literals internally % 36.77/5.87 % (1257090)Refutation not found, incomplete strategy % 36.77/5.87 % (1257090)------------------------------ % 36.77/5.87 % (1257090)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 36.77/5.87 % (1257090)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 36.77/5.87 % (1257090)CaDiCaL version: 2.1.3 % 36.77/5.87 % (1257090)Termination reason: Refutation not found, incomplete strategy % 36.77/5.87 % (1257090)Time elapsed: 0.475 s % 36.77/5.87 % (1257090)Peak memory usage: 58 MB % 36.77/5.87 % (1257090)Instructions burned: 1850 (million) % 36.77/5.87 % (1257090)------------------------------ % 36.77/5.87 % (1257090)------------------------------ % 36.77/5.87 % (1257096)ott+10_1_sil=32000:tgt=ground:random_seed=3771982797:i=5114:av=off_2980 on theBenchmark for (2980ds/5114Mi) % 36.77/5.87 % (1257088)Instruction limit reached! % 36.77/5.87 % (1257088)------------------------------ % 36.77/5.87 % (1257088)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 36.77/5.87 % (1257088)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 36.77/5.87 % (1257088)CaDiCaL version: 2.1.3 % 36.77/5.87 % (1257088)Termination reason: Instruction limit % 36.77/5.87 % (1257088)Termination phase: Saturation % 36.77/5.87 % (1257088)Time elapsed: 0.775 s % 36.77/5.87 % (1257088)Peak memory usage: 48 MB % 36.77/5.87 % (1257088)Instructions burned: 1473 (million) % 36.77/5.87 % (1257098)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2648660497:i=54282_2979 on theBenchmark for (2979ds/54282Mi) % 36.77/5.87 % (1257094)Instruction limit reached! % 36.77/5.87 % (1257094)------------------------------ % 36.77/5.87 % (1257094)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 36.77/5.87 % (1257094)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 36.77/5.87 % (1257094)CaDiCaL version: 2.1.3 % 36.77/5.87 % (1257094)Termination reason: Instruction limit % 36.77/5.87 % (1257094)Termination phase: Saturation % 36.77/5.87 % (1257094)Time elapsed: 0.431 s % 36.77/5.87 % (1257094)Peak memory usage: 43 MB % 36.77/5.87 % (1257094)Instructions burned: 869 (million) % 36.77/5.87 % (1257100)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=2723127832:i=3512:aac=none_2976 on theBenchmark for (2976ds/3512Mi) % 36.77/5.87 % (1257092)Instruction limit reached! % 36.77/5.87 % (1257092)------------------------------ % 36.77/5.87 % (1257092)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 36.77/5.87 % (1257092)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 83.35/12.27 % (1257092)CaDiCaL version: 2.1.3 % 83.35/12.27 % (1257092)Termination reason: Instruction limit % 83.35/12.27 % (1257092)Termination phase: Finite model building preprocessing % 83.35/12.27 % (1257092)Time elapsed: 1.049 s % 83.35/12.27 % (1257092)Peak memory usage: 71 MB % 83.35/12.27 % (1257092)Instructions burned: 2175 (million) % 83.35/12.27 % (1257102)dis+21_1_sil=32000:sas=cadical:random_seed=334809885:i=3773:amm=off_2972 on theBenchmark for (2972ds/3773Mi) % 83.35/12.27 % Detected minimum model sizes of [51] % 83.35/12.27 % Detected maximum model sizes of [max] % 83.35/12.27 % (1257098)Cannot represent all propositional literals internally % 83.35/12.27 % (1257098)Refutation not found, incomplete strategy % 83.35/12.27 % (1257098)------------------------------ % 83.35/12.27 % (1257098)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 83.35/12.27 % (1257098)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 83.35/12.27 % (1257098)CaDiCaL version: 2.1.3 % 83.35/12.27 % (1257098)Termination reason: Refutation not found, incomplete strategy % 83.35/12.27 % (1257098)Time elapsed: 0.891 s % 83.35/12.27 % (1257098)Peak memory usage: 59 MB % 83.35/12.27 % (1257098)Instructions burned: 1866 (million) % 83.35/12.27 % (1257098)------------------------------ % 83.35/12.27 % (1257098)------------------------------ % 83.35/12.27 % (1257104)ott+11_1_sil=16000:gs=on:random_seed=2154350251:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2970 on theBenchmark for (2970ds/2251Mi) % 83.35/12.27 % (1257096)Instruction limit reached! % 83.35/12.27 % (1257096)------------------------------ % 83.35/12.27 % (1257096)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 83.35/12.27 % (1257096)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 83.35/12.27 % (1257096)CaDiCaL version: 2.1.3 % 83.35/12.27 % (1257096)Termination reason: Instruction limit % 83.35/12.27 % (1257096)Termination phase: Saturation % 83.35/12.27 % (1257096)Time elapsed: 1.356 s % 83.35/12.27 % (1257096)Peak memory usage: 85 MB % 83.35/12.27 % (1257096)Instructions burned: 5115 (million) % 83.35/12.27 % (1257106)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=269240804:fmbsr=1.6:i=67534_2967 on theBenchmark for (2967ds/67534Mi) % 83.35/12.27 % Detected minimum model sizes of [51] % 83.35/12.27 % Detected maximum model sizes of [max] % 83.35/12.27 % (1257106)Cannot represent all propositional literals internally % 83.35/12.27 % (1257106)Refutation not found, incomplete strategy % 83.35/12.27 % (1257106)------------------------------ % 83.35/12.27 % (1257106)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 83.35/12.27 % (1257106)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 83.35/12.27 % (1257106)CaDiCaL version: 2.1.3 % 83.35/12.27 % (1257106)Termination reason: Refutation not found, incomplete strategy % 83.35/12.27 % (1257106)Time elapsed: 0.416 s % 83.35/12.27 % (1257106)Peak memory usage: 53 MB % 83.35/12.27 % (1257106)Instructions burned: 1686 (million) % 83.35/12.27 % (1257106)------------------------------ % 83.35/12.27 % (1257106)------------------------------ % 83.35/12.27 % (1257108)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=2784583644:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2962 on theBenchmark for (2962ds/4591Mi) % 83.35/12.27 % (1257086)Instruction limit reached! % 83.35/12.27 % (1257086)------------------------------ % 83.35/12.27 % (1257086)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 83.35/12.27 % (1257086)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 83.35/12.27 % (1257086)CaDiCaL version: 2.1.3 % 83.35/12.27 % (1257086)Termination reason: Instruction limit % 83.35/12.27 % (1257086)Termination phase: Saturation % 83.35/12.27 % (1257086)Time elapsed: 2.701 s % 83.35/12.27 % (1257086)Peak memory usage: 65 MB % 83.35/12.27 % (1257086)Instructions burned: 5132 (million) % 83.35/12.27 % (1257110)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=1863736298:i=29340_2960 on theBenchmark for (2960ds/29340Mi) % 83.35/12.27 % (1257104)Instruction limit reached! % 83.35/12.27 % (1257104)------------------------------ % 83.35/12.27 % (1257104)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 83.35/12.27 % (1257104)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 83.35/12.27 % (1257104)CaDiCaL version: 2.1.3 % 83.35/12.27 % (1257104)Termination reason: Instruction limit % 83.35/12.27 % (1257104)Termination phase: Saturation % 83.35/12.27 % (1257104)Time elapsed: 0.950 s % 83.35/12.27 % (1257104)Peak memory usage: 57 MB % 83.35/12.27 % (1257104)Instructions burned: 2252 (million) % 133.02/19.28 % (1257112)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=154344490:i=5211_2960 on theBenchmark for (2960ds/5211Mi) % 133.02/19.28 % (1257100)Instruction limit reached! % 133.02/19.28 % (1257100)------------------------------ % 133.02/19.28 % (1257100)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 133.02/19.28 % (1257100)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 133.02/19.28 % (1257100)CaDiCaL version: 2.1.3 % 133.02/19.28 % (1257100)Termination reason: Instruction limit % 133.02/19.28 % (1257100)Termination phase: Saturation % 133.02/19.28 % (1257100)Time elapsed: 1.641 s % 133.02/19.28 % (1257100)Peak memory usage: 75 MB % 133.02/19.28 % (1257100)Instructions burned: 3513 (million) % 133.02/19.28 % (1257114)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=1267009664:i=5497:nm=2_2960 on theBenchmark for (2960ds/5497Mi) % 133.02/19.28 % (1257102)Instruction limit reached! % 133.02/19.28 % (1257102)------------------------------ % 133.02/19.28 % (1257102)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 133.02/19.28 % (1257102)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 133.02/19.28 % (1257102)CaDiCaL version: 2.1.3 % 133.02/19.28 % (1257102)Termination reason: Instruction limit % 133.02/19.28 % (1257102)Termination phase: Saturation % 133.02/19.28 % (1257102)Time elapsed: 1.878 s % 133.02/19.28 % (1257102)Peak memory usage: 86 MB % 133.02/19.28 % (1257102)Instructions burned: 3774 (million) % 133.02/19.28 % (1257116)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=3076873951:fmbsr=2:i=46332_2953 on theBenchmark for (2953ds/46332Mi) % 133.02/19.28 % Detected minimum model sizes of [51] % 133.02/19.28 % Detected maximum model sizes of [max] % 133.02/19.28 % (1257114)Cannot represent all propositional literals internally % 133.02/19.28 % (1257114)Refutation not found, incomplete strategy % 133.02/19.28 % (1257114)------------------------------ % 133.02/19.28 % (1257114)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 133.02/19.28 % (1257114)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 133.02/19.28 % (1257114)CaDiCaL version: 2.1.3 % 133.02/19.28 % (1257114)Termination reason: Refutation not found, incomplete strategy % 133.02/19.28 % (1257114)Time elapsed: 0.830 s % 133.02/19.28 % (1257114)Peak memory usage: 54 MB % 133.02/19.28 % (1257114)Instructions burned: 1714 (million) % 133.02/19.28 % (1257114)------------------------------ % 133.02/19.28 % (1257114)------------------------------ % 133.02/19.28 % (1257118)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=4284077620:i=14071_2951 on theBenchmark for (2951ds/14071Mi) % 133.02/19.28 % (1257108)Instruction limit reached! % 133.02/19.28 % (1257108)------------------------------ % 133.02/19.28 % (1257108)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 133.02/19.28 % (1257108)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 133.02/19.28 % (1257108)CaDiCaL version: 2.1.3 % 133.02/19.28 % (1257108)Termination reason: Instruction limit % 133.02/19.28 % (1257108)Termination phase: Saturation % 133.02/19.28 % (1257108)Time elapsed: 1.448 s % 133.02/19.28 % (1257108)Peak memory usage: 98 MB % 133.02/19.28 % (1257108)Instructions burned: 4594 (million) % 133.02/19.28 % (1257120)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2813796894:i=22565:add=on:rawr=on_2947 on theBenchmark for (2947ds/22565Mi) % 133.02/19.28 % Detected minimum model sizes of [51] % 133.02/19.28 % Detected maximum model sizes of [max] % 133.02/19.28 % (1257116)Cannot represent all propositional literals internally % 133.02/19.28 % (1257116)Refutation not found, incomplete strategy % 133.02/19.28 % (1257116)------------------------------ % 133.02/19.28 % (1257116)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 133.02/19.28 % (1257116)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 133.02/19.28 % (1257116)CaDiCaL version: 2.1.3 % 133.02/19.28 % (1257116)Termination reason: Refutation not found, incomplete strategy % 133.02/19.28 % (1257116)Time elapsed: 0.759 s % 133.02/19.28 % (1257116)Peak memory usage: 53 MB % 133.02/19.28 % (1257116)Instructions burned: 1686 (million) % 133.02/19.28 % (1257116)------------------------------ % 133.02/19.28 % (1257116)------------------------------ % 133.02/19.28 % (1257122)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=139952550:i=8173:av=off_2945 on theBenchmark for (2945ds/8173Mi) % 133.02/19.28 % Detected minimum model sizes of [51] % 133.02/19.28 % Detected maximum model sizes of [max] % 133.02/19.28 % (1257118)Cannot represent all propositional literals internally % 133.02/19.28 % (1257118)Refutation not found, incomplete strategy % 149.36/21.56 % (1257118)------------------------------ % 149.36/21.56 % (1257118)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 149.36/21.56 % (1257118)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 149.36/21.56 % (1257118)CaDiCaL version: 2.1.3 % 149.36/21.56 % (1257118)Termination reason: Refutation not found, incomplete strategy % 149.36/21.56 % (1257118)Time elapsed: 0.738 s % 149.36/21.56 % (1257118)Peak memory usage: 53 MB % 149.36/21.56 % (1257118)Instructions burned: 1556 (million) % 149.36/21.56 % (1257118)------------------------------ % 149.36/21.56 % (1257118)------------------------------ % 149.36/21.56 % (1257124)dis+10_16:1_sil=16000:random_seed=4018665504:i=9155:fsr=off_2943 on theBenchmark for (2943ds/9155Mi) % 149.36/21.56 % (1257112)Instruction limit reached! % 149.36/21.56 % (1257112)------------------------------ % 149.36/21.56 % (1257112)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 149.36/21.56 % (1257112)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 149.36/21.56 % (1257112)CaDiCaL version: 2.1.3 % 149.36/21.56 % (1257112)Termination reason: Instruction limit % 149.36/21.56 % (1257112)Termination phase: Saturation % 149.36/21.56 % (1257112)Time elapsed: 2.214 s % 149.36/21.56 % (1257112)Peak memory usage: 66 MB % 149.36/21.56 % (1257112)Instructions burned: 5213 (million) % 149.36/21.56 % (1257126)ott-3_8_sil=64000:random_seed=3864112766:i=20139:bs=on_2937 on theBenchmark for (2937ds/20139Mi) % 149.36/21.56 % (1257122)Instruction limit reached! % 149.36/21.56 % (1257122)------------------------------ % 149.36/21.56 % (1257122)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 149.36/21.56 % (1257122)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 149.36/21.56 % (1257122)CaDiCaL version: 2.1.3 % 149.36/21.56 % (1257122)Termination reason: Instruction limit % 149.36/21.56 % (1257122)Termination phase: Saturation % 149.36/21.56 % (1257122)Time elapsed: 4.540 s % 149.36/21.56 % (1257122)Peak memory usage: 113 MB % 149.36/21.56 % (1257122)Instructions burned: 8175 (million) % 149.36/21.56 % (1257129)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=2293974235:fmbsr=2:i=32576_2899 on theBenchmark for (2899ds/32576Mi) % 149.36/21.56 % (1257124)Instruction limit reached! % 149.36/21.56 % (1257124)------------------------------ % 149.36/21.56 % (1257124)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 149.36/21.56 % (1257124)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 149.36/21.56 % (1257124)CaDiCaL version: 2.1.3 % 149.36/21.56 % (1257124)Termination reason: Instruction limit % 149.36/21.56 % (1257124)Termination phase: Saturation % 149.36/21.56 % (1257124)Time elapsed: 4.527 s % 149.36/21.56 % (1257124)Peak memory usage: 157 MB % 149.36/21.56 % (1257124)Instructions burned: 9159 (million) % 149.36/21.56 % (1257131)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=15032223:i=11404_2897 on theBenchmark for (2897ds/11404Mi) % 149.36/21.56 % Detected minimum model sizes of [51] % 149.36/21.56 % Detected maximum model sizes of [max] % 149.36/21.56 % (1257129)Cannot represent all propositional literals internally % 149.36/21.56 % (1257129)Refutation not found, incomplete strategy % 149.36/21.56 % (1257129)------------------------------ % 149.36/21.56 % (1257129)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 149.36/21.56 % (1257129)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 149.36/21.56 % (1257129)CaDiCaL version: 2.1.3 % 149.36/21.56 % (1257129)Termination reason: Refutation not found, incomplete strategy % 149.36/21.56 % (1257129)Time elapsed: 0.919 s % 149.36/21.56 % (1257129)Peak memory usage: 58 MB % 149.36/21.56 % (1257129)Instructions burned: 1850 (million) % 149.36/21.56 % (1257129)------------------------------ % 149.36/21.56 % (1257129)------------------------------ % 149.36/21.56 % (1257133)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=3420397909:i=14134_2889 on theBenchmark for (2889ds/14134Mi) % 149.36/21.56 % (1257120)Instruction limit reached! % 149.36/21.56 % (1257120)------------------------------ % 149.36/21.56 % (1257120)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 149.36/21.56 % (1257120)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 149.36/21.56 % (1257120)CaDiCaL version: 2.1.3 % 149.36/21.56 % (1257120)Termination reason: Instruction limit % 149.36/21.56 % (1257120)Termination phase: Saturation % 149.36/21.56 % (1257120)Time elapsed: 6.754 s % 149.36/21.56 % (1257120)Peak memory usage: 782 MB % 149.36/21.56 % (1257120)Instructions burned: 22566 (million) % 149.36/21.56 % (1257135)dis+33_16_sil=32000:sac=on:random_seed=4220057727:i=15851:nm=0_2879 on theBenchmark for (2879ds/15851Mi) % 156.97/22.63 % (1257135)Instruction limit reached! % 156.97/22.63 % (1257135)------------------------------ % 156.97/22.63 % (1257135)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 156.97/22.63 % (1257135)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 156.97/22.63 % (1257135)CaDiCaL version: 2.1.3 % 156.97/22.63 % (1257135)Termination reason: Instruction limit % 156.97/22.63 % (1257135)Termination phase: Saturation % 156.97/22.63 % (1257135)Time elapsed: 3.807 s % 156.97/22.63 % (1257135)Peak memory usage: 97 MB % 156.97/22.63 % (1257135)Instructions burned: 15854 (million) % 156.97/22.63 % (1257137)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=3313936660:avsq=on:i=17627:add=on:amm=off_2841 on theBenchmark for (2841ds/17627Mi) % 156.97/22.63 % (1257131)Instruction limit reached! % 156.97/22.63 % (1257131)------------------------------ % 156.97/22.63 % (1257131)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 156.97/22.63 % (1257131)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 156.97/22.63 % (1257131)CaDiCaL version: 2.1.3 % 156.97/22.63 % (1257131)Termination reason: Instruction limit % 156.97/22.63 % (1257131)Termination phase: Saturation % 156.97/22.63 % (1257131)Time elapsed: 6.776 s % 156.97/22.63 % (1257131)Peak memory usage: 307 MB % 156.97/22.63 % (1257131)Instructions burned: 11407 (million) % 156.97/22.63 % (1257139)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=3307140248:s2a=on:i=53295_2829 on theBenchmark for (2829ds/53295Mi) % 156.97/22.63 % (1257126)Instruction limit reached! % 156.97/22.63 % (1257126)------------------------------ % 156.97/22.63 % (1257126)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 156.97/22.63 % (1257126)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 156.97/22.63 % (1257126)CaDiCaL version: 2.1.3 % 156.97/22.63 % (1257126)Termination reason: Instruction limit % 156.97/22.63 % (1257126)Termination phase: Saturation % 156.97/22.63 % (1257126)Time elapsed: 11.686 s % 156.97/22.63 % (1257126)Peak memory usage: 165 MB % 156.97/22.63 % (1257126)Instructions burned: 20140 (million) % 156.97/22.63 % (1257141)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=2982858153:i=26857:ins=20_2820 on theBenchmark for (2820ds/26857Mi) % 156.97/22.63 % Detected minimum model sizes of [51] % 156.97/22.63 % Detected maximum model sizes of [max] % 156.97/22.63 % (1257141)Cannot represent all propositional literals internally % 156.97/22.63 % (1257141)Refutation not found, incomplete strategy % 156.97/22.63 % (1257141)------------------------------ % 156.97/22.63 % (1257141)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 156.97/22.63 % (1257141)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 156.97/22.63 % (1257141)CaDiCaL version: 2.1.3 % 156.97/22.63 % (1257141)Termination reason: Refutation not found, incomplete strategy % 156.97/22.63 % (1257141)Time elapsed: 0.729 s % 156.97/22.63 % (1257141)Peak memory usage: 53 MB % 156.97/22.63 % (1257141)Instructions burned: 1557 (million) % 156.97/22.63 % (1257141)------------------------------ % 156.97/22.63 % (1257141)------------------------------ % 156.97/22.63 % (1257143)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=2036843541:i=28120:bs=on:fsr=off_2812 on theBenchmark for (2812ds/28120Mi) % 156.97/22.63 % (1257133)Instruction limit reached! % 156.97/22.63 % (1257133)------------------------------ % 156.97/22.63 % (1257133)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 156.97/22.63 % (1257133)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 156.97/22.63 % (1257133)CaDiCaL version: 2.1.3 % 156.97/22.63 % (1257133)Termination reason: Instruction limit % 156.97/22.63 % (1257133)Termination phase: Saturation % 156.97/22.63 % (1257133)Time elapsed: 7.923 s % 156.97/22.63 % (1257133)Peak memory usage: 128 MB % 156.97/22.63 % (1257133)Instructions burned: 14135 (million) % 156.97/22.63 % (1257145)fmb+10_1_sil=256000:fmbss=7:random_seed=4168878702:fmbsr=1.6:i=182295_2810 on theBenchmark for (2810ds/182295Mi) % 156.97/22.63 % (1257110)Instruction limit reached! % 156.97/22.63 % (1257110)------------------------------ % 156.97/22.63 % (1257110)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 156.97/22.63 % (1257110)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 156.97/22.63 % (1257110)CaDiCaL version: 2.1.3 % 156.97/22.63 % (1257110)Termination reason: Instruction limit % 156.97/22.63 % (1257110)Termination phase: Saturation % 156.97/22.63 % (1257110)Time elapsed: 15.112 s % 156.97/22.63 % (1257110)Peak memory usage: 75 MB % 156.97/22.63 % (1257110)Instructions burned: 29341 (million) % 178.45/25.66 % (1257147)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=4199207367:i=44625:gsp=on_2809 on theBenchmark for (2809ds/44625Mi) % 178.45/25.66 % Detected minimum model sizes of [51] % 178.45/25.66 % Detected maximum model sizes of [max] % 178.45/25.66 % (1257145)Cannot represent all propositional literals internally % 178.45/25.66 % (1257145)Refutation not found, incomplete strategy % 178.45/25.66 % (1257145)------------------------------ % 178.45/25.66 % (1257145)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 178.45/25.66 % (1257145)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 178.45/25.66 % (1257145)CaDiCaL version: 2.1.3 % 178.45/25.66 % (1257145)Termination reason: Refutation not found, incomplete strategy % 178.45/25.66 % (1257145)Time elapsed: 0.727 s % 178.45/25.66 % (1257145)Peak memory usage: 53 MB % 178.45/25.66 % (1257145)Instructions burned: 1556 (million) % 178.45/25.66 % (1257145)------------------------------ % 178.45/25.66 % (1257145)------------------------------ % 178.45/25.66 % (1257149)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=2849241522:i=160505_2802 on theBenchmark for (2802ds/160505Mi) % 178.45/25.66 % Detected minimum model sizes of [51] % 178.45/25.66 % Detected maximum model sizes of [max] % 178.45/25.66 % (1257147)Cannot represent all propositional literals internally % 178.45/25.66 % (1257147)Refutation not found, incomplete strategy % 178.45/25.66 % (1257147)------------------------------ % 178.45/25.66 % (1257147)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 178.45/25.66 % (1257147)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 178.45/25.66 % (1257147)CaDiCaL version: 2.1.3 % 178.45/25.66 % (1257147)Termination reason: Refutation not found, incomplete strategy % 178.45/25.66 % (1257147)Time elapsed: 0.784 s % 178.45/25.66 % (1257147)Peak memory usage: 56 MB % 178.45/25.66 % (1257147)Instructions burned: 1671 (million) % 178.45/25.66 % (1257147)------------------------------ % 178.45/25.66 % (1257147)------------------------------ % 178.45/25.66 % (1257151)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=3805072717:fmbsr=1.3:i=225729_2801 on theBenchmark for (2801ds/225729Mi) % 178.45/25.66 % Detected minimum model sizes of [51] % 178.45/25.66 % Detected maximum model sizes of [max] % 178.45/25.66 % (1257149)Cannot represent all propositional literals internally % 178.45/25.66 % (1257149)Refutation not found, incomplete strategy % 178.45/25.66 % (1257149)------------------------------ % 178.45/25.66 % (1257149)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 178.45/25.66 % (1257149)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 178.45/25.66 % (1257149)CaDiCaL version: 2.1.3 % 178.45/25.66 % (1257149)Termination reason: Refutation not found, incomplete strategy % 178.45/25.66 % (1257149)Time elapsed: 0.751 s % 178.45/25.66 % (1257149)Peak memory usage: 53 MB % 178.45/25.66 % (1257149)Instructions burned: 1556 (million) % 178.45/25.66 % (1257149)------------------------------ % 178.45/25.66 % (1257149)------------------------------ % 178.45/25.66 % (1257153)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=2755368935:fmbsr=2:i=185024:ins=7_2794 on theBenchmark for (2794ds/185024Mi) % 178.45/25.66 % Detected minimum model sizes of [51] % 178.45/25.66 % Detected maximum model sizes of [max] % 178.45/25.66 % (1257151)Cannot represent all propositional literals internally % 178.45/25.66 % (1257151)Refutation not found, incomplete strategy % 178.45/25.66 % (1257151)------------------------------ % 178.45/25.66 % (1257151)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 178.45/25.66 % (1257151)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 178.45/25.66 % (1257151)CaDiCaL version: 2.1.3 % 178.45/25.66 % (1257151)Termination reason: Refutation not found, incomplete strategy % 178.45/25.66 % (1257151)Time elapsed: 0.734 s % 178.45/25.66 % (1257151)Peak memory usage: 53 MB % 178.45/25.66 % (1257151)Instructions burned: 1556 (million) % 178.45/25.66 % (1257151)------------------------------ % 178.45/25.66 % (1257151)------------------------------ % 178.45/25.66 % (1257155)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=1017764534:rtra=on_2793 on theBenchmark for (2793ds/0Mi) % 178.45/25.66 % Detected minimum model sizes of [51] % 178.45/25.66 % Detected maximum model sizes of [max] % 178.45/25.66 % (1257153)Cannot represent all propositional literals internally % 178.45/25.66 % (1257153)Refutation not found, incomplete strategy % 178.45/25.66 % (1257153)------------------------------ % 178.45/25.66 % (1257153)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 178.45/25.66 % (1257153)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 222.47/31.81 % (1257153)CaDiCaL version: 2.1.3 % 222.47/31.81 % (1257153)Termination reason: Refutation not found, incomplete strategy % 222.47/31.81 % (1257153)Time elapsed: 0.735 s % 222.47/31.81 % (1257153)Peak memory usage: 53 MB % 222.47/31.81 % (1257153)Instructions burned: 1557 (million) % 222.47/31.81 % (1257153)------------------------------ % 222.47/31.81 % (1257153)------------------------------ % 222.47/31.81 % (1257157)% WARNING: option uhcvi not known. % 222.47/31.81 % (1257157)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2775061262:i=271062:add=off:rtra=on:rawr=on_2786 on theBenchmark for (2786ds/271062Mi) % 222.47/31.81 % (1257137)Instruction limit reached! % 222.47/31.81 % (1257137)------------------------------ % 222.47/31.81 % (1257137)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 222.47/31.81 % (1257137)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 222.47/31.81 % (1257137)CaDiCaL version: 2.1.3 % 222.47/31.81 % (1257137)Termination reason: Instruction limit % 222.47/31.81 % (1257137)Termination phase: Saturation % 222.47/31.81 % (1257137)Time elapsed: 5.608 s % 222.47/31.81 % (1257137)Peak memory usage: 370 MB % 222.47/31.81 % (1257137)Instructions burned: 17630 (million) % 222.47/31.81 % (1257159)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2320406669:i=176048:add=on:rtra=on:rawr=on_2784 on theBenchmark for (2784ds/176048Mi) % 222.47/31.81 % Detected minimum model sizes of [51] % 222.47/31.81 % Detected maximum model sizes of [max] % 222.47/31.81 % (1257155)Cannot represent all propositional literals internally % 222.47/31.81 % (1257155)Refutation not found, incomplete strategy % 222.47/31.81 % (1257155)------------------------------ % 222.47/31.81 % (1257155)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 222.47/31.81 % (1257155)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 222.47/31.81 % (1257155)CaDiCaL version: 2.1.3 % 222.47/31.81 % (1257155)Termination reason: Refutation not found, incomplete strategy % 222.47/31.81 % (1257155)Time elapsed: 1.066 s % 222.47/31.81 % (1257155)Peak memory usage: 64 MB % 222.47/31.81 % (1257155)Instructions burned: 1934 (million) % 222.47/31.81 % (1257155)------------------------------ % 222.47/31.81 % (1257155)------------------------------ % 222.47/31.81 % (1257161)dis+10_1_sil=32000:si=on:sp=arity:random_seed=1687830468:i=206:fgj=on:rtra=on_2781 on theBenchmark for (2781ds/206Mi) % 222.47/31.81 % (1257161)Instruction limit reached! % 222.47/31.81 % (1257161)------------------------------ % 222.47/31.81 % (1257161)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 222.47/31.81 % (1257161)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 222.47/31.81 % (1257161)CaDiCaL version: 2.1.3 % 222.47/31.81 % (1257161)Termination reason: Instruction limit % 222.47/31.81 % (1257161)Termination phase: Property scanning % 222.47/31.81 % (1257161)Time elapsed: 0.155 s % 222.47/31.81 % (1257161)Peak memory usage: 35 MB % 222.47/31.81 % (1257161)Instructions burned: 207 (million) % 222.47/31.81 % (1257163)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=3489363490:i=232:rtra=on_2780 on theBenchmark for (2780ds/232Mi) % 222.47/31.81 % (1257163)Instruction limit reached! % 222.47/31.81 % (1257163)------------------------------ % 222.47/31.81 % (1257163)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 222.47/31.81 % (1257163)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 222.47/31.81 % (1257163)CaDiCaL version: 2.1.3 % 222.47/31.81 % (1257163)Termination reason: Instruction limit % 222.47/31.81 % (1257163)Termination phase: Property scanning % 222.47/31.81 % (1257163)Time elapsed: 0.166 s % 222.47/31.81 % (1257163)Peak memory usage: 36 MB % 222.47/31.81 % (1257163)Instructions burned: 233 (million) % 222.47/31.81 % (1257165)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=1446135039:i=262:rtra=on_2778 on theBenchmark for (2778ds/262Mi) % 222.47/31.81 % (1257165)Instruction limit reached! % 222.47/31.81 % (1257165)------------------------------ % 222.47/31.81 % (1257165)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 222.47/31.81 % (1257165)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 222.47/31.81 % (1257165)CaDiCaL version: 2.1.3 % 222.47/31.81 % (1257165)Termination reason: Instruction limit % 222.47/31.81 % (1257165)Termination phase: Saturation % 222.47/31.81 % (1257165)Time elapsed: 0.178 s % 222.47/31.81 % (1257165)Peak memory usage: 35 MB % 222.47/31.81 % (1257165)Instructions burned: 264 (million) % 222.47/31.81 % (1257167)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=2133123378:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2776 on theBenchmark for (2776ds/318Mi) % 283.54/40.44 % (1257167)Instruction limit reached! % 283.54/40.44 % (1257167)------------------------------ % 283.54/40.44 % (1257167)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 283.54/40.44 % (1257167)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 283.54/40.44 % (1257167)CaDiCaL version: 2.1.3 % 283.54/40.44 % (1257167)Termination reason: Instruction limit % 283.54/40.44 % (1257167)Termination phase: Property scanning % 283.54/40.44 % (1257167)Time elapsed: 0.213 s % 283.54/40.44 % (1257167)Peak memory usage: 37 MB % 283.54/40.44 % (1257167)Instructions burned: 320 (million) % 283.54/40.44 % (1257169)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=309385677:i=1428:nm=2:rtra=on_2773 on theBenchmark for (2773ds/1428Mi) % 283.54/40.44 % (1257169)Instruction limit reached! % 283.54/40.44 % (1257169)------------------------------ % 283.54/40.44 % (1257169)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 283.54/40.44 % (1257169)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 283.54/40.44 % (1257169)CaDiCaL version: 2.1.3 % 283.54/40.44 % (1257169)Termination reason: Instruction limit % 283.54/40.44 % (1257169)Termination phase: Finite model building preprocessing % 283.54/40.44 % (1257169)Time elapsed: 0.757 s % 283.54/40.44 % (1257169)Peak memory usage: 53 MB % 283.54/40.44 % (1257169)Instructions burned: 1428 (million) % 283.54/40.44 % (1257171)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=1700946445:i=262:bd=preordered:rtra=on:fsd=on_2765 on theBenchmark for (2765ds/262Mi) % 283.54/40.44 % (1257171)Instruction limit reached! % 283.54/40.44 % (1257171)------------------------------ % 283.54/40.44 % (1257171)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 283.54/40.44 % (1257171)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 283.54/40.44 % (1257171)CaDiCaL version: 2.1.3 % 283.54/40.44 % (1257171)Termination reason: Instruction limit % 283.54/40.44 % (1257171)Termination phase: Property scanning % 283.54/40.44 % (1257171)Time elapsed: 0.183 s % 283.54/40.44 % (1257171)Peak memory usage: 35 MB % 283.54/40.44 % (1257171)Instructions burned: 263 (million) % 283.54/40.44 % (1257173)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=3866099046:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2763 on theBenchmark for (2763ds/1368Mi) % 283.54/40.44 % (1257173)Instruction limit reached! % 283.54/40.44 % (1257173)------------------------------ % 283.54/40.44 % (1257173)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 283.54/40.44 % (1257173)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 283.54/40.44 % (1257173)CaDiCaL version: 2.1.3 % 283.54/40.44 % (1257173)Termination reason: Instruction limit % 283.54/40.44 % (1257173)Termination phase: Saturation % 283.54/40.44 % (1257173)Time elapsed: 0.863 s % 283.54/40.44 % (1257173)Peak memory usage: 50 MB % 283.54/40.44 % (1257173)Instructions burned: 1368 (million) % 283.54/40.44 % (1257175)ott-21_1_sil=16000:si=on:fs=off:random_seed=3316398523:i=360:av=off:fsr=off:rtra=on_2754 on theBenchmark for (2754ds/360Mi) % 283.54/40.44 % (1257175)Instruction limit reached! % 283.54/40.44 % (1257175)------------------------------ % 283.54/40.44 % (1257175)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 283.54/40.44 % (1257175)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 283.54/40.44 % (1257175)CaDiCaL version: 2.1.3 % 283.54/40.44 % (1257175)Termination reason: Instruction limit % 283.54/40.44 % (1257175)Termination phase: Saturation % 283.54/40.44 % (1257175)Time elapsed: 0.231 s % 283.54/40.44 % (1257175)Peak memory usage: 35 MB % 283.54/40.44 % (1257175)Instructions burned: 360 (million) % 283.54/40.44 % (1257177)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2700717244:i=954:bd=all:rtra=on_2752 on theBenchmark for (2752ds/954Mi) % 283.54/40.44 % (1257177)Instruction limit reached! % 283.54/40.44 % (1257177)------------------------------ % 283.54/40.44 % (1257177)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 283.54/40.44 % (1257177)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 283.54/40.44 % (1257177)CaDiCaL version: 2.1.3 % 283.54/40.44 % (1257177)Termination reason: Instruction limit % 283.54/40.44 % (1257177)Termination phase: Saturation % 283.54/40.44 % (1257177)Time elapsed: 0.608 s % 283.54/40.44 % (1257177)Peak memory usage: 45 MB % 283.54/40.44 % (1257177)Instructions burned: 955 (million) % 283.54/40.44 % (1257179)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=1374953578:fmbsr=1.3:i=1730:ins=25:rtra=on_2745 on theBenchmark for (2745ds/1730Mi) % 300.49/42.83 % Detected minimum model sizes of [51] % 300.49/42.83 % Detected maximum model sizes of [max] % 300.49/42.83 % (1257179)Cannot represent all propositional literals internally % 300.49/42.83 % (1257179)Refutation not found, incomplete strategy % 300.49/42.83 % (1257179)------------------------------ % 300.49/42.83 % (1257179)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.49/42.83 % (1257179)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.49/42.83 % (1257179)CaDiCaL version: 2.1.3 % 300.49/42.83 % (1257179)Termination reason: Refutation not found, incomplete strategy % 300.49/42.83 % (1257179)Time elapsed: 0.823 s % 300.49/42.83 % (1257179)Peak memory usage: 57 MB % 300.49/42.83 % (1257179)Instructions burned: 1521 (million) % 300.49/42.83 % (1257179)------------------------------ % 300.49/42.83 % (1257179)------------------------------ % 300.49/42.83 % (1257181)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=1613016708:i=2358:rtra=on_2737 on theBenchmark for (2737ds/2358Mi) % 300.49/42.83 % (1257181)Instruction limit reached! % 300.49/42.83 % (1257181)------------------------------ % 300.49/42.83 % (1257181)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.49/42.83 % (1257181)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.49/42.83 % (1257181)CaDiCaL version: 2.1.3 % 300.49/42.83 % (1257181)Termination reason: Instruction limit % 300.49/42.83 % (1257181)Termination phase: Saturation % 300.49/42.83 % (1257181)Time elapsed: 1.393 s % 300.49/42.83 % (1257181)Peak memory usage: 60 MB % 300.49/42.83 % (1257181)Instructions burned: 2358 (million) % 300.49/42.83 % (1257183)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=3169895110:i=1778:ins=1:rtra=on_2722 on theBenchmark for (2722ds/1778Mi) % 300.49/42.83 % (1257183)Cannot represent all propositional literals internally % 300.49/42.83 % (1257183)Refutation not found, incomplete strategy % 300.49/42.83 % (1257183)------------------------------ % 300.49/42.83 % (1257183)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.49/42.83 % (1257183)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.49/42.83 % (1257183)CaDiCaL version: 2.1.3 % 300.49/42.83 % (1257183)Termination reason: Refutation not found, incomplete strategy % 300.49/42.83 % (1257183)Time elapsed: 0.874 s % 300.49/42.83 % (1257183)Peak memory usage: 59 MB % 300.49/42.83 % (1257183)Instructions burned: 1602 (million) % 300.49/42.83 % (1257183)------------------------------ % 300.49/42.83 % (1257183)------------------------------ % 300.49/42.83 % (1257185)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:si=on:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=3247955918:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2713 on theBenchmark for (2713ds/1384Mi) % 300.49/42.83 % (1257185)Instruction limit reached! % 300.49/42.83 % (1257185)------------------------------ % 300.49/42.83 % (1257185)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.49/42.83 % (1257185)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.49/42.83 % (1257185)CaDiCaL version: 2.1.3 % 300.49/42.83 % (1257185)Termination reason: Instruction limit % 300.49/42.83 % (1257185)Termination phase: Saturation % 300.49/42.83 % (1257185)Time elapsed: 0.986 s % 300.49/42.83 % (1257185)Peak memory usage: 54 MB % 300.49/42.83 % (1257185)Instructions burned: 1384 (million) % 300.49/42.83 % (1257187)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=3526986763:i=1758:kws=inv_precedence:fsr=off:rtra=on_2703 on theBenchmark for (2703ds/1758Mi) % 300.49/42.83 % (1257187)Instruction limit reached! % 300.49/42.83 % (1257187)------------------------------ % 300.49/42.83 % (1257187)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.49/42.83 % (1257187)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.49/42.83 % (1257187)CaDiCaL version: 2.1.3 % 300.49/42.83 % (1257187)Termination reason: Instruction limit % 300.49/42.83 % (1257187)Termination phase: Saturation % 300.49/42.83 % (1257187)Time elapsed: 1.026 s % 300.49/42.83 % (1257187)Peak memory usage: 60 MB % 300.49/42.83 % (1257187)Instructions burned: 1760 (million) % 300.49/42.83 % (1257189)fmb+10_1_sil=64000:si=on:random_seed=3965883548:i=44122:nm=2:rtra=on:gsp=on_2692 on theBenchmark for (2692ds/44122Mi) % 300.49/42.83 % Detected minimum model sizes of [51] % 300.49/42.83 % Detected maximum model sizes of [max] % 300.49/42.83 % (1257189)Cannot represent all propositiona % 300.49/42.84 Terminated %------------------------------------------------------------------------------