%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWC448_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 : n014.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:01 PM UTC 2026 % Result : Timeout 297.91s 42.23s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWC448_1 : TPTP v9.3.1. Released v9.0.0. % 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.10/0.22 % Computer : n014.cluster.edu % 0.10/0.22 % Model : x86_64 x86_64 % 0.10/0.22 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.22 % Memory : 8046.5625MB % 0.10/0.22 % OS : Linux 6.8.0-71-generic % 0.10/0.22 % CPULimit : 300 % 0.10/0.22 % WCLimit : 300 % 0.10/0.22 % DateTime : Mon Sep 28 09:37:45 UTC 2026 % 0.10/0.22 % CPUTime : % 0.10/0.22 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.10/0.27 Running first-order model finding % 0.10/0.27 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 % 7.34/1.30 % (1662684)Will run a generic schedule for satisfiability detection. % 7.34/1.30 % (1662693)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2524358458:i=116_2999 on theBenchmark for (2999ds/116Mi) % 7.34/1.30 % (1662690)% WARNING: option uhcvi not known. % 7.34/1.30 % (1662689)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=4283840810_2999 on theBenchmark for (2999ds/0Mi) % 7.34/1.30 % (1662692)dis+10_1_sil=32000:sp=arity:random_seed=2340036602:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 7.34/1.30 % (1662690)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=893325986:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 7.34/1.30 % (1662689)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 7.34/1.30 % (1662689)Terminated due to inappropriate strategy. % 7.34/1.30 % (1662689)------------------------------ % 7.34/1.30 % (1662689)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.34/1.30 % (1662689)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.34/1.30 % (1662689)CaDiCaL version: 2.1.3 % 7.34/1.30 % (1662689)Termination reason: Inappropriate % 7.34/1.30 % (1662689)Time elapsed: 0.002 s % 7.34/1.30 % (1662689)Peak memory usage: 10 MB % 7.34/1.30 % (1662689)Instructions burned: 1 (million) % 7.34/1.30 % (1662691)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=760408435:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 7.34/1.30 % (1662694)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3210590981:i=131_2999 on theBenchmark for (2999ds/131Mi) % 7.34/1.30 % (1662695)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2408689226:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 7.34/1.30 % (1662689)------------------------------ % 7.34/1.30 % (1662689)------------------------------ % 7.34/1.30 % (1662703)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=4054893828:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 7.34/1.30 % (1662703)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 7.34/1.30 % (1662703)Terminated due to inappropriate strategy. % 7.34/1.30 % (1662703)------------------------------ % 7.34/1.30 % (1662703)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.34/1.30 % (1662703)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.34/1.30 % (1662703)CaDiCaL version: 2.1.3 % 7.34/1.30 % (1662703)Termination reason: Inappropriate % 7.34/1.30 % (1662703)Time elapsed: 0.001 s % 7.34/1.30 % (1662703)Peak memory usage: 10 MB % 7.34/1.30 % (1662703)Instructions burned: 1 (million) % 7.34/1.30 % (1662703)------------------------------ % 7.34/1.30 % (1662703)------------------------------ % 7.34/1.30 % (1662693)Instruction limit reached! % 7.34/1.30 % (1662693)------------------------------ % 7.34/1.30 % (1662693)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.34/1.30 % (1662693)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.34/1.30 % (1662693)CaDiCaL version: 2.1.3 % 7.34/1.30 % (1662693)Termination reason: Instruction limit % 7.34/1.30 % (1662693)Termination phase: Saturation % 7.34/1.30 % (1662693)Time elapsed: 0.063 s % 7.34/1.30 % (1662693)Peak memory usage: 12 MB % 7.34/1.30 % (1662693)Instructions burned: 117 (million) % 7.34/1.30 % (1662705)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2467304223:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 7.34/1.30 % (1662706)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=4166672563:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi) % 7.34/1.30 % (1662692)Instruction limit reached! % 7.34/1.30 % (1662692)------------------------------ % 7.34/1.30 % (1662692)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.34/1.30 % (1662692)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.34/1.30 % (1662692)CaDiCaL version: 2.1.3 % 7.34/1.30 % (1662692)Termination reason: Instruction limit % 7.34/1.30 % (1662692)Termination phase: Saturation % 7.34/1.30 % (1662692)Time elapsed: 0.099 s % 7.34/1.30 % (1662692)Peak memory usage: 12 MB % 7.34/1.30 % (1662692)Instructions burned: 103 (million) % 7.34/1.30 % (1662694)Instruction limit reached! % 7.34/1.30 % (1662694)------------------------------ % 7.34/1.30 % (1662694)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.03/1.44 % (1662694)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.03/1.44 % (1662694)CaDiCaL version: 2.1.3 % 8.03/1.44 % (1662694)Termination reason: Instruction limit % 8.03/1.44 % (1662694)Termination phase: Saturation % 8.03/1.44 % (1662694)Time elapsed: 0.125 s % 8.03/1.44 % (1662694)Peak memory usage: 12 MB % 8.03/1.44 % (1662694)Instructions burned: 131 (million) % 8.03/1.44 % (1662709)ott-21_1_sil=16000:fs=off:random_seed=1375631422:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 8.03/1.44 % (1662710)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3650953913:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 8.03/1.44 % (1662695)Instruction limit reached! % 8.03/1.44 % (1662695)------------------------------ % 8.03/1.44 % (1662695)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.03/1.44 % (1662695)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.03/1.44 % (1662695)CaDiCaL version: 2.1.3 % 8.03/1.44 % (1662695)Termination reason: Instruction limit % 8.03/1.44 % (1662695)Termination phase: Saturation % 8.03/1.44 % (1662695)Time elapsed: 0.170 s % 8.03/1.44 % (1662695)Peak memory usage: 13 MB % 8.03/1.44 % (1662695)Instructions burned: 159 (million) % 8.03/1.44 % (1662705)Instruction limit reached! % 8.03/1.44 % (1662705)------------------------------ % 8.03/1.44 % (1662705)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.03/1.44 % (1662705)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.03/1.44 % (1662705)CaDiCaL version: 2.1.3 % 8.03/1.44 % (1662705)Termination reason: Instruction limit % 8.03/1.44 % (1662705)Termination phase: Saturation % 8.03/1.44 % (1662705)Time elapsed: 0.146 s % 8.03/1.44 % (1662705)Peak memory usage: 13 MB % 8.03/1.44 % (1662705)Instructions burned: 131 (million) % 8.03/1.44 % (1662713)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3591564604:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi) % 8.03/1.44 % (1662713)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 8.03/1.44 % (1662713)Terminated due to inappropriate strategy. % 8.03/1.44 % (1662713)------------------------------ % 8.03/1.44 % (1662713)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.03/1.44 % (1662713)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.03/1.44 % (1662713)CaDiCaL version: 2.1.3 % 8.03/1.44 % (1662713)Termination reason: Inappropriate % 8.03/1.44 % (1662713)Time elapsed: 0.001 s % 8.03/1.44 % (1662713)Peak memory usage: 10 MB % 8.03/1.44 % (1662713)Instructions burned: 1 (million) % 8.03/1.44 % (1662713)------------------------------ % 8.03/1.44 % (1662713)------------------------------ % 8.03/1.44 % (1662714)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2705841093:i=1179_2997 on theBenchmark for (2997ds/1179Mi) % 8.03/1.44 % (1662716)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1234615063:i=889:ins=1_2997 on theBenchmark for (2997ds/889Mi) % 8.03/1.44 % (1662716)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 8.03/1.44 % (1662716)Terminated due to inappropriate strategy. % 8.03/1.44 % (1662716)------------------------------ % 8.03/1.44 % (1662716)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.03/1.44 % (1662716)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.03/1.44 % (1662716)CaDiCaL version: 2.1.3 % 8.03/1.44 % (1662716)Termination reason: Inappropriate % 8.03/1.44 % (1662716)Time elapsed: 0.001 s % 8.03/1.44 % (1662716)Peak memory usage: 10 MB % 8.03/1.44 % (1662716)Instructions burned: 1 (million) % 8.03/1.44 % (1662716)------------------------------ % 8.03/1.44 % (1662716)------------------------------ % 8.03/1.44 % (1662709)Instruction limit reached! % 8.03/1.44 % (1662709)------------------------------ % 8.03/1.44 % (1662709)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.03/1.44 % (1662709)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.03/1.44 % (1662709)CaDiCaL version: 2.1.3 % 8.03/1.44 % (1662709)Termination reason: Instruction limit % 8.03/1.44 % (1662709)Termination phase: Saturation % 8.03/1.44 % (1662709)Time elapsed: 0.141 s % 8.03/1.44 % (1662709)Peak memory usage: 12 MB % 8.03/1.44 % (1662709)Instructions burned: 181 (million) % 8.03/1.44 % (1662719)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=1620328084: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) % 30.77/4.67 % (1662720)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1980192451:i=879:kws=inv_precedence:fsr=off_2996 on theBenchmark for (2996ds/879Mi) % 30.77/4.67 % (1662706)Instruction limit reached! % 30.77/4.67 % (1662706)------------------------------ % 30.77/4.67 % (1662706)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 30.77/4.67 % (1662706)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 30.77/4.67 % (1662706)CaDiCaL version: 2.1.3 % 30.77/4.67 % (1662706)Termination reason: Instruction limit % 30.77/4.67 % (1662706)Termination phase: Saturation % 30.77/4.67 % (1662706)Time elapsed: 0.332 s % 30.77/4.67 % (1662706)Peak memory usage: 17 MB % 30.77/4.67 % (1662706)Instructions burned: 684 (million) % 30.77/4.67 % (1662723)fmb+10_1_sil=64000:random_seed=3164260735:i=22061:nm=2:gsp=on_2995 on theBenchmark for (2995ds/22061Mi) % 30.77/4.67 % (1662723)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 30.77/4.67 % (1662723)Terminated due to inappropriate strategy. % 30.77/4.67 % (1662723)------------------------------ % 30.77/4.67 % (1662723)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 30.77/4.67 % (1662723)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 30.77/4.67 % (1662723)CaDiCaL version: 2.1.3 % 30.77/4.67 % (1662723)Termination reason: Inappropriate % 30.77/4.67 % (1662723)Time elapsed: 0.001 s % 30.77/4.67 % (1662723)Peak memory usage: 11 MB % 30.77/4.67 % (1662723)Instructions burned: 1 (million) % 30.77/4.67 % (1662723)------------------------------ % 30.77/4.67 % (1662723)------------------------------ % 30.77/4.67 % (1662725)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2831323550:i=9515:nm=5_2995 on theBenchmark for (2995ds/9515Mi) % 30.77/4.67 % (1662725)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 30.77/4.67 % (1662725)Terminated due to inappropriate strategy. % 30.77/4.67 % (1662725)------------------------------ % 30.77/4.67 % (1662725)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 30.77/4.67 % (1662725)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 30.77/4.67 % (1662725)CaDiCaL version: 2.1.3 % 30.77/4.67 % (1662725)Termination reason: Inappropriate % 30.77/4.67 % (1662725)Time elapsed: 0.001 s % 30.77/4.67 % (1662725)Peak memory usage: 10 MB % 30.77/4.67 % (1662725)Instructions burned: 1 (million) % 30.77/4.67 % (1662725)------------------------------ % 30.77/4.67 % (1662725)------------------------------ % 30.77/4.67 % (1662727)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=4284746315:fmbsr=1.7:i=920_2995 on theBenchmark for (2995ds/920Mi) % 30.77/4.67 % (1662727)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 30.77/4.67 % (1662727)Terminated due to inappropriate strategy. % 30.77/4.67 % (1662727)------------------------------ % 30.77/4.67 % (1662727)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 30.77/4.67 % (1662727)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 30.77/4.67 % (1662727)CaDiCaL version: 2.1.3 % 30.77/4.67 % (1662727)Termination reason: Inappropriate % 30.77/4.67 % (1662727)Time elapsed: 0.001 s % 30.77/4.67 % (1662727)Peak memory usage: 10 MB % 30.77/4.67 % (1662727)Instructions burned: 1 (million) % 30.77/4.67 % (1662727)------------------------------ % 30.77/4.67 % (1662727)------------------------------ % 30.77/4.67 % (1662729)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2420418823:i=5131_2994 on theBenchmark for (2994ds/5131Mi) % 30.77/4.67 % (1662710)Instruction limit reached! % 30.77/4.67 % (1662710)------------------------------ % 30.77/4.67 % (1662710)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 30.77/4.67 % (1662710)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 30.77/4.67 % (1662710)CaDiCaL version: 2.1.3 % 30.77/4.67 % (1662710)Termination reason: Instruction limit % 30.77/4.67 % (1662710)Termination phase: Saturation % 30.77/4.67 % (1662710)Time elapsed: 0.504 s % 30.77/4.67 % (1662710)Peak memory usage: 14 MB % 30.77/4.67 % (1662710)Instructions burned: 478 (million) % 30.77/4.67 % (1662731)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1999547359:i=1472:ins=7:fdi=8:gsp=on_2993 on theBenchmark for (2993ds/1472Mi) % 30.77/4.67 % (1662719)Instruction limit reached! % 30.77/4.67 % (1662719)------------------------------ % 43.51/6.46 % (1662719)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 43.51/6.46 % (1662719)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 43.51/6.46 % (1662719)CaDiCaL version: 2.1.3 % 43.51/6.46 % (1662719)Termination reason: Instruction limit % 43.51/6.46 % (1662719)Termination phase: Saturation % 43.51/6.46 % (1662719)Time elapsed: 0.701 s % 43.51/6.46 % (1662719)Peak memory usage: 19 MB % 43.51/6.46 % (1662719)Instructions burned: 692 (million) % 43.51/6.46 % (1662733)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=974926528:i=6324_2989 on theBenchmark for (2989ds/6324Mi) % 43.51/6.46 % (1662733)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 43.51/6.46 % (1662733)Terminated due to inappropriate strategy. % 43.51/6.46 % (1662733)------------------------------ % 43.51/6.46 % (1662733)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 43.51/6.46 % (1662733)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 43.51/6.46 % (1662733)CaDiCaL version: 2.1.3 % 43.51/6.46 % (1662733)Termination reason: Inappropriate % 43.51/6.46 % (1662733)Time elapsed: 0.001 s % 43.51/6.46 % (1662733)Peak memory usage: 11 MB % 43.51/6.46 % (1662733)Instructions burned: 1 (million) % 43.51/6.46 % (1662733)------------------------------ % 43.51/6.46 % (1662733)------------------------------ % 43.51/6.46 % (1662735)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=2440446787:fmbsr=2.30978:i=2174_2989 on theBenchmark for (2989ds/2174Mi) % 43.51/6.46 % (1662735)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 43.51/6.46 % (1662735)Terminated due to inappropriate strategy. % 43.51/6.46 % (1662735)------------------------------ % 43.51/6.46 % (1662735)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 43.51/6.46 % (1662735)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 43.51/6.46 % (1662735)CaDiCaL version: 2.1.3 % 43.51/6.46 % (1662735)Termination reason: Inappropriate % 43.51/6.46 % (1662735)Time elapsed: 0.002 s % 43.51/6.46 % (1662735)Peak memory usage: 11 MB % 43.51/6.46 % (1662735)Instructions burned: 1 (million) % 43.51/6.46 % (1662735)------------------------------ % 43.51/6.46 % (1662735)------------------------------ % 43.51/6.46 % (1662737)ott-2_1_sil=16000:newcnf=on:random_seed=2445126216:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2989 on theBenchmark for (2989ds/869Mi) % 43.51/6.46 % (1662714)Instruction limit reached! % 43.51/6.46 % (1662714)------------------------------ % 43.51/6.46 % (1662714)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 43.51/6.46 % (1662714)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 43.51/6.46 % (1662714)CaDiCaL version: 2.1.3 % 43.51/6.46 % (1662714)Termination reason: Instruction limit % 43.51/6.46 % (1662714)Termination phase: Saturation % 43.51/6.46 % (1662714)Time elapsed: 0.850 s % 43.51/6.46 % (1662714)Peak memory usage: 14 MB % 43.51/6.46 % (1662714)Instructions burned: 1179 (million) % 43.51/6.46 % (1662720)Instruction limit reached! % 43.51/6.46 % (1662720)------------------------------ % 43.51/6.46 % (1662720)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 43.51/6.46 % (1662720)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 43.51/6.46 % (1662720)CaDiCaL version: 2.1.3 % 43.51/6.46 % (1662720)Termination reason: Instruction limit % 43.51/6.46 % (1662720)Termination phase: Saturation % 43.51/6.46 % (1662720)Time elapsed: 0.780 s % 43.51/6.46 % (1662720)Peak memory usage: 19 MB % 43.51/6.46 % (1662720)Instructions burned: 880 (million) % 43.51/6.46 % (1662739)ott+10_1_sil=32000:tgt=ground:random_seed=2944233557:i=5114:av=off_2988 on theBenchmark for (2988ds/5114Mi) % 43.51/6.46 % (1662740)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=738119764:i=54282_2988 on theBenchmark for (2988ds/54282Mi) % 43.51/6.46 % (1662740)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 43.51/6.46 % (1662740)Terminated due to inappropriate strategy. % 43.51/6.46 % (1662740)------------------------------ % 43.51/6.46 % (1662740)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 43.51/6.46 % (1662740)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 43.51/6.46 % (1662740)CaDiCaL version: 2.1.3 % 43.51/6.46 % (1662740)Termination reason: Inappropriate % 43.51/6.46 % (1662740)Time elapsed: 0.002 s % 43.51/6.46 % (1662740)Peak memory usage: 10 MB % 43.51/6.46 % (1662740)Instructions burned: 1 (million) % 173.68/24.78 % (1662740)------------------------------ % 173.68/24.78 % (1662740)------------------------------ % 173.68/24.78 % (1662743)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3492908692:i=3512:aac=none_2988 on theBenchmark for (2988ds/3512Mi) % 173.68/24.78 % (1662737)Instruction limit reached! % 173.68/24.78 % (1662737)------------------------------ % 173.68/24.78 % (1662737)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 173.68/24.78 % (1662737)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 173.68/24.78 % (1662737)CaDiCaL version: 2.1.3 % 173.68/24.78 % (1662737)Termination reason: Instruction limit % 173.68/24.78 % (1662737)Termination phase: Saturation % 173.68/24.78 % (1662737)Time elapsed: 0.780 s % 173.68/24.78 % (1662737)Peak memory usage: 17 MB % 173.68/24.78 % (1662737)Instructions burned: 870 (million) % 173.68/24.78 % (1662745)dis+21_1_sil=32000:sas=cadical:random_seed=784366988:i=3773:amm=off_2981 on theBenchmark for (2981ds/3773Mi) % 173.68/24.78 % (1662731)Instruction limit reached! % 173.68/24.78 % (1662731)------------------------------ % 173.68/24.78 % (1662731)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 173.68/24.78 % (1662731)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 173.68/24.78 % (1662731)CaDiCaL version: 2.1.3 % 173.68/24.78 % (1662731)Termination reason: Instruction limit % 173.68/24.78 % (1662731)Termination phase: Saturation % 173.68/24.78 % (1662731)Time elapsed: 1.474 s % 173.68/24.78 % (1662731)Peak memory usage: 23 MB % 173.68/24.78 % (1662731)Instructions burned: 1472 (million) % 173.68/24.78 % (1662749)ott+11_1_sil=16000:gs=on:random_seed=2497120167:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2977 on theBenchmark for (2977ds/2251Mi) % 173.68/24.78 % (1662729)Instruction limit reached! % 173.68/24.78 % (1662729)------------------------------ % 173.68/24.78 % (1662729)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 173.68/24.78 % (1662729)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 173.68/24.78 % (1662729)CaDiCaL version: 2.1.3 % 173.68/24.78 % (1662729)Termination reason: Instruction limit % 173.68/24.78 % (1662729)Termination phase: Saturation % 173.68/24.78 % (1662729)Time elapsed: 2.495 s % 173.68/24.78 % (1662729)Peak memory usage: 42 MB % 173.68/24.78 % (1662729)Instructions burned: 5132 (million) % 173.68/24.78 % (1662751)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=2616814744:fmbsr=1.6:i=67534_2969 on theBenchmark for (2969ds/67534Mi) % 173.68/24.78 % (1662751)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 173.68/24.78 % (1662751)Terminated due to inappropriate strategy. % 173.68/24.78 % (1662751)------------------------------ % 173.68/24.78 % (1662751)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 173.68/24.78 % (1662751)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 173.68/24.78 % (1662751)CaDiCaL version: 2.1.3 % 173.68/24.78 % (1662751)Termination reason: Inappropriate % 173.68/24.78 % (1662751)Time elapsed: 0.001 s % 173.68/24.78 % (1662751)Peak memory usage: 10 MB % 173.68/24.78 % (1662751)Instructions burned: 1 (million) % 173.68/24.78 % (1662751)------------------------------ % 173.68/24.78 % (1662751)------------------------------ % 173.68/24.78 % (1662753)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=3358609163:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2969 on theBenchmark for (2969ds/4591Mi) % 173.68/24.78 % (1662749)Instruction limit reached! % 173.68/24.78 % (1662749)------------------------------ % 173.68/24.78 % (1662749)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 173.68/24.78 % (1662749)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 173.68/24.78 % (1662749)CaDiCaL version: 2.1.3 % 173.68/24.78 % (1662749)Termination reason: Instruction limit % 173.68/24.78 % (1662749)Termination phase: Saturation % 173.68/24.78 % (1662749)Time elapsed: 2.128 s % 173.68/24.78 % (1662749)Peak memory usage: 22 MB % 173.68/24.78 % (1662749)Instructions burned: 2252 (million) % 173.68/24.78 % (1662743)Instruction limit reached! % 173.68/24.78 % (1662743)------------------------------ % 173.68/24.78 % (1662743)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 173.68/24.78 % (1662743)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 173.68/24.78 % (1662743)CaDiCaL version: 2.1.3 % 173.68/24.78 % (1662743)Termination reason: Instruction limit % 173.68/24.78 % (1662743)Termination phase: Saturation % 173.68/24.78 % (1662743)Time elapsed: 3.204 s % 173.68/24.78 % (1662743)Peak memory usage: 34 MB % 207.08/29.49 % (1662743)Instructions burned: 3513 (million) % 207.08/29.49 % (1662775)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=1747676152:i=29340_2956 on theBenchmark for (2956ds/29340Mi) % 207.08/29.49 % (1662777)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=2337787413:i=5211_2956 on theBenchmark for (2956ds/5211Mi) % 207.08/29.49 % (1662753)Instruction limit reached! % 207.08/29.49 % (1662753)------------------------------ % 207.08/29.49 % (1662753)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 207.08/29.49 % (1662753)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 207.08/29.49 % (1662753)CaDiCaL version: 2.1.3 % 207.08/29.49 % (1662753)Termination reason: Instruction limit % 207.08/29.49 % (1662753)Termination phase: Saturation % 207.08/29.49 % (1662753)Time elapsed: 2.191 s % 207.08/29.49 % (1662753)Peak memory usage: 43 MB % 207.08/29.49 % (1662753)Instructions burned: 4592 (million) % 207.08/29.49 % (1662781)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=2016473243:i=5497:nm=2_2947 on theBenchmark for (2947ds/5497Mi) % 207.08/29.49 % (1662781)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 207.08/29.49 % (1662781)Terminated due to inappropriate strategy. % 207.08/29.49 % (1662781)------------------------------ % 207.08/29.49 % (1662781)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 207.08/29.49 % (1662781)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 207.08/29.49 % (1662781)CaDiCaL version: 2.1.3 % 207.08/29.49 % (1662781)Termination reason: Inappropriate % 207.08/29.49 % (1662781)Time elapsed: 0.001 s % 207.08/29.49 % (1662781)Peak memory usage: 10 MB % 207.08/29.49 % (1662781)Instructions burned: 1 (million) % 207.08/29.49 % (1662781)------------------------------ % 207.08/29.49 % (1662781)------------------------------ % 207.08/29.49 % (1662783)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=103494899:fmbsr=2:i=46332_2946 on theBenchmark for (2946ds/46332Mi) % 207.08/29.49 % (1662783)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 207.08/29.49 % (1662783)Terminated due to inappropriate strategy. % 207.08/29.49 % (1662783)------------------------------ % 207.08/29.49 % (1662783)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 207.08/29.49 % (1662783)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 207.08/29.49 % (1662783)CaDiCaL version: 2.1.3 % 207.08/29.49 % (1662783)Termination reason: Inappropriate % 207.08/29.49 % (1662783)Time elapsed: 0.001 s % 207.08/29.49 % (1662783)Peak memory usage: 11 MB % 207.08/29.49 % (1662783)Instructions burned: 1 (million) % 207.08/29.49 % (1662783)------------------------------ % 207.08/29.49 % (1662783)------------------------------ % 207.08/29.49 % (1662785)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=8883704:i=14071_2946 on theBenchmark for (2946ds/14071Mi) % 207.08/29.49 % (1662785)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 207.08/29.49 % (1662785)Terminated due to inappropriate strategy. % 207.08/29.49 % (1662785)------------------------------ % 207.08/29.49 % (1662785)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 207.08/29.49 % (1662785)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 207.08/29.49 % (1662785)CaDiCaL version: 2.1.3 % 207.08/29.49 % (1662785)Termination reason: Inappropriate % 207.08/29.49 % (1662785)Time elapsed: 0.001 s % 207.08/29.49 % (1662785)Peak memory usage: 10 MB % 207.08/29.49 % (1662785)Instructions burned: 1 (million) % 207.08/29.49 % (1662785)------------------------------ % 207.08/29.49 % (1662785)------------------------------ % 207.08/29.49 % (1662787)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2917426376:i=22565:add=on:rawr=on_2946 on theBenchmark for (2946ds/22565Mi) % 207.08/29.49 % (1662745)Instruction limit reached! % 207.08/29.49 % (1662745)------------------------------ % 207.08/29.49 % (1662745)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 207.08/29.49 % (1662745)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 207.08/29.49 % (1662745)CaDiCaL version: 2.1.3 % 207.08/29.49 % (1662745)Termination reason: Instruction limit % 207.08/29.49 % (1662745)Termination phase: Saturation % 207.08/29.49 % (1662745)Time elapsed: 3.468 s % 207.08/29.49 % (1662745)Peak memory usage: 31 MB % 207.08/29.49 % (1662745)Instructions burned: 3773 (million) % 207.08/29.49 % (1662790)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=2698326752:i=8173:av=off_2946 on theBenchmark for (2946ds/8173Mi) % 207.08/29.49 % (1662739)Instruction limit reached! % 207.81/29.60 % (1662739)------------------------------ % 207.81/29.60 % (1662739)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 207.81/29.60 % (1662739)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 207.81/29.60 % (1662739)CaDiCaL version: 2.1.3 % 207.81/29.60 % (1662739)Termination reason: Instruction limit % 207.81/29.60 % (1662739)Termination phase: Saturation % 207.81/29.60 % (1662739)Time elapsed: 5.033 s % 207.81/29.60 % (1662739)Peak memory usage: 42 MB % 207.81/29.60 % (1662739)Instructions burned: 5114 (million) % 207.81/29.60 % (1662797)dis+10_16:1_sil=16000:random_seed=3418281002:i=9155:fsr=off_2938 on theBenchmark for (2938ds/9155Mi) % 207.81/29.60 % (1662777)Instruction limit reached! % 207.81/29.60 % (1662777)------------------------------ % 207.81/29.60 % (1662777)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 207.81/29.60 % (1662777)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 207.81/29.60 % (1662777)CaDiCaL version: 2.1.3 % 207.81/29.60 % (1662777)Termination reason: Instruction limit % 207.81/29.60 % (1662777)Termination phase: Saturation % 207.81/29.60 % (1662777)Time elapsed: 4.589 s % 207.81/29.60 % (1662777)Peak memory usage: 45 MB % 207.81/29.60 % (1662777)Instructions burned: 5211 (million) % 207.81/29.60 % (1662809)ott-3_8_sil=64000:random_seed=916641049:i=20139:bs=on_2909 on theBenchmark for (2909ds/20139Mi) % 207.81/29.60 % (1662790)Instruction limit reached! % 207.81/29.60 % (1662790)------------------------------ % 207.81/29.60 % (1662790)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 207.81/29.60 % (1662790)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 207.81/29.60 % (1662790)CaDiCaL version: 2.1.3 % 207.81/29.60 % (1662790)Termination reason: Instruction limit % 207.81/29.60 % (1662790)Termination phase: Saturation % 207.81/29.60 % (1662790)Time elapsed: 7.485 s % 207.81/29.60 % (1662790)Peak memory usage: 54 MB % 207.81/29.60 % (1662790)Instructions burned: 8173 (million) % 207.81/29.60 % (1662821)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=2728210941:fmbsr=2:i=32576_2870 on theBenchmark for (2870ds/32576Mi) % 207.81/29.60 % (1662821)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 207.81/29.60 % (1662821)Terminated due to inappropriate strategy. % 207.81/29.60 % (1662821)------------------------------ % 207.81/29.60 % (1662821)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 207.81/29.60 % (1662821)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 207.81/29.60 % (1662821)CaDiCaL version: 2.1.3 % 207.81/29.60 % (1662821)Termination reason: Inappropriate % 207.81/29.60 % (1662821)Time elapsed: 0.001 s % 207.81/29.60 % (1662821)Peak memory usage: 10 MB % 207.81/29.60 % (1662821)Instructions burned: 1 (million) % 207.81/29.60 % (1662821)------------------------------ % 207.81/29.60 % (1662821)------------------------------ % 207.81/29.60 % (1662823)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=3524483861:i=11404_2870 on theBenchmark for (2870ds/11404Mi) % 207.81/29.60 % (1662797)Instruction limit reached! % 207.81/29.60 % (1662797)------------------------------ % 207.81/29.60 % (1662797)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 207.81/29.60 % (1662797)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 207.81/29.60 % (1662797)CaDiCaL version: 2.1.3 % 207.81/29.60 % (1662797)Termination reason: Instruction limit % 207.81/29.60 % (1662797)Termination phase: Saturation % 207.81/29.60 % (1662797)Time elapsed: 7.815 s % 207.81/29.60 % (1662797)Peak memory usage: 51 MB % 207.81/29.60 % (1662797)Instructions burned: 9155 (million) % 207.81/29.60 % (1662825)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=2580706408:i=14134_2859 on theBenchmark for (2859ds/14134Mi) % 207.81/29.60 % (1662787)Instruction limit reached! % 207.81/29.60 % (1662787)------------------------------ % 207.81/29.60 % (1662787)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 207.81/29.60 % (1662787)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 207.81/29.60 % (1662787)CaDiCaL version: 2.1.3 % 207.81/29.60 % (1662787)Termination reason: Instruction limit % 207.81/29.60 % (1662787)Termination phase: Saturation % 207.81/29.60 % (1662787)Time elapsed: 16.590 s % 207.81/29.60 % (1662787)Peak memory usage: 72 MB % 207.81/29.60 % (1662787)Instructions burned: 22565 (million) % 207.81/29.60 % (1662836)dis+33_16_sil=32000:sac=on:random_seed=2615188771:i=15851:nm=0_2780 on theBenchmark for (2780ds/15851Mi) % 207.81/29.60 % (1662823)Instruction limit reached! % 207.81/29.60 % (1662823)------------------------------ % 207.81/29.60 % (1662823)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 253.06/36.00 % (1662823)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 253.06/36.00 % (1662823)CaDiCaL version: 2.1.3 % 253.06/36.00 % (1662823)Termination reason: Instruction limit % 253.06/36.00 % (1662823)Termination phase: Saturation % 253.06/36.00 % (1662823)Time elapsed: 11.508 s % 253.06/36.00 % (1662823)Peak memory usage: 63 MB % 253.06/36.00 % (1662823)Instructions burned: 11404 (million) % 253.06/36.00 % (1662839)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=2089703816:avsq=on:i=17627:add=on:amm=off_2754 on theBenchmark for (2754ds/17627Mi) % 253.06/36.00 % (1662825)Instruction limit reached! % 253.06/36.00 % (1662825)------------------------------ % 253.06/36.00 % (1662825)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 253.06/36.00 % (1662825)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 253.06/36.00 % (1662825)CaDiCaL version: 2.1.3 % 253.06/36.00 % (1662825)Termination reason: Instruction limit % 253.06/36.00 % (1662825)Termination phase: Saturation % 253.06/36.00 % (1662825)Time elapsed: 13.972 s % 253.06/36.00 % (1662825)Peak memory usage: 76 MB % 253.06/36.00 % (1662825)Instructions burned: 14135 (million) % 253.06/36.00 % (1662860)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=2610214813:s2a=on:i=53295_2719 on theBenchmark for (2719ds/53295Mi) % 253.06/36.00 % (1662775)Instruction limit reached! % 253.06/36.00 % (1662775)------------------------------ % 253.06/36.00 % (1662775)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 253.06/36.00 % (1662775)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 253.06/36.00 % (1662775)CaDiCaL version: 2.1.3 % 253.06/36.00 % (1662775)Termination reason: Instruction limit % 253.06/36.00 % (1662775)Termination phase: Saturation % 253.06/36.00 % (1662775)Time elapsed: 23.840 s % 253.06/36.00 % (1662775)Peak memory usage: 123 MB % 253.06/36.00 % (1662775)Instructions burned: 29340 (million) % 253.06/36.00 % (1662880)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=2270926542:i=26857:ins=20_2717 on theBenchmark for (2717ds/26857Mi) % 253.06/36.00 % (1662880)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 253.06/36.00 % (1662880)Terminated due to inappropriate strategy. % 253.06/36.00 % (1662880)------------------------------ % 253.06/36.00 % (1662880)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 253.06/36.00 % (1662880)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 253.06/36.00 % (1662880)CaDiCaL version: 2.1.3 % 253.06/36.00 % (1662880)Termination reason: Inappropriate % 253.06/36.00 % (1662880)Time elapsed: 0.001 s % 253.06/36.00 % (1662880)Peak memory usage: 11 MB % 253.06/36.00 % (1662880)Instructions burned: 1 (million) % 253.06/36.00 % (1662880)------------------------------ % 253.06/36.00 % (1662880)------------------------------ % 253.06/36.00 % (1662893)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=2407595159:i=28120:bs=on:fsr=off_2717 on theBenchmark for (2717ds/28120Mi) % 253.06/36.00 % (1662809)Instruction limit reached! % 253.06/36.00 % (1662809)------------------------------ % 253.06/36.00 % (1662809)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 253.06/36.00 % (1662809)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 253.06/36.00 % (1662809)CaDiCaL version: 2.1.3 % 253.06/36.00 % (1662809)Termination reason: Instruction limit % 253.06/36.00 % (1662809)Termination phase: Saturation % 253.06/36.00 % (1662809)Time elapsed: 20.112 s % 253.06/36.00 % (1662809)Peak memory usage: 65 MB % 253.06/36.00 % (1662809)Instructions burned: 20139 (million) % 253.06/36.00 % (1662900)fmb+10_1_sil=256000:fmbss=7:random_seed=3597887775:fmbsr=1.6:i=182295_2708 on theBenchmark for (2708ds/182295Mi) % 253.06/36.00 % (1662900)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 253.06/36.00 % (1662900)Terminated due to inappropriate strategy. % 253.06/36.00 % (1662900)------------------------------ % 253.06/36.00 % (1662900)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 253.06/36.00 % (1662900)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 253.06/36.00 % (1662900)CaDiCaL version: 2.1.3 % 253.06/36.00 % (1662900)Termination reason: Inappropriate % 253.06/36.00 % (1662900)Time elapsed: 0.001 s % 253.06/36.00 % (1662900)Peak memory usage: 10 MB % 253.06/36.00 % (1662900)Instructions burned: 1 (million) % 253.06/36.00 % (1662900)------------------------------ % 253.06/36.00 % (1662900)------------------------------ % 253.06/36.00 % (1662902)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=1876959230:i=44625:gsp=on_2708 on theBenchmark for (2708ds/44625Mi) % 265.43/37.78 % (1662902)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 265.43/37.78 % (1662902)Terminated due to inappropriate strategy. % 265.43/37.78 % (1662902)------------------------------ % 265.43/37.78 % (1662902)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 265.43/37.78 % (1662902)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 265.43/37.78 % (1662902)CaDiCaL version: 2.1.3 % 265.43/37.78 % (1662902)Termination reason: Inappropriate % 265.43/37.78 % (1662902)Time elapsed: 0.001 s % 265.43/37.78 % (1662902)Peak memory usage: 10 MB % 265.43/37.78 % (1662902)Instructions burned: 1 (million) % 265.43/37.78 % (1662902)------------------------------ % 265.43/37.78 % (1662902)------------------------------ % 265.43/37.78 % (1662904)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=2507051205:i=160505_2707 on theBenchmark for (2707ds/160505Mi) % 265.43/37.78 % (1662904)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 265.43/37.78 % (1662904)Terminated due to inappropriate strategy. % 265.43/37.78 % (1662904)------------------------------ % 265.43/37.78 % (1662904)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 265.43/37.78 % (1662904)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 265.43/37.78 % (1662904)CaDiCaL version: 2.1.3 % 265.43/37.78 % (1662904)Termination reason: Inappropriate % 265.43/37.78 % (1662904)Time elapsed: 0.001 s % 265.43/37.78 % (1662904)Peak memory usage: 10 MB % 265.43/37.78 % (1662904)Instructions burned: 1 (million) % 265.43/37.78 % (1662904)------------------------------ % 265.43/37.78 % (1662904)------------------------------ % 265.43/37.78 % (1662906)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=2075173879:fmbsr=1.3:i=225729_2707 on theBenchmark for (2707ds/225729Mi) % 265.43/37.78 % (1662906)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 265.43/37.78 % (1662906)Terminated due to inappropriate strategy. % 265.43/37.78 % (1662906)------------------------------ % 265.43/37.78 % (1662906)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 265.43/37.78 % (1662906)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 265.43/37.78 % (1662906)CaDiCaL version: 2.1.3 % 265.43/37.78 % (1662906)Termination reason: Inappropriate % 265.43/37.78 % (1662906)Time elapsed: 0.001 s % 265.43/37.78 % (1662906)Peak memory usage: 10 MB % 265.43/37.78 % (1662906)Instructions burned: 1 (million) % 265.43/37.78 % (1662906)------------------------------ % 265.43/37.78 % (1662906)------------------------------ % 265.43/37.78 % (1662908)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=3159250616:fmbsr=2:i=185024:ins=7_2707 on theBenchmark for (2707ds/185024Mi) % 265.43/37.78 % (1662908)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 265.43/37.78 % (1662908)Terminated due to inappropriate strategy. % 265.43/37.78 % (1662908)------------------------------ % 265.43/37.78 % (1662908)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 265.43/37.78 % (1662908)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 265.43/37.78 % (1662908)CaDiCaL version: 2.1.3 % 265.43/37.78 % (1662908)Termination reason: Inappropriate % 265.43/37.78 % (1662908)Time elapsed: 0.001 s % 265.43/37.78 % (1662908)Peak memory usage: 10 MB % 265.43/37.78 % (1662908)Instructions burned: 1 (million) % 265.43/37.78 % (1662908)------------------------------ % 265.43/37.78 % (1662908)------------------------------ % 265.43/37.78 % (1662910)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=1678122829:rtra=on_2707 on theBenchmark for (2707ds/0Mi) % 265.43/37.78 % (1662910)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 265.43/37.78 % (1662910)Terminated due to inappropriate strategy. % 265.43/37.78 % (1662910)------------------------------ % 265.43/37.78 % (1662910)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 265.43/37.78 % (1662910)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 265.43/37.78 % (1662910)CaDiCaL version: 2.1.3 % 265.43/37.78 % (1662910)Termination reason: Inappropriate % 265.43/37.78 % (1662910)Time elapsed: 0.001 s % 265.43/37.78 % (1662910)Peak memory usage: 10 MB % 265.43/37.78 % (1662910)Instructions burned: 1 (million) % 265.43/37.78 % (1662910)------------------------------ % 265.43/37.78 % (1662910)------------------------------ % 265.43/37.78 % (1662912)% WARNING: option uhcvi not known. % 265.43/37.78 % (1662912)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2395301942:i=271062:add=off:rtra=on:rawr=on_2707 on theBenchmark for (2707ds/271062Mi) % 280.11/39.77 % (1662836)Instruction limit reached! % 280.11/39.77 % (1662836)------------------------------ % 280.11/39.77 % (1662836)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 280.11/39.77 % (1662836)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 280.11/39.77 % (1662836)CaDiCaL version: 2.1.3 % 280.11/39.77 % (1662836)Termination reason: Instruction limit % 280.11/39.77 % (1662836)Termination phase: Saturation % 280.11/39.77 % (1662836)Time elapsed: 9.835 s % 280.11/39.77 % (1662836)Peak memory usage: 202 MB % 280.11/39.77 % (1662836)Instructions burned: 15853 (million) % 280.11/39.77 % (1662914)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3848666112:i=176048:add=on:rtra=on:rawr=on_2681 on theBenchmark for (2681ds/176048Mi) % 280.11/39.77 % (1662839)Instruction limit reached! % 280.11/39.77 % (1662839)------------------------------ % 280.11/39.77 % (1662839)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 280.11/39.77 % (1662839)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 280.11/39.77 % (1662839)CaDiCaL version: 2.1.3 % 280.11/39.77 % (1662839)Termination reason: Instruction limit % 280.11/39.77 % (1662839)Termination phase: Saturation % 280.11/39.77 % (1662839)Time elapsed: 10.454 s % 280.11/39.77 % (1662839)Peak memory usage: 80 MB % 280.11/39.77 % (1662839)Instructions burned: 17628 (million) % 280.11/39.77 % (1662916)dis+10_1_sil=32000:si=on:sp=arity:random_seed=3398374423:i=206:fgj=on:rtra=on_2650 on theBenchmark for (2650ds/206Mi) % 280.11/39.77 % (1662916)Instruction limit reached! % 280.11/39.77 % (1662916)------------------------------ % 280.11/39.77 % (1662916)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 280.11/39.77 % (1662916)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 280.11/39.77 % (1662916)CaDiCaL version: 2.1.3 % 280.11/39.77 % (1662916)Termination reason: Instruction limit % 280.11/39.77 % (1662916)Termination phase: Saturation % 280.11/39.77 % (1662916)Time elapsed: 0.124 s % 280.11/39.77 % (1662916)Peak memory usage: 13 MB % 280.11/39.77 % (1662916)Instructions burned: 206 (million) % 280.11/39.77 % (1662918)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=4190243114:i=232:rtra=on_2648 on theBenchmark for (2648ds/232Mi) % 280.11/39.77 % (1662918)Instruction limit reached! % 280.11/39.77 % (1662918)------------------------------ % 280.11/39.77 % (1662918)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 280.11/39.77 % (1662918)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 280.11/39.77 % (1662918)CaDiCaL version: 2.1.3 % 280.11/39.77 % (1662918)Termination reason: Instruction limit % 280.11/39.77 % (1662918)Termination phase: Saturation % 280.11/39.77 % (1662918)Time elapsed: 0.145 s % 280.11/39.77 % (1662918)Peak memory usage: 13 MB % 280.11/39.77 % (1662918)Instructions burned: 232 (million) % 280.11/39.77 % (1662920)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=825552924:i=262:rtra=on_2646 on theBenchmark for (2646ds/262Mi) % 280.11/39.77 % (1662920)Instruction limit reached! % 280.11/39.77 % (1662920)------------------------------ % 280.11/39.77 % (1662920)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 280.11/39.77 % (1662920)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 280.11/39.77 % (1662920)CaDiCaL version: 2.1.3 % 280.11/39.77 % (1662920)Termination reason: Instruction limit % 280.11/39.77 % (1662920)Termination phase: Saturation % 280.11/39.77 % (1662920)Time elapsed: 0.132 s % 280.11/39.77 % (1662920)Peak memory usage: 13 MB % 280.11/39.77 % (1662920)Instructions burned: 264 (million) % 280.11/39.77 % (1662922)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=2193358244:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2645 on theBenchmark for (2645ds/318Mi) % 280.11/39.77 % (1662922)Instruction limit reached! % 280.11/39.77 % (1662922)------------------------------ % 280.11/39.77 % (1662922)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 280.11/39.77 % (1662922)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 280.11/39.77 % (1662922)CaDiCaL version: 2.1.3 % 280.11/39.77 % (1662922)Termination reason: Instruction limit % 280.11/39.77 % (1662922)Termination phase: Saturation % 280.11/39.77 % (1662922)Time elapsed: 0.217 s % 280.11/39.77 % (1662922)Peak memory usage: 16 MB % 280.11/39.77 % (1662922)Instructions burned: 319 (million) % 280.11/39.77 % (1662924)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=3737114286:i=1428:nm=2:rtra=on_2643 on theBenchmark for (2643ds/1428Mi) % 297.91/42.23 % (1662924)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 297.91/42.23 % (1662924)Terminated due to inappropriate strategy. % 297.91/42.23 % (1662924)------------------------------ % 297.91/42.23 % (1662924)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 297.91/42.23 % (1662924)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 297.91/42.23 % (1662924)CaDiCaL version: 2.1.3 % 297.91/42.23 % (1662924)Termination reason: Inappropriate % 297.91/42.23 % (1662924)Time elapsed: 0.001 s % 297.91/42.23 % (1662924)Peak memory usage: 10 MB % 297.91/42.23 % (1662924)Instructions burned: 1 (million) % 297.91/42.23 % (1662924)------------------------------ % 297.91/42.23 % (1662924)------------------------------ % 297.91/42.23 % (1662926)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=3148568493:i=262:bd=preordered:rtra=on:fsd=on_2642 on theBenchmark for (2642ds/262Mi) % 297.91/42.23 % (1662926)Instruction limit reached! % 297.91/42.23 % (1662926)------------------------------ % 297.91/42.23 % (1662926)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 297.91/42.23 % (1662926)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 297.91/42.23 % (1662926)CaDiCaL version: 2.1.3 % 297.91/42.23 % (1662926)Termination reason: Instruction limit % 297.91/42.23 % (1662926)Termination phase: Saturation % 297.91/42.23 % (1662926)Time elapsed: 0.176 s % 297.91/42.23 % (1662926)Peak memory usage: 14 MB % 297.91/42.23 % (1662926)Instructions burned: 264 (million) % 297.91/42.23 % (1662928)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=3077425821:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2640 on theBenchmark for (2640ds/1368Mi) % 297.91/42.23 % (1662928)Instruction limit reached! % 297.91/42.23 % (1662928)------------------------------ % 297.91/42.23 % (1662928)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 297.91/42.23 % (1662928)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 297.91/42.23 % (1662928)CaDiCaL version: 2.1.3 % 297.91/42.23 % (1662928)Termination reason: Instruction limit % 297.91/42.23 % (1662928)Termination phase: Saturation % 297.91/42.23 % (1662928)Time elapsed: 0.725 s % 297.91/42.23 % (1662928)Peak memory usage: 23 MB % 297.91/42.23 % (1662928)Instructions burned: 1368 (million) % 297.91/42.23 % (1662930)ott-21_1_sil=16000:si=on:fs=off:random_seed=1273244578:i=360:av=off:fsr=off:rtra=on_2633 on theBenchmark for (2633ds/360Mi) % 297.91/42.23 % (1662930)Instruction limit reached! % 297.91/42.23 % (1662930)------------------------------ % 297.91/42.23 % (1662930)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 297.91/42.23 % (1662930)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 297.91/42.23 % (1662930)CaDiCaL version: 2.1.3 % 297.91/42.23 % (1662930)Termination reason: Instruction limit % 297.91/42.23 % (1662930)Termination phase: Saturation % 297.91/42.23 % (1662930)Time elapsed: 0.160 s % 297.91/42.23 % (1662930)Peak memory usage: 13 MB % 297.91/42.23 % (1662930)Instructions burned: 360 (million) % 297.91/42.23 % (1662932)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3117674086:i=954:bd=all:rtra=on_2631 on theBenchmark for (2631ds/954Mi) % 297.91/42.23 % (1662932)Instruction limit reached! % 297.91/42.23 % (1662932)------------------------------ % 297.91/42.23 % (1662932)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 297.91/42.23 % (1662932)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 297.91/42.23 % (1662932)CaDiCaL version: 2.1.3 % 297.91/42.23 % (1662932)Termination reason: Instruction limit % 297.91/42.23 % (1662932)Termination phase: Saturation % 297.91/42.23 % (1662932)Time elapsed: 0.612 s % 297.91/42.23 % (1662932)Peak memory usage: 16 MB % 297.91/42.23 % (1662932)Instructions burned: 955 (million) % 297.91/42.23 % (1662934)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=1480324110:fmbsr=1.3:i=1730:ins=25:rtra=on_2625 on theBenchmark for (2625ds/1730Mi) % 297.91/42.23 % (1662934)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 297.91/42.23 % (1662934)Terminated due to inappropriate strategy. % 297.91/42.23 % (1662934)------------------------------ % 297.91/42.23 % (1662934)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 297.91/42.23 % (1662934)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 297.91/42.23 % (1662934)CaDiCaL version: 2.1.3 % 297.91/42.23 % (1662934)Termination reason: InappropriatTerminated % 300.42/42.64 % Vampire exiting %------------------------------------------------------------------------------