%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWW842_1 : TPTP v9.3.1. Released v7.0.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % Computer : n007.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:45:03 PM UTC 2026 % Result : Timeout 300.63s 42.64s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWW842_1 : TPTP v9.3.1. Released v7.0.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.07/0.19 % Computer : n007.cluster.edu % 0.07/0.19 % Model : x86_64 x86_64 % 0.07/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.07/0.19 % Memory : 8046.5625MB % 0.07/0.19 % OS : Linux 6.8.0-71-generic % 0.07/0.19 % CPULimit : 300 % 0.07/0.19 % WCLimit : 300 % 0.07/0.19 % DateTime : Mon Sep 28 14:30:33 UTC 2026 % 0.07/0.19 % CPUTime : % 0.07/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.07/0.23 Running first-order model finding % 0.07/0.23 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 3.07/0.76 % (2429971)Will run a generic schedule for satisfiability detection. % 3.07/0.76 % (2429976)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=72993067_2999 on theBenchmark for (2999ds/0Mi) % 3.07/0.76 % (2429977)% WARNING: option uhcvi not known. % 3.07/0.76 % (2429979)dis+10_1_sil=32000:sp=arity:random_seed=3949724328:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 3.07/0.76 % (2429977)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1039236907:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 3.07/0.76 % (2429978)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1395825364:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 3.07/0.76 % (2429981)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=109989945:i=131_2999 on theBenchmark for (2999ds/131Mi) % 3.07/0.76 % (2429980)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3883819810:i=116_2999 on theBenchmark for (2999ds/116Mi) % 3.07/0.76 % (2429982)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2143401903:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 3.07/0.76 % (2429976)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.07/0.76 % (2429976)Terminated due to inappropriate strategy. % 3.07/0.76 % (2429976)------------------------------ % 3.07/0.76 % (2429976)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.07/0.76 % (2429976)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.07/0.76 % (2429976)CaDiCaL version: 2.1.3 % 3.07/0.76 % (2429976)Termination reason: Inappropriate % 3.07/0.76 % (2429976)Time elapsed: 0.021 s % 3.07/0.76 % (2429976)Peak memory usage: 12 MB % 3.07/0.76 % (2429976)Instructions burned: 86 (million) % 3.07/0.76 % (2429976)------------------------------ % 3.07/0.76 % (2429976)------------------------------ % 3.07/0.76 % (2429990)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2543833505:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 3.07/0.76 % (2429990)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.07/0.76 % (2429990)Terminated due to inappropriate strategy. % 3.07/0.76 % (2429990)------------------------------ % 3.07/0.76 % (2429990)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.07/0.76 % (2429990)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.07/0.76 % (2429990)CaDiCaL version: 2.1.3 % 3.07/0.76 % (2429990)Termination reason: Inappropriate % 3.07/0.76 % (2429990)Time elapsed: 0.020 s % 3.07/0.76 % (2429990)Peak memory usage: 12 MB % 3.07/0.76 % (2429990)Instructions burned: 85 (million) % 3.07/0.76 % (2429990)------------------------------ % 3.07/0.76 % (2429990)------------------------------ % 3.07/0.76 % (2429979)Instruction limit reached! % 3.07/0.76 % (2429979)------------------------------ % 3.07/0.76 % (2429979)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.07/0.76 % (2429979)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.07/0.76 % (2429979)CaDiCaL version: 2.1.3 % 3.07/0.76 % (2429979)Termination reason: Instruction limit % 3.07/0.76 % (2429979)Termination phase: Saturation % 3.07/0.76 % (2429979)Time elapsed: 0.051 s % 3.07/0.76 % (2429979)Peak memory usage: 14 MB % 3.07/0.76 % (2429979)Instructions burned: 103 (million) % 3.07/0.76 % (2429980)Instruction limit reached! % 3.07/0.76 % (2429980)------------------------------ % 3.07/0.76 % (2429980)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.07/0.76 % (2429980)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.07/0.76 % (2429980)CaDiCaL version: 2.1.3 % 3.07/0.76 % (2429980)Termination reason: Instruction limit % 3.07/0.76 % (2429980)Termination phase: Saturation % 3.07/0.76 % (2429980)Time elapsed: 0.054 s % 3.07/0.76 % (2429980)Peak memory usage: 13 MB % 3.07/0.76 % (2429980)Instructions burned: 116 (million) % 3.07/0.76 % (2429992)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=4229103283:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi) % 3.07/0.76 % (2429981)Instruction limit reached! % 3.07/0.76 % (2429981)------------------------------ % 3.07/0.76 % (2429981)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.07/0.76 % (2429981)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.07/0.76 % (2429981)CaDiCaL version: 2.1.3 % 3.07/0.76 % (2429981)Termination reason: Instruction limit % 5.46/1.08 % (2429981)Termination phase: Saturation % 5.46/1.08 % (2429981)Time elapsed: 0.064 s % 5.46/1.08 % (2429981)Peak memory usage: 14 MB % 5.46/1.08 % (2429981)Instructions burned: 131 (million) % 5.46/1.08 % (2429993)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=4025771313:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi) % 5.46/1.08 % (2429994)ott-21_1_sil=16000:fs=off:random_seed=1323928298:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 5.46/1.08 % (2429996)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3963521386:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 5.46/1.08 % (2429982)Instruction limit reached! % 5.46/1.08 % (2429982)------------------------------ % 5.46/1.08 % (2429982)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.46/1.08 % (2429982)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.46/1.08 % (2429982)CaDiCaL version: 2.1.3 % 5.46/1.08 % (2429982)Termination reason: Instruction limit % 5.46/1.08 % (2429982)Termination phase: Saturation % 5.46/1.08 % (2429982)Time elapsed: 0.084 s % 5.46/1.08 % (2429982)Peak memory usage: 14 MB % 5.46/1.08 % (2429982)Instructions burned: 159 (million) % 5.46/1.08 % (2429992)Instruction limit reached! % 5.46/1.08 % (2429992)------------------------------ % 5.46/1.08 % (2429992)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.46/1.08 % (2429992)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.46/1.08 % (2429992)CaDiCaL version: 2.1.3 % 5.46/1.08 % (2429992)Termination reason: Instruction limit % 5.46/1.08 % (2429992)Termination phase: Saturation % 5.46/1.08 % (2429992)Time elapsed: 0.036 s % 5.46/1.08 % (2429992)Peak memory usage: 14 MB % 5.46/1.08 % (2429992)Instructions burned: 133 (million) % 5.46/1.08 % (2430000)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2078241287:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 5.46/1.08 % (2430001)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3033111732:i=1179_2998 on theBenchmark for (2998ds/1179Mi) % 5.46/1.08 % (2430000)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 5.46/1.08 % (2430000)Terminated due to inappropriate strategy. % 5.46/1.08 % (2430000)------------------------------ % 5.46/1.08 % (2430000)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.46/1.08 % (2430000)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.46/1.08 % (2430000)CaDiCaL version: 2.1.3 % 5.46/1.08 % (2430000)Termination reason: Inappropriate % 5.46/1.08 % (2430000)Time elapsed: 0.038 s % 5.46/1.08 % (2430000)Peak memory usage: 12 MB % 5.46/1.08 % (2430000)Instructions burned: 85 (million) % 5.46/1.08 % (2430000)------------------------------ % 5.46/1.08 % (2430000)------------------------------ % 5.46/1.08 % (2429994)Instruction limit reached! % 5.46/1.08 % (2429994)------------------------------ % 5.46/1.08 % (2429994)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.46/1.08 % (2429994)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.46/1.08 % (2429994)CaDiCaL version: 2.1.3 % 5.46/1.08 % (2429994)Termination reason: Instruction limit % 5.46/1.08 % (2429994)Termination phase: Saturation % 5.46/1.08 % (2429994)Time elapsed: 0.085 s % 5.46/1.08 % (2429994)Peak memory usage: 14 MB % 5.46/1.08 % (2429994)Instructions burned: 180 (million) % 5.46/1.08 % (2430004)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3719913796:i=889:ins=1_2997 on theBenchmark for (2997ds/889Mi) % 5.46/1.08 % (2430005)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=3213515908: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) % 5.46/1.08 % (2430004)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 5.46/1.08 % (2430004)Terminated due to inappropriate strategy. % 5.46/1.08 % (2430004)------------------------------ % 5.46/1.08 % (2430004)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.46/1.08 % (2430004)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.46/1.08 % (2430004)CaDiCaL version: 2.1.3 % 5.46/1.08 % (2430004)Termination reason: Inappropriate % 5.46/1.08 % (2430004)Time elapsed: 0.039 s % 5.46/1.08 % (2430004)Peak memory usage: 13 MB % 17.81/3.00 % (2430004)Instructions burned: 86 (million) % 17.81/3.00 % (2430004)------------------------------ % 17.81/3.00 % (2430004)------------------------------ % 17.81/3.00 % (2430008)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2141890899:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi) % 17.81/3.00 % (2429996)Instruction limit reached! % 17.81/3.00 % (2429996)------------------------------ % 17.81/3.00 % (2429996)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 17.81/3.00 % (2429996)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.81/3.00 % (2429996)CaDiCaL version: 2.1.3 % 17.81/3.00 % (2429996)Termination reason: Instruction limit % 17.81/3.00 % (2429996)Termination phase: Saturation % 17.81/3.00 % (2429996)Time elapsed: 0.295 s % 17.81/3.00 % (2429996)Peak memory usage: 16 MB % 17.81/3.00 % (2429996)Instructions burned: 478 (million) % 17.81/3.00 % (2430001)Instruction limit reached! % 17.81/3.00 % (2430001)------------------------------ % 17.81/3.00 % (2430001)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 17.81/3.00 % (2430001)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.81/3.00 % (2430001)CaDiCaL version: 2.1.3 % 17.81/3.00 % (2430001)Termination reason: Instruction limit % 17.81/3.00 % (2430001)Termination phase: Saturation % 17.81/3.00 % (2430001)Time elapsed: 0.280 s % 17.81/3.00 % (2430001)Peak memory usage: 18 MB % 17.81/3.00 % (2430001)Instructions burned: 1184 (million) % 17.81/3.00 % (2430011)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1018816851:i=9515:nm=5_2995 on theBenchmark for (2995ds/9515Mi) % 17.81/3.00 % (2430010)fmb+10_1_sil=64000:random_seed=1107423978:i=22061:nm=2:gsp=on_2995 on theBenchmark for (2995ds/22061Mi) % 17.81/3.00 % (2430011)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 17.81/3.00 % (2430011)Terminated due to inappropriate strategy. % 17.81/3.00 % (2430011)------------------------------ % 17.81/3.00 % (2430011)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 17.81/3.00 % (2430011)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.81/3.00 % (2430011)CaDiCaL version: 2.1.3 % 17.81/3.00 % (2430011)Termination reason: Inappropriate % 17.81/3.00 % (2430011)Time elapsed: 0.021 s % 17.81/3.00 % (2430011)Peak memory usage: 12 MB % 17.81/3.00 % (2430011)Instructions burned: 86 (million) % 17.81/3.00 % (2430011)------------------------------ % 17.81/3.00 % (2430011)------------------------------ % 17.81/3.00 % (2430014)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=562240987:fmbsr=1.7:i=920_2995 on theBenchmark for (2995ds/920Mi) % 17.81/3.00 % (2429993)Instruction limit reached! % 17.81/3.00 % (2429993)------------------------------ % 17.81/3.00 % (2429993)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 17.81/3.00 % (2429993)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.81/3.00 % (2429993)CaDiCaL version: 2.1.3 % 17.81/3.00 % (2429993)Termination reason: Instruction limit % 17.81/3.00 % (2429993)Termination phase: Saturation % 17.81/3.00 % (2429993)Time elapsed: 0.366 s % 17.81/3.00 % (2429993)Peak memory usage: 17 MB % 17.81/3.00 % (2429993)Instructions burned: 685 (million) % 17.81/3.00 % (2430010)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 17.81/3.00 % (2430010)Terminated due to inappropriate strategy. % 17.81/3.00 % (2430010)------------------------------ % 17.81/3.00 % (2430010)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 17.81/3.00 % (2430010)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.81/3.00 % (2430010)CaDiCaL version: 2.1.3 % 17.81/3.00 % (2430010)Termination reason: Inappropriate % 17.81/3.00 % (2430010)Time elapsed: 0.040 s % 17.81/3.00 % (2430010)Peak memory usage: 12 MB % 17.81/3.00 % (2430010)Instructions burned: 87 (million) % 17.81/3.00 % (2430010)------------------------------ % 17.81/3.00 % (2430010)------------------------------ % 17.81/3.00 % (2430014)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 17.81/3.00 % (2430014)Terminated due to inappropriate strategy. % 17.81/3.00 % (2430014)------------------------------ % 17.81/3.00 % (2430014)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 17.81/3.00 % (2430014)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.81/3.00 % (2430014)CaDiCaL version: 2.1.3 % 17.81/3.00 % (2430014)Termination reason: Inappropriate % 17.81/3.00 % (2430014)Time elapsed: 0.021 s % 17.81/3.00 % (2430014)Peak memory usage: 12 MB % 19.60/3.52 % (2430014)Instructions burned: 86 (million) % 19.60/3.52 % (2430014)------------------------------ % 19.60/3.52 % (2430014)------------------------------ % 19.60/3.52 % (2430016)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=4204542884:i=5131_2994 on theBenchmark for (2994ds/5131Mi) % 19.60/3.52 % (2430017)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1718927631:i=1472:ins=7:fdi=8:gsp=on_2994 on theBenchmark for (2994ds/1472Mi) % 19.60/3.52 % (2430018)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=1682423794:i=6324_2994 on theBenchmark for (2994ds/6324Mi) % 19.60/3.52 % (2430018)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 19.60/3.52 % (2430018)Terminated due to inappropriate strategy. % 19.60/3.52 % (2430018)------------------------------ % 19.60/3.52 % (2430018)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 19.60/3.52 % (2430018)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.60/3.52 % (2430018)CaDiCaL version: 2.1.3 % 19.60/3.52 % (2430018)Termination reason: Inappropriate % 19.60/3.52 % (2430018)Time elapsed: 0.021 s % 19.60/3.52 % (2430018)Peak memory usage: 12 MB % 19.60/3.52 % (2430018)Instructions burned: 86 (million) % 19.60/3.52 % (2430018)------------------------------ % 19.60/3.52 % (2430018)------------------------------ % 19.60/3.52 % (2430022)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=2041750535:fmbsr=2.30978:i=2174_2994 on theBenchmark for (2994ds/2174Mi) % 19.60/3.52 % (2430022)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 19.60/3.52 % (2430022)Terminated due to inappropriate strategy. % 19.60/3.52 % (2430022)------------------------------ % 19.60/3.52 % (2430022)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 19.60/3.52 % (2430022)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.60/3.52 % (2430022)CaDiCaL version: 2.1.3 % 19.60/3.52 % (2430022)Termination reason: Inappropriate % 19.60/3.52 % (2430022)Time elapsed: 0.021 s % 19.60/3.52 % (2430022)Peak memory usage: 12 MB % 19.60/3.52 % (2430022)Instructions burned: 86 (million) % 19.60/3.52 % (2430022)------------------------------ % 19.60/3.52 % (2430022)------------------------------ % 19.60/3.52 % (2430024)ott-2_1_sil=16000:newcnf=on:random_seed=377278180:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2994 on theBenchmark for (2994ds/869Mi) % 19.60/3.52 % (2430005)Instruction limit reached! % 19.60/3.52 % (2430005)------------------------------ % 19.60/3.52 % (2430005)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 19.60/3.52 % (2430005)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.60/3.52 % (2430005)CaDiCaL version: 2.1.3 % 19.60/3.52 % (2430005)Termination reason: Instruction limit % 19.60/3.52 % (2430005)Termination phase: Saturation % 19.60/3.52 % (2430005)Time elapsed: 0.414 s % 19.60/3.52 % (2430005)Peak memory usage: 21 MB % 19.60/3.52 % (2430005)Instructions burned: 693 (million) % 19.60/3.52 % (2430026)ott+10_1_sil=32000:tgt=ground:random_seed=374025120:i=5114:av=off_2993 on theBenchmark for (2993ds/5114Mi) % 19.60/3.52 % (2430008)Instruction limit reached! % 19.60/3.52 % (2430008)------------------------------ % 19.60/3.52 % (2430008)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 19.60/3.52 % (2430008)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.60/3.52 % (2430008)CaDiCaL version: 2.1.3 % 19.60/3.52 % (2430008)Termination reason: Instruction limit % 19.60/3.52 % (2430008)Termination phase: Saturation % 19.60/3.52 % (2430008)Time elapsed: 0.492 s % 19.60/3.52 % (2430008)Peak memory usage: 19 MB % 19.60/3.52 % (2430008)Instructions burned: 880 (million) % 19.60/3.52 % (2430028)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=4254655181:i=54282_2992 on theBenchmark for (2992ds/54282Mi) % 19.60/3.52 % (2430024)Instruction limit reached! % 19.60/3.52 % (2430024)------------------------------ % 19.60/3.52 % (2430024)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 19.60/3.52 % (2430024)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.60/3.52 % (2430024)CaDiCaL version: 2.1.3 % 19.60/3.52 % (2430024)Termination reason: Instruction limit % 19.60/3.52 % (2430024)Termination phase: Saturation % 19.60/3.52 % (2430024)Time elapsed: 0.231 s % 19.60/3.52 % (2430024)Peak memory usage: 17 MB % 19.60/3.52 % (2430024)Instructions burned: 871 (million) % 19.60/3.52 % (2430030)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=139322665:i=3512:aac=none_2991 on theBenchmark for (2991ds/3512Mi) % 91.40/13.18 % (2430028)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 91.40/13.18 % (2430028)Terminated due to inappropriate strategy. % 91.40/13.18 % (2430028)------------------------------ % 91.40/13.18 % (2430028)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 91.40/13.18 % (2430028)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 91.40/13.18 % (2430028)CaDiCaL version: 2.1.3 % 91.40/13.18 % (2430028)Termination reason: Inappropriate % 91.40/13.18 % (2430028)Time elapsed: 0.040 s % 91.40/13.18 % (2430028)Peak memory usage: 13 MB % 91.40/13.18 % (2430028)Instructions burned: 87 (million) % 91.40/13.18 % (2430028)------------------------------ % 91.40/13.18 % (2430028)------------------------------ % 91.40/13.18 % (2430032)dis+21_1_sil=32000:sas=cadical:random_seed=756155423:i=3773:amm=off_2991 on theBenchmark for (2991ds/3773Mi) % 91.40/13.18 % (2430017)Instruction limit reached! % 91.40/13.18 % (2430017)------------------------------ % 91.40/13.18 % (2430017)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 91.40/13.18 % (2430017)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 91.40/13.18 % (2430017)CaDiCaL version: 2.1.3 % 91.40/13.18 % (2430017)Termination reason: Instruction limit % 91.40/13.18 % (2430017)Termination phase: Saturation % 91.40/13.18 % (2430017)Time elapsed: 0.720 s % 91.40/13.18 % (2430017)Peak memory usage: 27 MB % 91.40/13.18 % (2430017)Instructions burned: 1473 (million) % 91.40/13.18 % (2430034)ott+11_1_sil=16000:gs=on:random_seed=3548875849:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2987 on theBenchmark for (2987ds/2251Mi) % 91.40/13.18 % (2430030)Instruction limit reached! % 91.40/13.18 % (2430030)------------------------------ % 91.40/13.18 % (2430030)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 91.40/13.18 % (2430030)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 91.40/13.18 % (2430030)CaDiCaL version: 2.1.3 % 91.40/13.18 % (2430030)Termination reason: Instruction limit % 91.40/13.18 % (2430030)Termination phase: Saturation % 91.40/13.18 % (2430030)Time elapsed: 1.010 s % 91.40/13.18 % (2430030)Peak memory usage: 36 MB % 91.40/13.18 % (2430030)Instructions burned: 3513 (million) % 91.40/13.18 % (2430036)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=1010111626:fmbsr=1.6:i=67534_2981 on theBenchmark for (2981ds/67534Mi) % 91.40/13.18 % (2430036)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 91.40/13.18 % (2430036)Terminated due to inappropriate strategy. % 91.40/13.18 % (2430036)------------------------------ % 91.40/13.18 % (2430036)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 91.40/13.18 % (2430036)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 91.40/13.18 % (2430036)CaDiCaL version: 2.1.3 % 91.40/13.18 % (2430036)Termination reason: Inappropriate % 91.40/13.18 % (2430036)Time elapsed: 0.021 s % 91.40/13.18 % (2430036)Peak memory usage: 12 MB % 91.40/13.18 % (2430036)Instructions burned: 86 (million) % 91.40/13.18 % (2430036)------------------------------ % 91.40/13.18 % (2430036)------------------------------ % 91.40/13.18 % (2430038)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=1787137725:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2981 on theBenchmark for (2981ds/4591Mi) % 91.40/13.18 % (2430034)Instruction limit reached! % 91.40/13.18 % (2430034)------------------------------ % 91.40/13.18 % (2430034)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 91.40/13.18 % (2430034)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 91.40/13.18 % (2430034)CaDiCaL version: 2.1.3 % 91.40/13.18 % (2430034)Termination reason: Instruction limit % 91.40/13.18 % (2430034)Termination phase: Saturation % 91.40/13.18 % (2430034)Time elapsed: 1.235 s % 91.40/13.18 % (2430034)Peak memory usage: 29 MB % 91.40/13.18 % (2430034)Instructions burned: 2252 (million) % 91.40/13.18 % (2430040)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=3650697975:i=29340_2974 on theBenchmark for (2974ds/29340Mi) % 91.40/13.18 % (2430032)Instruction limit reached! % 91.40/13.18 % (2430032)------------------------------ % 91.40/13.18 % (2430032)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 91.40/13.18 % (2430032)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 91.40/13.18 % (2430032)CaDiCaL version: 2.1.3 % 91.40/13.18 % (2430032)Termination reason: Instruction limit % 107.43/15.47 % (2430032)Termination phase: Saturation % 107.43/15.47 % (2430032)Time elapsed: 1.897 s % 107.43/15.47 % (2430032)Peak memory usage: 21 MB % 107.43/15.47 % (2430032)Instructions burned: 3774 (million) % 107.43/15.47 % (2430042)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=2745413193:i=5211_2972 on theBenchmark for (2972ds/5211Mi) % 107.43/15.47 % (2430038)Instruction limit reached! % 107.43/15.47 % (2430038)------------------------------ % 107.43/15.47 % (2430038)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 107.43/15.47 % (2430038)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 107.43/15.47 % (2430038)CaDiCaL version: 2.1.3 % 107.43/15.47 % (2430038)Termination reason: Instruction limit % 107.43/15.47 % (2430038)Termination phase: Saturation % 107.43/15.47 % (2430038)Time elapsed: 1.115 s % 107.43/15.47 % (2430038)Peak memory usage: 40 MB % 107.43/15.47 % (2430038)Instructions burned: 4596 (million) % 107.43/15.47 % (2430044)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=811078699:i=5497:nm=2_2969 on theBenchmark for (2969ds/5497Mi) % 107.43/15.47 % (2430044)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 107.43/15.47 % (2430044)Terminated due to inappropriate strategy. % 107.43/15.47 % (2430044)------------------------------ % 107.43/15.47 % (2430044)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 107.43/15.47 % (2430044)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 107.43/15.47 % (2430044)CaDiCaL version: 2.1.3 % 107.43/15.47 % (2430044)Termination reason: Inappropriate % 107.43/15.47 % (2430044)Time elapsed: 0.036 s % 107.43/15.47 % (2430044)Peak memory usage: 13 MB % 107.43/15.47 % (2430044)Instructions burned: 86 (million) % 107.43/15.47 % (2430044)------------------------------ % 107.43/15.47 % (2430044)------------------------------ % 107.43/15.47 % (2430046)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=3548798664:fmbsr=2:i=46332_2969 on theBenchmark for (2969ds/46332Mi) % 107.43/15.47 % (2430046)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 107.43/15.47 % (2430046)Terminated due to inappropriate strategy. % 107.43/15.47 % (2430046)------------------------------ % 107.43/15.47 % (2430046)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 107.43/15.47 % (2430046)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 107.43/15.47 % (2430046)CaDiCaL version: 2.1.3 % 107.43/15.47 % (2430046)Termination reason: Inappropriate % 107.43/15.47 % (2430046)Time elapsed: 0.021 s % 107.43/15.47 % (2430046)Peak memory usage: 12 MB % 107.43/15.47 % (2430046)Instructions burned: 86 (million) % 107.43/15.47 % (2430046)------------------------------ % 107.43/15.47 % (2430046)------------------------------ % 107.43/15.47 % (2430048)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=1752481450:i=14071_2968 on theBenchmark for (2968ds/14071Mi) % 107.43/15.47 % (2430048)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 107.43/15.47 % (2430048)Terminated due to inappropriate strategy. % 107.43/15.47 % (2430048)------------------------------ % 107.43/15.47 % (2430048)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 107.43/15.47 % (2430048)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 107.43/15.47 % (2430048)CaDiCaL version: 2.1.3 % 107.43/15.47 % (2430048)Termination reason: Inappropriate % 107.43/15.47 % (2430048)Time elapsed: 0.021 s % 107.43/15.47 % (2430048)Peak memory usage: 12 MB % 107.43/15.47 % (2430048)Instructions burned: 86 (million) % 107.43/15.47 % (2430048)------------------------------ % 107.43/15.47 % (2430048)------------------------------ % 107.43/15.47 % (2430050)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3083098159:i=22565:add=on:rawr=on_2968 on theBenchmark for (2968ds/22565Mi) % 107.43/15.47 % (2430016)Instruction limit reached! % 107.43/15.47 % (2430016)------------------------------ % 107.43/15.47 % (2430016)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 107.43/15.47 % (2430016)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 107.43/15.47 % (2430016)CaDiCaL version: 2.1.3 % 107.43/15.47 % (2430016)Termination reason: Instruction limit % 107.43/15.47 % (2430016)Termination phase: Saturation % 107.43/15.47 % (2430016)Time elapsed: 2.737 s % 107.43/15.47 % (2430016)Peak memory usage: 48 MB % 107.43/15.47 % (2430016)Instructions burned: 5133 (million) % 107.43/15.47 % (2430052)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=1158095486:i=8173:av=off_2967 on theBenchmark for (2967ds/8173Mi) % 109.20/15.73 % (2430026)Instruction limit reached! % 109.20/15.73 % (2430026)------------------------------ % 109.20/15.73 % (2430026)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 109.20/15.73 % (2430026)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 109.20/15.73 % (2430026)CaDiCaL version: 2.1.3 % 109.20/15.73 % (2430026)Termination reason: Instruction limit % 109.20/15.73 % (2430026)Termination phase: Saturation % 109.20/15.73 % (2430026)Time elapsed: 2.997 s % 109.20/15.73 % (2430026)Peak memory usage: 55 MB % 109.20/15.73 % (2430026)Instructions burned: 5114 (million) % 109.20/15.73 % (2430054)dis+10_16:1_sil=16000:random_seed=75911167:i=9155:fsr=off_2963 on theBenchmark for (2963ds/9155Mi) % 109.20/15.73 % (2430042)Instruction limit reached! % 109.20/15.73 % (2430042)------------------------------ % 109.20/15.73 % (2430042)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 109.20/15.73 % (2430042)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 109.20/15.73 % (2430042)CaDiCaL version: 2.1.3 % 109.20/15.73 % (2430042)Termination reason: Instruction limit % 109.20/15.73 % (2430042)Termination phase: Saturation % 109.20/15.73 % (2430042)Time elapsed: 2.696 s % 109.20/15.73 % (2430042)Peak memory usage: 33 MB % 109.20/15.73 % (2430042)Instructions burned: 5212 (million) % 109.20/15.73 % (2430056)ott-3_8_sil=64000:random_seed=785255058:i=20139:bs=on_2945 on theBenchmark for (2945ds/20139Mi) % 109.20/15.73 % (2430052)Instruction limit reached! % 109.20/15.73 % (2430052)------------------------------ % 109.20/15.73 % (2430052)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 109.20/15.73 % (2430052)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 109.20/15.73 % (2430052)CaDiCaL version: 2.1.3 % 109.20/15.73 % (2430052)Termination reason: Instruction limit % 109.20/15.73 % (2430052)Termination phase: Saturation % 109.20/15.73 % (2430052)Time elapsed: 4.822 s % 109.20/15.73 % (2430052)Peak memory usage: 85 MB % 109.20/15.73 % (2430052)Instructions burned: 8174 (million) % 109.20/15.73 % (2430059)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=1931880444:fmbsr=2:i=32576_2918 on theBenchmark for (2918ds/32576Mi) % 109.20/15.73 % (2430059)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 109.20/15.73 % (2430059)Terminated due to inappropriate strategy. % 109.20/15.73 % (2430059)------------------------------ % 109.20/15.73 % (2430059)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 109.20/15.73 % (2430059)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 109.20/15.73 % (2430059)CaDiCaL version: 2.1.3 % 109.20/15.73 % (2430059)Termination reason: Inappropriate % 109.20/15.73 % (2430059)Time elapsed: 0.040 s % 109.20/15.73 % (2430059)Peak memory usage: 12 MB % 109.20/15.73 % (2430059)Instructions burned: 86 (million) % 109.20/15.73 % (2430059)------------------------------ % 109.20/15.73 % (2430059)------------------------------ % 109.20/15.73 % (2430061)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=3253091572:i=11404_2918 on theBenchmark for (2918ds/11404Mi) % 109.20/15.73 % (2430050)Instruction limit reached! % 109.20/15.73 % (2430050)------------------------------ % 109.20/15.73 % (2430050)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 109.20/15.73 % (2430050)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 109.20/15.73 % (2430050)CaDiCaL version: 2.1.3 % 109.20/15.73 % (2430050)Termination reason: Instruction limit % 109.20/15.73 % (2430050)Termination phase: Saturation % 109.20/15.73 % (2430050)Time elapsed: 5.194 s % 109.20/15.73 % (2430050)Peak memory usage: 83 MB % 109.20/15.73 % (2430050)Instructions burned: 22565 (million) % 109.20/15.73 % (2430063)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=737814048:i=14134_2916 on theBenchmark for (2916ds/14134Mi) % 109.20/15.73 % (2430054)Instruction limit reached! % 109.20/15.73 % (2430054)------------------------------ % 109.20/15.73 % (2430054)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 109.20/15.73 % (2430054)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 109.20/15.73 % (2430054)CaDiCaL version: 2.1.3 % 109.20/15.73 % (2430054)Termination reason: Instruction limit % 109.20/15.73 % (2430054)Termination phase: Saturation % 109.20/15.73 % (2430054)Time elapsed: 4.792 s % 109.20/15.73 % (2430054)Peak memory usage: 61 MB % 109.20/15.73 % (2430054)Instructions burned: 9157 (million) % 109.20/15.73 % (2430065)dis+33_16_sil=32000:sac=on:random_seed=2178693409:i=15851:nm=0_2914 on theBenchmark for (2914ds/15851Mi) % 109.20/15.73 % (2430063)Instruction limit reached! % 109.20/15.73 % (2430063)------------------------------ % 109.20/15.73 % (2430063)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 128.02/18.34 % (2430063)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 128.02/18.34 % (2430063)CaDiCaL version: 2.1.3 % 128.02/18.34 % (2430063)Termination reason: Instruction limit % 128.02/18.34 % (2430063)Termination phase: Saturation % 128.02/18.34 % (2430063)Time elapsed: 4.581 s % 128.02/18.34 % (2430063)Peak memory usage: 101 MB % 128.02/18.34 % (2430063)Instructions burned: 14135 (million) % 128.02/18.34 % (2430067)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=2126793900:avsq=on:i=17627:add=on:amm=off_2870 on theBenchmark for (2870ds/17627Mi) % 128.02/18.34 % (2430056)Instruction limit reached! % 128.02/18.34 % (2430056)------------------------------ % 128.02/18.34 % (2430056)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 128.02/18.34 % (2430056)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 128.02/18.34 % (2430056)CaDiCaL version: 2.1.3 % 128.02/18.34 % (2430056)Termination reason: Instruction limit % 128.02/18.34 % (2430056)Termination phase: Saturation % 128.02/18.34 % (2430056)Time elapsed: 9.154 s % 128.02/18.34 % (2430056)Peak memory usage: 79 MB % 128.02/18.34 % (2430056)Instructions burned: 20141 (million) % 128.02/18.34 % (2430069)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=783497956:s2a=on:i=53295_2853 on theBenchmark for (2853ds/53295Mi) % 128.02/18.34 % (2430061)Instruction limit reached! % 128.02/18.34 % (2430061)------------------------------ % 128.02/18.34 % (2430061)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 128.02/18.34 % (2430061)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 128.02/18.34 % (2430061)CaDiCaL version: 2.1.3 % 128.02/18.34 % (2430061)Termination reason: Instruction limit % 128.02/18.34 % (2430061)Termination phase: Saturation % 128.02/18.34 % (2430061)Time elapsed: 6.874 s % 128.02/18.34 % (2430061)Peak memory usage: 98 MB % 128.02/18.34 % (2430061)Instructions burned: 11405 (million) % 128.02/18.34 % (2430071)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=2923434731:i=26857:ins=20_2849 on theBenchmark for (2849ds/26857Mi) % 128.02/18.34 % (2430065)Instruction limit reached! % 128.02/18.34 % (2430065)------------------------------ % 128.02/18.34 % (2430065)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 128.02/18.34 % (2430065)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 128.02/18.34 % (2430065)CaDiCaL version: 2.1.3 % 128.02/18.34 % (2430065)Termination reason: Instruction limit % 128.02/18.34 % (2430065)Termination phase: Saturation % 128.02/18.34 % (2430065)Time elapsed: 6.586 s % 128.02/18.34 % (2430065)Peak memory usage: 19 MB % 128.02/18.34 % (2430065)Instructions burned: 15851 (million) % 128.02/18.34 % (2430073)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=3098827115:i=28120:bs=on:fsr=off_2848 on theBenchmark for (2848ds/28120Mi) % 128.02/18.34 % (2430071)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 128.02/18.34 % (2430071)Terminated due to inappropriate strategy. % 128.02/18.34 % (2430071)------------------------------ % 128.02/18.34 % (2430071)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 128.02/18.34 % (2430071)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 128.02/18.34 % (2430071)CaDiCaL version: 2.1.3 % 128.02/18.34 % (2430071)Termination reason: Inappropriate % 128.02/18.34 % (2430071)Time elapsed: 0.040 s % 128.02/18.34 % (2430071)Peak memory usage: 12 MB % 128.02/18.34 % (2430071)Instructions burned: 86 (million) % 128.02/18.34 % (2430071)------------------------------ % 128.02/18.34 % (2430071)------------------------------ % 128.02/18.34 % (2430075)fmb+10_1_sil=256000:fmbss=7:random_seed=4026697572:fmbsr=1.6:i=182295_2848 on theBenchmark for (2848ds/182295Mi) % 128.02/18.34 % (2430075)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 128.02/18.34 % (2430075)Terminated due to inappropriate strategy. % 128.02/18.34 % (2430075)------------------------------ % 128.02/18.34 % (2430075)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 128.02/18.34 % (2430075)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 128.02/18.34 % (2430075)CaDiCaL version: 2.1.3 % 128.02/18.34 % (2430075)Termination reason: Inappropriate % 128.02/18.34 % (2430075)Time elapsed: 0.040 s % 128.02/18.34 % (2430075)Peak memory usage: 12 MB % 128.02/18.34 % (2430075)Instructions burned: 86 (million) % 128.02/18.34 % (2430075)------------------------------ % 128.02/18.34 % (2430075)------------------------------ % 128.02/18.34 % (2430077)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=994004938:i=44625:gsp=on_2847 on theBenchmark for (2847ds/44625Mi) % 135.19/19.33 % (2430077)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 135.19/19.33 % (2430077)Terminated due to inappropriate strategy. % 135.19/19.33 % (2430077)------------------------------ % 135.19/19.33 % (2430077)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 135.19/19.33 % (2430077)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 135.19/19.33 % (2430077)CaDiCaL version: 2.1.3 % 135.19/19.33 % (2430077)Termination reason: Inappropriate % 135.19/19.33 % (2430077)Time elapsed: 0.041 s % 135.19/19.33 % (2430077)Peak memory usage: 12 MB % 135.19/19.33 % (2430077)Instructions burned: 90 (million) % 135.19/19.33 % (2430077)------------------------------ % 135.19/19.33 % (2430077)------------------------------ % 135.19/19.33 % (2430079)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=1160416431:i=160505_2847 on theBenchmark for (2847ds/160505Mi) % 135.19/19.33 % (2430079)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 135.19/19.33 % (2430079)Terminated due to inappropriate strategy. % 135.19/19.33 % (2430079)------------------------------ % 135.19/19.33 % (2430079)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 135.19/19.33 % (2430079)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 135.19/19.33 % (2430079)CaDiCaL version: 2.1.3 % 135.19/19.33 % (2430079)Termination reason: Inappropriate % 135.19/19.33 % (2430079)Time elapsed: 0.040 s % 135.19/19.33 % (2430079)Peak memory usage: 12 MB % 135.19/19.33 % (2430079)Instructions burned: 86 (million) % 135.19/19.33 % (2430079)------------------------------ % 135.19/19.33 % (2430079)------------------------------ % 135.19/19.33 % (2430081)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=1862278563:fmbsr=1.3:i=225729_2846 on theBenchmark for (2846ds/225729Mi) % 135.19/19.33 % (2430081)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 135.19/19.33 % (2430081)Terminated due to inappropriate strategy. % 135.19/19.33 % (2430081)------------------------------ % 135.19/19.33 % (2430081)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 135.19/19.33 % (2430081)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 135.19/19.33 % (2430081)CaDiCaL version: 2.1.3 % 135.19/19.33 % (2430081)Termination reason: Inappropriate % 135.19/19.33 % (2430081)Time elapsed: 0.040 s % 135.19/19.33 % (2430081)Peak memory usage: 12 MB % 135.19/19.33 % (2430081)Instructions burned: 86 (million) % 135.19/19.33 % (2430081)------------------------------ % 135.19/19.33 % (2430081)------------------------------ % 135.19/19.33 % (2430083)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=3848047645:fmbsr=2:i=185024:ins=7_2845 on theBenchmark for (2845ds/185024Mi) % 135.19/19.33 % (2430040)Instruction limit reached! % 135.19/19.33 % (2430040)------------------------------ % 135.19/19.33 % (2430040)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 135.19/19.33 % (2430040)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 135.19/19.33 % (2430040)CaDiCaL version: 2.1.3 % 135.19/19.33 % (2430040)Termination reason: Instruction limit % 135.19/19.33 % (2430040)Termination phase: Saturation % 135.19/19.33 % (2430040)Time elapsed: 12.894 s % 135.19/19.33 % (2430040)Peak memory usage: 51 MB % 135.19/19.33 % (2430040)Instructions burned: 29341 (million) % 135.19/19.33 % (2430085)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=1041878698:rtra=on_2845 on theBenchmark for (2845ds/0Mi) % 135.19/19.33 % (2430083)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 135.19/19.33 % (2430083)Terminated due to inappropriate strategy. % 135.19/19.33 % (2430083)------------------------------ % 135.19/19.33 % (2430083)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 135.19/19.33 % (2430083)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 135.19/19.33 % (2430083)CaDiCaL version: 2.1.3 % 135.19/19.33 % (2430083)Termination reason: Inappropriate % 135.19/19.33 % (2430083)Time elapsed: 0.040 s % 135.19/19.33 % (2430083)Peak memory usage: 12 MB % 135.19/19.33 % (2430083)Instructions burned: 86 (million) % 135.19/19.33 % (2430083)------------------------------ % 135.19/19.33 % (2430083)------------------------------ % 135.19/19.33 % (2430087)% WARNING: option uhcvi not known. % 135.19/19.33 % (2430087)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3934215393:i=271062:add=off:rtra=on:rawr=on_2845 on theBenchmark for (2845ds/271062Mi) % 135.19/19.33 % (2430085)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 148.66/21.23 % (2430085)Terminated due to inappropriate strategy. % 148.66/21.23 % (2430085)------------------------------ % 148.66/21.23 % (2430085)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 148.66/21.23 % (2430085)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 148.66/21.23 % (2430085)CaDiCaL version: 2.1.3 % 148.66/21.23 % (2430085)Termination reason: Inappropriate % 148.66/21.23 % (2430085)Time elapsed: 0.046 s % 148.66/21.23 % (2430085)Peak memory usage: 13 MB % 148.66/21.23 % (2430085)Instructions burned: 94 (million) % 148.66/21.23 % (2430085)------------------------------ % 148.66/21.23 % (2430085)------------------------------ % 148.66/21.23 % (2430089)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2715001715:i=176048:add=on:rtra=on:rawr=on_2845 on theBenchmark for (2845ds/176048Mi) % 148.66/21.23 % (2430067)Instruction limit reached! % 148.66/21.23 % (2430067)------------------------------ % 148.66/21.23 % (2430067)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 148.66/21.23 % (2430067)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 148.66/21.23 % (2430067)CaDiCaL version: 2.1.3 % 148.66/21.23 % (2430067)Termination reason: Instruction limit % 148.66/21.23 % (2430067)Termination phase: Saturation % 148.66/21.23 % (2430067)Time elapsed: 4.751 s % 148.66/21.23 % (2430067)Peak memory usage: 197 MB % 148.66/21.23 % (2430067)Instructions burned: 17632 (million) % 148.66/21.23 % (2430091)dis+10_1_sil=32000:si=on:sp=arity:random_seed=2061656041:i=206:fgj=on:rtra=on_2822 on theBenchmark for (2822ds/206Mi) % 148.66/21.23 % (2430091)Instruction limit reached! % 148.66/21.23 % (2430091)------------------------------ % 148.66/21.23 % (2430091)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 148.66/21.23 % (2430091)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 148.66/21.23 % (2430091)CaDiCaL version: 2.1.3 % 148.66/21.23 % (2430091)Termination reason: Instruction limit % 148.66/21.23 % (2430091)Termination phase: Saturation % 148.66/21.23 % (2430091)Time elapsed: 0.061 s % 148.66/21.23 % (2430091)Peak memory usage: 15 MB % 148.66/21.23 % (2430091)Instructions burned: 207 (million) % 148.66/21.23 % (2430093)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=3044192130:i=232:rtra=on_2821 on theBenchmark for (2821ds/232Mi) % 148.66/21.23 % (2430093)Instruction limit reached! % 148.66/21.23 % (2430093)------------------------------ % 148.66/21.23 % (2430093)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 148.66/21.23 % (2430093)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 148.66/21.23 % (2430093)CaDiCaL version: 2.1.3 % 148.66/21.23 % (2430093)Termination reason: Instruction limit % 148.66/21.23 % (2430093)Termination phase: Saturation % 148.66/21.23 % (2430093)Time elapsed: 0.070 s % 148.66/21.23 % (2430093)Peak memory usage: 15 MB % 148.66/21.23 % (2430093)Instructions burned: 232 (million) % 148.66/21.23 % (2430095)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=2062955083:i=262:rtra=on_2821 on theBenchmark for (2821ds/262Mi) % 148.66/21.23 % (2430095)Instruction limit reached! % 148.66/21.23 % (2430095)------------------------------ % 148.66/21.23 % (2430095)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 148.66/21.23 % (2430095)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 148.66/21.23 % (2430095)CaDiCaL version: 2.1.3 % 148.66/21.23 % (2430095)Termination reason: Instruction limit % 148.66/21.23 % (2430095)Termination phase: Saturation % 148.66/21.23 % (2430095)Time elapsed: 0.081 s % 148.66/21.23 % (2430095)Peak memory usage: 16 MB % 148.66/21.23 % (2430095)Instructions burned: 264 (million) % 148.66/21.23 % (2430097)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=1094385753:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2820 on theBenchmark for (2820ds/318Mi) % 148.66/21.23 % (2430097)Instruction limit reached! % 148.66/21.23 % (2430097)------------------------------ % 148.66/21.23 % (2430097)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 148.66/21.23 % (2430097)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 148.66/21.23 % (2430097)CaDiCaL version: 2.1.3 % 148.66/21.23 % (2430097)Termination reason: Instruction limit % 148.66/21.23 % (2430097)Termination phase: Saturation % 148.66/21.23 % (2430097)Time elapsed: 0.100 s % 148.66/21.23 % (2430097)Peak memory usage: 16 MB % 148.66/21.23 % (2430097)Instructions burned: 318 (million) % 148.66/21.23 % (2430099)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=3041616376:i=1428:nm=2:rtra=on_2819 on theBenchmark for (2819ds/1428Mi) % 178.49/25.46 % (2430099)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 178.49/25.46 % (2430099)Terminated due to inappropriate strategy. % 178.49/25.46 % (2430099)------------------------------ % 178.49/25.46 % (2430099)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 178.49/25.46 % (2430099)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 178.49/25.46 % (2430099)CaDiCaL version: 2.1.3 % 178.49/25.46 % (2430099)Termination reason: Inappropriate % 178.49/25.46 % (2430099)Time elapsed: 0.024 s % 178.49/25.46 % (2430099)Peak memory usage: 13 MB % 178.49/25.46 % (2430099)Instructions burned: 93 (million) % 178.49/25.46 % (2430099)------------------------------ % 178.49/25.46 % (2430099)------------------------------ % 178.49/25.46 % (2430101)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=3154806519:i=262:bd=preordered:rtra=on:fsd=on_2818 on theBenchmark for (2818ds/262Mi) % 178.49/25.46 % (2430101)Instruction limit reached! % 178.49/25.46 % (2430101)------------------------------ % 178.49/25.46 % (2430101)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 178.49/25.46 % (2430101)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 178.49/25.46 % (2430101)CaDiCaL version: 2.1.3 % 178.49/25.46 % (2430101)Termination reason: Instruction limit % 178.49/25.46 % (2430101)Termination phase: Saturation % 178.49/25.46 % (2430101)Time elapsed: 0.087 s % 178.49/25.46 % (2430101)Peak memory usage: 16 MB % 178.49/25.46 % (2430101)Instructions burned: 262 (million) % 178.49/25.46 % (2430103)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=2143244089:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2817 on theBenchmark for (2817ds/1368Mi) % 178.49/25.46 % (2430103)Instruction limit reached! % 178.49/25.46 % (2430103)------------------------------ % 178.49/25.46 % (2430103)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 178.49/25.46 % (2430103)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 178.49/25.46 % (2430103)CaDiCaL version: 2.1.3 % 178.49/25.46 % (2430103)Termination reason: Instruction limit % 178.49/25.46 % (2430103)Termination phase: Saturation % 178.49/25.46 % (2430103)Time elapsed: 0.380 s % 178.49/25.46 % (2430103)Peak memory usage: 21 MB % 178.49/25.46 % (2430103)Instructions burned: 1368 (million) % 178.49/25.46 % (2430105)ott-21_1_sil=16000:si=on:fs=off:random_seed=2039628706:i=360:av=off:fsr=off:rtra=on_2813 on theBenchmark for (2813ds/360Mi) % 178.49/25.46 % (2430105)Instruction limit reached! % 178.49/25.46 % (2430105)------------------------------ % 178.49/25.46 % (2430105)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 178.49/25.46 % (2430105)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 178.49/25.46 % (2430105)CaDiCaL version: 2.1.3 % 178.49/25.46 % (2430105)Termination reason: Instruction limit % 178.49/25.46 % (2430105)Termination phase: Saturation % 178.49/25.46 % (2430105)Time elapsed: 0.091 s % 178.49/25.46 % (2430105)Peak memory usage: 16 MB % 178.49/25.46 % (2430105)Instructions burned: 362 (million) % 178.49/25.46 % (2430107)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2973878688:i=954:bd=all:rtra=on_2812 on theBenchmark for (2812ds/954Mi) % 178.49/25.46 % (2430107)Instruction limit reached! % 178.49/25.46 % (2430107)------------------------------ % 178.49/25.46 % (2430107)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 178.49/25.46 % (2430107)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 178.49/25.46 % (2430107)CaDiCaL version: 2.1.3 % 178.49/25.46 % (2430107)Termination reason: Instruction limit % 178.49/25.46 % (2430107)Termination phase: Saturation % 178.49/25.46 % (2430107)Time elapsed: 0.319 s % 178.49/25.46 % (2430107)Peak memory usage: 19 MB % 178.49/25.46 % (2430107)Instructions burned: 956 (million) % 178.49/25.46 % (2430109)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=3183504564:fmbsr=1.3:i=1730:ins=25:rtra=on_2809 on theBenchmark for (2809ds/1730Mi) % 178.49/25.46 % (2430109)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 178.49/25.46 % (2430109)Terminated due to inappropriate strategy. % 178.49/25.46 % (2430109)------------------------------ % 178.49/25.46 % (2430109)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 178.49/25.46 % (2430109)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 178.49/25.46 % (2430109)CaDiCaL version: 2.1.3 % 178.49/25.46 % (2430109)Termination reason: Inappropriate % 216.84/30.82 % (2430109)Time elapsed: 0.024 s % 216.84/30.82 % (2430109)Peak memory usage: 13 MB % 216.84/30.82 % (2430109)Instructions burned: 92 (million) % 216.84/30.82 % (2430109)------------------------------ % 216.84/30.82 % (2430109)------------------------------ % 216.84/30.82 % (2430111)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=196996145:i=2358:rtra=on_2809 on theBenchmark for (2809ds/2358Mi) % 216.84/30.82 % (2430111)Instruction limit reached! % 216.84/30.82 % (2430111)------------------------------ % 216.84/30.82 % (2430111)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 216.84/30.82 % (2430111)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 216.84/30.82 % (2430111)CaDiCaL version: 2.1.3 % 216.84/30.82 % (2430111)Termination reason: Instruction limit % 216.84/30.82 % (2430111)Termination phase: Saturation % 216.84/30.82 % (2430111)Time elapsed: 0.786 s % 216.84/30.82 % (2430111)Peak memory usage: 32 MB % 216.84/30.82 % (2430111)Instructions burned: 2363 (million) % 216.84/30.82 % (2430113)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=3361734725:i=1778:ins=1:rtra=on_2800 on theBenchmark for (2800ds/1778Mi) % 216.84/30.82 % (2430113)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 216.84/30.82 % (2430113)Terminated due to inappropriate strategy. % 216.84/30.82 % (2430113)------------------------------ % 216.84/30.82 % (2430113)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 216.84/30.82 % (2430113)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 216.84/30.82 % (2430113)CaDiCaL version: 2.1.3 % 216.84/30.82 % (2430113)Termination reason: Inappropriate % 216.84/30.82 % (2430113)Time elapsed: 0.024 s % 216.84/30.82 % (2430113)Peak memory usage: 13 MB % 216.84/30.82 % (2430113)Instructions burned: 93 (million) % 216.84/30.82 % (2430113)------------------------------ % 216.84/30.82 % (2430113)------------------------------ % 216.84/30.82 % (2430115)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=123040981:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2800 on theBenchmark for (2800ds/1384Mi) % 216.84/30.82 % (2430115)Instruction limit reached! % 216.84/30.82 % (2430115)------------------------------ % 216.84/30.82 % (2430115)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 216.84/30.82 % (2430115)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 216.84/30.82 % (2430115)CaDiCaL version: 2.1.3 % 216.84/30.82 % (2430115)Termination reason: Instruction limit % 216.84/30.82 % (2430115)Termination phase: Saturation % 216.84/30.82 % (2430115)Time elapsed: 0.446 s % 216.84/30.82 % (2430115)Peak memory usage: 24 MB % 216.84/30.82 % (2430115)Instructions burned: 1387 (million) % 216.84/30.82 % (2430117)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=2223049872:i=1758:kws=inv_precedence:fsr=off:rtra=on_2795 on theBenchmark for (2795ds/1758Mi) % 216.84/30.82 % (2430117)Instruction limit reached! % 216.84/30.82 % (2430117)------------------------------ % 216.84/30.82 % (2430117)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 216.84/30.82 % (2430117)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 216.84/30.82 % (2430117)CaDiCaL version: 2.1.3 % 216.84/30.82 % (2430117)Termination reason: Instruction limit % 216.84/30.82 % (2430117)Termination phase: Saturation % 216.84/30.82 % (2430117)Time elapsed: 0.527 s % 216.84/30.82 % (2430117)Peak memory usage: 26 MB % 216.84/30.82 % (2430117)Instructions burned: 1761 (million) % 216.84/30.82 % (2430119)fmb+10_1_sil=64000:si=on:random_seed=1421440102:i=44122:nm=2:rtra=on:gsp=on_2790 on theBenchmark for (2790ds/44122Mi) % 216.84/30.82 % (2430119)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 216.84/30.82 % (2430119)Terminated due to inappropriate strategy. % 216.84/30.82 % (2430119)------------------------------ % 216.84/30.82 % (2430119)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 216.84/30.82 % (2430119)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 216.84/30.82 % (2430119)CaDiCaL version: 2.1.3 % 216.84/30.82 % (2430119)Termination reason: Inappropriate % 216.84/30.82 % (2430119)Time elapsed: 0.025 s % 216.84/30.82 % (2430119)Peak memory usage: 13 MB % 216.84/30.82 % (2430119)Instructions burned: 94 (million) % 216.84/30.82 % (2430119)------------------------------ % 216.84/30.82 % (2430119)------------------------------ % 216.84/30.82 % (2430121)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=163092187:i=19030:nm=5:rtra=on_2790 on theBenchmark for (2790ds/19030Mi) % 262.93/37.31 % (2430121)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 262.93/37.31 % (2430121)Terminated due to inappropriate strategy. % 262.93/37.31 % (2430121)------------------------------ % 262.93/37.31 % (2430121)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 262.93/37.31 % (2430121)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 262.93/37.31 % (2430121)CaDiCaL version: 2.1.3 % 262.93/37.31 % (2430121)Termination reason: Inappropriate % 262.93/37.31 % (2430121)Time elapsed: 0.024 s % 262.93/37.31 % (2430121)Peak memory usage: 13 MB % 262.93/37.31 % (2430121)Instructions burned: 93 (million) % 262.93/37.31 % (2430121)------------------------------ % 262.93/37.31 % (2430121)------------------------------ % 262.93/37.31 % (2430123)fmb+10_1_sil=64000:sas=cadical:si=on:fmbss=8:random_seed=1367131384:fmbsr=1.7:i=1840:rtra=on_2789 on theBenchmark for (2789ds/1840Mi) % 262.93/37.31 % (2430123)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 262.93/37.31 % (2430123)Terminated due to inappropriate strategy. % 262.93/37.31 % (2430123)------------------------------ % 262.93/37.31 % (2430123)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 262.93/37.31 % (2430123)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 262.93/37.31 % (2430123)CaDiCaL version: 2.1.3 % 262.93/37.31 % (2430123)Termination reason: Inappropriate % 262.93/37.31 % (2430123)Time elapsed: 0.024 s % 262.93/37.31 % (2430123)Peak memory usage: 13 MB % 262.93/37.31 % (2430123)Instructions burned: 93 (million) % 262.93/37.31 % (2430123)------------------------------ % 262.93/37.31 % (2430123)------------------------------ % 262.93/37.31 % (2430125)dis-4_1_sil=16000:drc=ordering:si=on:sp=const_frequency:sac=on:newcnf=on:random_seed=3190600859:i=10262:rtra=on_2789 on theBenchmark for (2789ds/10262Mi) % 262.93/37.31 % (2430125)Instruction limit reached! % 262.93/37.31 % (2430125)------------------------------ % 262.93/37.31 % (2430125)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 262.93/37.31 % (2430125)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 262.93/37.31 % (2430125)CaDiCaL version: 2.1.3 % 262.93/37.31 % (2430125)Termination reason: Instruction limit % 262.93/37.31 % (2430125)Termination phase: Saturation % 262.93/37.31 % (2430125)Time elapsed: 3.056 s % 262.93/37.31 % (2430125)Peak memory usage: 79 MB % 262.93/37.31 % (2430125)Instructions burned: 10266 (million) % 262.93/37.31 % (2430127)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:si=on:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1342733729:i=2944:ins=7:rtra=on:fdi=8:gsp=on_2758 on theBenchmark for (2758ds/2944Mi) % 262.93/37.31 % (2430127)Instruction limit reached! % 262.93/37.31 % (2430127)------------------------------ % 262.93/37.31 % (2430127)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 262.93/37.31 % (2430127)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 262.93/37.31 % (2430127)CaDiCaL version: 2.1.3 % 262.93/37.31 % (2430127)Termination reason: Instruction limit % 262.93/37.31 % (2430127)Termination phase: Saturation % 262.93/37.31 % (2430127)Time elapsed: 1.005 s % 262.93/37.31 % (2430127)Peak memory usage: 47 MB % 262.93/37.31 % (2430127)Instructions burned: 2944 (million) % 262.93/37.31 % (2430129)fmb+10_1_sil=16000:sas=cadical:si=on:bce=on:fmbss=77:random_seed=3768261720:i=12648:rtra=on_2748 on theBenchmark for (2748ds/12648Mi) % 262.93/37.31 % (2430129)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 262.93/37.31 % (2430129)Terminated due to inappropriate strategy. % 262.93/37.31 % (2430129)------------------------------ % 262.93/37.31 % (2430129)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 262.93/37.31 % (2430129)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 262.93/37.31 % (2430129)CaDiCaL version: 2.1.3 % 262.93/37.31 % (2430129)Termination reason: Inappropriate % 262.93/37.31 % (2430129)Time elapsed: 0.024 s % 262.93/37.31 % (2430129)Peak memory usage: 13 MB % 262.93/37.31 % (2430129)Instructions burned: 94 (million) % 262.93/37.31 % (2430129)------------------------------ % 262.93/37.31 % (2430129)------------------------------ % 262.93/37.31 % (2430131)fmb+10_1_fmbas=function:sil=32000:sas=cadical:si=on:fmbss=16:random_seed=2662327846:fmbsr=2.30978:i=4348:rtra=on_2748 on theBenchmark for (2748ds/4348Mi) % 262.93/37.31 % (2430131)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 262.93/37.31 % (2430131)Terminated due to inappropriate strategy. % 262.93/37.31 % (2430131)------------------------------ % 300.63/42.64 % (2430131)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.63/42.64 % (2430131)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.63/42.64 % (2430131)CaDiCaL version: 2.1.3 % 300.63/42.64 % (2430131)Termination reason: Inappropriate % 300.63/42.64 % (2430131)Time elapsed: 0.024 s % 300.63/42.64 % (2430131)Peak memory usage: 13 MB % 300.63/42.64 % (2430131)Instructions burned: 93 (million) % 300.63/42.64 % (2430131)------------------------------ % 300.63/42.64 % (2430131)------------------------------ % 300.63/42.64 % (2430133)ott-2_1_sil=16000:si=on:newcnf=on:random_seed=623525263:avsq=on:i=1738:avsqr=1,16:kws=inv_arity_squared:rtra=on_2747 on theBenchmark for (2747ds/1738Mi) % 300.63/42.64 % (2430133)Instruction limit reached! % 300.63/42.64 % (2430133)------------------------------ % 300.63/42.64 % (2430133)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.63/42.64 % (2430133)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.63/42.64 % (2430133)CaDiCaL version: 2.1.3 % 300.63/42.64 % (2430133)Termination reason: Instruction limit % 300.63/42.64 % (2430133)Termination phase: Saturation % 300.63/42.64 % (2430133)Time elapsed: 0.527 s % 300.63/42.64 % (2430133)Peak memory usage: 25 MB % 300.63/42.64 % (2430133)Instructions burned: 1747 (million) % 300.63/42.64 % (2430135)ott+10_1_sil=32000:tgt=ground:si=on:random_seed=1445277682:i=10228:av=off:rtra=on_2742 on theBenchmark for (2742ds/10228Mi) % 300.63/42.64 % (2430073)Instruction limit reached! % 300.63/42.64 % (2430073)------------------------------ % 300.63/42.64 % (2430073)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.63/42.64 % (2430073)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.63/42.64 % (2430073)CaDiCaL version: 2.1.3 % 300.63/42.64 % (2430073)Termination reason: Instruction limit % 300.63/42.64 % (2430073)Termination phase: Saturation % 300.63/42.64 % (2430073)Time elapsed: 13.263 s % 300.63/42.64 % (2430073)Peak memory usage: 91 MB % 300.63/42.64 % (2430073)Instructions burned: 28120 (million) % 300.63/42.64 % (2430137)fmb+10_1_sil=64000:sas=cadical:si=on:bce=on:rp=on:random_seed=517417466:i=108564:rtra=on_2715 on theBenchmark for (2715ds/108564Mi) % 300.63/42.64 % (2430135)Instruction limit reached! % 300.63/42.64 % (2430135)------------------------------ % 300.63/42.64 % (2430135)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.63/42.64 % (2430135)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.63/42.64 % (2430135)CaDiCaL version: 2.1.3 % 300.63/42.64 % (2430135)Termination reason: Instruction limit % 300.63/42.64 % (2430135)Termination phase: Saturation % 300.63/42.64 % (2430135)Time elapsed: 2.683 s % 300.63/42.64 % (2430135)Peak memory usage: 19 MB % 300.63/42.64 % (2430135)Instructions burned: 10232 (million) % 300.63/42.64 % (2430139)dis-11_1_sil=16000:si=on:sp=reverse_frequency:alpa=true:random_seed=4023988590:i=7024:aac=none:rtra=on_2715 on theBenchmark for (2715ds/7024Mi) % 300.63/42.64 % (2430137)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 300.63/42.64 % (2430137)Terminated due to inappropriate strategy. % 300.63/42.64 % (2430137)------------------------------ % 300.63/42.64 % (2430137)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.63/42.64 % (2430137)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.63/42.64 % (2430137)CaDiCaL version: 2.1.3 % 300.63/42.64 % (2430137)Termination reason: Inappropriate % 300.63/42.64 % (2430137)Time elapsed: 0.047 s % 300.63/42.64 % (2430137)Peak memory usage: 13 MB % 300.63/42.64 % (2430137)Instructions burned: 94 (million) % 300.63/42.64 % (2430137)------------------------------ % 300.63/42.64 % (2430137)------------------------------ % 300.63/42.64 % (2430141)dis+21_1_sil=32000:sas=cadical:si=on:random_seed=3236098405:i=7546:rtra=on:amm=off_2715 on theBenchmark for (2715ds/7546Mi) % 300.63/42.64 % (2430139)Instruction limit reached! % 300.63/42.64 % (2430139)------------------------------ % 300.63/42.64 % (2430139)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.63/42.64 % (2430139)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.63/42.64 % (2430139)CaDiCaL version: 2.1.3 % 300.63/42.64 % (2430139)Termination reason: Instruction limit % 300.63/42.64 % (2430139)Termination phase: Saturation % 300.63/42.64 % (2430139)Time elapsed: 2.094 s % 300.63/42.64 % (2430139)Peak memory usage: 55 MB % 300.63/42.64 % (2430139)Instructions burned: 7024 (million) % 300.63/42.64 % (2430144)ott+11_1_sil=16000:si=on:gs=on:random_seed=2398591070:s2a=on:i=4502:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:rtra=on:fsd= % 300.63/42.64 Terminated % 300.63/42.64 % Vampire exiting % 300.63/42.64 Terminated %------------------------------------------------------------------------------