%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWV944-1 : TPTP v9.3.1. Released v4.1.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % Computer : n015.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 29 01:26:42 PM UTC 2026 % Result : Timeout 300.64s 42.64s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWV944-1 : TPTP v9.3.1. Released v4.1.0. % 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.09/0.20 % Computer : n015.cluster.edu % 0.09/0.20 % Model : x86_64 x86_64 % 0.09/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.20 % Memory : 8046.5625MB % 0.09/0.20 % OS : Linux 6.8.0-71-generic % 0.09/0.20 % CPULimit : 300 % 0.09/0.20 % WCLimit : 300 % 0.09/0.20 % DateTime : Mon Sep 28 13:01:47 UTC 2026 % 0.09/0.20 % CPUTime : % 0.09/0.20 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.09/0.22 Running first-order model finding % 0.09/0.22 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 3.38/0.88 % (2612375)Will run a generic schedule for satisfiability detection. % 3.38/0.88 % (2612382)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2208185434:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 3.38/0.88 % (2612381)% WARNING: option uhcvi not known. % 3.38/0.88 % (2612381)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=875494715:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 3.38/0.88 % (2612380)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2175538533_2999 on theBenchmark for (2999ds/0Mi) % 3.38/0.88 % (2612383)dis+10_1_sil=32000:sp=arity:random_seed=1526856738:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 3.38/0.88 % (2612384)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2014998918:i=116_2999 on theBenchmark for (2999ds/116Mi) % 3.38/0.88 % (2612385)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1993594503:i=131_2999 on theBenchmark for (2999ds/131Mi) % 3.38/0.88 % (2612386)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1903790789:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 3.38/0.88 % (2612383)Instruction limit reached! % 3.38/0.88 % (2612383)------------------------------ % 3.38/0.88 % (2612383)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.38/0.88 % (2612383)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.38/0.88 % (2612383)CaDiCaL version: 2.1.3 % 3.38/0.88 % (2612383)Termination reason: Instruction limit % 3.38/0.88 % (2612383)Termination phase: Saturation % 3.38/0.88 % (2612383)Time elapsed: 0.054 s % 3.38/0.88 % (2612383)Peak memory usage: 12 MB % 3.38/0.88 % (2612383)Instructions burned: 103 (million) % 3.38/0.88 % (2612384)Instruction limit reached! % 3.38/0.88 % (2612384)------------------------------ % 3.38/0.88 % (2612384)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.38/0.88 % (2612384)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.38/0.88 % (2612384)CaDiCaL version: 2.1.3 % 3.38/0.88 % (2612384)Termination reason: Instruction limit % 3.38/0.88 % (2612384)Termination phase: Saturation % 3.38/0.88 % (2612384)Time elapsed: 0.058 s % 3.38/0.88 % (2612384)Peak memory usage: 13 MB % 3.38/0.88 % (2612384)Instructions burned: 118 (million) % 3.38/0.88 % (2612385)Instruction limit reached! % 3.38/0.88 % (2612385)------------------------------ % 3.38/0.88 % (2612385)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.38/0.88 % (2612385)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.38/0.88 % (2612385)CaDiCaL version: 2.1.3 % 3.38/0.88 % (2612385)Termination reason: Instruction limit % 3.38/0.88 % (2612385)Termination phase: Saturation % 3.38/0.88 % (2612385)Time elapsed: 0.073 s % 3.38/0.88 % (2612385)Peak memory usage: 13 MB % 3.38/0.88 % (2612385)Instructions burned: 132 (million) % 3.38/0.88 % (2612394)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2136388755:i=714:nm=2_2998 on theBenchmark for (2998ds/714Mi) % 3.38/0.88 % (2612395)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3802783966:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi) % 3.38/0.88 % Detected minimum model sizes of [4] % 3.38/0.88 % Detected maximum model sizes of [max] % 3.38/0.88 % (2612380)Cannot represent all propositional literals internally % 3.38/0.88 % (2612380)Refutation not found, incomplete strategy % 3.38/0.88 % (2612380)------------------------------ % 3.38/0.88 % (2612380)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.38/0.88 % (2612380)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.38/0.88 % (2612380)CaDiCaL version: 2.1.3 % 3.38/0.88 % (2612380)Termination reason: Refutation not found, incomplete strategy % 3.38/0.88 % (2612380)Time elapsed: 0.092 s % 3.38/0.88 % (2612380)Peak memory usage: 13 MB % 3.38/0.88 % (2612380)Instructions burned: 186 (million) % 3.38/0.88 % (2612396)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=3712990633:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi) % 3.38/0.88 % (2612380)------------------------------ % 3.38/0.88 % (2612380)------------------------------ % 3.38/0.88 % (2612386)Instruction limit reached! % 3.38/0.88 % (2612386)------------------------------ % 3.38/0.88 % (2612386)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.38/0.88 % (2612386)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.60/1.54 % (2612386)CaDiCaL version: 2.1.3 % 7.60/1.54 % (2612386)Termination reason: Instruction limit % 7.60/1.54 % (2612386)Termination phase: Saturation % 7.60/1.54 % (2612386)Time elapsed: 0.096 s % 7.60/1.54 % (2612386)Peak memory usage: 13 MB % 7.60/1.54 % (2612386)Instructions burned: 160 (million) % 7.60/1.54 % (2612400)ott-21_1_sil=16000:fs=off:random_seed=3877526809:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 7.60/1.54 % (2612401)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2976917467:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 7.60/1.54 % (2612395)Instruction limit reached! % 7.60/1.54 % (2612395)------------------------------ % 7.60/1.54 % (2612395)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.60/1.54 % (2612395)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.60/1.54 % (2612395)CaDiCaL version: 2.1.3 % 7.60/1.54 % (2612395)Termination reason: Instruction limit % 7.60/1.54 % (2612395)Termination phase: Saturation % 7.60/1.54 % (2612395)Time elapsed: 0.069 s % 7.60/1.54 % (2612395)Peak memory usage: 13 MB % 7.60/1.54 % (2612395)Instructions burned: 133 (million) % 7.60/1.54 % (2612404)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=600049559:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi) % 7.60/1.54 % Detected minimum model sizes of [4] % 7.60/1.54 % Detected maximum model sizes of [max] % 7.60/1.54 % (2612394)Cannot represent all propositional literals internally % 7.60/1.54 % (2612394)Refutation not found, incomplete strategy % 7.60/1.54 % (2612394)------------------------------ % 7.60/1.54 % (2612394)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.60/1.54 % (2612394)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.60/1.54 % (2612394)CaDiCaL version: 2.1.3 % 7.60/1.54 % (2612394)Termination reason: Refutation not found, incomplete strategy % 7.60/1.54 % (2612394)Time elapsed: 0.100 s % 7.60/1.54 % (2612394)Peak memory usage: 13 MB % 7.60/1.54 % (2612394)Instructions burned: 214 (million) % 7.60/1.54 % (2612394)------------------------------ % 7.60/1.54 % (2612394)------------------------------ % 7.60/1.54 % (2612406)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3231337508:i=1179_2997 on theBenchmark for (2997ds/1179Mi) % 7.60/1.54 % (2612400)Instruction limit reached! % 7.60/1.54 % (2612400)------------------------------ % 7.60/1.54 % (2612400)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.60/1.54 % (2612400)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.60/1.54 % (2612400)CaDiCaL version: 2.1.3 % 7.60/1.54 % (2612400)Termination reason: Instruction limit % 7.60/1.54 % (2612400)Termination phase: Saturation % 7.60/1.54 % (2612400)Time elapsed: 0.089 s % 7.60/1.54 % (2612400)Peak memory usage: 12 MB % 7.60/1.54 % (2612400)Instructions burned: 181 (million) % 7.60/1.54 % (2612408)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2098385586:i=889:ins=1_2997 on theBenchmark for (2997ds/889Mi) % 7.60/1.54 % Detected minimum model sizes of [4] % 7.60/1.54 % Detected maximum model sizes of [max] % 7.60/1.54 % (2612404)Cannot represent all propositional literals internally % 7.60/1.54 % (2612404)Refutation not found, incomplete strategy % 7.60/1.54 % (2612404)------------------------------ % 7.60/1.54 % (2612404)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.60/1.54 % (2612404)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.60/1.54 % (2612404)CaDiCaL version: 2.1.3 % 7.60/1.54 % (2612404)Termination reason: Refutation not found, incomplete strategy % 7.60/1.54 % (2612404)Time elapsed: 0.087 s % 7.60/1.54 % (2612404)Peak memory usage: 13 MB % 7.60/1.54 % (2612404)Instructions burned: 174 (million) % 7.60/1.54 % (2612404)------------------------------ % 7.60/1.54 % (2612404)------------------------------ % 7.60/1.54 % (2612410)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=2088009552:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2996 on theBenchmark for (2996ds/692Mi) % 7.60/1.54 % (2612408)Cannot represent all propositional literals internally % 7.60/1.54 % (2612408)Refutation not found, incomplete strategy % 7.60/1.54 % (2612408)------------------------------ % 7.60/1.54 % (2612408)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.60/1.54 % (2612408)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.56/2.99 % (2612408)CaDiCaL version: 2.1.3 % 18.56/2.99 % (2612408)Termination reason: Refutation not found, incomplete strategy % 18.56/2.99 % (2612408)Time elapsed: 0.091 s % 18.56/2.99 % (2612408)Peak memory usage: 13 MB % 18.56/2.99 % (2612408)Instructions burned: 181 (million) % 18.56/2.99 % (2612408)------------------------------ % 18.56/2.99 % (2612408)------------------------------ % 18.56/2.99 % (2612412)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2848022110:i=879:kws=inv_precedence:fsr=off_2996 on theBenchmark for (2996ds/879Mi) % 18.56/2.99 % (2612401)Instruction limit reached! % 18.56/2.99 % (2612401)------------------------------ % 18.56/2.99 % (2612401)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 18.56/2.99 % (2612401)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.56/2.99 % (2612401)CaDiCaL version: 2.1.3 % 18.56/2.99 % (2612401)Termination reason: Instruction limit % 18.56/2.99 % (2612401)Termination phase: Saturation % 18.56/2.99 % (2612401)Time elapsed: 0.264 s % 18.56/2.99 % (2612401)Peak memory usage: 15 MB % 18.56/2.99 % (2612401)Instructions burned: 479 (million) % 18.56/2.99 % (2612414)fmb+10_1_sil=64000:random_seed=352463368:i=22061:nm=2:gsp=on_2995 on theBenchmark for (2995ds/22061Mi) % 18.56/2.99 % (2612396)Instruction limit reached! % 18.56/2.99 % (2612396)------------------------------ % 18.56/2.99 % (2612396)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 18.56/2.99 % (2612396)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.56/2.99 % (2612396)CaDiCaL version: 2.1.3 % 18.56/2.99 % (2612396)Termination reason: Instruction limit % 18.56/2.99 % (2612396)Termination phase: Saturation % 18.56/2.99 % (2612396)Time elapsed: 0.314 s % 18.56/2.99 % (2612396)Peak memory usage: 18 MB % 18.56/2.99 % (2612396)Instructions burned: 684 (million) % 18.56/2.99 % (2612416)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=488704177:i=9515:nm=5_2995 on theBenchmark for (2995ds/9515Mi) % 18.56/2.99 % Detected minimum model sizes of [4] % 18.56/2.99 % Detected maximum model sizes of [max] % 18.56/2.99 % (2612414)Cannot represent all propositional literals internally % 18.56/2.99 % (2612414)Refutation not found, incomplete strategy % 18.56/2.99 % (2612414)------------------------------ % 18.56/2.99 % (2612414)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 18.56/2.99 % (2612414)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.56/2.99 % (2612414)CaDiCaL version: 2.1.3 % 18.56/2.99 % (2612414)Termination reason: Refutation not found, incomplete strategy % 18.56/2.99 % (2612414)Time elapsed: 0.090 s % 18.56/2.99 % (2612414)Peak memory usage: 13 MB % 18.56/2.99 % (2612414)Instructions burned: 182 (million) % 18.56/2.99 % (2612414)------------------------------ % 18.56/2.99 % (2612414)------------------------------ % 18.56/2.99 % (2612418)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1059637435:fmbsr=1.7:i=920_2994 on theBenchmark for (2994ds/920Mi) % 18.56/2.99 % Detected minimum model sizes of [4] % 18.56/2.99 % Detected maximum model sizes of [max] % 18.56/2.99 % (2612416)Cannot represent all propositional literals internally % 18.56/2.99 % (2612416)Refutation not found, incomplete strategy % 18.56/2.99 % (2612416)------------------------------ % 18.56/2.99 % (2612416)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 18.56/2.99 % (2612416)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.56/2.99 % (2612416)CaDiCaL version: 2.1.3 % 18.56/2.99 % (2612416)Termination reason: Refutation not found, incomplete strategy % 18.56/2.99 % (2612416)Time elapsed: 0.088 s % 18.56/2.99 % (2612416)Peak memory usage: 13 MB % 18.56/2.99 % (2612416)Instructions burned: 174 (million) % 18.56/2.99 % (2612416)------------------------------ % 18.56/2.99 % (2612416)------------------------------ % 18.56/2.99 % (2612420)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=3616193874:i=5131_2994 on theBenchmark for (2994ds/5131Mi) % 18.56/2.99 % Detected minimum model sizes of [4] % 18.56/2.99 % Detected maximum model sizes of [max] % 18.56/2.99 % (2612418)Cannot represent all propositional literals internally % 18.56/2.99 % (2612418)Refutation not found, incomplete strategy % 18.56/2.99 % (2612418)------------------------------ % 18.56/2.99 % (2612418)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 18.56/2.99 % (2612418)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.56/2.99 % (2612418)CaDiCaL version: 2.1.3 % 18.56/2.99 % (2612418)Termination reason: Refutation not found, incomplete strategy % 22.60/3.55 % (2612418)Time elapsed: 0.087 s % 22.60/3.55 % (2612418)Peak memory usage: 13 MB % 22.60/3.55 % (2612418)Instructions burned: 174 (million) % 22.60/3.55 % (2612418)------------------------------ % 22.60/3.55 % (2612418)------------------------------ % 22.60/3.55 % (2612422)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=760694315:i=1472:ins=7:fdi=8:gsp=on_2993 on theBenchmark for (2993ds/1472Mi) % 22.60/3.55 % (2612410)Instruction limit reached! % 22.60/3.55 % (2612410)------------------------------ % 22.60/3.55 % (2612410)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.60/3.55 % (2612410)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.60/3.55 % (2612410)CaDiCaL version: 2.1.3 % 22.60/3.55 % (2612410)Termination reason: Instruction limit % 22.60/3.55 % (2612410)Termination phase: Saturation % 22.60/3.55 % (2612410)Time elapsed: 0.414 s % 22.60/3.55 % (2612410)Peak memory usage: 20 MB % 22.60/3.55 % (2612410)Instructions burned: 693 (million) % 22.60/3.55 % (2612424)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3500991449:i=6324_2992 on theBenchmark for (2992ds/6324Mi) % 22.60/3.55 % (2612406)Instruction limit reached! % 22.60/3.55 % (2612406)------------------------------ % 22.60/3.55 % (2612406)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.60/3.55 % (2612406)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.60/3.55 % (2612406)CaDiCaL version: 2.1.3 % 22.60/3.55 % (2612406)Termination reason: Instruction limit % 22.60/3.55 % (2612406)Termination phase: Saturation % 22.60/3.55 % (2612406)Time elapsed: 0.564 s % 22.60/3.55 % (2612406)Peak memory usage: 16 MB % 22.60/3.55 % (2612406)Instructions burned: 1179 (million) % 22.60/3.55 % (2612412)Instruction limit reached! % 22.60/3.55 % (2612412)------------------------------ % 22.60/3.55 % (2612412)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.60/3.55 % (2612412)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.60/3.55 % (2612412)CaDiCaL version: 2.1.3 % 22.60/3.55 % (2612412)Termination reason: Instruction limit % 22.60/3.55 % (2612412)Termination phase: Saturation % 22.60/3.55 % (2612412)Time elapsed: 0.441 s % 22.60/3.55 % (2612412)Peak memory usage: 18 MB % 22.60/3.55 % (2612412)Instructions burned: 879 (million) % 22.60/3.55 % (2612426)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=3986678233:fmbsr=2.30978:i=2174_2991 on theBenchmark for (2991ds/2174Mi) % 22.60/3.55 % (2612427)ott-2_1_sil=16000:newcnf=on:random_seed=2077544414:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2991 on theBenchmark for (2991ds/869Mi) % 22.60/3.55 % Detected minimum model sizes of [4] % 22.60/3.55 % Detected maximum model sizes of [max] % 22.60/3.55 % (2612424)Cannot represent all propositional literals internally % 22.60/3.55 % (2612424)Refutation not found, incomplete strategy % 22.60/3.55 % (2612424)------------------------------ % 22.60/3.55 % (2612424)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.60/3.55 % (2612424)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.60/3.55 % (2612424)CaDiCaL version: 2.1.3 % 22.60/3.55 % (2612424)Termination reason: Refutation not found, incomplete strategy % 22.60/3.55 % (2612424)Time elapsed: 0.092 s % 22.60/3.55 % (2612424)Peak memory usage: 13 MB % 22.60/3.55 % (2612424)Instructions burned: 186 (million) % 22.60/3.55 % (2612424)------------------------------ % 22.60/3.55 % (2612424)------------------------------ % 22.60/3.55 % (2612430)ott+10_1_sil=32000:tgt=ground:random_seed=3771032772:i=5114:av=off_2991 on theBenchmark for (2991ds/5114Mi) % 22.60/3.55 % (2612427)Instruction limit reached! % 22.60/3.55 % (2612427)------------------------------ % 22.60/3.55 % (2612427)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.60/3.55 % (2612427)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.60/3.55 % (2612427)CaDiCaL version: 2.1.3 % 22.60/3.55 % (2612427)Termination reason: Instruction limit % 22.60/3.55 % (2612427)Termination phase: Saturation % 22.60/3.55 % (2612427)Time elapsed: 0.425 s % 22.60/3.55 % (2612427)Peak memory usage: 15 MB % 22.60/3.55 % (2612427)Instructions burned: 870 (million) % 22.60/3.55 % (2612432)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=3237664579:i=54282_2987 on theBenchmark for (2987ds/54282Mi) % 22.60/3.55 % (2612422)Instruction limit reached! % 22.60/3.55 % (2612422)------------------------------ % 22.60/3.55 % (2612422)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.60/3.55 % (2612422)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 56.47/8.27 % (2612422)CaDiCaL version: 2.1.3 % 56.47/8.27 % (2612422)Termination reason: Instruction limit % 56.47/8.27 % (2612422)Termination phase: Saturation % 56.47/8.27 % (2612422)Time elapsed: 0.638 s % 56.47/8.27 % (2612422)Peak memory usage: 23 MB % 56.47/8.27 % (2612422)Instructions burned: 1472 (million) % 56.47/8.27 % (2612434)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=2926782888:i=3512:aac=none_2986 on theBenchmark for (2986ds/3512Mi) % 56.47/8.27 % Detected minimum model sizes of [4] % 56.47/8.27 % Detected maximum model sizes of [max] % 56.47/8.27 % (2612432)Cannot represent all propositional literals internally % 56.47/8.27 % (2612432)Refutation not found, incomplete strategy % 56.47/8.27 % (2612432)------------------------------ % 56.47/8.27 % (2612432)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 56.47/8.27 % (2612432)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 56.47/8.27 % (2612432)CaDiCaL version: 2.1.3 % 56.47/8.27 % (2612432)Termination reason: Refutation not found, incomplete strategy % 56.47/8.27 % (2612432)Time elapsed: 0.092 s % 56.47/8.27 % (2612432)Peak memory usage: 13 MB % 56.47/8.27 % (2612432)Instructions burned: 186 (million) % 56.47/8.27 % (2612432)------------------------------ % 56.47/8.27 % (2612432)------------------------------ % 56.47/8.27 % (2612436)dis+21_1_sil=32000:sas=cadical:random_seed=213325498:i=3773:amm=off_2986 on theBenchmark for (2986ds/3773Mi) % 56.47/8.27 % Detected minimum model sizes of [4] % 56.47/8.27 % Detected maximum model sizes of [max] % 56.47/8.27 % (2612426)Cannot represent all propositional literals internally % 56.47/8.27 % (2612426)Refutation not found, incomplete strategy % 56.47/8.27 % (2612426)------------------------------ % 56.47/8.27 % (2612426)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 56.47/8.27 % (2612426)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 56.47/8.27 % (2612426)CaDiCaL version: 2.1.3 % 56.47/8.27 % (2612426)Termination reason: Refutation not found, incomplete strategy % 56.47/8.27 % (2612426)Time elapsed: 0.707 s % 56.47/8.27 % (2612426)Peak memory usage: 22 MB % 56.47/8.27 % (2612426)Instructions burned: 1359 (million) % 56.47/8.27 % (2612426)------------------------------ % 56.47/8.27 % (2612426)------------------------------ % 56.47/8.27 % (2612438)ott+11_1_sil=16000:gs=on:random_seed=4188840780:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2984 on theBenchmark for (2984ds/2251Mi) % 56.47/8.27 % (2612438)Instruction limit reached! % 56.47/8.27 % (2612438)------------------------------ % 56.47/8.27 % (2612438)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 56.47/8.27 % (2612438)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 56.47/8.27 % (2612438)CaDiCaL version: 2.1.3 % 56.47/8.27 % (2612438)Termination reason: Instruction limit % 56.47/8.27 % (2612438)Termination phase: Saturation % 56.47/8.27 % (2612438)Time elapsed: 0.701 s % 56.47/8.27 % (2612438)Peak memory usage: 19 MB % 56.47/8.27 % (2612438)Instructions burned: 2254 (million) % 56.47/8.27 % (2612440)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=1238092586:fmbsr=1.6:i=67534_2977 on theBenchmark for (2977ds/67534Mi) % 56.47/8.27 % Detected minimum model sizes of [4] % 56.47/8.27 % Detected maximum model sizes of [max] % 56.47/8.27 % (2612440)Cannot represent all propositional literals internally % 56.47/8.27 % (2612440)Refutation not found, incomplete strategy % 56.47/8.27 % (2612440)------------------------------ % 56.47/8.27 % (2612440)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 56.47/8.27 % (2612440)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 56.47/8.27 % (2612440)CaDiCaL version: 2.1.3 % 56.47/8.27 % (2612440)Termination reason: Refutation not found, incomplete strategy % 56.47/8.27 % (2612440)Time elapsed: 0.105 s % 56.47/8.27 % (2612440)Peak memory usage: 13 MB % 56.47/8.27 % (2612440)Instructions burned: 225 (million) % 56.47/8.27 % (2612440)------------------------------ % 56.47/8.27 % (2612440)------------------------------ % 56.47/8.27 % (2612442)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=1235576187:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2976 on theBenchmark for (2976ds/4591Mi) % 56.47/8.27 % (2612420)Instruction limit reached! % 56.47/8.27 % (2612420)------------------------------ % 56.47/8.27 % (2612420)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 56.47/8.27 % (2612420)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 120.34/17.23 % (2612420)CaDiCaL version: 2.1.3 % 120.34/17.23 % (2612420)Termination reason: Instruction limit % 120.34/17.23 % (2612420)Termination phase: Saturation % 120.34/17.23 % (2612420)Time elapsed: 2.169 s % 120.34/17.23 % (2612420)Peak memory usage: 23 MB % 120.34/17.23 % (2612420)Instructions burned: 5133 (million) % 120.34/17.23 % (2612444)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=431421238:i=29340_2972 on theBenchmark for (2972ds/29340Mi) % 120.34/17.23 % (2612434)Instruction limit reached! % 120.34/17.23 % (2612434)------------------------------ % 120.34/17.23 % (2612434)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 120.34/17.23 % (2612434)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 120.34/17.23 % (2612434)CaDiCaL version: 2.1.3 % 120.34/17.23 % (2612434)Termination reason: Instruction limit % 120.34/17.23 % (2612434)Termination phase: Saturation % 120.34/17.23 % (2612434)Time elapsed: 1.540 s % 120.34/17.23 % (2612434)Peak memory usage: 21 MB % 120.34/17.23 % (2612434)Instructions burned: 3513 (million) % 120.34/17.23 % (2612446)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=2232423836:i=5211_2971 on theBenchmark for (2971ds/5211Mi) % 120.34/17.23 % (2612436)Instruction limit reached! % 120.34/17.23 % (2612436)------------------------------ % 120.34/17.23 % (2612436)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 120.34/17.23 % (2612436)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 120.34/17.23 % (2612436)CaDiCaL version: 2.1.3 % 120.34/17.23 % (2612436)Termination reason: Instruction limit % 120.34/17.23 % (2612436)Termination phase: Saturation % 120.34/17.23 % (2612436)Time elapsed: 1.705 s % 120.34/17.23 % (2612436)Peak memory usage: 21 MB % 120.34/17.23 % (2612436)Instructions burned: 3773 (million) % 120.34/17.23 % (2612448)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=1369388196:i=5497:nm=2_2968 on theBenchmark for (2968ds/5497Mi) % 120.34/17.23 % (2612430)Instruction limit reached! % 120.34/17.23 % (2612430)------------------------------ % 120.34/17.23 % (2612430)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 120.34/17.23 % (2612430)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 120.34/17.23 % (2612430)CaDiCaL version: 2.1.3 % 120.34/17.23 % (2612430)Termination reason: Instruction limit % 120.34/17.23 % (2612430)Termination phase: Saturation % 120.34/17.23 % (2612430)Time elapsed: 2.292 s % 120.34/17.23 % (2612430)Peak memory usage: 26 MB % 120.34/17.23 % (2612430)Instructions burned: 5116 (million) % 120.34/17.23 % (2612450)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=2882063422:fmbsr=2:i=46332_2968 on theBenchmark for (2968ds/46332Mi) % 120.34/17.23 % Detected minimum model sizes of [4] % 120.34/17.23 % Detected maximum model sizes of [max] % 120.34/17.23 % (2612448)Cannot represent all propositional literals internally % 120.34/17.23 % (2612448)Refutation not found, incomplete strategy % 120.34/17.23 % (2612448)------------------------------ % 120.34/17.23 % (2612448)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 120.34/17.23 % (2612448)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 120.34/17.23 % (2612448)CaDiCaL version: 2.1.3 % 120.34/17.23 % (2612448)Termination reason: Refutation not found, incomplete strategy % 120.34/17.23 % (2612448)Time elapsed: 0.093 s % 120.34/17.23 % (2612448)Peak memory usage: 13 MB % 120.34/17.23 % (2612448)Instructions burned: 186 (million) % 120.34/17.23 % (2612448)------------------------------ % 120.34/17.23 % (2612448)------------------------------ % 120.34/17.23 % (2612452)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=1427397257:i=14071_2967 on theBenchmark for (2967ds/14071Mi) % 120.34/17.23 % Detected minimum model sizes of [4] % 120.34/17.23 % Detected maximum model sizes of [max] % 120.34/17.23 % (2612450)Cannot represent all propositional literals internally % 120.34/17.23 % (2612450)Refutation not found, incomplete strategy % 120.34/17.23 % (2612450)------------------------------ % 120.34/17.23 % (2612450)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 120.34/17.23 % (2612450)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 120.34/17.23 % (2612450)CaDiCaL version: 2.1.3 % 120.34/17.23 % (2612450)Termination reason: Refutation not found, incomplete strategy % 120.34/17.23 % (2612450)Time elapsed: 0.105 s % 120.34/17.23 % (2612450)Peak memory usage: 13 MB % 120.34/17.23 % (2612450)Instructions burned: 225 (million) % 120.34/17.23 % (2612450)------------------------------ % 120.34/17.23 % (2612450)------------------------------ % 120.34/17.23 % (2612454)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=823778379:i=22565:add=on:rawr=on_2966 on theBenchmark for (2966ds/22565Mi) % 124.52/17.83 % Detected minimum model sizes of [4] % 124.52/17.83 % Detected maximum model sizes of [max] % 124.52/17.83 % (2612452)Cannot represent all propositional literals internally % 124.52/17.83 % (2612452)Refutation not found, incomplete strategy % 124.52/17.83 % (2612452)------------------------------ % 124.52/17.83 % (2612452)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 124.52/17.83 % (2612452)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 124.52/17.83 % (2612452)CaDiCaL version: 2.1.3 % 124.52/17.83 % (2612452)Termination reason: Refutation not found, incomplete strategy % 124.52/17.83 % (2612452)Time elapsed: 0.092 s % 124.52/17.83 % (2612452)Peak memory usage: 13 MB % 124.52/17.83 % (2612452)Instructions burned: 186 (million) % 124.52/17.83 % (2612452)------------------------------ % 124.52/17.83 % (2612452)------------------------------ % 124.52/17.83 % (2612456)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=3786216836:i=8173:av=off_2966 on theBenchmark for (2966ds/8173Mi) % 124.52/17.83 % (2612442)Instruction limit reached! % 124.52/17.83 % (2612442)------------------------------ % 124.52/17.83 % (2612442)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 124.52/17.83 % (2612442)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 124.52/17.83 % (2612442)CaDiCaL version: 2.1.3 % 124.52/17.83 % (2612442)Termination reason: Instruction limit % 124.52/17.83 % (2612442)Termination phase: Saturation % 124.52/17.83 % (2612442)Time elapsed: 1.683 s % 124.52/17.83 % (2612442)Peak memory usage: 28 MB % 124.52/17.83 % (2612442)Instructions burned: 4591 (million) % 124.52/17.83 % (2612458)dis+10_16:1_sil=16000:random_seed=675937550:i=9155:fsr=off_2958 on theBenchmark for (2958ds/9155Mi) % 124.52/17.83 % (2612446)Instruction limit reached! % 124.52/17.83 % (2612446)------------------------------ % 124.52/17.83 % (2612446)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 124.52/17.83 % (2612446)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 124.52/17.83 % (2612446)CaDiCaL version: 2.1.3 % 124.52/17.83 % (2612446)Termination reason: Instruction limit % 124.52/17.83 % (2612446)Termination phase: Saturation % 124.52/17.83 % (2612446)Time elapsed: 2.641 s % 124.52/17.83 % (2612446)Peak memory usage: 43 MB % 124.52/17.83 % (2612446)Instructions burned: 5212 (million) % 124.52/17.83 % (2612460)ott-3_8_sil=64000:random_seed=3971991508:i=20139:bs=on_2944 on theBenchmark for (2944ds/20139Mi) % 124.52/17.83 % (2612456)Instruction limit reached! % 124.52/17.83 % (2612456)------------------------------ % 124.52/17.83 % (2612456)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 124.52/17.83 % (2612456)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 124.52/17.83 % (2612456)CaDiCaL version: 2.1.3 % 124.52/17.83 % (2612456)Termination reason: Instruction limit % 124.52/17.83 % (2612456)Termination phase: Saturation % 124.52/17.83 % (2612456)Time elapsed: 3.749 s % 124.52/17.83 % (2612456)Peak memory usage: 34 MB % 124.52/17.83 % (2612456)Instructions burned: 8173 (million) % 124.52/17.83 % (2612462)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=2855155963:fmbsr=2:i=32576_2928 on theBenchmark for (2928ds/32576Mi) % 124.52/17.83 % Detected minimum model sizes of [4] % 124.52/17.83 % Detected maximum model sizes of [max] % 124.52/17.83 % (2612462)Cannot represent all propositional literals internally % 124.52/17.83 % (2612462)Refutation not found, incomplete strategy % 124.52/17.83 % (2612462)------------------------------ % 124.52/17.83 % (2612462)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 124.52/17.83 % (2612462)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 124.52/17.83 % (2612462)CaDiCaL version: 2.1.3 % 124.52/17.83 % (2612462)Termination reason: Refutation not found, incomplete strategy % 124.52/17.83 % (2612462)Time elapsed: 0.096 s % 124.52/17.83 % (2612462)Peak memory usage: 13 MB % 124.52/17.83 % (2612462)Instructions burned: 192 (million) % 124.52/17.83 % (2612462)------------------------------ % 124.52/17.83 % (2612462)------------------------------ % 124.52/17.83 % (2612464)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=40333690:i=11404_2927 on theBenchmark for (2927ds/11404Mi) % 124.52/17.83 % (2612458)Instruction limit reached! % 124.52/17.83 % (2612458)------------------------------ % 124.52/17.83 % (2612458)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 124.52/17.83 % (2612458)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 124.52/17.83 % (2612458)CaDiCaL version: 2.1.3 % 124.52/17.83 % (2612458)Termination reason: Instruction limit % 124.52/17.83 % (2612458)Termination phase: Saturation % 141.07/20.17 % (2612458)Time elapsed: 3.922 s % 141.07/20.17 % (2612458)Peak memory usage: 30 MB % 141.07/20.17 % (2612458)Instructions burned: 9157 (million) % 141.07/20.17 % (2612466)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=1427921387:i=14134_2919 on theBenchmark for (2919ds/14134Mi) % 141.07/20.17 % (2612464)Instruction limit reached! % 141.07/20.17 % (2612464)------------------------------ % 141.07/20.17 % (2612464)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 141.07/20.17 % (2612464)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 141.07/20.17 % (2612464)CaDiCaL version: 2.1.3 % 141.07/20.17 % (2612464)Termination reason: Instruction limit % 141.07/20.17 % (2612464)Termination phase: Saturation % 141.07/20.17 % (2612464)Time elapsed: 5.003 s % 141.07/20.17 % (2612464)Peak memory usage: 32 MB % 141.07/20.17 % (2612464)Instructions burned: 11405 (million) % 141.07/20.17 % (2612468)dis+33_16_sil=32000:sac=on:random_seed=1293545059:i=15851:nm=0_2877 on theBenchmark for (2877ds/15851Mi) % 141.07/20.17 % (2612460)Instruction limit reached! % 141.07/20.17 % (2612460)------------------------------ % 141.07/20.17 % (2612460)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 141.07/20.17 % (2612460)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 141.07/20.17 % (2612460)CaDiCaL version: 2.1.3 % 141.07/20.17 % (2612460)Termination reason: Instruction limit % 141.07/20.17 % (2612460)Termination phase: Saturation % 141.07/20.17 % (2612460)Time elapsed: 7.744 s % 141.07/20.17 % (2612460)Peak memory usage: 23 MB % 141.07/20.17 % (2612460)Instructions burned: 20141 (million) % 141.07/20.17 % (2612470)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=3287196741:avsq=on:i=17627:add=on:amm=off_2866 on theBenchmark for (2866ds/17627Mi) % 141.07/20.17 % (2612466)Instruction limit reached! % 141.07/20.17 % (2612466)------------------------------ % 141.07/20.17 % (2612466)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 141.07/20.17 % (2612466)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 141.07/20.17 % (2612466)CaDiCaL version: 2.1.3 % 141.07/20.17 % (2612466)Termination reason: Instruction limit % 141.07/20.17 % (2612466)Termination phase: Saturation % 141.07/20.17 % (2612466)Time elapsed: 6.053 s % 141.07/20.17 % (2612466)Peak memory usage: 31 MB % 141.07/20.17 % (2612466)Instructions burned: 14134 (million) % 141.07/20.17 % (2612472)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=3038916423:s2a=on:i=53295_2858 on theBenchmark for (2858ds/53295Mi) % 141.07/20.17 % (2612454)Instruction limit reached! % 141.07/20.17 % (2612454)------------------------------ % 141.07/20.17 % (2612454)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 141.07/20.17 % (2612454)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 141.07/20.17 % (2612454)CaDiCaL version: 2.1.3 % 141.07/20.17 % (2612454)Termination reason: Instruction limit % 141.07/20.17 % (2612454)Termination phase: Saturation % 141.07/20.17 % (2612454)Time elapsed: 12.717 s % 141.07/20.17 % (2612454)Peak memory usage: 145 MB % 141.07/20.17 % (2612454)Instructions burned: 22566 (million) % 141.07/20.17 % (2612474)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=3986173173:i=26857:ins=20_2839 on theBenchmark for (2839ds/26857Mi) % 141.07/20.17 % Detected minimum model sizes of [4] % 141.07/20.17 % Detected maximum model sizes of [max] % 141.07/20.17 % (2612474)Cannot represent all propositional literals internally % 141.07/20.17 % (2612474)Refutation not found, incomplete strategy % 141.07/20.17 % (2612474)------------------------------ % 141.07/20.17 % (2612474)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 141.07/20.17 % (2612474)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 141.07/20.17 % (2612474)CaDiCaL version: 2.1.3 % 141.07/20.17 % (2612474)Termination reason: Refutation not found, incomplete strategy % 141.07/20.17 % (2612474)Time elapsed: 0.089 s % 141.07/20.17 % (2612474)Peak memory usage: 13 MB % 141.07/20.17 % (2612474)Instructions burned: 174 (million) % 141.07/20.17 % (2612474)------------------------------ % 141.07/20.17 % (2612474)------------------------------ % 141.07/20.17 % (2612476)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=7649421:i=28120:bs=on:fsr=off_2838 on theBenchmark for (2838ds/28120Mi) % 141.07/20.17 % (2612444)Instruction limit reached! % 141.07/20.17 % (2612444)------------------------------ % 141.07/20.17 % (2612444)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 141.07/20.17 % (2612444)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 152.10/21.72 % (2612444)CaDiCaL version: 2.1.3 % 152.10/21.72 % (2612444)Termination reason: Instruction limit % 152.10/21.72 % (2612444)Termination phase: Saturation % 152.10/21.72 % (2612444)Time elapsed: 14.223 s % 152.10/21.72 % (2612444)Peak memory usage: 287 MB % 152.10/21.72 % (2612444)Instructions burned: 29341 (million) % 152.10/21.72 % (2612478)fmb+10_1_sil=256000:fmbss=7:random_seed=3939417003:fmbsr=1.6:i=182295_2829 on theBenchmark for (2829ds/182295Mi) % 152.10/21.72 % Detected minimum model sizes of [4] % 152.10/21.72 % Detected maximum model sizes of [max] % 152.10/21.72 % (2612478)Cannot represent all propositional literals internally % 152.10/21.72 % (2612478)Refutation not found, incomplete strategy % 152.10/21.72 % (2612478)------------------------------ % 152.10/21.72 % (2612478)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 152.10/21.72 % (2612478)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 152.10/21.72 % (2612478)CaDiCaL version: 2.1.3 % 152.10/21.72 % (2612478)Termination reason: Refutation not found, incomplete strategy % 152.10/21.72 % (2612478)Time elapsed: 0.087 s % 152.10/21.72 % (2612478)Peak memory usage: 13 MB % 152.10/21.72 % (2612478)Instructions burned: 174 (million) % 152.10/21.72 % (2612478)------------------------------ % 152.10/21.72 % (2612478)------------------------------ % 152.10/21.72 % (2612480)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=2350963531:i=44625:gsp=on_2828 on theBenchmark for (2828ds/44625Mi) % 152.10/21.72 % Detected minimum model sizes of [4] % 152.10/21.72 % Detected maximum model sizes of [max] % 152.10/21.72 % (2612480)Cannot represent all propositional literals internally % 152.10/21.72 % (2612480)Refutation not found, incomplete strategy % 152.10/21.72 % (2612480)------------------------------ % 152.10/21.72 % (2612480)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 152.10/21.72 % (2612480)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 152.10/21.72 % (2612480)CaDiCaL version: 2.1.3 % 152.10/21.72 % (2612480)Termination reason: Refutation not found, incomplete strategy % 152.10/21.72 % (2612480)Time elapsed: 0.091 s % 152.10/21.72 % (2612480)Peak memory usage: 13 MB % 152.10/21.72 % (2612480)Instructions burned: 182 (million) % 152.10/21.72 % (2612480)------------------------------ % 152.10/21.72 % (2612480)------------------------------ % 152.10/21.72 % (2612482)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=3729877361:i=160505_2827 on theBenchmark for (2827ds/160505Mi) % 152.10/21.72 % Detected minimum model sizes of [4] % 152.10/21.72 % Detected maximum model sizes of [max] % 152.10/21.72 % (2612482)Cannot represent all propositional literals internally % 152.10/21.72 % (2612482)Refutation not found, incomplete strategy % 152.10/21.72 % (2612482)------------------------------ % 152.10/21.72 % (2612482)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 152.10/21.72 % (2612482)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 152.10/21.72 % (2612482)CaDiCaL version: 2.1.3 % 152.10/21.72 % (2612482)Termination reason: Refutation not found, incomplete strategy % 152.10/21.72 % (2612482)Time elapsed: 0.087 s % 152.10/21.72 % (2612482)Peak memory usage: 13 MB % 152.10/21.72 % (2612482)Instructions burned: 174 (million) % 152.10/21.72 % (2612482)------------------------------ % 152.10/21.72 % (2612482)------------------------------ % 152.10/21.72 % (2612484)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=1006615749:fmbsr=1.3:i=225729_2826 on theBenchmark for (2826ds/225729Mi) % 152.10/21.72 % Detected minimum model sizes of [4] % 152.10/21.72 % Detected maximum model sizes of [max] % 152.10/21.72 % (2612484)Cannot represent all propositional literals internally % 152.10/21.72 % (2612484)Refutation not found, incomplete strategy % 152.10/21.72 % (2612484)------------------------------ % 152.10/21.72 % (2612484)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 152.10/21.72 % (2612484)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 152.10/21.72 % (2612484)CaDiCaL version: 2.1.3 % 152.10/21.72 % (2612484)Termination reason: Refutation not found, incomplete strategy % 152.10/21.72 % (2612484)Time elapsed: 0.092 s % 152.10/21.72 % (2612484)Peak memory usage: 13 MB % 152.10/21.72 % (2612484)Instructions burned: 186 (million) % 152.10/21.72 % (2612484)------------------------------ % 152.10/21.72 % (2612484)------------------------------ % 152.10/21.72 % (2612486)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=1553582343:fmbsr=2:i=185024:ins=7_2825 on theBenchmark for (2825ds/185024Mi) % 152.10/21.72 % Detected minimum model sizes of [4] % 152.10/21.72 % Detected maximum model sizes of [max] % 152.10/21.72 % (2612486)Cannot represent all propositional literals internally % 152.10/21.72 % (2612486)Refutation not found, incomplete strategy % 152.10/21.72 % (2612486)------------------------------ % 172.86/24.61 % (2612486)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 172.86/24.61 % (2612486)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 172.86/24.61 % (2612486)CaDiCaL version: 2.1.3 % 172.86/24.61 % (2612486)Termination reason: Refutation not found, incomplete strategy % 172.86/24.61 % (2612486)Time elapsed: 0.092 s % 172.86/24.61 % (2612486)Peak memory usage: 13 MB % 172.86/24.61 % (2612486)Instructions burned: 186 (million) % 172.86/24.61 % (2612486)------------------------------ % 172.86/24.61 % (2612486)------------------------------ % 172.86/24.61 % (2612488)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=864235639:rtra=on_2823 on theBenchmark for (2823ds/0Mi) % 172.86/24.61 % Detected minimum model sizes of [4] % 172.86/24.61 % Detected maximum model sizes of [max] % 172.86/24.61 % (2612488)Cannot represent all propositional literals internally % 172.86/24.61 % (2612488)Refutation not found, incomplete strategy % 172.86/24.61 % (2612488)------------------------------ % 172.86/24.61 % (2612488)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 172.86/24.61 % (2612488)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 172.86/24.61 % (2612488)CaDiCaL version: 2.1.3 % 172.86/24.61 % (2612488)Termination reason: Refutation not found, incomplete strategy % 172.86/24.61 % (2612488)Time elapsed: 0.097 s % 172.86/24.61 % (2612488)Peak memory usage: 13 MB % 172.86/24.61 % (2612488)Instructions burned: 188 (million) % 172.86/24.61 % (2612488)------------------------------ % 172.86/24.61 % (2612488)------------------------------ % 172.86/24.61 % (2612490)% WARNING: option uhcvi not known. % 172.86/24.61 % (2612490)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=775390009:i=271062:add=off:rtra=on:rawr=on_2822 on theBenchmark for (2822ds/271062Mi) % 172.86/24.61 % (2612470)Instruction limit reached! % 172.86/24.61 % (2612470)------------------------------ % 172.86/24.61 % (2612470)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 172.86/24.61 % (2612470)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 172.86/24.61 % (2612470)CaDiCaL version: 2.1.3 % 172.86/24.61 % (2612470)Termination reason: Instruction limit % 172.86/24.61 % (2612470)Termination phase: Saturation % 172.86/24.61 % (2612470)Time elapsed: 5.009 s % 172.86/24.61 % (2612470)Peak memory usage: 25 MB % 172.86/24.61 % (2612470)Instructions burned: 17628 (million) % 172.86/24.61 % (2612492)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1707634969:i=176048:add=on:rtra=on:rawr=on_2816 on theBenchmark for (2816ds/176048Mi) % 172.86/24.61 % (2612468)Instruction limit reached! % 172.86/24.61 % (2612468)------------------------------ % 172.86/24.61 % (2612468)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 172.86/24.61 % (2612468)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 172.86/24.61 % (2612468)CaDiCaL version: 2.1.3 % 172.86/24.61 % (2612468)Termination reason: Instruction limit % 172.86/24.61 % (2612468)Termination phase: Saturation % 172.86/24.61 % (2612468)Time elapsed: 7.374 s % 172.86/24.61 % (2612468)Peak memory usage: 84 MB % 172.86/24.61 % (2612468)Instructions burned: 15852 (million) % 172.86/24.61 % (2612494)dis+10_1_sil=32000:si=on:sp=arity:random_seed=2828573139:i=206:fgj=on:rtra=on_2803 on theBenchmark for (2803ds/206Mi) % 172.86/24.61 % (2612494)Instruction limit reached! % 172.86/24.61 % (2612494)------------------------------ % 172.86/24.61 % (2612494)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 172.86/24.61 % (2612494)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 172.86/24.61 % (2612494)CaDiCaL version: 2.1.3 % 172.86/24.61 % (2612494)Termination reason: Instruction limit % 172.86/24.61 % (2612494)Termination phase: Saturation % 172.86/24.61 % (2612494)Time elapsed: 0.109 s % 172.86/24.61 % (2612494)Peak memory usage: 12 MB % 172.86/24.61 % (2612494)Instructions burned: 206 (million) % 172.86/24.61 % (2612496)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=3363883411:i=232:rtra=on_2802 on theBenchmark for (2802ds/232Mi) % 172.86/24.61 % (2612496)Instruction limit reached! % 172.86/24.61 % (2612496)------------------------------ % 172.86/24.61 % (2612496)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 172.86/24.61 % (2612496)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 172.86/24.61 % (2612496)CaDiCaL version: 2.1.3 % 172.86/24.61 % (2612496)Termination reason: Instruction limit % 172.86/24.61 % (2612496)Termination phase: Saturation % 172.86/24.61 % (2612496)Time elapsed: 0.120 s % 172.86/24.61 % (2612496)Peak memory usage: 13 MB % 182.01/25.92 % (2612496)Instructions burned: 233 (million) % 182.01/25.92 % (2612498)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=2353976356:i=262:rtra=on_2800 on theBenchmark for (2800ds/262Mi) % 182.01/25.92 % (2612498)Instruction limit reached! % 182.01/25.92 % (2612498)------------------------------ % 182.01/25.92 % (2612498)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 182.01/25.92 % (2612498)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 182.01/25.92 % (2612498)CaDiCaL version: 2.1.3 % 182.01/25.92 % (2612498)Termination reason: Instruction limit % 182.01/25.92 % (2612498)Termination phase: Saturation % 182.01/25.92 % (2612498)Time elapsed: 0.143 s % 182.01/25.92 % (2612498)Peak memory usage: 14 MB % 182.01/25.92 % (2612498)Instructions burned: 262 (million) % 182.01/25.92 % (2612500)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=2695806117:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2798 on theBenchmark for (2798ds/318Mi) % 182.01/25.92 % (2612500)Instruction limit reached! % 182.01/25.92 % (2612500)------------------------------ % 182.01/25.92 % (2612500)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 182.01/25.92 % (2612500)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 182.01/25.92 % (2612500)CaDiCaL version: 2.1.3 % 182.01/25.92 % (2612500)Termination reason: Instruction limit % 182.01/25.92 % (2612500)Termination phase: Saturation % 182.01/25.92 % (2612500)Time elapsed: 0.186 s % 182.01/25.92 % (2612500)Peak memory usage: 14 MB % 182.01/25.92 % (2612500)Instructions burned: 318 (million) % 182.01/25.92 % (2612502)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=2479336835:i=1428:nm=2:rtra=on_2796 on theBenchmark for (2796ds/1428Mi) % 182.01/25.92 % Detected minimum model sizes of [4] % 182.01/25.92 % Detected maximum model sizes of [max] % 182.01/25.92 % (2612502)Cannot represent all propositional literals internally % 182.01/25.92 % (2612502)Refutation not found, incomplete strategy % 182.01/25.92 % (2612502)------------------------------ % 182.01/25.92 % (2612502)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 182.01/25.92 % (2612502)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 182.01/25.92 % (2612502)CaDiCaL version: 2.1.3 % 182.01/25.92 % (2612502)Termination reason: Refutation not found, incomplete strategy % 182.01/25.92 % (2612502)Time elapsed: 0.106 s % 182.01/25.92 % (2612502)Peak memory usage: 13 MB % 182.01/25.92 % (2612502)Instructions burned: 215 (million) % 182.01/25.92 % (2612502)------------------------------ % 182.01/25.92 % (2612502)------------------------------ % 182.01/25.92 % (2612504)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=232890808:i=262:bd=preordered:rtra=on:fsd=on_2795 on theBenchmark for (2795ds/262Mi) % 182.01/25.92 % (2612504)Instruction limit reached! % 182.01/25.92 % (2612504)------------------------------ % 182.01/25.92 % (2612504)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 182.01/25.92 % (2612504)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 182.01/25.92 % (2612504)CaDiCaL version: 2.1.3 % 182.01/25.92 % (2612504)Termination reason: Instruction limit % 182.01/25.92 % (2612504)Termination phase: Saturation % 182.01/25.92 % (2612504)Time elapsed: 0.142 s % 182.01/25.92 % (2612504)Peak memory usage: 14 MB % 182.01/25.92 % (2612504)Instructions burned: 262 (million) % 182.01/25.92 % (2612506)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=3796429639:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2794 on theBenchmark for (2794ds/1368Mi) % 182.01/25.92 % (2612506)Instruction limit reached! % 182.01/25.92 % (2612506)------------------------------ % 182.01/25.92 % (2612506)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 182.01/25.92 % (2612506)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 182.01/25.92 % (2612506)CaDiCaL version: 2.1.3 % 182.01/25.92 % (2612506)Termination reason: Instruction limit % 182.01/25.92 % (2612506)Termination phase: Saturation % 182.01/25.92 % (2612506)Time elapsed: 0.668 s % 182.01/25.92 % (2612506)Peak memory usage: 22 MB % 182.01/25.92 % (2612506)Instructions burned: 1369 (million) % 182.01/25.92 % (2612508)ott-21_1_sil=16000:si=on:fs=off:random_seed=2071723988:i=360:av=off:fsr=off:rtra=on_2787 on theBenchmark for (2787ds/360Mi) % 182.01/25.92 % (2612508)Instruction limit reached! % 182.01/25.92 % (2612508)------------------------------ % 182.01/25.92 % (2612508)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 182.01/25.92 % (2612508)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 216.87/30.86 % (2612508)CaDiCaL version: 2.1.3 % 216.87/30.86 % (2612508)Termination reason: Instruction limit % 216.87/30.86 % (2612508)Termination phase: Saturation % 216.87/30.86 % (2612508)Time elapsed: 0.180 s % 216.87/30.86 % (2612508)Peak memory usage: 13 MB % 216.87/30.86 % (2612508)Instructions burned: 361 (million) % 216.87/30.86 % (2612510)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3064605118:i=954:bd=all:rtra=on_2785 on theBenchmark for (2785ds/954Mi) % 216.87/30.86 % (2612510)Instruction limit reached! % 216.87/30.86 % (2612510)------------------------------ % 216.87/30.86 % (2612510)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 216.87/30.86 % (2612510)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 216.87/30.86 % (2612510)CaDiCaL version: 2.1.3 % 216.87/30.86 % (2612510)Termination reason: Instruction limit % 216.87/30.86 % (2612510)Termination phase: Saturation % 216.87/30.86 % (2612510)Time elapsed: 0.512 s % 216.87/30.86 % (2612510)Peak memory usage: 17 MB % 216.87/30.86 % (2612510)Instructions burned: 955 (million) % 216.87/30.86 % (2612512)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=2156555216:fmbsr=1.3:i=1730:ins=25:rtra=on_2779 on theBenchmark for (2779ds/1730Mi) % 216.87/30.86 % Detected minimum model sizes of [4] % 216.87/30.86 % Detected maximum model sizes of [max] % 216.87/30.86 % (2612512)Cannot represent all propositional literals internally % 216.87/30.86 % (2612512)Refutation not found, incomplete strategy % 216.87/30.86 % (2612512)------------------------------ % 216.87/30.86 % (2612512)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 216.87/30.86 % (2612512)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 216.87/30.86 % (2612512)CaDiCaL version: 2.1.3 % 216.87/30.86 % (2612512)Termination reason: Refutation not found, incomplete strategy % 216.87/30.86 % (2612512)Time elapsed: 0.093 s % 216.87/30.86 % (2612512)Peak memory usage: 13 MB % 216.87/30.86 % (2612512)Instructions burned: 175 (million) % 216.87/30.86 % (2612512)------------------------------ % 216.87/30.86 % (2612512)------------------------------ % 216.87/30.86 % (2612514)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=4115589156:i=2358:rtra=on_2778 on theBenchmark for (2778ds/2358Mi) % 216.87/30.86 % (2612514)Instruction limit reached! % 216.87/30.86 % (2612514)------------------------------ % 216.87/30.86 % (2612514)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 216.87/30.86 % (2612514)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 216.87/30.86 % (2612514)CaDiCaL version: 2.1.3 % 216.87/30.86 % (2612514)Termination reason: Instruction limit % 216.87/30.86 % (2612514)Termination phase: Saturation % 216.87/30.86 % (2612514)Time elapsed: 1.267 s % 216.87/30.86 % (2612514)Peak memory usage: 20 MB % 216.87/30.86 % (2612514)Instructions burned: 2359 (million) % 216.87/30.86 % (2612516)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=2689272072:i=1778:ins=1:rtra=on_2765 on theBenchmark for (2765ds/1778Mi) % 216.87/30.86 % (2612516)Cannot represent all propositional literals internally % 216.87/30.86 % (2612516)Refutation not found, incomplete strategy % 216.87/30.86 % (2612516)------------------------------ % 216.87/30.86 % (2612516)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 216.87/30.86 % (2612516)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 216.87/30.86 % (2612516)CaDiCaL version: 2.1.3 % 216.87/30.86 % (2612516)Termination reason: Refutation not found, incomplete strategy % 216.87/30.86 % (2612516)Time elapsed: 0.098 s % 216.87/30.86 % (2612516)Peak memory usage: 13 MB % 216.87/30.86 % (2612516)Instructions burned: 182 (million) % 216.87/30.86 % (2612516)------------------------------ % 216.87/30.86 % (2612516)------------------------------ % 216.87/30.86 % (2612518)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=3861577808:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2764 on theBenchmark for (2764ds/1384Mi) % 216.87/30.86 % (2612518)Instruction limit reached! % 216.87/30.86 % (2612518)------------------------------ % 216.87/30.86 % (2612518)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 216.87/30.86 % (2612518)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 216.87/30.86 % (2612518)CaDiCaL version: 2.1.3 % 216.87/30.86 % (2612518)Termination reason: Instruction limit % 216.87/30.86 % (2612518)Termination phase: Saturation % 216.87/30.86 % (2612518)Time elapsed: 0.815 s % 216.87/30.86 % (2612518)Peak memory usage: 28 MB % 241.71/34.35 % (2612518)Instructions burned: 1384 (million) % 241.71/34.35 % (2612520)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=2077025949:i=1758:kws=inv_precedence:fsr=off:rtra=on_2756 on theBenchmark for (2756ds/1758Mi) % 241.71/34.35 % (2612520)Instruction limit reached! % 241.71/34.35 % (2612520)------------------------------ % 241.71/34.35 % (2612520)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 241.71/34.35 % (2612520)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 241.71/34.35 % (2612520)CaDiCaL version: 2.1.3 % 241.71/34.35 % (2612520)Termination reason: Instruction limit % 241.71/34.35 % (2612520)Termination phase: Saturation % 241.71/34.35 % (2612520)Time elapsed: 0.927 s % 241.71/34.35 % (2612520)Peak memory usage: 22 MB % 241.71/34.35 % (2612520)Instructions burned: 1759 (million) % 241.71/34.35 % (2612522)fmb+10_1_sil=64000:si=on:random_seed=4168491398:i=44122:nm=2:rtra=on:gsp=on_2746 on theBenchmark for (2746ds/44122Mi) % 241.71/34.35 % Detected minimum model sizes of [4] % 241.71/34.35 % Detected maximum model sizes of [max] % 241.71/34.35 % (2612522)Cannot represent all propositional literals internally % 241.71/34.35 % (2612522)Refutation not found, incomplete strategy % 241.71/34.35 % (2612522)------------------------------ % 241.71/34.35 % (2612522)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 241.71/34.35 % (2612522)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 241.71/34.35 % (2612522)CaDiCaL version: 2.1.3 % 241.71/34.35 % (2612522)Termination reason: Refutation not found, incomplete strategy % 241.71/34.35 % (2612522)Time elapsed: 0.098 s % 241.71/34.35 % (2612522)Peak memory usage: 13 MB % 241.71/34.35 % (2612522)Instructions burned: 183 (million) % 241.71/34.35 % (2612522)------------------------------ % 241.71/34.35 % (2612522)------------------------------ % 241.71/34.35 % (2612524)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=2966574648:i=19030:nm=5:rtra=on_2745 on theBenchmark for (2745ds/19030Mi) % 241.71/34.35 % Detected minimum model sizes of [4] % 241.71/34.35 % Detected maximum model sizes of [max] % 241.71/34.35 % (2612524)Cannot represent all propositional literals internally % 241.71/34.35 % (2612524)Refutation not found, incomplete strategy % 241.71/34.35 % (2612524)------------------------------ % 241.71/34.35 % (2612524)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 241.71/34.35 % (2612524)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 241.71/34.35 % (2612524)CaDiCaL version: 2.1.3 % 241.71/34.35 % (2612524)Termination reason: Refutation not found, incomplete strategy % 241.71/34.35 % (2612524)Time elapsed: 0.093 s % 241.71/34.35 % (2612524)Peak memory usage: 13 MB % 241.71/34.35 % (2612524)Instructions burned: 175 (million) % 241.71/34.35 % (2612524)------------------------------ % 241.71/34.35 % (2612524)------------------------------ % 241.71/34.35 % (2612526)fmb+10_1_sil=64000:sas=cadical:si=on:fmbss=8:random_seed=947415880:fmbsr=1.7:i=1840:rtra=on_2744 on theBenchmark for (2744ds/1840Mi) % 241.71/34.35 % (2612476)Instruction limit reached! % 241.71/34.35 % (2612476)------------------------------ % 241.71/34.35 % (2612476)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 241.71/34.35 % (2612476)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 241.71/34.35 % (2612476)CaDiCaL version: 2.1.3 % 241.71/34.35 % (2612476)Termination reason: Instruction limit % 241.71/34.35 % (2612476)Termination phase: Saturation % 241.71/34.35 % (2612476)Time elapsed: 9.482 s % 241.71/34.35 % (2612476)Peak memory usage: 21 MB % 241.71/34.35 % (2612476)Instructions burned: 28123 (million) % 241.71/34.35 % Detected minimum model sizes of [4] % 241.71/34.35 % Detected maximum model sizes of [max] % 241.71/34.35 % (2612526)Cannot represent all propositional literals internally % 241.71/34.35 % (2612526)Refutation not found, incomplete strategy % 241.71/34.35 % (2612526)------------------------------ % 241.71/34.35 % (2612526)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 241.71/34.35 % (2612526)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 241.71/34.35 % (2612526)CaDiCaL version: 2.1.3 % 241.71/34.35 % (2612526)Termination reason: Refutation not found, incomplete strategy % 241.71/34.35 % (2612526)Time elapsed: 0.093 s % 241.71/34.35 % (2612526)Peak memory usage: 13 MB % 241.71/34.35 % (2612526)Instructions burned: 175 (million) % 241.71/34.35 % (2612526)------------------------------ % 241.71/34.35 % (2612526)------------------------------ % 241.71/34.35 % (2612528)dis-4_1_sil=16000:drc=ordering:si=on:sp=const_frequency:sac=on:newcnf=on:random_seed=3085177498:i=10262:rtra=on_2743 on theBenchmark for (2743ds/10262Mi) % 252.34/35.84 % (2612529)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:si=on:sp=arity:spb=units:lsd=10:nwc=3:random_seed=513841472:i=2944:ins=7:rtra=on:fdi=8:gsp=on_2743 on theBenchmark for (2743ds/2944Mi) % 252.34/35.84 % (2612529)Instruction limit reached! % 252.34/35.84 % (2612529)------------------------------ % 252.34/35.84 % (2612529)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 252.34/35.84 % (2612529)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 252.34/35.84 % (2612529)CaDiCaL version: 2.1.3 % 252.34/35.84 % (2612529)Termination reason: Instruction limit % 252.34/35.84 % (2612529)Termination phase: Saturation % 252.34/35.84 % (2612529)Time elapsed: 1.374 s % 252.34/35.84 % (2612529)Peak memory usage: 36 MB % 252.34/35.84 % (2612529)Instructions burned: 2946 (million) % 252.34/35.84 % (2612532)fmb+10_1_sil=16000:sas=cadical:si=on:bce=on:fmbss=77:random_seed=829483611:i=12648:rtra=on_2729 on theBenchmark for (2729ds/12648Mi) % 252.34/35.84 % Detected minimum model sizes of [4] % 252.34/35.84 % Detected maximum model sizes of [max] % 252.34/35.84 % (2612532)Cannot represent all propositional literals internally % 252.34/35.84 % (2612532)Refutation not found, incomplete strategy % 252.34/35.84 % (2612532)------------------------------ % 252.34/35.84 % (2612532)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 252.34/35.84 % (2612532)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 252.34/35.84 % (2612532)CaDiCaL version: 2.1.3 % 252.34/35.84 % (2612532)Termination reason: Refutation not found, incomplete strategy % 252.34/35.84 % (2612532)Time elapsed: 0.099 s % 252.34/35.84 % (2612532)Peak memory usage: 13 MB % 252.34/35.84 % (2612532)Instructions burned: 187 (million) % 252.34/35.84 % (2612532)------------------------------ % 252.34/35.84 % (2612532)------------------------------ % 252.34/35.84 % (2612534)fmb+10_1_fmbas=function:sil=32000:sas=cadical:si=on:fmbss=16:random_seed=3317420131:fmbsr=2.30978:i=4348:rtra=on_2727 on theBenchmark for (2727ds/4348Mi) % 252.34/35.84 % Detected minimum model sizes of [4] % 252.34/35.84 % Detected maximum model sizes of [max] % 252.34/35.84 % (2612534)Cannot represent all propositional literals internally % 252.34/35.84 % (2612534)Refutation not found, incomplete strategy % 252.34/35.84 % (2612534)------------------------------ % 252.34/35.84 % (2612534)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 252.34/35.84 % (2612534)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 252.34/35.84 % (2612534)CaDiCaL version: 2.1.3 % 252.34/35.84 % (2612534)Termination reason: Refutation not found, incomplete strategy % 252.34/35.84 % (2612534)Time elapsed: 0.725 s % 252.34/35.84 % (2612534)Peak memory usage: 22 MB % 252.34/35.84 % (2612534)Instructions burned: 1365 (million) % 252.34/35.84 % (2612534)------------------------------ % 252.34/35.84 % (2612534)------------------------------ % 252.34/35.84 % (2612536)ott-2_1_sil=16000:si=on:newcnf=on:random_seed=3122508500:avsq=on:i=1738:avsqr=1,16:kws=inv_arity_squared:rtra=on_2720 on theBenchmark for (2720ds/1738Mi) % 252.34/35.84 % (2612536)Instruction limit reached! % 252.34/35.84 % (2612536)------------------------------ % 252.34/35.84 % (2612536)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 252.34/35.84 % (2612536)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 252.34/35.84 % (2612536)CaDiCaL version: 2.1.3 % 252.34/35.84 % (2612536)Termination reason: Instruction limit % 252.34/35.84 % (2612536)Termination phase: Saturation % 252.34/35.84 % (2612536)Time elapsed: 0.814 s % 252.34/35.84 % (2612536)Peak memory usage: 16 MB % 252.34/35.84 % (2612536)Instructions burned: 1739 (million) % 252.34/35.84 % (2612538)ott+10_1_sil=32000:tgt=ground:si=on:random_seed=3396095419:i=10228:av=off:rtra=on_2712 on theBenchmark for (2712ds/10228Mi) % 252.34/35.84 % (2612382)Instruction limit reached! % 252.34/35.84 % (2612382)------------------------------ % 252.34/35.84 % (2612382)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 252.34/35.84 % (2612382)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 252.34/35.84 % (2612382)CaDiCaL version: 2.1.3 % 252.34/35.84 % (2612382)Termination reason: Instruction limit % 252.34/35.84 % (2612382)Termination phase: Saturation % 252.34/35.84 % (2612382)Time elapsed: 30.499 s % 252.34/35.84 % (2612382)Peak memory usage: 243 MB % 252.34/35.84 % (2612382)Instructions burned: 88026 (million) % 252.34/35.84 % (2612540)fmb+10_1_sil=64000:sas=cadical:si=on:bce=on:rp=on:random_seed=2546455820:i=108564:rtra=on_2694 on theBenchmark for (2694ds/108564Mi) % 252.34/35.84 % Detected minimum model sizes of [4] % 252.34/35.84 % Detected maximum model sizes of [max] % 252.34/35.84 % (2612540)Cannot represent all propositional literals internally % 300.64/42.64 % (2612540)Refutation not found, incomplete strategy % 300.64/42.64 % (2612540)------------------------------ % 300.64/42.64 % (2612540)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.64/42.64 % (2612540)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.64/42.64 % (2612540)CaDiCaL version: 2.1.3 % 300.64/42.64 % (2612540)Termination reason: Refutation not found, incomplete strategy % 300.64/42.64 % (2612540)Time elapsed: 0.052 s % 300.64/42.64 % (2612540)Peak memory usage: 13 MB % 300.64/42.64 % (2612540)Instructions burned: 187 (million) % 300.64/42.64 % (2612540)------------------------------ % 300.64/42.64 % (2612540)------------------------------ % 300.64/42.64 % (2612542)dis-11_1_sil=16000:si=on:sp=reverse_frequency:alpa=true:random_seed=824695533:i=7024:aac=none:rtra=on_2693 on theBenchmark for (2693ds/7024Mi) % 300.64/42.64 % (2612528)Instruction limit reached! % 300.64/42.64 % (2612528)------------------------------ % 300.64/42.64 % (2612528)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.64/42.64 % (2612528)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.64/42.64 % (2612528)CaDiCaL version: 2.1.3 % 300.64/42.64 % (2612528)Termination reason: Instruction limit % 300.64/42.64 % (2612528)Termination phase: Saturation % 300.64/42.64 % (2612528)Time elapsed: 5.074 s % 300.64/42.64 % (2612528)Peak memory usage: 34 MB % 300.64/42.64 % (2612528)Instructions burned: 10265 (million) % 300.64/42.64 % (2612544)dis+21_1_sil=32000:sas=cadical:si=on:random_seed=4256517365:i=7546:rtra=on:amm=off_2692 on theBenchmark for (2692ds/7546Mi) % 300.64/42.64 % (2612542)Instruction limit reached! % 300.64/42.64 % (2612542)------------------------------ % 300.64/42.64 % (2612542)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.64/42.64 % (2612542)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.64/42.64 % (2612542)CaDiCaL version: 2.1.3 % 300.64/42.64 % (2612542)Termination reason: Instruction limit % 300.64/42.64 % (2612542)Termination phase: Saturation % 300.64/42.64 % (2612542)Time elapsed: 1.811 s % 300.64/42.64 % (2612542)Peak memory usage: 28 MB % 300.64/42.64 % (2612542)Instructions burned: 7025 (million) % 300.64/42.64 % (2612546)ott+11_1_sil=16000:si=on:gs=on:random_seed=3624046187:s2a=on:i=4502:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:rtra=on:fsd=on_2675 on theBenchmark for (2675ds/4502Mi) % 300.64/42.64 % (2612546)Instruction limit reached! % 300.64/42.64 % (2612546)------------------------------ % 300.64/42.64 % (2612546)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.64/42.64 % (2612546)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.64/42.64 % (2612546)CaDiCaL version: 2.1.3 % 300.64/42.64 % (2612546)Termination reason: Instruction limit % 300.64/42.64 % (2612546)Termination phase: Saturation % 300.64/42.64 % (2612546)Time elapsed: 1.078 s % 300.64/42.64 % (2612546)Peak memory usage: 20 MB % 300.64/42.64 % (2612546)Instructions burned: 4506 (million) % 300.64/42.64 % (2612548)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:si=on:fmbss=7:random_seed=1760555359:fmbsr=1.6:i=135068:rtra=on_2664 on theBenchmark for (2664ds/135068Mi) % 300.64/42.64 % Detected minimum model sizes of [4] % 300.64/42.64 % Detected maximum model sizes of [max] % 300.64/42.64 % (2612548)Cannot represent all propositional literals internally % 300.64/42.64 % (2612548)Refutation not found, incomplete strategy % 300.64/42.64 % (2612548)------------------------------ % 300.64/42.64 % (2612548)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.64/42.64 % (2612548)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.64/42.64 % (2612548)CaDiCaL version: 2.1.3 % 300.64/42.64 % (2612548)Termination reason: Refutation not found, incomplete strategy % 300.64/42.64 % (2612548)Time elapsed: 0.059 s % 300.64/42.64 % (2612548)Peak memory usage: 13 MB % 300.64/42.64 % (2612548)Instructions burned: 227 (million) % 300.64/42.64 % (2612548)------------------------------ % 300.64/42.64 % (2612548)------------------------------ % 300.64/42.64 % (2612550)ott-22_32_sil=16000:tgt=full:si=on:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=3511754993:avsq=on:i=9182:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:rtra=on:fdi=4_2663 on theBenchmark for (2663ds/9182Mi) % 300.64/42.64 % (2612538)Instruction limit reached! % 300.64/42.64 % (2612538)------------------------------ % 300.64/42.64 % (2612538)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.64/42.64 % (2612538)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.64/42.64 % % 300.64/42.64 Terminated % 300.64/42.64 % Vampire exiting % 300.64/42.64 Terminated %------------------------------------------------------------------------------