%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWX142_1 : TPTP v9.3.1. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % Computer : n012.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:46:33 PM UTC 2026 % Result : Timeout 301.35s 43.05s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.01 % Problem : SWX142_1 : TPTP v9.3.1. Released v9.3.0. % 0.00/0.03 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.00/0.11 % Computer : n012.cluster.edu % 0.00/0.11 % Model : x86_64 x86_64 % 0.00/0.11 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.00/0.11 % Memory : 8046.5625MB % 0.00/0.11 % OS : Linux 6.8.0-71-generic % 0.00/0.11 % CPULimit : 300 % 0.00/0.11 % WCLimit : 300 % 0.00/0.11 % DateTime : Mon Sep 28 15:04:19 UTC 2026 % 0.00/0.11 % CPUTime : % 0.00/0.11 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.09/0.13 Running first-order model finding % 0.09/0.13 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 % 2.86/0.72 % (3441573)Will run a generic schedule for satisfiability detection. % 2.86/0.72 % (3441579)% WARNING: option uhcvi not known. % 2.86/0.72 % (3441579)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1867590111:i=135531:add=off:rawr=on_2998 on theBenchmark for (2998ds/135531Mi) % 2.86/0.72 % (3441584)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3341554129:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2998 on theBenchmark for (2998ds/159Mi) % 2.86/0.72 % (3441582)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1439374487:i=116_2998 on theBenchmark for (2998ds/116Mi) % 2.86/0.72 % (3441581)dis+10_1_sil=32000:sp=arity:random_seed=774904850:i=103:fgj=on_2998 on theBenchmark for (2998ds/103Mi) % 2.86/0.72 % (3441578)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=473145385_2998 on theBenchmark for (2998ds/0Mi) % 2.86/0.72 % (3441580)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2741973694:i=88024:add=on:rawr=on_2998 on theBenchmark for (2998ds/88024Mi) % 2.86/0.72 % (3441583)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=4241479248:i=131_2998 on theBenchmark for (2998ds/131Mi) % 2.86/0.72 % (3441581)Instruction limit reached! % 2.86/0.72 % (3441581)------------------------------ % 2.86/0.72 % (3441581)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 2.86/0.72 % (3441581)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 2.86/0.72 % (3441581)CaDiCaL version: 2.1.3 % 2.86/0.72 % (3441581)Termination reason: Instruction limit % 2.86/0.72 % (3441581)Termination phase: Property scanning % 2.86/0.72 % (3441581)Time elapsed: 0.022 s % 2.86/0.72 % (3441581)Peak memory usage: 10 MB % 2.86/0.72 % (3441581)Instructions burned: 106 (million) % 2.86/0.72 % (3441582)Instruction limit reached! % 2.86/0.72 % (3441582)------------------------------ % 2.86/0.72 % (3441582)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 2.86/0.72 % (3441582)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 2.86/0.72 % (3441582)CaDiCaL version: 2.1.3 % 2.86/0.72 % (3441582)Termination reason: Instruction limit % 2.86/0.72 % (3441582)Termination phase: Property scanning % 2.86/0.72 % (3441582)Time elapsed: 0.025 s % 2.86/0.72 % (3441582)Peak memory usage: 10 MB % 2.86/0.72 % (3441582)Instructions burned: 119 (million) % 2.86/0.72 % (3441593)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3913990310:i=714:nm=2_2998 on theBenchmark for (2998ds/714Mi) % 2.86/0.72 % (3441584)Instruction limit reached! % 2.86/0.72 % (3441584)------------------------------ % 2.86/0.72 % (3441584)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 2.86/0.72 % (3441584)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 2.86/0.72 % (3441584)CaDiCaL version: 2.1.3 % 2.86/0.72 % (3441584)Termination reason: Instruction limit % 2.86/0.72 % (3441584)Termination phase: Property scanning % 2.86/0.72 % (3441584)Time elapsed: 0.033 s % 2.86/0.72 % (3441584)Peak memory usage: 10 MB % 2.86/0.72 % (3441584)Instructions burned: 161 (million) % 2.86/0.72 % (3441594)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1631105420:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi) % 2.86/0.72 % (3441583)Instruction limit reached! % 2.86/0.72 % (3441583)------------------------------ % 2.86/0.72 % (3441583)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 2.86/0.72 % (3441583)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 2.86/0.72 % (3441583)CaDiCaL version: 2.1.3 % 2.86/0.72 % (3441583)Termination reason: Instruction limit % 2.86/0.72 % (3441583)Termination phase: Property scanning % 2.86/0.72 % (3441583)Time elapsed: 0.039 s % 2.86/0.72 % (3441583)Peak memory usage: 10 MB % 2.86/0.72 % (3441583)Instructions burned: 133 (million) % 2.86/0.72 % (3441596)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=2824027415:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi) % 2.86/0.72 % (3441598)ott-21_1_sil=16000:fs=off:random_seed=3726729677:i=180:av=off:fsr=off_2997 on theBenchmark for (2997ds/180Mi) % 2.86/0.72 % (3441594)Instruction limit reached! % 2.86/0.72 % (3441594)------------------------------ % 2.86/0.72 % (3441594)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 2.86/0.72 % (3441594)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.39/1.09 % (3441594)CaDiCaL version: 2.1.3 % 5.39/1.09 % (3441594)Termination reason: Instruction limit % 5.39/1.09 % (3441594)Termination phase: Property scanning % 5.39/1.09 % (3441594)Time elapsed: 0.027 s % 5.39/1.09 % (3441594)Peak memory usage: 10 MB % 5.39/1.09 % (3441594)Instructions burned: 133 (million) % 5.39/1.09 % (3441601)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1118679057:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi) % 5.39/1.09 % (3441578)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 5.39/1.09 % (3441578)Terminated due to inappropriate strategy. % 5.39/1.09 % (3441578)------------------------------ % 5.39/1.09 % (3441578)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.39/1.09 % (3441578)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.39/1.09 % (3441578)CaDiCaL version: 2.1.3 % 5.39/1.09 % (3441578)Termination reason: Inappropriate % 5.39/1.09 % (3441578)Time elapsed: 0.093 s % 5.39/1.09 % (3441578)Peak memory usage: 11 MB % 5.39/1.09 % (3441578)Instructions burned: 467 (million) % 5.39/1.09 % (3441578)------------------------------ % 5.39/1.09 % (3441578)------------------------------ % 5.39/1.09 % (3441603)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3339013272:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi) % 5.39/1.09 % (3441598)Instruction limit reached! % 5.39/1.09 % (3441598)------------------------------ % 5.39/1.09 % (3441598)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.39/1.09 % (3441598)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.39/1.09 % (3441598)CaDiCaL version: 2.1.3 % 5.39/1.09 % (3441598)Termination reason: Instruction limit % 5.39/1.09 % (3441598)Termination phase: Property scanning % 5.39/1.09 % (3441598)Time elapsed: 0.052 s % 5.39/1.09 % (3441598)Peak memory usage: 10 MB % 5.39/1.09 % (3441598)Instructions burned: 183 (million) % 5.39/1.09 % (3441605)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1064964533:i=1179_2997 on theBenchmark for (2997ds/1179Mi) % 5.39/1.09 % (3441593)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 5.39/1.09 % (3441593)Terminated due to inappropriate strategy. % 5.39/1.09 % (3441593)------------------------------ % 5.39/1.09 % (3441593)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.39/1.09 % (3441593)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.39/1.09 % (3441593)CaDiCaL version: 2.1.3 % 5.39/1.09 % (3441593)Termination reason: Inappropriate % 5.39/1.09 % (3441593)Time elapsed: 0.093 s % 5.39/1.09 % (3441593)Peak memory usage: 11 MB % 5.39/1.09 % (3441593)Instructions burned: 467 (million) % 5.39/1.09 % (3441593)------------------------------ % 5.39/1.09 % (3441593)------------------------------ % 5.39/1.09 % (3441607)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1261779591:i=889:ins=1_2997 on theBenchmark for (2997ds/889Mi) % 5.39/1.09 % (3441601)Instruction limit reached! % 5.39/1.09 % (3441601)------------------------------ % 5.39/1.09 % (3441601)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.39/1.09 % (3441601)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.39/1.09 % (3441601)CaDiCaL version: 2.1.3 % 5.39/1.09 % (3441601)Termination reason: Instruction limit % 5.39/1.09 % (3441601)Termination phase: Saturation % 5.39/1.09 % (3441601)Time elapsed: 0.097 s % 5.39/1.09 % (3441601)Peak memory usage: 12 MB % 5.39/1.09 % (3441601)Instructions burned: 480 (million) % 5.39/1.09 % (3441603)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 5.39/1.09 % (3441603)Terminated due to inappropriate strategy. % 5.39/1.09 % (3441603)------------------------------ % 5.39/1.09 % (3441603)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.39/1.09 % (3441603)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.39/1.09 % (3441603)CaDiCaL version: 2.1.3 % 5.39/1.09 % (3441603)Termination reason: Inappropriate % 5.39/1.09 % (3441603)Time elapsed: 0.072 s % 5.39/1.09 % (3441603)Peak memory usage: 11 MB % 5.39/1.09 % (3441603)Instructions burned: 354 (million) % 5.39/1.09 % (3441603)------------------------------ % 5.39/1.09 % (3441603)------------------------------ % 5.39/1.09 % (3441609)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=2853709996: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) % 14.59/2.43 % (3441596)Instruction limit reached! % 14.59/2.43 % (3441596)------------------------------ % 14.59/2.43 % (3441596)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 14.59/2.43 % (3441596)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.59/2.43 % (3441596)CaDiCaL version: 2.1.3 % 14.59/2.43 % (3441596)Termination reason: Instruction limit % 14.59/2.43 % (3441596)Termination phase: Saturation % 14.59/2.43 % (3441596)Time elapsed: 0.139 s % 14.59/2.43 % (3441596)Peak memory usage: 13 MB % 14.59/2.43 % (3441596)Instructions burned: 684 (million) % 14.59/2.43 % (3441610)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=772767488:i=879:kws=inv_precedence:fsr=off_2996 on theBenchmark for (2996ds/879Mi) % 14.59/2.43 % (3441612)fmb+10_1_sil=64000:random_seed=882520931:i=22061:nm=2:gsp=on_2996 on theBenchmark for (2996ds/22061Mi) % 14.59/2.43 % (3441607)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 14.59/2.43 % (3441607)Terminated due to inappropriate strategy. % 14.59/2.43 % (3441607)------------------------------ % 14.59/2.43 % (3441607)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 14.59/2.43 % (3441607)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.59/2.43 % (3441607)CaDiCaL version: 2.1.3 % 14.59/2.43 % (3441607)Termination reason: Inappropriate % 14.59/2.43 % (3441607)Time elapsed: 0.073 s % 14.59/2.43 % (3441607)Peak memory usage: 11 MB % 14.59/2.43 % (3441607)Instructions burned: 354 (million) % 14.59/2.43 % (3441607)------------------------------ % 14.59/2.43 % (3441607)------------------------------ % 14.59/2.43 % (3441615)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=4088056295:i=9515:nm=5_2996 on theBenchmark for (2996ds/9515Mi) % 14.59/2.43 % (3441612)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 14.59/2.43 % (3441612)Terminated due to inappropriate strategy. % 14.59/2.43 % (3441612)------------------------------ % 14.59/2.43 % (3441612)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 14.59/2.43 % (3441612)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.59/2.43 % (3441612)CaDiCaL version: 2.1.3 % 14.59/2.43 % (3441612)Termination reason: Inappropriate % 14.59/2.43 % (3441612)Time elapsed: 0.100 s % 14.59/2.43 % (3441612)Peak memory usage: 11 MB % 14.59/2.43 % (3441612)Instructions burned: 467 (million) % 14.59/2.43 % (3441612)------------------------------ % 14.59/2.43 % (3441612)------------------------------ % 14.59/2.43 % (3441624)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3193069547:fmbsr=1.7:i=920_2995 on theBenchmark for (2995ds/920Mi) % 14.59/2.43 % (3441615)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 14.59/2.43 % (3441615)Terminated due to inappropriate strategy. % 14.59/2.43 % (3441615)------------------------------ % 14.59/2.43 % (3441615)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 14.59/2.43 % (3441615)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.59/2.43 % (3441615)CaDiCaL version: 2.1.3 % 14.59/2.43 % (3441615)Termination reason: Inappropriate % 14.59/2.43 % (3441615)Time elapsed: 0.126 s % 14.59/2.43 % (3441615)Peak memory usage: 11 MB % 14.59/2.43 % (3441615)Instructions burned: 467 (million) % 14.59/2.43 % (3441609)Instruction limit reached! % 14.59/2.43 % (3441609)------------------------------ % 14.59/2.43 % (3441609)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 14.59/2.43 % (3441609)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.59/2.43 % (3441609)CaDiCaL version: 2.1.3 % 14.59/2.43 % (3441609)Termination reason: Instruction limit % 14.59/2.43 % (3441609)Termination phase: Saturation % 14.59/2.43 % (3441609)Time elapsed: 0.169 s % 14.59/2.43 % (3441609)Peak memory usage: 13 MB % 14.59/2.43 % (3441609)Instructions burned: 694 (million) % 14.59/2.43 % (3441615)------------------------------ % 14.59/2.43 % (3441615)------------------------------ % 14.59/2.43 % (3441626)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1453964979:i=5131_2994 on theBenchmark for (2994ds/5131Mi) % 14.59/2.43 % (3441627)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1256331381:i=1472:ins=7:fdi=8:gsp=on_2994 on theBenchmark for (2994ds/1472Mi) % 14.59/2.43 % (3441610)Instruction limit reached! % 14.59/2.43 % (3441610)------------------------------ % 14.59/2.43 % (3441610)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 16.00/2.83 % (3441610)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.00/2.83 % (3441610)CaDiCaL version: 2.1.3 % 16.00/2.83 % (3441610)Termination reason: Instruction limit % 16.00/2.83 % (3441610)Termination phase: Saturation % 16.00/2.83 % (3441610)Time elapsed: 0.234 s % 16.00/2.83 % (3441610)Peak memory usage: 15 MB % 16.00/2.83 % (3441610)Instructions burned: 880 (million) % 16.00/2.83 % (3441630)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=254090450:i=6324_2994 on theBenchmark for (2994ds/6324Mi) % 16.00/2.83 % (3441624)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 16.00/2.83 % (3441624)Terminated due to inappropriate strategy. % 16.00/2.83 % (3441624)------------------------------ % 16.00/2.83 % (3441624)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 16.00/2.83 % (3441624)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.00/2.83 % (3441624)CaDiCaL version: 2.1.3 % 16.00/2.83 % (3441624)Termination reason: Inappropriate % 16.00/2.83 % (3441624)Time elapsed: 0.165 s % 16.00/2.83 % (3441624)Peak memory usage: 11 MB % 16.00/2.83 % (3441624)Instructions burned: 467 (million) % 16.00/2.83 % (3441624)------------------------------ % 16.00/2.83 % (3441624)------------------------------ % 16.00/2.83 % (3441644)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=3011931798:fmbsr=2.30978:i=2174_2993 on theBenchmark for (2993ds/2174Mi) % 16.00/2.83 % (3441605)Instruction limit reached! % 16.00/2.83 % (3441605)------------------------------ % 16.00/2.83 % (3441605)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 16.00/2.83 % (3441605)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.00/2.83 % (3441605)CaDiCaL version: 2.1.3 % 16.00/2.83 % (3441605)Termination reason: Instruction limit % 16.00/2.83 % (3441605)Termination phase: Saturation % 16.00/2.83 % (3441605)Time elapsed: 0.395 s % 16.00/2.83 % (3441605)Peak memory usage: 18 MB % 16.00/2.83 % (3441605)Instructions burned: 1180 (million) % 16.00/2.83 % (3441647)ott-2_1_sil=16000:newcnf=on:random_seed=3728951321:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2993 on theBenchmark for (2993ds/869Mi) % 16.00/2.83 % (3441630)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 16.00/2.83 % (3441630)Terminated due to inappropriate strategy. % 16.00/2.83 % (3441630)------------------------------ % 16.00/2.83 % (3441630)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 16.00/2.83 % (3441630)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.00/2.83 % (3441630)CaDiCaL version: 2.1.3 % 16.00/2.83 % (3441630)Termination reason: Inappropriate % 16.00/2.83 % (3441630)Time elapsed: 0.156 s % 16.00/2.83 % (3441630)Peak memory usage: 11 MB % 16.00/2.83 % (3441630)Instructions burned: 467 (million) % 16.00/2.83 % (3441630)------------------------------ % 16.00/2.83 % (3441630)------------------------------ % 16.00/2.83 % (3441651)ott+10_1_sil=32000:tgt=ground:random_seed=3326633870:i=5114:av=off_2992 on theBenchmark for (2992ds/5114Mi) % 16.00/2.83 % (3441644)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 16.00/2.83 % (3441644)Terminated due to inappropriate strategy. % 16.00/2.83 % (3441644)------------------------------ % 16.00/2.83 % (3441644)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 16.00/2.83 % (3441644)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.00/2.83 % (3441644)CaDiCaL version: 2.1.3 % 16.00/2.83 % (3441644)Termination reason: Inappropriate % 16.00/2.83 % (3441644)Time elapsed: 0.155 s % 16.00/2.83 % (3441644)Peak memory usage: 11 MB % 16.00/2.83 % (3441644)Instructions burned: 467 (million) % 16.00/2.83 % (3441644)------------------------------ % 16.00/2.83 % (3441644)------------------------------ % 16.00/2.83 % (3441663)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=3509695139:i=54282_2991 on theBenchmark for (2991ds/54282Mi) % 16.00/2.83 % (3441647)Instruction limit reached! % 16.00/2.83 % (3441647)------------------------------ % 16.00/2.83 % (3441647)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 16.00/2.83 % (3441647)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.00/2.83 % (3441647)CaDiCaL version: 2.1.3 % 16.00/2.83 % (3441647)Termination reason: Instruction limit % 16.00/2.83 % (3441647)Termination phase: Saturation % 16.00/2.83 % (3441647)Time elapsed: 0.252 s % 16.00/2.83 % (3441647)Peak memory usage: 17 MB % 16.00/2.83 % (3441647)Instructions burned: 869 (million) % 70.05/10.26 % (3441669)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=444149190:i=3512:aac=none_2990 on theBenchmark for (2990ds/3512Mi) % 70.05/10.26 % (3441663)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 70.05/10.26 % (3441663)Terminated due to inappropriate strategy. % 70.05/10.26 % (3441663)------------------------------ % 70.05/10.26 % (3441663)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 70.05/10.26 % (3441663)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 70.05/10.26 % (3441663)CaDiCaL version: 2.1.3 % 70.05/10.26 % (3441663)Termination reason: Inappropriate % 70.05/10.26 % (3441663)Time elapsed: 0.137 s % 70.05/10.26 % (3441663)Peak memory usage: 11 MB % 70.05/10.26 % (3441663)Instructions burned: 467 (million) % 70.05/10.26 % (3441663)------------------------------ % 70.05/10.26 % (3441663)------------------------------ % 70.05/10.26 % (3441676)dis+21_1_sil=32000:sas=cadical:random_seed=2071870380:i=3773:amm=off_2990 on theBenchmark for (2990ds/3773Mi) % 70.05/10.26 % (3441627)Instruction limit reached! % 70.05/10.26 % (3441627)------------------------------ % 70.05/10.26 % (3441627)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 70.05/10.26 % (3441627)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 70.05/10.26 % (3441627)CaDiCaL version: 2.1.3 % 70.05/10.26 % (3441627)Termination reason: Instruction limit % 70.05/10.26 % (3441627)Termination phase: Saturation % 70.05/10.26 % (3441627)Time elapsed: 0.531 s % 70.05/10.26 % (3441627)Peak memory usage: 18 MB % 70.05/10.26 % (3441627)Instructions burned: 1474 (million) % 70.05/10.26 % (3441683)ott+11_1_sil=16000:gs=on:random_seed=2819655920:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2989 on theBenchmark for (2989ds/2251Mi) % 70.05/10.26 % (3441683)Instruction limit reached! % 70.05/10.26 % (3441683)------------------------------ % 70.05/10.26 % (3441683)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 70.05/10.26 % (3441683)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 70.05/10.26 % (3441683)CaDiCaL version: 2.1.3 % 70.05/10.26 % (3441683)Termination reason: Instruction limit % 70.05/10.26 % (3441683)Termination phase: Saturation % 70.05/10.26 % (3441683)Time elapsed: 0.606 s % 70.05/10.26 % (3441683)Peak memory usage: 19 MB % 70.05/10.26 % (3441683)Instructions burned: 2256 (million) % 70.05/10.26 % (3441725)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=322479980:fmbsr=1.6:i=67534_2983 on theBenchmark for (2983ds/67534Mi) % 70.05/10.26 % (3441725)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 70.05/10.26 % (3441725)Terminated due to inappropriate strategy. % 70.05/10.26 % (3441725)------------------------------ % 70.05/10.26 % (3441725)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 70.05/10.26 % (3441725)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 70.05/10.26 % (3441725)CaDiCaL version: 2.1.3 % 70.05/10.26 % (3441725)Termination reason: Inappropriate % 70.05/10.26 % (3441725)Time elapsed: 0.156 s % 70.05/10.26 % (3441725)Peak memory usage: 11 MB % 70.05/10.26 % (3441725)Instructions burned: 467 (million) % 70.05/10.26 % (3441725)------------------------------ % 70.05/10.26 % (3441725)------------------------------ % 70.05/10.26 % (3441735)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=3413166099:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2981 on theBenchmark for (2981ds/4591Mi) % 70.05/10.26 % (3441669)Instruction limit reached! % 70.05/10.26 % (3441669)------------------------------ % 70.05/10.26 % (3441669)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 70.05/10.26 % (3441669)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 70.05/10.26 % (3441669)CaDiCaL version: 2.1.3 % 70.05/10.26 % (3441669)Termination reason: Instruction limit % 70.05/10.26 % (3441669)Termination phase: Saturation % 70.05/10.26 % (3441669)Time elapsed: 1.276 s % 70.05/10.26 % (3441669)Peak memory usage: 20 MB % 70.05/10.26 % (3441669)Instructions burned: 3517 (million) % 70.05/10.26 % (3441756)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=2073586260:i=29340_2977 on theBenchmark for (2977ds/29340Mi) % 70.05/10.26 % (3441676)Instruction limit reached! % 70.05/10.26 % (3441676)------------------------------ % 70.05/10.26 % (3441676)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 70.05/10.26 % (3441676)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 91.12/13.28 % (3441676)CaDiCaL version: 2.1.3 % 91.12/13.28 % (3441676)Termination reason: Instruction limit % 91.12/13.28 % (3441676)Termination phase: Saturation % 91.12/13.28 % (3441676)Time elapsed: 1.295 s % 91.12/13.28 % (3441676)Peak memory usage: 19 MB % 91.12/13.28 % (3441676)Instructions burned: 3776 (million) % 91.12/13.28 % (3441651)Instruction limit reached! % 91.12/13.28 % (3441651)------------------------------ % 91.12/13.28 % (3441651)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 91.12/13.28 % (3441651)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 91.12/13.28 % (3441651)CaDiCaL version: 2.1.3 % 91.12/13.28 % (3441651)Termination reason: Instruction limit % 91.12/13.28 % (3441651)Termination phase: Saturation % 91.12/13.28 % (3441651)Time elapsed: 1.535 s % 91.12/13.28 % (3441651)Peak memory usage: 29 MB % 91.12/13.28 % (3441651)Instructions burned: 5116 (million) % 91.12/13.28 % (3441761)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=2248728942:i=5211_2976 on theBenchmark for (2976ds/5211Mi) % 91.12/13.28 % (3441763)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=1122530743:i=5497:nm=2_2976 on theBenchmark for (2976ds/5497Mi) % 91.12/13.28 % (3441626)Instruction limit reached! % 91.12/13.28 % (3441626)------------------------------ % 91.12/13.28 % (3441626)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 91.12/13.28 % (3441626)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 91.12/13.28 % (3441626)CaDiCaL version: 2.1.3 % 91.12/13.28 % (3441626)Termination reason: Instruction limit % 91.12/13.28 % (3441626)Termination phase: Saturation % 91.12/13.28 % (3441626)Time elapsed: 1.832 s % 91.12/13.28 % (3441626)Peak memory usage: 20 MB % 91.12/13.28 % (3441626)Instructions burned: 5132 (million) % 91.12/13.28 % (3441766)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=3493578026:fmbsr=2:i=46332_2976 on theBenchmark for (2976ds/46332Mi) % 91.12/13.28 % (3441763)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 91.12/13.28 % (3441763)Terminated due to inappropriate strategy. % 91.12/13.28 % (3441763)------------------------------ % 91.12/13.28 % (3441763)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 91.12/13.28 % (3441763)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 91.12/13.28 % (3441763)CaDiCaL version: 2.1.3 % 91.12/13.28 % (3441763)Termination reason: Inappropriate % 91.12/13.28 % (3441763)Time elapsed: 0.164 s % 91.12/13.28 % (3441763)Peak memory usage: 11 MB % 91.12/13.28 % (3441763)Instructions burned: 467 (million) % 91.12/13.28 % (3441763)------------------------------ % 91.12/13.28 % (3441763)------------------------------ % 91.12/13.28 % (3441775)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=3849838779:i=14071_2975 on theBenchmark for (2975ds/14071Mi) % 91.12/13.28 % (3441766)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 91.12/13.28 % (3441766)Terminated due to inappropriate strategy. % 91.12/13.28 % (3441766)------------------------------ % 91.12/13.28 % (3441766)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 91.12/13.28 % (3441766)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 91.12/13.28 % (3441766)CaDiCaL version: 2.1.3 % 91.12/13.28 % (3441766)Termination reason: Inappropriate % 91.12/13.28 % (3441766)Time elapsed: 0.176 s % 91.12/13.28 % (3441766)Peak memory usage: 11 MB % 91.12/13.28 % (3441766)Instructions burned: 467 (million) % 91.12/13.28 % (3441766)------------------------------ % 91.12/13.28 % (3441766)------------------------------ % 91.12/13.28 % (3441779)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=225775731:i=22565:add=on:rawr=on_2974 on theBenchmark for (2974ds/22565Mi) % 91.12/13.28 % (3441775)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 91.12/13.28 % (3441775)Terminated due to inappropriate strategy. % 91.12/13.28 % (3441775)------------------------------ % 91.12/13.28 % (3441775)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 91.12/13.28 % (3441775)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 91.12/13.28 % (3441775)CaDiCaL version: 2.1.3 % 91.12/13.28 % (3441775)Termination reason: Inappropriate % 91.12/13.28 % (3441775)Time elapsed: 0.162 s % 91.12/13.28 % (3441775)Peak memory usage: 11 MB % 91.12/13.28 % (3441775)Instructions burned: 467 (million) % 91.12/13.28 % (3441775)------------------------------ % 91.12/13.28 % (3441775)------------------------------ % 91.12/13.28 % (3441783)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=3444617835:i=8173:av=off_2973 on theBenchmark for (2973ds/8173Mi) % 98.27/14.20 % (3441735)Instruction limit reached! % 98.27/14.20 % (3441735)------------------------------ % 98.27/14.20 % (3441735)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 98.27/14.20 % (3441735)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 98.27/14.20 % (3441735)CaDiCaL version: 2.1.3 % 98.27/14.20 % (3441735)Termination reason: Instruction limit % 98.27/14.20 % (3441735)Termination phase: Saturation % 98.27/14.20 % (3441735)Time elapsed: 1.777 s % 98.27/14.20 % (3441735)Peak memory usage: 18 MB % 98.27/14.20 % (3441735)Instructions burned: 4591 (million) % 98.27/14.20 % (3441821)dis+10_16:1_sil=16000:random_seed=3824814042:i=9155:fsr=off_2963 on theBenchmark for (2963ds/9155Mi) % 98.27/14.20 % (3441761)Instruction limit reached! % 98.27/14.20 % (3441761)------------------------------ % 98.27/14.20 % (3441761)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 98.27/14.20 % (3441761)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 98.27/14.20 % (3441761)CaDiCaL version: 2.1.3 % 98.27/14.20 % (3441761)Termination reason: Instruction limit % 98.27/14.20 % (3441761)Termination phase: Saturation % 98.27/14.20 % (3441761)Time elapsed: 1.911 s % 98.27/14.20 % (3441761)Peak memory usage: 21 MB % 98.27/14.20 % (3441761)Instructions burned: 5214 (million) % 98.27/14.20 % (3441840)ott-3_8_sil=64000:random_seed=2062564312:i=20139:bs=on_2957 on theBenchmark for (2957ds/20139Mi) % 98.27/14.20 % (3441783)Instruction limit reached! % 98.27/14.20 % (3441783)------------------------------ % 98.27/14.20 % (3441783)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 98.27/14.20 % (3441783)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 98.27/14.20 % (3441783)CaDiCaL version: 2.1.3 % 98.27/14.20 % (3441783)Termination reason: Instruction limit % 98.27/14.20 % (3441783)Termination phase: Saturation % 98.27/14.20 % (3441783)Time elapsed: 2.594 s % 98.27/14.20 % (3441783)Peak memory usage: 29 MB % 98.27/14.20 % (3441783)Instructions burned: 8175 (million) % 98.27/14.20 % (3441867)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=131810450:fmbsr=2:i=32576_2947 on theBenchmark for (2947ds/32576Mi) % 98.27/14.20 % (3441867)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 98.27/14.20 % (3441867)Terminated due to inappropriate strategy. % 98.27/14.20 % (3441867)------------------------------ % 98.27/14.20 % (3441867)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 98.27/14.20 % (3441867)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 98.27/14.20 % (3441867)CaDiCaL version: 2.1.3 % 98.27/14.20 % (3441867)Termination reason: Inappropriate % 98.27/14.20 % (3441867)Time elapsed: 0.158 s % 98.27/14.20 % (3441867)Peak memory usage: 11 MB % 98.27/14.20 % (3441867)Instructions burned: 467 (million) % 98.27/14.20 % (3441867)------------------------------ % 98.27/14.20 % (3441867)------------------------------ % 98.27/14.20 % (3441871)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=3484445881:i=11404_2945 on theBenchmark for (2945ds/11404Mi) % 98.27/14.20 % (3441821)Instruction limit reached! % 98.27/14.20 % (3441821)------------------------------ % 98.27/14.20 % (3441821)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 98.27/14.20 % (3441821)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 98.27/14.20 % (3441821)CaDiCaL version: 2.1.3 % 98.27/14.20 % (3441821)Termination reason: Instruction limit % 98.27/14.20 % (3441821)Termination phase: Saturation % 98.27/14.20 % (3441821)Time elapsed: 3.340 s % 98.27/14.20 % (3441821)Peak memory usage: 22 MB % 98.27/14.20 % (3441821)Instructions burned: 9157 (million) % 98.27/14.20 % (3441888)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=1317016141:i=14134_2929 on theBenchmark for (2929ds/14134Mi) % 98.27/14.20 % (3441871)Instruction limit reached! % 98.27/14.20 % (3441871)------------------------------ % 98.27/14.20 % (3441871)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 98.27/14.20 % (3441871)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 98.27/14.20 % (3441871)CaDiCaL version: 2.1.3 % 98.27/14.20 % (3441871)Termination reason: Instruction limit % 98.27/14.20 % (3441871)Termination phase: Saturation % 98.27/14.20 % (3441871)Time elapsed: 3.968 s % 98.27/14.20 % (3441871)Peak memory usage: 29 MB % 98.27/14.20 % (3441871)Instructions burned: 11406 (million) % 98.27/14.20 % (3441909)dis+33_16_sil=32000:sac=on:random_seed=1506028402:i=15851:nm=0_2905 on theBenchmark for (2905ds/15851Mi) % 98.27/14.20 % (3441779)Instruction limit reached! % 98.27/14.20 % (3441779)------------------------------ % 124.34/17.99 % (3441779)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 124.34/17.99 % (3441779)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 124.34/17.99 % (3441779)CaDiCaL version: 2.1.3 % 124.34/17.99 % (3441779)Termination reason: Instruction limit % 124.34/17.99 % (3441779)Termination phase: Saturation % 124.34/17.99 % (3441779)Time elapsed: 7.551 s % 124.34/17.99 % (3441779)Peak memory usage: 18 MB % 124.34/17.99 % (3441779)Instructions burned: 22568 (million) % 124.34/17.99 % (3441913)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=293813966:avsq=on:i=17627:add=on:amm=off_2898 on theBenchmark for (2898ds/17627Mi) % 124.34/17.99 % (3441840)Instruction limit reached! % 124.34/17.99 % (3441840)------------------------------ % 124.34/17.99 % (3441840)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 124.34/17.99 % (3441840)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 124.34/17.99 % (3441840)CaDiCaL version: 2.1.3 % 124.34/17.99 % (3441840)Termination reason: Instruction limit % 124.34/17.99 % (3441840)Termination phase: Saturation % 124.34/17.99 % (3441840)Time elapsed: 6.569 s % 124.34/17.99 % (3441840)Peak memory usage: 31 MB % 124.34/17.99 % (3441840)Instructions burned: 20139 (million) % 124.34/17.99 % (3441919)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=1136420542:s2a=on:i=53295_2891 on theBenchmark for (2891ds/53295Mi) % 124.34/17.99 % (3441888)Instruction limit reached! % 124.34/17.99 % (3441888)------------------------------ % 124.34/17.99 % (3441888)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 124.34/17.99 % (3441888)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 124.34/17.99 % (3441888)CaDiCaL version: 2.1.3 % 124.34/17.99 % (3441888)Termination reason: Instruction limit % 124.34/17.99 % (3441888)Termination phase: Saturation % 124.34/17.99 % (3441888)Time elapsed: 5.110 s % 124.34/17.99 % (3441888)Peak memory usage: 29 MB % 124.34/17.99 % (3441888)Instructions burned: 14134 (million) % 124.34/17.99 % (3441930)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=1903913701:i=26857:ins=20_2878 on theBenchmark for (2878ds/26857Mi) % 124.34/17.99 % (3441930)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 124.34/17.99 % (3441930)Terminated due to inappropriate strategy. % 124.34/17.99 % (3441930)------------------------------ % 124.34/17.99 % (3441930)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 124.34/17.99 % (3441930)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 124.34/17.99 % (3441930)CaDiCaL version: 2.1.3 % 124.34/17.99 % (3441930)Termination reason: Inappropriate % 124.34/17.99 % (3441930)Time elapsed: 0.106 s % 124.34/17.99 % (3441930)Peak memory usage: 11 MB % 124.34/17.99 % (3441930)Instructions burned: 467 (million) % 124.34/17.99 % (3441930)------------------------------ % 124.34/17.99 % (3441930)------------------------------ % 124.34/17.99 % (3441933)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=453072620:i=28120:bs=on:fsr=off_2877 on theBenchmark for (2877ds/28120Mi) % 124.34/17.99 % (3441756)Instruction limit reached! % 124.34/17.99 % (3441756)------------------------------ % 124.34/17.99 % (3441756)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 124.34/17.99 % (3441756)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 124.34/17.99 % (3441756)CaDiCaL version: 2.1.3 % 124.34/17.99 % (3441756)Termination reason: Instruction limit % 124.34/17.99 % (3441756)Termination phase: Saturation % 124.34/17.99 % (3441756)Time elapsed: 10.695 s % 124.34/17.99 % (3441756)Peak memory usage: 17 MB % 124.34/17.99 % (3441756)Instructions burned: 29340 (million) % 124.34/17.99 % (3441938)fmb+10_1_sil=256000:fmbss=7:random_seed=2733471293:fmbsr=1.6:i=182295_2870 on theBenchmark for (2870ds/182295Mi) % 124.34/17.99 % (3441938)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 124.34/17.99 % (3441938)Terminated due to inappropriate strategy. % 124.34/17.99 % (3441938)------------------------------ % 124.34/17.99 % (3441938)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 124.34/17.99 % (3441938)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 124.34/17.99 % (3441938)CaDiCaL version: 2.1.3 % 124.34/17.99 % (3441938)Termination reason: Inappropriate % 124.34/17.99 % (3441938)Time elapsed: 0.182 s % 124.34/17.99 % (3441938)Peak memory usage: 11 MB % 124.34/17.99 % (3441938)Instructions burned: 467 (million) % 124.34/17.99 % (3441938)------------------------------ % 124.34/17.99 % (3441938)------------------------------ % 132.84/19.19 % (3441942)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=374073552:i=44625:gsp=on_2868 on theBenchmark for (2868ds/44625Mi) % 132.84/19.19 % (3441942)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 132.84/19.19 % (3441942)Terminated due to inappropriate strategy. % 132.84/19.19 % (3441942)------------------------------ % 132.84/19.19 % (3441942)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 132.84/19.19 % (3441942)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 132.84/19.19 % (3441942)CaDiCaL version: 2.1.3 % 132.84/19.19 % (3441942)Termination reason: Inappropriate % 132.84/19.19 % (3441942)Time elapsed: 0.197 s % 132.84/19.19 % (3441942)Peak memory usage: 11 MB % 132.84/19.19 % (3441942)Instructions burned: 467 (million) % 132.84/19.19 % (3441942)------------------------------ % 132.84/19.19 % (3441942)------------------------------ % 132.84/19.19 % (3441946)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=252468891:i=160505_2866 on theBenchmark for (2866ds/160505Mi) % 132.84/19.19 % (3441946)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 132.84/19.19 % (3441946)Terminated due to inappropriate strategy. % 132.84/19.19 % (3441946)------------------------------ % 132.84/19.19 % (3441946)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 132.84/19.19 % (3441946)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 132.84/19.19 % (3441946)CaDiCaL version: 2.1.3 % 132.84/19.19 % (3441946)Termination reason: Inappropriate % 132.84/19.19 % (3441946)Time elapsed: 0.201 s % 132.84/19.19 % (3441946)Peak memory usage: 11 MB % 132.84/19.19 % (3441946)Instructions burned: 467 (million) % 132.84/19.19 % (3441946)------------------------------ % 132.84/19.19 % (3441946)------------------------------ % 132.84/19.19 % (3441950)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=1731816864:fmbsr=1.3:i=225729_2864 on theBenchmark for (2864ds/225729Mi) % 132.84/19.19 % (3441950)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 132.84/19.19 % (3441950)Terminated due to inappropriate strategy. % 132.84/19.19 % (3441950)------------------------------ % 132.84/19.19 % (3441950)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 132.84/19.19 % (3441950)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 132.84/19.19 % (3441950)CaDiCaL version: 2.1.3 % 132.84/19.19 % (3441950)Termination reason: Inappropriate % 132.84/19.19 % (3441950)Time elapsed: 0.098 s % 132.84/19.19 % (3441950)Peak memory usage: 11 MB % 132.84/19.19 % (3441950)Instructions burned: 467 (million) % 132.84/19.19 % (3441950)------------------------------ % 132.84/19.19 % (3441950)------------------------------ % 132.84/19.19 % (3441952)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=2617058217:fmbsr=2:i=185024:ins=7_2863 on theBenchmark for (2863ds/185024Mi) % 132.84/19.19 % (3441952)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 132.84/19.19 % (3441952)Terminated due to inappropriate strategy. % 132.84/19.19 % (3441952)------------------------------ % 132.84/19.19 % (3441952)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 132.84/19.19 % (3441952)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 132.84/19.19 % (3441952)CaDiCaL version: 2.1.3 % 132.84/19.19 % (3441952)Termination reason: Inappropriate % 132.84/19.19 % (3441952)Time elapsed: 0.184 s % 132.84/19.19 % (3441952)Peak memory usage: 11 MB % 132.84/19.19 % (3441952)Instructions burned: 467 (million) % 132.84/19.19 % (3441952)------------------------------ % 132.84/19.19 % (3441952)------------------------------ % 132.84/19.19 % (3441956)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=1904259472:rtra=on_2861 on theBenchmark for (2861ds/0Mi) % 132.84/19.19 % (3441956)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 132.84/19.19 % (3441956)Terminated due to inappropriate strategy. % 132.84/19.19 % (3441956)------------------------------ % 132.84/19.19 % (3441956)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 132.84/19.19 % (3441956)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 132.84/19.19 % (3441956)CaDiCaL version: 2.1.3 % 132.84/19.19 % (3441956)Termination reason: Inappropriate % 132.84/19.19 % (3441956)Time elapsed: 0.151 s % 132.84/19.19 % (3441956)Peak memory usage: 11 MB % 132.84/19.19 % (3441956)Instructions burned: 468 (million) % 132.84/19.19 % (3441956)------------------------------ % 132.84/19.19 % (3441956)------------------------------ % 132.84/19.19 % (3441958)% WARNING: option uhcvi not known. % 132.84/19.19 % (3441958)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=216485229:i=271062:add=off:rtra=on:rawr=on_2859 on theBenchmark for (2859ds/271062Mi) % 149.00/21.49 % (3441909)Instruction limit reached! % 149.00/21.49 % (3441909)------------------------------ % 149.00/21.49 % (3441909)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 149.00/21.49 % (3441909)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 149.00/21.49 % (3441909)CaDiCaL version: 2.1.3 % 149.00/21.49 % (3441909)Termination reason: Instruction limit % 149.00/21.49 % (3441909)Termination phase: Saturation % 149.00/21.49 % (3441909)Time elapsed: 6.376 s % 149.00/21.49 % (3441909)Peak memory usage: 27 MB % 149.00/21.49 % (3441909)Instructions burned: 15851 (million) % 149.00/21.49 % (3441964)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2974234931:i=176048:add=on:rtra=on:rawr=on_2841 on theBenchmark for (2841ds/176048Mi) % 149.00/21.49 % (3441913)Instruction limit reached! % 149.00/21.49 % (3441913)------------------------------ % 149.00/21.49 % (3441913)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 149.00/21.49 % (3441913)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 149.00/21.49 % (3441913)CaDiCaL version: 2.1.3 % 149.00/21.49 % (3441913)Termination reason: Instruction limit % 149.00/21.49 % (3441913)Termination phase: Saturation % 149.00/21.49 % (3441913)Time elapsed: 7.336 s % 149.00/21.49 % (3441913)Peak memory usage: 93 MB % 149.00/21.49 % (3441913)Instructions burned: 17627 (million) % 149.00/21.49 % (3441969)dis+10_1_sil=32000:si=on:sp=arity:random_seed=173665971:i=206:fgj=on:rtra=on_2825 on theBenchmark for (2825ds/206Mi) % 149.00/21.49 % (3441969)Instruction limit reached! % 149.00/21.49 % (3441969)------------------------------ % 149.00/21.49 % (3441969)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 149.00/21.49 % (3441969)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 149.00/21.49 % (3441969)CaDiCaL version: 2.1.3 % 149.00/21.49 % (3441969)Termination reason: Instruction limit % 149.00/21.49 % (3441969)Termination phase: Property scanning % 149.00/21.49 % (3441969)Time elapsed: 0.048 s % 149.00/21.49 % (3441969)Peak memory usage: 11 MB % 149.00/21.49 % (3441969)Instructions burned: 206 (million) % 149.00/21.49 % (3441971)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=460237633:i=232:rtra=on_2824 on theBenchmark for (2824ds/232Mi) % 149.00/21.49 % (3441971)Instruction limit reached! % 149.00/21.49 % (3441971)------------------------------ % 149.00/21.49 % (3441971)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 149.00/21.49 % (3441971)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 149.00/21.49 % (3441971)CaDiCaL version: 2.1.3 % 149.00/21.49 % (3441971)Termination reason: Instruction limit % 149.00/21.49 % (3441971)Termination phase: Property scanning % 149.00/21.49 % (3441971)Time elapsed: 0.054 s % 149.00/21.49 % (3441971)Peak memory usage: 11 MB % 149.00/21.49 % (3441971)Instructions burned: 232 (million) % 149.00/21.49 % (3441973)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=1991364319:i=262:rtra=on_2823 on theBenchmark for (2823ds/262Mi) % 149.00/21.49 % (3441973)Instruction limit reached! % 149.00/21.49 % (3441973)------------------------------ % 149.00/21.49 % (3441973)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 149.00/21.49 % (3441973)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 149.00/21.49 % (3441973)CaDiCaL version: 2.1.3 % 149.00/21.49 % (3441973)Termination reason: Instruction limit % 149.00/21.49 % (3441973)Termination phase: Property scanning % 149.00/21.49 % (3441973)Time elapsed: 0.062 s % 149.00/21.49 % (3441973)Peak memory usage: 11 MB % 149.00/21.49 % (3441973)Instructions burned: 263 (million) % 149.00/21.49 % (3441975)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=4287039031:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2823 on theBenchmark for (2823ds/318Mi) % 149.00/21.49 % (3441975)Instruction limit reached! % 149.00/21.49 % (3441975)------------------------------ % 149.00/21.49 % (3441975)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 149.00/21.49 % (3441975)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 149.00/21.49 % (3441975)CaDiCaL version: 2.1.3 % 149.00/21.49 % (3441975)Termination reason: Instruction limit % 149.00/21.49 % (3441975)Termination phase: Property scanning % 149.00/21.49 % (3441975)Time elapsed: 0.135 s % 149.00/21.49 % (3441975)Peak memory usage: 11 MB % 149.00/21.49 % (3441975)Instructions burned: 319 (million) % 149.00/21.49 % (3441977)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=1198845512:i=1428:nm=2:rtra=on_2821 on theBenchmark for (2821ds/1428Mi) % 169.33/24.39 % (3441977)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 169.33/24.39 % (3441977)Terminated due to inappropriate strategy. % 169.33/24.39 % (3441977)------------------------------ % 169.33/24.39 % (3441977)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 169.33/24.39 % (3441977)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 169.33/24.39 % (3441977)CaDiCaL version: 2.1.3 % 169.33/24.39 % (3441977)Termination reason: Inappropriate % 169.33/24.39 % (3441977)Time elapsed: 0.129 s % 169.33/24.39 % (3441977)Peak memory usage: 11 MB % 169.33/24.39 % (3441977)Instructions burned: 468 (million) % 169.33/24.39 % (3441977)------------------------------ % 169.33/24.39 % (3441977)------------------------------ % 169.33/24.39 % (3441979)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=3253014638:i=262:bd=preordered:rtra=on:fsd=on_2820 on theBenchmark for (2820ds/262Mi) % 169.33/24.39 % (3441979)Instruction limit reached! % 169.33/24.39 % (3441979)------------------------------ % 169.33/24.39 % (3441979)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 169.33/24.39 % (3441979)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 169.33/24.39 % (3441979)CaDiCaL version: 2.1.3 % 169.33/24.39 % (3441979)Termination reason: Instruction limit % 169.33/24.39 % (3441979)Termination phase: Property scanning % 169.33/24.39 % (3441979)Time elapsed: 0.111 s % 169.33/24.39 % (3441979)Peak memory usage: 11 MB % 169.33/24.39 % (3441979)Instructions burned: 263 (million) % 169.33/24.39 % (3441981)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=1173190191:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2818 on theBenchmark for (2818ds/1368Mi) % 169.33/24.39 % (3441981)Instruction limit reached! % 169.33/24.39 % (3441981)------------------------------ % 169.33/24.39 % (3441981)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 169.33/24.39 % (3441981)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 169.33/24.39 % (3441981)CaDiCaL version: 2.1.3 % 169.33/24.39 % (3441981)Termination reason: Instruction limit % 169.33/24.39 % (3441981)Termination phase: Saturation % 169.33/24.39 % (3441981)Time elapsed: 0.355 s % 169.33/24.39 % (3441981)Peak memory usage: 18 MB % 169.33/24.39 % (3441981)Instructions burned: 1371 (million) % 169.33/24.39 % (3441983)ott-21_1_sil=16000:si=on:fs=off:random_seed=4127384593:i=360:av=off:fsr=off:rtra=on_2815 on theBenchmark for (2815ds/360Mi) % 169.33/24.39 % (3441983)Instruction limit reached! % 169.33/24.39 % (3441983)------------------------------ % 169.33/24.39 % (3441983)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 169.33/24.39 % (3441983)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 169.33/24.39 % (3441983)CaDiCaL version: 2.1.3 % 169.33/24.39 % (3441983)Termination reason: Instruction limit % 169.33/24.39 % (3441983)Termination phase: Property scanning % 169.33/24.39 % (3441983)Time elapsed: 0.134 s % 169.33/24.39 % (3441983)Peak memory usage: 11 MB % 169.33/24.39 % (3441983)Instructions burned: 361 (million) % 169.33/24.39 % (3441986)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3595927034:i=954:bd=all:rtra=on_2813 on theBenchmark for (2813ds/954Mi) % 169.33/24.39 % (3441986)Instruction limit reached! % 169.33/24.39 % (3441986)------------------------------ % 169.33/24.39 % (3441986)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 169.33/24.39 % (3441986)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 169.33/24.39 % (3441986)CaDiCaL version: 2.1.3 % 169.33/24.39 % (3441986)Termination reason: Instruction limit % 169.33/24.39 % (3441986)Termination phase: Saturation % 169.33/24.39 % (3441986)Time elapsed: 0.242 s % 169.33/24.39 % (3441986)Peak memory usage: 15 MB % 169.33/24.39 % (3441986)Instructions burned: 955 (million) % 169.33/24.39 % (3441989)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=1980018087:fmbsr=1.3:i=1730:ins=25:rtra=on_2811 on theBenchmark for (2811ds/1730Mi) % 169.33/24.39 % (3441989)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 169.33/24.39 % (3441989)Terminated due to inappropriate strategy. % 169.33/24.39 % (3441989)------------------------------ % 169.33/24.39 % (3441989)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 169.33/24.39 % (3441989)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 204.66/29.33 % (3441989)CaDiCaL version: 2.1.3 % 204.66/29.33 % (3441989)Termination reason: Inappropriate % 204.66/29.33 % (3441989)Time elapsed: 0.152 s % 204.66/29.33 % (3441989)Peak memory usage: 11 MB % 204.66/29.33 % (3441989)Instructions burned: 355 (million) % 204.66/29.33 % (3441989)------------------------------ % 204.66/29.33 % (3441989)------------------------------ % 204.66/29.33 % (3441991)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=1235870862:i=2358:rtra=on_2809 on theBenchmark for (2809ds/2358Mi) % 204.66/29.33 % (3441991)Instruction limit reached! % 204.66/29.33 % (3441991)------------------------------ % 204.66/29.33 % (3441991)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 204.66/29.33 % (3441991)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 204.66/29.33 % (3441991)CaDiCaL version: 2.1.3 % 204.66/29.33 % (3441991)Termination reason: Instruction limit % 204.66/29.33 % (3441991)Termination phase: Saturation % 204.66/29.33 % (3441991)Time elapsed: 0.976 s % 204.66/29.33 % (3441991)Peak memory usage: 15 MB % 204.66/29.33 % (3441991)Instructions burned: 2358 (million) % 204.66/29.33 % (3441993)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=1181569913:i=1778:ins=1:rtra=on_2799 on theBenchmark for (2799ds/1778Mi) % 204.66/29.33 % (3441993)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 204.66/29.33 % (3441993)Terminated due to inappropriate strategy. % 204.66/29.33 % (3441993)------------------------------ % 204.66/29.33 % (3441993)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 204.66/29.33 % (3441993)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 204.66/29.33 % (3441993)CaDiCaL version: 2.1.3 % 204.66/29.33 % (3441993)Termination reason: Inappropriate % 204.66/29.33 % (3441993)Time elapsed: 0.082 s % 204.66/29.33 % (3441993)Peak memory usage: 11 MB % 204.66/29.33 % (3441993)Instructions burned: 355 (million) % 204.66/29.33 % (3441993)------------------------------ % 204.66/29.33 % (3441993)------------------------------ % 204.66/29.33 % (3441995)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=2417108573:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2798 on theBenchmark for (2798ds/1384Mi) % 204.66/29.33 % (3441995)Instruction limit reached! % 204.66/29.33 % (3441995)------------------------------ % 204.66/29.33 % (3441995)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 204.66/29.33 % (3441995)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 204.66/29.33 % (3441995)CaDiCaL version: 2.1.3 % 204.66/29.33 % (3441995)Termination reason: Instruction limit % 204.66/29.33 % (3441995)Termination phase: Saturation % 204.66/29.33 % (3441995)Time elapsed: 0.355 s % 204.66/29.33 % (3441995)Peak memory usage: 17 MB % 204.66/29.33 % (3441995)Instructions burned: 1388 (million) % 204.66/29.33 % (3441997)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=3909112742:i=1758:kws=inv_precedence:fsr=off:rtra=on_2794 on theBenchmark for (2794ds/1758Mi) % 204.66/29.33 % (3441997)Instruction limit reached! % 204.66/29.33 % (3441997)------------------------------ % 204.66/29.33 % (3441997)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 204.66/29.33 % (3441997)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 204.66/29.33 % (3441997)CaDiCaL version: 2.1.3 % 204.66/29.33 % (3441997)Termination reason: Instruction limit % 204.66/29.33 % (3441997)Termination phase: Saturation % 204.66/29.33 % (3441997)Time elapsed: 0.704 s % 204.66/29.33 % (3441997)Peak memory usage: 15 MB % 204.66/29.33 % (3441997)Instructions burned: 1758 (million) % 204.66/29.33 % (3441999)fmb+10_1_sil=64000:si=on:random_seed=56630754:i=44122:nm=2:rtra=on:gsp=on_2787 on theBenchmark for (2787ds/44122Mi) % 204.66/29.33 % (3441999)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 204.66/29.33 % (3441999)Terminated due to inappropriate strategy. % 204.66/29.33 % (3441999)------------------------------ % 204.66/29.33 % (3441999)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 204.66/29.33 % (3441999)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 204.66/29.33 % (3441999)CaDiCaL version: 2.1.3 % 204.66/29.33 % (3441999)Termination reason: Inappropriate % 204.66/29.33 % (3441999)Time elapsed: 0.106 s % 204.66/29.33 % (3441999)Peak memory usage: 11 MB % 204.66/29.33 % (3441999)Instructions burned: 468 (million) % 204.66/29.33 % (3441999)------------------------------ % 204.66/29.33 % (3441999)------------------------------ % 229.93/32.99 % (3442001)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=3113634191:i=19030:nm=5:rtra=on_2786 on theBenchmark for (2786ds/19030Mi) % 229.93/32.99 % (3442001)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 229.93/32.99 % (3442001)Terminated due to inappropriate strategy. % 229.93/32.99 % (3442001)------------------------------ % 229.93/32.99 % (3442001)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 229.93/32.99 % (3442001)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 229.93/32.99 % (3442001)CaDiCaL version: 2.1.3 % 229.93/32.99 % (3442001)Termination reason: Inappropriate % 229.93/32.99 % (3442001)Time elapsed: 0.107 s % 229.93/32.99 % (3442001)Peak memory usage: 11 MB % 229.93/32.99 % (3442001)Instructions burned: 468 (million) % 229.93/32.99 % (3442001)------------------------------ % 229.93/32.99 % (3442001)------------------------------ % 229.93/32.99 % (3442004)fmb+10_1_sil=64000:sas=cadical:si=on:fmbss=8:random_seed=2155767708:fmbsr=1.7:i=1840:rtra=on_2785 on theBenchmark for (2785ds/1840Mi) % 229.93/32.99 % (3442004)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 229.93/32.99 % (3442004)Terminated due to inappropriate strategy. % 229.93/32.99 % (3442004)------------------------------ % 229.93/32.99 % (3442004)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 229.93/32.99 % (3442004)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 229.93/32.99 % (3442004)CaDiCaL version: 2.1.3 % 229.93/32.99 % (3442004)Termination reason: Inappropriate % 229.93/32.99 % (3442004)Time elapsed: 0.107 s % 229.93/32.99 % (3442004)Peak memory usage: 11 MB % 229.93/32.99 % (3442004)Instructions burned: 468 (million) % 229.93/32.99 % (3442004)------------------------------ % 229.93/32.99 % (3442004)------------------------------ % 229.93/32.99 % (3442007)dis-4_1_sil=16000:drc=ordering:si=on:sp=const_frequency:sac=on:newcnf=on:random_seed=210069939:i=10262:rtra=on_2783 on theBenchmark for (2783ds/10262Mi) % 229.93/32.99 % (3441933)Instruction limit reached! % 229.93/32.99 % (3441933)------------------------------ % 229.93/32.99 % (3441933)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 229.93/32.99 % (3441933)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 229.93/32.99 % (3441933)CaDiCaL version: 2.1.3 % 229.93/32.99 % (3441933)Termination reason: Instruction limit % 229.93/32.99 % (3441933)Termination phase: Saturation % 229.93/32.99 % (3441933)Time elapsed: 10.280 s % 229.93/32.99 % (3441933)Peak memory usage: 29 MB % 229.93/32.99 % (3441933)Instructions burned: 28121 (million) % 229.93/32.99 % (3442009)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:si=on:sp=arity:spb=units:lsd=10:nwc=3:random_seed=143194141:i=2944:ins=7:rtra=on:fdi=8:gsp=on_2774 on theBenchmark for (2774ds/2944Mi) % 229.93/32.99 % (3442009)Instruction limit reached! % 229.93/32.99 % (3442009)------------------------------ % 229.93/32.99 % (3442009)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 229.93/32.99 % (3442009)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 229.93/32.99 % (3442009)CaDiCaL version: 2.1.3 % 229.93/32.99 % (3442009)Termination reason: Instruction limit % 229.93/32.99 % (3442009)Termination phase: Saturation % 229.93/32.99 % (3442009)Time elapsed: 1.217 s % 229.93/32.99 % (3442009)Peak memory usage: 16 MB % 229.93/32.99 % (3442009)Instructions burned: 2947 (million) % 229.93/32.99 % (3442013)fmb+10_1_sil=16000:sas=cadical:si=on:bce=on:fmbss=77:random_seed=1872343820:i=12648:rtra=on_2761 on theBenchmark for (2761ds/12648Mi) % 229.93/32.99 % (3442013)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 229.93/32.99 % (3442013)Terminated due to inappropriate strategy. % 229.93/32.99 % (3442013)------------------------------ % 229.93/32.99 % (3442013)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 229.93/32.99 % (3442013)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 229.93/32.99 % (3442013)CaDiCaL version: 2.1.3 % 229.93/32.99 % (3442013)Termination reason: Inappropriate % 229.93/32.99 % (3442013)Time elapsed: 0.198 s % 229.93/32.99 % (3442013)Peak memory usage: 11 MB % 229.93/32.99 % (3442013)Instructions burned: 468 (million) % 229.93/32.99 % (3442013)------------------------------ % 229.93/32.99 % (3442013)------------------------------ % 229.93/32.99 % (3442016)fmb+10_1_fmbas=function:sil=32000:sas=cadical:si=on:fmbss=16:random_seed=1727111537:fmbsr=2.30978:i=4348:rtra=on_2759 on theBenchmark for (2759ds/4348Mi) % 229.93/32.99 % (3442016)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 284.33/40.68 % (3442016)Terminated due to inappropriate strategy. % 284.33/40.68 % (3442016)------------------------------ % 284.33/40.68 % (3442016)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 284.33/40.68 % (3442016)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 284.33/40.68 % (3442016)CaDiCaL version: 2.1.3 % 284.33/40.68 % (3442016)Termination reason: Inappropriate % 284.33/40.68 % (3442016)Time elapsed: 0.197 s % 284.33/40.68 % (3442016)Peak memory usage: 11 MB % 284.33/40.68 % (3442016)Instructions burned: 468 (million) % 284.33/40.68 % (3442016)------------------------------ % 284.33/40.68 % (3442016)------------------------------ % 284.33/40.68 % (3442019)ott-2_1_sil=16000:si=on:newcnf=on:random_seed=1285644487:avsq=on:i=1738:avsqr=1,16:kws=inv_arity_squared:rtra=on_2757 on theBenchmark for (2757ds/1738Mi) % 284.33/40.68 % (3442019)Instruction limit reached! % 284.33/40.68 % (3442019)------------------------------ % 284.33/40.68 % (3442019)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 284.33/40.68 % (3442019)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 284.33/40.68 % (3442019)CaDiCaL version: 2.1.3 % 284.33/40.68 % (3442019)Termination reason: Instruction limit % 284.33/40.68 % (3442019)Termination phase: Saturation % 284.33/40.68 % (3442019)Time elapsed: 0.577 s % 284.33/40.68 % (3442019)Peak memory usage: 15 MB % 284.33/40.68 % (3442019)Instructions burned: 1740 (million) % 284.33/40.68 % (3442024)ott+10_1_sil=32000:tgt=ground:si=on:random_seed=2782776113:i=10228:av=off:rtra=on_2751 on theBenchmark for (2751ds/10228Mi) % 284.33/40.68 % (3442007)Instruction limit reached! % 284.33/40.68 % (3442007)------------------------------ % 284.33/40.68 % (3442007)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 284.33/40.68 % (3442007)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 284.33/40.68 % (3442007)CaDiCaL version: 2.1.3 % 284.33/40.68 % (3442007)Termination reason: Instruction limit % 284.33/40.68 % (3442007)Termination phase: Saturation % 284.33/40.68 % (3442007)Time elapsed: 3.801 s % 284.33/40.68 % (3442007)Peak memory usage: 26 MB % 284.33/40.68 % (3442007)Instructions burned: 10265 (million) % 284.33/40.68 % (3442033)fmb+10_1_sil=64000:sas=cadical:si=on:bce=on:rp=on:random_seed=3061128956:i=108564:rtra=on_2745 on theBenchmark for (2745ds/108564Mi) % 284.33/40.68 % (3442033)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 284.33/40.68 % (3442033)Terminated due to inappropriate strategy. % 284.33/40.68 % (3442033)------------------------------ % 284.33/40.68 % (3442033)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 284.33/40.68 % (3442033)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 284.33/40.68 % (3442033)CaDiCaL version: 2.1.3 % 284.33/40.68 % (3442033)Termination reason: Inappropriate % 284.33/40.68 % (3442033)Time elapsed: 0.197 s % 284.33/40.68 % (3442033)Peak memory usage: 11 MB % 284.33/40.68 % (3442033)Instructions burned: 468 (million) % 284.33/40.68 % (3442033)------------------------------ % 284.33/40.68 % (3442033)------------------------------ % 284.33/40.68 % (3442035)dis-11_1_sil=16000:si=on:sp=reverse_frequency:alpa=true:random_seed=2507567499:i=7024:aac=none:rtra=on_2743 on theBenchmark for (2743ds/7024Mi) % 284.33/40.68 % (3442035)Instruction limit reached! % 284.33/40.68 % (3442035)------------------------------ % 284.33/40.68 % (3442035)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 284.33/40.68 % (3442035)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 284.33/40.68 % (3442035)CaDiCaL version: 2.1.3 % 284.33/40.68 % (3442035)Termination reason: Instruction limit % 284.33/40.68 % (3442035)Termination phase: Saturation % 284.33/40.68 % (3442035)Time elapsed: 2.495 s % 284.33/40.68 % (3442035)Peak memory usage: 22 MB % 284.33/40.68 % (3442035)Instructions burned: 7024 (million) % 284.33/40.68 % (3442043)dis+21_1_sil=32000:sas=cadical:si=on:random_seed=4085086185:i=7546:rtra=on:amm=off_2718 on theBenchmark for (2718ds/7546Mi) % 284.33/40.68 % (3442024)Instruction limit reached! % 284.33/40.68 % (3442024)------------------------------ % 284.33/40.68 % (3442024)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 284.33/40.68 % (3442024)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 284.33/40.68 % (3442024)CaDiCaL version: 2.1.3 % 284.33/40.68 % (3442024)Termination reason: Instruction limit % 284.33/40.68 % (3442024)Termination phase: Saturation % 284.33/40.68 % (3442024)Time elapsed: 4.322 s % 284.33/40.68 % (3442024)Peak memory usage: 21 MB % 284.33/40.68 % (3442024)Instructions burned: 10228 (million) % 284.33/40.68 % (3442045)ott+11_1_Terminated % 301.35/43.05 % Vampire exiting % 301.35/43.06 Terminated %------------------------------------------------------------------------------