%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWV960-1 : TPTP v9.3.1. Released v4.1.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % Computer : n009.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:26:44 PM UTC 2026 % Result : Timeout 300.41s 42.63s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWV960-1 : TPTP v9.3.1. Released v4.1.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.09/0.18 % Computer : n009.cluster.edu % 0.09/0.18 % Model : x86_64 x86_64 % 0.09/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.18 % Memory : 8046.5625MB % 0.09/0.18 % OS : Linux 6.8.0-71-generic % 0.09/0.18 % CPULimit : 300 % 0.09/0.18 % WCLimit : 300 % 0.09/0.18 % DateTime : Mon Sep 28 13:02:00 UTC 2026 % 0.09/0.18 % CPUTime : % 0.09/0.18 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.09/0.21 Running first-order model finding % 0.09/0.21 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 % 3.25/0.79 % (3011325)Will run a generic schedule for satisfiability detection. % 3.25/0.79 % (3011330)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2406673245_2999 on theBenchmark for (2999ds/0Mi) % 3.25/0.79 % (3011331)% WARNING: option uhcvi not known. % 3.25/0.79 % (3011331)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=425399953:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 3.25/0.79 % (3011332)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1284392746:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 3.25/0.79 % (3011333)dis+10_1_sil=32000:sp=arity:random_seed=3259411611:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 3.25/0.79 % (3011335)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1279533847:i=131_2999 on theBenchmark for (2999ds/131Mi) % 3.25/0.79 % (3011334)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2319001967:i=116_2999 on theBenchmark for (2999ds/116Mi) % 3.25/0.79 % (3011336)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3300823557:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 3.25/0.79 % Detected minimum model sizes of [3] % 3.25/0.79 % Detected maximum model sizes of [max] % 3.25/0.79 % (3011330)Cannot represent all propositional literals internally % 3.25/0.79 % (3011330)Refutation not found, incomplete strategy % 3.25/0.79 % (3011330)------------------------------ % 3.25/0.79 % (3011330)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.25/0.79 % (3011330)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.25/0.79 % (3011330)CaDiCaL version: 2.1.3 % 3.25/0.79 % (3011330)Termination reason: Refutation not found, incomplete strategy % 3.25/0.79 % (3011330)Time elapsed: 0.043 s % 3.25/0.79 % (3011330)Peak memory usage: 13 MB % 3.25/0.79 % (3011330)Instructions burned: 155 (million) % 3.25/0.79 % (3011330)------------------------------ % 3.25/0.79 % (3011330)------------------------------ % 3.25/0.79 % (3011344)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=989840656:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 3.25/0.79 % (3011334)Instruction limit reached! % 3.25/0.79 % (3011334)------------------------------ % 3.25/0.79 % (3011334)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.25/0.79 % (3011334)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.25/0.79 % (3011334)CaDiCaL version: 2.1.3 % 3.25/0.79 % (3011334)Termination reason: Instruction limit % 3.25/0.79 % (3011334)Termination phase: Saturation % 3.25/0.79 % (3011334)Time elapsed: 0.055 s % 3.25/0.79 % (3011334)Peak memory usage: 12 MB % 3.25/0.79 % (3011334)Instructions burned: 118 (million) % 3.25/0.79 % (3011336)Instruction limit reached! % 3.25/0.79 % (3011336)------------------------------ % 3.25/0.79 % (3011336)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.25/0.79 % (3011336)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.25/0.79 % (3011336)CaDiCaL version: 2.1.3 % 3.25/0.79 % (3011336)Termination reason: Instruction limit % 3.25/0.79 % (3011336)Termination phase: Saturation % 3.25/0.79 % (3011336)Time elapsed: 0.061 s % 3.25/0.79 % (3011336)Peak memory usage: 12 MB % 3.25/0.79 % (3011336)Instructions burned: 161 (million) % 3.25/0.79 % (3011333)Instruction limit reached! % 3.25/0.79 % (3011333)------------------------------ % 3.25/0.79 % (3011333)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.25/0.79 % (3011333)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.25/0.79 % (3011333)CaDiCaL version: 2.1.3 % 3.25/0.79 % (3011333)Termination reason: Instruction limit % 3.25/0.79 % (3011333)Termination phase: Saturation % 3.25/0.79 % (3011333)Time elapsed: 0.063 s % 3.25/0.79 % (3011333)Peak memory usage: 12 MB % 3.25/0.79 % (3011333)Instructions burned: 104 (million) % 3.25/0.79 % (3011346)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1978734045:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 3.25/0.79 % (3011335)Instruction limit reached! % 3.25/0.79 % (3011335)------------------------------ % 3.25/0.79 % (3011335)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.25/0.79 % (3011335)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.25/0.79 % (3011335)CaDiCaL version: 2.1.3 % 3.25/0.79 % (3011335)Termination reason: Instruction limit % 3.25/0.79 % (3011335)Termination phase: Saturation % 3.25/0.79 % (3011335)Time elapsed: 0.078 s % 6.73/1.24 % (3011335)Peak memory usage: 13 MB % 6.73/1.24 % (3011335)Instructions burned: 132 (million) % 6.73/1.24 % (3011348)ott-21_1_sil=16000:fs=off:random_seed=1407497708:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 6.73/1.24 % (3011347)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=1682923801:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi) % 6.73/1.24 % Detected minimum model sizes of [3] % 6.73/1.24 % Detected maximum model sizes of [max] % 6.73/1.24 % (3011344)Cannot represent all propositional literals internally % 6.73/1.24 % (3011344)Refutation not found, incomplete strategy % 6.73/1.24 % (3011344)------------------------------ % 6.73/1.24 % (3011344)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.73/1.24 % (3011344)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.73/1.24 % (3011344)CaDiCaL version: 2.1.3 % 6.73/1.24 % (3011344)Termination reason: Refutation not found, incomplete strategy % 6.73/1.24 % (3011344)Time elapsed: 0.047 s % 6.73/1.24 % (3011344)Peak memory usage: 12 MB % 6.73/1.24 % (3011344)Instructions burned: 184 (million) % 6.73/1.24 % (3011344)------------------------------ % 6.73/1.24 % (3011344)------------------------------ % 6.73/1.24 % (3011350)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2096059516:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 6.73/1.24 % (3011353)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2901996547:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 6.73/1.24 % Detected minimum model sizes of [3] % 6.73/1.24 % Detected maximum model sizes of [max] % 6.73/1.24 % (3011353)Cannot represent all propositional literals internally % 6.73/1.24 % (3011353)Refutation not found, incomplete strategy % 6.73/1.24 % (3011353)------------------------------ % 6.73/1.24 % (3011353)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.73/1.24 % (3011353)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.73/1.24 % (3011353)CaDiCaL version: 2.1.3 % 6.73/1.24 % (3011353)Termination reason: Refutation not found, incomplete strategy % 6.73/1.24 % (3011353)Time elapsed: 0.041 s % 6.73/1.24 % (3011353)Peak memory usage: 12 MB % 6.73/1.24 % (3011353)Instructions burned: 151 (million) % 6.73/1.24 % (3011353)------------------------------ % 6.73/1.24 % (3011353)------------------------------ % 6.73/1.24 % (3011346)Instruction limit reached! % 6.73/1.24 % (3011346)------------------------------ % 6.73/1.24 % (3011346)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.73/1.24 % (3011346)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.73/1.24 % (3011346)CaDiCaL version: 2.1.3 % 6.73/1.24 % (3011346)Termination reason: Instruction limit % 6.73/1.24 % (3011346)Termination phase: Saturation % 6.73/1.24 % (3011346)Time elapsed: 0.081 s % 6.73/1.24 % (3011346)Peak memory usage: 14 MB % 6.73/1.24 % (3011346)Instructions burned: 131 (million) % 6.73/1.24 % (3011356)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3373176304:i=1179_2998 on theBenchmark for (2998ds/1179Mi) % 6.73/1.24 % (3011357)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1506981956:i=889:ins=1_2997 on theBenchmark for (2997ds/889Mi) % 6.73/1.24 % (3011348)Instruction limit reached! % 6.73/1.24 % (3011348)------------------------------ % 6.73/1.24 % (3011348)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.73/1.24 % (3011348)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.73/1.24 % (3011348)CaDiCaL version: 2.1.3 % 6.73/1.24 % (3011348)Termination reason: Instruction limit % 6.73/1.24 % (3011348)Termination phase: Saturation % 6.73/1.24 % (3011348)Time elapsed: 0.099 s % 6.73/1.24 % (3011348)Peak memory usage: 13 MB % 6.73/1.24 % (3011348)Instructions burned: 181 (million) % 6.73/1.24 % (3011360)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=1423052357:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2997 on theBenchmark for (2997ds/692Mi) % 6.73/1.24 % (3011357)Cannot represent all propositional literals internally % 6.73/1.24 % (3011357)Refutation not found, incomplete strategy % 6.73/1.24 % (3011357)------------------------------ % 6.73/1.24 % (3011357)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.73/1.24 % (3011357)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.25/2.74 % (3011357)CaDiCaL version: 2.1.3 % 17.25/2.74 % (3011357)Termination reason: Refutation not found, incomplete strategy % 17.25/2.74 % (3011357)Time elapsed: 0.080 s % 17.25/2.74 % (3011357)Peak memory usage: 13 MB % 17.25/2.74 % (3011357)Instructions burned: 156 (million) % 17.25/2.74 % (3011357)------------------------------ % 17.25/2.74 % (3011357)------------------------------ % 17.25/2.74 % (3011362)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1790442286:i=879:kws=inv_precedence:fsr=off_2996 on theBenchmark for (2996ds/879Mi) % 17.25/2.74 % (3011347)Instruction limit reached! % 17.25/2.74 % (3011347)------------------------------ % 17.25/2.74 % (3011347)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 17.25/2.74 % (3011347)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.25/2.74 % (3011347)CaDiCaL version: 2.1.3 % 17.25/2.74 % (3011347)Termination reason: Instruction limit % 17.25/2.74 % (3011347)Termination phase: Saturation % 17.25/2.74 % (3011347)Time elapsed: 0.293 s % 17.25/2.74 % (3011347)Peak memory usage: 16 MB % 17.25/2.74 % (3011347)Instructions burned: 686 (million) % 17.25/2.74 % (3011350)Instruction limit reached! % 17.25/2.74 % (3011350)------------------------------ % 17.25/2.74 % (3011350)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 17.25/2.74 % (3011350)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.25/2.74 % (3011350)CaDiCaL version: 2.1.3 % 17.25/2.74 % (3011350)Termination reason: Instruction limit % 17.25/2.74 % (3011350)Termination phase: Saturation % 17.25/2.74 % (3011350)Time elapsed: 0.278 s % 17.25/2.74 % (3011350)Peak memory usage: 15 MB % 17.25/2.74 % (3011350)Instructions burned: 479 (million) % 17.25/2.74 % (3011365)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1846749974:i=9515:nm=5_2995 on theBenchmark for (2995ds/9515Mi) % 17.25/2.74 % (3011364)fmb+10_1_sil=64000:random_seed=244293898:i=22061:nm=2:gsp=on_2995 on theBenchmark for (2995ds/22061Mi) % 17.25/2.74 % Detected minimum model sizes of [3] % 17.25/2.74 % Detected maximum model sizes of [max] % 17.25/2.74 % (3011364)Cannot represent all propositional literals internally % 17.25/2.74 % (3011364)Refutation not found, incomplete strategy % 17.25/2.74 % (3011364)------------------------------ % 17.25/2.74 % (3011364)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 17.25/2.74 % (3011364)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.25/2.74 % (3011364)CaDiCaL version: 2.1.3 % 17.25/2.74 % (3011364)Termination reason: Refutation not found, incomplete strategy % 17.25/2.74 % (3011364)Time elapsed: 0.078 s % 17.25/2.74 % (3011364)Peak memory usage: 12 MB % 17.25/2.74 % (3011364)Instructions burned: 152 (million) % 17.25/2.74 % Detected minimum model sizes of [3] % 17.25/2.74 % Detected maximum model sizes of [max] % 17.25/2.74 % (3011365)Cannot represent all propositional literals internally % 17.25/2.74 % (3011365)Refutation not found, incomplete strategy % 17.25/2.74 % (3011365)------------------------------ % 17.25/2.74 % (3011365)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 17.25/2.74 % (3011365)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.25/2.74 % (3011365)CaDiCaL version: 2.1.3 % 17.25/2.74 % (3011365)Termination reason: Refutation not found, incomplete strategy % 17.25/2.74 % (3011365)Time elapsed: 0.078 s % 17.25/2.74 % (3011365)Peak memory usage: 12 MB % 17.25/2.74 % (3011365)Instructions burned: 151 (million) % 17.25/2.74 % (3011364)------------------------------ % 17.25/2.74 % (3011364)------------------------------ % 17.25/2.74 % (3011365)------------------------------ % 17.25/2.74 % (3011365)------------------------------ % 17.25/2.74 % (3011368)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3973085128:fmbsr=1.7:i=920_2994 on theBenchmark for (2994ds/920Mi) % 17.25/2.74 % (3011369)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=3813813767:i=5131_2994 on theBenchmark for (2994ds/5131Mi) % 17.25/2.74 % (3011356)Instruction limit reached! % 17.25/2.74 % (3011356)------------------------------ % 17.25/2.74 % (3011356)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 17.25/2.74 % (3011356)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.25/2.74 % (3011356)CaDiCaL version: 2.1.3 % 17.25/2.74 % (3011356)Termination reason: Instruction limit % 17.25/2.74 % (3011356)Termination phase: Saturation % 17.25/2.74 % (3011356)Time elapsed: 0.356 s % 17.25/2.74 % (3011356)Peak memory usage: 29 MB % 17.25/2.74 % (3011356)Instructions burned: 1182 (million) % 17.25/2.74 % (3011372)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3375972408:i=1472:ins=7:fdi=8:gsp=on_2994 on theBenchmark for (2994ds/1472Mi) % 22.76/3.55 % Detected minimum model sizes of [3] % 22.76/3.55 % Detected maximum model sizes of [max] % 22.76/3.55 % (3011368)Cannot represent all propositional literals internally % 22.76/3.55 % (3011368)Refutation not found, incomplete strategy % 22.76/3.55 % (3011368)------------------------------ % 22.76/3.55 % (3011368)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.76/3.55 % (3011368)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.76/3.55 % (3011368)CaDiCaL version: 2.1.3 % 22.76/3.55 % (3011368)Termination reason: Refutation not found, incomplete strategy % 22.76/3.55 % (3011368)Time elapsed: 0.078 s % 22.76/3.55 % (3011368)Peak memory usage: 12 MB % 22.76/3.55 % (3011368)Instructions burned: 151 (million) % 22.76/3.55 % (3011368)------------------------------ % 22.76/3.55 % (3011368)------------------------------ % 22.76/3.55 % (3011360)Instruction limit reached! % 22.76/3.55 % (3011360)------------------------------ % 22.76/3.55 % (3011360)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.76/3.55 % (3011360)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.76/3.55 % (3011360)CaDiCaL version: 2.1.3 % 22.76/3.55 % (3011360)Termination reason: Instruction limit % 22.76/3.55 % (3011360)Termination phase: Saturation % 22.76/3.55 % (3011360)Time elapsed: 0.392 s % 22.76/3.55 % (3011360)Peak memory usage: 20 MB % 22.76/3.55 % (3011360)Instructions burned: 693 (million) % 22.76/3.55 % (3011374)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3855266521:i=6324_2993 on theBenchmark for (2993ds/6324Mi) % 22.76/3.55 % (3011375)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1582257827:fmbsr=2.30978:i=2174_2993 on theBenchmark for (2993ds/2174Mi) % 22.76/3.55 % Detected minimum model sizes of [3] % 22.76/3.55 % Detected maximum model sizes of [max] % 22.76/3.55 % (3011374)Cannot represent all propositional literals internally % 22.76/3.55 % (3011374)Refutation not found, incomplete strategy % 22.76/3.55 % (3011374)------------------------------ % 22.76/3.55 % (3011374)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.76/3.55 % (3011374)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.76/3.55 % (3011374)CaDiCaL version: 2.1.3 % 22.76/3.55 % (3011374)Termination reason: Refutation not found, incomplete strategy % 22.76/3.55 % (3011374)Time elapsed: 0.080 s % 22.76/3.55 % (3011374)Peak memory usage: 13 MB % 22.76/3.55 % (3011374)Instructions burned: 155 (million) % 22.76/3.55 % (3011374)------------------------------ % 22.76/3.55 % (3011374)------------------------------ % 22.76/3.55 % (3011378)ott-2_1_sil=16000:newcnf=on:random_seed=3390827878:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2992 on theBenchmark for (2992ds/869Mi) % 22.76/3.55 % (3011362)Instruction limit reached! % 22.76/3.55 % (3011362)------------------------------ % 22.76/3.55 % (3011362)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.76/3.55 % (3011362)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.76/3.55 % (3011362)CaDiCaL version: 2.1.3 % 22.76/3.55 % (3011362)Termination reason: Instruction limit % 22.76/3.55 % (3011362)Termination phase: Saturation % 22.76/3.55 % (3011362)Time elapsed: 0.485 s % 22.76/3.55 % (3011362)Peak memory usage: 19 MB % 22.76/3.55 % (3011362)Instructions burned: 879 (million) % 22.76/3.55 % (3011380)ott+10_1_sil=32000:tgt=ground:random_seed=3162437853:i=5114:av=off_2991 on theBenchmark for (2991ds/5114Mi) % 22.76/3.55 % (3011372)Instruction limit reached! % 22.76/3.55 % (3011372)------------------------------ % 22.76/3.55 % (3011372)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.76/3.55 % (3011372)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.76/3.55 % (3011372)CaDiCaL version: 2.1.3 % 22.76/3.55 % (3011372)Termination reason: Instruction limit % 22.76/3.55 % (3011372)Termination phase: Saturation % 22.76/3.55 % (3011372)Time elapsed: 0.423 s % 22.76/3.55 % (3011372)Peak memory usage: 28 MB % 22.76/3.55 % (3011372)Instructions burned: 1474 (million) % 22.76/3.55 % (3011382)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2786891972:i=54282_2990 on theBenchmark for (2990ds/54282Mi) % 22.76/3.55 % (3011378)Instruction limit reached! % 22.76/3.55 % (3011378)------------------------------ % 22.76/3.55 % (3011378)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.76/3.55 % (3011378)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 60.14/8.79 % (3011378)CaDiCaL version: 2.1.3 % 60.14/8.79 % (3011378)Termination reason: Instruction limit % 60.14/8.79 % (3011378)Termination phase: Saturation % 60.14/8.79 % (3011378)Time elapsed: 0.283 s % 60.14/8.79 % (3011378)Peak memory usage: 12 MB % 60.14/8.79 % (3011378)Instructions burned: 872 (million) % 60.14/8.79 % (3011384)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=4183713937:i=3512:aac=none_2989 on theBenchmark for (2989ds/3512Mi) % 60.14/8.79 % Detected minimum model sizes of [3] % 60.14/8.79 % Detected maximum model sizes of [max] % 60.14/8.79 % (3011382)Cannot represent all propositional literals internally % 60.14/8.79 % (3011382)Refutation not found, incomplete strategy % 60.14/8.79 % (3011382)------------------------------ % 60.14/8.79 % (3011382)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 60.14/8.79 % (3011382)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 60.14/8.79 % (3011382)CaDiCaL version: 2.1.3 % 60.14/8.79 % (3011382)Termination reason: Refutation not found, incomplete strategy % 60.14/8.79 % (3011382)Time elapsed: 0.043 s % 60.14/8.79 % (3011382)Peak memory usage: 13 MB % 60.14/8.79 % (3011382)Instructions burned: 155 (million) % 60.14/8.79 % (3011382)------------------------------ % 60.14/8.79 % (3011382)------------------------------ % 60.14/8.79 % (3011386)dis+21_1_sil=32000:sas=cadical:random_seed=38254562:i=3773:amm=off_2989 on theBenchmark for (2989ds/3773Mi) % 60.14/8.79 % Detected minimum model sizes of [3] % 60.14/8.79 % Detected maximum model sizes of [max] % 60.14/8.79 % (3011375)Cannot represent all propositional literals internally % 60.14/8.79 % (3011375)Refutation not found, incomplete strategy % 60.14/8.79 % (3011375)------------------------------ % 60.14/8.79 % (3011375)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 60.14/8.79 % (3011375)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 60.14/8.79 % (3011375)CaDiCaL version: 2.1.3 % 60.14/8.79 % (3011375)Termination reason: Refutation not found, incomplete strategy % 60.14/8.79 % (3011375)Time elapsed: 0.592 s % 60.14/8.79 % (3011375)Peak memory usage: 20 MB % 60.14/8.79 % (3011375)Instructions burned: 1112 (million) % 60.14/8.79 % (3011375)------------------------------ % 60.14/8.79 % (3011375)------------------------------ % 60.14/8.79 % (3011388)ott+11_1_sil=16000:gs=on:random_seed=1381821253:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2987 on theBenchmark for (2987ds/2251Mi) % 60.14/8.79 % (3011386)Instruction limit reached! % 60.14/8.79 % (3011386)------------------------------ % 60.14/8.79 % (3011386)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 60.14/8.79 % (3011386)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 60.14/8.79 % (3011386)CaDiCaL version: 2.1.3 % 60.14/8.79 % (3011386)Termination reason: Instruction limit % 60.14/8.79 % (3011386)Termination phase: Saturation % 60.14/8.79 % (3011386)Time elapsed: 1.044 s % 60.14/8.79 % (3011386)Peak memory usage: 39 MB % 60.14/8.79 % (3011386)Instructions burned: 3774 (million) % 60.14/8.79 % (3011390)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=1606044865:fmbsr=1.6:i=67534_2978 on theBenchmark for (2978ds/67534Mi) % 60.14/8.79 % Detected minimum model sizes of [3] % 60.14/8.79 % Detected maximum model sizes of [max] % 60.14/8.79 % (3011390)Cannot represent all propositional literals internally % 60.14/8.79 % (3011390)Refutation not found, incomplete strategy % 60.14/8.79 % (3011390)------------------------------ % 60.14/8.79 % (3011390)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 60.14/8.79 % (3011390)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 60.14/8.79 % (3011390)CaDiCaL version: 2.1.3 % 60.14/8.79 % (3011390)Termination reason: Refutation not found, incomplete strategy % 60.14/8.79 % (3011390)Time elapsed: 0.049 s % 60.14/8.79 % (3011390)Peak memory usage: 12 MB % 60.14/8.79 % (3011390)Instructions burned: 193 (million) % 60.14/8.79 % (3011390)------------------------------ % 60.14/8.79 % (3011390)------------------------------ % 60.14/8.79 % (3011392)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=3470792864:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2978 on theBenchmark for (2978ds/4591Mi) % 60.14/8.79 % (3011388)Instruction limit reached! % 60.14/8.79 % (3011388)------------------------------ % 60.14/8.79 % (3011388)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 60.14/8.79 % (3011388)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 117.61/16.82 % (3011388)CaDiCaL version: 2.1.3 % 117.61/16.82 % (3011388)Termination reason: Instruction limit % 117.61/16.82 % (3011388)Termination phase: Saturation % 117.61/16.82 % (3011388)Time elapsed: 1.248 s % 117.61/16.82 % (3011388)Peak memory usage: 38 MB % 117.61/16.82 % (3011388)Instructions burned: 2252 (million) % 117.61/16.82 % (3011394)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=1943503488:i=29340_2974 on theBenchmark for (2974ds/29340Mi) % 117.61/16.82 % (3011384)Instruction limit reached! % 117.61/16.82 % (3011384)------------------------------ % 117.61/16.82 % (3011384)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 117.61/16.82 % (3011384)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 117.61/16.82 % (3011384)CaDiCaL version: 2.1.3 % 117.61/16.82 % (3011384)Termination reason: Instruction limit % 117.61/16.82 % (3011384)Termination phase: Saturation % 117.61/16.82 % (3011384)Time elapsed: 1.838 s % 117.61/16.82 % (3011384)Peak memory usage: 38 MB % 117.61/16.82 % (3011384)Instructions burned: 3513 (million) % 117.61/16.82 % (3011396)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=508647459:i=5211_2971 on theBenchmark for (2971ds/5211Mi) % 117.61/16.82 % (3011369)Instruction limit reached! % 117.61/16.82 % (3011369)------------------------------ % 117.61/16.82 % (3011369)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 117.61/16.82 % (3011369)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 117.61/16.82 % (3011369)CaDiCaL version: 2.1.3 % 117.61/16.82 % (3011369)Termination reason: Instruction limit % 117.61/16.82 % (3011369)Termination phase: Saturation % 117.61/16.82 % (3011369)Time elapsed: 2.667 s % 117.61/16.82 % (3011369)Peak memory usage: 48 MB % 117.61/16.82 % (3011369)Instructions burned: 5131 (million) % 117.61/16.82 % (3011398)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=130321023:i=5497:nm=2_2967 on theBenchmark for (2967ds/5497Mi) % 117.61/16.82 % (3011392)Instruction limit reached! % 117.61/16.82 % (3011392)------------------------------ % 117.61/16.82 % (3011392)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 117.61/16.82 % (3011392)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 117.61/16.82 % (3011392)CaDiCaL version: 2.1.3 % 117.61/16.82 % (3011392)Termination reason: Instruction limit % 117.61/16.82 % (3011392)Termination phase: Saturation % 117.61/16.82 % (3011392)Time elapsed: 1.059 s % 117.61/16.82 % (3011392)Peak memory usage: 37 MB % 117.61/16.82 % (3011392)Instructions burned: 4595 (million) % 117.61/16.82 % (3011400)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=3197804722:fmbsr=2:i=46332_2967 on theBenchmark for (2967ds/46332Mi) % 117.61/16.82 % Detected minimum model sizes of [3] % 117.61/16.82 % Detected maximum model sizes of [max] % 117.61/16.82 % (3011400)Cannot represent all propositional literals internally % 117.61/16.82 % (3011400)Refutation not found, incomplete strategy % 117.61/16.82 % (3011400)------------------------------ % 117.61/16.82 % (3011400)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 117.61/16.82 % (3011400)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 117.61/16.82 % (3011400)CaDiCaL version: 2.1.3 % 117.61/16.82 % (3011400)Termination reason: Refutation not found, incomplete strategy % 117.61/16.82 % (3011400)Time elapsed: 0.049 s % 117.61/16.82 % (3011400)Peak memory usage: 12 MB % 117.61/16.82 % (3011400)Instructions burned: 193 (million) % 117.61/16.82 % (3011400)------------------------------ % 117.61/16.82 % (3011400)------------------------------ % 117.61/16.82 % Detected minimum model sizes of [3] % 117.61/16.82 % Detected maximum model sizes of [max] % 117.61/16.82 % (3011398)Cannot represent all propositional literals internally % 117.61/16.82 % (3011398)Refutation not found, incomplete strategy % 117.61/16.82 % (3011398)------------------------------ % 117.61/16.82 % (3011398)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 117.61/16.82 % (3011398)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 117.61/16.82 % (3011398)CaDiCaL version: 2.1.3 % 117.61/16.82 % (3011398)Termination reason: Refutation not found, incomplete strategy % 117.61/16.82 % (3011398)Time elapsed: 0.081 s % 117.61/16.82 % (3011398)Peak memory usage: 13 MB % 117.61/16.82 % (3011398)Instructions burned: 155 (million) % 117.61/16.82 % (3011398)------------------------------ % 117.61/16.82 % (3011398)------------------------------ % 117.61/16.82 % (3011402)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=2451089853:i=14071_2966 on theBenchmark for (2966ds/14071Mi) % 117.61/16.82 % (3011403)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=4101634486:i=22565:add=on:rawr=on_2966 on theBenchmark for (2966ds/22565Mi) % 119.89/17.17 % Detected minimum model sizes of [3] % 119.89/17.17 % Detected maximum model sizes of [max] % 119.89/17.17 % (3011402)Cannot represent all propositional literals internally % 119.89/17.17 % (3011402)Refutation not found, incomplete strategy % 119.89/17.17 % (3011402)------------------------------ % 119.89/17.17 % (3011402)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 119.89/17.17 % (3011402)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 119.89/17.17 % (3011402)CaDiCaL version: 2.1.3 % 119.89/17.17 % (3011402)Termination reason: Refutation not found, incomplete strategy % 119.89/17.17 % (3011402)Time elapsed: 0.044 s % 119.89/17.17 % (3011402)Peak memory usage: 13 MB % 119.89/17.17 % (3011402)Instructions burned: 160 (million) % 119.89/17.17 % (3011402)------------------------------ % 119.89/17.17 % (3011402)------------------------------ % 119.89/17.17 % (3011406)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=3878462876:i=8173:av=off_2966 on theBenchmark for (2966ds/8173Mi) % 119.89/17.17 % (3011380)Instruction limit reached! % 119.89/17.17 % (3011380)------------------------------ % 119.89/17.17 % (3011380)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 119.89/17.17 % (3011380)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 119.89/17.17 % (3011380)CaDiCaL version: 2.1.3 % 119.89/17.17 % (3011380)Termination reason: Instruction limit % 119.89/17.17 % (3011380)Termination phase: Saturation % 119.89/17.17 % (3011380)Time elapsed: 2.957 s % 119.89/17.17 % (3011380)Peak memory usage: 93 MB % 119.89/17.17 % (3011380)Instructions burned: 5114 (million) % 119.89/17.17 % (3011408)dis+10_16:1_sil=16000:random_seed=2660862857:i=9155:fsr=off_2962 on theBenchmark for (2962ds/9155Mi) % 119.89/17.17 % (3011396)Instruction limit reached! % 119.89/17.17 % (3011396)------------------------------ % 119.89/17.17 % (3011396)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 119.89/17.17 % (3011396)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 119.89/17.17 % (3011396)CaDiCaL version: 2.1.3 % 119.89/17.17 % (3011396)Termination reason: Instruction limit % 119.89/17.17 % (3011396)Termination phase: Saturation % 119.89/17.17 % (3011396)Time elapsed: 2.716 s % 119.89/17.17 % (3011396)Peak memory usage: 47 MB % 119.89/17.17 % (3011396)Instructions burned: 5211 (million) % 119.89/17.17 % (3011410)ott-3_8_sil=64000:random_seed=1944966122:i=20139:bs=on_2943 on theBenchmark for (2943ds/20139Mi) % 119.89/17.17 % (3011406)Instruction limit reached! % 119.89/17.17 % (3011406)------------------------------ % 119.89/17.17 % (3011406)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 119.89/17.17 % (3011406)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 119.89/17.17 % (3011406)CaDiCaL version: 2.1.3 % 119.89/17.17 % (3011406)Termination reason: Instruction limit % 119.89/17.17 % (3011406)Termination phase: Saturation % 119.89/17.17 % (3011406)Time elapsed: 2.530 s % 119.89/17.17 % (3011406)Peak memory usage: 136 MB % 119.89/17.17 % (3011406)Instructions burned: 8176 (million) % 119.89/17.17 % (3011412)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=1239828166:fmbsr=2:i=32576_2940 on theBenchmark for (2940ds/32576Mi) % 119.89/17.17 % Detected minimum model sizes of [3] % 119.89/17.17 % Detected maximum model sizes of [max] % 119.89/17.17 % (3011412)Cannot represent all propositional literals internally % 119.89/17.17 % (3011412)Refutation not found, incomplete strategy % 119.89/17.17 % (3011412)------------------------------ % 119.89/17.17 % (3011412)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 119.89/17.17 % (3011412)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 119.89/17.17 % (3011412)CaDiCaL version: 2.1.3 % 119.89/17.17 % (3011412)Termination reason: Refutation not found, incomplete strategy % 119.89/17.17 % (3011412)Time elapsed: 0.044 s % 119.89/17.17 % (3011412)Peak memory usage: 13 MB % 119.89/17.17 % (3011412)Instructions burned: 164 (million) % 119.89/17.17 % (3011412)------------------------------ % 119.89/17.17 % (3011412)------------------------------ % 119.89/17.17 % (3011414)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=1867769091:i=11404_2940 on theBenchmark for (2940ds/11404Mi) % 119.89/17.17 % (3011408)Instruction limit reached! % 119.89/17.17 % (3011408)------------------------------ % 119.89/17.17 % (3011408)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 119.89/17.17 % (3011408)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 119.89/17.17 % (3011408)CaDiCaL version: 2.1.3 % 119.89/17.17 % (3011408)Termination reason: Instruction limit % 127.47/18.25 % (3011408)Termination phase: Saturation % 127.47/18.25 % (3011408)Time elapsed: 4.754 s % 127.47/18.25 % (3011408)Peak memory usage: 72 MB % 127.47/18.25 % (3011408)Instructions burned: 9155 (million) % 127.47/18.25 % (3011416)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=2465197291:i=14134_2914 on theBenchmark for (2914ds/14134Mi) % 127.47/18.25 % (3011414)Instruction limit reached! % 127.47/18.25 % (3011414)------------------------------ % 127.47/18.25 % (3011414)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 127.47/18.25 % (3011414)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 127.47/18.25 % (3011414)CaDiCaL version: 2.1.3 % 127.47/18.25 % (3011414)Termination reason: Instruction limit % 127.47/18.25 % (3011414)Termination phase: Saturation % 127.47/18.25 % (3011414)Time elapsed: 3.559 s % 127.47/18.25 % (3011414)Peak memory usage: 184 MB % 127.47/18.25 % (3011414)Instructions burned: 11405 (million) % 127.47/18.25 % (3011418)dis+33_16_sil=32000:sac=on:random_seed=2952165596:i=15851:nm=0_2904 on theBenchmark for (2904ds/15851Mi) % 127.47/18.25 % (3011410)Instruction limit reached! % 127.47/18.25 % (3011410)------------------------------ % 127.47/18.25 % (3011410)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 127.47/18.25 % (3011410)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 127.47/18.25 % (3011410)CaDiCaL version: 2.1.3 % 127.47/18.25 % (3011410)Termination reason: Instruction limit % 127.47/18.25 % (3011410)Termination phase: Saturation % 127.47/18.25 % (3011410)Time elapsed: 6.534 s % 127.47/18.25 % (3011410)Peak memory usage: 15 MB % 127.47/18.25 % (3011410)Instructions burned: 20142 (million) % 127.47/18.25 % (3011420)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=2753470950:avsq=on:i=17627:add=on:amm=off_2878 on theBenchmark for (2878ds/17627Mi) % 127.47/18.25 % (3011403)Instruction limit reached! % 127.47/18.25 % (3011403)------------------------------ % 127.47/18.25 % (3011403)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 127.47/18.25 % (3011403)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 127.47/18.25 % (3011403)CaDiCaL version: 2.1.3 % 127.47/18.25 % (3011403)Termination reason: Instruction limit % 127.47/18.25 % (3011403)Termination phase: Saturation % 127.47/18.25 % (3011403)Time elapsed: 9.291 s % 127.47/18.25 % (3011403)Peak memory usage: 47 MB % 127.47/18.25 % (3011403)Instructions burned: 22567 (million) % 127.47/18.25 % (3011422)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=417248078:s2a=on:i=53295_2873 on theBenchmark for (2873ds/53295Mi) % 127.47/18.25 % (3011418)Instruction limit reached! % 127.47/18.25 % (3011418)------------------------------ % 127.47/18.25 % (3011418)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 127.47/18.25 % (3011418)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 127.47/18.25 % (3011418)CaDiCaL version: 2.1.3 % 127.47/18.25 % (3011418)Termination reason: Instruction limit % 127.47/18.25 % (3011418)Termination phase: Saturation % 127.47/18.25 % (3011418)Time elapsed: 4.451 s % 127.47/18.25 % (3011418)Peak memory usage: 132 MB % 127.47/18.25 % (3011418)Instructions burned: 15854 (million) % 127.47/18.25 % (3011424)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=1514890080:i=26857:ins=20_2859 on theBenchmark for (2859ds/26857Mi) % 127.47/18.25 % Detected minimum model sizes of [3] % 127.47/18.25 % Detected maximum model sizes of [max] % 127.47/18.25 % (3011424)Cannot represent all propositional literals internally % 127.47/18.25 % (3011424)Refutation not found, incomplete strategy % 127.47/18.25 % (3011424)------------------------------ % 127.47/18.25 % (3011424)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 127.47/18.25 % (3011424)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 127.47/18.25 % (3011424)CaDiCaL version: 2.1.3 % 127.47/18.25 % (3011424)Termination reason: Refutation not found, incomplete strategy % 127.47/18.25 % (3011424)Time elapsed: 0.042 s % 127.47/18.25 % (3011424)Peak memory usage: 12 MB % 127.47/18.25 % (3011424)Instructions burned: 151 (million) % 127.47/18.25 % (3011424)------------------------------ % 127.47/18.25 % (3011424)------------------------------ % 127.47/18.25 % (3011426)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=3551133609:i=28120:bs=on:fsr=off_2859 on theBenchmark for (2859ds/28120Mi) % 127.47/18.25 % (3011394)Instruction limit reached! % 127.47/18.25 % (3011394)------------------------------ % 127.47/18.25 % (3011394)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 127.47/18.25 % (3011394)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 137.37/19.70 % (3011394)CaDiCaL version: 2.1.3 % 137.37/19.70 % (3011394)Termination reason: Instruction limit % 137.37/19.70 % (3011394)Termination phase: Saturation % 137.37/19.70 % (3011394)Time elapsed: 14.060 s % 137.37/19.70 % (3011394)Peak memory usage: 283 MB % 137.37/19.70 % (3011394)Instructions burned: 29342 (million) % 137.37/19.70 % (3011428)fmb+10_1_sil=256000:fmbss=7:random_seed=3111662316:fmbsr=1.6:i=182295_2833 on theBenchmark for (2833ds/182295Mi) % 137.37/19.70 % Detected minimum model sizes of [3] % 137.37/19.70 % Detected maximum model sizes of [max] % 137.37/19.70 % (3011428)Cannot represent all propositional literals internally % 137.37/19.70 % (3011428)Refutation not found, incomplete strategy % 137.37/19.70 % (3011428)------------------------------ % 137.37/19.70 % (3011428)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 137.37/19.70 % (3011428)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 137.37/19.70 % (3011428)CaDiCaL version: 2.1.3 % 137.37/19.70 % (3011428)Termination reason: Refutation not found, incomplete strategy % 137.37/19.70 % (3011428)Time elapsed: 0.078 s % 137.37/19.70 % (3011428)Peak memory usage: 12 MB % 137.37/19.70 % (3011428)Instructions burned: 151 (million) % 137.37/19.70 % (3011428)------------------------------ % 137.37/19.70 % (3011428)------------------------------ % 137.37/19.70 % (3011430)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=3916337700:i=44625:gsp=on_2832 on theBenchmark for (2832ds/44625Mi) % 137.37/19.70 % (3011416)Instruction limit reached! % 137.37/19.70 % (3011416)------------------------------ % 137.37/19.70 % (3011416)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 137.37/19.70 % (3011416)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 137.37/19.70 % (3011416)CaDiCaL version: 2.1.3 % 137.37/19.70 % (3011416)Termination reason: Instruction limit % 137.37/19.70 % (3011416)Termination phase: Saturation % 137.37/19.70 % (3011416)Time elapsed: 8.201 s % 137.37/19.70 % (3011416)Peak memory usage: 246 MB % 137.37/19.70 % (3011416)Instructions burned: 14134 (million) % 137.37/19.70 % Detected minimum model sizes of [3] % 137.37/19.70 % Detected maximum model sizes of [max] % 137.37/19.70 % (3011430)Cannot represent all propositional literals internally % 137.37/19.70 % (3011430)Refutation not found, incomplete strategy % 137.37/19.70 % (3011430)------------------------------ % 137.37/19.70 % (3011430)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 137.37/19.70 % (3011430)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 137.37/19.70 % (3011430)CaDiCaL version: 2.1.3 % 137.37/19.70 % (3011430)Termination reason: Refutation not found, incomplete strategy % 137.37/19.70 % (3011430)Time elapsed: 0.079 s % 137.37/19.70 % (3011430)Peak memory usage: 12 MB % 137.37/19.70 % (3011430)Instructions burned: 152 (million) % 137.37/19.70 % (3011430)------------------------------ % 137.37/19.70 % (3011430)------------------------------ % 137.37/19.70 % (3011432)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=384115352:i=160505_2831 on theBenchmark for (2831ds/160505Mi) % 137.37/19.70 % (3011433)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=4284107871:fmbsr=1.3:i=225729_2831 on theBenchmark for (2831ds/225729Mi) % 137.37/19.70 % Detected minimum model sizes of [3] % 137.37/19.70 % Detected maximum model sizes of [max] % 137.37/19.70 % (3011432)Cannot represent all propositional literals internally % 137.37/19.70 % (3011432)Refutation not found, incomplete strategy % 137.37/19.70 % (3011432)------------------------------ % 137.37/19.70 % (3011432)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 137.37/19.70 % (3011432)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 137.37/19.70 % (3011432)CaDiCaL version: 2.1.3 % 137.37/19.70 % (3011432)Termination reason: Refutation not found, incomplete strategy % 137.37/19.70 % (3011432)Time elapsed: 0.079 s % 137.37/19.70 % (3011432)Peak memory usage: 12 MB % 137.37/19.70 % (3011432)Instructions burned: 151 (million) % 137.37/19.70 % (3011432)------------------------------ % 137.37/19.70 % (3011432)------------------------------ % 137.37/19.70 % Detected minimum model sizes of [3] % 137.37/19.70 % Detected maximum model sizes of [max] % 137.37/19.70 % (3011433)Cannot represent all propositional literals internally % 137.37/19.70 % (3011433)Refutation not found, incomplete strategy % 137.37/19.70 % (3011433)------------------------------ % 137.37/19.70 % (3011433)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 137.37/19.70 % (3011433)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 137.37/19.70 % (3011433)CaDiCaL version: 2.1.3 % 137.37/19.70 % (3011433)Termination reason: Refutation not found, incomplete strategy % 137.37/19.70 % (3011433)Time elapsed: 0.082 s % 158.77/22.69 % (3011433)Peak memory usage: 13 MB % 158.77/22.69 % (3011433)Instructions burned: 160 (million) % 158.77/22.69 % (3011433)------------------------------ % 158.77/22.69 % (3011433)------------------------------ % 158.77/22.69 % (3011436)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=3784014663:fmbsr=2:i=185024:ins=7_2830 on theBenchmark for (2830ds/185024Mi) % 158.77/22.69 % (3011437)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=2133537204:rtra=on_2830 on theBenchmark for (2830ds/0Mi) % 158.77/22.69 % Detected minimum model sizes of [3] % 158.77/22.69 % Detected maximum model sizes of [max] % 158.77/22.69 % (3011436)Cannot represent all propositional literals internally % 158.77/22.69 % (3011436)Refutation not found, incomplete strategy % 158.77/22.69 % (3011436)------------------------------ % 158.77/22.69 % (3011436)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 158.77/22.69 % (3011436)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 158.77/22.69 % (3011436)CaDiCaL version: 2.1.3 % 158.77/22.69 % (3011436)Termination reason: Refutation not found, incomplete strategy % 158.77/22.69 % (3011436)Time elapsed: 0.082 s % 158.77/22.69 % (3011436)Peak memory usage: 13 MB % 158.77/22.69 % (3011436)Instructions burned: 160 (million) % 158.77/22.69 % (3011436)------------------------------ % 158.77/22.69 % (3011436)------------------------------ % 158.77/22.69 % Detected minimum model sizes of [3] % 158.77/22.69 % Detected maximum model sizes of [max] % 158.77/22.69 % (3011437)Cannot represent all propositional literals internally % 158.77/22.69 % (3011437)Refutation not found, incomplete strategy % 158.77/22.69 % (3011437)------------------------------ % 158.77/22.69 % (3011437)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 158.77/22.69 % (3011437)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 158.77/22.69 % (3011437)CaDiCaL version: 2.1.3 % 158.77/22.69 % (3011437)Termination reason: Refutation not found, incomplete strategy % 158.77/22.69 % (3011437)Time elapsed: 0.082 s % 158.77/22.69 % (3011437)Peak memory usage: 13 MB % 158.77/22.69 % (3011437)Instructions burned: 156 (million) % 158.77/22.69 % (3011437)------------------------------ % 158.77/22.69 % (3011437)------------------------------ % 158.77/22.69 % (3011440)% WARNING: option uhcvi not known. % 158.77/22.69 % (3011440)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=4180077994:i=271062:add=off:rtra=on:rawr=on_2829 on theBenchmark for (2829ds/271062Mi) % 158.77/22.69 % (3011441)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3264716090:i=176048:add=on:rtra=on:rawr=on_2829 on theBenchmark for (2829ds/176048Mi) % 158.77/22.69 % (3011420)Instruction limit reached! % 158.77/22.69 % (3011420)------------------------------ % 158.77/22.69 % (3011420)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 158.77/22.69 % (3011420)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 158.77/22.69 % (3011420)CaDiCaL version: 2.1.3 % 158.77/22.69 % (3011420)Termination reason: Instruction limit % 158.77/22.69 % (3011420)Termination phase: Saturation % 158.77/22.69 % (3011420)Time elapsed: 5.554 s % 158.77/22.69 % (3011420)Peak memory usage: 28 MB % 158.77/22.69 % (3011420)Instructions burned: 17627 (million) % 158.77/22.69 % (3011444)dis+10_1_sil=32000:si=on:sp=arity:random_seed=2496018120:i=206:fgj=on:rtra=on_2822 on theBenchmark for (2822ds/206Mi) % 158.77/22.69 % (3011444)Instruction limit reached! % 158.77/22.69 % (3011444)------------------------------ % 158.77/22.69 % (3011444)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 158.77/22.69 % (3011444)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 158.77/22.69 % (3011444)CaDiCaL version: 2.1.3 % 158.77/22.69 % (3011444)Termination reason: Instruction limit % 158.77/22.69 % (3011444)Termination phase: Saturation % 158.77/22.69 % (3011444)Time elapsed: 0.123 s % 158.77/22.69 % (3011444)Peak memory usage: 13 MB % 158.77/22.69 % (3011444)Instructions burned: 207 (million) % 158.77/22.69 % (3011446)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=1181734989:i=232:rtra=on_2820 on theBenchmark for (2820ds/232Mi) % 158.77/22.69 % (3011446)Instruction limit reached! % 158.77/22.69 % (3011446)------------------------------ % 158.77/22.69 % (3011446)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 158.77/22.69 % (3011446)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 158.77/22.69 % (3011446)CaDiCaL version: 2.1.3 % 158.77/22.69 % (3011446)Termination reason: Instruction limit % 158.77/22.69 % (3011446)Termination phase: Saturation % 158.77/22.69 % (3011446)Time elapsed: 0.110 s % 165.62/23.69 % (3011446)Peak memory usage: 13 MB % 165.62/23.69 % (3011446)Instructions burned: 233 (million) % 165.62/23.69 % (3011448)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=3622058747:i=262:rtra=on_2819 on theBenchmark for (2819ds/262Mi) % 165.62/23.69 % (3011448)Instruction limit reached! % 165.62/23.69 % (3011448)------------------------------ % 165.62/23.69 % (3011448)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 165.62/23.69 % (3011448)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 165.62/23.69 % (3011448)CaDiCaL version: 2.1.3 % 165.62/23.69 % (3011448)Termination reason: Instruction limit % 165.62/23.69 % (3011448)Termination phase: Saturation % 165.62/23.69 % (3011448)Time elapsed: 0.155 s % 165.62/23.69 % (3011448)Peak memory usage: 15 MB % 165.62/23.69 % (3011448)Instructions burned: 263 (million) % 165.62/23.69 % (3011450)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=592150338:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2817 on theBenchmark for (2817ds/318Mi) % 165.62/23.69 % (3011450)Instruction limit reached! % 165.62/23.69 % (3011450)------------------------------ % 165.62/23.69 % (3011450)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 165.62/23.69 % (3011450)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 165.62/23.69 % (3011450)CaDiCaL version: 2.1.3 % 165.62/23.69 % (3011450)Termination reason: Instruction limit % 165.62/23.69 % (3011450)Termination phase: Saturation % 165.62/23.69 % (3011450)Time elapsed: 0.130 s % 165.62/23.69 % (3011450)Peak memory usage: 12 MB % 165.62/23.69 % (3011450)Instructions burned: 320 (million) % 165.62/23.69 % (3011452)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=256554732:i=1428:nm=2:rtra=on_2816 on theBenchmark for (2816ds/1428Mi) % 165.62/23.69 % Detected minimum model sizes of [3] % 165.62/23.69 % Detected maximum model sizes of [max] % 165.62/23.69 % (3011452)Cannot represent all propositional literals internally % 165.62/23.69 % (3011452)Refutation not found, incomplete strategy % 165.62/23.69 % (3011452)------------------------------ % 165.62/23.69 % (3011452)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 165.62/23.69 % (3011452)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 165.62/23.69 % (3011452)CaDiCaL version: 2.1.3 % 165.62/23.69 % (3011452)Termination reason: Refutation not found, incomplete strategy % 165.62/23.69 % (3011452)Time elapsed: 0.092 s % 165.62/23.69 % (3011452)Peak memory usage: 12 MB % 165.62/23.69 % (3011452)Instructions burned: 185 (million) % 165.62/23.69 % (3011452)------------------------------ % 165.62/23.69 % (3011452)------------------------------ % 165.62/23.69 % (3011454)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=1129840271:i=262:bd=preordered:rtra=on:fsd=on_2815 on theBenchmark for (2815ds/262Mi) % 165.62/23.69 % (3011454)Instruction limit reached! % 165.62/23.69 % (3011454)------------------------------ % 165.62/23.69 % (3011454)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 165.62/23.69 % (3011454)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 165.62/23.69 % (3011454)CaDiCaL version: 2.1.3 % 165.62/23.69 % (3011454)Termination reason: Instruction limit % 165.62/23.69 % (3011454)Termination phase: Saturation % 165.62/23.69 % (3011454)Time elapsed: 0.160 s % 165.62/23.69 % (3011454)Peak memory usage: 16 MB % 165.62/23.69 % (3011454)Instructions burned: 262 (million) % 165.62/23.69 % (3011456)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=286749896:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2813 on theBenchmark for (2813ds/1368Mi) % 165.62/23.69 % (3011456)Instruction limit reached! % 165.62/23.69 % (3011456)------------------------------ % 165.62/23.69 % (3011456)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 165.62/23.69 % (3011456)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 165.62/23.69 % (3011456)CaDiCaL version: 2.1.3 % 165.62/23.69 % (3011456)Termination reason: Instruction limit % 165.62/23.69 % (3011456)Termination phase: Saturation % 165.62/23.69 % (3011456)Time elapsed: 0.582 s % 165.62/23.69 % (3011456)Peak memory usage: 21 MB % 165.62/23.69 % (3011456)Instructions burned: 1370 (million) % 165.62/23.69 % (3011458)ott-21_1_sil=16000:si=on:fs=off:random_seed=2181096644:i=360:av=off:fsr=off:rtra=on_2807 on theBenchmark for (2807ds/360Mi) % 165.62/23.69 % (3011458)Instruction limit reached! % 165.62/23.69 % (3011458)------------------------------ % 165.62/23.69 % (3011458)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 165.62/23.69 % (3011458)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 186.21/26.53 % (3011458)CaDiCaL version: 2.1.3 % 186.21/26.53 % (3011458)Termination reason: Instruction limit % 186.21/26.53 % (3011458)Termination phase: Saturation % 186.21/26.53 % (3011458)Time elapsed: 0.198 s % 186.21/26.53 % (3011458)Peak memory usage: 15 MB % 186.21/26.53 % (3011458)Instructions burned: 361 (million) % 186.21/26.53 % (3011460)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2972105955:i=954:bd=all:rtra=on_2805 on theBenchmark for (2805ds/954Mi) % 186.21/26.53 % (3011460)Instruction limit reached! % 186.21/26.53 % (3011460)------------------------------ % 186.21/26.53 % (3011460)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 186.21/26.53 % (3011460)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 186.21/26.53 % (3011460)CaDiCaL version: 2.1.3 % 186.21/26.53 % (3011460)Termination reason: Instruction limit % 186.21/26.53 % (3011460)Termination phase: Saturation % 186.21/26.53 % (3011460)Time elapsed: 0.530 s % 186.21/26.53 % (3011460)Peak memory usage: 18 MB % 186.21/26.53 % (3011460)Instructions burned: 955 (million) % 186.21/26.53 % (3011462)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=102463799:fmbsr=1.3:i=1730:ins=25:rtra=on_2799 on theBenchmark for (2799ds/1730Mi) % 186.21/26.53 % Detected minimum model sizes of [3] % 186.21/26.53 % Detected maximum model sizes of [max] % 186.21/26.53 % (3011462)Cannot represent all propositional literals internally % 186.21/26.53 % (3011462)Refutation not found, incomplete strategy % 186.21/26.53 % (3011462)------------------------------ % 186.21/26.53 % (3011462)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 186.21/26.53 % (3011462)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 186.21/26.53 % (3011462)CaDiCaL version: 2.1.3 % 186.21/26.53 % (3011462)Termination reason: Refutation not found, incomplete strategy % 186.21/26.53 % (3011462)Time elapsed: 0.080 s % 186.21/26.53 % (3011462)Peak memory usage: 12 MB % 186.21/26.53 % (3011462)Instructions burned: 152 (million) % 186.21/26.53 % (3011462)------------------------------ % 186.21/26.53 % (3011462)------------------------------ % 186.21/26.53 % (3011464)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=4098853775:i=2358:rtra=on_2798 on theBenchmark for (2798ds/2358Mi) % 186.21/26.53 % (3011464)Instruction limit reached! % 186.21/26.53 % (3011464)------------------------------ % 186.21/26.53 % (3011464)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 186.21/26.53 % (3011464)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 186.21/26.53 % (3011464)CaDiCaL version: 2.1.3 % 186.21/26.53 % (3011464)Termination reason: Instruction limit % 186.21/26.53 % (3011464)Termination phase: Saturation % 186.21/26.53 % (3011464)Time elapsed: 1.428 s % 186.21/26.53 % (3011464)Peak memory usage: 44 MB % 186.21/26.53 % (3011464)Instructions burned: 2360 (million) % 186.21/26.53 % (3011466)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=8695645:i=1778:ins=1:rtra=on_2784 on theBenchmark for (2784ds/1778Mi) % 186.21/26.53 % (3011466)Cannot represent all propositional literals internally % 186.21/26.53 % (3011466)Refutation not found, incomplete strategy % 186.21/26.53 % (3011466)------------------------------ % 186.21/26.53 % (3011466)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 186.21/26.53 % (3011466)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 186.21/26.53 % (3011466)CaDiCaL version: 2.1.3 % 186.21/26.53 % (3011466)Termination reason: Refutation not found, incomplete strategy % 186.21/26.53 % (3011466)Time elapsed: 0.082 s % 186.21/26.53 % (3011466)Peak memory usage: 13 MB % 186.21/26.53 % (3011466)Instructions burned: 157 (million) % 186.21/26.53 % (3011466)------------------------------ % 186.21/26.53 % (3011466)------------------------------ % 186.21/26.53 % (3011468)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=3375873765:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2783 on theBenchmark for (2783ds/1384Mi) % 186.21/26.53 % (3011468)Instruction limit reached! % 186.21/26.53 % (3011468)------------------------------ % 186.21/26.53 % (3011468)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 186.21/26.53 % (3011468)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 186.21/26.53 % (3011468)CaDiCaL version: 2.1.3 % 186.21/26.53 % (3011468)Termination reason: Instruction limit % 186.21/26.53 % (3011468)Termination phase: Saturation % 186.21/26.53 % (3011468)Time elapsed: 0.764 s % 186.21/26.53 % (3011468)Peak memory usage: 26 MB % 231.07/33.03 % (3011468)Instructions burned: 1384 (million) % 231.07/33.03 % (3011470)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=648270499:i=1758:kws=inv_precedence:fsr=off:rtra=on_2775 on theBenchmark for (2775ds/1758Mi) % 231.07/33.03 % (3011426)Instruction limit reached! % 231.07/33.03 % (3011426)------------------------------ % 231.07/33.03 % (3011426)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 231.07/33.03 % (3011426)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 231.07/33.03 % (3011426)CaDiCaL version: 2.1.3 % 231.07/33.03 % (3011426)Termination reason: Instruction limit % 231.07/33.03 % (3011426)Termination phase: Saturation % 231.07/33.03 % (3011426)Time elapsed: 8.820 s % 231.07/33.03 % (3011426)Peak memory usage: 312 MB % 231.07/33.03 % (3011426)Instructions burned: 28125 (million) % 231.07/33.03 % (3011472)fmb+10_1_sil=64000:si=on:random_seed=2972441740:i=44122:nm=2:rtra=on:gsp=on_2770 on theBenchmark for (2770ds/44122Mi) % 231.07/33.03 % Detected minimum model sizes of [3] % 231.07/33.03 % Detected maximum model sizes of [max] % 231.07/33.03 % (3011472)Cannot represent all propositional literals internally % 231.07/33.03 % (3011472)Refutation not found, incomplete strategy % 231.07/33.03 % (3011472)------------------------------ % 231.07/33.03 % (3011472)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 231.07/33.03 % (3011472)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 231.07/33.03 % (3011472)CaDiCaL version: 2.1.3 % 231.07/33.03 % (3011472)Termination reason: Refutation not found, incomplete strategy % 231.07/33.03 % (3011472)Time elapsed: 0.043 s % 231.07/33.03 % (3011472)Peak memory usage: 12 MB % 231.07/33.03 % (3011472)Instructions burned: 153 (million) % 231.07/33.03 % (3011472)------------------------------ % 231.07/33.03 % (3011472)------------------------------ % 231.07/33.03 % (3011474)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=788311095:i=19030:nm=5:rtra=on_2769 on theBenchmark for (2769ds/19030Mi) % 231.07/33.03 % Detected minimum model sizes of [3] % 231.07/33.03 % Detected maximum model sizes of [max] % 231.07/33.03 % (3011474)Cannot represent all propositional literals internally % 231.07/33.03 % (3011474)Refutation not found, incomplete strategy % 231.07/33.03 % (3011474)------------------------------ % 231.07/33.03 % (3011474)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 231.07/33.03 % (3011474)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 231.07/33.03 % (3011474)CaDiCaL version: 2.1.3 % 231.07/33.03 % (3011474)Termination reason: Refutation not found, incomplete strategy % 231.07/33.03 % (3011474)Time elapsed: 0.042 s % 231.07/33.03 % (3011474)Peak memory usage: 12 MB % 231.07/33.03 % (3011474)Instructions burned: 152 (million) % 231.07/33.03 % (3011474)------------------------------ % 231.07/33.03 % (3011474)------------------------------ % 231.07/33.03 % (3011476)fmb+10_1_sil=64000:sas=cadical:si=on:fmbss=8:random_seed=3313728785:fmbsr=1.7:i=1840:rtra=on_2769 on theBenchmark for (2769ds/1840Mi) % 231.07/33.03 % Detected minimum model sizes of [3] % 231.07/33.03 % Detected maximum model sizes of [max] % 231.07/33.03 % (3011476)Cannot represent all propositional literals internally % 231.07/33.03 % (3011476)Refutation not found, incomplete strategy % 231.07/33.03 % (3011476)------------------------------ % 231.07/33.03 % (3011476)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 231.07/33.03 % (3011476)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 231.07/33.03 % (3011476)CaDiCaL version: 2.1.3 % 231.07/33.03 % (3011476)Termination reason: Refutation not found, incomplete strategy % 231.07/33.03 % (3011476)Time elapsed: 0.043 s % 231.07/33.03 % (3011476)Peak memory usage: 12 MB % 231.07/33.03 % (3011476)Instructions burned: 152 (million) % 231.07/33.03 % (3011476)------------------------------ % 231.07/33.03 % (3011476)------------------------------ % 231.07/33.03 % (3011478)dis-4_1_sil=16000:drc=ordering:si=on:sp=const_frequency:sac=on:newcnf=on:random_seed=646425796:i=10262:rtra=on_2768 on theBenchmark for (2768ds/10262Mi) % 231.07/33.03 % (3011470)Instruction limit reached! % 231.07/33.03 % (3011470)------------------------------ % 231.07/33.03 % (3011470)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 231.07/33.03 % (3011470)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 231.07/33.03 % (3011470)CaDiCaL version: 2.1.3 % 231.07/33.03 % (3011470)Termination reason: Instruction limit % 231.07/33.03 % (3011470)Termination phase: Saturation % 231.07/33.03 % (3011470)Time elapsed: 0.972 s % 231.07/33.03 % (3011470)Peak memory usage: 26 MB % 231.07/33.03 % (3011470)Instructions burned: 1759 (million) % 248.17/35.26 % (3011480)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:si=on:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2441265881:i=2944:ins=7:rtra=on:fdi=8:gsp=on_2765 on theBenchmark for (2765ds/2944Mi) % 248.17/35.26 % (3011480)Instruction limit reached! % 248.17/35.26 % (3011480)------------------------------ % 248.17/35.26 % (3011480)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 248.17/35.26 % (3011480)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 248.17/35.26 % (3011480)CaDiCaL version: 2.1.3 % 248.17/35.26 % (3011480)Termination reason: Instruction limit % 248.17/35.26 % (3011480)Termination phase: Saturation % 248.17/35.26 % (3011480)Time elapsed: 1.381 s % 248.17/35.26 % (3011480)Peak memory usage: 32 MB % 248.17/35.26 % (3011480)Instructions burned: 2946 (million) % 248.17/35.26 % (3011482)fmb+10_1_sil=16000:sas=cadical:si=on:bce=on:fmbss=77:random_seed=1790020432:i=12648:rtra=on_2751 on theBenchmark for (2751ds/12648Mi) % 248.17/35.26 % Detected minimum model sizes of [3] % 248.17/35.26 % Detected maximum model sizes of [max] % 248.17/35.26 % (3011482)Cannot represent all propositional literals internally % 248.17/35.26 % (3011482)Refutation not found, incomplete strategy % 248.17/35.26 % (3011482)------------------------------ % 248.17/35.26 % (3011482)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 248.17/35.26 % (3011482)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 248.17/35.26 % (3011482)CaDiCaL version: 2.1.3 % 248.17/35.26 % (3011482)Termination reason: Refutation not found, incomplete strategy % 248.17/35.26 % (3011482)Time elapsed: 0.083 s % 248.17/35.26 % (3011482)Peak memory usage: 13 MB % 248.17/35.26 % (3011482)Instructions burned: 156 (million) % 248.17/35.26 % (3011482)------------------------------ % 248.17/35.26 % (3011482)------------------------------ % 248.17/35.26 % (3011484)fmb+10_1_fmbas=function:sil=32000:sas=cadical:si=on:fmbss=16:random_seed=2812018014:fmbsr=2.30978:i=4348:rtra=on_2750 on theBenchmark for (2750ds/4348Mi) % 248.17/35.26 % Detected minimum model sizes of [3] % 248.17/35.26 % Detected maximum model sizes of [max] % 248.17/35.26 % (3011484)Cannot represent all propositional literals internally % 248.17/35.26 % (3011484)Refutation not found, incomplete strategy % 248.17/35.26 % (3011484)------------------------------ % 248.17/35.26 % (3011484)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 248.17/35.26 % (3011484)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 248.17/35.26 % (3011484)CaDiCaL version: 2.1.3 % 248.17/35.26 % (3011484)Termination reason: Refutation not found, incomplete strategy % 248.17/35.26 % (3011484)Time elapsed: 0.600 s % 248.17/35.26 % (3011484)Peak memory usage: 20 MB % 248.17/35.26 % (3011484)Instructions burned: 1114 (million) % 248.17/35.26 % (3011484)------------------------------ % 248.17/35.26 % (3011484)------------------------------ % 248.17/35.26 % (3011486)ott-2_1_sil=16000:si=on:newcnf=on:random_seed=1229848991:avsq=on:i=1738:avsqr=1,16:kws=inv_arity_squared:rtra=on_2743 on theBenchmark for (2743ds/1738Mi) % 248.17/35.26 % (3011478)Instruction limit reached! % 248.17/35.26 % (3011478)------------------------------ % 248.17/35.26 % (3011478)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 248.17/35.26 % (3011478)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 248.17/35.26 % (3011478)CaDiCaL version: 2.1.3 % 248.17/35.26 % (3011478)Termination reason: Instruction limit % 248.17/35.26 % (3011478)Termination phase: Saturation % 248.17/35.26 % (3011478)Time elapsed: 2.937 s % 248.17/35.26 % (3011478)Peak memory usage: 88 MB % 248.17/35.26 % (3011478)Instructions burned: 10262 (million) % 248.17/35.26 % (3011488)ott+10_1_sil=32000:tgt=ground:si=on:random_seed=2543430243:i=10228:av=off:rtra=on_2739 on theBenchmark for (2739ds/10228Mi) % 248.17/35.26 % (3011486)Instruction limit reached! % 248.17/35.26 % (3011486)------------------------------ % 248.17/35.26 % (3011486)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 248.17/35.26 % (3011486)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 248.17/35.26 % (3011486)CaDiCaL version: 2.1.3 % 248.17/35.26 % (3011486)Termination reason: Instruction limit % 248.17/35.26 % (3011486)Termination phase: Saturation % 248.17/35.26 % (3011486)Time elapsed: 0.584 s % 248.17/35.26 % (3011486)Peak memory usage: 12 MB % 248.17/35.26 % (3011486)Instructions burned: 1739 (million) % 248.17/35.26 % (3011490)fmb+10_1_sil=64000:sas=cadical:si=on:bce=on:rp=on:random_seed=471382529:i=108564:rtra=on_2737 on theBenchmark for (2737ds/108564Mi) % 248.17/35.26 % Detected minimum model sizes of [3] % 248.17/35.26 % Detected maximum model sizes of [max] % 248.17/35.26 % (3011490)Cannot represent all propositional literals internally % 300.41/42.63 % (3011490)Refutation not found, incomplete strategy % 300.41/42.63 % (3011490)------------------------------ % 300.41/42.63 % (3011490)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.41/42.63 % (3011490)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.41/42.63 % (3011490)CaDiCaL version: 2.1.3 % 300.41/42.63 % (3011490)Termination reason: Refutation not found, incomplete strategy % 300.41/42.63 % (3011490)Time elapsed: 0.082 s % 300.41/42.63 % (3011490)Peak memory usage: 13 MB % 300.41/42.63 % (3011490)Instructions burned: 156 (million) % 300.41/42.63 % (3011490)------------------------------ % 300.41/42.63 % (3011490)------------------------------ % 300.41/42.63 % (3011492)dis-11_1_sil=16000:si=on:sp=reverse_frequency:alpa=true:random_seed=3929443016:i=7024:aac=none:rtra=on_2736 on theBenchmark for (2736ds/7024Mi) % 300.41/42.63 % (3011488)Instruction limit reached! % 300.41/42.63 % (3011488)------------------------------ % 300.41/42.63 % (3011488)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.41/42.63 % (3011488)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.41/42.63 % (3011488)CaDiCaL version: 2.1.3 % 300.41/42.63 % (3011488)Termination reason: Instruction limit % 300.41/42.63 % (3011488)Termination phase: Saturation % 300.41/42.63 % (3011488)Time elapsed: 3.488 s % 300.41/42.63 % (3011488)Peak memory usage: 169 MB % 300.41/42.63 % (3011488)Instructions burned: 10231 (million) % 300.41/42.63 % (3011494)dis+21_1_sil=32000:sas=cadical:si=on:random_seed=1347689323:i=7546:rtra=on:amm=off_2704 on theBenchmark for (2704ds/7546Mi) % 300.41/42.63 % (3011492)Instruction limit reached! % 300.41/42.63 % (3011492)------------------------------ % 300.41/42.63 % (3011492)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.41/42.63 % (3011492)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.41/42.63 % (3011492)CaDiCaL version: 2.1.3 % 300.41/42.63 % (3011492)Termination reason: Instruction limit % 300.41/42.63 % (3011492)Termination phase: Saturation % 300.41/42.63 % (3011492)Time elapsed: 3.812 s % 300.41/42.63 % (3011492)Peak memory usage: 64 MB % 300.41/42.63 % (3011492)Instructions burned: 7024 (million) % 300.41/42.63 % (3011496)ott+11_1_sil=16000:si=on:gs=on:random_seed=2905028618:s2a=on:i=4502:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:rtra=on:fsd=on_2698 on theBenchmark for (2698ds/4502Mi) % 300.41/42.63 % (3011494)Instruction limit reached! % 300.41/42.63 % (3011494)------------------------------ % 300.41/42.63 % (3011494)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.41/42.63 % (3011494)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.41/42.63 % (3011494)CaDiCaL version: 2.1.3 % 300.41/42.63 % (3011494)Termination reason: Instruction limit % 300.41/42.63 % (3011494)Termination phase: Saturation % 300.41/42.63 % (3011494)Time elapsed: 2.205 s % 300.41/42.63 % (3011494)Peak memory usage: 68 MB % 300.41/42.63 % (3011494)Instructions burned: 7548 (million) % 300.41/42.63 % (3011498)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:si=on:fmbss=7:random_seed=2548768887:fmbsr=1.6:i=135068:rtra=on_2681 on theBenchmark for (2681ds/135068Mi) % 300.41/42.63 % Detected minimum model sizes of [3] % 300.41/42.63 % Detected maximum model sizes of [max] % 300.41/42.63 % (3011498)Cannot represent all propositional literals internally % 300.41/42.63 % (3011498)Refutation not found, incomplete strategy % 300.41/42.63 % (3011498)------------------------------ % 300.41/42.63 % (3011498)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.41/42.63 % (3011498)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.41/42.63 % (3011498)CaDiCaL version: 2.1.3 % 300.41/42.63 % (3011498)Termination reason: Refutation not found, incomplete strategy % 300.41/42.63 % (3011498)Time elapsed: 0.051 s % 300.41/42.63 % (3011498)Peak memory usage: 13 MB % 300.41/42.63 % (3011498)Instructions burned: 194 (million) % 300.41/42.63 % (3011498)------------------------------ % 300.41/42.63 % (3011498)------------------------------ % 300.41/42.63 % (3011500)ott-22_32_sil=16000:tgt=full:si=on:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=3164686973:avsq=on:i=9182:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:rtra=on:fdi=4_2681 on theBenchmark for (2681ds/9182Mi) % 300.41/42.63 % (3011496)Instruction limit reached! % 300.41/42.63 % (3011496)------------------------------ % 300.41/42.63 % (3011496)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.41/42.63 % (3011496)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.41/42.63 Terminated % 300.41/42.63 % Vampire exiting % 300.41/42.63 Terminated %------------------------------------------------------------------------------