%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWW607_2 : TPTP v9.3.1. Released v6.1.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % Computer : n018.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:40:31 PM UTC 2026 % Result : Timeout 287.34s 40.76s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : SWW607_2 : TPTP v9.3.1. Released v6.1.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.08/0.19 % Computer : n018.cluster.edu % 0.08/0.19 % Model : x86_64 x86_64 % 0.08/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.08/0.19 % Memory : 8046.5625MB % 0.08/0.19 % OS : Linux 6.8.0-71-generic % 0.08/0.19 % CPULimit : 300 % 0.08/0.19 % WCLimit : 300 % 0.08/0.19 % DateTime : Mon Sep 28 14:24:57 UTC 2026 % 0.08/0.19 % CPUTime : % 0.08/0.19 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.28/0.71 % (3419864)Will run a generic schedule for satisfiability detection. % 3.28/0.71 % (3419879)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=4106268332:i=116_2999 on theBenchmark for (2999ds/116Mi) % 3.28/0.71 % (3419876)% WARNING: option uhcvi not known. % 3.28/0.71 % (3419875)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2983342945_2999 on theBenchmark for (2999ds/0Mi) % 3.28/0.71 % (3419876)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=12586307:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 3.28/0.71 % (3419877)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=800110738:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 3.28/0.71 % (3419878)dis+10_1_sil=32000:sp=arity:random_seed=4223510744:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 3.28/0.71 % (3419880)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3309081443:i=131_2999 on theBenchmark for (2999ds/131Mi) % 3.28/0.71 % (3419881)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=489019830:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 3.28/0.71 % (3419875)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.28/0.71 % (3419875)Terminated due to inappropriate strategy. % 3.28/0.71 % (3419875)------------------------------ % 3.28/0.71 % (3419875)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.28/0.71 % (3419875)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.28/0.71 % (3419875)CaDiCaL version: 2.1.3 % 3.28/0.71 % (3419875)Termination reason: Inappropriate % 3.28/0.71 % (3419875)Time elapsed: 0.006 s % 3.28/0.71 % (3419875)Peak memory usage: 11 MB % 3.28/0.71 % (3419875)Instructions burned: 11 (million) % 3.28/0.71 % (3419875)------------------------------ % 3.28/0.71 % (3419875)------------------------------ % 3.28/0.71 % (3419894)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3176287006:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 3.28/0.71 % (3419894)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.28/0.71 % (3419894)Terminated due to inappropriate strategy. % 3.28/0.71 % (3419894)------------------------------ % 3.28/0.71 % (3419894)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.28/0.71 % (3419894)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.28/0.71 % (3419894)CaDiCaL version: 2.1.3 % 3.28/0.71 % (3419894)Termination reason: Inappropriate % 3.28/0.71 % (3419894)Time elapsed: 0.005 s % 3.28/0.71 % (3419894)Peak memory usage: 11 MB % 3.28/0.71 % (3419894)Instructions burned: 9 (million) % 3.28/0.71 % (3419879)Instruction limit reached! % 3.28/0.71 % (3419879)------------------------------ % 3.28/0.71 % (3419879)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.28/0.71 % (3419879)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.28/0.71 % (3419879)CaDiCaL version: 2.1.3 % 3.28/0.71 % (3419879)Termination reason: Instruction limit % 3.28/0.71 % (3419879)Termination phase: Saturation % 3.28/0.71 % (3419879)Time elapsed: 0.040 s % 3.28/0.71 % (3419879)Peak memory usage: 13 MB % 3.28/0.71 % (3419879)Instructions burned: 119 (million) % 3.28/0.71 % (3419894)------------------------------ % 3.28/0.71 % (3419894)------------------------------ % 3.28/0.71 % (3419903)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2372227445:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 3.28/0.71 % (3419904)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=1489730455:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi) % 3.28/0.71 % (3419878)Instruction limit reached! % 3.28/0.71 % (3419878)------------------------------ % 3.28/0.71 % (3419878)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.28/0.71 % (3419878)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.28/0.71 % (3419878)CaDiCaL version: 2.1.3 % 3.28/0.71 % (3419878)Termination reason: Instruction limit % 3.28/0.71 % (3419878)Termination phase: Saturation % 3.28/0.71 % (3419878)Time elapsed: 0.064 s % 3.28/0.71 % (3419878)Peak memory usage: 13 MB % 3.28/0.71 % (3419878)Instructions burned: 105 (million) % 3.28/0.71 % (3419880)Instruction limit reached! % 3.28/0.71 % (3419880)------------------------------ % 3.28/0.71 % (3419880)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.77/1.05 % (3419880)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.77/1.05 % (3419880)CaDiCaL version: 2.1.3 % 5.77/1.05 % (3419880)Termination reason: Instruction limit % 5.77/1.05 % (3419880)Termination phase: Saturation % 5.77/1.05 % (3419880)Time elapsed: 0.079 s % 5.77/1.05 % (3419880)Peak memory usage: 13 MB % 5.77/1.05 % (3419880)Instructions burned: 131 (million) % 5.77/1.05 % (3419916)ott-21_1_sil=16000:fs=off:random_seed=3190974558:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 5.77/1.05 % (3419903)Instruction limit reached! % 5.77/1.05 % (3419903)------------------------------ % 5.77/1.05 % (3419903)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.77/1.05 % (3419903)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.77/1.05 % (3419903)CaDiCaL version: 2.1.3 % 5.77/1.05 % (3419903)Termination reason: Instruction limit % 5.77/1.05 % (3419903)Termination phase: Saturation % 5.77/1.05 % (3419903)Time elapsed: 0.045 s % 5.77/1.05 % (3419903)Peak memory usage: 13 MB % 5.77/1.05 % (3419903)Instructions burned: 132 (million) % 5.77/1.05 % (3419921)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=4215656244:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 5.77/1.05 % (3419925)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=4042711043:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 5.77/1.05 % (3419925)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 5.77/1.05 % (3419925)Terminated due to inappropriate strategy. % 5.77/1.05 % (3419925)------------------------------ % 5.77/1.05 % (3419925)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.77/1.05 % (3419925)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.77/1.05 % (3419925)CaDiCaL version: 2.1.3 % 5.77/1.05 % (3419925)Termination reason: Inappropriate % 5.77/1.05 % (3419925)Time elapsed: 0.002 s % 5.77/1.05 % (3419925)Peak memory usage: 11 MB % 5.77/1.05 % (3419925)Instructions burned: 9 (million) % 5.77/1.05 % (3419925)------------------------------ % 5.77/1.05 % (3419925)------------------------------ % 5.77/1.05 % (3419881)Instruction limit reached! % 5.77/1.05 % (3419881)------------------------------ % 5.77/1.05 % (3419881)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.77/1.05 % (3419881)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.77/1.05 % (3419881)CaDiCaL version: 2.1.3 % 5.77/1.05 % (3419881)Termination reason: Instruction limit % 5.77/1.05 % (3419881)Termination phase: Saturation % 5.77/1.05 % (3419881)Time elapsed: 0.107 s % 5.77/1.05 % (3419881)Peak memory usage: 14 MB % 5.77/1.05 % (3419881)Instructions burned: 160 (million) % 5.77/1.05 % (3419934)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1366195128:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi) % 5.77/1.05 % (3419931)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2243268440:i=1179_2998 on theBenchmark for (2998ds/1179Mi) % 5.77/1.05 % (3419934)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 5.77/1.05 % (3419934)Terminated due to inappropriate strategy. % 5.77/1.05 % (3419934)------------------------------ % 5.77/1.05 % (3419934)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.77/1.05 % (3419934)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.77/1.05 % (3419934)CaDiCaL version: 2.1.3 % 5.77/1.05 % (3419934)Termination reason: Inappropriate % 5.77/1.05 % (3419934)Time elapsed: 0.002 s % 5.77/1.05 % (3419934)Peak memory usage: 11 MB % 5.77/1.05 % (3419934)Instructions burned: 9 (million) % 5.77/1.05 % (3419934)------------------------------ % 5.77/1.05 % (3419934)------------------------------ % 5.77/1.05 % (3419941)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=2010454006: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) % 5.77/1.05 % (3419916)Instruction limit reached! % 5.77/1.05 % (3419916)------------------------------ % 5.77/1.05 % (3419916)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.77/1.05 % (3419916)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.77/1.05 % (3419916)CaDiCaL version: 2.1.3 % 5.77/1.05 % (3419916)Termination reason: Instruction limit % 5.77/1.05 % (3419916)Termination phase: Saturation % 23.02/3.55 % (3419916)Time elapsed: 0.098 s % 23.02/3.55 % (3419916)Peak memory usage: 13 MB % 23.02/3.55 % (3419916)Instructions burned: 180 (million) % 23.02/3.55 % (3419962)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3257609350:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi) % 23.02/3.55 % (3419941)Instruction limit reached! % 23.02/3.55 % (3419941)------------------------------ % 23.02/3.55 % (3419941)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 23.02/3.55 % (3419941)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.02/3.55 % (3419941)CaDiCaL version: 2.1.3 % 23.02/3.55 % (3419941)Termination reason: Instruction limit % 23.02/3.55 % (3419941)Termination phase: Saturation % 23.02/3.55 % (3419941)Time elapsed: 0.242 s % 23.02/3.55 % (3419941)Peak memory usage: 19 MB % 23.02/3.55 % (3419941)Instructions burned: 696 (million) % 23.02/3.55 % (3420007)fmb+10_1_sil=64000:random_seed=4042758092:i=22061:nm=2:gsp=on_2995 on theBenchmark for (2995ds/22061Mi) % 23.02/3.55 % (3420007)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 23.02/3.55 % (3420007)Terminated due to inappropriate strategy. % 23.02/3.55 % (3420007)------------------------------ % 23.02/3.55 % (3420007)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 23.02/3.55 % (3420007)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.02/3.55 % (3420007)CaDiCaL version: 2.1.3 % 23.02/3.55 % (3420007)Termination reason: Inappropriate % 23.02/3.55 % (3420007)Time elapsed: 0.003 s % 23.02/3.55 % (3420007)Peak memory usage: 11 MB % 23.02/3.55 % (3420007)Instructions burned: 10 (million) % 23.02/3.55 % (3420007)------------------------------ % 23.02/3.55 % (3420007)------------------------------ % 23.02/3.55 % (3420011)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3370959724:i=9515:nm=5_2995 on theBenchmark for (2995ds/9515Mi) % 23.02/3.55 % (3420011)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 23.02/3.55 % (3420011)Terminated due to inappropriate strategy. % 23.02/3.55 % (3420011)------------------------------ % 23.02/3.55 % (3420011)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 23.02/3.55 % (3420011)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.02/3.55 % (3420011)CaDiCaL version: 2.1.3 % 23.02/3.55 % (3420011)Termination reason: Inappropriate % 23.02/3.55 % (3420011)Time elapsed: 0.002 s % 23.02/3.55 % (3420011)Peak memory usage: 11 MB % 23.02/3.55 % (3420011)Instructions burned: 9 (million) % 23.02/3.55 % (3420011)------------------------------ % 23.02/3.55 % (3420011)------------------------------ % 23.02/3.55 % (3420016)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1339550505:fmbsr=1.7:i=920_2995 on theBenchmark for (2995ds/920Mi) % 23.02/3.55 % (3419904)Instruction limit reached! % 23.02/3.55 % (3419904)------------------------------ % 23.02/3.55 % (3419904)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 23.02/3.55 % (3419904)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.02/3.55 % (3419904)CaDiCaL version: 2.1.3 % 23.02/3.55 % (3419904)Termination reason: Instruction limit % 23.02/3.55 % (3419904)Termination phase: Saturation % 23.02/3.55 % (3419904)Time elapsed: 0.376 s % 23.02/3.55 % (3419904)Peak memory usage: 16 MB % 23.02/3.55 % (3419904)Instructions burned: 686 (million) % 23.02/3.55 % (3420016)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 23.02/3.55 % (3420016)Terminated due to inappropriate strategy. % 23.02/3.55 % (3420016)------------------------------ % 23.02/3.55 % (3420016)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 23.02/3.55 % (3420016)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.02/3.55 % (3420016)CaDiCaL version: 2.1.3 % 23.02/3.55 % (3420016)Termination reason: Inappropriate % 23.02/3.55 % (3420016)Time elapsed: 0.010 s % 23.02/3.55 % (3420016)Peak memory usage: 11 MB % 23.02/3.55 % (3420016)Instructions burned: 9 (million) % 23.02/3.55 % (3420016)------------------------------ % 23.02/3.55 % (3420016)------------------------------ % 23.02/3.55 % (3419921)Instruction limit reached! % 23.02/3.55 % (3419921)------------------------------ % 23.02/3.55 % (3419921)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 23.02/3.55 % (3419921)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.02/3.55 % (3419921)CaDiCaL version: 2.1.3 % 23.02/3.55 % (3419921)Termination reason: Instruction limit % 23.02/3.55 % (3419921)Termination phase: Saturation % 28.86/4.38 % (3419921)Time elapsed: 0.339 s % 28.86/4.38 % (3419921)Peak memory usage: 15 MB % 28.86/4.38 % (3419921)Instructions burned: 477 (million) % 28.86/4.38 % (3420027)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2842381134:i=5131_2995 on theBenchmark for (2995ds/5131Mi) % 28.86/4.38 % (3420029)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=42672290:i=6324_2995 on theBenchmark for (2995ds/6324Mi) % 28.86/4.38 % (3420029)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 28.86/4.38 % (3420029)Terminated due to inappropriate strategy. % 28.86/4.38 % (3420029)------------------------------ % 28.86/4.38 % (3420029)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 28.86/4.38 % (3420029)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.86/4.38 % (3420029)CaDiCaL version: 2.1.3 % 28.86/4.38 % (3420029)Termination reason: Inappropriate % 28.86/4.38 % (3420029)Time elapsed: 0.003 s % 28.86/4.38 % (3420029)Peak memory usage: 11 MB % 28.86/4.38 % (3420029)Instructions burned: 11 (million) % 28.86/4.38 % (3420029)------------------------------ % 28.86/4.38 % (3420029)------------------------------ % 28.86/4.38 % (3420028)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3157041913:i=1472:ins=7:fdi=8:gsp=on_2995 on theBenchmark for (2995ds/1472Mi) % 28.86/4.38 % (3420035)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1535805540:fmbsr=2.30978:i=2174_2995 on theBenchmark for (2995ds/2174Mi) % 28.86/4.38 % (3420035)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 28.86/4.38 % (3420035)Terminated due to inappropriate strategy. % 28.86/4.38 % (3420035)------------------------------ % 28.86/4.38 % (3420035)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 28.86/4.38 % (3420035)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.86/4.38 % (3420035)CaDiCaL version: 2.1.3 % 28.86/4.38 % (3420035)Termination reason: Inappropriate % 28.86/4.38 % (3420035)Time elapsed: 0.002 s % 28.86/4.38 % (3420035)Peak memory usage: 11 MB % 28.86/4.38 % (3420035)Instructions burned: 9 (million) % 28.86/4.38 % (3420035)------------------------------ % 28.86/4.38 % (3420035)------------------------------ % 28.86/4.38 % (3420044)ott-2_1_sil=16000:newcnf=on:random_seed=67462883:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2994 on theBenchmark for (2994ds/869Mi) % 28.86/4.38 % (3419962)Instruction limit reached! % 28.86/4.38 % (3419962)------------------------------ % 28.86/4.38 % (3419962)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 28.86/4.38 % (3419962)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.86/4.38 % (3419962)CaDiCaL version: 2.1.3 % 28.86/4.38 % (3419962)Termination reason: Instruction limit % 28.86/4.38 % (3419962)Termination phase: Saturation % 28.86/4.38 % (3419962)Time elapsed: 0.530 s % 28.86/4.38 % (3419962)Peak memory usage: 19 MB % 28.86/4.38 % (3419962)Instructions burned: 880 (million) % 28.86/4.38 % (3420046)ott+10_1_sil=32000:tgt=ground:random_seed=1683177360:i=5114:av=off_2992 on theBenchmark for (2992ds/5114Mi) % 28.86/4.38 % (3420044)Instruction limit reached! % 28.86/4.38 % (3420044)------------------------------ % 28.86/4.38 % (3420044)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 28.86/4.38 % (3420044)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.86/4.38 % (3420044)CaDiCaL version: 2.1.3 % 28.86/4.38 % (3420044)Termination reason: Instruction limit % 28.86/4.38 % (3420044)Termination phase: Saturation % 28.86/4.38 % (3420044)Time elapsed: 0.287 s % 28.86/4.38 % (3420044)Peak memory usage: 17 MB % 28.86/4.38 % (3420044)Instructions burned: 871 (million) % 28.86/4.38 % (3420048)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=3084782750:i=54282_2991 on theBenchmark for (2991ds/54282Mi) % 28.86/4.38 % (3420048)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 28.86/4.38 % (3420048)Terminated due to inappropriate strategy. % 28.86/4.38 % (3420048)------------------------------ % 28.86/4.38 % (3420048)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 28.86/4.38 % (3420048)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.86/4.38 % (3420048)CaDiCaL version: 2.1.3 % 28.86/4.38 % (3420048)Termination reason: Inappropriate % 28.86/4.38 % (3420048)Time elapsed: 0.003 s % 28.86/4.38 % (3420048)Peak memory usage: 11 MB % 28.86/4.38 % (3420048)Instructions burned: 11 (million) % 92.75/13.37 % (3420048)------------------------------ % 92.75/13.37 % (3420048)------------------------------ % 92.75/13.37 % (3420050)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=471200587:i=3512:aac=none_2991 on theBenchmark for (2991ds/3512Mi) % 92.75/13.37 % (3419931)Instruction limit reached! % 92.75/13.37 % (3419931)------------------------------ % 92.75/13.37 % (3419931)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 92.75/13.37 % (3419931)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 92.75/13.37 % (3419931)CaDiCaL version: 2.1.3 % 92.75/13.37 % (3419931)Termination reason: Instruction limit % 92.75/13.37 % (3419931)Termination phase: Saturation % 92.75/13.37 % (3419931)Time elapsed: 0.743 s % 92.75/13.37 % (3419931)Peak memory usage: 21 MB % 92.75/13.37 % (3419931)Instructions burned: 1179 (million) % 92.75/13.37 % (3420052)dis+21_1_sil=32000:sas=cadical:random_seed=3136917414:i=3773:amm=off_2990 on theBenchmark for (2990ds/3773Mi) % 92.75/13.37 % (3420028)Instruction limit reached! % 92.75/13.37 % (3420028)------------------------------ % 92.75/13.37 % (3420028)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 92.75/13.37 % (3420028)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 92.75/13.37 % (3420028)CaDiCaL version: 2.1.3 % 92.75/13.37 % (3420028)Termination reason: Instruction limit % 92.75/13.37 % (3420028)Termination phase: Saturation % 92.75/13.37 % (3420028)Time elapsed: 1.382 s % 92.75/13.37 % (3420028)Peak memory usage: 31 MB % 92.75/13.37 % (3420028)Instructions burned: 1473 (million) % 92.75/13.37 % (3420097)ott+11_1_sil=16000:gs=on:random_seed=3151843125:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2981 on theBenchmark for (2981ds/2251Mi) % 92.75/13.37 % (3420050)Instruction limit reached! % 92.75/13.37 % (3420050)------------------------------ % 92.75/13.37 % (3420050)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 92.75/13.37 % (3420050)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 92.75/13.37 % (3420050)CaDiCaL version: 2.1.3 % 92.75/13.37 % (3420050)Termination reason: Instruction limit % 92.75/13.37 % (3420050)Termination phase: Saturation % 92.75/13.37 % (3420050)Time elapsed: 1.317 s % 92.75/13.37 % (3420050)Peak memory usage: 34 MB % 92.75/13.37 % (3420050)Instructions burned: 3514 (million) % 92.75/13.37 % (3420104)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=3660661565:fmbsr=1.6:i=67534_2978 on theBenchmark for (2978ds/67534Mi) % 92.75/13.37 % (3420104)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 92.75/13.37 % (3420104)Terminated due to inappropriate strategy. % 92.75/13.37 % (3420104)------------------------------ % 92.75/13.37 % (3420104)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 92.75/13.37 % (3420104)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 92.75/13.37 % (3420104)CaDiCaL version: 2.1.3 % 92.75/13.37 % (3420104)Termination reason: Inappropriate % 92.75/13.37 % (3420104)Time elapsed: 0.003 s % 92.75/13.37 % (3420104)Peak memory usage: 11 MB % 92.75/13.37 % (3420104)Instructions burned: 9 (million) % 92.75/13.37 % (3420104)------------------------------ % 92.75/13.37 % (3420104)------------------------------ % 92.75/13.37 % (3420106)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=902356004:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2978 on theBenchmark for (2978ds/4591Mi) % 92.75/13.37 % (3420097)Instruction limit reached! % 92.75/13.37 % (3420097)------------------------------ % 92.75/13.37 % (3420097)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 92.75/13.37 % (3420097)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 92.75/13.37 % (3420097)CaDiCaL version: 2.1.3 % 92.75/13.37 % (3420097)Termination reason: Instruction limit % 92.75/13.37 % (3420097)Termination phase: Saturation % 92.75/13.37 % (3420097)Time elapsed: 1.156 s % 92.75/13.37 % (3420097)Peak memory usage: 20 MB % 92.75/13.37 % (3420097)Instructions burned: 2251 (million) % 92.75/13.37 % (3420257)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=2937352932:i=29340_2969 on theBenchmark for (2969ds/29340Mi) % 92.75/13.37 % (3420106)Instruction limit reached! % 92.75/13.37 % (3420106)------------------------------ % 92.75/13.37 % (3420106)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 92.75/13.37 % (3420106)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 92.75/13.37 % (3420106)CaDiCaL version: 2.1.3 % 92.75/13.37 % (3420106)Termination reason: Instruction limit % 127.57/18.28 % (3420106)Termination phase: Saturation % 127.57/18.28 % (3420106)Time elapsed: 1.137 s % 127.57/18.28 % (3420106)Peak memory usage: 37 MB % 127.57/18.28 % (3420106)Instructions burned: 4592 (million) % 127.57/18.28 % (3420052)Instruction limit reached! % 127.57/18.28 % (3420052)------------------------------ % 127.57/18.28 % (3420052)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 127.57/18.28 % (3420052)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 127.57/18.28 % (3420052)CaDiCaL version: 2.1.3 % 127.57/18.28 % (3420052)Termination reason: Instruction limit % 127.57/18.28 % (3420052)Termination phase: Saturation % 127.57/18.28 % (3420052)Time elapsed: 2.399 s % 127.57/18.28 % (3420052)Peak memory usage: 36 MB % 127.57/18.28 % (3420052)Instructions burned: 3774 (million) % 127.57/18.28 % (3420263)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=3598731232:i=5211_2966 on theBenchmark for (2966ds/5211Mi) % 127.57/18.28 % (3420264)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=4235419751:i=5497:nm=2_2966 on theBenchmark for (2966ds/5497Mi) % 127.57/18.28 % (3420264)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 127.57/18.28 % (3420264)Terminated due to inappropriate strategy. % 127.57/18.28 % (3420264)------------------------------ % 127.57/18.28 % (3420264)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 127.57/18.28 % (3420264)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 127.57/18.28 % (3420264)CaDiCaL version: 2.1.3 % 127.57/18.28 % (3420264)Termination reason: Inappropriate % 127.57/18.28 % (3420264)Time elapsed: 0.006 s % 127.57/18.28 % (3420264)Peak memory usage: 11 MB % 127.57/18.28 % (3420264)Instructions burned: 11 (million) % 127.57/18.28 % (3420264)------------------------------ % 127.57/18.28 % (3420264)------------------------------ % 127.57/18.28 % (3420267)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=3057970520:fmbsr=2:i=46332_2966 on theBenchmark for (2966ds/46332Mi) % 127.57/18.28 % (3420267)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 127.57/18.28 % (3420267)Terminated due to inappropriate strategy. % 127.57/18.28 % (3420267)------------------------------ % 127.57/18.28 % (3420267)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 127.57/18.28 % (3420267)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 127.57/18.28 % (3420267)CaDiCaL version: 2.1.3 % 127.57/18.28 % (3420267)Termination reason: Inappropriate % 127.57/18.28 % (3420267)Time elapsed: 0.005 s % 127.57/18.28 % (3420267)Peak memory usage: 11 MB % 127.57/18.28 % (3420267)Instructions burned: 9 (million) % 127.57/18.28 % (3420267)------------------------------ % 127.57/18.28 % (3420267)------------------------------ % 127.57/18.28 % (3420269)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=2828251687:i=14071_2966 on theBenchmark for (2966ds/14071Mi) % 127.57/18.28 % (3420269)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 127.57/18.28 % (3420269)Terminated due to inappropriate strategy. % 127.57/18.28 % (3420269)------------------------------ % 127.57/18.28 % (3420269)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 127.57/18.28 % (3420269)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 127.57/18.28 % (3420269)CaDiCaL version: 2.1.3 % 127.57/18.28 % (3420269)Termination reason: Inappropriate % 127.57/18.28 % (3420269)Time elapsed: 0.005 s % 127.57/18.28 % (3420269)Peak memory usage: 11 MB % 127.57/18.28 % (3420269)Instructions burned: 9 (million) % 127.57/18.28 % (3420269)------------------------------ % 127.57/18.28 % (3420269)------------------------------ % 127.57/18.28 % (3420271)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1542993161:i=22565:add=on:rawr=on_2965 on theBenchmark for (2965ds/22565Mi) % 127.57/18.28 % (3420027)Instruction limit reached! % 127.57/18.28 % (3420027)------------------------------ % 127.57/18.28 % (3420027)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 127.57/18.28 % (3420027)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 127.57/18.28 % (3420027)CaDiCaL version: 2.1.3 % 127.57/18.28 % (3420027)Termination reason: Instruction limit % 127.57/18.28 % (3420027)Termination phase: Saturation % 127.57/18.28 % (3420027)Time elapsed: 3.181 s % 127.57/18.28 % (3420027)Peak memory usage: 43 MB % 127.57/18.28 % (3420027)Instructions burned: 5133 (million) % 127.57/18.28 % (3420273)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=815394353:i=8173:av=off_2963 on theBenchmark for (2963ds/8173Mi) % 127.57/18.28 % (3420046)Instruction limit reached! % 129.00/18.41 % (3420046)------------------------------ % 129.00/18.41 % (3420046)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 129.00/18.41 % (3420046)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 129.00/18.41 % (3420046)CaDiCaL version: 2.1.3 % 129.00/18.41 % (3420046)Termination reason: Instruction limit % 129.00/18.41 % (3420046)Termination phase: Saturation % 129.00/18.41 % (3420046)Time elapsed: 3.354 s % 129.00/18.41 % (3420046)Peak memory usage: 43 MB % 129.00/18.41 % (3420046)Instructions burned: 5115 (million) % 129.00/18.41 % (3420275)dis+10_16:1_sil=16000:random_seed=3041701110:i=9155:fsr=off_2958 on theBenchmark for (2958ds/9155Mi) % 129.00/18.41 % (3420263)Instruction limit reached! % 129.00/18.41 % (3420263)------------------------------ % 129.00/18.41 % (3420263)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 129.00/18.41 % (3420263)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 129.00/18.41 % (3420263)CaDiCaL version: 2.1.3 % 129.00/18.41 % (3420263)Termination reason: Instruction limit % 129.00/18.41 % (3420263)Termination phase: Saturation % 129.00/18.41 % (3420263)Time elapsed: 1.491 s % 129.00/18.41 % (3420263)Peak memory usage: 53 MB % 129.00/18.41 % (3420263)Instructions burned: 5215 (million) % 129.00/18.41 % (3420277)ott-3_8_sil=64000:random_seed=2549315422:i=20139:bs=on_2951 on theBenchmark for (2951ds/20139Mi) % 129.00/18.41 % (3420273)Instruction limit reached! % 129.00/18.41 % (3420273)------------------------------ % 129.00/18.41 % (3420273)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 129.00/18.41 % (3420273)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 129.00/18.41 % (3420273)CaDiCaL version: 2.1.3 % 129.00/18.41 % (3420273)Termination reason: Instruction limit % 129.00/18.41 % (3420273)Termination phase: Saturation % 129.00/18.41 % (3420273)Time elapsed: 4.992 s % 129.00/18.41 % (3420273)Peak memory usage: 67 MB % 129.00/18.41 % (3420273)Instructions burned: 8173 (million) % 129.00/18.41 % (3420279)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=3102808827:fmbsr=2:i=32576_2913 on theBenchmark for (2913ds/32576Mi) % 129.00/18.41 % (3420279)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 129.00/18.41 % (3420279)Terminated due to inappropriate strategy. % 129.00/18.41 % (3420279)------------------------------ % 129.00/18.41 % (3420279)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 129.00/18.41 % (3420279)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 129.00/18.41 % (3420279)CaDiCaL version: 2.1.3 % 129.00/18.41 % (3420279)Termination reason: Inappropriate % 129.00/18.41 % (3420279)Time elapsed: 0.006 s % 129.00/18.41 % (3420279)Peak memory usage: 11 MB % 129.00/18.41 % (3420279)Instructions burned: 11 (million) % 129.00/18.41 % (3420279)------------------------------ % 129.00/18.41 % (3420279)------------------------------ % 129.00/18.41 % (3420281)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=1292679343:i=11404_2912 on theBenchmark for (2912ds/11404Mi) % 129.00/18.41 % (3420275)Instruction limit reached! % 129.00/18.41 % (3420275)------------------------------ % 129.00/18.41 % (3420275)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 129.00/18.41 % (3420275)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 129.00/18.41 % (3420275)CaDiCaL version: 2.1.3 % 129.00/18.41 % (3420275)Termination reason: Instruction limit % 129.00/18.41 % (3420275)Termination phase: Saturation % 129.00/18.41 % (3420275)Time elapsed: 4.875 s % 129.00/18.41 % (3420275)Peak memory usage: 53 MB % 129.00/18.41 % (3420275)Instructions burned: 9156 (million) % 129.00/18.41 % (3420283)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=2424970961:i=14134_2909 on theBenchmark for (2909ds/14134Mi) % 129.00/18.41 % (3420277)Instruction limit reached! % 129.00/18.41 % (3420277)------------------------------ % 129.00/18.41 % (3420277)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 129.00/18.41 % (3420277)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 129.00/18.41 % (3420277)CaDiCaL version: 2.1.3 % 129.00/18.41 % (3420277)Termination reason: Instruction limit % 129.00/18.41 % (3420277)Termination phase: Saturation % 129.00/18.41 % (3420277)Time elapsed: 6.900 s % 129.00/18.41 % (3420277)Peak memory usage: 99 MB % 129.00/18.41 % (3420277)Instructions burned: 20140 (million) % 129.00/18.41 % (3420359)dis+33_16_sil=32000:sac=on:random_seed=2484672695:i=15851:nm=0_2882 on theBenchmark for (2882ds/15851Mi) % 129.00/18.41 % (3420271)Instruction limit reached! % 129.00/18.41 % (3420271)------------------------------ % 129.00/18.41 % (3420271)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 161.90/23.09 % (3420271)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 161.90/23.09 % (3420271)CaDiCaL version: 2.1.3 % 161.90/23.09 % (3420271)Termination reason: Instruction limit % 161.90/23.09 % (3420271)Termination phase: Saturation % 161.90/23.09 % (3420271)Time elapsed: 9.720 s % 161.90/23.09 % (3420271)Peak memory usage: 23 MB % 161.90/23.09 % (3420271)Instructions burned: 22567 (million) % 161.90/23.09 % (3420549)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=823720584:avsq=on:i=17627:add=on:amm=off_2868 on theBenchmark for (2868ds/17627Mi) % 161.90/23.09 % (3420281)Instruction limit reached! % 161.90/23.09 % (3420281)------------------------------ % 161.90/23.09 % (3420281)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 161.90/23.09 % (3420281)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 161.90/23.09 % (3420281)CaDiCaL version: 2.1.3 % 161.90/23.09 % (3420281)Termination reason: Instruction limit % 161.90/23.09 % (3420281)Termination phase: Saturation % 161.90/23.09 % (3420281)Time elapsed: 8.905 s % 161.90/23.09 % (3420281)Peak memory usage: 80 MB % 161.90/23.09 % (3420281)Instructions burned: 11404 (million) % 161.90/23.09 % (3420711)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=3316142266:s2a=on:i=53295_2823 on theBenchmark for (2823ds/53295Mi) % 161.90/23.09 % (3420359)Instruction limit reached! % 161.90/23.09 % (3420359)------------------------------ % 161.90/23.09 % (3420359)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 161.90/23.09 % (3420359)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 161.90/23.09 % (3420359)CaDiCaL version: 2.1.3 % 161.90/23.09 % (3420359)Termination reason: Instruction limit % 161.90/23.09 % (3420359)Termination phase: Saturation % 161.90/23.09 % (3420359)Time elapsed: 5.925 s % 161.90/23.09 % (3420359)Peak memory usage: 143 MB % 161.90/23.09 % (3420359)Instructions burned: 15855 (million) % 161.90/23.09 % (3420724)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=2641453897:i=26857:ins=20_2823 on theBenchmark for (2823ds/26857Mi) % 161.90/23.09 % (3420724)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 161.90/23.09 % (3420724)Terminated due to inappropriate strategy. % 161.90/23.09 % (3420724)------------------------------ % 161.90/23.09 % (3420724)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 161.90/23.09 % (3420724)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 161.90/23.09 % (3420724)CaDiCaL version: 2.1.3 % 161.90/23.09 % (3420724)Termination reason: Inappropriate % 161.90/23.09 % (3420724)Time elapsed: 0.003 s % 161.90/23.09 % (3420724)Peak memory usage: 11 MB % 161.90/23.09 % (3420724)Instructions burned: 9 (million) % 161.90/23.09 % (3420724)------------------------------ % 161.90/23.09 % (3420724)------------------------------ % 161.90/23.09 % (3420728)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=2672353032:i=28120:bs=on:fsr=off_2822 on theBenchmark for (2822ds/28120Mi) % 161.90/23.09 % (3420257)Instruction limit reached! % 161.90/23.09 % (3420257)------------------------------ % 161.90/23.09 % (3420257)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 161.90/23.09 % (3420257)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 161.90/23.09 % (3420257)CaDiCaL version: 2.1.3 % 161.90/23.09 % (3420257)Termination reason: Instruction limit % 161.90/23.09 % (3420257)Termination phase: Saturation % 161.90/23.09 % (3420257)Time elapsed: 14.857 s % 161.90/23.09 % (3420257)Peak memory usage: 282 MB % 161.90/23.09 % (3420257)Instructions burned: 29341 (million) % 161.90/23.09 % (3420783)fmb+10_1_sil=256000:fmbss=7:random_seed=1916915544:fmbsr=1.6:i=182295_2819 on theBenchmark for (2819ds/182295Mi) % 161.90/23.09 % (3420783)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 161.90/23.09 % (3420783)Terminated due to inappropriate strategy. % 161.90/23.09 % (3420783)------------------------------ % 161.90/23.09 % (3420783)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 161.90/23.09 % (3420783)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 161.90/23.09 % (3420783)CaDiCaL version: 2.1.3 % 161.90/23.09 % (3420783)Termination reason: Inappropriate % 161.90/23.09 % (3420783)Time elapsed: 0.005 s % 161.90/23.09 % (3420783)Peak memory usage: 11 MB % 161.90/23.09 % (3420783)Instructions burned: 9 (million) % 161.90/23.09 % (3420783)------------------------------ % 161.90/23.09 % (3420783)------------------------------ % 161.90/23.09 % (3420788)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=2766490604:i=44625:gsp=on_2819 on theBenchmark for (2819ds/44625Mi) % 167.26/23.88 % (3420788)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 167.26/23.88 % (3420788)Terminated due to inappropriate strategy. % 167.26/23.88 % (3420788)------------------------------ % 167.26/23.88 % (3420788)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 167.26/23.88 % (3420788)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 167.26/23.88 % (3420788)CaDiCaL version: 2.1.3 % 167.26/23.88 % (3420788)Termination reason: Inappropriate % 167.26/23.88 % (3420788)Time elapsed: 0.005 s % 167.26/23.88 % (3420788)Peak memory usage: 11 MB % 167.26/23.88 % (3420788)Instructions burned: 9 (million) % 167.26/23.88 % (3420788)------------------------------ % 167.26/23.88 % (3420788)------------------------------ % 167.26/23.88 % (3420798)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=4124489602:i=160505_2819 on theBenchmark for (2819ds/160505Mi) % 167.26/23.88 % (3420798)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 167.26/23.88 % (3420798)Terminated due to inappropriate strategy. % 167.26/23.88 % (3420798)------------------------------ % 167.26/23.88 % (3420798)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 167.26/23.88 % (3420798)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 167.26/23.88 % (3420798)CaDiCaL version: 2.1.3 % 167.26/23.88 % (3420798)Termination reason: Inappropriate % 167.26/23.88 % (3420798)Time elapsed: 0.005 s % 167.26/23.88 % (3420798)Peak memory usage: 11 MB % 167.26/23.88 % (3420798)Instructions burned: 9 (million) % 167.26/23.88 % (3420798)------------------------------ % 167.26/23.88 % (3420798)------------------------------ % 167.26/23.88 % (3420800)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=4003886879:fmbsr=1.3:i=225729_2819 on theBenchmark for (2819ds/225729Mi) % 167.26/23.88 % (3420800)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 167.26/23.88 % (3420800)Terminated due to inappropriate strategy. % 167.26/23.88 % (3420800)------------------------------ % 167.26/23.88 % (3420800)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 167.26/23.88 % (3420800)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 167.26/23.88 % (3420800)CaDiCaL version: 2.1.3 % 167.26/23.88 % (3420800)Termination reason: Inappropriate % 167.26/23.88 % (3420800)Time elapsed: 0.005 s % 167.26/23.88 % (3420800)Peak memory usage: 11 MB % 167.26/23.88 % (3420800)Instructions burned: 9 (million) % 167.26/23.88 % (3420800)------------------------------ % 167.26/23.88 % (3420800)------------------------------ % 167.26/23.88 % (3420802)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=2258897193:fmbsr=2:i=185024:ins=7_2818 on theBenchmark for (2818ds/185024Mi) % 167.26/23.88 % (3420802)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 167.26/23.88 % (3420802)Terminated due to inappropriate strategy. % 167.26/23.88 % (3420802)------------------------------ % 167.26/23.88 % (3420802)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 167.26/23.88 % (3420802)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 167.26/23.88 % (3420802)CaDiCaL version: 2.1.3 % 167.26/23.88 % (3420802)Termination reason: Inappropriate % 167.26/23.88 % (3420802)Time elapsed: 0.005 s % 167.26/23.88 % (3420802)Peak memory usage: 11 MB % 167.26/23.88 % (3420802)Instructions burned: 9 (million) % 167.26/23.88 % (3420802)------------------------------ % 167.26/23.88 % (3420802)------------------------------ % 167.26/23.88 % (3420804)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=745944146:rtra=on_2818 on theBenchmark for (2818ds/0Mi) % 167.26/23.88 % (3420804)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 167.26/23.88 % (3420804)Terminated due to inappropriate strategy. % 167.26/23.88 % (3420804)------------------------------ % 167.26/23.88 % (3420804)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 167.26/23.88 % (3420804)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 167.26/23.88 % (3420804)CaDiCaL version: 2.1.3 % 167.26/23.88 % (3420804)Termination reason: Inappropriate % 167.26/23.88 % (3420804)Time elapsed: 0.007 s % 167.26/23.88 % (3420804)Peak memory usage: 11 MB % 167.26/23.88 % (3420804)Instructions burned: 12 (million) % 167.26/23.88 % (3420804)------------------------------ % 167.26/23.88 % (3420804)------------------------------ % 167.26/23.88 % (3420807)% WARNING: option uhcvi not known. % 167.26/23.88 % (3420807)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1434284910:i=271062:add=off:rtra=on:rawr=on_2818 on theBenchmark for (2818ds/271062Mi) % 176.09/25.13 % (3420283)Instruction limit reached! % 176.09/25.13 % (3420283)------------------------------ % 176.09/25.13 % (3420283)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 176.09/25.13 % (3420283)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 176.09/25.13 % (3420283)CaDiCaL version: 2.1.3 % 176.09/25.13 % (3420283)Termination reason: Instruction limit % 176.09/25.13 % (3420283)Termination phase: Saturation % 176.09/25.13 % (3420283)Time elapsed: 9.984 s % 176.09/25.13 % (3420283)Peak memory usage: 79 MB % 176.09/25.13 % (3420283)Instructions burned: 14135 (million) % 176.09/25.13 % (3420855)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=32007834:i=176048:add=on:rtra=on:rawr=on_2809 on theBenchmark for (2809ds/176048Mi) % 176.09/25.13 % (3420728)Instruction limit reached! % 176.09/25.13 % (3420728)------------------------------ % 176.09/25.13 % (3420728)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 176.09/25.13 % (3420728)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 176.09/25.13 % (3420728)CaDiCaL version: 2.1.3 % 176.09/25.13 % (3420728)Termination reason: Instruction limit % 176.09/25.13 % (3420728)Termination phase: Saturation % 176.09/25.13 % (3420728)Time elapsed: 4.697 s % 176.09/25.13 % (3420728)Peak memory usage: 13 MB % 176.09/25.13 % (3420728)Instructions burned: 28123 (million) % 176.09/25.13 % (3420857)dis+10_1_sil=32000:si=on:sp=arity:random_seed=1690982459:i=206:fgj=on:rtra=on_2775 on theBenchmark for (2775ds/206Mi) % 176.09/25.13 % (3420857)Instruction limit reached! % 176.09/25.13 % (3420857)------------------------------ % 176.09/25.13 % (3420857)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 176.09/25.13 % (3420857)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 176.09/25.13 % (3420857)CaDiCaL version: 2.1.3 % 176.09/25.13 % (3420857)Termination reason: Instruction limit % 176.09/25.13 % (3420857)Termination phase: Saturation % 176.09/25.13 % (3420857)Time elapsed: 0.087 s % 176.09/25.13 % (3420857)Peak memory usage: 14 MB % 176.09/25.13 % (3420857)Instructions burned: 206 (million) % 176.09/25.13 % (3420859)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=1992148798:i=232:rtra=on_2774 on theBenchmark for (2774ds/232Mi) % 176.09/25.13 % (3420859)Instruction limit reached! % 176.09/25.13 % (3420859)------------------------------ % 176.09/25.13 % (3420859)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 176.09/25.13 % (3420859)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 176.09/25.13 % (3420859)CaDiCaL version: 2.1.3 % 176.09/25.13 % (3420859)Termination reason: Instruction limit % 176.09/25.13 % (3420859)Termination phase: Saturation % 176.09/25.13 % (3420859)Time elapsed: 0.081 s % 176.09/25.13 % (3420859)Peak memory usage: 14 MB % 176.09/25.13 % (3420859)Instructions burned: 234 (million) % 176.09/25.13 % (3420861)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=1048675548:i=262:rtra=on_2773 on theBenchmark for (2773ds/262Mi) % 176.09/25.13 % (3420861)Instruction limit reached! % 176.09/25.13 % (3420861)------------------------------ % 176.09/25.13 % (3420861)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 176.09/25.13 % (3420861)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 176.09/25.13 % (3420861)CaDiCaL version: 2.1.3 % 176.09/25.13 % (3420861)Termination reason: Instruction limit % 176.09/25.13 % (3420861)Termination phase: Saturation % 176.09/25.13 % (3420861)Time elapsed: 0.085 s % 176.09/25.13 % (3420861)Peak memory usage: 14 MB % 176.09/25.13 % (3420861)Instructions burned: 265 (million) % 176.09/25.13 % (3420863)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=889010695:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2772 on theBenchmark for (2772ds/318Mi) % 176.09/25.13 % (3420863)Instruction limit reached! % 176.09/25.13 % (3420863)------------------------------ % 176.09/25.13 % (3420863)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 176.09/25.13 % (3420863)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 176.09/25.13 % (3420863)CaDiCaL version: 2.1.3 % 176.09/25.13 % (3420863)Termination reason: Instruction limit % 176.09/25.13 % (3420863)Termination phase: Saturation % 176.09/25.13 % (3420863)Time elapsed: 0.119 s % 176.09/25.13 % (3420863)Peak memory usage: 15 MB % 176.09/25.13 % (3420863)Instructions burned: 320 (million) % 176.09/25.13 % (3420865)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=27876792:i=1428:nm=2:rtra=on_2771 on theBenchmark for (2771ds/1428Mi) % 184.36/26.26 % (3420865)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 184.36/26.26 % (3420865)Terminated due to inappropriate strategy. % 184.36/26.26 % (3420865)------------------------------ % 184.36/26.26 % (3420865)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 184.36/26.26 % (3420865)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 184.36/26.26 % (3420865)CaDiCaL version: 2.1.3 % 184.36/26.26 % (3420865)Termination reason: Inappropriate % 184.36/26.26 % (3420865)Time elapsed: 0.003 s % 184.36/26.26 % (3420865)Peak memory usage: 11 MB % 184.36/26.26 % (3420865)Instructions burned: 10 (million) % 184.36/26.26 % (3420865)------------------------------ % 184.36/26.26 % (3420865)------------------------------ % 184.36/26.26 % (3420867)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=786673511:i=262:bd=preordered:rtra=on:fsd=on_2771 on theBenchmark for (2771ds/262Mi) % 184.36/26.26 % (3420867)Instruction limit reached! % 184.36/26.26 % (3420867)------------------------------ % 184.36/26.26 % (3420867)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 184.36/26.26 % (3420867)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 184.36/26.26 % (3420867)CaDiCaL version: 2.1.3 % 184.36/26.26 % (3420867)Termination reason: Instruction limit % 184.36/26.26 % (3420867)Termination phase: Saturation % 184.36/26.26 % (3420867)Time elapsed: 0.091 s % 184.36/26.26 % (3420867)Peak memory usage: 14 MB % 184.36/26.26 % (3420867)Instructions burned: 263 (million) % 184.36/26.26 % (3420869)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=608809864:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2770 on theBenchmark for (2770ds/1368Mi) % 184.36/26.26 % (3420869)Instruction limit reached! % 184.36/26.26 % (3420869)------------------------------ % 184.36/26.26 % (3420869)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 184.36/26.26 % (3420869)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 184.36/26.26 % (3420869)CaDiCaL version: 2.1.3 % 184.36/26.26 % (3420869)Termination reason: Instruction limit % 184.36/26.26 % (3420869)Termination phase: Saturation % 184.36/26.26 % (3420869)Time elapsed: 0.386 s % 184.36/26.26 % (3420869)Peak memory usage: 20 MB % 184.36/26.26 % (3420869)Instructions burned: 1369 (million) % 184.36/26.26 % (3420871)ott-21_1_sil=16000:si=on:fs=off:random_seed=849458667:i=360:av=off:fsr=off:rtra=on_2766 on theBenchmark for (2766ds/360Mi) % 184.36/26.26 % (3420871)Instruction limit reached! % 184.36/26.26 % (3420871)------------------------------ % 184.36/26.26 % (3420871)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 184.36/26.26 % (3420871)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 184.36/26.26 % (3420871)CaDiCaL version: 2.1.3 % 184.36/26.26 % (3420871)Termination reason: Instruction limit % 184.36/26.26 % (3420871)Termination phase: Saturation % 184.36/26.26 % (3420871)Time elapsed: 0.097 s % 184.36/26.26 % (3420871)Peak memory usage: 14 MB % 184.36/26.26 % (3420871)Instructions burned: 361 (million) % 184.36/26.26 % (3420873)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1523666745:i=954:bd=all:rtra=on_2765 on theBenchmark for (2765ds/954Mi) % 184.36/26.26 % (3420549)Instruction limit reached! % 184.36/26.26 % (3420549)------------------------------ % 184.36/26.26 % (3420549)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 184.36/26.26 % (3420549)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 184.36/26.26 % (3420549)CaDiCaL version: 2.1.3 % 184.36/26.26 % (3420549)Termination reason: Instruction limit % 184.36/26.26 % (3420549)Termination phase: Saturation % 184.36/26.26 % (3420549)Time elapsed: 10.447 s % 184.36/26.26 % (3420549)Peak memory usage: 92 MB % 184.36/26.26 % (3420549)Instructions burned: 17627 (million) % 184.36/26.26 % (3420875)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=2598246774:fmbsr=1.3:i=1730:ins=25:rtra=on_2763 on theBenchmark for (2763ds/1730Mi) % 184.36/26.26 % (3420875)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 184.36/26.26 % (3420875)Terminated due to inappropriate strategy. % 184.36/26.26 % (3420875)------------------------------ % 184.36/26.26 % (3420875)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 184.36/26.26 % (3420875)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 184.36/26.26 % (3420875)CaDiCaL version: 2.1.3 % 184.36/26.26 % (3420875)Termination reason: Inappropriate % 184.36/26.26 % (3420875)Time elapsed: 0.006 s % 238.34/33.89 % (3420875)Peak memory usage: 10 MB % 238.34/33.89 % (3420875)Instructions burned: 11 (million) % 238.34/33.89 % (3420875)------------------------------ % 238.34/33.89 % (3420875)------------------------------ % 238.34/33.89 % (3420877)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=2032264856:i=2358:rtra=on_2763 on theBenchmark for (2763ds/2358Mi) % 238.34/33.89 % (3420873)Instruction limit reached! % 238.34/33.89 % (3420873)------------------------------ % 238.34/33.89 % (3420873)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 238.34/33.89 % (3420873)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 238.34/33.89 % (3420873)CaDiCaL version: 2.1.3 % 238.34/33.89 % (3420873)Termination reason: Instruction limit % 238.34/33.89 % (3420873)Termination phase: Saturation % 238.34/33.89 % (3420873)Time elapsed: 0.334 s % 238.34/33.89 % (3420873)Peak memory usage: 16 MB % 238.34/33.89 % (3420873)Instructions burned: 956 (million) % 238.34/33.89 % (3420879)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=2636088816:i=1778:ins=1:rtra=on_2761 on theBenchmark for (2761ds/1778Mi) % 238.34/33.89 % (3420879)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 238.34/33.89 % (3420879)Terminated due to inappropriate strategy. % 238.34/33.89 % (3420879)------------------------------ % 238.34/33.89 % (3420879)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 238.34/33.89 % (3420879)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 238.34/33.89 % (3420879)CaDiCaL version: 2.1.3 % 238.34/33.89 % (3420879)Termination reason: Inappropriate % 238.34/33.89 % (3420879)Time elapsed: 0.003 s % 238.34/33.89 % (3420879)Peak memory usage: 10 MB % 238.34/33.89 % (3420879)Instructions burned: 10 (million) % 238.34/33.89 % (3420879)------------------------------ % 238.34/33.89 % (3420879)------------------------------ % 238.34/33.89 % (3420881)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=3822448121:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2761 on theBenchmark for (2761ds/1384Mi) % 238.34/33.89 % (3420881)Instruction limit reached! % 238.34/33.89 % (3420881)------------------------------ % 238.34/33.89 % (3420881)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 238.34/33.89 % (3420881)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 238.34/33.89 % (3420881)CaDiCaL version: 2.1.3 % 238.34/33.89 % (3420881)Termination reason: Instruction limit % 238.34/33.89 % (3420881)Termination phase: Saturation % 238.34/33.89 % (3420881)Time elapsed: 0.469 s % 238.34/33.89 % (3420881)Peak memory usage: 25 MB % 238.34/33.89 % (3420881)Instructions burned: 1386 (million) % 238.34/33.89 % (3420883)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=45241494:i=1758:kws=inv_precedence:fsr=off:rtra=on_2756 on theBenchmark for (2756ds/1758Mi) % 238.34/33.89 % (3420883)Instruction limit reached! % 238.34/33.89 % (3420883)------------------------------ % 238.34/33.89 % (3420883)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 238.34/33.89 % (3420883)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 238.34/33.89 % (3420883)CaDiCaL version: 2.1.3 % 238.34/33.89 % (3420883)Termination reason: Instruction limit % 238.34/33.89 % (3420883)Termination phase: Saturation % 238.34/33.89 % (3420883)Time elapsed: 0.546 s % 238.34/33.89 % (3420883)Peak memory usage: 26 MB % 238.34/33.89 % (3420883)Instructions burned: 1759 (million) % 238.34/33.89 % (3420886)fmb+10_1_sil=64000:si=on:random_seed=2423306059:i=44122:nm=2:rtra=on:gsp=on_2751 on theBenchmark for (2751ds/44122Mi) % 238.34/33.89 % (3420886)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 238.34/33.89 % (3420886)Terminated due to inappropriate strategy. % 238.34/33.89 % (3420886)------------------------------ % 238.34/33.89 % (3420886)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 238.34/33.89 % (3420886)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 238.34/33.89 % (3420886)CaDiCaL version: 2.1.3 % 238.34/33.89 % (3420886)Termination reason: Inappropriate % 238.34/33.89 % (3420886)Time elapsed: 0.003 s % 238.34/33.89 % (3420886)Peak memory usage: 11 MB % 238.34/33.89 % (3420886)Instructions burned: 11 (million) % 238.34/33.89 % (3420886)------------------------------ % 238.34/33.89 % (3420886)------------------------------ % 238.34/33.89 % (3420888)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=2093877090:i=19030:nm=5:rtra=on_2751 on theBenchmark for (2751ds/19030Mi) % 287.34/40.76 % (3420888)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 287.34/40.76 % (3420888)Terminated due to inappropriate strategy. % 287.34/40.76 % (3420888)------------------------------ % 287.34/40.76 % (3420888)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 287.34/40.76 % (3420888)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 287.34/40.76 % (3420888)CaDiCaL version: 2.1.3 % 287.34/40.76 % (3420888)Termination reason: Inappropriate % 287.34/40.76 % (3420888)Time elapsed: 0.003 s % 287.34/40.76 % (3420888)Peak memory usage: 11 MB % 287.34/40.76 % (3420888)Instructions burned: 10 (million) % 287.34/40.76 % (3420888)------------------------------ % 287.34/40.76 % (3420888)------------------------------ % 287.34/40.76 % (3420877)Instruction limit reached! % 287.34/40.76 % (3420877)------------------------------ % 287.34/40.76 % (3420877)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 287.34/40.76 % (3420877)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 287.34/40.76 % (3420877)CaDiCaL version: 2.1.3 % 287.34/40.76 % (3420877)Termination reason: Instruction limit % 287.34/40.76 % (3420877)Termination phase: Saturation % 287.34/40.76 % (3420877)Time elapsed: 1.236 s % 287.34/40.76 % (3420877)Peak memory usage: 22 MB % 287.34/40.76 % (3420877)Instructions burned: 2359 (million) % 287.34/40.76 % (3420890)fmb+10_1_sil=64000:sas=cadical:si=on:fmbss=8:random_seed=3630631117:fmbsr=1.7:i=1840:rtra=on_2750 on theBenchmark for (2750ds/1840Mi) % 287.34/40.76 % (3420891)dis-4_1_sil=16000:drc=ordering:si=on:sp=const_frequency:sac=on:newcnf=on:random_seed=2920285078:i=10262:rtra=on_2750 on theBenchmark for (2750ds/10262Mi) % 287.34/40.76 % (3420890)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 287.34/40.76 % (3420890)Terminated due to inappropriate strategy. % 287.34/40.76 % (3420890)------------------------------ % 287.34/40.76 % (3420890)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 287.34/40.76 % (3420890)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 287.34/40.76 % (3420890)CaDiCaL version: 2.1.3 % 287.34/40.76 % (3420890)Termination reason: Inappropriate % 287.34/40.76 % (3420890)Time elapsed: 0.006 s % 287.34/40.76 % (3420890)Peak memory usage: 11 MB % 287.34/40.76 % (3420890)Instructions burned: 10 (million) % 287.34/40.76 % (3420890)------------------------------ % 287.34/40.76 % (3420890)------------------------------ % 287.34/40.76 % (3420894)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:si=on:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3651161404:i=2944:ins=7:rtra=on:fdi=8:gsp=on_2750 on theBenchmark for (2750ds/2944Mi) % 287.34/40.76 % (3420894)Instruction limit reached! % 287.34/40.76 % (3420894)------------------------------ % 287.34/40.76 % (3420894)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 287.34/40.76 % (3420894)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 287.34/40.76 % (3420894)CaDiCaL version: 2.1.3 % 287.34/40.76 % (3420894)Termination reason: Instruction limit % 287.34/40.76 % (3420894)Termination phase: Saturation % 287.34/40.76 % (3420894)Time elapsed: 1.045 s % 287.34/40.76 % (3420894)Peak memory usage: 32 MB % 287.34/40.76 % (3420894)Instructions burned: 2946 (million) % 287.34/40.76 % (3420896)fmb+10_1_sil=16000:sas=cadical:si=on:bce=on:fmbss=77:random_seed=2141164665:i=12648:rtra=on_2740 on theBenchmark for (2740ds/12648Mi) % 287.34/40.76 % (3420896)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 287.34/40.76 % (3420896)Terminated due to inappropriate strategy. % 287.34/40.76 % (3420896)------------------------------ % 287.34/40.76 % (3420896)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 287.34/40.76 % (3420896)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 287.34/40.76 % (3420896)CaDiCaL version: 2.1.3 % 287.34/40.76 % (3420896)Termination reason: Inappropriate % 287.34/40.76 % (3420896)Time elapsed: 0.004 s % 287.34/40.76 % (3420896)Peak memory usage: 11 MB % 287.34/40.76 % (3420896)Instructions burned: 12 (million) % 287.34/40.76 % (3420896)------------------------------ % 287.34/40.76 % (3420896)------------------------------ % 287.34/40.76 % (3420898)fmb+10_1_fmbas=function:sil=32000:sas=cadical:si=on:fmbss=16:random_seed=3316321927:fmbsr=2.30978:i=4348:rtra=on_2739 on theBenchmark for (2739ds/4348Mi) % 287.34/40.76 % (3420898)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 287.34/40.76 % (3420898)Terminated due to inappropriate strategy. % 287.34/40.76 % (3420898)------------------------------ % 287.34/40.76 % (3420898)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.09/42.53 % (3420898)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.09/42.53 % (3420898)CaDiCaL version: 2.1.3 % 300.09/42.53 % (3420898)Termination reason: Inappropriate % 300.09/42.53 % (3420898)Time elapsed: 0.003 s % 300.09/42.53 % (3420898)Peak memory usage: 11 MB % 300.09/42.53 % (3420898)Instructions burned: 10 (million) % 300.09/42.53 % (3420898)------------------------------ % 300.09/42.53 % (3420898)------------------------------ % 300.09/42.53 % (3420900)ott-2_1_sil=16000:si=on:newcnf=on:random_seed=67255767:avsq=on:i=1738:avsqr=1,16:kws=inv_arity_squared:rtra=on_2739 on theBenchmark for (2739ds/1738Mi) % 300.09/42.53 % (3420900)Instruction limit reached! % 300.09/42.53 % (3420900)------------------------------ % 300.09/42.53 % (3420900)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.09/42.53 % (3420900)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.09/42.53 % (3420900)CaDiCaL version: 2.1.3 % 300.09/42.53 % (3420900)Termination reason: Instruction limit % 300.09/42.53 % (3420900)Termination phase: Saturation % 300.09/42.53 % (3420900)Time elapsed: 0.631 s % 300.09/42.53 % (3420900)Peak memory usage: 21 MB % 300.09/42.53 % (3420900)Instructions burned: 1740 (million) % 300.09/42.53 % (3421034)ott+10_1_sil=32000:tgt=ground:si=on:random_seed=1086940818:i=10228:av=off:rtra=on_2733 on theBenchmark for (2733ds/10228Mi) % 300.09/42.53 % (3421034)Instruction limit reached! % 300.09/42.53 % (3421034)------------------------------ % 300.09/42.53 % (3421034)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.09/42.53 % (3421034)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.09/42.53 % (3421034)CaDiCaL version: 2.1.3 % 300.09/42.53 % (3421034)Termination reason: Instruction limit % 300.09/42.53 % (3421034)Termination phase: Saturation % 300.09/42.53 % (3421034)Time elapsed: 4.700 s % 300.09/42.53 % (3421034)Peak memory usage: 70 MB % 300.09/42.53 % (3421034)Instructions burned: 10230 (million) % 300.09/42.53 % (3421370)fmb+10_1_sil=64000:sas=cadical:si=on:bce=on:rp=on:random_seed=3708376816:i=108564:rtra=on_2686 on theBenchmark for (2686ds/108564Mi) % 300.09/42.53 % (3421370)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 300.09/42.53 % (3421370)Terminated due to inappropriate strategy. % 300.09/42.53 % (3421370)------------------------------ % 300.09/42.53 % (3421370)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.09/42.53 % (3421370)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.09/42.53 % (3421370)CaDiCaL version: 2.1.3 % 300.09/42.53 % (3421370)Termination reason: Inappropriate % 300.09/42.53 % (3421370)Time elapsed: 0.004 s % 300.09/42.53 % (3421370)Peak memory usage: 11 MB % 300.09/42.53 % (3421370)Instructions burned: 12 (million) % 300.09/42.53 % (3421370)------------------------------ % 300.09/42.53 % (3421370)------------------------------ % 300.09/42.53 % (3421374)dis-11_1_sil=16000:si=on:sp=reverse_frequency:alpa=true:random_seed=1379081085:i=7024:aac=none:rtra=on_2686 on theBenchmark for (2686ds/7024Mi) % 300.09/42.53 % (3420891)Instruction limit reached! % 300.09/42.53 % (3420891)------------------------------ % 300.09/42.53 % (3420891)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.09/42.53 % (3420891)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.09/42.53 % (3420891)CaDiCaL version: 2.1.3 % 300.09/42.53 % (3420891)Termination reason: Instruction limit % 300.09/42.53 % (3420891)Termination phase: Saturation % 300.09/42.53 % (3420891)Time elapsed: 7.282 s % 300.09/42.53 % (3420891)Peak memory usage: 77 MB % 300.09/42.53 % (3420891)Instructions burned: 10263 (million) % 300.09/42.53 % (3421432)dis+21_1_sil=32000:sas=cadical:si=on:random_seed=930584346:i=7546:rtra=on:amm=off_2677 on theBenchmark for (2677ds/7546Mi) % 300.09/42.53 % (3421374)Instruction limit reached! % 300.09/42.53 % (3421374)------------------------------ % 300.09/42.53 % (3421374)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.09/42.53 % (3421374)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.09/42.53 % (3421374)CaDiCaL version: 2.1.3 % 300.09/42.53 % (3421374)Termination reason: Instruction limit % 300.09/42.53 % (3421374)Termination phase: Saturation % 300.09/42.53 % (3421374)Time elapsed: 2.227 s % 300.09/42.53 % (3421374)Peak memory usage: 52 MB % 300.09/42.53 % (3421374)Instructions burned: 7026 (million) % 300.09/42.53 % (3421434)ott+11_1_sil=16000:si=on:gs=on:random_seed=1193936705:s2a=on:i=4502:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:rtra=on:fsd=on_2663 on theBenchma % 300.09/42.54 Terminated %------------------------------------------------------------------------------