%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWW827_1 : TPTP v9.3.1. Released v7.0.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % Computer : n012.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 29 01:45:02 PM UTC 2026 % Result : Timeout 300.07s 42.74s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.01 % Problem : SWW827_1 : TPTP v9.3.1. Released v7.0.0. % 0.00/0.03 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.00/0.11 % Computer : n012.cluster.edu % 0.00/0.11 % Model : x86_64 x86_64 % 0.00/0.11 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.00/0.11 % Memory : 8046.5625MB % 0.00/0.11 % OS : Linux 6.8.0-71-generic % 0.00/0.11 % CPULimit : 300 % 0.00/0.11 % WCLimit : 300 % 0.00/0.11 % DateTime : Mon Sep 28 14:30:34 UTC 2026 % 0.00/0.11 % CPUTime : % 0.00/0.11 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.08/0.12 Running first-order model finding % 0.08/0.12 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.61/0.54 % (3420047)Will run a generic schedule for satisfiability detection. % 2.61/0.54 % (3420065)% WARNING: option uhcvi not known. % 2.61/0.54 % (3420064)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1223300334_2999 on theBenchmark for (2999ds/0Mi) % 2.61/0.54 % (3420067)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2577597667:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 2.61/0.54 % (3420068)dis+10_1_sil=32000:sp=arity:random_seed=938262309:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 2.61/0.54 % (3420069)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1731250514:i=116_2999 on theBenchmark for (2999ds/116Mi) % 2.61/0.54 % (3420065)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=899649011:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 2.61/0.54 % (3420070)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3488339677:i=131_2999 on theBenchmark for (2999ds/131Mi) % 2.61/0.54 % (3420071)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1596361499:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 2.61/0.54 % (3420064)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 2.61/0.54 % (3420064)Terminated due to inappropriate strategy. % 2.61/0.54 % (3420064)------------------------------ % 2.61/0.54 % (3420064)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 2.61/0.54 % (3420064)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 2.61/0.54 % (3420064)CaDiCaL version: 2.1.3 % 2.61/0.54 % (3420064)Termination reason: Inappropriate % 2.61/0.54 % (3420064)Time elapsed: 0.018 s % 2.61/0.54 % (3420064)Peak memory usage: 12 MB % 2.61/0.54 % (3420064)Instructions burned: 75 (million) % 2.61/0.54 % (3420064)------------------------------ % 2.61/0.54 % (3420064)------------------------------ % 2.61/0.54 % (3420068)Instruction limit reached! % 2.61/0.54 % (3420068)------------------------------ % 2.61/0.54 % (3420068)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 2.61/0.54 % (3420068)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 2.61/0.54 % (3420068)CaDiCaL version: 2.1.3 % 2.61/0.54 % (3420068)Termination reason: Instruction limit % 2.61/0.54 % (3420068)Termination phase: Saturation % 2.61/0.54 % (3420068)Time elapsed: 0.028 s % 2.61/0.54 % (3420068)Peak memory usage: 13 MB % 2.61/0.54 % (3420068)Instructions burned: 104 (million) % 2.61/0.54 % (3420090)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=183904899:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 2.61/0.54 % (3420069)Instruction limit reached! % 2.61/0.54 % (3420069)------------------------------ % 2.61/0.54 % (3420069)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 2.61/0.54 % (3420069)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 2.61/0.54 % (3420069)CaDiCaL version: 2.1.3 % 2.61/0.54 % (3420069)Termination reason: Instruction limit % 2.61/0.54 % (3420069)Termination phase: Saturation % 2.61/0.54 % (3420069)Time elapsed: 0.030 s % 2.61/0.54 % (3420069)Peak memory usage: 14 MB % 2.61/0.54 % (3420069)Instructions burned: 117 (million) % 2.61/0.54 % (3420097)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3951356280:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 2.61/0.54 % (3420100)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=188341231:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi) % 2.61/0.54 % (3420070)Instruction limit reached! % 2.61/0.54 % (3420070)------------------------------ % 2.61/0.54 % (3420070)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 2.61/0.54 % (3420070)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 2.61/0.54 % (3420070)CaDiCaL version: 2.1.3 % 2.61/0.54 % (3420070)Termination reason: Instruction limit % 2.61/0.54 % (3420070)Termination phase: Saturation % 2.61/0.54 % (3420070)Time elapsed: 0.044 s % 2.61/0.54 % (3420070)Peak memory usage: 14 MB % 2.61/0.54 % (3420070)Instructions burned: 133 (million) % 2.61/0.54 % (3420090)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 2.61/0.54 % (3420090)Terminated due to inappropriate strategy. % 2.61/0.54 % (3420090)------------------------------ % 2.61/0.54 % (3420090)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.59/0.72 % (3420090)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.59/0.72 % (3420090)CaDiCaL version: 2.1.3 % 3.59/0.72 % (3420090)Termination reason: Inappropriate % 3.59/0.72 % (3420090)Time elapsed: 0.024 s % 3.59/0.72 % (3420090)Peak memory usage: 12 MB % 3.59/0.72 % (3420090)Instructions burned: 75 (million) % 3.59/0.72 % (3420090)------------------------------ % 3.59/0.72 % (3420090)------------------------------ % 3.59/0.72 % (3420110)ott-21_1_sil=16000:fs=off:random_seed=4092382917:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi) % 3.59/0.72 % (3420112)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2940396375:i=477:bd=all_2999 on theBenchmark for (2999ds/477Mi) % 3.59/0.72 % (3420071)Instruction limit reached! % 3.59/0.72 % (3420071)------------------------------ % 3.59/0.72 % (3420071)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.59/0.72 % (3420071)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.59/0.72 % (3420071)CaDiCaL version: 2.1.3 % 3.59/0.72 % (3420071)Termination reason: Instruction limit % 3.59/0.72 % (3420071)Termination phase: Saturation % 3.59/0.72 % (3420071)Time elapsed: 0.079 s % 3.59/0.72 % (3420071)Peak memory usage: 14 MB % 3.59/0.72 % (3420071)Instructions burned: 159 (million) % 3.59/0.72 % (3420097)Instruction limit reached! % 3.59/0.72 % (3420097)------------------------------ % 3.59/0.72 % (3420097)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.59/0.72 % (3420097)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.59/0.72 % (3420097)CaDiCaL version: 2.1.3 % 3.59/0.72 % (3420097)Termination reason: Instruction limit % 3.59/0.72 % (3420097)Termination phase: Saturation % 3.59/0.72 % (3420097)Time elapsed: 0.061 s % 3.59/0.72 % (3420097)Peak memory usage: 14 MB % 3.59/0.72 % (3420097)Instructions burned: 132 (million) % 3.59/0.72 % (3420123)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1279160662:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 3.59/0.72 % (3420110)Instruction limit reached! % 3.59/0.72 % (3420110)------------------------------ % 3.59/0.72 % (3420110)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.59/0.72 % (3420110)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.59/0.72 % (3420110)CaDiCaL version: 2.1.3 % 3.59/0.72 % (3420110)Termination reason: Instruction limit % 3.59/0.72 % (3420110)Termination phase: Saturation % 3.59/0.72 % (3420110)Time elapsed: 0.047 s % 3.59/0.72 % (3420110)Peak memory usage: 13 MB % 3.59/0.72 % (3420110)Instructions burned: 182 (million) % 3.59/0.72 % (3420124)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3687577580:i=1179_2998 on theBenchmark for (2998ds/1179Mi) % 3.59/0.72 % (3420127)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=315032838:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi) % 3.59/0.72 % (3420123)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.59/0.72 % (3420123)Terminated due to inappropriate strategy. % 3.59/0.72 % (3420123)------------------------------ % 3.59/0.72 % (3420123)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.59/0.72 % (3420123)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.59/0.72 % (3420123)CaDiCaL version: 2.1.3 % 3.59/0.72 % (3420123)Termination reason: Inappropriate % 3.59/0.72 % (3420123)Time elapsed: 0.025 s % 3.59/0.72 % (3420123)Peak memory usage: 12 MB % 3.59/0.72 % (3420123)Instructions burned: 74 (million) % 3.59/0.72 % (3420123)------------------------------ % 3.59/0.72 % (3420123)------------------------------ % 3.59/0.72 % (3420135)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=340463877: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) % 3.59/0.72 % (3420127)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.59/0.72 % (3420127)Terminated due to inappropriate strategy. % 3.59/0.72 % (3420127)------------------------------ % 3.59/0.72 % (3420127)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.59/0.72 % (3420127)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.59/0.72 % (3420127)CaDiCaL version: 2.1.3 % 3.59/0.72 % (3420127)Termination reason: Inappropriate % 3.59/0.72 % (3420127)Time elapsed: 0.027 s % 3.59/0.72 % (3420127)Peak memory usage: 12 MB % 11.91/1.98 % (3420127)Instructions burned: 76 (million) % 11.91/1.98 % (3420127)------------------------------ % 11.91/1.98 % (3420127)------------------------------ % 11.91/1.98 % (3420139)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3668680861:i=879:kws=inv_precedence:fsr=off_2998 on theBenchmark for (2998ds/879Mi) % 11.91/1.98 % (3420112)Instruction limit reached! % 11.91/1.98 % (3420112)------------------------------ % 11.91/1.98 % (3420112)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 11.91/1.98 % (3420112)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.91/1.98 % (3420112)CaDiCaL version: 2.1.3 % 11.91/1.98 % (3420112)Termination reason: Instruction limit % 11.91/1.98 % (3420112)Termination phase: Saturation % 11.91/1.98 % (3420112)Time elapsed: 0.192 s % 11.91/1.98 % (3420112)Peak memory usage: 15 MB % 11.91/1.98 % (3420112)Instructions burned: 477 (million) % 11.91/1.98 % (3420176)fmb+10_1_sil=64000:random_seed=3956206977:i=22061:nm=2:gsp=on_2996 on theBenchmark for (2996ds/22061Mi) % 11.91/1.98 % (3420100)Instruction limit reached! % 11.91/1.98 % (3420100)------------------------------ % 11.91/1.98 % (3420100)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 11.91/1.98 % (3420100)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.91/1.98 % (3420100)CaDiCaL version: 2.1.3 % 11.91/1.98 % (3420100)Termination reason: Instruction limit % 11.91/1.98 % (3420100)Termination phase: Saturation % 11.91/1.98 % (3420100)Time elapsed: 0.243 s % 11.91/1.98 % (3420100)Peak memory usage: 17 MB % 11.91/1.98 % (3420100)Instructions burned: 684 (million) % 11.91/1.98 % (3420176)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 11.91/1.98 % (3420176)Terminated due to inappropriate strategy. % 11.91/1.98 % (3420176)------------------------------ % 11.91/1.98 % (3420176)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 11.91/1.98 % (3420176)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.91/1.98 % (3420176)CaDiCaL version: 2.1.3 % 11.91/1.98 % (3420176)Termination reason: Inappropriate % 11.91/1.98 % (3420176)Time elapsed: 0.019 s % 11.91/1.98 % (3420176)Peak memory usage: 12 MB % 11.91/1.98 % (3420176)Instructions burned: 76 (million) % 11.91/1.98 % (3420183)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=865413031:i=9515:nm=5_2996 on theBenchmark for (2996ds/9515Mi) % 11.91/1.98 % (3420176)------------------------------ % 11.91/1.98 % (3420176)------------------------------ % 11.91/1.98 % (3420190)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3378265844:fmbsr=1.7:i=920_2996 on theBenchmark for (2996ds/920Mi) % 11.91/1.98 % (3420183)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 11.91/1.98 % (3420183)Terminated due to inappropriate strategy. % 11.91/1.98 % (3420183)------------------------------ % 11.91/1.98 % (3420183)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 11.91/1.98 % (3420183)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.91/1.98 % (3420183)CaDiCaL version: 2.1.3 % 11.91/1.98 % (3420183)Termination reason: Inappropriate % 11.91/1.98 % (3420183)Time elapsed: 0.019 s % 11.91/1.98 % (3420183)Peak memory usage: 12 MB % 11.91/1.98 % (3420183)Instructions burned: 75 (million) % 11.91/1.98 % (3420183)------------------------------ % 11.91/1.98 % (3420183)------------------------------ % 11.91/1.98 % (3420190)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 11.91/1.98 % (3420190)Terminated due to inappropriate strategy. % 11.91/1.98 % (3420190)------------------------------ % 11.91/1.98 % (3420190)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 11.91/1.98 % (3420190)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.91/1.98 % (3420190)CaDiCaL version: 2.1.3 % 11.91/1.98 % (3420190)Termination reason: Inappropriate % 11.91/1.98 % (3420190)Time elapsed: 0.018 s % 11.91/1.98 % (3420190)Peak memory usage: 12 MB % 11.91/1.98 % (3420190)Instructions burned: 75 (million) % 11.91/1.98 % (3420201)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=771708660:i=5131_2996 on theBenchmark for (2996ds/5131Mi) % 11.91/1.98 % (3420190)------------------------------ % 11.91/1.98 % (3420190)------------------------------ % 11.91/1.98 % (3420209)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3719824106:i=1472:ins=7:fdi=8:gsp=on_2996 on theBenchmark for (2996ds/1472Mi) % 11.91/1.98 % (3420135)Instruction limit reached! % 11.91/1.98 % (3420135)------------------------------ % 17.92/2.99 % (3420135)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 17.92/2.99 % (3420135)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.92/2.99 % (3420135)CaDiCaL version: 2.1.3 % 17.92/2.99 % (3420135)Termination reason: Instruction limit % 17.92/2.99 % (3420135)Termination phase: Saturation % 17.92/2.99 % (3420135)Time elapsed: 0.223 s % 17.92/2.99 % (3420135)Peak memory usage: 21 MB % 17.92/2.99 % (3420135)Instructions burned: 692 (million) % 17.92/2.99 % (3420227)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=130744108:i=6324_2995 on theBenchmark for (2995ds/6324Mi) % 17.92/2.99 % (3420227)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 17.92/2.99 % (3420227)Terminated due to inappropriate strategy. % 17.92/2.99 % (3420227)------------------------------ % 17.92/2.99 % (3420227)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 17.92/2.99 % (3420227)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.92/2.99 % (3420227)CaDiCaL version: 2.1.3 % 17.92/2.99 % (3420227)Termination reason: Inappropriate % 17.92/2.99 % (3420227)Time elapsed: 0.018 s % 17.92/2.99 % (3420227)Peak memory usage: 12 MB % 17.92/2.99 % (3420227)Instructions burned: 75 (million) % 17.92/2.99 % (3420227)------------------------------ % 17.92/2.99 % (3420227)------------------------------ % 17.92/2.99 % (3420241)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=2078857541:fmbsr=2.30978:i=2174_2995 on theBenchmark for (2995ds/2174Mi) % 17.92/2.99 % (3420241)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 17.92/2.99 % (3420241)Terminated due to inappropriate strategy. % 17.92/2.99 % (3420241)------------------------------ % 17.92/2.99 % (3420241)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 17.92/2.99 % (3420241)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.92/2.99 % (3420241)CaDiCaL version: 2.1.3 % 17.92/2.99 % (3420241)Termination reason: Inappropriate % 17.92/2.99 % (3420241)Time elapsed: 0.018 s % 17.92/2.99 % (3420241)Peak memory usage: 12 MB % 17.92/2.99 % (3420241)Instructions burned: 75 (million) % 17.92/2.99 % (3420139)Instruction limit reached! % 17.92/2.99 % (3420139)------------------------------ % 17.92/2.99 % (3420139)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 17.92/2.99 % (3420139)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.92/2.99 % (3420139)CaDiCaL version: 2.1.3 % 17.92/2.99 % (3420139)Termination reason: Instruction limit % 17.92/2.99 % (3420139)Termination phase: Saturation % 17.92/2.99 % (3420139)Time elapsed: 0.269 s % 17.92/2.99 % (3420139)Peak memory usage: 19 MB % 17.92/2.99 % (3420139)Instructions burned: 880 (million) % 17.92/2.99 % (3420241)------------------------------ % 17.92/2.99 % (3420241)------------------------------ % 17.92/2.99 % (3420250)ott-2_1_sil=16000:newcnf=on:random_seed=700781623:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2995 on theBenchmark for (2995ds/869Mi) % 17.92/2.99 % (3420251)ott+10_1_sil=32000:tgt=ground:random_seed=4290151618:i=5114:av=off_2995 on theBenchmark for (2995ds/5114Mi) % 17.92/2.99 % (3420124)Instruction limit reached! % 17.92/2.99 % (3420124)------------------------------ % 17.92/2.99 % (3420124)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 17.92/2.99 % (3420124)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.92/2.99 % (3420124)CaDiCaL version: 2.1.3 % 17.92/2.99 % (3420124)Termination reason: Instruction limit % 17.92/2.99 % (3420124)Termination phase: Saturation % 17.92/2.99 % (3420124)Time elapsed: 0.398 s % 17.92/2.99 % (3420124)Peak memory usage: 23 MB % 17.92/2.99 % (3420124)Instructions burned: 1179 (million) % 17.92/2.99 % (3420264)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=276370899:i=54282_2994 on theBenchmark for (2994ds/54282Mi) % 17.92/2.99 % (3420264)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 17.92/2.99 % (3420264)Terminated due to inappropriate strategy. % 17.92/2.99 % (3420264)------------------------------ % 17.92/2.99 % (3420264)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 17.92/2.99 % (3420264)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.92/2.99 % (3420264)CaDiCaL version: 2.1.3 % 17.92/2.99 % (3420264)Termination reason: Inappropriate % 17.92/2.99 % (3420264)Time elapsed: 0.019 s % 17.92/2.99 % (3420264)Peak memory usage: 12 MB % 17.92/2.99 % (3420264)Instructions burned: 75 (million) % 60.19/8.74 % (3420264)------------------------------ % 60.19/8.74 % (3420264)------------------------------ % 60.19/8.74 % (3420266)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=363313078:i=3512:aac=none_2994 on theBenchmark for (2994ds/3512Mi) % 60.19/8.74 % (3420250)Instruction limit reached! % 60.19/8.74 % (3420250)------------------------------ % 60.19/8.74 % (3420250)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 60.19/8.74 % (3420250)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 60.19/8.74 % (3420250)CaDiCaL version: 2.1.3 % 60.19/8.74 % (3420250)Termination reason: Instruction limit % 60.19/8.74 % (3420250)Termination phase: Saturation % 60.19/8.74 % (3420250)Time elapsed: 0.199 s % 60.19/8.74 % (3420250)Peak memory usage: 16 MB % 60.19/8.74 % (3420250)Instructions burned: 870 (million) % 60.19/8.74 % (3420300)dis+21_1_sil=32000:sas=cadical:random_seed=2670177173:i=3773:amm=off_2993 on theBenchmark for (2993ds/3773Mi) % 60.19/8.74 % (3420209)Instruction limit reached! % 60.19/8.74 % (3420209)------------------------------ % 60.19/8.74 % (3420209)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 60.19/8.74 % (3420209)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 60.19/8.74 % (3420209)CaDiCaL version: 2.1.3 % 60.19/8.74 % (3420209)Termination reason: Instruction limit % 60.19/8.74 % (3420209)Termination phase: Saturation % 60.19/8.74 % (3420209)Time elapsed: 0.464 s % 60.19/8.74 % (3420209)Peak memory usage: 32 MB % 60.19/8.74 % (3420209)Instructions burned: 1472 (million) % 60.19/8.74 % (3420317)ott+11_1_sil=16000:gs=on:random_seed=913103393:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2991 on theBenchmark for (2991ds/2251Mi) % 60.19/8.74 % (3420317)Instruction limit reached! % 60.19/8.74 % (3420317)------------------------------ % 60.19/8.74 % (3420317)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 60.19/8.74 % (3420317)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 60.19/8.74 % (3420317)CaDiCaL version: 2.1.3 % 60.19/8.74 % (3420317)Termination reason: Instruction limit % 60.19/8.74 % (3420317)Termination phase: Saturation % 60.19/8.74 % (3420317)Time elapsed: 0.661 s % 60.19/8.74 % (3420317)Peak memory usage: 27 MB % 60.19/8.74 % (3420317)Instructions burned: 2251 (million) % 60.19/8.74 % (3420319)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=1984969235:fmbsr=1.6:i=67534_2984 on theBenchmark for (2984ds/67534Mi) % 60.19/8.74 % (3420319)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 60.19/8.74 % (3420319)Terminated due to inappropriate strategy. % 60.19/8.74 % (3420319)------------------------------ % 60.19/8.74 % (3420319)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 60.19/8.74 % (3420319)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 60.19/8.74 % (3420319)CaDiCaL version: 2.1.3 % 60.19/8.74 % (3420319)Termination reason: Inappropriate % 60.19/8.74 % (3420319)Time elapsed: 0.019 s % 60.19/8.74 % (3420319)Peak memory usage: 12 MB % 60.19/8.74 % (3420319)Instructions burned: 75 (million) % 60.19/8.74 % (3420319)------------------------------ % 60.19/8.74 % (3420319)------------------------------ % 60.19/8.74 % (3420321)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=934748917:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2984 on theBenchmark for (2984ds/4591Mi) % 60.19/8.74 % (3420266)Instruction limit reached! % 60.19/8.74 % (3420266)------------------------------ % 60.19/8.74 % (3420266)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 60.19/8.74 % (3420266)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 60.19/8.74 % (3420266)CaDiCaL version: 2.1.3 % 60.19/8.74 % (3420266)Termination reason: Instruction limit % 60.19/8.74 % (3420266)Termination phase: Saturation % 60.19/8.74 % (3420266)Time elapsed: 1.040 s % 60.19/8.74 % (3420266)Peak memory usage: 37 MB % 60.19/8.74 % (3420266)Instructions burned: 3512 (million) % 60.19/8.74 % (3420323)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=2003678604:i=29340_2983 on theBenchmark for (2983ds/29340Mi) % 60.19/8.74 % (3420300)Instruction limit reached! % 60.19/8.74 % (3420300)------------------------------ % 60.19/8.74 % (3420300)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 60.19/8.74 % (3420300)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 60.19/8.74 % (3420300)CaDiCaL version: 2.1.3 % 60.19/8.74 % (3420300)Termination reason: Instruction limit % 73.59/10.60 % (3420300)Termination phase: Saturation % 73.59/10.60 % (3420300)Time elapsed: 1.156 s % 73.59/10.60 % (3420300)Peak memory usage: 37 MB % 73.59/10.60 % (3420300)Instructions burned: 3775 (million) % 73.59/10.60 % (3420325)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=1520920852:i=5211_2981 on theBenchmark for (2981ds/5211Mi) % 73.59/10.60 % (3420201)Instruction limit reached! % 73.59/10.60 % (3420201)------------------------------ % 73.59/10.60 % (3420201)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 73.59/10.60 % (3420201)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 73.59/10.60 % (3420201)CaDiCaL version: 2.1.3 % 73.59/10.60 % (3420201)Termination reason: Instruction limit % 73.59/10.60 % (3420201)Termination phase: Saturation % 73.59/10.60 % (3420201)Time elapsed: 1.553 s % 73.59/10.60 % (3420201)Peak memory usage: 47 MB % 73.59/10.60 % (3420201)Instructions burned: 5132 (million) % 73.59/10.60 % (3420327)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=2645012715:i=5497:nm=2_2980 on theBenchmark for (2980ds/5497Mi) % 73.59/10.60 % (3420327)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 73.59/10.60 % (3420327)Terminated due to inappropriate strategy. % 73.59/10.60 % (3420327)------------------------------ % 73.59/10.60 % (3420327)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 73.59/10.60 % (3420327)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 73.59/10.60 % (3420327)CaDiCaL version: 2.1.3 % 73.59/10.60 % (3420327)Termination reason: Inappropriate % 73.59/10.60 % (3420327)Time elapsed: 0.019 s % 73.59/10.60 % (3420327)Peak memory usage: 12 MB % 73.59/10.60 % (3420327)Instructions burned: 76 (million) % 73.59/10.60 % (3420327)------------------------------ % 73.59/10.60 % (3420327)------------------------------ % 73.59/10.60 % (3420329)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=865992706:fmbsr=2:i=46332_2980 on theBenchmark for (2980ds/46332Mi) % 73.59/10.60 % (3420329)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 73.59/10.60 % (3420329)Terminated due to inappropriate strategy. % 73.59/10.60 % (3420329)------------------------------ % 73.59/10.60 % (3420329)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 73.59/10.60 % (3420329)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 73.59/10.60 % (3420329)CaDiCaL version: 2.1.3 % 73.59/10.60 % (3420329)Termination reason: Inappropriate % 73.59/10.60 % (3420329)Time elapsed: 0.018 s % 73.59/10.60 % (3420329)Peak memory usage: 12 MB % 73.59/10.60 % (3420329)Instructions burned: 75 (million) % 73.59/10.60 % (3420329)------------------------------ % 73.59/10.60 % (3420329)------------------------------ % 73.59/10.60 % (3420331)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=2414266271:i=14071_2980 on theBenchmark for (2980ds/14071Mi) % 73.59/10.60 % (3420331)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 73.59/10.60 % (3420331)Terminated due to inappropriate strategy. % 73.59/10.60 % (3420331)------------------------------ % 73.59/10.60 % (3420331)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 73.59/10.60 % (3420331)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 73.59/10.60 % (3420331)CaDiCaL version: 2.1.3 % 73.59/10.60 % (3420331)Termination reason: Inappropriate % 73.59/10.60 % (3420331)Time elapsed: 0.019 s % 73.59/10.60 % (3420331)Peak memory usage: 12 MB % 73.59/10.60 % (3420331)Instructions burned: 75 (million) % 73.59/10.60 % (3420331)------------------------------ % 73.59/10.60 % (3420331)------------------------------ % 73.59/10.60 % (3420333)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=926329542:i=22565:add=on:rawr=on_2979 on theBenchmark for (2979ds/22565Mi) % 73.59/10.60 % (3420251)Instruction limit reached! % 73.59/10.60 % (3420251)------------------------------ % 73.59/10.60 % (3420251)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 73.59/10.60 % (3420251)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 73.59/10.60 % (3420251)CaDiCaL version: 2.1.3 % 73.59/10.60 % (3420251)Termination reason: Instruction limit % 73.59/10.60 % (3420251)Termination phase: Saturation % 73.59/10.60 % (3420251)Time elapsed: 1.656 s % 73.59/10.60 % (3420251)Peak memory usage: 55 MB % 73.59/10.60 % (3420251)Instructions burned: 5117 (million) % 73.59/10.60 % (3420335)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=684147808:i=8173:av=off_2978 on theBenchmark for (2978ds/8173Mi) % 73.59/10.60 % (3420321)Instruction limit reached! % 74.27/10.75 % (3420321)------------------------------ % 74.27/10.75 % (3420321)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 74.27/10.75 % (3420321)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 74.27/10.75 % (3420321)CaDiCaL version: 2.1.3 % 74.27/10.75 % (3420321)Termination reason: Instruction limit % 74.27/10.75 % (3420321)Termination phase: Saturation % 74.27/10.75 % (3420321)Time elapsed: 1.303 s % 74.27/10.75 % (3420321)Peak memory usage: 34 MB % 74.27/10.75 % (3420321)Instructions burned: 4591 (million) % 74.27/10.75 % (3420337)dis+10_16:1_sil=16000:random_seed=1847048051:i=9155:fsr=off_2971 on theBenchmark for (2971ds/9155Mi) % 74.27/10.75 % (3420325)Instruction limit reached! % 74.27/10.75 % (3420325)------------------------------ % 74.27/10.75 % (3420325)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 74.27/10.75 % (3420325)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 74.27/10.75 % (3420325)CaDiCaL version: 2.1.3 % 74.27/10.75 % (3420325)Termination reason: Instruction limit % 74.27/10.75 % (3420325)Termination phase: Saturation % 74.27/10.75 % (3420325)Time elapsed: 1.476 s % 74.27/10.75 % (3420325)Peak memory usage: 44 MB % 74.27/10.75 % (3420325)Instructions burned: 5214 (million) % 74.27/10.75 % (3420339)ott-3_8_sil=64000:random_seed=1066729212:i=20139:bs=on_2966 on theBenchmark for (2966ds/20139Mi) % 74.27/10.75 % (3420335)Instruction limit reached! % 74.27/10.75 % (3420335)------------------------------ % 74.27/10.75 % (3420335)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 74.27/10.75 % (3420335)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 74.27/10.75 % (3420335)CaDiCaL version: 2.1.3 % 74.27/10.75 % (3420335)Termination reason: Instruction limit % 74.27/10.75 % (3420335)Termination phase: Saturation % 74.27/10.75 % (3420335)Time elapsed: 2.759 s % 74.27/10.75 % (3420335)Peak memory usage: 86 MB % 74.27/10.75 % (3420335)Instructions burned: 8173 (million) % 74.27/10.75 % (3420341)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=1096420281:fmbsr=2:i=32576_2950 on theBenchmark for (2950ds/32576Mi) % 74.27/10.75 % (3420341)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 74.27/10.75 % (3420341)Terminated due to inappropriate strategy. % 74.27/10.75 % (3420341)------------------------------ % 74.27/10.75 % (3420341)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 74.27/10.75 % (3420341)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 74.27/10.75 % (3420341)CaDiCaL version: 2.1.3 % 74.27/10.75 % (3420341)Termination reason: Inappropriate % 74.27/10.75 % (3420341)Time elapsed: 0.019 s % 74.27/10.75 % (3420341)Peak memory usage: 12 MB % 74.27/10.75 % (3420341)Instructions burned: 75 (million) % 74.27/10.75 % (3420341)------------------------------ % 74.27/10.75 % (3420341)------------------------------ % 74.27/10.75 % (3420343)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=1147343019:i=11404_2950 on theBenchmark for (2950ds/11404Mi) % 74.27/10.75 % (3420337)Instruction limit reached! % 74.27/10.75 % (3420337)------------------------------ % 74.27/10.75 % (3420337)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 74.27/10.75 % (3420337)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 74.27/10.75 % (3420337)CaDiCaL version: 2.1.3 % 74.27/10.75 % (3420337)Termination reason: Instruction limit % 74.27/10.75 % (3420337)Termination phase: Saturation % 74.27/10.75 % (3420337)Time elapsed: 2.694 s % 74.27/10.75 % (3420337)Peak memory usage: 62 MB % 74.27/10.75 % (3420337)Instructions burned: 9158 (million) % 74.27/10.75 % (3420345)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=4259235824:i=14134_2944 on theBenchmark for (2944ds/14134Mi) % 74.27/10.75 % (3420333)Instruction limit reached! % 74.27/10.75 % (3420333)------------------------------ % 74.27/10.75 % (3420333)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 74.27/10.75 % (3420333)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 74.27/10.75 % (3420333)CaDiCaL version: 2.1.3 % 74.27/10.75 % (3420333)Termination reason: Instruction limit % 74.27/10.75 % (3420333)Termination phase: Saturation % 74.27/10.75 % (3420333)Time elapsed: 4.985 s % 74.27/10.75 % (3420333)Peak memory usage: 23 MB % 74.27/10.75 % (3420333)Instructions burned: 22566 (million) % 74.27/10.75 % (3420347)dis+33_16_sil=32000:sac=on:random_seed=674167123:i=15851:nm=0_2929 on theBenchmark for (2929ds/15851Mi) % 74.27/10.75 % (3420323)Instruction limit reached! % 74.27/10.75 % (3420323)------------------------------ % 74.27/10.75 % (3420323)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 101.69/14.62 % (3420323)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 101.69/14.62 % (3420323)CaDiCaL version: 2.1.3 % 101.69/14.62 % (3420323)Termination reason: Instruction limit % 101.69/14.62 % (3420323)Termination phase: Saturation % 101.69/14.62 % (3420323)Time elapsed: 6.954 s % 101.69/14.62 % (3420323)Peak memory usage: 50 MB % 101.69/14.62 % (3420323)Instructions burned: 29341 (million) % 101.69/14.62 % (3420349)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=3983042830:avsq=on:i=17627:add=on:amm=off_2913 on theBenchmark for (2913ds/17627Mi) % 101.69/14.62 % (3420343)Instruction limit reached! % 101.69/14.62 % (3420343)------------------------------ % 101.69/14.62 % (3420343)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 101.69/14.62 % (3420343)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 101.69/14.62 % (3420343)CaDiCaL version: 2.1.3 % 101.69/14.62 % (3420343)Termination reason: Instruction limit % 101.69/14.62 % (3420343)Termination phase: Saturation % 101.69/14.62 % (3420343)Time elapsed: 3.877 s % 101.69/14.62 % (3420343)Peak memory usage: 102 MB % 101.69/14.62 % (3420343)Instructions burned: 11405 (million) % 101.69/14.62 % (3420351)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=474817919:s2a=on:i=53295_2911 on theBenchmark for (2911ds/53295Mi) % 101.69/14.62 % (3420339)Instruction limit reached! % 101.69/14.62 % (3420339)------------------------------ % 101.69/14.62 % (3420339)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 101.69/14.62 % (3420339)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 101.69/14.62 % (3420339)CaDiCaL version: 2.1.3 % 101.69/14.62 % (3420339)Termination reason: Instruction limit % 101.69/14.62 % (3420339)Termination phase: Saturation % 101.69/14.62 % (3420339)Time elapsed: 5.707 s % 101.69/14.62 % (3420339)Peak memory usage: 98 MB % 101.69/14.62 % (3420339)Instructions burned: 20140 (million) % 101.69/14.62 % (3420353)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=4289123948:i=26857:ins=20_2909 on theBenchmark for (2909ds/26857Mi) % 101.69/14.62 % (3420353)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 101.69/14.62 % (3420353)Terminated due to inappropriate strategy. % 101.69/14.62 % (3420353)------------------------------ % 101.69/14.62 % (3420353)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 101.69/14.62 % (3420353)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 101.69/14.62 % (3420353)CaDiCaL version: 2.1.3 % 101.69/14.62 % (3420353)Termination reason: Inappropriate % 101.69/14.62 % (3420353)Time elapsed: 0.019 s % 101.69/14.62 % (3420353)Peak memory usage: 12 MB % 101.69/14.62 % (3420353)Instructions burned: 75 (million) % 101.69/14.62 % (3420353)------------------------------ % 101.69/14.62 % (3420353)------------------------------ % 101.69/14.62 % (3420355)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=3564596765:i=28120:bs=on:fsr=off_2908 on theBenchmark for (2908ds/28120Mi) % 101.69/14.62 % (3420345)Instruction limit reached! % 101.69/14.62 % (3420345)------------------------------ % 101.69/14.62 % (3420345)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 101.69/14.62 % (3420345)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 101.69/14.62 % (3420345)CaDiCaL version: 2.1.3 % 101.69/14.62 % (3420345)Termination reason: Instruction limit % 101.69/14.62 % (3420345)Termination phase: Saturation % 101.69/14.62 % (3420345)Time elapsed: 4.830 s % 101.69/14.62 % (3420345)Peak memory usage: 112 MB % 101.69/14.62 % (3420345)Instructions burned: 14137 (million) % 101.69/14.62 % (3420357)fmb+10_1_sil=256000:fmbss=7:random_seed=1398080435:fmbsr=1.6:i=182295_2895 on theBenchmark for (2895ds/182295Mi) % 101.69/14.62 % (3420357)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 101.69/14.62 % (3420357)Terminated due to inappropriate strategy. % 101.69/14.62 % (3420357)------------------------------ % 101.69/14.62 % (3420357)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 101.69/14.62 % (3420357)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 101.69/14.62 % (3420357)CaDiCaL version: 2.1.3 % 101.69/14.62 % (3420357)Termination reason: Inappropriate % 101.69/14.62 % (3420357)Time elapsed: 0.019 s % 101.69/14.62 % (3420357)Peak memory usage: 12 MB % 101.69/14.62 % (3420357)Instructions burned: 75 (million) % 101.69/14.62 % (3420357)------------------------------ % 101.69/14.62 % (3420357)------------------------------ % 101.69/14.62 % (3420359)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=649146861:i=44625:gsp=on_2895 on theBenchmark for (2895ds/44625Mi) % 108.52/15.65 % (3420359)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 108.52/15.65 % (3420359)Terminated due to inappropriate strategy. % 108.52/15.65 % (3420359)------------------------------ % 108.52/15.65 % (3420359)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 108.52/15.65 % (3420359)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 108.52/15.65 % (3420359)CaDiCaL version: 2.1.3 % 108.52/15.65 % (3420359)Termination reason: Inappropriate % 108.52/15.65 % (3420359)Time elapsed: 0.019 s % 108.52/15.65 % (3420359)Peak memory usage: 12 MB % 108.52/15.65 % (3420359)Instructions burned: 76 (million) % 108.52/15.65 % (3420359)------------------------------ % 108.52/15.65 % (3420359)------------------------------ % 108.52/15.65 % (3420361)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=4193584479:i=160505_2895 on theBenchmark for (2895ds/160505Mi) % 108.52/15.65 % (3420361)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 108.52/15.65 % (3420361)Terminated due to inappropriate strategy. % 108.52/15.65 % (3420361)------------------------------ % 108.52/15.65 % (3420361)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 108.52/15.65 % (3420361)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 108.52/15.65 % (3420361)CaDiCaL version: 2.1.3 % 108.52/15.65 % (3420361)Termination reason: Inappropriate % 108.52/15.65 % (3420361)Time elapsed: 0.019 s % 108.52/15.65 % (3420361)Peak memory usage: 12 MB % 108.52/15.65 % (3420361)Instructions burned: 75 (million) % 108.52/15.65 % (3420361)------------------------------ % 108.52/15.65 % (3420361)------------------------------ % 108.52/15.65 % (3420363)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=1000704846:fmbsr=1.3:i=225729_2894 on theBenchmark for (2894ds/225729Mi) % 108.52/15.65 % (3420363)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 108.52/15.65 % (3420363)Terminated due to inappropriate strategy. % 108.52/15.65 % (3420363)------------------------------ % 108.52/15.65 % (3420363)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 108.52/15.65 % (3420363)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 108.52/15.65 % (3420363)CaDiCaL version: 2.1.3 % 108.52/15.65 % (3420363)Termination reason: Inappropriate % 108.52/15.65 % (3420363)Time elapsed: 0.019 s % 108.52/15.65 % (3420363)Peak memory usage: 12 MB % 108.52/15.65 % (3420363)Instructions burned: 75 (million) % 108.52/15.65 % (3420363)------------------------------ % 108.52/15.65 % (3420363)------------------------------ % 108.52/15.65 % (3420365)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=214132009:fmbsr=2:i=185024:ins=7_2894 on theBenchmark for (2894ds/185024Mi) % 108.52/15.65 % (3420365)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 108.52/15.65 % (3420365)Terminated due to inappropriate strategy. % 108.52/15.65 % (3420365)------------------------------ % 108.52/15.65 % (3420365)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 108.52/15.65 % (3420365)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 108.52/15.65 % (3420365)CaDiCaL version: 2.1.3 % 108.52/15.65 % (3420365)Termination reason: Inappropriate % 108.52/15.65 % (3420365)Time elapsed: 0.019 s % 108.52/15.65 % (3420365)Peak memory usage: 12 MB % 108.52/15.65 % (3420365)Instructions burned: 75 (million) % 108.52/15.65 % (3420365)------------------------------ % 108.52/15.65 % (3420365)------------------------------ % 108.52/15.65 % (3420367)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=2093061765:rtra=on_2894 on theBenchmark for (2894ds/0Mi) % 108.52/15.65 % (3420347)Instruction limit reached! % 108.52/15.65 % (3420347)------------------------------ % 108.52/15.65 % (3420347)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 108.52/15.65 % (3420347)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 108.52/15.65 % (3420347)CaDiCaL version: 2.1.3 % 108.52/15.65 % (3420347)Termination reason: Instruction limit % 108.52/15.65 % (3420347)Termination phase: Saturation % 108.52/15.65 % (3420347)Time elapsed: 3.568 s % 108.52/15.65 % (3420347)Peak memory usage: 18 MB % 108.52/15.65 % (3420347)Instructions burned: 15855 (million) % 108.52/15.65 % (3420369)% WARNING: option uhcvi not known. % 108.52/15.65 % (3420369)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=798363999:i=271062:add=off:rtra=on:rawr=on_2894 on theBenchmark for (2894ds/271062Mi) % 108.52/15.65 % (3420367)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 114.34/16.45 % (3420367)Terminated due to inappropriate strategy. % 114.34/16.45 % (3420367)------------------------------ % 114.34/16.45 % (3420367)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 114.34/16.45 % (3420367)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 114.34/16.45 % (3420367)CaDiCaL version: 2.1.3 % 114.34/16.45 % (3420367)Termination reason: Inappropriate % 114.34/16.45 % (3420367)Time elapsed: 0.022 s % 114.34/16.45 % (3420367)Peak memory usage: 13 MB % 114.34/16.45 % (3420367)Instructions burned: 82 (million) % 114.34/16.45 % (3420367)------------------------------ % 114.34/16.45 % (3420367)------------------------------ % 114.34/16.45 % (3420371)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1807640056:i=176048:add=on:rtra=on:rawr=on_2893 on theBenchmark for (2893ds/176048Mi) % 114.34/16.45 % (3420349)Instruction limit reached! % 114.34/16.45 % (3420349)------------------------------ % 114.34/16.45 % (3420349)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 114.34/16.45 % (3420349)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 114.34/16.45 % (3420349)CaDiCaL version: 2.1.3 % 114.34/16.45 % (3420349)Termination reason: Instruction limit % 114.34/16.45 % (3420349)Termination phase: Saturation % 114.34/16.45 % (3420349)Time elapsed: 5.449 s % 114.34/16.45 % (3420349)Peak memory usage: 198 MB % 114.34/16.45 % (3420349)Instructions burned: 17629 (million) % 114.34/16.45 % (3420375)dis+10_1_sil=32000:si=on:sp=arity:random_seed=67805630:i=206:fgj=on:rtra=on_2859 on theBenchmark for (2859ds/206Mi) % 114.34/16.45 % (3420375)Instruction limit reached! % 114.34/16.45 % (3420375)------------------------------ % 114.34/16.45 % (3420375)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 114.34/16.45 % (3420375)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 114.34/16.45 % (3420375)CaDiCaL version: 2.1.3 % 114.34/16.45 % (3420375)Termination reason: Instruction limit % 114.34/16.45 % (3420375)Termination phase: Saturation % 114.34/16.45 % (3420375)Time elapsed: 0.067 s % 114.34/16.45 % (3420375)Peak memory usage: 15 MB % 114.34/16.45 % (3420375)Instructions burned: 208 (million) % 114.34/16.45 % (3420401)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=3379031700:i=232:rtra=on_2858 on theBenchmark for (2858ds/232Mi) % 114.34/16.45 % (3420401)Instruction limit reached! % 114.34/16.45 % (3420401)------------------------------ % 114.34/16.45 % (3420401)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 114.34/16.45 % (3420401)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 114.34/16.45 % (3420401)CaDiCaL version: 2.1.3 % 114.34/16.45 % (3420401)Termination reason: Instruction limit % 114.34/16.45 % (3420401)Termination phase: Saturation % 114.34/16.45 % (3420401)Time elapsed: 0.077 s % 114.34/16.45 % (3420401)Peak memory usage: 16 MB % 114.34/16.45 % (3420401)Instructions burned: 232 (million) % 114.34/16.45 % (3420433)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=2130559369:i=262:rtra=on_2857 on theBenchmark for (2857ds/262Mi) % 114.34/16.45 % (3420433)Instruction limit reached! % 114.34/16.45 % (3420433)------------------------------ % 114.34/16.45 % (3420433)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 114.34/16.45 % (3420433)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 114.34/16.45 % (3420433)CaDiCaL version: 2.1.3 % 114.34/16.45 % (3420433)Termination reason: Instruction limit % 114.34/16.45 % (3420433)Termination phase: Saturation % 114.34/16.45 % (3420433)Time elapsed: 0.087 s % 114.34/16.45 % (3420433)Peak memory usage: 16 MB % 114.34/16.45 % (3420433)Instructions burned: 263 (million) % 114.34/16.45 % (3420480)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=3223879292:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2856 on theBenchmark for (2856ds/318Mi) % 114.34/16.45 % (3420480)Instruction limit reached! % 114.34/16.45 % (3420480)------------------------------ % 114.34/16.45 % (3420480)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 114.34/16.45 % (3420480)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 114.34/16.45 % (3420480)CaDiCaL version: 2.1.3 % 114.34/16.45 % (3420480)Termination reason: Instruction limit % 114.34/16.45 % (3420480)Termination phase: Saturation % 114.34/16.45 % (3420480)Time elapsed: 0.109 s % 114.34/16.45 % (3420480)Peak memory usage: 17 MB % 114.34/16.45 % (3420480)Instructions burned: 318 (million) % 114.34/16.45 % (3420529)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=3904711712:i=1428:nm=2:rtra=on_2855 on theBenchmark for (2855ds/1428Mi) % 124.36/17.86 % (3420529)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 124.36/17.86 % (3420529)Terminated due to inappropriate strategy. % 124.36/17.86 % (3420529)------------------------------ % 124.36/17.86 % (3420529)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 124.36/17.86 % (3420529)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 124.36/17.86 % (3420529)CaDiCaL version: 2.1.3 % 124.36/17.86 % (3420529)Termination reason: Inappropriate % 124.36/17.86 % (3420529)Time elapsed: 0.022 s % 124.36/17.86 % (3420529)Peak memory usage: 13 MB % 124.36/17.86 % (3420529)Instructions burned: 81 (million) % 124.36/17.86 % (3420529)------------------------------ % 124.36/17.86 % (3420529)------------------------------ % 124.36/17.86 % (3420544)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=1387271418:i=262:bd=preordered:rtra=on:fsd=on_2854 on theBenchmark for (2854ds/262Mi) % 124.36/17.86 % (3420544)Instruction limit reached! % 124.36/17.86 % (3420544)------------------------------ % 124.36/17.86 % (3420544)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 124.36/17.86 % (3420544)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 124.36/17.86 % (3420544)CaDiCaL version: 2.1.3 % 124.36/17.86 % (3420544)Termination reason: Instruction limit % 124.36/17.86 % (3420544)Termination phase: Saturation % 124.36/17.86 % (3420544)Time elapsed: 0.090 s % 124.36/17.86 % (3420544)Peak memory usage: 16 MB % 124.36/17.86 % (3420544)Instructions burned: 262 (million) % 124.36/17.86 % (3420592)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=1461893433:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2853 on theBenchmark for (2853ds/1368Mi) % 124.36/17.86 % (3420592)Instruction limit reached! % 124.36/17.86 % (3420592)------------------------------ % 124.36/17.86 % (3420592)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 124.36/17.86 % (3420592)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 124.36/17.86 % (3420592)CaDiCaL version: 2.1.3 % 124.36/17.86 % (3420592)Termination reason: Instruction limit % 124.36/17.86 % (3420592)Termination phase: Saturation % 124.36/17.86 % (3420592)Time elapsed: 0.398 s % 124.36/17.86 % (3420592)Peak memory usage: 21 MB % 124.36/17.86 % (3420592)Instructions burned: 1370 (million) % 124.36/17.86 % (3420718)ott-21_1_sil=16000:si=on:fs=off:random_seed=3829719358:i=360:av=off:fsr=off:rtra=on_2849 on theBenchmark for (2849ds/360Mi) % 124.36/17.86 % (3420718)Instruction limit reached! % 124.36/17.86 % (3420718)------------------------------ % 124.36/17.86 % (3420718)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 124.36/17.86 % (3420718)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 124.36/17.86 % (3420718)CaDiCaL version: 2.1.3 % 124.36/17.86 % (3420718)Termination reason: Instruction limit % 124.36/17.86 % (3420718)Termination phase: Saturation % 124.36/17.86 % (3420718)Time elapsed: 0.101 s % 124.36/17.86 % (3420718)Peak memory usage: 16 MB % 124.36/17.86 % (3420718)Instructions burned: 363 (million) % 124.36/17.86 % (3420748)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3353839787:i=954:bd=all:rtra=on_2848 on theBenchmark for (2848ds/954Mi) % 124.36/17.86 % (3420748)Instruction limit reached! % 124.36/17.86 % (3420748)------------------------------ % 124.36/17.86 % (3420748)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 124.36/17.86 % (3420748)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 124.36/17.86 % (3420748)CaDiCaL version: 2.1.3 % 124.36/17.86 % (3420748)Termination reason: Instruction limit % 124.36/17.86 % (3420748)Termination phase: Saturation % 124.36/17.86 % (3420748)Time elapsed: 0.342 s % 124.36/17.86 % (3420748)Peak memory usage: 18 MB % 124.36/17.86 % (3420748)Instructions burned: 954 (million) % 124.36/17.86 % (3420750)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=258574869:fmbsr=1.3:i=1730:ins=25:rtra=on_2845 on theBenchmark for (2845ds/1730Mi) % 124.36/17.86 % (3420750)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 124.36/17.86 % (3420750)Terminated due to inappropriate strategy. % 124.36/17.86 % (3420750)------------------------------ % 124.36/17.86 % (3420750)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 124.36/17.86 % (3420750)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 124.36/17.86 % (3420750)CaDiCaL version: 2.1.3 % 124.36/17.86 % (3420750)Termination reason: Inappropriate % 154.71/22.14 % (3420750)Time elapsed: 0.021 s % 154.71/22.14 % (3420750)Peak memory usage: 13 MB % 154.71/22.14 % (3420750)Instructions burned: 80 (million) % 154.71/22.14 % (3420750)------------------------------ % 154.71/22.14 % (3420750)------------------------------ % 154.71/22.14 % (3420752)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=81996402:i=2358:rtra=on_2844 on theBenchmark for (2844ds/2358Mi) % 154.71/22.14 % (3420355)Instruction limit reached! % 154.71/22.14 % (3420355)------------------------------ % 154.71/22.14 % (3420355)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 154.71/22.14 % (3420355)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 154.71/22.14 % (3420355)CaDiCaL version: 2.1.3 % 154.71/22.14 % (3420355)Termination reason: Instruction limit % 154.71/22.14 % (3420355)Termination phase: Saturation % 154.71/22.14 % (3420355)Time elapsed: 6.575 s % 154.71/22.14 % (3420355)Peak memory usage: 34 MB % 154.71/22.14 % (3420355)Instructions burned: 28122 (million) % 154.71/22.14 % (3420754)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=3560952913:i=1778:ins=1:rtra=on_2843 on theBenchmark for (2843ds/1778Mi) % 154.71/22.14 % (3420754)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 154.71/22.14 % (3420754)Terminated due to inappropriate strategy. % 154.71/22.14 % (3420754)------------------------------ % 154.71/22.14 % (3420754)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 154.71/22.14 % (3420754)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 154.71/22.14 % (3420754)CaDiCaL version: 2.1.3 % 154.71/22.14 % (3420754)Termination reason: Inappropriate % 154.71/22.14 % (3420754)Time elapsed: 0.021 s % 154.71/22.14 % (3420754)Peak memory usage: 13 MB % 154.71/22.14 % (3420754)Instructions burned: 82 (million) % 154.71/22.14 % (3420754)------------------------------ % 154.71/22.14 % (3420754)------------------------------ % 154.71/22.14 % (3420756)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=2104529497:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2842 on theBenchmark for (2842ds/1384Mi) % 154.71/22.14 % (3420756)Instruction limit reached! % 154.71/22.14 % (3420756)------------------------------ % 154.71/22.14 % (3420756)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 154.71/22.14 % (3420756)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 154.71/22.14 % (3420756)CaDiCaL version: 2.1.3 % 154.71/22.14 % (3420756)Termination reason: Instruction limit % 154.71/22.14 % (3420756)Termination phase: Saturation % 154.71/22.14 % (3420756)Time elapsed: 0.370 s % 154.71/22.14 % (3420756)Peak memory usage: 19 MB % 154.71/22.14 % (3420756)Instructions burned: 1386 (million) % 154.71/22.14 % (3420758)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=3230888947:i=1758:kws=inv_precedence:fsr=off:rtra=on_2838 on theBenchmark for (2838ds/1758Mi) % 154.71/22.14 % (3420752)Instruction limit reached! % 154.71/22.14 % (3420752)------------------------------ % 154.71/22.14 % (3420752)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 154.71/22.14 % (3420752)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 154.71/22.14 % (3420752)CaDiCaL version: 2.1.3 % 154.71/22.14 % (3420752)Termination reason: Instruction limit % 154.71/22.14 % (3420752)Termination phase: Saturation % 154.71/22.14 % (3420752)Time elapsed: 0.736 s % 154.71/22.14 % (3420752)Peak memory usage: 31 MB % 154.71/22.14 % (3420752)Instructions burned: 2359 (million) % 154.71/22.14 % (3420760)fmb+10_1_sil=64000:si=on:random_seed=1109458019:i=44122:nm=2:rtra=on:gsp=on_2837 on theBenchmark for (2837ds/44122Mi) % 154.71/22.14 % (3420760)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 154.71/22.14 % (3420760)Terminated due to inappropriate strategy. % 154.71/22.14 % (3420760)------------------------------ % 154.71/22.14 % (3420760)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 154.71/22.14 % (3420760)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 154.71/22.14 % (3420760)CaDiCaL version: 2.1.3 % 154.71/22.14 % (3420760)Termination reason: Inappropriate % 154.71/22.14 % (3420760)Time elapsed: 0.022 s % 154.71/22.14 % (3420760)Peak memory usage: 13 MB % 154.71/22.14 % (3420760)Instructions burned: 83 (million) % 154.71/22.14 % (3420760)------------------------------ % 154.71/22.14 % (3420760)------------------------------ % 154.71/22.14 % (3420762)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=2337222152:i=19030:nm=5:rtra=on_2836 on theBenchmark for (2836ds/19030Mi) % 177.98/25.42 % (3420762)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 177.98/25.42 % (3420762)Terminated due to inappropriate strategy. % 177.98/25.42 % (3420762)------------------------------ % 177.98/25.42 % (3420762)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 177.98/25.42 % (3420762)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 177.98/25.42 % (3420762)CaDiCaL version: 2.1.3 % 177.98/25.42 % (3420762)Termination reason: Inappropriate % 177.98/25.42 % (3420762)Time elapsed: 0.021 s % 177.98/25.42 % (3420762)Peak memory usage: 13 MB % 177.98/25.42 % (3420762)Instructions burned: 81 (million) % 177.98/25.42 % (3420762)------------------------------ % 177.98/25.42 % (3420762)------------------------------ % 177.98/25.42 % (3420764)fmb+10_1_sil=64000:sas=cadical:si=on:fmbss=8:random_seed=504841183:fmbsr=1.7:i=1840:rtra=on_2836 on theBenchmark for (2836ds/1840Mi) % 177.98/25.42 % (3420764)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 177.98/25.42 % (3420764)Terminated due to inappropriate strategy. % 177.98/25.42 % (3420764)------------------------------ % 177.98/25.42 % (3420764)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 177.98/25.42 % (3420764)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 177.98/25.42 % (3420764)CaDiCaL version: 2.1.3 % 177.98/25.42 % (3420764)Termination reason: Inappropriate % 177.98/25.42 % (3420764)Time elapsed: 0.021 s % 177.98/25.42 % (3420764)Peak memory usage: 13 MB % 177.98/25.42 % (3420764)Instructions burned: 81 (million) % 177.98/25.42 % (3420764)------------------------------ % 177.98/25.42 % (3420764)------------------------------ % 177.98/25.42 % (3420766)dis-4_1_sil=16000:drc=ordering:si=on:sp=const_frequency:sac=on:newcnf=on:random_seed=327240514:i=10262:rtra=on_2836 on theBenchmark for (2836ds/10262Mi) % 177.98/25.42 % (3420758)Instruction limit reached! % 177.98/25.42 % (3420758)------------------------------ % 177.98/25.42 % (3420758)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 177.98/25.42 % (3420758)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 177.98/25.42 % (3420758)CaDiCaL version: 2.1.3 % 177.98/25.42 % (3420758)Termination reason: Instruction limit % 177.98/25.42 % (3420758)Termination phase: Saturation % 177.98/25.42 % (3420758)Time elapsed: 0.543 s % 177.98/25.42 % (3420758)Peak memory usage: 26 MB % 177.98/25.42 % (3420758)Instructions burned: 1761 (million) % 177.98/25.42 % (3420768)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:si=on:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2396097026:i=2944:ins=7:rtra=on:fdi=8:gsp=on_2833 on theBenchmark for (2833ds/2944Mi) % 177.98/25.42 % (3420768)Instruction limit reached! % 177.98/25.42 % (3420768)------------------------------ % 177.98/25.42 % (3420768)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 177.98/25.42 % (3420768)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 177.98/25.42 % (3420768)CaDiCaL version: 2.1.3 % 177.98/25.42 % (3420768)Termination reason: Instruction limit % 177.98/25.42 % (3420768)Termination phase: Saturation % 177.98/25.42 % (3420768)Time elapsed: 0.980 s % 177.98/25.42 % (3420768)Peak memory usage: 46 MB % 177.98/25.42 % (3420768)Instructions burned: 2945 (million) % 177.98/25.42 % (3420770)fmb+10_1_sil=16000:sas=cadical:si=on:bce=on:fmbss=77:random_seed=1274002642:i=12648:rtra=on_2823 on theBenchmark for (2823ds/12648Mi) % 177.98/25.42 % (3420770)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 177.98/25.42 % (3420770)Terminated due to inappropriate strategy. % 177.98/25.42 % (3420770)------------------------------ % 177.98/25.42 % (3420770)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 177.98/25.42 % (3420770)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 177.98/25.42 % (3420770)CaDiCaL version: 2.1.3 % 177.98/25.42 % (3420770)Termination reason: Inappropriate % 177.98/25.42 % (3420770)Time elapsed: 0.022 s % 177.98/25.42 % (3420770)Peak memory usage: 13 MB % 177.98/25.42 % (3420770)Instructions burned: 81 (million) % 177.98/25.42 % (3420770)------------------------------ % 177.98/25.42 % (3420770)------------------------------ % 177.98/25.42 % (3420772)fmb+10_1_fmbas=function:sil=32000:sas=cadical:si=on:fmbss=16:random_seed=3704074058:fmbsr=2.30978:i=4348:rtra=on_2823 on theBenchmark for (2823ds/4348Mi) % 177.98/25.42 % (3420772)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 177.98/25.42 % (3420772)Terminated due to inappropriate strategy. % 177.98/25.42 % (3420772)------------------------------ % 177.98/25.42 % (3420772)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 240.80/34.40 % (3420772)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 240.80/34.40 % (3420772)CaDiCaL version: 2.1.3 % 240.80/34.40 % (3420772)Termination reason: Inappropriate % 240.80/34.40 % (3420772)Time elapsed: 0.022 s % 240.80/34.40 % (3420772)Peak memory usage: 13 MB % 240.80/34.40 % (3420772)Instructions burned: 81 (million) % 240.80/34.40 % (3420772)------------------------------ % 240.80/34.40 % (3420772)------------------------------ % 240.80/34.40 % (3420774)ott-2_1_sil=16000:si=on:newcnf=on:random_seed=1897513704:avsq=on:i=1738:avsqr=1,16:kws=inv_arity_squared:rtra=on_2822 on theBenchmark for (2822ds/1738Mi) % 240.80/34.40 % (3420774)Instruction limit reached! % 240.80/34.40 % (3420774)------------------------------ % 240.80/34.40 % (3420774)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 240.80/34.40 % (3420774)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 240.80/34.40 % (3420774)CaDiCaL version: 2.1.3 % 240.80/34.40 % (3420774)Termination reason: Instruction limit % 240.80/34.40 % (3420774)Termination phase: Saturation % 240.80/34.40 % (3420774)Time elapsed: 0.387 s % 240.80/34.40 % (3420774)Peak memory usage: 17 MB % 240.80/34.40 % (3420774)Instructions burned: 1739 (million) % 240.80/34.40 % (3420776)ott+10_1_sil=32000:tgt=ground:si=on:random_seed=335567773:i=10228:av=off:rtra=on_2818 on theBenchmark for (2818ds/10228Mi) % 240.80/34.40 % (3420766)Instruction limit reached! % 240.80/34.40 % (3420766)------------------------------ % 240.80/34.40 % (3420766)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 240.80/34.40 % (3420766)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 240.80/34.40 % (3420766)CaDiCaL version: 2.1.3 % 240.80/34.40 % (3420766)Termination reason: Instruction limit % 240.80/34.40 % (3420766)Termination phase: Saturation % 240.80/34.40 % (3420766)Time elapsed: 3.299 s % 240.80/34.40 % (3420766)Peak memory usage: 79 MB % 240.80/34.40 % (3420766)Instructions burned: 10263 (million) % 240.80/34.40 % (3420778)fmb+10_1_sil=64000:sas=cadical:si=on:bce=on:rp=on:random_seed=2772996555:i=108564:rtra=on_2803 on theBenchmark for (2803ds/108564Mi) % 240.80/34.40 % (3420778)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 240.80/34.40 % (3420778)Terminated due to inappropriate strategy. % 240.80/34.40 % (3420778)------------------------------ % 240.80/34.40 % (3420778)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 240.80/34.40 % (3420778)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 240.80/34.40 % (3420778)CaDiCaL version: 2.1.3 % 240.80/34.40 % (3420778)Termination reason: Inappropriate % 240.80/34.40 % (3420778)Time elapsed: 0.022 s % 240.80/34.40 % (3420778)Peak memory usage: 13 MB % 240.80/34.40 % (3420778)Instructions burned: 82 (million) % 240.80/34.40 % (3420778)------------------------------ % 240.80/34.40 % (3420778)------------------------------ % 240.80/34.40 % (3420780)dis-11_1_sil=16000:si=on:sp=reverse_frequency:alpa=true:random_seed=1023764704:i=7024:aac=none:rtra=on_2802 on theBenchmark for (2802ds/7024Mi) % 240.80/34.40 % (3420776)Instruction limit reached! % 240.80/34.40 % (3420776)------------------------------ % 240.80/34.40 % (3420776)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 240.80/34.40 % (3420776)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 240.80/34.40 % (3420776)CaDiCaL version: 2.1.3 % 234.66/34.40 % (3420776)Termination reason: Instruction limit % 234.66/34.40 % (3420776)Termination phase: Saturation % 234.66/34.40 % (3420776)Time elapsed: 3.726 s % 234.66/34.40 % (3420776)Peak memory usage: 92 MB % 234.66/34.40 % (3420776)Instructions burned: 10229 (million) % 234.66/34.40 % (3420782)dis+21_1_sil=32000:sas=cadical:si=on:random_seed=2091800835:i=7546:rtra=on:amm=off_2781 on theBenchmark for (2781ds/7546Mi) % 234.66/34.40 % (3420780)Instruction limit reached! % 234.66/34.40 % (3420780)------------------------------ % 234.66/34.40 % (3420780)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 234.66/34.40 % (3420780)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 234.66/34.40 % (3420780)CaDiCaL version: 2.1.3 % 234.66/34.40 % (3420780)Termination reason: Instruction limit % 234.66/34.40 % (3420780)Termination phase: Saturation % 234.66/34.40 % (3420780)Time elapsed: 2.256 s % 234.66/34.40 % (3420780)Peak memory usage: 59 MB % 234.66/34.40 % (3420780)Instructions burned: 7026 (million) % 234.66/34.40 % (3420784)ott+11_1_sil=16000:si=on:gs=on:random_seed=4181520181:s2a=on:i=4502:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:rtra=on:fsd=on_2779 on Terminated % 300.07/42.74 % Vampire exiting % 300.07/42.74 Terminated %------------------------------------------------------------------------------