%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : PRO032_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 12:30:43 PM UTC 2026 % Result : Timeout 300.15s 42.74s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : PRO032_1 : TPTP v9.3.1. Released v9.0.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.09/0.37 % Computer : n014.cluster.edu % 0.09/0.37 % Model : x86_64 x86_64 % 0.09/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.37 % Memory : 8046.5625MB % 0.09/0.37 % OS : Linux 6.8.0-71-generic % 0.09/0.37 % CPULimit : 300 % 0.09/0.37 % WCLimit : 300 % 0.09/0.37 % DateTime : Sun Sep 27 22:26:46 UTC 2026 % 0.09/0.37 % CPUTime : % 0.09/0.37 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.09/0.40 Running first-order model finding % 0.09/0.40 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 % 2.66/0.91 % (1228113)Will run a generic schedule for satisfiability detection. % 2.66/0.91 % (1228118)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2439887851_2999 on theBenchmark for (2999ds/0Mi) % 2.66/0.91 % (1228118)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 2.66/0.91 % (1228118)Terminated due to inappropriate strategy. % 2.66/0.91 % (1228118)------------------------------ % 2.66/0.91 % (1228118)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 2.66/0.91 % (1228118)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 2.66/0.91 % (1228118)CaDiCaL version: 2.1.3 % 2.66/0.91 % (1228118)Termination reason: Inappropriate % 2.66/0.91 % (1228118)Time elapsed: 0.0000 s % 2.66/0.91 % (1228118)Peak memory usage: 10 MB % 2.66/0.91 % (1228118)------------------------------ % 2.66/0.91 % (1228118)------------------------------ % 2.66/0.91 % (1228120)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2355384364:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 2.66/0.91 % (1228121)dis+10_1_sil=32000:sp=arity:random_seed=3184966200:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 2.66/0.91 % (1228122)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1329666903:i=116_2999 on theBenchmark for (2999ds/116Mi) % 2.66/0.91 % (1228123)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2260515284:i=131_2999 on theBenchmark for (2999ds/131Mi) % 2.66/0.91 % (1228124)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2779219689:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 2.66/0.91 % (1228119)% WARNING: option uhcvi not known. % 2.66/0.91 % (1228119)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=26609291:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 2.66/0.91 % (1228126)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=505702583:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 2.66/0.91 % (1228126)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 2.66/0.91 % (1228126)Terminated due to inappropriate strategy. % 2.66/0.91 % (1228126)------------------------------ % 2.66/0.91 % (1228126)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 2.66/0.91 % (1228126)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 2.66/0.91 % (1228126)CaDiCaL version: 2.1.3 % 2.66/0.91 % (1228126)Termination reason: Inappropriate % 2.66/0.91 % (1228126)Time elapsed: 0.0000 s % 2.66/0.91 % (1228126)Peak memory usage: 10 MB % 2.66/0.91 % (1228126)------------------------------ % 2.66/0.91 % (1228126)------------------------------ % 2.66/0.91 % (1228134)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2288413829:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 2.66/0.91 % (1228121)Instruction limit reached! % 2.66/0.91 % (1228121)------------------------------ % 2.66/0.91 % (1228121)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 2.66/0.91 % (1228121)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 2.66/0.91 % (1228121)CaDiCaL version: 2.1.3 % 2.66/0.91 % (1228121)Termination reason: Instruction limit % 2.66/0.91 % (1228121)Termination phase: Saturation % 2.66/0.91 % (1228121)Time elapsed: 0.066 s % 2.66/0.91 % (1228121)Peak memory usage: 12 MB % 2.66/0.91 % (1228121)Instructions burned: 104 (million) % 2.66/0.91 % (1228134)Instruction limit reached! % 2.66/0.91 % (1228134)------------------------------ % 2.66/0.91 % (1228134)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 2.66/0.91 % (1228134)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 2.66/0.91 % (1228134)CaDiCaL version: 2.1.3 % 2.66/0.91 % (1228134)Termination reason: Instruction limit % 2.66/0.91 % (1228134)Termination phase: Saturation % 2.66/0.91 % (1228134)Time elapsed: 0.048 s % 2.66/0.91 % (1228134)Peak memory usage: 13 MB % 2.66/0.91 % (1228134)Instructions burned: 133 (million) % 2.66/0.91 % (1228122)Instruction limit reached! % 2.66/0.91 % (1228122)------------------------------ % 2.66/0.91 % (1228122)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 2.66/0.91 % (1228122)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 2.66/0.91 % (1228122)CaDiCaL version: 2.1.3 % 2.66/0.91 % (1228122)Termination reason: Instruction limit % 2.66/0.91 % (1228122)Termination phase: Saturation % 2.66/0.91 % (1228122)Time elapsed: 0.071 s % 7.07/1.51 % (1228122)Peak memory usage: 12 MB % 7.07/1.51 % (1228122)Instructions burned: 117 (million) % 7.07/1.51 % (1228137)ott-21_1_sil=16000:fs=off:random_seed=1079903558:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi) % 7.07/1.51 % (1228123)Instruction limit reached! % 7.07/1.51 % (1228123)------------------------------ % 7.07/1.51 % (1228123)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.07/1.51 % (1228123)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.07/1.51 % (1228123)CaDiCaL version: 2.1.3 % 7.07/1.51 % (1228123)Termination reason: Instruction limit % 7.07/1.51 % (1228123)Termination phase: Saturation % 7.07/1.51 % (1228123)Time elapsed: 0.081 s % 7.07/1.51 % (1228123)Peak memory usage: 12 MB % 7.07/1.51 % (1228123)Instructions burned: 131 (million) % 7.07/1.51 % (1228136)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=1150898874:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi) % 7.07/1.51 % (1228138)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=299156957:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 7.07/1.51 % (1228124)Instruction limit reached! % 7.07/1.51 % (1228124)------------------------------ % 7.07/1.51 % (1228124)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.07/1.51 % (1228124)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.07/1.51 % (1228124)CaDiCaL version: 2.1.3 % 7.07/1.51 % (1228124)Termination reason: Instruction limit % 7.07/1.51 % (1228124)Termination phase: Saturation % 7.07/1.51 % (1228124)Time elapsed: 0.100 s % 7.07/1.51 % (1228124)Peak memory usage: 13 MB % 7.07/1.51 % (1228124)Instructions burned: 160 (million) % 7.07/1.51 % (1228140)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2711758297:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 7.07/1.51 % (1228140)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 7.07/1.51 % (1228140)Terminated due to inappropriate strategy. % 7.07/1.51 % (1228140)------------------------------ % 7.07/1.51 % (1228140)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.07/1.51 % (1228140)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.07/1.51 % (1228140)CaDiCaL version: 2.1.3 % 7.07/1.51 % (1228140)Termination reason: Inappropriate % 7.07/1.51 % (1228140)Time elapsed: 0.0000 s % 7.07/1.51 % (1228140)Peak memory usage: 10 MB % 7.07/1.51 % (1228140)------------------------------ % 7.07/1.51 % (1228140)------------------------------ % 7.07/1.51 % (1228137)Instruction limit reached! % 7.07/1.51 % (1228137)------------------------------ % 7.07/1.51 % (1228137)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.07/1.51 % (1228137)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.07/1.51 % (1228137)CaDiCaL version: 2.1.3 % 7.07/1.51 % (1228137)Termination reason: Instruction limit % 7.07/1.51 % (1228137)Termination phase: Saturation % 7.07/1.51 % (1228137)Time elapsed: 0.042 s % 7.07/1.51 % (1228137)Peak memory usage: 12 MB % 7.07/1.51 % (1228137)Instructions burned: 181 (million) % 7.07/1.51 % (1228144)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1713659478:i=1179_2998 on theBenchmark for (2998ds/1179Mi) % 7.07/1.51 % (1228145)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2605335168:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi) % 7.07/1.51 % (1228145)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 7.07/1.51 % (1228145)Terminated due to inappropriate strategy. % 7.07/1.51 % (1228145)------------------------------ % 7.07/1.51 % (1228145)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.07/1.51 % (1228145)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.07/1.51 % (1228145)CaDiCaL version: 2.1.3 % 7.07/1.51 % (1228145)Termination reason: Inappropriate % 7.07/1.51 % (1228145)Time elapsed: 0.0000 s % 7.07/1.51 % (1228145)Peak memory usage: 10 MB % 7.07/1.51 % (1228145)------------------------------ % 7.07/1.51 % (1228145)------------------------------ % 7.07/1.51 % (1228147)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=71988174:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2998 on theBenchmark for (2998ds/692Mi) % 7.07/1.51 % (1228149)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2939756877:i=879:kws=inv_precedence:fsr=off_2998 on theBenchmark for (2998ds/879Mi) % 21.54/3.54 % (1228147)Instruction limit reached! % 21.54/3.54 % (1228147)------------------------------ % 21.54/3.54 % (1228147)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 21.54/3.54 % (1228147)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.54/3.54 % (1228147)CaDiCaL version: 2.1.3 % 21.54/3.54 % (1228147)Termination reason: Instruction limit % 21.54/3.54 % (1228147)Termination phase: Saturation % 21.54/3.54 % (1228147)Time elapsed: 0.213 s % 21.54/3.54 % (1228147)Peak memory usage: 16 MB % 21.54/3.54 % (1228147)Instructions burned: 693 (million) % 21.54/3.54 % (1228152)fmb+10_1_sil=64000:random_seed=4228106467:i=22061:nm=2:gsp=on_2996 on theBenchmark for (2996ds/22061Mi) % 21.54/3.54 % (1228152)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 21.54/3.54 % (1228152)Terminated due to inappropriate strategy. % 21.54/3.54 % (1228152)------------------------------ % 21.54/3.54 % (1228152)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 21.54/3.55 % (1228152)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.54/3.55 % (1228152)CaDiCaL version: 2.1.3 % 21.54/3.55 % (1228152)Termination reason: Inappropriate % 21.54/3.55 % (1228152)Time elapsed: 0.0000 s % 21.54/3.55 % (1228152)Peak memory usage: 10 MB % 21.54/3.55 % (1228152)------------------------------ % 21.54/3.55 % (1228152)------------------------------ % 21.54/3.55 % (1228154)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1366796273:i=9515:nm=5_2996 on theBenchmark for (2996ds/9515Mi) % 21.54/3.55 % (1228154)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 21.54/3.55 % (1228154)Terminated due to inappropriate strategy. % 21.54/3.55 % (1228154)------------------------------ % 21.54/3.55 % (1228154)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 21.54/3.55 % (1228154)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.54/3.55 % (1228154)CaDiCaL version: 2.1.3 % 21.54/3.55 % (1228154)Termination reason: Inappropriate % 21.54/3.55 % (1228154)Time elapsed: 0.0000 s % 21.54/3.55 % (1228154)Peak memory usage: 10 MB % 21.54/3.55 % (1228154)------------------------------ % 21.54/3.55 % (1228154)------------------------------ % 21.54/3.55 % (1228156)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=4294224880:fmbsr=1.7:i=920_2996 on theBenchmark for (2996ds/920Mi) % 21.54/3.55 % (1228156)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 21.54/3.55 % (1228156)Terminated due to inappropriate strategy. % 21.54/3.55 % (1228156)------------------------------ % 21.54/3.55 % (1228156)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 21.54/3.55 % (1228156)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.54/3.55 % (1228156)CaDiCaL version: 2.1.3 % 21.54/3.55 % (1228156)Termination reason: Inappropriate % 21.54/3.55 % (1228156)Time elapsed: 0.0000 s % 21.54/3.55 % (1228156)Peak memory usage: 10 MB % 21.54/3.55 % (1228156)------------------------------ % 21.54/3.55 % (1228156)------------------------------ % 21.54/3.55 % (1228138)Instruction limit reached! % 21.54/3.55 % (1228138)------------------------------ % 21.54/3.55 % (1228138)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 21.54/3.55 % (1228138)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.54/3.55 % (1228138)CaDiCaL version: 2.1.3 % 21.54/3.55 % (1228138)Termination reason: Instruction limit % 21.54/3.55 % (1228138)Termination phase: Saturation % 21.54/3.55 % (1228138)Time elapsed: 0.297 s % 21.54/3.55 % (1228138)Peak memory usage: 14 MB % 21.54/3.55 % (1228138)Instructions burned: 477 (million) % 21.54/3.55 % (1228158)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=3927742085:i=5131_2995 on theBenchmark for (2995ds/5131Mi) % 21.54/3.55 % (1228159)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2478069416:i=1472:ins=7:fdi=8:gsp=on_2995 on theBenchmark for (2995ds/1472Mi) % 21.54/3.55 % (1228136)Instruction limit reached! % 21.54/3.55 % (1228136)------------------------------ % 21.54/3.55 % (1228136)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 21.54/3.55 % (1228136)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.54/3.55 % (1228136)CaDiCaL version: 2.1.3 % 21.54/3.55 % (1228136)Termination reason: Instruction limit % 26.87/4.27 % (1228136)Termination phase: Saturation % 26.87/4.27 % (1228136)Time elapsed: 0.380 s % 26.87/4.27 % (1228136)Peak memory usage: 18 MB % 26.87/4.27 % (1228136)Instructions burned: 685 (million) % 26.87/4.27 % (1228162)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=2809178414:i=6324_2995 on theBenchmark for (2995ds/6324Mi) % 26.87/4.27 % (1228162)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 26.87/4.27 % (1228162)Terminated due to inappropriate strategy. % 26.87/4.27 % (1228162)------------------------------ % 26.87/4.27 % (1228162)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 26.87/4.27 % (1228162)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.87/4.27 % (1228162)CaDiCaL version: 2.1.3 % 26.87/4.27 % (1228162)Termination reason: Inappropriate % 26.87/4.27 % (1228162)Time elapsed: 0.0000 s % 26.87/4.27 % (1228162)Peak memory usage: 10 MB % 26.87/4.27 % (1228162)------------------------------ % 26.87/4.27 % (1228162)------------------------------ % 26.87/4.27 % (1228164)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=3966237009:fmbsr=2.30978:i=2174_2994 on theBenchmark for (2994ds/2174Mi) % 26.87/4.27 % (1228164)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 26.87/4.27 % (1228164)Terminated due to inappropriate strategy. % 26.87/4.27 % (1228164)------------------------------ % 26.87/4.27 % (1228164)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 26.87/4.27 % (1228164)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.87/4.27 % (1228164)CaDiCaL version: 2.1.3 % 26.87/4.27 % (1228164)Termination reason: Inappropriate % 26.87/4.27 % (1228164)Time elapsed: 0.0000 s % 26.87/4.27 % (1228164)Peak memory usage: 10 MB % 26.87/4.27 % (1228164)------------------------------ % 26.87/4.27 % (1228164)------------------------------ % 26.87/4.27 % (1228166)ott-2_1_sil=16000:newcnf=on:random_seed=3303101864:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2994 on theBenchmark for (2994ds/869Mi) % 26.87/4.27 % (1228149)Instruction limit reached! % 26.87/4.27 % (1228149)------------------------------ % 26.87/4.27 % (1228149)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 26.87/4.27 % (1228149)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.87/4.27 % (1228149)CaDiCaL version: 2.1.3 % 26.87/4.27 % (1228149)Termination reason: Instruction limit % 26.87/4.27 % (1228149)Termination phase: Saturation % 26.87/4.27 % (1228149)Time elapsed: 0.501 s % 26.87/4.27 % (1228149)Peak memory usage: 19 MB % 26.87/4.27 % (1228149)Instructions burned: 879 (million) % 26.87/4.27 % (1228168)ott+10_1_sil=32000:tgt=ground:random_seed=137557619:i=5114:av=off_2993 on theBenchmark for (2993ds/5114Mi) % 26.87/4.27 % (1228144)Instruction limit reached! % 26.87/4.27 % (1228144)------------------------------ % 26.87/4.27 % (1228144)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 26.87/4.27 % (1228144)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.87/4.27 % (1228144)CaDiCaL version: 2.1.3 % 26.87/4.27 % (1228144)Termination reason: Instruction limit % 26.87/4.27 % (1228144)Termination phase: Saturation % 26.87/4.27 % (1228144)Time elapsed: 0.699 s % 26.87/4.27 % (1228144)Peak memory usage: 17 MB % 26.87/4.27 % (1228144)Instructions burned: 1179 (million) % 26.87/4.27 % (1228170)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=3803334048:i=54282_2991 on theBenchmark for (2991ds/54282Mi) % 26.87/4.27 % (1228170)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 26.87/4.27 % (1228170)Terminated due to inappropriate strategy. % 26.87/4.27 % (1228170)------------------------------ % 26.87/4.27 % (1228170)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 26.87/4.27 % (1228170)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.87/4.27 % (1228170)CaDiCaL version: 2.1.3 % 26.87/4.27 % (1228170)Termination reason: Inappropriate % 26.87/4.27 % (1228170)Time elapsed: 0.0000 s % 26.87/4.27 % (1228170)Peak memory usage: 10 MB % 26.87/4.27 % (1228170)------------------------------ % 26.87/4.27 % (1228170)------------------------------ % 26.87/4.27 % (1228172)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=1839588766:i=3512:aac=none_2991 on theBenchmark for (2991ds/3512Mi) % 26.87/4.27 % (1228166)Instruction limit reached! % 26.87/4.27 % (1228166)------------------------------ % 26.87/4.27 % (1228166)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 26.87/4.27 % (1228166)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 106.37/15.49 % (1228166)CaDiCaL version: 2.1.3 % 106.37/15.49 % (1228166)Termination reason: Instruction limit % 106.37/15.49 % (1228166)Termination phase: Saturation % 106.37/15.49 % (1228166)Time elapsed: 0.534 s % 106.37/15.49 % (1228166)Peak memory usage: 16 MB % 106.37/15.49 % (1228166)Instructions burned: 869 (million) % 106.37/15.49 % (1228174)dis+21_1_sil=32000:sas=cadical:random_seed=2776191660:i=3773:amm=off_2989 on theBenchmark for (2989ds/3773Mi) % 106.37/15.49 % (1228159)Instruction limit reached! % 106.37/15.49 % (1228159)------------------------------ % 106.37/15.49 % (1228159)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 106.37/15.49 % (1228159)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 106.37/15.49 % (1228159)CaDiCaL version: 2.1.3 % 106.37/15.49 % (1228159)Termination reason: Instruction limit % 106.37/15.49 % (1228159)Termination phase: Saturation % 106.37/15.49 % (1228159)Time elapsed: 0.696 s % 106.37/15.49 % (1228159)Peak memory usage: 26 MB % 106.37/15.49 % (1228159)Instructions burned: 1474 (million) % 106.37/15.49 % (1228176)ott+11_1_sil=16000:gs=on:random_seed=3569669404:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2988 on theBenchmark for (2988ds/2251Mi) % 106.37/15.49 % (1228158)Instruction limit reached! % 106.37/15.49 % (1228158)------------------------------ % 106.37/15.49 % (1228158)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 106.37/15.49 % (1228158)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 106.37/15.49 % (1228158)CaDiCaL version: 2.1.3 % 106.37/15.49 % (1228158)Termination reason: Instruction limit % 106.37/15.49 % (1228158)Termination phase: Saturation % 106.37/15.49 % (1228158)Time elapsed: 1.423 s % 106.37/15.49 % (1228158)Peak memory usage: 40 MB % 106.37/15.49 % (1228158)Instructions burned: 5131 (million) % 106.37/15.49 % (1228178)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=1690379487:fmbsr=1.6:i=67534_2981 on theBenchmark for (2981ds/67534Mi) % 106.37/15.49 % (1228178)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 106.37/15.49 % (1228178)Terminated due to inappropriate strategy. % 106.37/15.49 % (1228178)------------------------------ % 106.37/15.49 % (1228178)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 106.37/15.49 % (1228178)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 106.37/15.49 % (1228178)CaDiCaL version: 2.1.3 % 106.37/15.49 % (1228178)Termination reason: Inappropriate % 106.37/15.49 % (1228178)Time elapsed: 0.0000 s % 106.37/15.49 % (1228178)Peak memory usage: 10 MB % 106.37/15.49 % (1228178)------------------------------ % 106.37/15.49 % (1228178)------------------------------ % 106.37/15.49 % (1228180)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=4162910030:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2981 on theBenchmark for (2981ds/4591Mi) % 106.37/15.49 % (1228176)Instruction limit reached! % 106.37/15.49 % (1228176)------------------------------ % 106.37/15.49 % (1228176)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 106.37/15.49 % (1228176)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 106.37/15.49 % (1228176)CaDiCaL version: 2.1.3 % 106.37/15.49 % (1228176)Termination reason: Instruction limit % 106.37/15.49 % (1228176)Termination phase: Saturation % 106.37/15.49 % (1228176)Time elapsed: 1.221 s % 106.37/15.49 % (1228176)Peak memory usage: 21 MB % 106.37/15.49 % (1228176)Instructions burned: 2251 (million) % 106.37/15.49 % (1228182)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=2936483197:i=29340_2976 on theBenchmark for (2976ds/29340Mi) % 106.37/15.49 % (1228172)Instruction limit reached! % 106.37/15.49 % (1228172)------------------------------ % 106.37/15.49 % (1228172)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 106.37/15.49 % (1228172)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 106.37/15.49 % (1228172)CaDiCaL version: 2.1.3 % 106.37/15.49 % (1228172)Termination reason: Instruction limit % 106.37/15.49 % (1228172)Termination phase: Saturation % 106.37/15.49 % (1228172)Time elapsed: 1.834 s % 106.37/15.49 % (1228172)Peak memory usage: 29 MB % 106.37/15.49 % (1228172)Instructions burned: 3513 (million) % 106.37/15.49 % (1228184)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=1747618440:i=5211_2972 on theBenchmark for (2972ds/5211Mi) % 106.37/15.49 % (1228174)Instruction limit reached! % 106.37/15.49 % (1228174)------------------------------ % 106.37/15.49 % (1228174)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 106.38/17.57 % (1228174)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 106.38/17.57 % (1228174)CaDiCaL version: 2.1.3 % 106.38/17.57 % (1228174)Termination reason: Instruction limit % 106.38/17.57 % (1228174)Termination phase: Saturation % 106.38/17.57 % (1228174)Time elapsed: 2.018 s % 106.38/17.57 % (1228174)Peak memory usage: 29 MB % 106.38/17.57 % (1228174)Instructions burned: 3774 (million) % 106.38/17.57 % (1228186)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=2310358362:i=5497:nm=2_2968 on theBenchmark for (2968ds/5497Mi) % 106.38/17.57 % (1228186)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 106.38/17.57 % (1228186)Terminated due to inappropriate strategy. % 106.38/17.57 % (1228186)------------------------------ % 106.38/17.57 % (1228186)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 106.38/17.57 % (1228186)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 106.38/17.57 % (1228186)CaDiCaL version: 2.1.3 % 106.38/17.57 % (1228186)Termination reason: Inappropriate % 106.38/17.57 % (1228186)Time elapsed: 0.0000 s % 106.38/17.57 % (1228186)Peak memory usage: 10 MB % 106.38/17.57 % (1228186)------------------------------ % 106.38/17.57 % (1228186)------------------------------ % 106.38/17.57 % (1228188)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=610123075:fmbsr=2:i=46332_2968 on theBenchmark for (2968ds/46332Mi) % 106.38/17.57 % (1228188)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 106.38/17.57 % (1228188)Terminated due to inappropriate strategy. % 106.38/17.57 % (1228188)------------------------------ % 106.38/17.57 % (1228188)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 106.38/17.57 % (1228188)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 106.38/17.57 % (1228188)CaDiCaL version: 2.1.3 % 106.38/17.57 % (1228188)Termination reason: Inappropriate % 106.38/17.57 % (1228188)Time elapsed: 0.0000 s % 106.38/17.57 % (1228188)Peak memory usage: 10 MB % 106.38/17.57 % (1228188)------------------------------ % 106.38/17.57 % (1228188)------------------------------ % 106.38/17.57 % (1228190)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=4081605943:i=14071_2968 on theBenchmark for (2968ds/14071Mi) % 106.38/17.57 % (1228190)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 106.38/17.57 % (1228190)Terminated due to inappropriate strategy. % 106.38/17.57 % (1228190)------------------------------ % 106.38/17.57 % (1228190)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 106.38/17.57 % (1228190)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 106.38/17.57 % (1228190)CaDiCaL version: 2.1.3 % 106.38/17.57 % (1228190)Termination reason: Inappropriate % 106.38/17.57 % (1228190)Time elapsed: 0.0000 s % 106.38/17.57 % (1228190)Peak memory usage: 10 MB % 106.38/17.57 % (1228190)------------------------------ % 106.38/17.57 % (1228190)------------------------------ % 106.38/17.57 % (1228192)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2518898556:i=22565:add=on:rawr=on_2968 on theBenchmark for (2968ds/22565Mi) % 106.38/17.57 % (1228180)Instruction limit reached! % 106.38/17.57 % (1228180)------------------------------ % 106.38/17.57 % (1228180)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 106.38/17.57 % (1228180)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 106.38/17.57 % (1228180)CaDiCaL version: 2.1.3 % 106.38/17.57 % (1228180)Termination reason: Instruction limit % 106.38/17.57 % (1228180)Termination phase: Saturation % 106.38/17.57 % (1228180)Time elapsed: 1.461 s % 106.38/17.57 % (1228180)Peak memory usage: 41 MB % 106.38/17.57 % (1228180)Instructions burned: 4592 (million) % 106.38/17.57 % (1228194)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=3173417556:i=8173:av=off_2966 on theBenchmark for (2966ds/8173Mi) % 106.38/17.57 % (1228168)Instruction limit reached! % 106.38/17.57 % (1228168)------------------------------ % 106.38/17.57 % (1228168)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 106.38/17.57 % (1228168)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 106.38/17.57 % (1228168)CaDiCaL version: 2.1.3 % 106.38/17.57 % (1228168)Termination reason: Instruction limit % 106.38/17.57 % (1228168)Termination phase: Saturation % 106.38/17.57 % (1228168)Time elapsed: 3.138 s % 106.38/17.57 % (1228168)Peak memory usage: 28 MB % 106.38/17.57 % (1228168)Instructions burned: 5115 (million) % 106.38/17.57 % (1228196)dis+10_16:1_sil=16000:random_seed=153822224:i=9155:fsr=off_2961 on theBenchmark for (2961ds/9155Mi) % 130.47/19.03 % (1228184)Instruction limit reached! % 130.47/19.03 % (1228184)------------------------------ % 130.47/19.03 % (1228184)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 130.47/19.03 % (1228184)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 130.47/19.03 % (1228184)CaDiCaL version: 2.1.3 % 130.47/19.03 % (1228184)Termination reason: Instruction limit % 130.47/19.03 % (1228184)Termination phase: Saturation % 130.47/19.03 % (1228184)Time elapsed: 2.804 s % 130.47/19.03 % (1228184)Peak memory usage: 45 MB % 130.47/19.03 % (1228184)Instructions burned: 5213 (million) % 130.47/19.03 % (1228198)ott-3_8_sil=64000:random_seed=2540115358:i=20139:bs=on_2944 on theBenchmark for (2944ds/20139Mi) % 130.47/19.03 % (1228194)Instruction limit reached! % 130.47/19.03 % (1228194)------------------------------ % 130.47/19.03 % (1228194)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 130.47/19.03 % (1228194)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 130.47/19.03 % (1228194)CaDiCaL version: 2.1.3 % 130.47/19.03 % (1228194)Termination reason: Instruction limit % 130.47/19.03 % (1228194)Termination phase: Saturation % 130.47/19.03 % (1228194)Time elapsed: 2.779 s % 130.47/19.03 % (1228194)Peak memory usage: 44 MB % 130.47/19.03 % (1228194)Instructions burned: 8173 (million) % 130.47/19.03 % (1228200)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=2251482509:fmbsr=2:i=32576_2938 on theBenchmark for (2938ds/32576Mi) % 130.47/19.03 % (1228200)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 130.47/19.03 % (1228200)Terminated due to inappropriate strategy. % 130.47/19.03 % (1228200)------------------------------ % 130.47/19.03 % (1228200)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 130.47/19.03 % (1228200)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 130.47/19.03 % (1228200)CaDiCaL version: 2.1.3 % 130.47/19.03 % (1228200)Termination reason: Inappropriate % 130.47/19.03 % (1228200)Time elapsed: 0.0000 s % 130.47/19.03 % (1228200)Peak memory usage: 10 MB % 130.47/19.03 % (1228200)------------------------------ % 130.47/19.03 % (1228200)------------------------------ % 130.47/19.03 % (1228202)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=3767005484:i=11404_2938 on theBenchmark for (2938ds/11404Mi) % 130.47/19.03 % (1228196)Instruction limit reached! % 130.47/19.03 % (1228196)------------------------------ % 130.47/19.03 % (1228196)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 130.47/19.03 % (1228196)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 130.47/19.03 % (1228196)CaDiCaL version: 2.1.3 % 130.47/19.03 % (1228196)Termination reason: Instruction limit % 130.47/19.03 % (1228196)Termination phase: Saturation % 130.47/19.03 % (1228196)Time elapsed: 4.743 s % 130.47/19.03 % (1228196)Peak memory usage: 50 MB % 130.47/19.03 % (1228196)Instructions burned: 9157 (million) % 130.47/19.03 % (1228204)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=2566946483:i=14134_2913 on theBenchmark for (2913ds/14134Mi) % 130.47/19.03 % (1228202)Instruction limit reached! % 130.47/19.03 % (1228202)------------------------------ % 130.47/19.03 % (1228202)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 130.47/19.03 % (1228202)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 130.47/19.03 % (1228202)CaDiCaL version: 2.1.3 % 130.47/19.03 % (1228202)Termination reason: Instruction limit % 130.47/19.03 % (1228202)Termination phase: Saturation % 130.47/19.03 % (1228202)Time elapsed: 4.017 s % 130.47/19.03 % (1228202)Peak memory usage: 44 MB % 130.47/19.03 % (1228202)Instructions burned: 11406 (million) % 130.47/19.03 % (1228206)dis+33_16_sil=32000:sac=on:random_seed=1481943247:i=15851:nm=0_2898 on theBenchmark for (2898ds/15851Mi) % 130.47/19.03 % (1228206)Instruction limit reached! % 130.47/19.03 % (1228206)------------------------------ % 130.47/19.03 % (1228206)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 130.47/19.03 % (1228206)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 130.47/19.03 % (1228206)CaDiCaL version: 2.1.3 % 130.47/19.03 % (1228206)Termination reason: Instruction limit % 130.47/19.03 % (1228206)Termination phase: Saturation % 130.47/19.03 % (1228206)Time elapsed: 3.573 s % 130.47/19.03 % (1228206)Peak memory usage: 25 MB % 130.47/19.03 % (1228206)Instructions burned: 15853 (million) % 130.47/19.03 % (1228208)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=1972127520:avsq=on:i=17627:add=on:amm=off_2862 on theBenchmark for (2862ds/17627Mi) % 130.47/19.03 % (1228198)Instruction limit reached! % 130.47/19.03 % (1228198)------------------------------ % 135.41/19.55 % (1228198)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 135.41/19.55 % (1228198)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 135.41/19.55 % (1228198)CaDiCaL version: 2.1.3 % 135.41/19.55 % (1228198)Termination reason: Instruction limit % 135.41/19.55 % (1228198)Termination phase: Saturation % 135.41/19.55 % (1228198)Time elapsed: 9.502 s % 135.41/19.55 % (1228198)Peak memory usage: 42 MB % 135.41/19.55 % (1228198)Instructions burned: 20140 (million) % 135.41/19.55 % (1228210)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=109376752:s2a=on:i=53295_2849 on theBenchmark for (2849ds/53295Mi) % 135.41/19.55 % (1228192)Instruction limit reached! % 135.41/19.55 % (1228192)------------------------------ % 135.41/19.55 % (1228192)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 135.41/19.55 % (1228192)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 135.41/19.55 % (1228192)CaDiCaL version: 2.1.3 % 135.41/19.55 % (1228192)Termination reason: Instruction limit % 135.41/19.55 % (1228192)Termination phase: Saturation % 135.41/19.55 % (1228192)Time elapsed: 13.168 s % 135.41/19.55 % (1228192)Peak memory usage: 705 MB % 135.41/19.55 % (1228192)Instructions burned: 22567 (million) % 135.41/19.55 % (1228212)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=3320824313:i=26857:ins=20_2835 on theBenchmark for (2835ds/26857Mi) % 135.41/19.55 % (1228212)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 135.41/19.55 % (1228212)Terminated due to inappropriate strategy. % 135.41/19.55 % (1228212)------------------------------ % 135.41/19.55 % (1228212)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 135.41/19.55 % (1228212)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 135.41/19.55 % (1228212)CaDiCaL version: 2.1.3 % 135.41/19.55 % (1228212)Termination reason: Inappropriate % 135.41/19.55 % (1228212)Time elapsed: 0.0000 s % 135.41/19.55 % (1228212)Peak memory usage: 10 MB % 135.41/19.55 % (1228212)------------------------------ % 135.41/19.55 % (1228212)------------------------------ % 135.41/19.55 % (1228214)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=733287596:i=28120:bs=on:fsr=off_2834 on theBenchmark for (2834ds/28120Mi) % 135.41/19.55 % (1228182)Instruction limit reached! % 135.41/19.55 % (1228182)------------------------------ % 135.41/19.55 % (1228182)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 135.41/19.55 % (1228182)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 135.41/19.55 % (1228182)CaDiCaL version: 2.1.3 % 135.41/19.55 % (1228182)Termination reason: Instruction limit % 135.41/19.55 % (1228182)Termination phase: Saturation % 135.41/19.55 % (1228182)Time elapsed: 14.666 s % 135.41/19.55 % (1228182)Peak memory usage: 221 MB % 135.41/19.55 % (1228182)Instructions burned: 29341 (million) % 135.41/19.55 % (1228216)fmb+10_1_sil=256000:fmbss=7:random_seed=1164552766:fmbsr=1.6:i=182295_2829 on theBenchmark for (2829ds/182295Mi) % 135.41/19.55 % (1228216)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 135.41/19.55 % (1228216)Terminated due to inappropriate strategy. % 135.41/19.55 % (1228216)------------------------------ % 135.41/19.55 % (1228216)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 135.41/19.55 % (1228216)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 135.41/19.55 % (1228216)CaDiCaL version: 2.1.3 % 135.41/19.55 % (1228216)Termination reason: Inappropriate % 135.41/19.55 % (1228216)Time elapsed: 0.0000 s % 135.41/19.55 % (1228216)Peak memory usage: 10 MB % 135.41/19.55 % (1228216)------------------------------ % 135.41/19.55 % (1228216)------------------------------ % 135.41/19.55 % (1228218)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=530266185:i=44625:gsp=on_2828 on theBenchmark for (2828ds/44625Mi) % 135.41/19.55 % (1228218)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 135.41/19.55 % (1228218)Terminated due to inappropriate strategy. % 135.41/19.55 % (1228218)------------------------------ % 135.41/19.55 % (1228218)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 135.41/19.55 % (1228218)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 135.41/19.55 % (1228218)CaDiCaL version: 2.1.3 % 135.41/19.55 % (1228218)Termination reason: Inappropriate % 135.41/19.55 % (1228218)Time elapsed: 0.0000 s % 135.41/19.55 % (1228218)Peak memory usage: 10 MB % 135.41/19.55 % (1228218)------------------------------ % 135.41/19.55 % (1228218)------------------------------ % 135.41/19.55 % (1228220)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=249402376:i=160505_2828 on theBenchmark for (2828ds/160505Mi) % 147.57/21.25 % (1228220)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 147.57/21.25 % (1228220)Terminated due to inappropriate strategy. % 147.57/21.25 % (1228220)------------------------------ % 147.57/21.25 % (1228220)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 147.57/21.25 % (1228220)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 147.57/21.25 % (1228220)CaDiCaL version: 2.1.3 % 147.57/21.25 % (1228220)Termination reason: Inappropriate % 147.57/21.25 % (1228220)Time elapsed: 0.0000 s % 147.57/21.25 % (1228220)Peak memory usage: 10 MB % 147.57/21.25 % (1228220)------------------------------ % 147.57/21.25 % (1228220)------------------------------ % 147.57/21.25 % (1228222)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=3424541702:fmbsr=1.3:i=225729_2828 on theBenchmark for (2828ds/225729Mi) % 147.57/21.25 % (1228222)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 147.57/21.25 % (1228222)Terminated due to inappropriate strategy. % 147.57/21.25 % (1228222)------------------------------ % 147.57/21.25 % (1228222)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 147.57/21.25 % (1228222)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 147.57/21.25 % (1228222)CaDiCaL version: 2.1.3 % 147.57/21.25 % (1228222)Termination reason: Inappropriate % 147.57/21.25 % (1228222)Time elapsed: 0.0000 s % 147.57/21.25 % (1228222)Peak memory usage: 10 MB % 147.57/21.25 % (1228222)------------------------------ % 147.57/21.25 % (1228222)------------------------------ % 147.57/21.25 % (1228224)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=466569180:fmbsr=2:i=185024:ins=7_2828 on theBenchmark for (2828ds/185024Mi) % 147.57/21.25 % (1228224)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 147.57/21.25 % (1228224)Terminated due to inappropriate strategy. % 147.57/21.25 % (1228224)------------------------------ % 147.57/21.25 % (1228224)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 147.57/21.25 % (1228224)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 147.57/21.25 % (1228224)CaDiCaL version: 2.1.3 % 147.57/21.25 % (1228224)Termination reason: Inappropriate % 147.57/21.25 % (1228224)Time elapsed: 0.0000 s % 147.57/21.25 % (1228224)Peak memory usage: 10 MB % 147.57/21.25 % (1228224)------------------------------ % 147.57/21.25 % (1228224)------------------------------ % 147.57/21.25 % (1228226)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=4061292982:rtra=on_2827 on theBenchmark for (2827ds/0Mi) % 147.57/21.25 % (1228226)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 147.57/21.25 % (1228226)Terminated due to inappropriate strategy. % 147.57/21.25 % (1228226)------------------------------ % 147.57/21.25 % (1228226)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 147.57/21.25 % (1228226)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 147.57/21.25 % (1228226)CaDiCaL version: 2.1.3 % 147.57/21.25 % (1228226)Termination reason: Inappropriate % 147.57/21.25 % (1228226)Time elapsed: 0.0000 s % 147.57/21.25 % (1228226)Peak memory usage: 10 MB % 147.57/21.25 % (1228226)------------------------------ % 147.57/21.25 % (1228226)------------------------------ % 147.57/21.25 % (1228228)% WARNING: option uhcvi not known. % 147.57/21.25 % (1228228)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=519461279:i=271062:add=off:rtra=on:rawr=on_2827 on theBenchmark for (2827ds/271062Mi) % 147.57/21.25 % (1228204)Instruction limit reached! % 147.57/21.25 % (1228204)------------------------------ % 147.57/21.25 % (1228204)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 147.57/21.25 % (1228204)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 147.57/21.25 % (1228204)CaDiCaL version: 2.1.3 % 147.57/21.25 % (1228204)Termination reason: Instruction limit % 147.57/21.25 % (1228204)Termination phase: Saturation % 147.57/21.25 % (1228204)Time elapsed: 9.096 s % 147.57/21.25 % (1228204)Peak memory usage: 49 MB % 147.57/21.25 % (1228204)Instructions burned: 14134 (million) % 147.57/21.25 % (1228230)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=923010783:i=176048:add=on:rtra=on:rawr=on_2822 on theBenchmark for (2822ds/176048Mi) % 147.57/21.25 % (1228208)Instruction limit reached! % 147.57/21.25 % (1228208)------------------------------ % 147.57/21.25 % (1228208)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 154.65/22.27 % (1228208)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 154.65/22.27 % (1228208)CaDiCaL version: 2.1.3 % 154.65/22.27 % (1228208)Termination reason: Instruction limit % 154.65/22.27 % (1228208)Termination phase: Saturation % 154.65/22.27 % (1228208)Time elapsed: 4.852 s % 154.65/22.27 % (1228208)Peak memory usage: 187 MB % 154.65/22.27 % (1228208)Instructions burned: 17628 (million) % 154.65/22.27 % (1228232)dis+10_1_sil=32000:si=on:sp=arity:random_seed=3277693191:i=206:fgj=on:rtra=on_2813 on theBenchmark for (2813ds/206Mi) % 154.65/22.27 % (1228232)Instruction limit reached! % 154.65/22.27 % (1228232)------------------------------ % 154.65/22.27 % (1228232)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 154.65/22.27 % (1228232)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 154.65/22.27 % (1228232)CaDiCaL version: 2.1.3 % 154.65/22.27 % (1228232)Termination reason: Instruction limit % 154.65/22.27 % (1228232)Termination phase: Saturation % 154.65/22.27 % (1228232)Time elapsed: 0.068 s % 154.65/22.27 % (1228232)Peak memory usage: 13 MB % 154.65/22.27 % (1228232)Instructions burned: 208 (million) % 154.65/22.27 % (1228234)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=530944487:i=232:rtra=on_2812 on theBenchmark for (2812ds/232Mi) % 154.65/22.27 % (1228234)Instruction limit reached! % 154.65/22.27 % (1228234)------------------------------ % 154.65/22.27 % (1228234)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 154.65/22.27 % (1228234)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 154.65/22.27 % (1228234)CaDiCaL version: 2.1.3 % 154.65/22.27 % (1228234)Termination reason: Instruction limit % 154.65/22.27 % (1228234)Termination phase: Saturation % 154.65/22.27 % (1228234)Time elapsed: 0.077 s % 154.65/22.27 % (1228234)Peak memory usage: 13 MB % 154.65/22.27 % (1228234)Instructions burned: 234 (million) % 154.65/22.27 % (1228236)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=2542724327:i=262:rtra=on_2811 on theBenchmark for (2811ds/262Mi) % 154.65/22.27 % (1228236)Instruction limit reached! % 154.65/22.27 % (1228236)------------------------------ % 154.65/22.27 % (1228236)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 154.65/22.27 % (1228236)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 154.65/22.27 % (1228236)CaDiCaL version: 2.1.3 % 154.65/22.27 % (1228236)Termination reason: Instruction limit % 154.65/22.27 % (1228236)Termination phase: Saturation % 154.65/22.27 % (1228236)Time elapsed: 0.086 s % 154.65/22.27 % (1228236)Peak memory usage: 13 MB % 154.65/22.27 % (1228236)Instructions burned: 264 (million) % 154.65/22.27 % (1228238)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=2875515679:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2810 on theBenchmark for (2810ds/318Mi) % 154.65/22.27 % (1228238)Instruction limit reached! % 154.65/22.27 % (1228238)------------------------------ % 154.65/22.27 % (1228238)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 154.65/22.27 % (1228238)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 154.65/22.27 % (1228238)CaDiCaL version: 2.1.3 % 154.65/22.27 % (1228238)Termination reason: Instruction limit % 154.65/22.27 % (1228238)Termination phase: Saturation % 154.65/22.27 % (1228238)Time elapsed: 0.105 s % 154.65/22.27 % (1228238)Peak memory usage: 14 MB % 154.65/22.27 % (1228238)Instructions burned: 319 (million) % 154.65/22.27 % (1228240)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=2379661088:i=1428:nm=2:rtra=on_2809 on theBenchmark for (2809ds/1428Mi) % 154.65/22.27 % (1228240)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 154.65/22.27 % (1228240)Terminated due to inappropriate strategy. % 154.65/22.27 % (1228240)------------------------------ % 154.65/22.27 % (1228240)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 154.65/22.27 % (1228240)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 154.65/22.27 % (1228240)CaDiCaL version: 2.1.3 % 154.65/22.27 % (1228240)Termination reason: Inappropriate % 154.65/22.27 % (1228240)Time elapsed: 0.0000 s % 154.65/22.27 % (1228240)Peak memory usage: 10 MB % 154.65/22.27 % (1228240)------------------------------ % 154.65/22.27 % (1228240)------------------------------ % 154.65/22.27 % (1228242)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=1493085497:i=262:bd=preordered:rtra=on:fsd=on_2809 on theBenchmark for (2809ds/262Mi) % 154.65/22.27 % (1228242)Instruction limit reached! % 154.65/22.27 % (1228242)------------------------------ % 154.65/22.27 % (1228242)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 196.75/28.16 % (1228242)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 196.75/28.16 % (1228242)CaDiCaL version: 2.1.3 % 196.75/28.16 % (1228242)Termination reason: Instruction limit % 196.75/28.16 % (1228242)Termination phase: Saturation % 196.75/28.16 % (1228242)Time elapsed: 0.093 s % 196.75/28.16 % (1228242)Peak memory usage: 14 MB % 196.75/28.16 % (1228242)Instructions burned: 265 (million) % 196.75/28.16 % (1228244)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=4110468211:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2808 on theBenchmark for (2808ds/1368Mi) % 196.75/28.16 % (1228244)Instruction limit reached! % 196.75/28.16 % (1228244)------------------------------ % 196.75/28.16 % (1228244)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 196.75/28.16 % (1228244)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 196.75/28.16 % (1228244)CaDiCaL version: 2.1.3 % 196.75/28.16 % (1228244)Termination reason: Instruction limit % 196.75/28.16 % (1228244)Termination phase: Saturation % 196.75/28.16 % (1228244)Time elapsed: 0.421 s % 196.75/28.16 % (1228244)Peak memory usage: 23 MB % 196.75/28.16 % (1228244)Instructions burned: 1371 (million) % 196.75/28.16 % (1228246)ott-21_1_sil=16000:si=on:fs=off:random_seed=1395669888:i=360:av=off:fsr=off:rtra=on_2804 on theBenchmark for (2804ds/360Mi) % 196.75/28.16 % (1228246)Instruction limit reached! % 196.75/28.16 % (1228246)------------------------------ % 196.75/28.16 % (1228246)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 196.75/28.16 % (1228246)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 196.75/28.16 % (1228246)CaDiCaL version: 2.1.3 % 196.75/28.16 % (1228246)Termination reason: Instruction limit % 196.75/28.16 % (1228246)Termination phase: Saturation % 196.75/28.16 % (1228246)Time elapsed: 0.083 s % 196.75/28.16 % (1228246)Peak memory usage: 12 MB % 196.75/28.16 % (1228246)Instructions burned: 363 (million) % 196.75/28.16 % (1228248)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3526009320:i=954:bd=all:rtra=on_2803 on theBenchmark for (2803ds/954Mi) % 196.75/28.16 % (1228248)Instruction limit reached! % 196.75/28.16 % (1228248)------------------------------ % 196.75/28.16 % (1228248)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 196.75/28.16 % (1228248)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 196.75/28.16 % (1228248)CaDiCaL version: 2.1.3 % 196.75/28.16 % (1228248)Termination reason: Instruction limit % 196.75/28.16 % (1228248)Termination phase: Saturation % 196.75/28.16 % (1228248)Time elapsed: 0.308 s % 196.75/28.16 % (1228248)Peak memory usage: 17 MB % 196.75/28.16 % (1228248)Instructions burned: 955 (million) % 196.75/28.16 % (1228250)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=1943415160:fmbsr=1.3:i=1730:ins=25:rtra=on_2800 on theBenchmark for (2800ds/1730Mi) % 196.75/28.16 % (1228250)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 196.75/28.16 % (1228250)Terminated due to inappropriate strategy. % 196.75/28.16 % (1228250)------------------------------ % 196.75/28.16 % (1228250)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 196.75/28.16 % (1228250)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 196.75/28.16 % (1228250)CaDiCaL version: 2.1.3 % 196.75/28.16 % (1228250)Termination reason: Inappropriate % 196.75/28.16 % (1228250)Time elapsed: 0.0000 s % 196.75/28.16 % (1228250)Peak memory usage: 10 MB % 196.75/28.16 % (1228250)------------------------------ % 196.75/28.16 % (1228250)------------------------------ % 196.75/28.16 % (1228252)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=2900618868:i=2358:rtra=on_2800 on theBenchmark for (2800ds/2358Mi) % 196.75/28.16 % (1228252)Instruction limit reached! % 196.75/28.16 % (1228252)------------------------------ % 196.75/28.16 % (1228252)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 196.75/28.16 % (1228252)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 196.75/28.16 % (1228252)CaDiCaL version: 2.1.3 % 196.75/28.16 % (1228252)Termination reason: Instruction limit % 196.75/28.16 % (1228252)Termination phase: Saturation % 196.75/28.16 % (1228252)Time elapsed: 0.814 s % 196.75/28.16 % (1228252)Peak memory usage: 21 MB % 196.75/28.16 % (1228252)Instructions burned: 2360 (million) % 196.75/28.16 % (1228254)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=428983788:i=1778:ins=1:rtra=on_2791 on theBenchmark for (2791ds/1778Mi) % 196.75/28.16 % (1228254)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 232.26/33.15 % (1228254)Terminated due to inappropriate strategy. % 232.26/33.15 % (1228254)------------------------------ % 232.26/33.15 % (1228254)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 232.26/33.15 % (1228254)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 232.26/33.15 % (1228254)CaDiCaL version: 2.1.3 % 232.26/33.15 % (1228254)Termination reason: Inappropriate % 232.26/33.15 % (1228254)Time elapsed: 0.0000 s % 232.26/33.15 % (1228254)Peak memory usage: 10 MB % 232.26/33.15 % (1228254)------------------------------ % 232.26/33.15 % (1228254)------------------------------ % 232.26/33.15 % (1228256)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=1879535806:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2791 on theBenchmark for (2791ds/1384Mi) % 232.26/33.15 % (1228256)Instruction limit reached! % 232.26/33.15 % (1228256)------------------------------ % 232.26/33.15 % (1228256)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 232.26/33.15 % (1228256)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 232.26/33.15 % (1228256)CaDiCaL version: 2.1.3 % 232.26/33.15 % (1228256)Termination reason: Instruction limit % 232.26/33.15 % (1228256)Termination phase: Saturation % 232.26/33.15 % (1228256)Time elapsed: 0.430 s % 232.26/33.15 % (1228256)Peak memory usage: 21 MB % 232.26/33.15 % (1228256)Instructions burned: 1387 (million) % 232.26/33.15 % (1228258)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=4017387633:i=1758:kws=inv_precedence:fsr=off:rtra=on_2787 on theBenchmark for (2787ds/1758Mi) % 232.26/33.15 % (1228258)Instruction limit reached! % 232.26/33.15 % (1228258)------------------------------ % 232.26/33.15 % (1228258)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 232.26/33.15 % (1228258)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 232.26/33.15 % (1228258)CaDiCaL version: 2.1.3 % 232.26/33.15 % (1228258)Termination reason: Instruction limit % 232.26/33.15 % (1228258)Termination phase: Saturation % 232.26/33.15 % (1228258)Time elapsed: 0.531 s % 232.26/33.15 % (1228258)Peak memory usage: 26 MB % 232.26/33.15 % (1228258)Instructions burned: 1758 (million) % 232.26/33.15 % (1228260)fmb+10_1_sil=64000:si=on:random_seed=551974386:i=44122:nm=2:rtra=on:gsp=on_2781 on theBenchmark for (2781ds/44122Mi) % 232.26/33.15 % (1228260)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 232.26/33.15 % (1228260)Terminated due to inappropriate strategy. % 232.26/33.15 % (1228260)------------------------------ % 232.26/33.15 % (1228260)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 232.26/33.15 % (1228260)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 232.26/33.15 % (1228260)CaDiCaL version: 2.1.3 % 232.26/33.15 % (1228260)Termination reason: Inappropriate % 232.26/33.15 % (1228260)Time elapsed: 0.0000 s % 232.26/33.15 % (1228260)Peak memory usage: 10 MB % 232.26/33.15 % (1228260)------------------------------ % 232.26/33.15 % (1228260)------------------------------ % 232.26/33.15 % (1228262)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=1310026407:i=19030:nm=5:rtra=on_2781 on theBenchmark for (2781ds/19030Mi) % 232.26/33.15 % (1228262)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 232.26/33.15 % (1228262)Terminated due to inappropriate strategy. % 232.26/33.15 % (1228262)------------------------------ % 232.26/33.15 % (1228262)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 232.26/33.15 % (1228262)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 232.26/33.15 % (1228262)CaDiCaL version: 2.1.3 % 232.26/33.15 % (1228262)Termination reason: Inappropriate % 232.26/33.15 % (1228262)Time elapsed: 0.0000 s % 232.26/33.15 % (1228262)Peak memory usage: 10 MB % 232.26/33.15 % (1228262)------------------------------ % 232.26/33.15 % (1228262)------------------------------ % 232.26/33.15 % (1228264)fmb+10_1_sil=64000:sas=cadical:si=on:fmbss=8:random_seed=2890724375:fmbsr=1.7:i=1840:rtra=on_2781 on theBenchmark for (2781ds/1840Mi) % 232.26/33.15 % (1228264)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 232.26/33.15 % (1228264)Terminated due to inappropriate strategy. % 232.26/33.15 % (1228264)------------------------------ % 232.26/33.15 % (1228264)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 232.26/33.15 % (1228264)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 268.22/38.29 % (1228264)CaDiCaL version: 2.1.3 % 268.22/38.29 % (1228264)Termination reason: Inappropriate % 268.22/38.29 % (1228264)Time elapsed: 0.0000 s % 268.22/38.29 % (1228264)Peak memory usage: 10 MB % 268.22/38.29 % (1228264)------------------------------ % 268.22/38.29 % (1228264)------------------------------ % 268.22/38.29 % (1228266)dis-4_1_sil=16000:drc=ordering:si=on:sp=const_frequency:sac=on:newcnf=on:random_seed=3765406848:i=10262:rtra=on_2781 on theBenchmark for (2781ds/10262Mi) % 268.22/38.29 % (1228266)Instruction limit reached! % 268.22/38.29 % (1228266)------------------------------ % 268.22/38.29 % (1228266)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 268.22/38.29 % (1228266)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 268.22/38.29 % (1228266)CaDiCaL version: 2.1.3 % 268.22/38.29 % (1228266)Termination reason: Instruction limit % 268.22/38.29 % (1228266)Termination phase: Saturation % 268.22/38.29 % (1228266)Time elapsed: 3.144 s % 268.22/38.29 % (1228266)Peak memory usage: 67 MB % 268.22/38.29 % (1228266)Instructions burned: 10263 (million) % 268.22/38.29 % (1228269)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:si=on:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1967359943:i=2944:ins=7:rtra=on:fdi=8:gsp=on_2749 on theBenchmark for (2749ds/2944Mi) % 268.22/38.29 % (1228269)Instruction limit reached! % 268.22/38.29 % (1228269)------------------------------ % 268.22/38.29 % (1228269)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 268.22/38.29 % (1228269)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 268.22/38.29 % (1228269)CaDiCaL version: 2.1.3 % 268.22/38.29 % (1228269)Termination reason: Instruction limit % 268.22/38.29 % (1228269)Termination phase: Saturation % 268.22/38.29 % (1228269)Time elapsed: 0.754 s % 268.22/38.29 % (1228269)Peak memory usage: 31 MB % 268.22/38.29 % (1228269)Instructions burned: 2948 (million) % 268.22/38.29 % (1228271)fmb+10_1_sil=16000:sas=cadical:si=on:bce=on:fmbss=77:random_seed=3064766286:i=12648:rtra=on_2742 on theBenchmark for (2742ds/12648Mi) % 268.22/38.29 % (1228271)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 268.22/38.29 % (1228271)Terminated due to inappropriate strategy. % 268.22/38.29 % (1228271)------------------------------ % 268.22/38.29 % (1228271)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 268.22/38.29 % (1228271)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 268.22/38.29 % (1228271)CaDiCaL version: 2.1.3 % 268.22/38.29 % (1228271)Termination reason: Inappropriate % 268.22/38.29 % (1228271)Time elapsed: 0.0000 s % 268.22/38.29 % (1228271)Peak memory usage: 10 MB % 268.22/38.29 % (1228271)------------------------------ % 268.22/38.29 % (1228271)------------------------------ % 268.22/38.29 % (1228273)fmb+10_1_fmbas=function:sil=32000:sas=cadical:si=on:fmbss=16:random_seed=2350338892:fmbsr=2.30978:i=4348:rtra=on_2741 on theBenchmark for (2741ds/4348Mi) % 268.22/38.29 % (1228273)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 268.22/38.29 % (1228273)Terminated due to inappropriate strategy. % 268.22/38.29 % (1228273)------------------------------ % 268.22/38.29 % (1228273)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 268.22/38.29 % (1228273)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 268.22/38.29 % (1228273)CaDiCaL version: 2.1.3 % 268.22/38.29 % (1228273)Termination reason: Inappropriate % 268.22/38.29 % (1228273)Time elapsed: 0.0000 s % 268.22/38.29 % (1228273)Peak memory usage: 10 MB % 268.22/38.29 % (1228273)------------------------------ % 268.22/38.29 % (1228273)------------------------------ % 268.22/38.29 % (1228275)ott-2_1_sil=16000:si=on:newcnf=on:random_seed=3284687292:avsq=on:i=1738:avsqr=1,16:kws=inv_arity_squared:rtra=on_2741 on theBenchmark for (2741ds/1738Mi) % 268.22/38.29 % (1228275)Instruction limit reached! % 268.22/38.29 % (1228275)------------------------------ % 268.22/38.29 % (1228275)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 268.22/38.29 % (1228275)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 268.22/38.29 % (1228275)CaDiCaL version: 2.1.3 % 268.22/38.29 % (1228275)Termination reason: Instruction limit % 268.22/38.29 % (1228275)Termination phase: Saturation % 268.22/38.29 % (1228275)Time elapsed: 0.619 s % 268.22/38.29 % (1228275)Peak memory usage: 20 MB % 268.22/38.29 % (1228275)Instructions burned: 1738 (million) % 268.22/38.29 % (1228277)ott+10_1_sil=32000:tgt=ground:si=on:random_seed=2090858780:i=10228:av=off:rtra=on_2735 on theBenchmark for (2735ds/10228Mi) % 268.22/38.29 % (1228214)Instruction limit reached! % 300.15/42.74 % (1228214)------------------------------ % 300.15/42.74 % (1228214)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.15/42.74 % (1228214)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.15/42.74 % (1228214)CaDiCaL version: 2.1.3 % 300.15/42.74 % (1228214)Termination reason: Instruction limit % 300.15/42.74 % (1228214)Termination phase: Saturation % 300.15/42.74 % (1228214)Time elapsed: 11.226 s % 300.15/42.74 % (1228214)Peak memory usage: 26 MB % 300.15/42.74 % (1228214)Instructions burned: 28122 (million) % 300.15/42.74 % (1228279)fmb+10_1_sil=64000:sas=cadical:si=on:bce=on:rp=on:random_seed=2080434170:i=108564:rtra=on_2722 on theBenchmark for (2722ds/108564Mi) % 300.15/42.74 % (1228279)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 300.15/42.74 % (1228279)Terminated due to inappropriate strategy. % 300.15/42.74 % (1228279)------------------------------ % 300.15/42.74 % (1228279)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.15/42.74 % (1228279)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.15/42.74 % (1228279)CaDiCaL version: 2.1.3 % 300.15/42.74 % (1228279)Termination reason: Inappropriate % 300.15/42.74 % (1228279)Time elapsed: 0.0000 s % 300.15/42.74 % (1228279)Peak memory usage: 10 MB % 300.15/42.74 % (1228279)------------------------------ % 300.15/42.74 % (1228279)------------------------------ % 300.15/42.74 % (1228281)dis-11_1_sil=16000:si=on:sp=reverse_frequency:alpa=true:random_seed=238093758:i=7024:aac=none:rtra=on_2722 on theBenchmark for (2722ds/7024Mi) % 300.15/42.74 % (1228277)Instruction limit reached! % 300.15/42.74 % (1228277)------------------------------ % 300.15/42.74 % (1228277)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.15/42.74 % (1228277)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.15/42.74 % (1228277)CaDiCaL version: 2.1.3 % 300.15/42.74 % (1228277)Termination reason: Instruction limit % 300.15/42.74 % (1228277)Termination phase: Saturation % 300.15/42.74 % (1228277)Time elapsed: 3.873 s % 300.15/42.74 % (1228277)Peak memory usage: 40 MB % 300.15/42.74 % (1228277)Instructions burned: 10230 (million) % 300.15/42.74 % (1228283)dis+21_1_sil=32000:sas=cadical:si=on:random_seed=2403906838:i=7546:rtra=on:amm=off_2696 on theBenchmark for (2696ds/7546Mi) % 300.15/42.74 % (1228281)Instruction limit reached! % 300.15/42.74 % (1228281)------------------------------ % 300.15/42.74 % (1228281)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.15/42.74 % (1228281)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.15/42.74 % (1228281)CaDiCaL version: 2.1.3 % 300.15/42.74 % (1228281)Termination reason: Instruction limit % 300.15/42.74 % (1228281)Termination phase: Saturation % 300.15/42.74 % (1228281)Time elapsed: 4.056 s % 300.15/42.74 % (1228281)Peak memory usage: 43 MB % 300.15/42.74 % (1228281)Instructions burned: 7024 (million) % 300.15/42.74 % (1228285)ott+11_1_sil=16000:si=on:gs=on:random_seed=513575497:s2a=on:i=4502:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:rtra=on:fsd=on_2681 on theBenchmark for (2681ds/4502Mi) % 300.15/42.74 % (1228283)Instruction limit reached! % 300.15/42.74 % (1228283)------------------------------ % 300.15/42.74 % (1228283)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.15/42.74 % (1228283)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.15/42.74 % (1228283)CaDiCaL version: 2.1.3 % 300.15/42.74 % (1228283)Termination reason: Instruction limit % 300.15/42.74 % (1228283)Termination phase: Saturation % 300.15/42.74 % (1228283)Time elapsed: 2.350 s % 300.15/42.74 % (1228283)Peak memory usage: 44 MB % 300.15/42.74 % (1228283)Instructions burned: 7549 (million) % 300.15/42.74 % (1228287)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:si=on:fmbss=7:random_seed=239492285:fmbsr=1.6:i=135068:rtra=on_2672 on theBenchmark for (2672ds/135068Mi) % 300.15/42.74 % (1228287)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 300.15/42.74 % (1228287)Terminated due to inappropriate strategy. % 300.15/42.74 % (1228287)------------------------------ % 300.15/42.74 % (1228287)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.15/42.74 % (1228287)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.15/42.74 % (1228287)CaDiCaL version: 2.1.3 % 300.15/42.74 % (1228287)Termination reason: Inappropriate % 300.15/42.74 % (1228287)Time elapsed: 0.0000 s % 300.15/42.74 % (1228287)Peak memory usage: 10 MB % 300.15/42.74 % (1228287)------------------------------ % 300.15/42.74 % (1228287)------------------------------ % 300.15/42.74 % (1228289) % 300.15/42.74 Terminated % 300.15/42.74 % Vampire exiting % 300.15/42.74 Terminated %------------------------------------------------------------------------------