%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : NUM862_1 : TPTP v9.3.1. Released v4.1.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % Computer : 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 12:25:57 PM UTC 2026 % Result : Timeout 300.92s 43.05s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.01 % Problem : NUM862_1 : TPTP v9.3.1. Released v4.1.0. % 0.00/0.02 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.05/0.31 % Computer : n012.cluster.edu % 0.05/0.31 % Model : x86_64 x86_64 % 0.05/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.05/0.31 % Memory : 8046.5625MB % 0.05/0.31 % OS : Linux 6.8.0-71-generic % 0.05/0.31 % CPULimit : 300 % 0.05/0.31 % WCLimit : 300 % 0.05/0.31 % DateTime : Sun Sep 27 21:36:38 UTC 2026 % 0.05/0.31 % CPUTime : % 0.05/0.31 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.07/0.33 Running first-order model finding % 0.07/0.33 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 % 1.87/0.69 % (2766749)Will run a generic schedule for satisfiability detection. % 1.87/0.69 % (2766755)% WARNING: option uhcvi not known. % 1.87/0.69 % (2766756)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2291001662:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 1.87/0.69 % (2766760)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2015583299:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 1.87/0.69 % (2766754)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=739272628_2999 on theBenchmark for (2999ds/0Mi) % 1.87/0.69 % (2766755)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=603537052:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 1.87/0.69 % (2766757)dis+10_1_sil=32000:sp=arity:random_seed=1692032934:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 1.87/0.69 % (2766758)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1462451312:i=116_2999 on theBenchmark for (2999ds/116Mi) % 1.87/0.69 % (2766759)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=4121576814:i=131_2999 on theBenchmark for (2999ds/131Mi) % 1.87/0.69 % (2766754)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 1.87/0.69 % (2766754)Terminated due to inappropriate strategy. % 1.87/0.69 % (2766754)------------------------------ % 1.87/0.69 % (2766754)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 1.87/0.69 % (2766754)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 1.87/0.69 % (2766754)CaDiCaL version: 2.1.3 % 1.87/0.69 % (2766754)Termination reason: Inappropriate % 1.87/0.69 % (2766754)Time elapsed: 0.0000 s % 1.87/0.69 % (2766754)Peak memory usage: 10 MB % 1.87/0.69 % (2766754)Instructions burned: 1 (million) % 1.87/0.69 % (2766754)------------------------------ % 1.87/0.69 % (2766754)------------------------------ % 1.87/0.69 % (2766768)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1491286506:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 1.87/0.69 % (2766768)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 1.87/0.69 % (2766768)Terminated due to inappropriate strategy. % 1.87/0.69 % (2766768)------------------------------ % 1.87/0.69 % (2766768)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 1.87/0.69 % (2766768)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 1.87/0.69 % (2766768)CaDiCaL version: 2.1.3 % 1.87/0.69 % (2766768)Termination reason: Inappropriate % 1.87/0.69 % (2766768)Time elapsed: 0.0000 s % 1.87/0.69 % (2766768)Peak memory usage: 10 MB % 1.87/0.69 % (2766768)Instructions burned: 1 (million) % 1.87/0.69 % (2766768)------------------------------ % 1.87/0.69 % (2766768)------------------------------ % 1.87/0.69 % (2766770)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3983575085:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 1.87/0.69 % (2766757)Instruction limit reached! % 1.87/0.69 % (2766757)------------------------------ % 1.87/0.69 % (2766757)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 1.87/0.69 % (2766757)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 1.87/0.69 % (2766757)CaDiCaL version: 2.1.3 % 1.87/0.69 % (2766757)Termination reason: Instruction limit % 1.87/0.69 % (2766757)Termination phase: Saturation % 1.87/0.69 % (2766757)Time elapsed: 0.037 s % 1.87/0.69 % (2766757)Peak memory usage: 12 MB % 1.87/0.69 % (2766757)Instructions burned: 103 (million) % 1.87/0.69 % (2766758)Instruction limit reached! % 1.87/0.69 % (2766758)------------------------------ % 1.87/0.69 % (2766758)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 1.87/0.69 % (2766758)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 1.87/0.69 % (2766758)CaDiCaL version: 2.1.3 % 1.87/0.69 % (2766758)Termination reason: Instruction limit % 1.87/0.69 % (2766758)Termination phase: Saturation % 1.87/0.69 % (2766758)Time elapsed: 0.039 s % 1.87/0.69 % (2766758)Peak memory usage: 12 MB % 1.87/0.69 % (2766758)Instructions burned: 116 (million) % 1.87/0.69 % (2766759)Instruction limit reached! % 1.87/0.69 % (2766759)------------------------------ % 1.87/0.69 % (2766759)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 1.87/0.69 % (2766759)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 1.87/0.69 % (2766759)CaDiCaL version: 2.1.3 % 1.87/0.69 % (2766759)Termination reason: Instruction limit % 2.68/0.85 % (2766759)Termination phase: Saturation % 2.68/0.85 % (2766759)Time elapsed: 0.047 s % 2.68/0.85 % (2766759)Peak memory usage: 13 MB % 2.68/0.85 % (2766759)Instructions burned: 133 (million) % 2.68/0.85 % (2766772)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=1801549622:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi) % 2.68/0.85 % (2766773)ott-21_1_sil=16000:fs=off:random_seed=3892140205:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi) % 2.68/0.85 % (2766774)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3188322913:i=477:bd=all_2999 on theBenchmark for (2999ds/477Mi) % 2.68/0.85 % (2766760)Instruction limit reached! % 2.68/0.85 % (2766760)------------------------------ % 2.68/0.85 % (2766760)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 2.68/0.85 % (2766760)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 2.68/0.85 % (2766760)CaDiCaL version: 2.1.3 % 2.68/0.85 % (2766760)Termination reason: Instruction limit % 2.68/0.85 % (2766760)Termination phase: Saturation % 2.68/0.85 % (2766760)Time elapsed: 0.059 s % 2.68/0.85 % (2766760)Peak memory usage: 14 MB % 2.68/0.85 % (2766760)Instructions burned: 159 (million) % 2.68/0.85 % (2766770)Instruction limit reached! % 2.68/0.85 % (2766770)------------------------------ % 2.68/0.85 % (2766770)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 2.68/0.85 % (2766770)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 2.68/0.85 % (2766770)CaDiCaL version: 2.1.3 % 2.68/0.85 % (2766770)Termination reason: Instruction limit % 2.68/0.85 % (2766770)Termination phase: Saturation % 2.68/0.85 % (2766770)Time elapsed: 0.042 s % 2.68/0.85 % (2766770)Peak memory usage: 12 MB % 2.68/0.85 % (2766770)Instructions burned: 134 (million) % 2.68/0.85 % (2766778)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3590111547:fmbsr=1.3:i=865:ins=25_2999 on theBenchmark for (2999ds/865Mi) % 2.68/0.85 % (2766778)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 2.68/0.85 % (2766778)Terminated due to inappropriate strategy. % 2.68/0.85 % (2766778)------------------------------ % 2.68/0.85 % (2766778)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 2.68/0.85 % (2766778)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 2.68/0.85 % (2766778)CaDiCaL version: 2.1.3 % 2.68/0.85 % (2766778)Termination reason: Inappropriate % 2.68/0.85 % (2766778)Time elapsed: 0.0000 s % 2.68/0.85 % (2766778)Peak memory usage: 10 MB % 2.68/0.85 % (2766778)Instructions burned: 1 (million) % 2.68/0.85 % (2766778)------------------------------ % 2.68/0.85 % (2766778)------------------------------ % 2.68/0.85 % (2766780)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=4099894964:i=1179_2999 on theBenchmark for (2999ds/1179Mi) % 2.68/0.85 % (2766781)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3762241142:i=889:ins=1_2999 on theBenchmark for (2999ds/889Mi) % 2.68/0.85 % (2766781)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 2.68/0.85 % (2766781)Terminated due to inappropriate strategy. % 2.68/0.85 % (2766781)------------------------------ % 2.68/0.85 % (2766781)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 2.68/0.85 % (2766781)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 2.68/0.85 % (2766781)CaDiCaL version: 2.1.3 % 2.68/0.85 % (2766781)Termination reason: Inappropriate % 2.68/0.85 % (2766781)Time elapsed: 0.0000 s % 2.68/0.85 % (2766781)Peak memory usage: 10 MB % 2.68/0.85 % (2766781)Instructions burned: 1 (million) % 2.68/0.85 % (2766781)------------------------------ % 2.68/0.85 % (2766781)------------------------------ % 2.68/0.85 % (2766784)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=3471339075:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2998 on theBenchmark for (2998ds/692Mi) % 2.68/0.85 % (2766773)Instruction limit reached! % 2.68/0.85 % (2766773)------------------------------ % 2.68/0.85 % (2766773)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 2.68/0.85 % (2766773)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 2.68/0.85 % (2766773)CaDiCaL version: 2.1.3 % 2.68/0.85 % (2766773)Termination reason: Instruction limit % 2.68/0.85 % (2766773)Termination phase: Saturation % 11.72/2.09 % (2766773)Time elapsed: 0.043 s % 11.72/2.09 % (2766773)Peak memory usage: 12 MB % 11.72/2.09 % (2766773)Instructions burned: 182 (million) % 11.72/2.09 % (2766786)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3998051511:i=879:kws=inv_precedence:fsr=off_2998 on theBenchmark for (2998ds/879Mi) % 11.72/2.09 % (2766774)Instruction limit reached! % 11.72/2.09 % (2766774)------------------------------ % 11.72/2.09 % (2766774)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 11.72/2.09 % (2766774)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.72/2.09 % (2766774)CaDiCaL version: 2.1.3 % 11.72/2.09 % (2766774)Termination reason: Instruction limit % 11.72/2.09 % (2766774)Termination phase: Saturation % 11.72/2.09 % (2766774)Time elapsed: 0.175 s % 11.72/2.09 % (2766774)Peak memory usage: 14 MB % 11.72/2.09 % (2766774)Instructions burned: 479 (million) % 11.72/2.09 % (2766788)fmb+10_1_sil=64000:random_seed=2810796110:i=22061:nm=2:gsp=on_2997 on theBenchmark for (2997ds/22061Mi) % 11.72/2.09 % (2766788)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 11.72/2.09 % (2766788)Terminated due to inappropriate strategy. % 11.72/2.09 % (2766788)------------------------------ % 11.72/2.09 % (2766788)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 11.72/2.09 % (2766788)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.72/2.09 % (2766788)CaDiCaL version: 2.1.3 % 11.72/2.09 % (2766788)Termination reason: Inappropriate % 11.72/2.09 % (2766788)Time elapsed: 0.0000 s % 11.72/2.09 % (2766788)Peak memory usage: 10 MB % 11.72/2.09 % (2766788)Instructions burned: 1 (million) % 11.72/2.09 % (2766788)------------------------------ % 11.72/2.09 % (2766788)------------------------------ % 11.72/2.09 % (2766772)Instruction limit reached! % 11.72/2.09 % (2766772)------------------------------ % 11.72/2.09 % (2766772)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 11.72/2.09 % (2766772)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.72/2.09 % (2766772)CaDiCaL version: 2.1.3 % 11.72/2.09 % (2766772)Termination reason: Instruction limit % 11.72/2.09 % (2766772)Termination phase: Saturation % 11.72/2.09 % (2766772)Time elapsed: 0.202 s % 11.72/2.09 % (2766772)Peak memory usage: 15 MB % 11.72/2.09 % (2766772)Instructions burned: 685 (million) % 11.72/2.09 % (2766790)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3948340873:i=9515:nm=5_2997 on theBenchmark for (2997ds/9515Mi) % 11.72/2.09 % (2766790)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 11.72/2.09 % (2766790)Terminated due to inappropriate strategy. % 11.72/2.09 % (2766790)------------------------------ % 11.72/2.09 % (2766790)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 11.72/2.09 % (2766790)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.72/2.09 % (2766790)CaDiCaL version: 2.1.3 % 11.72/2.09 % (2766790)Termination reason: Inappropriate % 11.72/2.09 % (2766790)Time elapsed: 0.0000 s % 11.72/2.09 % (2766790)Peak memory usage: 10 MB % 11.72/2.09 % (2766790)Instructions burned: 1 (million) % 11.72/2.09 % (2766790)------------------------------ % 11.72/2.09 % (2766790)------------------------------ % 11.72/2.09 % (2766791)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2885297576:fmbsr=1.7:i=920_2997 on theBenchmark for (2997ds/920Mi) % 11.72/2.09 % (2766791)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 11.72/2.09 % (2766791)Terminated due to inappropriate strategy. % 11.72/2.09 % (2766791)------------------------------ % 11.72/2.09 % (2766791)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 11.72/2.09 % (2766791)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.72/2.09 % (2766791)CaDiCaL version: 2.1.3 % 11.72/2.09 % (2766791)Termination reason: Inappropriate % 11.72/2.09 % (2766791)Time elapsed: 0.0000 s % 11.72/2.09 % (2766791)Peak memory usage: 10 MB % 11.72/2.09 % (2766791)Instructions burned: 1 (million) % 11.72/2.09 % (2766791)------------------------------ % 11.72/2.09 % (2766791)------------------------------ % 11.72/2.09 % (2766793)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=3984461545:i=5131_2997 on theBenchmark for (2997ds/5131Mi) % 11.72/2.09 % (2766795)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1515582483:i=1472:ins=7:fdi=8:gsp=on_2997 on theBenchmark for (2997ds/1472Mi) % 11.72/2.09 % (2766784)Instruction limit reached! % 11.72/2.09 % (2766784)------------------------------ % 13.85/2.45 % (2766784)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 13.85/2.45 % (2766784)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.85/2.45 % (2766784)CaDiCaL version: 2.1.3 % 13.85/2.45 % (2766784)Termination reason: Instruction limit % 13.85/2.45 % (2766784)Termination phase: Saturation % 13.85/2.45 % (2766784)Time elapsed: 0.233 s % 13.85/2.45 % (2766784)Peak memory usage: 18 MB % 13.85/2.45 % (2766784)Instructions burned: 693 (million) % 13.85/2.45 % (2766798)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=712622613:i=6324_2996 on theBenchmark for (2996ds/6324Mi) % 13.85/2.45 % (2766798)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 13.85/2.45 % (2766798)Terminated due to inappropriate strategy. % 13.85/2.45 % (2766798)------------------------------ % 13.85/2.45 % (2766798)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 13.85/2.45 % (2766798)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.85/2.45 % (2766798)CaDiCaL version: 2.1.3 % 13.85/2.45 % (2766798)Termination reason: Inappropriate % 13.85/2.45 % (2766798)Time elapsed: 0.0000 s % 13.85/2.45 % (2766798)Peak memory usage: 10 MB % 13.85/2.45 % (2766798)Instructions burned: 1 (million) % 13.85/2.45 % (2766798)------------------------------ % 13.85/2.45 % (2766798)------------------------------ % 13.85/2.45 % (2766800)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1132530207:fmbsr=2.30978:i=2174_2996 on theBenchmark for (2996ds/2174Mi) % 13.85/2.45 % (2766800)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 13.85/2.45 % (2766800)Terminated due to inappropriate strategy. % 13.85/2.45 % (2766800)------------------------------ % 13.85/2.45 % (2766800)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 13.85/2.45 % (2766800)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.85/2.45 % (2766800)CaDiCaL version: 2.1.3 % 13.85/2.45 % (2766800)Termination reason: Inappropriate % 13.85/2.45 % (2766800)Time elapsed: 0.0000 s % 13.85/2.45 % (2766800)Peak memory usage: 10 MB % 13.85/2.45 % (2766800)Instructions burned: 1 (million) % 13.85/2.45 % (2766800)------------------------------ % 13.85/2.45 % (2766800)------------------------------ % 13.85/2.45 % (2766802)ott-2_1_sil=16000:newcnf=on:random_seed=2396903885:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2996 on theBenchmark for (2996ds/869Mi) % 13.85/2.45 % (2766786)Instruction limit reached! % 13.85/2.45 % (2766786)------------------------------ % 13.85/2.45 % (2766786)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 13.85/2.45 % (2766786)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.85/2.45 % (2766786)CaDiCaL version: 2.1.3 % 13.85/2.45 % (2766786)Termination reason: Instruction limit % 13.85/2.45 % (2766786)Termination phase: Saturation % 13.85/2.45 % (2766786)Time elapsed: 0.279 s % 13.85/2.45 % (2766786)Peak memory usage: 18 MB % 13.85/2.45 % (2766786)Instructions burned: 880 (million) % 13.85/2.45 % (2766804)ott+10_1_sil=32000:tgt=ground:random_seed=419329217:i=5114:av=off_2995 on theBenchmark for (2995ds/5114Mi) % 13.85/2.45 % (2766780)Instruction limit reached! % 13.85/2.45 % (2766780)------------------------------ % 13.85/2.45 % (2766780)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 13.85/2.45 % (2766780)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.85/2.45 % (2766780)CaDiCaL version: 2.1.3 % 13.85/2.45 % (2766780)Termination reason: Instruction limit % 13.85/2.45 % (2766780)Termination phase: Saturation % 13.85/2.45 % (2766780)Time elapsed: 0.396 s % 13.85/2.45 % (2766780)Peak memory usage: 18 MB % 13.85/2.45 % (2766780)Instructions burned: 1180 (million) % 13.85/2.45 % (2766806)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2874709980:i=54282_2994 on theBenchmark for (2994ds/54282Mi) % 13.85/2.45 % (2766806)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 13.85/2.45 % (2766806)Terminated due to inappropriate strategy. % 13.85/2.45 % (2766806)------------------------------ % 13.85/2.45 % (2766806)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 13.85/2.45 % (2766806)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.85/2.45 % (2766806)CaDiCaL version: 2.1.3 % 13.85/2.45 % (2766806)Termination reason: Inappropriate % 13.85/2.45 % (2766806)Time elapsed: 0.0000 s % 13.85/2.45 % (2766806)Peak memory usage: 10 MB % 13.85/2.45 % (2766806)Instructions burned: 1 (million) % 61.80/9.13 % (2766806)------------------------------ % 61.80/9.13 % (2766806)------------------------------ % 61.80/9.13 % (2766808)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=2258424014:i=3512:aac=none_2994 on theBenchmark for (2994ds/3512Mi) % 61.80/9.13 % (2766802)Instruction limit reached! % 61.80/9.13 % (2766802)------------------------------ % 61.80/9.13 % (2766802)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 61.80/9.13 % (2766802)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 61.80/9.13 % (2766802)CaDiCaL version: 2.1.3 % 61.80/9.13 % (2766802)Termination reason: Instruction limit % 61.80/9.13 % (2766802)Termination phase: Saturation % 61.80/9.13 % (2766802)Time elapsed: 0.263 s % 61.80/9.13 % (2766802)Peak memory usage: 17 MB % 61.80/9.13 % (2766802)Instructions burned: 870 (million) % 61.80/9.13 % (2766810)dis+21_1_sil=32000:sas=cadical:random_seed=2440313110:i=3773:amm=off_2993 on theBenchmark for (2993ds/3773Mi) % 61.80/9.13 % (2766795)Instruction limit reached! % 61.80/9.13 % (2766795)------------------------------ % 61.80/9.13 % (2766795)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 61.80/9.13 % (2766795)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 61.80/9.13 % (2766795)CaDiCaL version: 2.1.3 % 61.80/9.13 % (2766795)Termination reason: Instruction limit % 61.80/9.13 % (2766795)Termination phase: Saturation % 61.80/9.13 % (2766795)Time elapsed: 0.450 s % 61.80/9.13 % (2766795)Peak memory usage: 27 MB % 61.80/9.13 % (2766795)Instructions burned: 1475 (million) % 61.80/9.13 % (2766812)ott+11_1_sil=16000:gs=on:random_seed=1739296756:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2992 on theBenchmark for (2992ds/2251Mi) % 61.80/9.13 % (2766812)Instruction limit reached! % 61.80/9.13 % (2766812)------------------------------ % 61.80/9.13 % (2766812)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 61.80/9.13 % (2766812)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 61.80/9.13 % (2766812)CaDiCaL version: 2.1.3 % 61.80/9.13 % (2766812)Termination reason: Instruction limit % 61.80/9.13 % (2766812)Termination phase: Saturation % 61.80/9.13 % (2766812)Time elapsed: 0.627 s % 61.80/9.13 % (2766812)Peak memory usage: 17 MB % 61.80/9.13 % (2766812)Instructions burned: 2253 (million) % 61.80/9.13 % (2766814)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=463636504:fmbsr=1.6:i=67534_2986 on theBenchmark for (2986ds/67534Mi) % 61.80/9.13 % (2766814)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 61.80/9.13 % (2766814)Terminated due to inappropriate strategy. % 61.80/9.13 % (2766814)------------------------------ % 61.80/9.13 % (2766814)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 61.80/9.13 % (2766814)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 61.80/9.13 % (2766814)CaDiCaL version: 2.1.3 % 61.80/9.13 % (2766814)Termination reason: Inappropriate % 61.80/9.13 % (2766814)Time elapsed: 0.0000 s % 61.80/9.13 % (2766814)Peak memory usage: 10 MB % 61.80/9.13 % (2766814)Instructions burned: 1 (million) % 61.80/9.13 % (2766814)------------------------------ % 61.80/9.13 % (2766814)------------------------------ % 61.80/9.13 % (2766816)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=1755577433:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2985 on theBenchmark for (2985ds/4591Mi) % 61.80/9.13 % (2766808)Instruction limit reached! % 61.80/9.13 % (2766808)------------------------------ % 61.80/9.13 % (2766808)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 61.80/9.13 % (2766808)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 61.80/9.13 % (2766808)CaDiCaL version: 2.1.3 % 61.80/9.13 % (2766808)Termination reason: Instruction limit % 61.80/9.13 % (2766808)Termination phase: Saturation % 61.80/9.13 % (2766808)Time elapsed: 0.997 s % 61.80/9.13 % (2766808)Peak memory usage: 30 MB % 61.80/9.13 % (2766808)Instructions burned: 3514 (million) % 61.80/9.13 % (2766818)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=414561499:i=29340_2984 on theBenchmark for (2984ds/29340Mi) % 61.80/9.13 % (2766793)Instruction limit reached! % 61.80/9.13 % (2766793)------------------------------ % 61.80/9.13 % (2766793)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 61.80/9.13 % (2766793)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 61.80/9.13 % (2766793)CaDiCaL version: 2.1.3 % 61.80/9.13 % (2766793)Termination reason: Instruction limit % 72.50/10.83 % (2766793)Termination phase: Saturation % 72.50/10.83 % (2766793)Time elapsed: 1.455 s % 72.50/10.83 % (2766793)Peak memory usage: 40 MB % 72.50/10.83 % (2766793)Instructions burned: 5132 (million) % 72.50/10.83 % (2766810)Instruction limit reached! % 72.50/10.83 % (2766810)------------------------------ % 72.50/10.83 % (2766810)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 72.50/10.83 % (2766810)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 72.50/10.83 % (2766810)CaDiCaL version: 2.1.3 % 72.50/10.83 % (2766810)Termination reason: Instruction limit % 72.50/10.83 % (2766810)Termination phase: Saturation % 72.50/10.83 % (2766810)Time elapsed: 1.091 s % 72.50/10.83 % (2766810)Peak memory usage: 30 MB % 72.50/10.83 % (2766810)Instructions burned: 3777 (million) % 72.50/10.83 % (2766821)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=1332656747:i=5497:nm=2_2982 on theBenchmark for (2982ds/5497Mi) % 72.50/10.83 % (2766820)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=3573122833:i=5211_2982 on theBenchmark for (2982ds/5211Mi) % 72.50/10.83 % (2766821)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 72.50/10.83 % (2766821)Terminated due to inappropriate strategy. % 72.50/10.83 % (2766821)------------------------------ % 72.50/10.83 % (2766821)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 72.50/10.83 % (2766821)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 72.50/10.83 % (2766821)CaDiCaL version: 2.1.3 % 72.50/10.83 % (2766821)Termination reason: Inappropriate % 72.50/10.83 % (2766821)Time elapsed: 0.0000 s % 72.50/10.83 % (2766821)Peak memory usage: 10 MB % 72.50/10.83 % (2766821)Instructions burned: 1 (million) % 72.50/10.83 % (2766821)------------------------------ % 72.50/10.83 % (2766821)------------------------------ % 72.50/10.83 % (2766824)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=3306345968:fmbsr=2:i=46332_2982 on theBenchmark for (2982ds/46332Mi) % 72.50/10.83 % (2766824)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 72.50/10.83 % (2766824)Terminated due to inappropriate strategy. % 72.50/10.83 % (2766824)------------------------------ % 72.50/10.83 % (2766824)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 72.50/10.83 % (2766824)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 72.50/10.83 % (2766824)CaDiCaL version: 2.1.3 % 72.50/10.83 % (2766824)Termination reason: Inappropriate % 72.50/10.83 % (2766824)Time elapsed: 0.0000 s % 72.50/10.83 % (2766824)Peak memory usage: 10 MB % 72.50/10.83 % (2766824)Instructions burned: 1 (million) % 72.50/10.83 % (2766824)------------------------------ % 72.50/10.83 % (2766824)------------------------------ % 72.50/10.83 % (2766826)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=946370856:i=14071_2982 on theBenchmark for (2982ds/14071Mi) % 72.50/10.83 % (2766826)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 72.50/10.83 % (2766826)Terminated due to inappropriate strategy. % 72.50/10.83 % (2766826)------------------------------ % 72.50/10.83 % (2766826)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 72.50/10.83 % (2766826)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 72.50/10.83 % (2766826)CaDiCaL version: 2.1.3 % 72.50/10.83 % (2766826)Termination reason: Inappropriate % 72.50/10.83 % (2766826)Time elapsed: 0.0000 s % 72.50/10.83 % (2766826)Peak memory usage: 10 MB % 72.50/10.83 % (2766826)Instructions burned: 1 (million) % 72.50/10.83 % (2766826)------------------------------ % 72.50/10.83 % (2766826)------------------------------ % 72.50/10.83 % (2766828)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3922419645:i=22565:add=on:rawr=on_2982 on theBenchmark for (2982ds/22565Mi) % 72.50/10.83 % (2766804)Instruction limit reached! % 72.50/10.83 % (2766804)------------------------------ % 72.50/10.83 % (2766804)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 72.50/10.83 % (2766804)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 72.50/10.83 % (2766804)CaDiCaL version: 2.1.3 % 72.50/10.83 % (2766804)Termination reason: Instruction limit % 72.50/10.83 % (2766804)Termination phase: Saturation % 72.50/10.83 % (2766804)Time elapsed: 1.679 s % 72.50/10.83 % (2766804)Peak memory usage: 32 MB % 72.50/10.83 % (2766804)Instructions burned: 5116 (million) % 72.50/10.83 % (2766830)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=1321793036:i=8173:av=off_2978 on theBenchmark for (2978ds/8173Mi) % 72.50/10.89 % (2766816)Instruction limit reached! % 72.50/10.89 % (2766816)------------------------------ % 72.50/10.89 % (2766816)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 72.50/10.89 % (2766816)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 72.50/10.89 % (2766816)CaDiCaL version: 2.1.3 % 72.50/10.89 % (2766816)Termination reason: Instruction limit % 72.50/10.89 % (2766816)Termination phase: Saturation % 72.50/10.89 % (2766816)Time elapsed: 1.027 s % 72.50/10.89 % (2766816)Peak memory usage: 33 MB % 72.50/10.89 % (2766816)Instructions burned: 4593 (million) % 72.50/10.89 % (2766832)dis+10_16:1_sil=16000:random_seed=3361246979:i=9155:fsr=off_2975 on theBenchmark for (2975ds/9155Mi) % 72.50/10.89 % (2766820)Instruction limit reached! % 72.50/10.89 % (2766820)------------------------------ % 72.50/10.89 % (2766820)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 72.50/10.89 % (2766820)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 72.50/10.89 % (2766820)CaDiCaL version: 2.1.3 % 72.50/10.89 % (2766820)Termination reason: Instruction limit % 72.50/10.89 % (2766820)Termination phase: Saturation % 72.50/10.89 % (2766820)Time elapsed: 1.478 s % 72.50/10.89 % (2766820)Peak memory usage: 45 MB % 72.50/10.89 % (2766820)Instructions burned: 5211 (million) % 72.50/10.89 % (2766834)ott-3_8_sil=64000:random_seed=1151085332:i=20139:bs=on_2967 on theBenchmark for (2967ds/20139Mi) % 72.50/10.89 % (2766830)Instruction limit reached! % 72.50/10.89 % (2766830)------------------------------ % 72.50/10.89 % (2766830)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 72.50/10.89 % (2766830)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 72.50/10.89 % (2766830)CaDiCaL version: 2.1.3 % 72.50/10.89 % (2766830)Termination reason: Instruction limit % 72.50/10.89 % (2766830)Termination phase: Saturation % 72.50/10.89 % (2766830)Time elapsed: 2.664 s % 72.50/10.89 % (2766830)Peak memory usage: 66 MB % 72.50/10.89 % (2766830)Instructions burned: 8173 (million) % 72.50/10.89 % (2766836)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=1897643718:fmbsr=2:i=32576_2952 on theBenchmark for (2952ds/32576Mi) % 72.50/10.89 % (2766836)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 72.50/10.89 % (2766836)Terminated due to inappropriate strategy. % 72.50/10.89 % (2766836)------------------------------ % 72.50/10.89 % (2766836)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 72.50/10.89 % (2766836)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 72.50/10.89 % (2766836)CaDiCaL version: 2.1.3 % 72.50/10.89 % (2766836)Termination reason: Inappropriate % 72.50/10.89 % (2766836)Time elapsed: 0.0000 s % 72.50/10.89 % (2766836)Peak memory usage: 10 MB % 72.50/10.89 % (2766836)Instructions burned: 1 (million) % 72.50/10.89 % (2766836)------------------------------ % 72.50/10.89 % (2766836)------------------------------ % 72.50/10.89 % (2766838)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=4044287356:i=11404_2952 on theBenchmark for (2952ds/11404Mi) % 72.50/10.89 % (2766832)Instruction limit reached! % 72.50/10.89 % (2766832)------------------------------ % 72.50/10.89 % (2766832)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 72.50/10.89 % (2766832)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 72.50/10.89 % (2766832)CaDiCaL version: 2.1.3 % 72.50/10.89 % (2766832)Termination reason: Instruction limit % 72.50/10.89 % (2766832)Termination phase: Saturation % 72.50/10.89 % (2766832)Time elapsed: 2.468 s % 72.50/10.89 % (2766832)Peak memory usage: 49 MB % 72.50/10.89 % (2766832)Instructions burned: 9159 (million) % 72.50/10.89 % (2766840)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=1910199734:i=14134_2950 on theBenchmark for (2950ds/14134Mi) % 72.50/10.89 % (2766828)Instruction limit reached! % 72.50/10.89 % (2766828)------------------------------ % 72.50/10.89 % (2766828)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 72.50/10.89 % (2766828)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 72.50/10.89 % (2766828)CaDiCaL version: 2.1.3 % 72.50/10.89 % (2766828)Termination reason: Instruction limit % 72.50/10.89 % (2766828)Termination phase: Saturation % 72.50/10.89 % (2766828)Time elapsed: 5.202 s % 72.50/10.89 % (2766828)Peak memory usage: 81 MB % 72.50/10.89 % (2766828)Instructions burned: 22565 (million) % 72.50/10.89 % (2766842)dis+33_16_sil=32000:sac=on:random_seed=2722971755:i=15851:nm=0_2929 on theBenchmark for (2929ds/15851Mi) % 72.50/10.89 % (2766838)Instruction limit reached! % 72.50/10.89 % (2766838)------------------------------ % 72.50/10.89 % (2766838)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 101.08/14.74 % (2766838)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 101.08/14.74 % (2766838)CaDiCaL version: 2.1.3 % 101.08/14.74 % (2766838)Termination reason: Instruction limit % 101.08/14.74 % (2766838)Termination phase: Saturation % 101.08/14.74 % (2766838)Time elapsed: 3.989 s % 101.08/14.74 % (2766838)Peak memory usage: 51 MB % 101.08/14.74 % (2766838)Instructions burned: 11404 (million) % 101.08/14.74 % (2766844)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=1599609938:avsq=on:i=17627:add=on:amm=off_2912 on theBenchmark for (2912ds/17627Mi) % 101.08/14.74 % (2766818)Instruction limit reached! % 101.08/14.74 % (2766818)------------------------------ % 101.08/14.74 % (2766818)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 101.08/14.74 % (2766818)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 101.08/14.74 % (2766818)CaDiCaL version: 2.1.3 % 101.08/14.74 % (2766818)Termination reason: Instruction limit % 101.08/14.74 % (2766818)Termination phase: Saturation % 101.08/14.74 % (2766818)Time elapsed: 8.249 s % 101.08/14.74 % (2766818)Peak memory usage: 394 MB % 101.08/14.74 % (2766818)Instructions burned: 29342 (million) % 101.08/14.74 % (2766846)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=621787373:s2a=on:i=53295_2901 on theBenchmark for (2901ds/53295Mi) % 101.08/14.74 % (2766840)Instruction limit reached! % 101.08/14.74 % (2766840)------------------------------ % 101.08/14.74 % (2766840)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 101.08/14.74 % (2766840)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 101.08/14.74 % (2766840)CaDiCaL version: 2.1.3 % 101.08/14.74 % (2766840)Termination reason: Instruction limit % 101.08/14.74 % (2766840)Termination phase: Saturation % 101.08/14.74 % (2766840)Time elapsed: 4.978 s % 101.08/14.74 % (2766840)Peak memory usage: 63 MB % 101.08/14.74 % (2766840)Instructions burned: 14135 (million) % 101.08/14.74 % (2766848)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=1526971232:i=26857:ins=20_2900 on theBenchmark for (2900ds/26857Mi) % 101.08/14.74 % (2766848)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 101.08/14.74 % (2766848)Terminated due to inappropriate strategy. % 101.08/14.74 % (2766848)------------------------------ % 101.08/14.74 % (2766848)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 101.08/14.74 % (2766848)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 101.08/14.74 % (2766848)CaDiCaL version: 2.1.3 % 101.08/14.74 % (2766848)Termination reason: Inappropriate % 101.08/14.74 % (2766848)Time elapsed: 0.0000 s % 101.08/14.74 % (2766848)Peak memory usage: 10 MB % 101.08/14.74 % (2766848)Instructions burned: 1 (million) % 101.08/14.74 % (2766848)------------------------------ % 101.08/14.74 % (2766848)------------------------------ % 101.08/14.74 % (2766850)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=3878994202:i=28120:bs=on:fsr=off_2900 on theBenchmark for (2900ds/28120Mi) % 101.08/14.74 % (2766834)Instruction limit reached! % 101.08/14.74 % (2766834)------------------------------ % 101.08/14.74 % (2766834)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 101.08/14.74 % (2766834)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 101.08/14.74 % (2766834)CaDiCaL version: 2.1.3 % 101.08/14.74 % (2766834)Termination reason: Instruction limit % 101.08/14.74 % (2766834)Termination phase: Saturation % 101.08/14.74 % (2766834)Time elapsed: 7.209 s % 101.08/14.74 % (2766834)Peak memory usage: 76 MB % 101.08/14.74 % (2766834)Instructions burned: 20140 (million) % 101.08/14.74 % (2766852)fmb+10_1_sil=256000:fmbss=7:random_seed=3930997288:fmbsr=1.6:i=182295_2895 on theBenchmark for (2895ds/182295Mi) % 101.08/14.74 % (2766852)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 101.08/14.74 % (2766852)Terminated due to inappropriate strategy. % 101.08/14.74 % (2766852)------------------------------ % 101.08/14.74 % (2766852)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 101.08/14.74 % (2766852)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 101.08/14.74 % (2766852)CaDiCaL version: 2.1.3 % 101.08/14.74 % (2766852)Termination reason: Inappropriate % 101.08/14.74 % (2766852)Time elapsed: 0.0000 s % 101.08/14.74 % (2766852)Peak memory usage: 10 MB % 101.08/14.74 % (2766852)Instructions burned: 1 (million) % 101.08/14.74 % (2766852)------------------------------ % 101.08/14.74 % (2766852)------------------------------ % 101.08/14.74 % (2766854)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=3296376526:i=44625:gsp=on_2895 on theBenchmark for (2895ds/44625Mi) % 107.92/15.76 % (2766854)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 107.92/15.76 % (2766854)Terminated due to inappropriate strategy. % 107.92/15.76 % (2766854)------------------------------ % 107.92/15.76 % (2766854)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 107.92/15.76 % (2766854)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 107.92/15.76 % (2766854)CaDiCaL version: 2.1.3 % 107.92/15.76 % (2766854)Termination reason: Inappropriate % 107.92/15.76 % (2766854)Time elapsed: 0.0000 s % 107.92/15.76 % (2766854)Peak memory usage: 11 MB % 107.92/15.76 % (2766854)Instructions burned: 1 (million) % 107.92/15.76 % (2766854)------------------------------ % 107.92/15.76 % (2766854)------------------------------ % 107.92/15.76 % (2766856)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=2234257512:i=160505_2895 on theBenchmark for (2895ds/160505Mi) % 107.92/15.76 % (2766856)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 107.92/15.76 % (2766856)Terminated due to inappropriate strategy. % 107.92/15.76 % (2766856)------------------------------ % 107.92/15.76 % (2766856)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 107.92/15.76 % (2766856)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 107.92/15.76 % (2766856)CaDiCaL version: 2.1.3 % 107.92/15.76 % (2766856)Termination reason: Inappropriate % 107.92/15.76 % (2766856)Time elapsed: 0.0000 s % 107.92/15.76 % (2766856)Peak memory usage: 10 MB % 107.92/15.76 % (2766856)Instructions burned: 1 (million) % 107.92/15.76 % (2766856)------------------------------ % 107.92/15.76 % (2766856)------------------------------ % 107.92/15.76 % (2766858)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=3833652292:fmbsr=1.3:i=225729_2894 on theBenchmark for (2894ds/225729Mi) % 107.92/15.76 % (2766858)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 107.92/15.76 % (2766858)Terminated due to inappropriate strategy. % 107.92/15.76 % (2766858)------------------------------ % 107.92/15.76 % (2766858)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 107.92/15.76 % (2766858)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 107.92/15.76 % (2766858)CaDiCaL version: 2.1.3 % 107.92/15.76 % (2766858)Termination reason: Inappropriate % 107.92/15.76 % (2766858)Time elapsed: 0.0000 s % 107.92/15.76 % (2766858)Peak memory usage: 10 MB % 107.92/15.76 % (2766858)Instructions burned: 1 (million) % 107.92/15.76 % (2766858)------------------------------ % 107.92/15.76 % (2766858)------------------------------ % 107.92/15.76 % (2766860)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=580331434:fmbsr=2:i=185024:ins=7_2894 on theBenchmark for (2894ds/185024Mi) % 107.92/15.76 % (2766860)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 107.92/15.76 % (2766860)Terminated due to inappropriate strategy. % 107.92/15.76 % (2766860)------------------------------ % 107.92/15.76 % (2766860)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 107.92/15.76 % (2766860)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 107.92/15.76 % (2766860)CaDiCaL version: 2.1.3 % 107.92/15.76 % (2766860)Termination reason: Inappropriate % 107.92/15.76 % (2766860)Time elapsed: 0.0000 s % 107.92/15.76 % (2766860)Peak memory usage: 10 MB % 107.92/15.76 % (2766860)Instructions burned: 1 (million) % 107.92/15.76 % (2766860)------------------------------ % 107.92/15.76 % (2766860)------------------------------ % 107.92/15.76 % (2766862)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=4116050559:rtra=on_2894 on theBenchmark for (2894ds/0Mi) % 107.92/15.76 % (2766862)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 107.92/15.76 % (2766862)Terminated due to inappropriate strategy. % 107.92/15.76 % (2766862)------------------------------ % 107.92/15.76 % (2766862)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 107.92/15.76 % (2766862)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 107.92/15.76 % (2766862)CaDiCaL version: 2.1.3 % 107.92/15.76 % (2766862)Termination reason: Inappropriate % 107.92/15.76 % (2766862)Time elapsed: 0.0000 s % 107.92/15.76 % (2766862)Peak memory usage: 10 MB % 107.92/15.76 % (2766862)Instructions burned: 1 (million) % 107.92/15.76 % (2766862)------------------------------ % 107.92/15.76 % (2766862)------------------------------ % 107.92/15.76 % (2766864)% WARNING: option uhcvi not known. % 107.92/15.76 % (2766864)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=665830150:i=271062:add=off:rtra=on:rawr=on_2894 on theBenchmark for (2894ds/271062Mi) % 118.85/17.20 % (2766842)Instruction limit reached! % 118.85/17.20 % (2766842)------------------------------ % 118.85/17.20 % (2766842)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 118.85/17.20 % (2766842)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 118.85/17.20 % (2766842)CaDiCaL version: 2.1.3 % 118.85/17.20 % (2766842)Termination reason: Instruction limit % 118.85/17.20 % (2766842)Termination phase: Saturation % 118.85/17.20 % (2766842)Time elapsed: 4.553 s % 118.85/17.20 % (2766842)Peak memory usage: 128 MB % 118.85/17.20 % (2766842)Instructions burned: 15854 (million) % 118.85/17.20 % (2766866)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1387554750:i=176048:add=on:rtra=on:rawr=on_2884 on theBenchmark for (2884ds/176048Mi) % 118.85/17.20 % (2766844)Instruction limit reached! % 118.85/17.20 % (2766844)------------------------------ % 118.85/17.20 % (2766844)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 118.85/17.20 % (2766844)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 118.85/17.20 % (2766844)CaDiCaL version: 2.1.3 % 118.85/17.20 % (2766844)Termination reason: Instruction limit % 118.85/17.20 % (2766844)Termination phase: Saturation % 118.85/17.20 % (2766844)Time elapsed: 5.157 s % 118.85/17.20 % (2766844)Peak memory usage: 236 MB % 118.85/17.20 % (2766844)Instructions burned: 17629 (million) % 118.85/17.20 % (2766868)dis+10_1_sil=32000:si=on:sp=arity:random_seed=4170673882:i=206:fgj=on:rtra=on_2860 on theBenchmark for (2860ds/206Mi) % 118.85/17.20 % (2766868)Instruction limit reached! % 118.85/17.20 % (2766868)------------------------------ % 118.85/17.20 % (2766868)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 118.85/17.20 % (2766868)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 118.85/17.20 % (2766868)CaDiCaL version: 2.1.3 % 118.85/17.20 % (2766868)Termination reason: Instruction limit % 118.85/17.20 % (2766868)Termination phase: Saturation % 118.85/17.20 % (2766868)Time elapsed: 0.071 s % 118.85/17.20 % (2766868)Peak memory usage: 13 MB % 118.85/17.20 % (2766868)Instructions burned: 206 (million) % 118.85/17.20 % (2766870)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=953416650:i=232:rtra=on_2859 on theBenchmark for (2859ds/232Mi) % 118.85/17.20 % (2766870)Instruction limit reached! % 118.85/17.20 % (2766870)------------------------------ % 118.85/17.20 % (2766870)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 118.85/17.20 % (2766870)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 118.85/17.20 % (2766870)CaDiCaL version: 2.1.3 % 118.85/17.20 % (2766870)Termination reason: Instruction limit % 118.85/17.20 % (2766870)Termination phase: Saturation % 118.85/17.20 % (2766870)Time elapsed: 0.078 s % 118.85/17.20 % (2766870)Peak memory usage: 13 MB % 118.85/17.20 % (2766870)Instructions burned: 234 (million) % 118.85/17.20 % (2766872)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=2454680864:i=262:rtra=on_2858 on theBenchmark for (2858ds/262Mi) % 118.85/17.20 % (2766872)Instruction limit reached! % 118.85/17.20 % (2766872)------------------------------ % 118.85/17.20 % (2766872)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 118.85/17.20 % (2766872)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 118.85/17.20 % (2766872)CaDiCaL version: 2.1.3 % 118.85/17.20 % (2766872)Termination reason: Instruction limit % 118.85/17.20 % (2766872)Termination phase: Saturation % 118.85/17.20 % (2766872)Time elapsed: 0.089 s % 118.85/17.20 % (2766872)Peak memory usage: 13 MB % 118.85/17.20 % (2766872)Instructions burned: 262 (million) % 118.85/17.20 % (2766874)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=1091246639:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2857 on theBenchmark for (2857ds/318Mi) % 118.85/17.20 % (2766874)Instruction limit reached! % 118.85/17.20 % (2766874)------------------------------ % 118.85/17.20 % (2766874)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 118.85/17.20 % (2766874)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 118.85/17.20 % (2766874)CaDiCaL version: 2.1.3 % 118.85/17.20 % (2766874)Termination reason: Instruction limit % 118.85/17.20 % (2766874)Termination phase: Saturation % 118.85/17.20 % (2766874)Time elapsed: 0.118 s % 118.85/17.20 % (2766874)Peak memory usage: 15 MB % 118.85/17.20 % (2766874)Instructions burned: 321 (million) % 118.85/17.20 % (2766876)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=3640634504:i=1428:nm=2:rtra=on_2856 on theBenchmark for (2856ds/1428Mi) % 126.56/18.34 % (2766876)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 126.56/18.34 % (2766876)Terminated due to inappropriate strategy. % 126.56/18.34 % (2766876)------------------------------ % 126.56/18.34 % (2766876)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 126.56/18.34 % (2766876)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 126.56/18.34 % (2766876)CaDiCaL version: 2.1.3 % 126.56/18.34 % (2766876)Termination reason: Inappropriate % 126.56/18.34 % (2766876)Time elapsed: 0.0000 s % 126.56/18.34 % (2766876)Peak memory usage: 10 MB % 126.56/18.34 % (2766876)Instructions burned: 1 (million) % 126.56/18.34 % (2766876)------------------------------ % 126.56/18.34 % (2766876)------------------------------ % 126.56/18.34 % (2766878)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=2031441337:i=262:bd=preordered:rtra=on:fsd=on_2855 on theBenchmark for (2855ds/262Mi) % 126.56/18.34 % (2766878)Instruction limit reached! % 126.56/18.34 % (2766878)------------------------------ % 126.56/18.34 % (2766878)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 126.56/18.34 % (2766878)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 126.56/18.34 % (2766878)CaDiCaL version: 2.1.3 % 126.56/18.34 % (2766878)Termination reason: Instruction limit % 126.56/18.34 % (2766878)Termination phase: Saturation % 126.56/18.34 % (2766878)Time elapsed: 0.080 s % 126.56/18.34 % (2766878)Peak memory usage: 13 MB % 126.56/18.34 % (2766878)Instructions burned: 264 (million) % 126.56/18.34 % (2766880)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=1123984500:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2855 on theBenchmark for (2855ds/1368Mi) % 126.56/18.34 % (2766880)Instruction limit reached! % 126.56/18.34 % (2766880)------------------------------ % 126.56/18.34 % (2766880)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 126.56/18.34 % (2766880)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 126.56/18.34 % (2766880)CaDiCaL version: 2.1.3 % 126.56/18.34 % (2766880)Termination reason: Instruction limit % 126.56/18.34 % (2766880)Termination phase: Saturation % 126.56/18.34 % (2766880)Time elapsed: 0.444 s % 126.56/18.34 % (2766880)Peak memory usage: 22 MB % 126.56/18.34 % (2766880)Instructions burned: 1368 (million) % 126.56/18.34 % (2766882)ott-21_1_sil=16000:si=on:fs=off:random_seed=2507307103:i=360:av=off:fsr=off:rtra=on_2850 on theBenchmark for (2850ds/360Mi) % 126.56/18.34 % (2766882)Instruction limit reached! % 126.56/18.34 % (2766882)------------------------------ % 126.56/18.34 % (2766882)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 126.56/18.34 % (2766882)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 126.56/18.34 % (2766882)CaDiCaL version: 2.1.3 % 126.56/18.34 % (2766882)Termination reason: Instruction limit % 126.56/18.34 % (2766882)Termination phase: Saturation % 126.56/18.34 % (2766882)Time elapsed: 0.087 s % 126.56/18.34 % (2766882)Peak memory usage: 13 MB % 126.56/18.34 % (2766882)Instructions burned: 361 (million) % 126.56/18.34 % (2766884)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1279629894:i=954:bd=all:rtra=on_2849 on theBenchmark for (2849ds/954Mi) % 126.56/18.34 % (2766884)Instruction limit reached! % 126.56/18.34 % (2766884)------------------------------ % 126.56/18.34 % (2766884)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 126.56/18.34 % (2766884)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 126.56/18.34 % (2766884)CaDiCaL version: 2.1.3 % 126.56/18.34 % (2766884)Termination reason: Instruction limit % 126.56/18.34 % (2766884)Termination phase: Saturation % 126.56/18.34 % (2766884)Time elapsed: 0.353 s % 126.56/18.34 % (2766884)Peak memory usage: 16 MB % 126.56/18.34 % (2766884)Instructions burned: 956 (million) % 126.56/18.34 % (2766886)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=829458730:fmbsr=1.3:i=1730:ins=25:rtra=on_2845 on theBenchmark for (2845ds/1730Mi) % 126.56/18.34 % (2766886)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 126.56/18.34 % (2766886)Terminated due to inappropriate strategy. % 126.56/18.34 % (2766886)------------------------------ % 126.56/18.34 % (2766886)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 126.56/18.34 % (2766886)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 126.56/18.34 % (2766886)CaDiCaL version: 2.1.3 % 126.56/18.34 % (2766886)Termination reason: Inappropriate % 156.20/22.57 % (2766886)Time elapsed: 0.0000 s % 156.20/22.57 % (2766886)Peak memory usage: 10 MB % 156.20/22.57 % (2766886)Instructions burned: 1 (million) % 156.20/22.57 % (2766886)------------------------------ % 156.20/22.57 % (2766886)------------------------------ % 156.20/22.57 % (2766888)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=1611712407:i=2358:rtra=on_2845 on theBenchmark for (2845ds/2358Mi) % 156.20/22.57 % (2766888)Instruction limit reached! % 156.20/22.57 % (2766888)------------------------------ % 156.20/22.57 % (2766888)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 156.20/22.57 % (2766888)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 156.20/22.57 % (2766888)CaDiCaL version: 2.1.3 % 156.20/22.57 % (2766888)Termination reason: Instruction limit % 156.20/22.57 % (2766888)Termination phase: Saturation % 156.20/22.57 % (2766888)Time elapsed: 0.858 s % 156.20/22.57 % (2766888)Peak memory usage: 23 MB % 156.20/22.57 % (2766888)Instructions burned: 2359 (million) % 156.20/22.57 % (2766890)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=2045583831:i=1778:ins=1:rtra=on_2837 on theBenchmark for (2837ds/1778Mi) % 156.20/22.57 % (2766890)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 156.20/22.57 % (2766890)Terminated due to inappropriate strategy. % 156.20/22.57 % (2766890)------------------------------ % 156.20/22.57 % (2766890)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 156.20/22.57 % (2766890)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 156.20/22.57 % (2766890)CaDiCaL version: 2.1.3 % 156.20/22.57 % (2766890)Termination reason: Inappropriate % 156.20/22.57 % (2766890)Time elapsed: 0.0000 s % 156.20/22.57 % (2766890)Peak memory usage: 10 MB % 156.20/22.57 % (2766890)Instructions burned: 1 (million) % 156.20/22.57 % (2766890)------------------------------ % 156.20/22.57 % (2766890)------------------------------ % 156.20/22.57 % (2766892)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=1618941191:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2836 on theBenchmark for (2836ds/1384Mi) % 156.20/22.57 % (2766850)Instruction limit reached! % 156.20/22.57 % (2766850)------------------------------ % 156.20/22.57 % (2766850)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 156.20/22.57 % (2766850)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 156.20/22.57 % (2766850)CaDiCaL version: 2.1.3 % 156.20/22.57 % (2766850)Termination reason: Instruction limit % 156.20/22.57 % (2766850)Termination phase: Saturation % 156.20/22.57 % (2766850)Time elapsed: 6.549 s % 156.20/22.57 % (2766850)Peak memory usage: 31 MB % 156.20/22.57 % (2766850)Instructions burned: 28122 (million) % 156.20/22.57 % (2766894)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=597582388:i=1758:kws=inv_precedence:fsr=off:rtra=on_2835 on theBenchmark for (2835ds/1758Mi) % 156.20/22.57 % (2766892)Instruction limit reached! % 156.20/22.57 % (2766892)------------------------------ % 156.20/22.57 % (2766892)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 156.20/22.57 % (2766892)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 156.20/22.57 % (2766892)CaDiCaL version: 2.1.3 % 156.20/22.57 % (2766892)Termination reason: Instruction limit % 156.20/22.57 % (2766892)Termination phase: Saturation % 156.20/22.57 % (2766892)Time elapsed: 0.519 s % 156.20/22.57 % (2766892)Peak memory usage: 26 MB % 156.20/22.57 % (2766892)Instructions burned: 1385 (million) % 156.20/22.57 % (2766896)fmb+10_1_sil=64000:si=on:random_seed=3250448706:i=44122:nm=2:rtra=on:gsp=on_2831 on theBenchmark for (2831ds/44122Mi) % 156.20/22.57 % (2766896)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 156.20/22.57 % (2766896)Terminated due to inappropriate strategy. % 156.20/22.57 % (2766896)------------------------------ % 156.20/22.57 % (2766896)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 156.20/22.57 % (2766896)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 156.20/22.57 % (2766896)CaDiCaL version: 2.1.3 % 156.20/22.57 % (2766896)Termination reason: Inappropriate % 156.20/22.57 % (2766896)Time elapsed: 0.0000 s % 156.20/22.57 % (2766896)Peak memory usage: 10 MB % 156.20/22.57 % (2766896)Instructions burned: 1 (million) % 156.20/22.57 % (2766896)------------------------------ % 156.20/22.57 % (2766896)------------------------------ % 156.20/22.57 % (2766898)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=182082024:i=19030:nm=5:rtra=on_2831 on theBenchmark for (2831ds/19030Mi) % 165.38/23.86 % (2766898)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 165.38/23.86 % (2766898)Terminated due to inappropriate strategy. % 165.38/23.86 % (2766898)------------------------------ % 165.38/23.86 % (2766898)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 165.38/23.86 % (2766898)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 165.38/23.86 % (2766898)CaDiCaL version: 2.1.3 % 165.38/23.86 % (2766898)Termination reason: Inappropriate % 165.38/23.86 % (2766898)Time elapsed: 0.0000 s % 165.38/23.86 % (2766898)Peak memory usage: 10 MB % 165.38/23.86 % (2766898)Instructions burned: 1 (million) % 165.38/23.86 % (2766898)------------------------------ % 165.38/23.86 % (2766898)------------------------------ % 165.38/23.86 % (2766900)fmb+10_1_sil=64000:sas=cadical:si=on:fmbss=8:random_seed=381876683:fmbsr=1.7:i=1840:rtra=on_2831 on theBenchmark for (2831ds/1840Mi) % 165.38/23.86 % (2766900)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 165.38/23.86 % (2766900)Terminated due to inappropriate strategy. % 165.38/23.86 % (2766900)------------------------------ % 165.38/23.86 % (2766900)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 165.38/23.86 % (2766900)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 165.38/23.86 % (2766900)CaDiCaL version: 2.1.3 % 165.38/23.86 % (2766900)Termination reason: Inappropriate % 165.38/23.86 % (2766900)Time elapsed: 0.0000 s % 165.38/23.86 % (2766900)Peak memory usage: 10 MB % 165.38/23.86 % (2766900)Instructions burned: 1 (million) % 165.38/23.86 % (2766900)------------------------------ % 165.38/23.86 % (2766900)------------------------------ % 165.38/23.86 % (2766902)dis-4_1_sil=16000:drc=ordering:si=on:sp=const_frequency:sac=on:newcnf=on:random_seed=521109843:i=10262:rtra=on_2831 on theBenchmark for (2831ds/10262Mi) % 165.38/23.86 % (2766894)Instruction limit reached! % 165.38/23.86 % (2766894)------------------------------ % 165.38/23.86 % (2766894)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 165.38/23.86 % (2766894)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 165.38/23.86 % (2766894)CaDiCaL version: 2.1.3 % 165.38/23.86 % (2766894)Termination reason: Instruction limit % 165.38/23.86 % (2766894)Termination phase: Saturation % 165.38/23.86 % (2766894)Time elapsed: 0.542 s % 165.38/23.86 % (2766894)Peak memory usage: 23 MB % 165.38/23.86 % (2766894)Instructions burned: 1760 (million) % 165.38/23.86 % (2766904)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:si=on:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2668194877:i=2944:ins=7:rtra=on:fdi=8:gsp=on_2829 on theBenchmark for (2829ds/2944Mi) % 165.38/23.86 % (2766904)Instruction limit reached! % 165.38/23.86 % (2766904)------------------------------ % 165.38/23.86 % (2766904)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 165.38/23.86 % (2766904)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 165.38/23.86 % (2766904)CaDiCaL version: 2.1.3 % 165.38/23.86 % (2766904)Termination reason: Instruction limit % 165.38/23.86 % (2766904)Termination phase: Saturation % 165.38/23.86 % (2766904)Time elapsed: 0.916 s % 165.38/23.86 % (2766904)Peak memory usage: 42 MB % 165.38/23.86 % (2766904)Instructions burned: 2947 (million) % 165.38/23.86 % (2766906)fmb+10_1_sil=16000:sas=cadical:si=on:bce=on:fmbss=77:random_seed=772973065:i=12648:rtra=on_2820 on theBenchmark for (2820ds/12648Mi) % 165.38/23.86 % (2766906)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 165.38/23.86 % (2766906)Terminated due to inappropriate strategy. % 165.38/23.86 % (2766906)------------------------------ % 165.38/23.86 % (2766906)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 165.38/23.86 % (2766906)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 165.38/23.86 % (2766906)CaDiCaL version: 2.1.3 % 165.38/23.86 % (2766906)Termination reason: Inappropriate % 165.38/23.86 % (2766906)Time elapsed: 0.0000 s % 165.38/23.86 % (2766906)Peak memory usage: 10 MB % 165.38/23.86 % (2766906)Instructions burned: 1 (million) % 165.38/23.86 % (2766906)------------------------------ % 165.38/23.86 % (2766906)------------------------------ % 165.38/23.86 % (2766908)fmb+10_1_fmbas=function:sil=32000:sas=cadical:si=on:fmbss=16:random_seed=514251605:fmbsr=2.30978:i=4348:rtra=on_2820 on theBenchmark for (2820ds/4348Mi) % 165.38/23.86 % (2766908)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 165.38/23.86 % (2766908)Terminated due to inappropriate strategy. % 165.38/23.86 % (2766908)------------------------------ % 220.69/31.70 % (2766908)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 220.69/31.70 % (2766908)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 220.69/31.70 % (2766908)CaDiCaL version: 2.1.3 % 220.69/31.70 % (2766908)Termination reason: Inappropriate % 220.69/31.70 % (2766908)Time elapsed: 0.0000 s % 220.69/31.70 % (2766908)Peak memory usage: 10 MB % 220.69/31.70 % (2766908)Instructions burned: 1 (million) % 220.69/31.70 % (2766908)------------------------------ % 220.69/31.70 % (2766908)------------------------------ % 220.69/31.70 % (2766910)ott-2_1_sil=16000:si=on:newcnf=on:random_seed=758321255:avsq=on:i=1738:avsqr=1,16:kws=inv_arity_squared:rtra=on_2819 on theBenchmark for (2819ds/1738Mi) % 220.69/31.70 % (2766910)Instruction limit reached! % 220.69/31.70 % (2766910)------------------------------ % 220.69/31.70 % (2766910)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 220.69/31.70 % (2766910)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 220.69/31.70 % (2766910)CaDiCaL version: 2.1.3 % 220.69/31.70 % (2766910)Termination reason: Instruction limit % 220.69/31.70 % (2766910)Termination phase: Saturation % 220.69/31.70 % (2766910)Time elapsed: 0.627 s % 220.69/31.70 % (2766910)Peak memory usage: 22 MB % 220.69/31.70 % (2766910)Instructions burned: 1739 (million) % 220.69/31.70 % (2766912)ott+10_1_sil=32000:tgt=ground:si=on:random_seed=586351474:i=10228:av=off:rtra=on_2813 on theBenchmark for (2813ds/10228Mi) % 220.69/31.70 % (2766756)Instruction limit reached! % 220.69/31.70 % (2766756)------------------------------ % 220.69/31.70 % (2766756)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 220.69/31.70 % (2766756)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 220.69/31.70 % (2766756)CaDiCaL version: 2.1.3 % 220.69/31.70 % (2766756)Termination reason: Instruction limit % 220.69/31.70 % (2766756)Termination phase: Saturation % 220.69/31.70 % (2766756)Time elapsed: 19.986 s % 220.69/31.70 % (2766756)Peak memory usage: 34 MB % 220.69/31.70 % (2766756)Instructions burned: 88028 (million) % 220.69/31.70 % (2766914)fmb+10_1_sil=64000:sas=cadical:si=on:bce=on:rp=on:random_seed=1320996805:i=108564:rtra=on_2799 on theBenchmark for (2799ds/108564Mi) % 220.69/31.70 % (2766914)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 220.69/31.70 % (2766914)Terminated due to inappropriate strategy. % 220.69/31.70 % (2766914)------------------------------ % 220.69/31.70 % (2766914)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 220.69/31.70 % (2766914)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 220.69/31.70 % (2766914)CaDiCaL version: 2.1.3 % 220.69/31.70 % (2766914)Termination reason: Inappropriate % 220.69/31.70 % (2766914)Time elapsed: 0.0000 s % 220.69/31.70 % (2766914)Peak memory usage: 10 MB % 220.69/31.70 % (2766914)Instructions burned: 1 (million) % 220.69/31.70 % (2766914)------------------------------ % 220.69/31.70 % (2766914)------------------------------ % 220.69/31.70 % (2766916)dis-11_1_sil=16000:si=on:sp=reverse_frequency:alpa=true:random_seed=4037030734:i=7024:aac=none:rtra=on_2799 on theBenchmark for (2799ds/7024Mi) % 220.69/31.70 % (2766902)Instruction limit reached! % 220.69/31.70 % (2766902)------------------------------ % 220.69/31.70 % (2766902)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 220.69/31.70 % (2766902)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 220.69/31.70 % (2766902)CaDiCaL version: 2.1.3 % 220.69/31.70 % (2766902)Termination reason: Instruction limit % 220.69/31.70 % (2766902)Termination phase: Saturation % 220.69/31.70 % (2766902)Time elapsed: 3.199 s % 220.69/31.70 % (2766902)Peak memory usage: 65 MB % 220.69/31.70 % (2766902)Instructions burned: 10266 (million) % 220.69/31.70 % (2766918)dis+21_1_sil=32000:sas=cadical:si=on:random_seed=1288739973:i=7546:rtra=on:amm=off_2799 on theBenchmark for (2799ds/7546Mi) % 220.69/31.70 % (2766916)Instruction limit reached! % 220.69/31.70 % (2766916)------------------------------ % 220.69/31.70 % (2766916)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 220.69/31.70 % (2766916)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 220.69/31.70 % (2766916)CaDiCaL version: 2.1.3 % 220.69/31.70 % (2766916)Termination reason: Instruction limit % 220.69/31.70 % (2766916)Termination phase: Saturation % 220.69/31.70 % (2766916)Time elapsed: 2.184 s % 220.69/31.70 % (2766916)Peak memory usage: 45 MB % 220.69/31.70 % (2766916)Instructions burned: 7027 (million) % 220.69/31.70 % (2766920)ott+11_1_sil=16000:si=on:gs=on:random_seed=3635556164:s2a=on:i=4502:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:rtra=on:fsd=on_2777 on theBenchmark for (2777ds/4502Mi) % 252.56/42.13 % (2766918)Instruction limit reached! % 252.56/42.13 % (2766918)------------------------------ % 252.56/42.13 % (2766918)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 252.56/42.13 % (2766918)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 252.56/42.13 % (2766918)CaDiCaL version: 2.1.3 % 252.56/42.13 % (2766918)Termination reason: Instruction limit % 252.56/42.13 % (2766918)Termination phase: Saturation % 252.56/42.13 % (2766918)Time elapsed: 2.388 s % 252.56/42.13 % (2766918)Peak memory usage: 47 MB % 252.56/42.13 % (2766918)Instructions burned: 7546 (million) % 252.56/42.13 % (2766912)Instruction limit reached! % 252.56/42.13 % (2766912)------------------------------ % 252.56/42.13 % (2766912)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 252.56/42.13 % (2766912)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 252.56/42.13 % (2766912)CaDiCaL version: 2.1.3 % 252.56/42.13 % (2766912)Termination reason: Instruction limit % 252.56/42.13 % (2766912)Termination phase: Saturation % 252.56/42.13 % (2766912)Time elapsed: 3.843 s % 252.56/42.13 % (2766912)Peak memory usage: 46 MB % 252.56/42.13 % (2766912)Instructions burned: 10228 (million) % 252.56/42.13 % (2766922)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:si=on:fmbss=7:random_seed=3395459084:fmbsr=1.6:i=135068:rtra=on_2775 on theBenchmark for (2775ds/135068Mi) % 252.56/42.13 % (2766922)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 252.56/42.13 % (2766922)Terminated due to inappropriate strategy. % 252.56/42.13 % (2766922)------------------------------ % 252.56/42.13 % (2766922)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 252.56/42.13 % (2766922)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 252.56/42.13 % (2766922)CaDiCaL version: 2.1.3 % 252.56/42.13 % (2766922)Termination reason: Inappropriate % 252.56/42.13 % (2766922)Time elapsed: 0.0000 s % 252.56/42.13 % (2766922)Peak memory usage: 10 MB % 252.56/42.13 % (2766922)Instructions burned: 1 (million) % 252.56/42.13 % (2766922)------------------------------ % 252.56/42.13 % (2766922)------------------------------ % 252.56/42.13 % (2766923)ott-22_32_sil=16000:tgt=full:si=on:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=992048933:avsq=on:i=9182:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:rtra=on:fdi=4_2775 on theBenchmark for (2775ds/9182Mi) % 252.56/42.13 % (2766846)Instruction limit reached! % 252.56/42.13 % (2766846)------------------------------ % 252.56/42.13 % (2766846)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 252.56/42.13 % (2766846)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 252.56/42.13 % (2766846)CaDiCaL version: 2.1.3 % 252.56/42.13 % (2766846)Termination reason: Instruction limit % 252.56/42.13 % (2766846)Termination phase: Saturation % 252.56/42.13 % (2766846)Time elapsed: 12.693 s % 252.56/42.13 % (2766846)Peak memory usage: 114 MB % 252.56/42.13 % (2766846)Instructions burned: 53296 (million) % 252.56/42.13 % (2766926)dis+10_64_to=lpo:sil=32000:si=on:spb=intro:urr=on:sac=on:random_seed=3340240440:i=58680:rtra=on_2774 on theBenchmark for (2774ds/58680Mi) % 252.56/42.13 % (2766928)dis-10_1_sil=64000:sas=cadical:si=on:cn=on:random_seed=1445036026:i=10422:rtra=on_2774 on theBenchmark for (2774ds/10422Mi) % 252.56/42.13 % (2766920)Instruction limit reached! % 252.56/42.13 % (2766920)------------------------------ % 252.56/42.13 % (2766920)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 252.56/42.13 % (2766920)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 252.56/42.13 % (2766920)CaDiCaL version: 2.1.3 % 252.56/42.13 % (2766920)Termination reason: Instruction limit % 252.56/42.13 % (2766920)Termination phase: Saturation % 252.56/42.13 % (2766920)Time elapsed: 1.278 s % 252.56/42.13 % (2766920)Peak memory usage: 20 MB % 252.56/42.13 % (2766920)Instructions burned: 4505 (million) % 252.56/42.13 % (2766930)fmb+10_1_sil=32000:sas=cadical:si=on:bce=on:fmbss=17:random_seed=3500682594:i=10994:nm=2:rtra=on_2764 on theBenchmark for (2764ds/10994Mi) % 252.56/42.13 % (2766930)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 252.56/42.13 % (2766930)Terminated due to inappropriate strategy. % 252.56/42.13 % (2766930)------------------------------ % 252.56/42.13 % (2766930)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 252.56/42.13 % (2766930)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 252.56/42.13 % (2766930)CaDiCaL version: 2.1.3 % 252.56/42.13 % (2766930)Termination reason: InappropriatTerminated % 300.92/43.05 % Vampire exiting %------------------------------------------------------------------------------