%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWC472_1 : TPTP v9.3.1. Released v9.0.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % Computer : n004.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:06:02 PM UTC 2026 % Result : Timeout 300.05s 42.54s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.04 % Problem : SWC472_1 : TPTP v9.3.1. Released v9.0.0. % 0.00/0.08 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.10/0.25 % Computer : n004.cluster.edu % 0.10/0.25 % Model : x86_64 x86_64 % 0.10/0.25 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.25 % Memory : 8046.5625MB % 0.10/0.25 % OS : Linux 6.8.0-71-generic % 0.10/0.25 % CPULimit : 300 % 0.10/0.25 % WCLimit : 300 % 0.10/0.25 % DateTime : Mon Sep 28 09:39:51 UTC 2026 % 0.10/0.25 % CPUTime : % 0.10/0.25 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.27/0.30 Running first-order model finding % 0.27/0.31 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 % 5.90/1.15 % (238260)Will run a generic schedule for satisfiability detection. % 5.90/1.15 % (238265)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=4067182406_2999 on theBenchmark for (2999ds/0Mi) % 5.90/1.15 % (238265)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 5.90/1.15 % (238265)Terminated due to inappropriate strategy. % 5.90/1.15 % (238265)------------------------------ % 5.90/1.15 % (238265)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.90/1.15 % (238265)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.90/1.15 % (238265)CaDiCaL version: 2.1.3 % 5.90/1.15 % (238265)Termination reason: Inappropriate % 5.90/1.15 % (238265)Time elapsed: 0.001 s % 5.90/1.15 % (238265)Peak memory usage: 10 MB % 5.90/1.15 % (238265)Instructions burned: 1 (million) % 5.90/1.15 % (238265)------------------------------ % 5.90/1.15 % (238265)------------------------------ % 5.90/1.15 % (238266)% WARNING: option uhcvi not known. % 5.90/1.15 % (238267)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3978933167:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 5.90/1.15 % (238269)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3970967589:i=116_2999 on theBenchmark for (2999ds/116Mi) % 5.90/1.15 % (238268)dis+10_1_sil=32000:sp=arity:random_seed=4161934945:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 5.90/1.15 % (238266)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=4004317398:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 5.90/1.15 % (238270)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2503001816:i=131_2999 on theBenchmark for (2999ds/131Mi) % 5.90/1.15 % (238271)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3306555461:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 5.90/1.15 % (238273)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2645386843:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 5.90/1.15 % (238273)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 5.90/1.15 % (238273)Terminated due to inappropriate strategy. % 5.90/1.15 % (238273)------------------------------ % 5.90/1.15 % (238273)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.90/1.15 % (238273)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.90/1.15 % (238273)CaDiCaL version: 2.1.3 % 5.90/1.15 % (238273)Termination reason: Inappropriate % 5.90/1.15 % (238273)Time elapsed: 0.001 s % 5.90/1.15 % (238273)Peak memory usage: 10 MB % 5.90/1.15 % (238273)Instructions burned: 1 (million) % 5.90/1.15 % (238273)------------------------------ % 5.90/1.15 % (238273)------------------------------ % 5.90/1.15 % (238281)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3667897039:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 5.90/1.15 % (238268)Instruction limit reached! % 5.90/1.15 % (238268)------------------------------ % 5.90/1.15 % (238268)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.90/1.15 % (238268)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.90/1.15 % (238268)CaDiCaL version: 2.1.3 % 5.90/1.15 % (238268)Termination reason: Instruction limit % 5.90/1.15 % (238268)Termination phase: Saturation % 5.90/1.15 % (238268)Time elapsed: 0.104 s % 5.90/1.15 % (238268)Peak memory usage: 12 MB % 5.90/1.15 % (238268)Instructions burned: 103 (million) % 5.90/1.15 % (238281)Instruction limit reached! % 5.90/1.15 % (238281)------------------------------ % 5.90/1.15 % (238281)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.90/1.15 % (238281)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.90/1.15 % (238281)CaDiCaL version: 2.1.3 % 5.90/1.15 % (238281)Termination reason: Instruction limit % 5.90/1.15 % (238281)Termination phase: Saturation % 5.90/1.15 % (238281)Time elapsed: 0.077 s % 5.90/1.15 % (238281)Peak memory usage: 13 MB % 5.90/1.15 % (238281)Instructions burned: 132 (million) % 5.90/1.15 % (238269)Instruction limit reached! % 5.90/1.15 % (238269)------------------------------ % 5.90/1.15 % (238269)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.90/1.15 % (238269)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.90/1.15 % (238269)CaDiCaL version: 2.1.3 % 5.90/1.15 % (238269)Termination reason: Instruction limit % 5.90/1.15 % (238269)Termination phase: Saturation % 8.25/2.01 % (238269)Time elapsed: 0.117 s % 8.25/2.01 % (238269)Peak memory usage: 12 MB % 8.25/2.01 % (238269)Instructions burned: 118 (million) % 8.25/2.01 % (238270)Instruction limit reached! % 8.25/2.01 % (238270)------------------------------ % 8.25/2.01 % (238270)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.25/2.01 % (238270)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.25/2.01 % (238270)CaDiCaL version: 2.1.3 % 8.25/2.01 % (238270)Termination reason: Instruction limit % 8.25/2.01 % (238270)Termination phase: Saturation % 8.25/2.01 % (238270)Time elapsed: 0.129 s % 8.25/2.01 % (238270)Peak memory usage: 13 MB % 8.25/2.01 % (238270)Instructions burned: 131 (million) % 8.25/2.01 % (238284)ott-21_1_sil=16000:fs=off:random_seed=1288666566:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 8.25/2.01 % (238283)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=2504042803:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi) % 8.25/2.01 % (238285)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3486638558:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 8.25/2.01 % (238286)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=4088746094:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 8.25/2.01 % (238286)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 8.25/2.01 % (238286)Terminated due to inappropriate strategy. % 8.25/2.01 % (238286)------------------------------ % 8.25/2.01 % (238286)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.25/2.01 % (238286)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.25/2.01 % (238286)CaDiCaL version: 2.1.3 % 8.25/2.01 % (238286)Termination reason: Inappropriate % 8.25/2.01 % (238286)Time elapsed: 0.001 s % 8.25/2.01 % (238286)Peak memory usage: 10 MB % 8.25/2.01 % (238286)Instructions burned: 1 (million) % 8.25/2.01 % (238286)------------------------------ % 8.25/2.01 % (238286)------------------------------ % 8.25/2.01 % (238271)Instruction limit reached! % 8.25/2.01 % (238271)------------------------------ % 8.25/2.01 % (238271)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.25/2.01 % (238271)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.25/2.01 % (238271)CaDiCaL version: 2.1.3 % 8.25/2.01 % (238271)Termination reason: Instruction limit % 8.25/2.01 % (238271)Termination phase: Saturation % 8.25/2.01 % (238271)Time elapsed: 0.156 s % 8.25/2.01 % (238271)Peak memory usage: 12 MB % 8.25/2.01 % (238271)Instructions burned: 159 (million) % 8.25/2.01 % (238291)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=515901706:i=1179_2998 on theBenchmark for (2998ds/1179Mi) % 8.25/2.01 % (238292)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3694312198:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi) % 8.25/2.01 % (238292)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 8.25/2.01 % (238292)Terminated due to inappropriate strategy. % 8.25/2.01 % (238292)------------------------------ % 8.25/2.01 % (238292)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.25/2.01 % (238292)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.25/2.01 % (238292)CaDiCaL version: 2.1.3 % 8.25/2.01 % (238292)Termination reason: Inappropriate % 8.25/2.01 % (238292)Time elapsed: 0.002 s % 8.25/2.01 % (238292)Peak memory usage: 10 MB % 8.25/2.01 % (238292)Instructions burned: 1 (million) % 8.25/2.01 % (238292)------------------------------ % 8.25/2.01 % (238292)------------------------------ % 8.25/2.01 % (238284)Instruction limit reached! % 8.25/2.01 % (238284)------------------------------ % 8.25/2.01 % (238284)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.25/2.01 % (238284)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.25/2.01 % (238284)CaDiCaL version: 2.1.3 % 8.25/2.01 % (238284)Termination reason: Instruction limit % 8.25/2.01 % (238284)Termination phase: Saturation % 8.25/2.01 % (238284)Time elapsed: 0.078 s % 8.25/2.01 % (238284)Peak memory usage: 12 MB % 8.25/2.01 % (238284)Instructions burned: 182 (million) % 8.25/2.01 % (238295)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=198537151:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2997 on theBenchmark for (2997ds/692Mi) % 37.01/5.59 % (238296)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=4266231364:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi) % 37.01/5.59 % (238285)Instruction limit reached! % 37.01/5.59 % (238285)------------------------------ % 37.01/5.59 % (238285)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 37.01/5.59 % (238285)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 37.01/5.59 % (238285)CaDiCaL version: 2.1.3 % 37.01/5.59 % (238285)Termination reason: Instruction limit % 37.01/5.59 % (238285)Termination phase: Saturation % 37.01/5.59 % (238285)Time elapsed: 0.477 s % 37.01/5.59 % (238285)Peak memory usage: 13 MB % 37.01/5.59 % (238285)Instructions burned: 477 (million) % 37.01/5.59 % (238299)fmb+10_1_sil=64000:random_seed=882735859:i=22061:nm=2:gsp=on_2993 on theBenchmark for (2993ds/22061Mi) % 37.01/5.59 % (238299)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 37.01/5.59 % (238299)Terminated due to inappropriate strategy. % 37.01/5.59 % (238299)------------------------------ % 37.01/5.59 % (238299)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 37.01/5.59 % (238299)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 37.01/5.59 % (238299)CaDiCaL version: 2.1.3 % 37.01/5.59 % (238299)Termination reason: Inappropriate % 37.01/5.59 % (238299)Time elapsed: 0.002 s % 37.01/5.59 % (238299)Peak memory usage: 11 MB % 37.01/5.59 % (238299)Instructions burned: 1 (million) % 37.01/5.59 % (238299)------------------------------ % 37.01/5.59 % (238299)------------------------------ % 37.01/5.59 % (238296)Instruction limit reached! % 37.01/5.59 % (238296)------------------------------ % 37.01/5.59 % (238296)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 37.01/5.59 % (238296)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 37.01/5.59 % (238296)CaDiCaL version: 2.1.3 % 37.01/5.59 % (238296)Termination reason: Instruction limit % 37.01/5.59 % (238296)Termination phase: Saturation % 37.01/5.59 % (238296)Time elapsed: 0.462 s % 37.01/5.59 % (238296)Peak memory usage: 18 MB % 37.01/5.59 % (238296)Instructions burned: 880 (million) % 37.01/5.59 % (238301)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3440362078:i=9515:nm=5_2992 on theBenchmark for (2992ds/9515Mi) % 37.01/5.59 % (238301)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 37.01/5.59 % (238301)Terminated due to inappropriate strategy. % 37.01/5.59 % (238301)------------------------------ % 37.01/5.59 % (238301)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 37.01/5.59 % (238301)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 37.01/5.59 % (238301)CaDiCaL version: 2.1.3 % 37.01/5.59 % (238301)Termination reason: Inappropriate % 37.01/5.59 % (238301)Time elapsed: 0.002 s % 37.01/5.59 % (238301)Peak memory usage: 11 MB % 37.01/5.59 % (238301)Instructions burned: 1 (million) % 37.01/5.59 % (238301)------------------------------ % 37.01/5.59 % (238301)------------------------------ % 37.01/5.59 % (238302)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3582766898:fmbsr=1.7:i=920_2992 on theBenchmark for (2992ds/920Mi) % 37.01/5.59 % (238302)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 37.01/5.59 % (238302)Terminated due to inappropriate strategy. % 37.01/5.59 % (238302)------------------------------ % 37.01/5.59 % (238302)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 37.01/5.59 % (238302)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 37.01/5.59 % (238302)CaDiCaL version: 2.1.3 % 37.01/5.59 % (238302)Termination reason: Inappropriate % 37.01/5.59 % (238302)Time elapsed: 0.001 s % 37.01/5.59 % (238302)Peak memory usage: 10 MB % 37.01/5.59 % (238302)Instructions burned: 1 (million) % 37.01/5.59 % (238302)------------------------------ % 37.01/5.59 % (238302)------------------------------ % 37.01/5.59 % (238304)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1773445068:i=5131_2992 on theBenchmark for (2992ds/5131Mi) % 37.01/5.59 % (238307)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2415249940:i=1472:ins=7:fdi=8:gsp=on_2992 on theBenchmark for (2992ds/1472Mi) % 37.01/5.59 % (238283)Instruction limit reached! % 37.01/5.59 % (238283)------------------------------ % 37.01/5.59 % (238283)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 37.01/5.59 % (238283)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 53.36/7.81 % (238283)CaDiCaL version: 2.1.3 % 53.36/7.81 % (238283)Termination reason: Instruction limit % 53.36/7.81 % (238283)Termination phase: Saturation % 53.36/7.81 % (238283)Time elapsed: 0.660 s % 53.36/7.81 % (238283)Peak memory usage: 18 MB % 53.36/7.81 % (238283)Instructions burned: 684 (million) % 53.36/7.81 % (238309)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=2917621487:i=6324_2991 on theBenchmark for (2991ds/6324Mi) % 53.36/7.81 % (238309)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 53.36/7.81 % (238309)Terminated due to inappropriate strategy. % 53.36/7.81 % (238309)------------------------------ % 53.36/7.81 % (238309)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 53.36/7.81 % (238309)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 53.36/7.81 % (238309)CaDiCaL version: 2.1.3 % 53.36/7.81 % (238309)Termination reason: Inappropriate % 53.36/7.81 % (238309)Time elapsed: 0.001 s % 53.36/7.81 % (238309)Peak memory usage: 10 MB % 53.36/7.81 % (238309)Instructions burned: 1 (million) % 53.36/7.81 % (238309)------------------------------ % 53.36/7.81 % (238309)------------------------------ % 53.36/7.81 % (238311)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=3218253983:fmbsr=2.30978:i=2174_2991 on theBenchmark for (2991ds/2174Mi) % 53.36/7.81 % (238311)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 53.36/7.81 % (238311)Terminated due to inappropriate strategy. % 53.36/7.81 % (238311)------------------------------ % 53.36/7.81 % (238311)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 53.36/7.81 % (238311)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 53.36/7.81 % (238311)CaDiCaL version: 2.1.3 % 53.36/7.81 % (238311)Termination reason: Inappropriate % 53.36/7.81 % (238311)Time elapsed: 0.001 s % 53.36/7.81 % (238311)Peak memory usage: 10 MB % 53.36/7.81 % (238311)Instructions burned: 1 (million) % 53.36/7.81 % (238311)------------------------------ % 53.36/7.81 % (238311)------------------------------ % 53.36/7.81 % (238313)ott-2_1_sil=16000:newcnf=on:random_seed=1887059286:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2991 on theBenchmark for (2991ds/869Mi) % 53.36/7.81 % (238295)Instruction limit reached! % 53.36/7.81 % (238295)------------------------------ % 53.36/7.81 % (238295)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 53.36/7.81 % (238295)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 53.36/7.81 % (238295)CaDiCaL version: 2.1.3 % 53.36/7.81 % (238295)Termination reason: Instruction limit % 53.36/7.81 % (238295)Termination phase: Saturation % 53.36/7.81 % (238295)Time elapsed: 0.711 s % 53.36/7.81 % (238295)Peak memory usage: 17 MB % 53.36/7.81 % (238295)Instructions burned: 692 (million) % 53.36/7.81 % (238315)ott+10_1_sil=32000:tgt=ground:random_seed=76948946:i=5114:av=off_2990 on theBenchmark for (2990ds/5114Mi) % 53.36/7.81 % (238291)Instruction limit reached! % 53.36/7.81 % (238291)------------------------------ % 53.36/7.81 % (238291)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 53.36/7.81 % (238291)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 53.36/7.81 % (238291)CaDiCaL version: 2.1.3 % 53.36/7.81 % (238291)Termination reason: Instruction limit % 53.36/7.81 % (238291)Termination phase: Saturation % 53.36/7.81 % (238291)Time elapsed: 1.127 s % 53.36/7.81 % (238291)Peak memory usage: 18 MB % 53.36/7.81 % (238291)Instructions burned: 1179 (million) % 53.36/7.81 % (238319)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=832653006:i=54282_2986 on theBenchmark for (2986ds/54282Mi) % 53.36/7.81 % (238319)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 53.36/7.81 % (238319)Terminated due to inappropriate strategy. % 53.36/7.81 % (238319)------------------------------ % 53.36/7.81 % (238319)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 53.36/7.81 % (238319)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 53.36/7.81 % (238319)CaDiCaL version: 2.1.3 % 53.36/7.81 % (238319)Termination reason: Inappropriate % 53.36/7.81 % (238319)Time elapsed: 0.002 s % 53.36/7.81 % (238319)Peak memory usage: 10 MB % 53.36/7.81 % (238319)Instructions burned: 1 (million) % 53.36/7.81 % (238319)------------------------------ % 53.36/7.81 % (238319)------------------------------ % 53.36/7.81 % (238321)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=1145044347:i=3512:aac=none_2986 on theBenchmark for (2986ds/3512Mi) % 53.36/7.81 % (238313)Instruction limit reached! % 155.86/22.29 % (238313)------------------------------ % 155.86/22.29 % (238313)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 155.86/22.29 % (238313)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 155.86/22.29 % (238313)CaDiCaL version: 2.1.3 % 155.86/22.29 % (238313)Termination reason: Instruction limit % 155.86/22.29 % (238313)Termination phase: Saturation % 155.86/22.29 % (238313)Time elapsed: 0.772 s % 155.86/22.29 % (238313)Peak memory usage: 14 MB % 155.86/22.29 % (238313)Instructions burned: 870 (million) % 155.86/22.29 % (238327)dis+21_1_sil=32000:sas=cadical:random_seed=3122210079:i=3773:amm=off_2983 on theBenchmark for (2983ds/3773Mi) % 155.86/22.29 % (238307)Instruction limit reached! % 155.86/22.29 % (238307)------------------------------ % 155.86/22.29 % (238307)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 155.86/22.29 % (238307)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 155.86/22.29 % (238307)CaDiCaL version: 2.1.3 % 155.86/22.29 % (238307)Termination reason: Instruction limit % 155.86/22.29 % (238307)Termination phase: Saturation % 155.86/22.29 % (238307)Time elapsed: 1.324 s % 155.86/22.29 % (238307)Peak memory usage: 26 MB % 155.86/22.29 % (238307)Instructions burned: 1472 (million) % 155.86/22.29 % (238329)ott+11_1_sil=16000:gs=on:random_seed=917723009:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2978 on theBenchmark for (2978ds/2251Mi) % 155.86/22.29 % (238304)Instruction limit reached! % 155.86/22.29 % (238304)------------------------------ % 155.86/22.29 % (238304)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 155.86/22.29 % (238304)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 155.86/22.29 % (238304)CaDiCaL version: 2.1.3 % 155.86/22.29 % (238304)Termination reason: Instruction limit % 155.86/22.29 % (238304)Termination phase: Saturation % 155.86/22.29 % (238304)Time elapsed: 2.579 s % 155.86/22.29 % (238304)Peak memory usage: 41 MB % 155.86/22.29 % (238304)Instructions burned: 5132 (million) % 155.86/22.29 % (238345)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=904544588:fmbsr=1.6:i=67534_2966 on theBenchmark for (2966ds/67534Mi) % 155.86/22.29 % (238345)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 155.86/22.29 % (238345)Terminated due to inappropriate strategy. % 155.86/22.29 % (238345)------------------------------ % 155.86/22.29 % (238345)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 155.86/22.29 % (238345)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 155.86/22.29 % (238345)CaDiCaL version: 2.1.3 % 155.86/22.29 % (238345)Termination reason: Inappropriate % 155.86/22.29 % (238345)Time elapsed: 0.002 s % 155.86/22.29 % (238345)Peak memory usage: 10 MB % 155.86/22.29 % (238345)Instructions burned: 2 (million) % 155.86/22.29 % (238345)------------------------------ % 155.86/22.29 % (238345)------------------------------ % 155.86/22.29 % (238347)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=858039760:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2966 on theBenchmark for (2966ds/4591Mi) % 155.86/22.29 % (238329)Instruction limit reached! % 155.86/22.29 % (238329)------------------------------ % 155.86/22.29 % (238329)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 155.86/22.29 % (238329)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 155.86/22.29 % (238329)CaDiCaL version: 2.1.3 % 155.86/22.29 % (238329)Termination reason: Instruction limit % 155.86/22.29 % (238329)Termination phase: Saturation % 155.86/22.29 % (238329)Time elapsed: 1.615 s % 155.86/22.29 % (238329)Peak memory usage: 21 MB % 155.86/22.29 % (238329)Instructions burned: 2251 (million) % 155.86/22.29 % (238349)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=3444440197:i=29340_2962 on theBenchmark for (2962ds/29340Mi) % 155.86/22.29 % (238321)Instruction limit reached! % 155.86/22.29 % (238321)------------------------------ % 155.86/22.29 % (238321)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 155.86/22.29 % (238321)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 155.86/22.29 % (238321)CaDiCaL version: 2.1.3 % 155.86/22.29 % (238321)Termination reason: Instruction limit % 155.86/22.29 % (238321)Termination phase: Saturation % 155.86/22.29 % (238321)Time elapsed: 3.137 s % 155.86/22.29 % (238321)Peak memory usage: 33 MB % 155.86/22.29 % (238321)Instructions burned: 3513 (million) % 155.86/22.29 % (238351)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=1653671715:i=5211_2954 on theBenchmark for (2954ds/5211Mi) % 155.86/22.29 % (238327)Instruction limit reached! % 204.43/29.11 % (238327)------------------------------ % 204.43/29.11 % (238327)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 204.43/29.11 % (238327)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 204.43/29.11 % (238327)CaDiCaL version: 2.1.3 % 204.43/29.11 % (238327)Termination reason: Instruction limit % 204.43/29.11 % (238327)Termination phase: Saturation % 204.43/29.11 % (238327)Time elapsed: 3.542 s % 204.43/29.11 % (238327)Peak memory usage: 32 MB % 204.43/29.11 % (238327)Instructions burned: 3774 (million) % 204.43/29.11 % (238355)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=4279014681:i=5497:nm=2_2947 on theBenchmark for (2947ds/5497Mi) % 204.43/29.11 % (238355)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 204.43/29.11 % (238355)Terminated due to inappropriate strategy. % 204.43/29.11 % (238355)------------------------------ % 204.43/29.11 % (238355)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 204.43/29.11 % (238355)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 204.43/29.11 % (238355)CaDiCaL version: 2.1.3 % 204.43/29.11 % (238355)Termination reason: Inappropriate % 204.43/29.11 % (238355)Time elapsed: 0.003 s % 204.43/29.11 % (238355)Peak memory usage: 10 MB % 204.43/29.11 % (238355)Instructions burned: 1 (million) % 204.43/29.11 % (238355)------------------------------ % 204.43/29.11 % (238355)------------------------------ % 204.43/29.11 % (238357)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=419278027:fmbsr=2:i=46332_2946 on theBenchmark for (2946ds/46332Mi) % 204.43/29.11 % (238357)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 204.43/29.11 % (238357)Terminated due to inappropriate strategy. % 204.43/29.11 % (238357)------------------------------ % 204.43/29.11 % (238357)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 204.43/29.11 % (238357)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 204.43/29.11 % (238357)CaDiCaL version: 2.1.3 % 204.43/29.11 % (238357)Termination reason: Inappropriate % 204.43/29.11 % (238357)Time elapsed: 0.001 s % 204.43/29.11 % (238357)Peak memory usage: 10 MB % 204.43/29.11 % (238357)Instructions burned: 2 (million) % 204.43/29.11 % (238357)------------------------------ % 204.43/29.11 % (238357)------------------------------ % 204.43/29.11 % (238359)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=4157046508:i=14071_2946 on theBenchmark for (2946ds/14071Mi) % 204.43/29.11 % (238359)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 204.43/29.11 % (238359)Terminated due to inappropriate strategy. % 204.43/29.11 % (238359)------------------------------ % 204.43/29.11 % (238359)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 204.43/29.11 % (238359)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 204.43/29.11 % (238359)CaDiCaL version: 2.1.3 % 204.43/29.11 % (238359)Termination reason: Inappropriate % 204.43/29.11 % (238359)Time elapsed: 0.002 s % 204.43/29.11 % (238359)Peak memory usage: 10 MB % 204.43/29.11 % (238359)Instructions burned: 2 (million) % 204.43/29.11 % (238359)------------------------------ % 204.43/29.11 % (238359)------------------------------ % 204.43/29.11 % (238362)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1428286581:i=22565:add=on:rawr=on_2946 on theBenchmark for (2946ds/22565Mi) % 204.43/29.11 % (238315)Instruction limit reached! % 204.43/29.11 % (238315)------------------------------ % 204.43/29.11 % (238315)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 204.43/29.11 % (238315)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 204.43/29.11 % (238315)CaDiCaL version: 2.1.3 % 204.43/29.11 % (238315)Termination reason: Instruction limit % 204.43/29.11 % (238315)Termination phase: Saturation % 204.43/29.11 % (238315)Time elapsed: 5.306 s % 204.43/29.11 % (238315)Peak memory usage: 35 MB % 204.43/29.11 % (238315)Instructions burned: 5114 (million) % 204.43/29.11 % (238375)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=749499108:i=8173:av=off_2936 on theBenchmark for (2936ds/8173Mi) % 204.43/29.11 % (238347)Instruction limit reached! % 204.43/29.11 % (238347)------------------------------ % 204.43/29.11 % (238347)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 204.43/29.11 % (238347)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 204.43/29.11 % (238347)CaDiCaL version: 2.1.3 % 204.43/29.11 % (238347)Termination reason: Instruction limit % 204.43/29.11 % (238347)Termination phase: Saturation % 204.43/29.11 % (238347)Time elapsed: 4.080 s % 206.84/29.43 % (238347)Peak memory usage: 37 MB % 206.84/29.43 % (238347)Instructions burned: 4592 (million) % 206.84/29.43 % (238383)dis+10_16:1_sil=16000:random_seed=2250212672:i=9155:fsr=off_2925 on theBenchmark for (2925ds/9155Mi) % 206.84/29.43 % (238351)Instruction limit reached! % 206.84/29.43 % (238351)------------------------------ % 206.84/29.43 % (238351)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 206.84/29.43 % (238351)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 206.84/29.43 % (238351)CaDiCaL version: 2.1.3 % 206.84/29.43 % (238351)Termination reason: Instruction limit % 206.84/29.43 % (238351)Termination phase: Saturation % 206.84/29.43 % (238351)Time elapsed: 4.521 s % 206.84/29.43 % (238351)Peak memory usage: 49 MB % 206.84/29.43 % (238351)Instructions burned: 5212 (million) % 206.84/29.43 % (238393)ott-3_8_sil=64000:random_seed=825710505:i=20139:bs=on_2909 on theBenchmark for (2909ds/20139Mi) % 206.84/29.43 % (238375)Instruction limit reached! % 206.84/29.43 % (238375)------------------------------ % 206.84/29.43 % (238375)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 206.84/29.43 % (238375)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 206.84/29.43 % (238375)CaDiCaL version: 2.1.3 % 206.84/29.43 % (238375)Termination reason: Instruction limit % 206.84/29.43 % (238375)Termination phase: Saturation % 206.84/29.43 % (238375)Time elapsed: 8.099 s % 206.84/29.43 % (238375)Peak memory usage: 62 MB % 206.84/29.43 % (238375)Instructions burned: 8173 (million) % 206.84/29.43 % (238405)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=1191273881:fmbsr=2:i=32576_2855 on theBenchmark for (2855ds/32576Mi) % 206.84/29.43 % (238405)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 206.84/29.43 % (238405)Terminated due to inappropriate strategy. % 206.84/29.43 % (238405)------------------------------ % 206.84/29.43 % (238405)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 206.84/29.43 % (238405)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 206.84/29.43 % (238405)CaDiCaL version: 2.1.3 % 206.84/29.43 % (238405)Termination reason: Inappropriate % 206.84/29.43 % (238405)Time elapsed: 0.002 s % 206.84/29.43 % (238405)Peak memory usage: 10 MB % 206.84/29.43 % (238405)Instructions burned: 2 (million) % 206.84/29.43 % (238405)------------------------------ % 206.84/29.43 % (238405)------------------------------ % 206.84/29.43 % (238407)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=3141066197:i=11404_2855 on theBenchmark for (2855ds/11404Mi) % 206.84/29.43 % (238349)Instruction limit reached! % 206.84/29.43 % (238349)------------------------------ % 206.84/29.43 % (238349)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 206.84/29.43 % (238349)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 206.84/29.43 % (238349)CaDiCaL version: 2.1.3 % 206.84/29.43 % (238349)Termination reason: Instruction limit % 206.84/29.43 % (238349)Termination phase: Saturation % 206.84/29.43 % (238349)Time elapsed: 11.490 s % 206.84/29.43 % (238349)Peak memory usage: 206 MB % 206.84/29.43 % (238349)Instructions burned: 29342 (million) % 206.84/29.43 % (238409)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=1603033859:i=14134_2847 on theBenchmark for (2847ds/14134Mi) % 206.84/29.43 % (238383)Instruction limit reached! % 206.84/29.43 % (238383)------------------------------ % 206.84/29.43 % (238383)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 206.84/29.43 % (238383)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 206.84/29.43 % (238383)CaDiCaL version: 2.1.3 % 206.84/29.43 % (238383)Termination reason: Instruction limit % 206.84/29.43 % (238383)Termination phase: Saturation % 206.84/29.43 % (238383)Time elapsed: 8.266 s % 206.84/29.43 % (238383)Peak memory usage: 52 MB % 206.84/29.43 % (238383)Instructions burned: 9156 (million) % 206.84/29.43 % (238413)dis+33_16_sil=32000:sac=on:random_seed=2847109125:i=15851:nm=0_2842 on theBenchmark for (2842ds/15851Mi) % 206.84/29.43 % (238362)Instruction limit reached! % 206.84/29.43 % (238362)------------------------------ % 206.84/29.43 % (238362)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 206.84/29.43 % (238362)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 206.84/29.43 % (238362)CaDiCaL version: 2.1.3 % 206.84/29.43 % (238362)Termination reason: Instruction limit % 206.84/29.43 % (238362)Termination phase: Saturation % 206.84/29.43 % (238362)Time elapsed: 16.500 s % 206.84/29.43 % (238362)Peak memory usage: 65 MB % 206.84/29.43 % (238362)Instructions burned: 22565 (million) % 206.84/29.43 % (238423)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=432154125:avsq=on:i=17627:add=on:amm=off_2780 on theBenchmark for (2780ds/17627Mi) % 238.06/33.83 % (238409)Instruction limit reached! % 238.06/33.83 % (238409)------------------------------ % 238.06/33.83 % (238409)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 238.06/33.83 % (238409)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 238.06/33.83 % (238409)CaDiCaL version: 2.1.3 % 238.06/33.83 % (238409)Termination reason: Instruction limit % 238.06/33.83 % (238409)Termination phase: Saturation % 238.06/33.83 % (238409)Time elapsed: 7.923 s % 238.06/33.83 % (238409)Peak memory usage: 74 MB % 238.06/33.83 % (238409)Instructions burned: 14135 (million) % 238.06/33.83 % (238425)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=2374889645:s2a=on:i=53295_2767 on theBenchmark for (2767ds/53295Mi) % 238.06/33.83 % (238407)Instruction limit reached! % 238.06/33.83 % (238407)------------------------------ % 238.06/33.83 % (238407)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 238.06/33.83 % (238407)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 238.06/33.83 % (238407)CaDiCaL version: 2.1.3 % 238.06/33.83 % (238407)Termination reason: Instruction limit % 238.06/33.83 % (238407)Termination phase: Saturation % 238.06/33.83 % (238407)Time elapsed: 11.039 s % 238.06/33.83 % (238407)Peak memory usage: 61 MB % 238.06/33.83 % (238407)Instructions burned: 11404 (million) % 238.06/33.83 % (238433)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=790186264:i=26857:ins=20_2744 on theBenchmark for (2744ds/26857Mi) % 238.06/33.83 % (238433)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 238.06/33.83 % (238433)Terminated due to inappropriate strategy. % 238.06/33.83 % (238433)------------------------------ % 238.06/33.83 % (238433)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 238.06/33.83 % (238433)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 238.06/33.83 % (238433)CaDiCaL version: 2.1.3 % 238.06/33.83 % (238433)Termination reason: Inappropriate % 238.06/33.83 % (238433)Time elapsed: 0.001 s % 238.06/33.83 % (238433)Peak memory usage: 10 MB % 238.06/33.83 % (238433)Instructions burned: 1 (million) % 238.06/33.83 % (238433)------------------------------ % 238.06/33.83 % (238433)------------------------------ % 238.06/33.83 % (238435)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=3658479542:i=28120:bs=on:fsr=off_2744 on theBenchmark for (2744ds/28120Mi) % 238.06/33.83 % (238413)Instruction limit reached! % 238.06/33.83 % (238413)------------------------------ % 238.06/33.83 % (238413)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 238.06/33.83 % (238413)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 238.06/33.83 % (238413)CaDiCaL version: 2.1.3 % 238.06/33.83 % (238413)Termination reason: Instruction limit % 238.06/33.83 % (238413)Termination phase: Saturation % 238.06/33.83 % (238413)Time elapsed: 12.907 s % 238.06/33.83 % (238413)Peak memory usage: 197 MB % 238.06/33.83 % (238413)Instructions burned: 15853 (million) % 238.06/33.83 % (238591)fmb+10_1_sil=256000:fmbss=7:random_seed=2610300062:fmbsr=1.6:i=182295_2712 on theBenchmark for (2712ds/182295Mi) % 238.06/33.83 % (238591)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 238.06/33.83 % (238591)Terminated due to inappropriate strategy. % 238.06/33.83 % (238591)------------------------------ % 238.06/33.83 % (238591)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 238.06/33.83 % (238591)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 238.06/33.83 % (238591)CaDiCaL version: 2.1.3 % 238.06/33.83 % (238591)Termination reason: Inappropriate % 238.06/33.83 % (238591)Time elapsed: 0.001 s % 238.06/33.83 % (238591)Peak memory usage: 10 MB % 238.06/33.83 % (238591)Instructions burned: 1 (million) % 238.06/33.83 % (238591)------------------------------ % 238.06/33.83 % (238591)------------------------------ % 238.06/33.83 % (238593)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=3222803324:i=44625:gsp=on_2712 on theBenchmark for (2712ds/44625Mi) % 238.06/33.83 % (238593)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 238.06/33.83 % (238593)Terminated due to inappropriate strategy. % 238.06/33.83 % (238593)------------------------------ % 238.06/33.83 % (238593)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 238.06/33.83 % (238593)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 238.06/33.83 % (238593)CaDiCaL version: 2.1.3 % 238.06/33.83 % (238593)Termination reason: Inappropriate % 260.29/37.02 % (238593)Time elapsed: 0.001 s % 260.29/37.02 % (238593)Peak memory usage: 11 MB % 260.29/37.02 % (238593)Instructions burned: 1 (million) % 260.29/37.02 % (238593)------------------------------ % 260.29/37.02 % (238593)------------------------------ % 260.29/37.02 % (238595)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=3702705260:i=160505_2712 on theBenchmark for (2712ds/160505Mi) % 260.29/37.02 % (238595)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 260.29/37.02 % (238595)Terminated due to inappropriate strategy. % 260.29/37.02 % (238595)------------------------------ % 260.29/37.02 % (238595)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 260.29/37.02 % (238595)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 260.29/37.02 % (238595)CaDiCaL version: 2.1.3 % 260.29/37.02 % (238595)Termination reason: Inappropriate % 260.29/37.02 % (238595)Time elapsed: 0.001 s % 260.29/37.02 % (238595)Peak memory usage: 10 MB % 260.29/37.02 % (238595)Instructions burned: 1 (million) % 260.29/37.02 % (238595)------------------------------ % 260.29/37.02 % (238595)------------------------------ % 260.29/37.02 % (238597)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=2748294324:fmbsr=1.3:i=225729_2711 on theBenchmark for (2711ds/225729Mi) % 260.29/37.02 % (238597)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 260.29/37.02 % (238597)Terminated due to inappropriate strategy. % 260.29/37.02 % (238597)------------------------------ % 260.29/37.02 % (238597)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 260.29/37.02 % (238597)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 260.29/37.02 % (238597)CaDiCaL version: 2.1.3 % 260.29/37.02 % (238597)Termination reason: Inappropriate % 260.29/37.02 % (238597)Time elapsed: 0.001 s % 260.29/37.02 % (238597)Peak memory usage: 11 MB % 260.29/37.02 % (238597)Instructions burned: 2 (million) % 260.29/37.02 % (238597)------------------------------ % 260.29/37.02 % (238597)------------------------------ % 260.29/37.02 % (238599)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=3757852417:fmbsr=2:i=185024:ins=7_2711 on theBenchmark for (2711ds/185024Mi) % 260.29/37.02 % (238599)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 260.29/37.02 % (238599)Terminated due to inappropriate strategy. % 260.29/37.02 % (238599)------------------------------ % 260.29/37.02 % (238599)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 260.29/37.02 % (238599)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 260.29/37.02 % (238599)CaDiCaL version: 2.1.3 % 260.29/37.02 % (238599)Termination reason: Inappropriate % 260.29/37.02 % (238599)Time elapsed: 0.001 s % 260.29/37.02 % (238599)Peak memory usage: 11 MB % 260.29/37.02 % (238599)Instructions burned: 2 (million) % 260.29/37.02 % (238599)------------------------------ % 260.29/37.02 % (238599)------------------------------ % 260.29/37.02 % (238601)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=2150786277:rtra=on_2711 on theBenchmark for (2711ds/0Mi) % 260.29/37.02 % (238601)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 260.29/37.02 % (238601)Terminated due to inappropriate strategy. % 260.29/37.02 % (238601)------------------------------ % 260.29/37.02 % (238601)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 260.29/37.02 % (238601)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 260.29/37.02 % (238601)CaDiCaL version: 2.1.3 % 260.29/37.02 % (238601)Termination reason: Inappropriate % 260.29/37.02 % (238601)Time elapsed: 0.001 s % 260.29/37.02 % (238601)Peak memory usage: 10 MB % 260.29/37.02 % (238601)Instructions burned: 2 (million) % 260.29/37.02 % (238601)------------------------------ % 260.29/37.02 % (238601)------------------------------ % 260.29/37.02 % (238603)% WARNING: option uhcvi not known. % 260.29/37.02 % (238603)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1820075841:i=271062:add=off:rtra=on:rawr=on_2711 on theBenchmark for (2711ds/271062Mi) % 260.29/37.02 % (238393)Instruction limit reached! % 260.29/37.02 % (238393)------------------------------ % 260.29/37.02 % (238393)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 260.29/37.02 % (238393)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 260.29/37.02 % (238393)CaDiCaL version: 2.1.3 % 260.29/37.02 % (238393)Termination reason: Instruction limit % 260.29/37.02 % (238393)Termination phase: Saturation % 260.29/37.02 % (238393)Time elapsed: 19.969 s % 260.29/37.02 % (238393)Peak memory usage: 73 MB % 260.29/37.02 % (238393)Instructions burned: 20139 (million) % 260.29/37.02 % (238605)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3910634294:i=176048:add=on:rtra=on:rawr=on_2709 on theBenchmark for (2709ds/176048Mi) % 269.08/38.14 % (238423)Instruction limit reached! % 269.08/38.14 % (238423)------------------------------ % 269.08/38.14 % (238423)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 269.08/38.14 % (238423)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 269.08/38.14 % (238423)CaDiCaL version: 2.1.3 % 269.08/38.14 % (238423)Termination reason: Instruction limit % 269.08/38.14 % (238423)Termination phase: Saturation % 269.08/38.14 % (238423)Time elapsed: 10.765 s % 269.08/38.14 % (238423)Peak memory usage: 233 MB % 269.08/38.14 % (238423)Instructions burned: 17628 (million) % 269.08/38.14 % (238607)dis+10_1_sil=32000:si=on:sp=arity:random_seed=3030215782:i=206:fgj=on:rtra=on_2672 on theBenchmark for (2672ds/206Mi) % 269.08/38.14 % (238607)Instruction limit reached! % 269.08/38.14 % (238607)------------------------------ % 269.08/38.14 % (238607)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 269.08/38.14 % (238607)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 269.08/38.14 % (238607)CaDiCaL version: 2.1.3 % 269.08/38.14 % (238607)Termination reason: Instruction limit % 269.08/38.14 % (238607)Termination phase: Saturation % 269.08/38.14 % (238607)Time elapsed: 0.122 s % 269.08/38.14 % (238607)Peak memory usage: 13 MB % 269.08/38.14 % (238607)Instructions burned: 206 (million) % 269.08/38.14 % (238609)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=2477917142:i=232:rtra=on_2670 on theBenchmark for (2670ds/232Mi) % 269.08/38.14 % (238609)Instruction limit reached! % 269.08/38.14 % (238609)------------------------------ % 269.08/38.14 % (238609)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 269.08/38.14 % (238609)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 269.08/38.14 % (238609)CaDiCaL version: 2.1.3 % 269.08/38.14 % (238609)Termination reason: Instruction limit % 269.08/38.14 % (238609)Termination phase: Saturation % 269.08/38.14 % (238609)Time elapsed: 0.149 s % 269.08/38.14 % (238609)Peak memory usage: 13 MB % 269.08/38.14 % (238609)Instructions burned: 233 (million) % 269.08/38.14 % (238611)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=2926934854:i=262:rtra=on_2669 on theBenchmark for (2669ds/262Mi) % 269.08/38.14 % (238611)Instruction limit reached! % 269.08/38.14 % (238611)------------------------------ % 269.08/38.14 % (238611)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 269.08/38.14 % (238611)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 269.08/38.14 % (238611)CaDiCaL version: 2.1.3 % 269.08/38.14 % (238611)Termination reason: Instruction limit % 269.08/38.14 % (238611)Termination phase: Saturation % 269.08/38.14 % (238611)Time elapsed: 0.160 s % 269.08/38.14 % (238611)Peak memory usage: 14 MB % 269.08/38.14 % (238611)Instructions burned: 262 (million) % 269.08/38.14 % (238614)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=3370307582:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2667 on theBenchmark for (2667ds/318Mi) % 269.08/38.14 % (238614)Instruction limit reached! % 269.08/38.14 % (238614)------------------------------ % 269.08/38.14 % (238614)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 269.08/38.14 % (238614)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 269.08/38.14 % (238614)CaDiCaL version: 2.1.3 % 269.08/38.14 % (238614)Termination reason: Instruction limit % 269.08/38.14 % (238614)Termination phase: Saturation % 269.08/38.14 % (238614)Time elapsed: 0.204 s % 269.08/38.14 % (238614)Peak memory usage: 13 MB % 269.08/38.14 % (238614)Instructions burned: 319 (million) % 269.08/38.14 % (238616)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=182884957:i=1428:nm=2:rtra=on_2665 on theBenchmark for (2665ds/1428Mi) % 269.08/38.14 % (238616)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 269.08/38.14 % (238616)Terminated due to inappropriate strategy. % 269.08/38.14 % (238616)------------------------------ % 269.08/38.14 % (238616)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 269.08/38.14 % (238616)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 269.08/38.14 % (238616)CaDiCaL version: 2.1.3 % 269.08/38.14 % (238616)Termination reason: Inappropriate % 269.08/38.14 % (238616)Time elapsed: 0.001 s % 269.08/38.14 % (238616)Peak memory usage: 10 MB % 269.08/38.14 % (238616)Instructions burned: 2 (million) % 269.08/38.14 % (238616)------------------------------ % 269.08/38.14 % (238616)------------------------------ % 281.56/40.01 % (238618)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=2000370582:i=262:bd=preordered:rtra=on:fsd=on_2664 on theBenchmark for (2664ds/262Mi) % 281.56/40.01 % (238618)Instruction limit reached! % 281.56/40.01 % (238618)------------------------------ % 281.56/40.01 % (238618)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 281.56/40.01 % (238618)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 281.56/40.01 % (238618)CaDiCaL version: 2.1.3 % 281.56/40.01 % (238618)Termination reason: Instruction limit % 281.56/40.01 % (238618)Termination phase: Saturation % 281.56/40.01 % (238618)Time elapsed: 0.172 s % 281.56/40.01 % (238618)Peak memory usage: 14 MB % 281.56/40.01 % (238618)Instructions burned: 262 (million) % 281.56/40.01 % (238620)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=2857646565:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2662 on theBenchmark for (2662ds/1368Mi) % 281.56/40.01 % (238620)Instruction limit reached! % 281.56/40.01 % (238620)------------------------------ % 281.56/40.01 % (238620)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 281.56/40.01 % (238620)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 281.56/40.01 % (238620)CaDiCaL version: 2.1.3 % 281.56/40.01 % (238620)Termination reason: Instruction limit % 281.56/40.01 % (238620)Termination phase: Saturation % 281.56/40.01 % (238620)Time elapsed: 0.777 s % 281.56/40.01 % (238620)Peak memory usage: 22 MB % 281.56/40.01 % (238620)Instructions burned: 1368 (million) % 281.56/40.01 % (238622)ott-21_1_sil=16000:si=on:fs=off:random_seed=1260409004:i=360:av=off:fsr=off:rtra=on_2654 on theBenchmark for (2654ds/360Mi) % 281.56/40.01 % (238622)Instruction limit reached! % 281.56/40.01 % (238622)------------------------------ % 281.56/40.01 % (238622)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 281.56/40.01 % (238622)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 281.56/40.01 % (238622)CaDiCaL version: 2.1.3 % 281.56/40.01 % (238622)Termination reason: Instruction limit % 281.56/40.01 % (238622)Termination phase: Saturation % 281.56/40.01 % (238622)Time elapsed: 0.161 s % 281.56/40.01 % (238622)Peak memory usage: 13 MB % 281.56/40.02 % (238622)Instructions burned: 361 (million) % 281.56/40.02 % (238624)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1179401678:i=954:bd=all:rtra=on_2653 on theBenchmark for (2653ds/954Mi) % 281.56/40.02 % (238624)Instruction limit reached! % 281.56/40.02 % (238624)------------------------------ % 281.56/40.02 % (238624)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 281.56/40.02 % (238624)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 281.56/40.02 % (238624)CaDiCaL version: 2.1.3 % 281.56/40.02 % (238624)Termination reason: Instruction limit % 281.56/40.02 % (238624)Termination phase: Saturation % 281.56/40.02 % (238624)Time elapsed: 0.644 s % 281.56/40.02 % (238624)Peak memory usage: 16 MB % 281.56/40.02 % (238624)Instructions burned: 954 (million) % 281.56/40.02 % (238626)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=3311514425:fmbsr=1.3:i=1730:ins=25:rtra=on_2646 on theBenchmark for (2646ds/1730Mi) % 281.56/40.02 % (238626)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 281.56/40.02 % (238626)Terminated due to inappropriate strategy. % 281.56/40.02 % (238626)------------------------------ % 281.56/40.02 % (238626)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 281.56/40.02 % (238626)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 281.56/40.02 % (238626)CaDiCaL version: 2.1.3 % 281.56/40.02 % (238626)Termination reason: Inappropriate % 281.56/40.02 % (238626)Time elapsed: 0.001 s % 281.56/40.02 % (238626)Peak memory usage: 10 MB % 281.56/40.02 % (238626)Instructions burned: 2 (million) % 281.56/40.02 % (238626)------------------------------ % 281.56/40.02 % (238626)------------------------------ % 281.56/40.02 % (238628)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=2885898219:i=2358:rtra=on_2646 on theBenchmark for (2646ds/2358Mi) % 281.56/40.02 % (238628)Instruction limit reached! % 281.56/40.02 % (238628)------------------------------ % 281.56/40.02 % (238628)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 281.56/40.02 % (238628)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 281.56/40.02 % (238628)CaDiCaL version: 2.1.3 % 281.56/40.02 % (238628)Termination reason: Instruction limit % 281.56/40.02 % (238628)Termination phase: Saturation % 300.05/42.54 % (238628)Time elapsed: 1.290 s % 300.05/42.54 % (238628)Peak memory usage: 22 MB % 300.05/42.54 % (238628)Instructions burned: 2360 (million) % 300.05/42.54 % (238630)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=575188016:i=1778:ins=1:rtra=on_2632 on theBenchmark for (2632ds/1778Mi) % 300.05/42.54 % (238630)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 300.05/42.54 % (238630)Terminated due to inappropriate strategy. % 300.05/42.54 % (238630)------------------------------ % 300.05/42.54 % (238630)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.05/42.54 % (238630)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.05/42.54 % (238630)CaDiCaL version: 2.1.3 % 300.05/42.54 % (238630)Termination reason: Inappropriate % 300.05/42.54 % (238630)Time elapsed: 0.001 s % 300.05/42.54 % (238630)Peak memory usage: 11 MB % 300.05/42.54 % (238630)Instructions burned: 2 (million) % 300.05/42.54 % (238630)------------------------------ % 300.05/42.54 % (238630)------------------------------ % 300.05/42.54 % (238632)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=421802814:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2632 on theBenchmark for (2632ds/1384Mi) % 300.05/42.54 % (238632)Instruction limit reached! % 300.05/42.54 % (238632)------------------------------ % 300.05/42.54 % (238632)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.05/42.54 % (238632)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.05/42.54 % (238632)CaDiCaL version: 2.1.3 % 300.05/42.54 % (238632)Termination reason: Instruction limit % 300.05/42.54 % (238632)Termination phase: Saturation % 300.05/42.54 % (238632)Time elapsed: 0.829 s % 300.05/42.54 % (238632)Peak memory usage: 23 MB % 300.05/42.54 % (238632)Instructions burned: 1385 (million) % 300.05/42.54 % (238634)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=2927933591:i=1758:kws=inv_precedence:fsr=off:rtra=on_2624 on theBenchmark for (2624ds/1758Mi) % 300.05/42.54 % (238425)Instruction limit reached! % 300.05/42.54 % (238425)------------------------------ % 300.05/42.54 % (238425)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.05/42.54 % (238425)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.05/42.54 % (238425)CaDiCaL version: 2.1.3 % 300.05/42.54 % (238425)Termination reason: Instruction limit % 300.05/42.54 % (238425)Termination phase: Saturation % 300.05/42.54 % (238425)Time elapsed: 14.475 s % 300.05/42.54 % (238425)Peak memory usage: 257 MB % 300.05/42.54 % (238425)Instructions burned: 53296 (million) % 300.05/42.54 % (238636)fmb+10_1_sil=64000:si=on:random_seed=2406380619:i=44122:nm=2:rtra=on:gsp=on_2622 on theBenchmark for (2622ds/44122Mi) % 300.05/42.54 % (238636)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 300.05/42.54 % (238636)Terminated due to inappropriate strategy. % 300.05/42.54 % (238636)------------------------------ % 300.05/42.54 % (238636)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.05/42.54 % (238636)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.05/42.54 % (238636)CaDiCaL version: 2.1.3 % 300.05/42.54 % (238636)Termination reason: Inappropriate % 300.05/42.54 % (238636)Time elapsed: 0.001 s % 300.05/42.54 % (238636)Peak memory usage: 10 MB % 300.05/42.54 % (238636)Instructions burned: 2 (million) % 300.05/42.54 % (238636)------------------------------ % 300.05/42.54 % (238636)------------------------------ % 300.05/42.54 % (238638)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=2149144075:i=19030:nm=5:rtra=on_2622 on theBenchmark for (2622ds/19030Mi) % 300.05/42.54 % (238638)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 300.05/42.54 % (238638)Terminated due to inappropriate strategy. % 300.05/42.54 % (238638)------------------------------ % 300.05/42.54 % (238638)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.05/42.54 % (238638)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.05/42.54 % (238638)CaDiCaL version: 2.1.3 % 300.05/42.54 % (238638)Termination reason: Inappropriate % 300.05/42.54 % (238638)Time elapsed: 0.001 s % 300.05/42.54 % (238638)Peak memory usage: 10 MB % 300.05/42.54 % (238638)Instructions burned: 2 (million) % 300.05/42.54 % (238638)------------------------------ % 300.05/42.54 % (238638)------------------------------ % 300.05/42.54 % (238640)fmb+10_1_sil=64000:sas=cadical:si=on:fmbss=8:random_seed=3321956337:fmbsr=1.7:i=1840:rtra=on_26 % 300.05/42.54 Terminated % 300.05/42.54 % Vampire exiting %------------------------------------------------------------------------------