%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWX129_1 : TPTP v9.3.1. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/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:46:32 PM UTC 2026 % Result : Timeout 300.57s 42.64s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWX129_1 : TPTP v9.3.1. Released v9.3.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.08/0.20 % Computer : n015.cluster.edu % 0.08/0.20 % Model : x86_64 x86_64 % 0.08/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.08/0.20 % Memory : 8046.5625MB % 0.08/0.20 % OS : Linux 6.8.0-71-generic % 0.08/0.20 % CPULimit : 300 % 0.08/0.20 % WCLimit : 300 % 0.08/0.20 % DateTime : Mon Sep 28 15:06:17 UTC 2026 % 0.08/0.20 % CPUTime : % 0.08/0.20 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.08/0.22 Running first-order model finding % 0.08/0.22 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 3.04/0.77 % (2698707)Will run a generic schedule for satisfiability detection. % 3.04/0.77 % (2698714)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2926955525:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 3.04/0.77 % (2698713)% WARNING: option uhcvi not known. % 3.04/0.77 % (2698712)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=706615667_2999 on theBenchmark for (2999ds/0Mi) % 3.04/0.77 % (2698713)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3735750702:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 3.04/0.77 % (2698715)dis+10_1_sil=32000:sp=arity:random_seed=1511843499:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 3.04/0.77 % (2698716)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=358644953:i=116_2999 on theBenchmark for (2999ds/116Mi) % 3.04/0.77 % (2698717)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3525731450:i=131_2999 on theBenchmark for (2999ds/131Mi) % 3.04/0.77 % (2698718)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2597313759:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 3.04/0.77 % (2698712)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.04/0.77 % (2698712)Terminated due to inappropriate strategy. % 3.04/0.77 % (2698712)------------------------------ % 3.04/0.77 % (2698712)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.04/0.77 % (2698712)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.04/0.77 % (2698712)CaDiCaL version: 2.1.3 % 3.04/0.77 % (2698712)Termination reason: Inappropriate % 3.04/0.77 % (2698712)Time elapsed: 0.013 s % 3.04/0.77 % (2698712)Peak memory usage: 11 MB % 3.04/0.77 % (2698712)Instructions burned: 31 (million) % 3.04/0.77 % (2698712)------------------------------ % 3.04/0.77 % (2698712)------------------------------ % 3.04/0.77 % (2698726)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1023331157:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 3.04/0.77 % (2698715)Instruction limit reached! % 3.04/0.77 % (2698715)------------------------------ % 3.04/0.77 % (2698715)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.04/0.77 % (2698715)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.04/0.77 % (2698715)CaDiCaL version: 2.1.3 % 3.04/0.77 % (2698715)Termination reason: Instruction limit % 3.04/0.77 % (2698715)Termination phase: Saturation % 3.04/0.77 % (2698715)Time elapsed: 0.045 s % 3.04/0.77 % (2698715)Peak memory usage: 13 MB % 3.04/0.77 % (2698715)Instructions burned: 105 (million) % 3.04/0.77 % (2698726)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.04/0.77 % (2698726)Terminated due to inappropriate strategy. % 3.04/0.77 % (2698726)------------------------------ % 3.04/0.77 % (2698726)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.04/0.77 % (2698726)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.04/0.77 % (2698726)CaDiCaL version: 2.1.3 % 3.04/0.77 % (2698726)Termination reason: Inappropriate % 3.04/0.77 % (2698726)Time elapsed: 0.013 s % 3.04/0.77 % (2698726)Peak memory usage: 11 MB % 3.04/0.77 % (2698726)Instructions burned: 31 (million) % 3.04/0.77 % (2698726)------------------------------ % 3.04/0.77 % (2698726)------------------------------ % 3.04/0.77 % (2698716)Instruction limit reached! % 3.04/0.77 % (2698716)------------------------------ % 3.04/0.77 % (2698716)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.04/0.77 % (2698716)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.04/0.77 % (2698716)CaDiCaL version: 2.1.3 % 3.04/0.77 % (2698716)Termination reason: Instruction limit % 3.04/0.77 % (2698716)Termination phase: Saturation % 3.04/0.77 % (2698716)Time elapsed: 0.052 s % 3.04/0.77 % (2698716)Peak memory usage: 13 MB % 3.04/0.77 % (2698716)Instructions burned: 117 (million) % 3.04/0.77 % (2698717)Instruction limit reached! % 3.04/0.77 % (2698717)------------------------------ % 3.04/0.77 % (2698717)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.04/0.77 % (2698717)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.04/0.77 % (2698717)CaDiCaL version: 2.1.3 % 3.04/0.77 % (2698717)Termination reason: Instruction limit % 3.04/0.77 % (2698717)Termination phase: Saturation % 3.04/0.77 % (2698717)Time elapsed: 0.057 s % 3.04/0.77 % (2698717)Peak memory usage: 14 MB % 3.04/0.77 % (2698717)Instructions burned: 131 (million) % 3.93/0.91 % (2698729)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=2340649534:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi) % 3.93/0.91 % (2698728)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=4172980197:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi) % 3.93/0.91 % (2698730)ott-21_1_sil=16000:fs=off:random_seed=3765222536:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 3.93/0.91 % (2698731)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=727531132:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 3.93/0.91 % (2698718)Instruction limit reached! % 3.93/0.91 % (2698718)------------------------------ % 3.93/0.91 % (2698718)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.93/0.91 % (2698718)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.93/0.91 % (2698718)CaDiCaL version: 2.1.3 % 3.93/0.91 % (2698718)Termination reason: Instruction limit % 3.93/0.91 % (2698718)Termination phase: Saturation % 3.93/0.91 % (2698718)Time elapsed: 0.079 s % 3.93/0.91 % (2698718)Peak memory usage: 14 MB % 3.93/0.91 % (2698718)Instructions burned: 159 (million) % 3.93/0.91 % (2698736)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1377861989:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 3.93/0.91 % (2698736)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.93/0.91 % (2698736)Terminated due to inappropriate strategy. % 3.93/0.91 % (2698736)------------------------------ % 3.93/0.91 % (2698736)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.93/0.91 % (2698736)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.93/0.91 % (2698736)CaDiCaL version: 2.1.3 % 3.93/0.91 % (2698736)Termination reason: Inappropriate % 3.93/0.91 % (2698736)Time elapsed: 0.010 s % 3.93/0.91 % (2698736)Peak memory usage: 11 MB % 3.93/0.91 % (2698736)Instructions burned: 23 (million) % 3.93/0.91 % (2698736)------------------------------ % 3.93/0.91 % (2698736)------------------------------ % 3.93/0.91 % (2698728)Instruction limit reached! % 3.93/0.91 % (2698728)------------------------------ % 3.93/0.91 % (2698728)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.93/0.91 % (2698728)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.93/0.91 % (2698728)CaDiCaL version: 2.1.3 % 3.93/0.91 % (2698728)Termination reason: Instruction limit % 3.93/0.91 % (2698728)Termination phase: Saturation % 3.93/0.91 % (2698728)Time elapsed: 0.058 s % 3.93/0.91 % (2698728)Peak memory usage: 15 MB % 3.93/0.91 % (2698728)Instructions burned: 132 (million) % 3.93/0.91 % (2698738)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3956236186:i=1179_2998 on theBenchmark for (2998ds/1179Mi) % 3.93/0.91 % (2698739)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=38242580:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi) % 3.93/0.91 % (2698730)Instruction limit reached! % 3.93/0.91 % (2698730)------------------------------ % 3.93/0.91 % (2698730)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.93/0.91 % (2698730)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.93/0.91 % (2698730)CaDiCaL version: 2.1.3 % 3.93/0.91 % (2698730)Termination reason: Instruction limit % 3.93/0.91 % (2698730)Termination phase: Saturation % 3.93/0.91 % (2698730)Time elapsed: 0.077 s % 3.93/0.91 % (2698730)Peak memory usage: 13 MB % 3.93/0.91 % (2698730)Instructions burned: 180 (million) % 3.93/0.91 % (2698739)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.93/0.91 % (2698739)Terminated due to inappropriate strategy. % 3.93/0.91 % (2698739)------------------------------ % 3.93/0.91 % (2698739)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.93/0.91 % (2698739)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.93/0.91 % (2698739)CaDiCaL version: 2.1.3 % 3.93/0.91 % (2698739)Termination reason: Inappropriate % 3.93/0.91 % (2698739)Time elapsed: 0.010 s % 3.93/0.91 % (2698739)Peak memory usage: 10 MB % 3.93/0.91 % (2698739)Instructions burned: 23 (million) % 3.93/0.91 % (2698739)------------------------------ % 3.93/0.91 % (2698739)------------------------------ % 3.93/0.91 % (2698742)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=166111104:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2997 on theBenchmark for (2997ds/692Mi) % 16.07/2.63 % (2698743)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2806401860:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi) % 16.07/2.63 % (2698731)Instruction limit reached! % 16.07/2.63 % (2698731)------------------------------ % 16.07/2.63 % (2698731)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 16.07/2.63 % (2698731)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.07/2.63 % (2698731)CaDiCaL version: 2.1.3 % 16.07/2.63 % (2698731)Termination reason: Instruction limit % 16.07/2.63 % (2698731)Termination phase: Saturation % 16.07/2.63 % (2698731)Time elapsed: 0.187 s % 16.07/2.63 % (2698731)Peak memory usage: 14 MB % 16.07/2.63 % (2698731)Instructions burned: 477 (million) % 16.07/2.63 % (2698746)fmb+10_1_sil=64000:random_seed=605341747:i=22061:nm=2:gsp=on_2996 on theBenchmark for (2996ds/22061Mi) % 16.07/2.63 % (2698746)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 16.07/2.63 % (2698746)Terminated due to inappropriate strategy. % 16.07/2.63 % (2698746)------------------------------ % 16.07/2.63 % (2698746)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 16.07/2.63 % (2698746)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.07/2.63 % (2698746)CaDiCaL version: 2.1.3 % 16.07/2.63 % (2698746)Termination reason: Inappropriate % 16.07/2.63 % (2698746)Time elapsed: 0.013 s % 16.07/2.63 % (2698746)Peak memory usage: 11 MB % 16.07/2.63 % (2698746)Instructions burned: 31 (million) % 16.07/2.63 % (2698746)------------------------------ % 16.07/2.63 % (2698746)------------------------------ % 16.07/2.63 % (2698748)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=139805305:i=9515:nm=5_2996 on theBenchmark for (2996ds/9515Mi) % 16.07/2.63 % (2698748)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 16.07/2.63 % (2698748)Terminated due to inappropriate strategy. % 16.07/2.63 % (2698748)------------------------------ % 16.07/2.63 % (2698748)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 16.07/2.63 % (2698748)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.07/2.63 % (2698748)CaDiCaL version: 2.1.3 % 16.07/2.63 % (2698748)Termination reason: Inappropriate % 16.07/2.63 % (2698748)Time elapsed: 0.012 s % 16.07/2.63 % (2698748)Peak memory usage: 11 MB % 16.07/2.63 % (2698748)Instructions burned: 31 (million) % 16.07/2.63 % (2698748)------------------------------ % 16.07/2.63 % (2698748)------------------------------ % 16.07/2.63 % (2698729)Instruction limit reached! % 16.07/2.63 % (2698729)------------------------------ % 16.07/2.63 % (2698729)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 16.07/2.63 % (2698729)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.07/2.63 % (2698729)CaDiCaL version: 2.1.3 % 16.07/2.63 % (2698729)Termination reason: Instruction limit % 16.07/2.63 % (2698729)Termination phase: Saturation % 16.07/2.63 % (2698729)Time elapsed: 0.283 s % 16.07/2.63 % (2698729)Peak memory usage: 15 MB % 16.07/2.63 % (2698729)Instructions burned: 685 (million) % 16.07/2.63 % (2698750)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1078045610:fmbsr=1.7:i=920_2996 on theBenchmark for (2996ds/920Mi) % 16.07/2.63 % (2698750)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 16.07/2.63 % (2698750)Terminated due to inappropriate strategy. % 16.07/2.63 % (2698750)------------------------------ % 16.07/2.63 % (2698750)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 16.07/2.63 % (2698750)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.07/2.63 % (2698750)CaDiCaL version: 2.1.3 % 16.07/2.63 % (2698750)Termination reason: Inappropriate % 16.07/2.63 % (2698750)Time elapsed: 0.012 s % 16.07/2.63 % (2698750)Peak memory usage: 11 MB % 16.07/2.63 % (2698750)Instructions burned: 31 (million) % 16.07/2.63 % (2698750)------------------------------ % 16.07/2.63 % (2698750)------------------------------ % 16.07/2.63 % (2698752)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1662587043:i=5131_2995 on theBenchmark for (2995ds/5131Mi) % 16.07/2.63 % (2698753)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3306996707:i=1472:ins=7:fdi=8:gsp=on_2995 on theBenchmark for (2995ds/1472Mi) % 16.07/2.63 % (2698742)Instruction limit reached! % 16.07/2.63 % (2698742)------------------------------ % 30.82/4.66 % (2698742)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 30.82/4.66 % (2698742)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 30.82/4.66 % (2698742)CaDiCaL version: 2.1.3 % 30.82/4.66 % (2698742)Termination reason: Instruction limit % 30.82/4.66 % (2698742)Termination phase: Saturation % 30.82/4.66 % (2698742)Time elapsed: 0.306 s % 30.82/4.66 % (2698742)Peak memory usage: 16 MB % 30.82/4.66 % (2698742)Instructions burned: 694 (million) % 30.82/4.66 % (2698756)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=698405403:i=6324_2994 on theBenchmark for (2994ds/6324Mi) % 30.82/4.66 % (2698756)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 30.82/4.66 % (2698756)Terminated due to inappropriate strategy. % 30.82/4.66 % (2698756)------------------------------ % 30.82/4.66 % (2698756)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 30.82/4.66 % (2698756)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 30.82/4.66 % (2698756)CaDiCaL version: 2.1.3 % 30.82/4.66 % (2698756)Termination reason: Inappropriate % 30.82/4.66 % (2698756)Time elapsed: 0.013 s % 30.82/4.66 % (2698756)Peak memory usage: 11 MB % 30.82/4.66 % (2698756)Instructions burned: 31 (million) % 30.82/4.66 % (2698756)------------------------------ % 30.82/4.66 % (2698756)------------------------------ % 30.82/4.66 % (2698743)Instruction limit reached! % 30.82/4.66 % (2698743)------------------------------ % 30.82/4.66 % (2698743)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 30.82/4.66 % (2698743)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 30.82/4.66 % (2698743)CaDiCaL version: 2.1.3 % 30.82/4.66 % (2698743)Termination reason: Instruction limit % 30.82/4.66 % (2698743)Termination phase: Saturation % 30.82/4.66 % (2698743)Time elapsed: 0.337 s % 30.82/4.66 % (2698743)Peak memory usage: 14 MB % 30.82/4.66 % (2698743)Instructions burned: 879 (million) % 30.82/4.66 % (2698758)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1846159616:fmbsr=2.30978:i=2174_2994 on theBenchmark for (2994ds/2174Mi) % 30.82/4.66 % (2698759)ott-2_1_sil=16000:newcnf=on:random_seed=3451971415:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2994 on theBenchmark for (2994ds/869Mi) % 30.82/4.66 % (2698758)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 30.82/4.66 % (2698758)Terminated due to inappropriate strategy. % 30.82/4.66 % (2698758)------------------------------ % 30.82/4.66 % (2698758)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 30.82/4.66 % (2698758)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 30.82/4.66 % (2698758)CaDiCaL version: 2.1.3 % 30.82/4.66 % (2698758)Termination reason: Inappropriate % 30.82/4.66 % (2698758)Time elapsed: 0.012 s % 30.82/4.66 % (2698758)Peak memory usage: 11 MB % 30.82/4.66 % (2698758)Instructions burned: 31 (million) % 30.82/4.66 % (2698758)------------------------------ % 30.82/4.66 % (2698758)------------------------------ % 30.82/4.66 % (2698762)ott+10_1_sil=32000:tgt=ground:random_seed=730523632:i=5114:av=off_2993 on theBenchmark for (2993ds/5114Mi) % 30.82/4.66 % (2698738)Instruction limit reached! % 30.82/4.66 % (2698738)------------------------------ % 30.82/4.66 % (2698738)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 30.82/4.66 % (2698738)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 30.82/4.66 % (2698738)CaDiCaL version: 2.1.3 % 30.82/4.66 % (2698738)Termination reason: Instruction limit % 30.82/4.66 % (2698738)Termination phase: Saturation % 30.82/4.66 % (2698738)Time elapsed: 0.459 s % 30.82/4.66 % (2698738)Peak memory usage: 14 MB % 30.82/4.66 % (2698738)Instructions burned: 1179 (million) % 30.82/4.66 % (2698764)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=1466405520:i=54282_2993 on theBenchmark for (2993ds/54282Mi) % 30.82/4.66 % (2698764)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 30.82/4.66 % (2698764)Terminated due to inappropriate strategy. % 30.82/4.66 % (2698764)------------------------------ % 30.82/4.66 % (2698764)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 30.82/4.66 % (2698764)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 30.82/4.66 % (2698764)CaDiCaL version: 2.1.3 % 30.82/4.66 % (2698764)Termination reason: Inappropriate % 30.82/4.66 % (2698764)Time elapsed: 0.014 s % 30.82/4.66 % (2698764)Peak memory usage: 11 MB % 30.82/4.66 % (2698764)Instructions burned: 31 (million) % 81.91/11.89 % (2698764)------------------------------ % 81.91/11.89 % (2698764)------------------------------ % 81.91/11.89 % (2698766)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=1896279048:i=3512:aac=none_2993 on theBenchmark for (2993ds/3512Mi) % 81.91/11.89 % (2698759)Instruction limit reached! % 81.91/11.89 % (2698759)------------------------------ % 81.91/11.89 % (2698759)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 81.91/11.89 % (2698759)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 81.91/11.89 % (2698759)CaDiCaL version: 2.1.3 % 81.91/11.89 % (2698759)Termination reason: Instruction limit % 81.91/11.89 % (2698759)Termination phase: Saturation % 81.91/11.89 % (2698759)Time elapsed: 0.352 s % 81.91/11.89 % (2698759)Peak memory usage: 15 MB % 81.91/11.89 % (2698759)Instructions burned: 870 (million) % 81.91/11.89 % (2698768)dis+21_1_sil=32000:sas=cadical:random_seed=1259898172:i=3773:amm=off_2990 on theBenchmark for (2990ds/3773Mi) % 81.91/11.89 % (2698753)Instruction limit reached! % 81.91/11.89 % (2698753)------------------------------ % 81.91/11.89 % (2698753)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 81.91/11.89 % (2698753)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 81.91/11.89 % (2698753)CaDiCaL version: 2.1.3 % 81.91/11.89 % (2698753)Termination reason: Instruction limit % 81.91/11.89 % (2698753)Termination phase: Saturation % 81.91/11.89 % (2698753)Time elapsed: 0.746 s % 81.91/11.89 % (2698753)Peak memory usage: 23 MB % 81.91/11.89 % (2698753)Instructions burned: 1473 (million) % 81.91/11.89 % (2698770)ott+11_1_sil=16000:gs=on:random_seed=2365158959:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2988 on theBenchmark for (2988ds/2251Mi) % 81.91/11.89 % (2698770)Instruction limit reached! % 81.91/11.89 % (2698770)------------------------------ % 81.91/11.89 % (2698770)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 81.91/11.89 % (2698770)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 81.91/11.89 % (2698770)CaDiCaL version: 2.1.3 % 81.91/11.89 % (2698770)Termination reason: Instruction limit % 81.91/11.89 % (2698770)Termination phase: Saturation % 81.91/11.89 % (2698770)Time elapsed: 0.860 s % 81.91/11.89 % (2698770)Peak memory usage: 14 MB % 81.91/11.89 % (2698770)Instructions burned: 2253 (million) % 81.91/11.89 % (2698766)Instruction limit reached! % 81.91/11.89 % (2698766)------------------------------ % 81.91/11.89 % (2698766)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 81.91/11.89 % (2698766)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 81.91/11.89 % (2698766)CaDiCaL version: 2.1.3 % 81.91/11.89 % (2698766)Termination reason: Instruction limit % 81.91/11.89 % (2698766)Termination phase: Saturation % 81.91/11.89 % (2698766)Time elapsed: 1.374 s % 81.91/11.89 % (2698766)Peak memory usage: 17 MB % 81.91/11.89 % (2698766)Instructions burned: 3513 (million) % 81.91/11.89 % (2698772)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=4125734690:fmbsr=1.6:i=67534_2979 on theBenchmark for (2979ds/67534Mi) % 81.91/11.89 % (2698773)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=1701628547:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2979 on theBenchmark for (2979ds/4591Mi) % 81.91/11.89 % (2698772)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 81.91/11.89 % (2698772)Terminated due to inappropriate strategy. % 81.91/11.89 % (2698772)------------------------------ % 81.91/11.89 % (2698772)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 81.91/11.89 % (2698772)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 81.91/11.89 % (2698772)CaDiCaL version: 2.1.3 % 81.91/11.89 % (2698772)Termination reason: Inappropriate % 81.91/11.89 % (2698772)Time elapsed: 0.013 s % 81.91/11.89 % (2698772)Peak memory usage: 11 MB % 81.91/11.89 % (2698772)Instructions burned: 31 (million) % 81.91/11.89 % (2698772)------------------------------ % 81.91/11.89 % (2698772)------------------------------ % 81.91/11.89 % (2698776)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=2045223211:i=29340_2978 on theBenchmark for (2978ds/29340Mi) % 81.91/11.89 % (2698768)Instruction limit reached! % 81.91/11.89 % (2698768)------------------------------ % 81.91/11.89 % (2698768)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 81.91/11.89 % (2698768)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 81.91/11.89 % (2698768)CaDiCaL version: 2.1.3 % 81.91/11.89 % (2698768)Termination reason: Instruction limit % 95.36/13.71 % (2698768)Termination phase: Saturation % 95.36/13.71 % (2698768)Time elapsed: 1.431 s % 95.36/13.71 % (2698768)Peak memory usage: 16 MB % 95.36/13.71 % (2698768)Instructions burned: 3773 (million) % 95.36/13.71 % (2698752)Instruction limit reached! % 95.36/13.71 % (2698752)------------------------------ % 95.36/13.71 % (2698752)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 95.36/13.71 % (2698752)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 95.36/13.71 % (2698752)CaDiCaL version: 2.1.3 % 95.36/13.71 % (2698752)Termination reason: Instruction limit % 95.36/13.71 % (2698752)Termination phase: Saturation % 95.36/13.71 % (2698752)Time elapsed: 1.969 s % 95.36/13.71 % (2698752)Peak memory usage: 20 MB % 95.36/13.71 % (2698752)Instructions burned: 5132 (million) % 95.36/13.71 % (2698778)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=1572716804:i=5211_2976 on theBenchmark for (2976ds/5211Mi) % 95.36/13.71 % (2698779)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=1571643818:i=5497:nm=2_2975 on theBenchmark for (2975ds/5497Mi) % 95.36/13.71 % (2698779)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 95.36/13.71 % (2698779)Terminated due to inappropriate strategy. % 95.36/13.71 % (2698779)------------------------------ % 95.36/13.71 % (2698779)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 95.36/13.71 % (2698779)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 95.36/13.71 % (2698779)CaDiCaL version: 2.1.3 % 95.36/13.71 % (2698779)Termination reason: Inappropriate % 95.36/13.71 % (2698779)Time elapsed: 0.013 s % 95.36/13.71 % (2698779)Peak memory usage: 11 MB % 95.36/13.71 % (2698779)Instructions burned: 31 (million) % 95.36/13.71 % (2698779)------------------------------ % 95.36/13.71 % (2698779)------------------------------ % 95.36/13.71 % (2698782)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=1804430984:fmbsr=2:i=46332_2975 on theBenchmark for (2975ds/46332Mi) % 95.36/13.71 % (2698782)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 95.36/13.71 % (2698782)Terminated due to inappropriate strategy. % 95.36/13.71 % (2698782)------------------------------ % 95.36/13.71 % (2698782)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 95.36/13.71 % (2698782)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 95.36/13.71 % (2698782)CaDiCaL version: 2.1.3 % 95.36/13.71 % (2698782)Termination reason: Inappropriate % 95.36/13.71 % (2698782)Time elapsed: 0.012 s % 95.36/13.71 % (2698782)Peak memory usage: 11 MB % 95.36/13.71 % (2698782)Instructions burned: 31 (million) % 95.36/13.71 % (2698782)------------------------------ % 95.36/13.71 % (2698782)------------------------------ % 95.36/13.71 % (2698784)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=808349632:i=14071_2975 on theBenchmark for (2975ds/14071Mi) % 95.36/13.71 % (2698784)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 95.36/13.71 % (2698784)Terminated due to inappropriate strategy. % 95.36/13.71 % (2698784)------------------------------ % 95.36/13.71 % (2698784)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 95.36/13.71 % (2698784)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 95.36/13.71 % (2698784)CaDiCaL version: 2.1.3 % 95.36/13.71 % (2698784)Termination reason: Inappropriate % 95.36/13.71 % (2698784)Time elapsed: 0.012 s % 95.36/13.71 % (2698784)Peak memory usage: 11 MB % 95.36/13.71 % (2698784)Instructions burned: 31 (million) % 95.36/13.71 % (2698784)------------------------------ % 95.36/13.71 % (2698784)------------------------------ % 95.36/13.71 % (2698786)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1084990203:i=22565:add=on:rawr=on_2975 on theBenchmark for (2975ds/22565Mi) % 95.36/13.71 % (2698762)Instruction limit reached! % 95.36/13.71 % (2698762)------------------------------ % 95.36/13.71 % (2698762)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 95.36/13.71 % (2698762)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 95.36/13.71 % (2698762)CaDiCaL version: 2.1.3 % 95.36/13.71 % (2698762)Termination reason: Instruction limit % 95.36/13.71 % (2698762)Termination phase: Saturation % 95.36/13.71 % (2698762)Time elapsed: 1.972 s % 95.36/13.71 % (2698762)Peak memory usage: 15 MB % 95.36/13.71 % (2698762)Instructions burned: 5115 (million) % 95.36/13.71 % (2698788)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=4179034146:i=8173:av=off_2974 on theBenchmark for (2974ds/8173Mi) % 95.36/13.71 % (2698778)Instruction limit reached! % 95.96/13.88 % (2698778)------------------------------ % 95.96/13.88 % (2698778)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 95.96/13.88 % (2698778)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 95.96/13.88 % (2698778)CaDiCaL version: 2.1.3 % 95.96/13.88 % (2698778)Termination reason: Instruction limit % 95.96/13.88 % (2698778)Termination phase: Saturation % 95.96/13.88 % (2698778)Time elapsed: 2.013 s % 95.96/13.88 % (2698778)Peak memory usage: 22 MB % 95.96/13.88 % (2698778)Instructions burned: 5211 (million) % 95.96/13.88 % (2698790)dis+10_16:1_sil=16000:random_seed=202366689:i=9155:fsr=off_2955 on theBenchmark for (2955ds/9155Mi) % 95.96/13.88 % (2698773)Instruction limit reached! % 95.96/13.88 % (2698773)------------------------------ % 95.96/13.88 % (2698773)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 95.96/13.88 % (2698773)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 95.96/13.88 % (2698773)CaDiCaL version: 2.1.3 % 95.96/13.88 % (2698773)Termination reason: Instruction limit % 95.96/13.88 % (2698773)Termination phase: Saturation % 95.96/13.88 % (2698773)Time elapsed: 2.530 s % 95.96/13.88 % (2698773)Peak memory usage: 43 MB % 95.96/13.88 % (2698773)Instructions burned: 4591 (million) % 95.96/13.88 % (2698792)ott-3_8_sil=64000:random_seed=2099600768:i=20139:bs=on_2953 on theBenchmark for (2953ds/20139Mi) % 95.96/13.88 % (2698788)Instruction limit reached! % 95.96/13.88 % (2698788)------------------------------ % 95.96/13.88 % (2698788)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 95.96/13.88 % (2698788)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 95.96/13.88 % (2698788)CaDiCaL version: 2.1.3 % 95.96/13.88 % (2698788)Termination reason: Instruction limit % 95.96/13.88 % (2698788)Termination phase: Saturation % 95.96/13.88 % (2698788)Time elapsed: 3.163 s % 95.96/13.88 % (2698788)Peak memory usage: 15 MB % 95.96/13.88 % (2698788)Instructions burned: 8175 (million) % 95.96/13.88 % (2698794)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=4078372205:fmbsr=2:i=32576_2942 on theBenchmark for (2942ds/32576Mi) % 95.96/13.88 % (2698794)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 95.96/13.88 % (2698794)Terminated due to inappropriate strategy. % 95.96/13.88 % (2698794)------------------------------ % 95.96/13.88 % (2698794)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 95.96/13.88 % (2698794)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 95.96/13.88 % (2698794)CaDiCaL version: 2.1.3 % 95.96/13.88 % (2698794)Termination reason: Inappropriate % 95.96/13.88 % (2698794)Time elapsed: 0.013 s % 95.96/13.88 % (2698794)Peak memory usage: 11 MB % 95.96/13.88 % (2698794)Instructions burned: 31 (million) % 95.96/13.88 % (2698794)------------------------------ % 95.96/13.88 % (2698794)------------------------------ % 95.96/13.88 % (2698796)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=3526854735:i=11404_2941 on theBenchmark for (2941ds/11404Mi) % 95.96/13.88 % (2698790)Instruction limit reached! % 95.96/13.88 % (2698790)------------------------------ % 95.96/13.88 % (2698790)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 95.96/13.88 % (2698790)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 95.96/13.88 % (2698790)CaDiCaL version: 2.1.3 % 95.96/13.88 % (2698790)Termination reason: Instruction limit % 95.96/13.88 % (2698790)Termination phase: Saturation % 95.96/13.88 % (2698790)Time elapsed: 3.471 s % 95.96/13.88 % (2698790)Peak memory usage: 18 MB % 95.96/13.88 % (2698790)Instructions burned: 9157 (million) % 95.96/13.88 % (2698798)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=4249508360:i=14134_2920 on theBenchmark for (2920ds/14134Mi) % 95.96/13.88 % (2698796)Instruction limit reached! % 95.96/13.88 % (2698796)------------------------------ % 95.96/13.88 % (2698796)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 95.96/13.88 % (2698796)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 95.96/13.88 % (2698796)CaDiCaL version: 2.1.3 % 95.96/13.88 % (2698796)Termination reason: Instruction limit % 95.96/13.88 % (2698796)Termination phase: Saturation % 95.96/13.88 % (2698796)Time elapsed: 4.424 s % 95.96/13.88 % (2698796)Peak memory usage: 16 MB % 95.96/13.88 % (2698796)Instructions burned: 11406 (million) % 95.96/13.88 % (2698800)dis+33_16_sil=32000:sac=on:random_seed=227140120:i=15851:nm=0_2897 on theBenchmark for (2897ds/15851Mi) % 95.96/13.88 % (2698786)Instruction limit reached! % 95.96/13.88 % (2698786)------------------------------ % 95.96/13.88 % (2698786)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 141.01/20.16 % (2698786)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 141.01/20.16 % (2698786)CaDiCaL version: 2.1.3 % 141.01/20.16 % (2698786)Termination reason: Instruction limit % 141.01/20.16 % (2698786)Termination phase: Saturation % 141.01/20.16 % (2698786)Time elapsed: 9.143 s % 141.01/20.16 % (2698786)Peak memory usage: 17 MB % 141.01/20.16 % (2698786)Instructions burned: 22568 (million) % 141.01/20.16 % (2698802)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=126628892:avsq=on:i=17627:add=on:amm=off_2883 on theBenchmark for (2883ds/17627Mi) % 141.01/20.16 % (2698792)Instruction limit reached! % 141.01/20.16 % (2698792)------------------------------ % 141.01/20.16 % (2698792)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 141.01/20.16 % (2698792)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 141.01/20.16 % (2698792)CaDiCaL version: 2.1.3 % 141.01/20.16 % (2698792)Termination reason: Instruction limit % 141.01/20.16 % (2698792)Termination phase: Saturation % 141.01/20.16 % (2698792)Time elapsed: 7.676 s % 141.01/20.16 % (2698792)Peak memory usage: 19 MB % 141.01/20.16 % (2698792)Instructions burned: 20139 (million) % 141.01/20.16 % (2698804)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=2320628509:s2a=on:i=53295_2876 on theBenchmark for (2876ds/53295Mi) % 141.01/20.16 % (2698776)Instruction limit reached! % 141.01/20.16 % (2698776)------------------------------ % 141.01/20.16 % (2698776)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 141.01/20.16 % (2698776)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 141.01/20.16 % (2698776)CaDiCaL version: 2.1.3 % 141.01/20.16 % (2698776)Termination reason: Instruction limit % 141.01/20.16 % (2698776)Termination phase: Saturation % 141.01/20.16 % (2698776)Time elapsed: 11.250 s % 141.01/20.16 % (2698776)Peak memory usage: 21 MB % 141.01/20.16 % (2698776)Instructions burned: 29342 (million) % 141.01/20.16 % (2698862)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=2139584548:i=26857:ins=20_2866 on theBenchmark for (2866ds/26857Mi) % 141.01/20.16 % (2698862)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 141.01/20.16 % (2698862)Terminated due to inappropriate strategy. % 141.01/20.16 % (2698862)------------------------------ % 141.01/20.16 % (2698862)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 141.01/20.16 % (2698862)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 141.01/20.16 % (2698862)CaDiCaL version: 2.1.3 % 141.01/20.16 % (2698862)Termination reason: Inappropriate % 141.01/20.16 % (2698862)Time elapsed: 0.013 s % 141.01/20.16 % (2698862)Peak memory usage: 11 MB % 141.01/20.16 % (2698862)Instructions burned: 31 (million) % 141.01/20.16 % (2698862)------------------------------ % 141.01/20.16 % (2698862)------------------------------ % 141.01/20.16 % (2698869)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=3739882139:i=28120:bs=on:fsr=off_2865 on theBenchmark for (2865ds/28120Mi) % 141.01/20.16 % (2698798)Instruction limit reached! % 141.01/20.16 % (2698798)------------------------------ % 141.01/20.16 % (2698798)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 141.01/20.16 % (2698798)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 141.01/20.16 % (2698798)CaDiCaL version: 2.1.3 % 141.01/20.16 % (2698798)Termination reason: Instruction limit % 141.01/20.16 % (2698798)Termination phase: Saturation % 141.01/20.16 % (2698798)Time elapsed: 5.488 s % 141.01/20.16 % (2698798)Peak memory usage: 16 MB % 141.01/20.16 % (2698798)Instructions burned: 14136 (million) % 141.01/20.16 % (2698872)fmb+10_1_sil=256000:fmbss=7:random_seed=3945624438:fmbsr=1.6:i=182295_2865 on theBenchmark for (2865ds/182295Mi) % 141.01/20.16 % (2698872)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 141.01/20.16 % (2698872)Terminated due to inappropriate strategy. % 141.01/20.16 % (2698872)------------------------------ % 141.01/20.16 % (2698872)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 141.01/20.16 % (2698872)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 141.01/20.16 % (2698872)CaDiCaL version: 2.1.3 % 141.01/20.16 % (2698872)Termination reason: Inappropriate % 141.01/20.16 % (2698872)Time elapsed: 0.013 s % 141.01/20.16 % (2698872)Peak memory usage: 11 MB % 141.01/20.16 % (2698872)Instructions burned: 31 (million) % 141.01/20.16 % (2698872)------------------------------ % 141.01/20.16 % (2698872)------------------------------ % 141.01/20.16 % (2698877)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=1340227170:i=44625:gsp=on_2865 on theBenchmark for (2865ds/44625Mi) % 143.35/20.53 % (2698877)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 143.35/20.53 % (2698877)Terminated due to inappropriate strategy. % 143.35/20.53 % (2698877)------------------------------ % 143.35/20.53 % (2698877)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 143.35/20.53 % (2698877)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 143.35/20.53 % (2698877)CaDiCaL version: 2.1.3 % 143.35/20.53 % (2698877)Termination reason: Inappropriate % 143.35/20.53 % (2698877)Time elapsed: 0.013 s % 143.35/20.53 % (2698877)Peak memory usage: 11 MB % 143.35/20.53 % (2698877)Instructions burned: 31 (million) % 143.35/20.53 % (2698877)------------------------------ % 143.35/20.53 % (2698877)------------------------------ % 143.35/20.53 % (2698887)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=3803676820:i=160505_2865 on theBenchmark for (2865ds/160505Mi) % 143.35/20.53 % (2698887)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 143.35/20.53 % (2698887)Terminated due to inappropriate strategy. % 143.35/20.53 % (2698887)------------------------------ % 143.35/20.53 % (2698887)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 143.35/20.53 % (2698887)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 143.35/20.53 % (2698887)CaDiCaL version: 2.1.3 % 143.35/20.53 % (2698887)Termination reason: Inappropriate % 143.35/20.53 % (2698887)Time elapsed: 0.013 s % 143.35/20.53 % (2698887)Peak memory usage: 11 MB % 143.35/20.53 % (2698887)Instructions burned: 31 (million) % 143.35/20.53 % (2698887)------------------------------ % 143.35/20.53 % (2698887)------------------------------ % 143.35/20.53 % (2698895)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=803233970:fmbsr=1.3:i=225729_2864 on theBenchmark for (2864ds/225729Mi) % 143.35/20.53 % (2698895)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 143.35/20.53 % (2698895)Terminated due to inappropriate strategy. % 143.35/20.53 % (2698895)------------------------------ % 143.35/20.53 % (2698895)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 143.35/20.53 % (2698895)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 143.35/20.53 % (2698895)CaDiCaL version: 2.1.3 % 143.35/20.53 % (2698895)Termination reason: Inappropriate % 143.35/20.53 % (2698895)Time elapsed: 0.013 s % 143.35/20.53 % (2698895)Peak memory usage: 11 MB % 143.35/20.53 % (2698895)Instructions burned: 31 (million) % 143.35/20.53 % (2698895)------------------------------ % 143.35/20.53 % (2698895)------------------------------ % 143.35/20.53 % (2698908)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=433368250:fmbsr=2:i=185024:ins=7_2864 on theBenchmark for (2864ds/185024Mi) % 143.35/20.53 % (2698908)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 143.35/20.53 % (2698908)Terminated due to inappropriate strategy. % 143.35/20.53 % (2698908)------------------------------ % 143.35/20.53 % (2698908)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 143.35/20.53 % (2698908)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 143.35/20.53 % (2698908)CaDiCaL version: 2.1.3 % 143.35/20.53 % (2698908)Termination reason: Inappropriate % 143.35/20.53 % (2698908)Time elapsed: 0.013 s % 143.35/20.53 % (2698908)Peak memory usage: 11 MB % 143.35/20.53 % (2698908)Instructions burned: 31 (million) % 143.35/20.53 % (2698908)------------------------------ % 143.35/20.53 % (2698908)------------------------------ % 143.35/20.53 % (2698922)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=2539651945:rtra=on_2864 on theBenchmark for (2864ds/0Mi) % 143.35/20.53 % (2698922)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 143.35/20.53 % (2698922)Terminated due to inappropriate strategy. % 143.35/20.53 % (2698922)------------------------------ % 143.35/20.53 % (2698922)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 143.35/20.53 % (2698922)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 143.35/20.53 % (2698922)CaDiCaL version: 2.1.3 % 143.35/20.53 % (2698922)Termination reason: Inappropriate % 143.35/20.53 % (2698922)Time elapsed: 0.013 s % 143.35/20.53 % (2698922)Peak memory usage: 11 MB % 143.35/20.53 % (2698922)Instructions burned: 31 (million) % 143.35/20.53 % (2698922)------------------------------ % 143.35/20.53 % (2698922)------------------------------ % 143.35/20.53 % (2698931)% WARNING: option uhcvi not known. % 143.35/20.53 % (2698931)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1183090969:i=271062:add=off:rtra=on:rawr=on_2863 on theBenchmark for (2863ds/271062Mi) % 149.69/21.42 % (2698800)Instruction limit reached! % 149.69/21.42 % (2698800)------------------------------ % 149.69/21.42 % (2698800)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 149.69/21.42 % (2698800)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 149.69/21.42 % (2698800)CaDiCaL version: 2.1.3 % 149.69/21.42 % (2698800)Termination reason: Instruction limit % 149.69/21.42 % (2698800)Termination phase: Saturation % 149.69/21.42 % (2698800)Time elapsed: 6.194 s % 149.69/21.42 % (2698800)Peak memory usage: 22 MB % 149.69/21.42 % (2698800)Instructions burned: 15852 (million) % 149.69/21.42 % (2699122)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=27543713:i=176048:add=on:rtra=on:rawr=on_2835 on theBenchmark for (2835ds/176048Mi) % 149.69/21.42 % (2698802)Instruction limit reached! % 149.69/21.42 % (2698802)------------------------------ % 149.69/21.42 % (2698802)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 149.69/21.42 % (2698802)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 149.69/21.42 % (2698802)CaDiCaL version: 2.1.3 % 149.69/21.42 % (2698802)Termination reason: Instruction limit % 149.69/21.42 % (2698802)Termination phase: Saturation % 149.69/21.42 % (2698802)Time elapsed: 7.999 s % 149.69/21.42 % (2698802)Peak memory usage: 149 MB % 149.69/21.42 % (2698802)Instructions burned: 17629 (million) % 149.69/21.42 % (2699124)dis+10_1_sil=32000:si=on:sp=arity:random_seed=2426824751:i=206:fgj=on:rtra=on_2803 on theBenchmark for (2803ds/206Mi) % 149.69/21.42 % (2699124)Instruction limit reached! % 149.69/21.42 % (2699124)------------------------------ % 149.69/21.42 % (2699124)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 149.69/21.42 % (2699124)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 149.69/21.42 % (2699124)CaDiCaL version: 2.1.3 % 149.69/21.42 % (2699124)Termination reason: Instruction limit % 149.69/21.42 % (2699124)Termination phase: Saturation % 149.69/21.42 % (2699124)Time elapsed: 0.084 s % 149.69/21.42 % (2699124)Peak memory usage: 13 MB % 149.69/21.42 % (2699124)Instructions burned: 208 (million) % 149.69/21.42 % (2699126)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=1130929688:i=232:rtra=on_2801 on theBenchmark for (2801ds/232Mi) % 149.69/21.42 % (2698714)Instruction limit reached! % 149.69/21.42 % (2698714)------------------------------ % 149.69/21.42 % (2698714)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 149.69/21.42 % (2698714)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 149.69/21.42 % (2698714)CaDiCaL version: 2.1.3 % 149.69/21.42 % (2698714)Termination reason: Instruction limit % 149.69/21.42 % (2698714)Termination phase: Saturation % 149.69/21.42 % (2698714)Time elapsed: 19.770 s % 149.69/21.42 % (2698714)Peak memory usage: 22 MB % 149.69/21.42 % (2698714)Instructions burned: 88028 (million) % 149.69/21.42 % (2699128)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=1816948133:i=262:rtra=on_2801 on theBenchmark for (2801ds/262Mi) % 149.69/21.42 % (2699128)Instruction limit reached! % 149.69/21.42 % (2699128)------------------------------ % 149.69/21.42 % (2699128)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 149.69/21.42 % (2699128)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 149.69/21.42 % (2699128)CaDiCaL version: 2.1.3 % 149.69/21.42 % (2699128)Termination reason: Instruction limit % 149.69/21.42 % (2699128)Termination phase: Saturation % 149.69/21.42 % (2699128)Time elapsed: 0.055 s % 149.69/21.42 % (2699128)Peak memory usage: 12 MB % 149.69/21.42 % (2699128)Instructions burned: 266 (million) % 149.69/21.42 % (2699130)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=1940463792:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2801 on theBenchmark for (2801ds/318Mi) % 149.69/21.42 % (2699126)Instruction limit reached! % 149.69/21.42 % (2699126)------------------------------ % 149.69/21.42 % (2699126)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 149.69/21.42 % (2699126)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 149.69/21.42 % (2699126)CaDiCaL version: 2.1.3 % 149.69/21.42 % (2699126)Termination reason: Instruction limit % 149.69/21.42 % (2699126)Termination phase: Saturation % 149.69/21.42 % (2699126)Time elapsed: 0.091 s % 149.69/21.42 % (2699126)Peak memory usage: 13 MB % 149.69/21.42 % (2699126)Instructions burned: 234 (million) % 149.69/21.42 % (2699132)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=396033315:i=1428:nm=2:rtra=on_2800 on theBenchmark for (2800ds/1428Mi) % 158.57/22.69 % (2699132)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 158.57/22.69 % (2699132)Terminated due to inappropriate strategy. % 158.57/22.69 % (2699132)------------------------------ % 158.57/22.69 % (2699132)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 158.57/22.69 % (2699132)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 158.57/22.69 % (2699132)CaDiCaL version: 2.1.3 % 158.57/22.69 % (2699132)Termination reason: Inappropriate % 158.57/22.69 % (2699132)Time elapsed: 0.013 s % 158.57/22.69 % (2699132)Peak memory usage: 11 MB % 158.57/22.69 % (2699132)Instructions burned: 31 (million) % 158.57/22.69 % (2699132)------------------------------ % 158.57/22.69 % (2699132)------------------------------ % 158.57/22.69 % (2699134)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=681595024:i=262:bd=preordered:rtra=on:fsd=on_2800 on theBenchmark for (2800ds/262Mi) % 158.57/22.69 % (2699130)Instruction limit reached! % 158.57/22.69 % (2699130)------------------------------ % 158.57/22.69 % (2699130)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 158.57/22.69 % (2699130)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 158.57/22.69 % (2699130)CaDiCaL version: 2.1.3 % 158.57/22.69 % (2699130)Termination reason: Instruction limit % 158.57/22.69 % (2699130)Termination phase: Saturation % 158.57/22.69 % (2699130)Time elapsed: 0.076 s % 158.57/22.69 % (2699130)Peak memory usage: 15 MB % 158.57/22.69 % (2699130)Instructions burned: 321 (million) % 158.57/22.69 % (2699136)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=2304592169:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2800 on theBenchmark for (2800ds/1368Mi) % 158.57/22.69 % (2699134)Instruction limit reached! % 158.57/22.69 % (2699134)------------------------------ % 158.57/22.69 % (2699134)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 158.57/22.69 % (2699134)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 158.57/22.69 % (2699134)CaDiCaL version: 2.1.3 % 158.57/22.69 % (2699134)Termination reason: Instruction limit % 158.57/22.69 % (2699134)Termination phase: Saturation % 158.57/22.69 % (2699134)Time elapsed: 0.103 s % 158.57/22.69 % (2699134)Peak memory usage: 12 MB % 158.57/22.69 % (2699134)Instructions burned: 263 (million) % 158.57/22.69 % (2699138)ott-21_1_sil=16000:si=on:fs=off:random_seed=2897523648:i=360:av=off:fsr=off:rtra=on_2799 on theBenchmark for (2799ds/360Mi) % 158.57/22.69 % (2699138)Instruction limit reached! % 158.57/22.69 % (2699138)------------------------------ % 158.57/22.69 % (2699138)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 158.57/22.69 % (2699138)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 158.57/22.69 % (2699138)CaDiCaL version: 2.1.3 % 158.57/22.69 % (2699138)Termination reason: Instruction limit % 158.57/22.69 % (2699138)Termination phase: Saturation % 158.57/22.69 % (2699138)Time elapsed: 0.136 s % 158.57/22.69 % (2699138)Peak memory usage: 12 MB % 158.57/22.69 % (2699138)Instructions burned: 362 (million) % 158.57/22.69 % (2699140)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=488574036:i=954:bd=all:rtra=on_2797 on theBenchmark for (2797ds/954Mi) % 158.57/22.69 % (2699136)Instruction limit reached! % 158.57/22.69 % (2699136)------------------------------ % 158.57/22.69 % (2699136)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 158.57/22.69 % (2699136)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 158.57/22.69 % (2699136)CaDiCaL version: 2.1.3 % 158.57/22.69 % (2699136)Termination reason: Instruction limit % 158.57/22.69 % (2699136)Termination phase: Saturation % 158.57/22.69 % (2699136)Time elapsed: 0.298 s % 158.57/22.69 % (2699136)Peak memory usage: 16 MB % 158.57/22.69 % (2699136)Instructions burned: 1372 (million) % 158.57/22.69 % (2699142)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=1006560047:fmbsr=1.3:i=1730:ins=25:rtra=on_2797 on theBenchmark for (2797ds/1730Mi) % 158.57/22.69 % (2699142)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 158.57/22.69 % (2699142)Terminated due to inappropriate strategy. % 158.57/22.69 % (2699142)------------------------------ % 158.57/22.69 % (2699142)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 158.57/22.69 % (2699142)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 158.57/22.69 % (2699142)CaDiCaL version: 2.1.3 % 158.57/22.69 % (2699142)Termination reason: Inappropriate % 175.87/25.13 % (2699142)Time elapsed: 0.005 s % 175.87/25.13 % (2699142)Peak memory usage: 10 MB % 175.87/25.13 % (2699142)Instructions burned: 24 (million) % 175.87/25.13 % (2699142)------------------------------ % 175.87/25.13 % (2699142)------------------------------ % 175.87/25.13 % (2699144)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=2670910622:i=2358:rtra=on_2796 on theBenchmark for (2796ds/2358Mi) % 175.87/25.13 % (2699140)Instruction limit reached! % 175.87/25.13 % (2699140)------------------------------ % 175.87/25.13 % (2699140)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 175.87/25.13 % (2699140)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 175.87/25.13 % (2699140)CaDiCaL version: 2.1.3 % 175.87/25.13 % (2699140)Termination reason: Instruction limit % 175.87/25.13 % (2699140)Termination phase: Saturation % 175.87/25.13 % (2699140)Time elapsed: 0.367 s % 175.87/25.13 % (2699140)Peak memory usage: 14 MB % 175.87/25.13 % (2699140)Instructions burned: 955 (million) % 175.87/25.13 % (2699146)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=1510802912:i=1778:ins=1:rtra=on_2793 on theBenchmark for (2793ds/1778Mi) % 175.87/25.13 % (2699146)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 175.87/25.13 % (2699146)Terminated due to inappropriate strategy. % 175.87/25.13 % (2699146)------------------------------ % 175.87/25.13 % (2699146)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 175.87/25.13 % (2699146)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 175.87/25.13 % (2699146)CaDiCaL version: 2.1.3 % 175.87/25.13 % (2699146)Termination reason: Inappropriate % 175.87/25.13 % (2699146)Time elapsed: 0.010 s % 175.87/25.13 % (2699146)Peak memory usage: 10 MB % 175.87/25.13 % (2699146)Instructions burned: 24 (million) % 175.87/25.13 % (2699146)------------------------------ % 175.87/25.13 % (2699146)------------------------------ % 175.87/25.13 % (2699148)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=3702712727:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2793 on theBenchmark for (2793ds/1384Mi) % 175.87/25.13 % (2699144)Instruction limit reached! % 175.87/25.13 % (2699144)------------------------------ % 175.87/25.13 % (2699144)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 175.87/25.13 % (2699144)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 175.87/25.13 % (2699144)CaDiCaL version: 2.1.3 % 175.87/25.13 % (2699144)Termination reason: Instruction limit % 175.87/25.13 % (2699144)Termination phase: Saturation % 175.87/25.13 % (2699144)Time elapsed: 0.484 s % 175.87/25.13 % (2699144)Peak memory usage: 13 MB % 175.87/25.13 % (2699144)Instructions burned: 2362 (million) % 175.87/25.13 % (2699150)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=3514439647:i=1758:kws=inv_precedence:fsr=off:rtra=on_2792 on theBenchmark for (2792ds/1758Mi) % 175.87/25.13 % (2699150)Instruction limit reached! % 175.87/25.13 % (2699150)------------------------------ % 175.87/25.13 % (2699150)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 175.87/25.13 % (2699150)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 175.87/25.13 % (2699150)CaDiCaL version: 2.1.3 % 175.87/25.13 % (2699150)Termination reason: Instruction limit % 175.87/25.13 % (2699150)Termination phase: Saturation % 175.87/25.13 % (2699150)Time elapsed: 0.359 s % 175.87/25.13 % (2699150)Peak memory usage: 15 MB % 175.87/25.13 % (2699150)Instructions burned: 1761 (million) % 175.87/25.13 % (2699152)fmb+10_1_sil=64000:si=on:random_seed=2434926293:i=44122:nm=2:rtra=on:gsp=on_2788 on theBenchmark for (2788ds/44122Mi) % 175.87/25.13 % (2699152)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 175.87/25.13 % (2699152)Terminated due to inappropriate strategy. % 175.87/25.13 % (2699152)------------------------------ % 175.87/25.13 % (2699152)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 175.87/25.13 % (2699152)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 175.87/25.13 % (2699152)CaDiCaL version: 2.1.3 % 175.87/25.13 % (2699152)Termination reason: Inappropriate % 175.87/25.13 % (2699152)Time elapsed: 0.007 s % 175.87/25.13 % (2699152)Peak memory usage: 11 MB % 175.87/25.13 % (2699152)Instructions burned: 32 (million) % 175.87/25.13 % (2699148)Instruction limit reached! % 175.87/25.13 % (2699148)------------------------------ % 175.87/25.13 % (2699148)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 175.87/25.13 % (2699148)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 201.89/28.78 % (2699148)CaDiCaL version: 2.1.3 % 201.89/28.78 % (2699148)Termination reason: Instruction limit % 201.89/28.78 % (2699148)Termination phase: Saturation % 201.89/28.78 % (2699148)Time elapsed: 0.527 s % 201.89/28.78 % (2699148)Peak memory usage: 14 MB % 201.89/28.78 % (2699148)Instructions burned: 1384 (million) % 201.89/28.78 % (2699152)------------------------------ % 201.89/28.78 % (2699152)------------------------------ % 201.89/28.78 % (2699154)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=3081388546:i=19030:nm=5:rtra=on_2788 on theBenchmark for (2788ds/19030Mi) % 201.89/28.78 % (2699154)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 201.89/28.78 % (2699154)Terminated due to inappropriate strategy. % 201.89/28.78 % (2699154)------------------------------ % 201.89/28.78 % (2699154)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 201.89/28.78 % (2699154)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 201.89/28.78 % (2699154)CaDiCaL version: 2.1.3 % 201.89/28.78 % (2699154)Termination reason: Inappropriate % 201.89/28.78 % (2699154)Time elapsed: 0.006 s % 201.89/28.78 % (2699154)Peak memory usage: 11 MB % 201.89/28.78 % (2699154)Instructions burned: 31 (million) % 201.89/28.78 % (2699154)------------------------------ % 201.89/28.78 % (2699154)------------------------------ % 201.89/28.78 % (2699155)fmb+10_1_sil=64000:sas=cadical:si=on:fmbss=8:random_seed=1029100642:fmbsr=1.7:i=1840:rtra=on_2788 on theBenchmark for (2788ds/1840Mi) % 201.89/28.78 % (2699157)dis-4_1_sil=16000:drc=ordering:si=on:sp=const_frequency:sac=on:newcnf=on:random_seed=3116198628:i=10262:rtra=on_2787 on theBenchmark for (2787ds/10262Mi) % 201.89/28.78 % (2699155)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 201.89/28.78 % (2699155)Terminated due to inappropriate strategy. % 201.89/28.78 % (2699155)------------------------------ % 201.89/28.78 % (2699155)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 201.89/28.78 % (2699155)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 201.89/28.78 % (2699155)CaDiCaL version: 2.1.3 % 201.89/28.78 % (2699155)Termination reason: Inappropriate % 201.89/28.78 % (2699155)Time elapsed: 0.013 s % 201.89/28.78 % (2699155)Peak memory usage: 11 MB % 201.89/28.78 % (2699155)Instructions burned: 31 (million) % 201.89/28.78 % (2699155)------------------------------ % 201.89/28.78 % (2699155)------------------------------ % 201.89/28.78 % (2699160)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:si=on:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3079050829:i=2944:ins=7:rtra=on:fdi=8:gsp=on_2787 on theBenchmark for (2787ds/2944Mi) % 201.89/28.78 % (2699160)Instruction limit reached! % 201.89/28.78 % (2699160)------------------------------ % 201.89/28.78 % (2699160)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 201.89/28.78 % (2699160)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 201.89/28.78 % (2699160)CaDiCaL version: 2.1.3 % 201.89/28.78 % (2699160)Termination reason: Instruction limit % 201.89/28.78 % (2699160)Termination phase: Saturation % 201.89/28.78 % (2699160)Time elapsed: 1.149 s % 201.89/28.78 % (2699160)Peak memory usage: 17 MB % 201.89/28.78 % (2699160)Instructions burned: 2945 (million) % 201.89/28.78 % (2699162)fmb+10_1_sil=16000:sas=cadical:si=on:bce=on:fmbss=77:random_seed=1929484845:i=12648:rtra=on_2776 on theBenchmark for (2776ds/12648Mi) % 201.89/28.78 % (2699162)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 201.89/28.78 % (2699162)Terminated due to inappropriate strategy. % 201.89/28.78 % (2699162)------------------------------ % 201.89/28.78 % (2699162)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 201.89/28.78 % (2699162)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 201.89/28.78 % (2699162)CaDiCaL version: 2.1.3 % 201.89/28.78 % (2699162)Termination reason: Inappropriate % 201.89/28.78 % (2699162)Time elapsed: 0.013 s % 201.89/28.78 % (2699162)Peak memory usage: 11 MB % 201.89/28.78 % (2699162)Instructions burned: 31 (million) % 201.89/28.78 % (2699162)------------------------------ % 201.89/28.78 % (2699162)------------------------------ % 201.89/28.78 % (2699164)fmb+10_1_fmbas=function:sil=32000:sas=cadical:si=on:fmbss=16:random_seed=2780078390:fmbsr=2.30978:i=4348:rtra=on_2775 on theBenchmark for (2775ds/4348Mi) % 201.89/28.78 % (2699164)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 201.89/28.78 % (2699164)Terminated due to inappropriate strategy. % 201.89/28.78 % (2699164)------------------------------ % 272.87/38.75 % (2699164)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 272.87/38.75 % (2699164)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 272.87/38.75 % (2699164)CaDiCaL version: 2.1.3 % 272.87/38.75 % (2699164)Termination reason: Inappropriate % 272.87/38.75 % (2699164)Time elapsed: 0.013 s % 272.87/38.75 % (2699164)Peak memory usage: 11 MB % 272.87/38.75 % (2699164)Instructions burned: 31 (million) % 272.87/38.75 % (2699164)------------------------------ % 272.87/38.75 % (2699164)------------------------------ % 272.87/38.75 % (2699166)ott-2_1_sil=16000:si=on:newcnf=on:random_seed=3101655383:avsq=on:i=1738:avsqr=1,16:kws=inv_arity_squared:rtra=on_2775 on theBenchmark for (2775ds/1738Mi) % 272.87/38.75 % (2699166)Instruction limit reached! % 272.87/38.75 % (2699166)------------------------------ % 272.87/38.75 % (2699166)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 272.87/38.75 % (2699166)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 272.87/38.75 % (2699166)CaDiCaL version: 2.1.3 % 272.87/38.75 % (2699166)Termination reason: Instruction limit % 272.87/38.75 % (2699166)Termination phase: Saturation % 272.87/38.75 % (2699166)Time elapsed: 0.662 s % 272.87/38.75 % (2699166)Peak memory usage: 14 MB % 272.87/38.75 % (2699166)Instructions burned: 1741 (million) % 272.87/38.75 % (2699168)ott+10_1_sil=32000:tgt=ground:si=on:random_seed=4257859692:i=10228:av=off:rtra=on_2768 on theBenchmark for (2768ds/10228Mi) % 272.87/38.75 % (2699157)Instruction limit reached! % 272.87/38.75 % (2699157)------------------------------ % 272.87/38.75 % (2699157)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 272.87/38.75 % (2699157)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 272.87/38.75 % (2699157)CaDiCaL version: 2.1.3 % 272.87/38.75 % (2699157)Termination reason: Instruction limit % 272.87/38.75 % (2699157)Termination phase: Saturation % 272.87/38.75 % (2699157)Time elapsed: 2.147 s % 272.87/38.75 % (2699157)Peak memory usage: 21 MB % 272.87/38.75 % (2699157)Instructions burned: 10264 (million) % 272.87/38.75 % (2699170)fmb+10_1_sil=64000:sas=cadical:si=on:bce=on:rp=on:random_seed=1940874638:i=108564:rtra=on_2766 on theBenchmark for (2766ds/108564Mi) % 272.87/38.75 % (2699170)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 272.87/38.75 % (2699170)Terminated due to inappropriate strategy. % 272.87/38.75 % (2699170)------------------------------ % 272.87/38.75 % (2699170)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 272.87/38.75 % (2699170)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 272.87/38.75 % (2699170)CaDiCaL version: 2.1.3 % 272.87/38.75 % (2699170)Termination reason: Inappropriate % 272.87/38.75 % (2699170)Time elapsed: 0.007 s % 272.87/38.75 % (2699170)Peak memory usage: 11 MB % 272.87/38.75 % (2699170)Instructions burned: 32 (million) % 272.87/38.75 % (2699170)------------------------------ % 272.87/38.75 % (2699170)------------------------------ % 272.87/38.75 % (2699172)dis-11_1_sil=16000:si=on:sp=reverse_frequency:alpa=true:random_seed=777158975:i=7024:aac=none:rtra=on_2766 on theBenchmark for (2766ds/7024Mi) % 272.87/38.75 % (2698869)Instruction limit reached! % 272.87/38.75 % (2698869)------------------------------ % 272.87/38.75 % (2698869)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 272.87/38.75 % (2698869)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 272.87/38.75 % (2698869)CaDiCaL version: 2.1.3 % 272.87/38.76 % (2698869)Termination reason: Instruction limit % 272.87/38.76 % (2698869)Termination phase: Saturation % 272.87/38.76 % (2698869)Time elapsed: 10.887 s % 272.87/38.76 % (2698869)Peak memory usage: 18 MB % 272.87/38.76 % (2698869)Instructions burned: 28120 (million) % 272.87/38.76 % (2699174)dis+21_1_sil=32000:sas=cadical:si=on:random_seed=1257269010:i=7546:rtra=on:amm=off_2756 on theBenchmark for (2756ds/7546Mi) % 272.87/38.76 % (2699172)Instruction limit reached! % 272.87/38.76 % (2699172)------------------------------ % 272.87/38.76 % (2699172)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 272.87/38.76 % (2699172)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 272.87/38.76 % (2699172)CaDiCaL version: 2.1.3 % 272.87/38.76 % (2699172)Termination reason: Instruction limit % 272.87/38.76 % (2699172)Termination phase: Saturation % 272.87/38.76 % (2699172)Time elapsed: 1.490 s % 272.87/38.76 % (2699172)Peak memory usage: 20 MB % 272.87/38.76 % (2699172)Instructions burned: 7024 (million) % 272.87/38.76 % (2699176)ott+11_1_sil=16000:si=on:gs=on:random_seed=2854328881:s2a=on:i=4502:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:rtra=on:fsd=onTerminated % 300.57/42.64 % Vampire exiting %------------------------------------------------------------------------------