%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWX137_1 : TPTP v9.3.1. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % Computer : n007.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 29 01:46:32 PM UTC 2026 % Result : Timeout 289.83s 41.29s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWX137_1 : TPTP v9.3.1. Released v9.3.0. % 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.11/0.23 % Computer : n007.cluster.edu % 0.11/0.23 % Model : x86_64 x86_64 % 0.11/0.23 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.23 % Memory : 8046.5625MB % 0.11/0.23 % OS : Linux 6.8.0-71-generic % 0.11/0.23 % CPULimit : 300 % 0.11/0.23 % WCLimit : 300 % 0.11/0.23 % DateTime : Mon Sep 28 15:01:10 UTC 2026 % 0.11/0.23 % CPUTime : % 0.11/0.23 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.24/0.28 Running first-order model finding % 0.24/0.29 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 5.28/1.17 % (2479187)Will run a generic schedule for satisfiability detection. % 5.28/1.17 % (2479198)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3545116077:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2998 on theBenchmark for (2998ds/159Mi) % 5.28/1.17 % (2479195)dis+10_1_sil=32000:sp=arity:random_seed=2748293965:i=103:fgj=on_2998 on theBenchmark for (2998ds/103Mi) % 5.28/1.17 % (2479193)% WARNING: option uhcvi not known. % 5.28/1.17 % (2479197)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2334205661:i=131_2998 on theBenchmark for (2998ds/131Mi) % 5.28/1.17 % (2479192)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2557185744_2998 on theBenchmark for (2998ds/0Mi) % 5.28/1.17 % (2479193)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1445874440:i=135531:add=off:rawr=on_2998 on theBenchmark for (2998ds/135531Mi) % 5.28/1.17 % (2479194)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=329070970:i=88024:add=on:rawr=on_2998 on theBenchmark for (2998ds/88024Mi) % 5.28/1.17 % (2479196)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1715485465:i=116_2998 on theBenchmark for (2998ds/116Mi) % 5.28/1.17 % (2479198)Instruction limit reached! % 5.28/1.17 % (2479198)------------------------------ % 5.28/1.17 % (2479198)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.28/1.17 % (2479198)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.28/1.17 % (2479198)CaDiCaL version: 2.1.3 % 5.28/1.17 % (2479198)Termination reason: Instruction limit % 5.28/1.17 % (2479198)Termination phase: Saturation % 5.28/1.17 % (2479198)Time elapsed: 0.066 s % 5.28/1.17 % (2479198)Peak memory usage: 12 MB % 5.28/1.17 % (2479198)Instructions burned: 160 (million) % 5.28/1.17 % (2479206)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3567089378:i=714:nm=2_2997 on theBenchmark for (2997ds/714Mi) % 5.28/1.17 % (2479195)Instruction limit reached! % 5.28/1.17 % (2479195)------------------------------ % 5.28/1.17 % (2479195)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.28/1.17 % (2479195)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.28/1.17 % (2479195)CaDiCaL version: 2.1.3 % 5.28/1.17 % (2479195)Termination reason: Instruction limit % 5.28/1.17 % (2479195)Termination phase: Property scanning % 5.28/1.17 % (2479195)Time elapsed: 0.084 s % 5.28/1.17 % (2479195)Peak memory usage: 10 MB % 5.28/1.17 % (2479195)Instructions burned: 103 (million) % 5.28/1.17 % (2479192)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 5.28/1.17 % (2479192)Terminated due to inappropriate strategy. % 5.28/1.17 % (2479192)------------------------------ % 5.28/1.17 % (2479192)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.28/1.17 % (2479192)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.28/1.17 % (2479192)CaDiCaL version: 2.1.3 % 5.28/1.17 % (2479192)Termination reason: Inappropriate % 5.28/1.17 % (2479192)Time elapsed: 0.095 s % 5.28/1.17 % (2479192)Peak memory usage: 10 MB % 5.28/1.17 % (2479192)Instructions burned: 118 (million) % 5.28/1.17 % (2479196)Instruction limit reached! % 5.28/1.17 % (2479196)------------------------------ % 5.28/1.17 % (2479196)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.28/1.17 % (2479196)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.28/1.17 % (2479196)CaDiCaL version: 2.1.3 % 5.28/1.17 % (2479196)Termination reason: Instruction limit % 5.28/1.17 % (2479196)Termination phase: Property scanning % 5.28/1.17 % (2479196)Time elapsed: 0.095 s % 5.28/1.17 % (2479196)Peak memory usage: 10 MB % 5.28/1.17 % (2479196)Instructions burned: 116 (million) % 5.28/1.17 % (2479192)------------------------------ % 5.28/1.17 % (2479192)------------------------------ % 5.28/1.17 % (2479197)Instruction limit reached! % 5.28/1.17 % (2479197)------------------------------ % 5.28/1.17 % (2479197)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.28/1.17 % (2479197)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.28/1.17 % (2479197)CaDiCaL version: 2.1.3 % 5.28/1.17 % (2479197)Termination reason: Instruction limit % 5.28/1.17 % (2479197)Termination phase: Saturation % 5.28/1.17 % (2479197)Time elapsed: 0.104 s % 5.28/1.17 % (2479197)Peak memory usage: 11 MB % 5.28/1.17 % (2479197)Instructions burned: 132 (million) % 5.28/1.17 % (2479208)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=10700369:i=131:bd=preordered:fsd=on_2997 on theBenchmark for (2997ds/131Mi) % 6.81/1.59 % (2479206)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 6.81/1.59 % (2479206)Terminated due to inappropriate strategy. % 6.81/1.59 % (2479206)------------------------------ % 6.81/1.59 % (2479206)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.81/1.59 % (2479206)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.81/1.59 % (2479206)CaDiCaL version: 2.1.3 % 6.81/1.59 % (2479206)Termination reason: Inappropriate % 6.81/1.59 % (2479206)Time elapsed: 0.049 s % 6.81/1.59 % (2479206)Peak memory usage: 11 MB % 6.81/1.59 % (2479206)Instructions burned: 118 (million) % 6.81/1.59 % (2479206)------------------------------ % 6.81/1.59 % (2479206)------------------------------ % 6.81/1.59 % (2479209)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=1248667572:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2997 on theBenchmark for (2997ds/684Mi) % 6.81/1.59 % (2479210)ott-21_1_sil=16000:fs=off:random_seed=3947175049:i=180:av=off:fsr=off_2997 on theBenchmark for (2997ds/180Mi) % 6.81/1.59 % (2479211)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3435960572:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi) % 6.81/1.59 % (2479213)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3061242381:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi) % 6.81/1.59 % (2479213)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 6.81/1.59 % (2479213)Terminated due to inappropriate strategy. % 6.81/1.59 % (2479213)------------------------------ % 6.81/1.59 % (2479213)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.81/1.59 % (2479213)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.81/1.59 % (2479213)CaDiCaL version: 2.1.3 % 6.81/1.59 % (2479213)Termination reason: Inappropriate % 6.81/1.59 % (2479213)Time elapsed: 0.038 s % 6.81/1.59 % (2479213)Peak memory usage: 10 MB % 6.81/1.59 % (2479213)Instructions burned: 89 (million) % 6.81/1.59 % (2479213)------------------------------ % 6.81/1.59 % (2479213)------------------------------ % 6.81/1.59 % (2479218)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2059138380:i=1179_2996 on theBenchmark for (2996ds/1179Mi) % 6.81/1.59 % (2479208)Instruction limit reached! % 6.81/1.59 % (2479208)------------------------------ % 6.81/1.59 % (2479208)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.81/1.59 % (2479208)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.81/1.59 % (2479208)CaDiCaL version: 2.1.3 % 6.81/1.59 % (2479208)Termination reason: Instruction limit % 6.81/1.59 % (2479208)Termination phase: Saturation % 6.81/1.59 % (2479208)Time elapsed: 0.108 s % 6.81/1.59 % (2479208)Peak memory usage: 11 MB % 6.81/1.59 % (2479208)Instructions burned: 132 (million) % 6.81/1.59 % (2479220)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1425572460:i=889:ins=1_2996 on theBenchmark for (2996ds/889Mi) % 6.81/1.59 % (2479210)Instruction limit reached! % 6.81/1.59 % (2479210)------------------------------ % 6.81/1.59 % (2479210)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.81/1.59 % (2479210)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.81/1.59 % (2479210)CaDiCaL version: 2.1.3 % 6.81/1.59 % (2479210)Termination reason: Instruction limit % 6.81/1.59 % (2479210)Termination phase: Saturation % 6.81/1.59 % (2479210)Time elapsed: 0.142 s % 6.81/1.59 % (2479210)Peak memory usage: 11 MB % 6.81/1.59 % (2479210)Instructions burned: 181 (million) % 6.81/1.59 % (2479222)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=2792827841:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2995 on theBenchmark for (2995ds/692Mi) % 6.81/1.59 % (2479220)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 6.81/1.59 % (2479220)Terminated due to inappropriate strategy. % 6.81/1.59 % (2479220)------------------------------ % 6.81/1.59 % (2479220)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.81/1.59 % (2479220)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.81/1.59 % (2479220)CaDiCaL version: 2.1.3 % 6.81/1.59 % (2479220)Termination reason: Inappropriate % 6.81/1.59 % (2479220)Time elapsed: 0.073 s % 6.81/1.59 % (2479220)Peak memory usage: 10 MB % 23.91/4.00 % (2479220)Instructions burned: 89 (million) % 23.91/4.00 % (2479220)------------------------------ % 23.91/4.00 % (2479220)------------------------------ % 23.91/4.00 % (2479224)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3264546523:i=879:kws=inv_precedence:fsr=off_2995 on theBenchmark for (2995ds/879Mi) % 23.91/4.00 % (2479211)Instruction limit reached! % 23.91/4.00 % (2479211)------------------------------ % 23.91/4.00 % (2479211)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 23.91/4.00 % (2479211)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.91/4.00 % (2479211)CaDiCaL version: 2.1.3 % 23.91/4.00 % (2479211)Termination reason: Instruction limit % 23.91/4.00 % (2479211)Termination phase: Saturation % 23.91/4.00 % (2479211)Time elapsed: 0.359 s % 23.91/4.00 % (2479211)Peak memory usage: 13 MB % 23.91/4.00 % (2479211)Instructions burned: 478 (million) % 23.91/4.00 % (2479226)fmb+10_1_sil=64000:random_seed=1685763358:i=22061:nm=2:gsp=on_2993 on theBenchmark for (2993ds/22061Mi) % 23.91/4.00 % (2479218)Instruction limit reached! % 23.91/4.00 % (2479218)------------------------------ % 23.91/4.00 % (2479218)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 23.91/4.00 % (2479218)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.91/4.00 % (2479218)CaDiCaL version: 2.1.3 % 23.91/4.00 % (2479218)Termination reason: Instruction limit % 23.91/4.00 % (2479218)Termination phase: Saturation % 23.91/4.00 % (2479218)Time elapsed: 0.425 s % 23.91/4.00 % (2479218)Peak memory usage: 16 MB % 23.91/4.00 % (2479218)Instructions burned: 1181 (million) % 23.91/4.00 % (2479226)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 23.91/4.00 % (2479226)Terminated due to inappropriate strategy. % 23.91/4.00 % (2479226)------------------------------ % 23.91/4.00 % (2479226)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 23.91/4.00 % (2479226)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.91/4.00 % (2479226)CaDiCaL version: 2.1.3 % 23.91/4.00 % (2479226)Termination reason: Inappropriate % 23.91/4.00 % (2479226)Time elapsed: 0.096 s % 23.91/4.00 % (2479226)Peak memory usage: 10 MB % 23.91/4.00 % (2479226)Instructions burned: 118 (million) % 23.91/4.00 % (2479226)------------------------------ % 23.91/4.00 % (2479226)------------------------------ % 23.91/4.00 % (2479228)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1214915519:i=9515:nm=5_2992 on theBenchmark for (2992ds/9515Mi) % 23.91/4.00 % (2479229)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2138470693:fmbsr=1.7:i=920_2992 on theBenchmark for (2992ds/920Mi) % 23.91/4.00 % (2479209)Instruction limit reached! % 23.91/4.00 % (2479209)------------------------------ % 23.91/4.00 % (2479209)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 23.91/4.00 % (2479209)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.91/4.00 % (2479209)CaDiCaL version: 2.1.3 % 23.91/4.00 % (2479209)Termination reason: Instruction limit % 23.91/4.00 % (2479209)Termination phase: Saturation % 23.91/4.00 % (2479209)Time elapsed: 0.532 s % 23.91/4.00 % (2479209)Peak memory usage: 15 MB % 23.91/4.00 % (2479209)Instructions burned: 685 (million) % 23.91/4.00 % (2479232)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=259383652:i=5131_2991 on theBenchmark for (2991ds/5131Mi) % 23.91/4.00 % (2479228)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 23.91/4.00 % (2479228)Terminated due to inappropriate strategy. % 23.91/4.00 % (2479228)------------------------------ % 23.91/4.00 % (2479228)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 23.91/4.00 % (2479228)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.91/4.00 % (2479228)CaDiCaL version: 2.1.3 % 23.91/4.00 % (2479228)Termination reason: Inappropriate % 23.91/4.00 % (2479228)Time elapsed: 0.062 s % 23.91/4.00 % (2479228)Peak memory usage: 11 MB % 23.91/4.00 % (2479228)Instructions burned: 118 (million) % 23.91/4.00 % (2479228)------------------------------ % 23.91/4.00 % (2479228)------------------------------ % 23.91/4.00 % (2479222)Instruction limit reached! % 23.91/4.00 % (2479222)------------------------------ % 23.91/4.00 % (2479222)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 23.91/4.00 % (2479222)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.91/4.00 % (2479222)CaDiCaL version: 2.1.3 % 23.91/4.00 % (2479222)Termination reason: Instruction limit % 31.89/4.95 % (2479222)Termination phase: Saturation % 31.89/4.95 % (2479222)Time elapsed: 0.425 s % 31.89/4.95 % (2479222)Peak memory usage: 16 MB % 31.89/4.95 % (2479222)Instructions burned: 692 (million) % 31.89/4.95 % (2479234)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3152795707:i=1472:ins=7:fdi=8:gsp=on_2991 on theBenchmark for (2991ds/1472Mi) % 31.89/4.95 % (2479235)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=4118381625:i=6324_2991 on theBenchmark for (2991ds/6324Mi) % 31.89/4.95 % (2479229)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 31.89/4.95 % (2479229)Terminated due to inappropriate strategy. % 31.89/4.95 % (2479229)------------------------------ % 31.89/4.95 % (2479229)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 31.89/4.95 % (2479229)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.89/4.95 % (2479229)CaDiCaL version: 2.1.3 % 31.89/4.95 % (2479229)Termination reason: Inappropriate % 31.89/4.95 % (2479229)Time elapsed: 0.096 s % 31.89/4.95 % (2479229)Peak memory usage: 10 MB % 31.89/4.95 % (2479229)Instructions burned: 118 (million) % 31.89/4.95 % (2479229)------------------------------ % 31.89/4.95 % (2479229)------------------------------ % 31.89/4.95 % (2479238)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=2990554308:fmbsr=2.30978:i=2174_2990 on theBenchmark for (2990ds/2174Mi) % 31.89/4.95 % (2479235)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 31.89/4.95 % (2479235)Terminated due to inappropriate strategy. % 31.89/4.95 % (2479235)------------------------------ % 31.89/4.95 % (2479235)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 31.89/4.95 % (2479235)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.89/4.95 % (2479235)CaDiCaL version: 2.1.3 % 31.89/4.95 % (2479235)Termination reason: Inappropriate % 31.89/4.95 % (2479235)Time elapsed: 0.059 s % 31.89/4.95 % (2479235)Peak memory usage: 11 MB % 31.89/4.95 % (2479235)Instructions burned: 118 (million) % 31.89/4.95 % (2479235)------------------------------ % 31.89/4.95 % (2479235)------------------------------ % 31.89/4.95 % (2479240)ott-2_1_sil=16000:newcnf=on:random_seed=1723740999:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2990 on theBenchmark for (2990ds/869Mi) % 31.89/4.95 % (2479238)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 31.89/4.95 % (2479238)Terminated due to inappropriate strategy. % 31.89/4.95 % (2479238)------------------------------ % 31.89/4.95 % (2479238)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 31.89/4.95 % (2479238)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.89/4.95 % (2479238)CaDiCaL version: 2.1.3 % 31.89/4.95 % (2479238)Termination reason: Inappropriate % 31.89/4.95 % (2479238)Time elapsed: 0.096 s % 31.89/4.95 % (2479238)Peak memory usage: 10 MB % 31.89/4.95 % (2479238)Instructions burned: 118 (million) % 31.89/4.95 % (2479238)------------------------------ % 31.89/4.95 % (2479238)------------------------------ % 31.89/4.95 % (2479242)ott+10_1_sil=32000:tgt=ground:random_seed=2542136544:i=5114:av=off_2989 on theBenchmark for (2989ds/5114Mi) % 31.89/4.95 % (2479224)Instruction limit reached! % 31.89/4.95 % (2479224)------------------------------ % 31.89/4.95 % (2479224)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 31.89/4.95 % (2479224)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.89/4.95 % (2479224)CaDiCaL version: 2.1.3 % 31.89/4.95 % (2479224)Termination reason: Instruction limit % 31.89/4.95 % (2479224)Termination phase: Saturation % 31.89/4.95 % (2479224)Time elapsed: 0.645 s % 31.89/4.95 % (2479224)Peak memory usage: 13 MB % 31.89/4.95 % (2479224)Instructions burned: 879 (million) % 31.89/4.95 % (2479244)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=3731593665:i=54282_2988 on theBenchmark for (2988ds/54282Mi) % 31.89/4.95 % (2479244)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 31.89/4.95 % (2479244)Terminated due to inappropriate strategy. % 31.89/4.95 % (2479244)------------------------------ % 31.89/4.95 % (2479244)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 31.89/4.95 % (2479244)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.89/4.95 % (2479244)CaDiCaL version: 2.1.3 % 31.89/4.95 % (2479244)Termination reason: Inappropriate % 31.89/4.95 % (2479244)Time elapsed: 0.100 s % 31.89/4.95 % (2479244)Peak memory usage: 10 MB % 31.89/4.95 % (2479244)Instructions burned: 118 (million) % 131.57/18.94 % (2479244)------------------------------ % 131.57/18.94 % (2479244)------------------------------ % 131.57/18.94 % (2479246)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3548785262:i=3512:aac=none_2987 on theBenchmark for (2987ds/3512Mi) % 131.57/18.94 % (2479240)Instruction limit reached! % 131.57/18.94 % (2479240)------------------------------ % 131.57/18.94 % (2479240)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 131.57/18.94 % (2479240)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 131.57/18.94 % (2479240)CaDiCaL version: 2.1.3 % 131.57/18.94 % (2479240)Termination reason: Instruction limit % 131.57/18.94 % (2479240)Termination phase: Saturation % 131.57/18.94 % (2479240)Time elapsed: 0.613 s % 131.57/18.94 % (2479240)Peak memory usage: 17 MB % 131.57/18.94 % (2479240)Instructions burned: 869 (million) % 131.57/18.94 % (2479248)dis+21_1_sil=32000:sas=cadical:random_seed=3014813996:i=3773:amm=off_2984 on theBenchmark for (2984ds/3773Mi) % 131.57/18.94 % (2479234)Instruction limit reached! % 131.57/18.94 % (2479234)------------------------------ % 131.57/18.94 % (2479234)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 131.57/18.94 % (2479234)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 131.57/18.94 % (2479234)CaDiCaL version: 2.1.3 % 131.57/18.94 % (2479234)Termination reason: Instruction limit % 131.57/18.94 % (2479234)Termination phase: Saturation % 131.57/18.94 % (2479234)Time elapsed: 1.079 s % 131.57/18.94 % (2479234)Peak memory usage: 15 MB % 131.57/18.94 % (2479234)Instructions burned: 1473 (million) % 131.57/18.94 % (2479250)ott+11_1_sil=16000:gs=on:random_seed=392741568:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2980 on theBenchmark for (2980ds/2251Mi) % 131.57/18.94 % (2479232)Instruction limit reached! % 131.57/18.94 % (2479232)------------------------------ % 131.57/18.94 % (2479232)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 131.57/18.94 % (2479232)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 131.57/18.94 % (2479232)CaDiCaL version: 2.1.3 % 131.57/18.94 % (2479232)Termination reason: Instruction limit % 131.57/18.94 % (2479232)Termination phase: Saturation % 131.57/18.94 % (2479232)Time elapsed: 1.919 s % 131.57/18.94 % (2479232)Peak memory usage: 15 MB % 131.57/18.94 % (2479232)Instructions burned: 5133 (million) % 131.57/18.94 % (2479252)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=1082268651:fmbsr=1.6:i=67534_2972 on theBenchmark for (2972ds/67534Mi) % 131.57/18.94 % (2479252)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 131.57/18.94 % (2479252)Terminated due to inappropriate strategy. % 131.57/18.94 % (2479252)------------------------------ % 131.57/18.94 % (2479252)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 131.57/18.94 % (2479252)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 131.57/18.94 % (2479252)CaDiCaL version: 2.1.3 % 131.57/18.94 % (2479252)Termination reason: Inappropriate % 131.57/18.94 % (2479252)Time elapsed: 0.054 s % 131.57/18.94 % (2479252)Peak memory usage: 11 MB % 131.57/18.94 % (2479252)Instructions burned: 118 (million) % 131.57/18.94 % (2479252)------------------------------ % 131.57/18.94 % (2479252)------------------------------ % 131.57/18.94 % (2479254)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=164592764:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2971 on theBenchmark for (2971ds/4591Mi) % 131.57/18.94 % (2479250)Instruction limit reached! % 131.57/18.94 % (2479250)------------------------------ % 131.57/18.94 % (2479250)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 131.57/18.94 % (2479250)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 131.57/18.94 % (2479250)CaDiCaL version: 2.1.3 % 131.57/18.94 % (2479250)Termination reason: Instruction limit % 131.57/18.94 % (2479250)Termination phase: Saturation % 131.57/18.94 % (2479250)Time elapsed: 1.419 s % 131.57/18.94 % (2479250)Peak memory usage: 16 MB % 131.57/18.94 % (2479250)Instructions burned: 2252 (million) % 131.57/18.94 % (2479256)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=1925350773:i=29340_2965 on theBenchmark for (2965ds/29340Mi) % 131.57/18.94 % (2479246)Instruction limit reached! % 131.57/18.94 % (2479246)------------------------------ % 131.57/18.94 % (2479246)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 131.57/18.94 % (2479246)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 131.57/18.94 % (2479246)CaDiCaL version: 2.1.3 % 154.58/22.20 % (2479246)Termination reason: Instruction limit % 154.58/22.20 % (2479246)Termination phase: Saturation % 154.58/22.20 % (2479246)Time elapsed: 2.381 s % 154.58/22.20 % (2479246)Peak memory usage: 15 MB % 154.58/22.20 % (2479246)Instructions burned: 3513 (million) % 154.58/22.20 % (2479258)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=74672727:i=5211_2962 on theBenchmark for (2962ds/5211Mi) % 154.58/22.20 % (2479248)Instruction limit reached! % 154.58/22.20 % (2479248)------------------------------ % 154.58/22.20 % (2479248)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 154.58/22.20 % (2479248)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 154.58/22.20 % (2479248)CaDiCaL version: 2.1.3 % 154.58/22.20 % (2479248)Termination reason: Instruction limit % 154.58/22.20 % (2479248)Termination phase: Saturation % 154.58/22.20 % (2479248)Time elapsed: 2.728 s % 154.58/22.20 % (2479248)Peak memory usage: 15 MB % 154.58/22.20 % (2479248)Instructions burned: 3774 (million) % 154.58/22.20 % (2479260)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=4240258747:i=5497:nm=2_2956 on theBenchmark for (2956ds/5497Mi) % 154.58/22.20 % (2479260)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 154.58/22.20 % (2479260)Terminated due to inappropriate strategy. % 154.58/22.20 % (2479260)------------------------------ % 154.58/22.20 % (2479260)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 154.58/22.20 % (2479260)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 154.58/22.20 % (2479260)CaDiCaL version: 2.1.3 % 154.58/22.20 % (2479260)Termination reason: Inappropriate % 154.58/22.20 % (2479260)Time elapsed: 0.061 s % 154.58/22.20 % (2479260)Peak memory usage: 11 MB % 154.58/22.20 % (2479260)Instructions burned: 118 (million) % 154.58/22.20 % (2479260)------------------------------ % 154.58/22.20 % (2479260)------------------------------ % 154.58/22.20 % (2479262)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=4006913420:fmbsr=2:i=46332_2955 on theBenchmark for (2955ds/46332Mi) % 154.58/22.20 % (2479262)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 154.58/22.20 % (2479262)Terminated due to inappropriate strategy. % 154.58/22.20 % (2479262)------------------------------ % 154.58/22.20 % (2479262)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 154.58/22.20 % (2479262)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 154.58/22.20 % (2479262)CaDiCaL version: 2.1.3 % 154.58/22.20 % (2479262)Termination reason: Inappropriate % 154.58/22.20 % (2479262)Time elapsed: 0.060 s % 154.58/22.20 % (2479262)Peak memory usage: 11 MB % 154.58/22.20 % (2479262)Instructions burned: 118 (million) % 154.58/22.20 % (2479262)------------------------------ % 154.58/22.20 % (2479262)------------------------------ % 154.58/22.20 % (2479264)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=577640895:i=14071_2954 on theBenchmark for (2954ds/14071Mi) % 154.58/22.20 % (2479242)Instruction limit reached! % 154.58/22.20 % (2479242)------------------------------ % 154.58/22.20 % (2479242)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 154.58/22.20 % (2479242)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 154.58/22.20 % (2479242)CaDiCaL version: 2.1.3 % 154.58/22.20 % (2479242)Termination reason: Instruction limit % 154.58/22.20 % (2479242)Termination phase: Saturation % 154.58/22.20 % (2479242)Time elapsed: 3.543 s % 154.58/22.20 % (2479242)Peak memory usage: 15 MB % 154.58/22.20 % (2479242)Instructions burned: 5116 (million) % 154.58/22.20 % (2479264)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 154.58/22.20 % (2479264)Terminated due to inappropriate strategy. % 154.58/22.20 % (2479264)------------------------------ % 154.58/22.20 % (2479264)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 154.58/22.20 % (2479264)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 154.58/22.20 % (2479264)CaDiCaL version: 2.1.3 % 154.58/22.20 % (2479264)Termination reason: Inappropriate % 154.58/22.20 % (2479264)Time elapsed: 0.060 s % 154.58/22.20 % (2479264)Peak memory usage: 11 MB % 154.58/22.20 % (2479264)Instructions burned: 118 (million) % 154.58/22.20 % (2479264)------------------------------ % 154.58/22.20 % (2479264)------------------------------ % 154.58/22.20 % (2479266)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2215625686:i=22565:add=on:rawr=on_2953 on theBenchmark for (2953ds/22565Mi) % 154.58/22.20 % (2479267)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=3440569731:i=8173:av=off_2953 on theBenchmark for (2953ds/8173Mi) % 159.10/22.83 % (2479254)Instruction limit reached! % 159.10/22.83 % (2479254)------------------------------ % 159.10/22.83 % (2479254)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 159.10/22.83 % (2479254)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 159.10/22.83 % (2479254)CaDiCaL version: 2.1.3 % 159.10/22.83 % (2479254)Termination reason: Instruction limit % 159.10/22.83 % (2479254)Termination phase: Saturation % 159.10/22.83 % (2479254)Time elapsed: 2.190 s % 159.10/22.83 % (2479254)Peak memory usage: 39 MB % 159.10/22.83 % (2479254)Instructions burned: 4591 (million) % 159.10/22.83 % (2479270)dis+10_16:1_sil=16000:random_seed=3990709132:i=9155:fsr=off_2949 on theBenchmark for (2949ds/9155Mi) % 159.10/22.83 % (2479258)Instruction limit reached! % 159.10/22.83 % (2479258)------------------------------ % 159.10/22.83 % (2479258)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 159.10/22.83 % (2479258)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 159.10/22.83 % (2479258)CaDiCaL version: 2.1.3 % 159.10/22.83 % (2479258)Termination reason: Instruction limit % 159.10/22.83 % (2479258)Termination phase: Saturation % 159.10/22.83 % (2479258)Time elapsed: 3.804 s % 159.10/22.83 % (2479258)Peak memory usage: 17 MB % 159.10/22.83 % (2479258)Instructions burned: 5212 (million) % 159.10/22.83 % (2479280)ott-3_8_sil=64000:random_seed=2210523320:i=20139:bs=on_2924 on theBenchmark for (2924ds/20139Mi) % 159.10/22.83 % (2479270)Instruction limit reached! % 159.10/22.83 % (2479270)------------------------------ % 159.10/22.83 % (2479270)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 159.10/22.83 % (2479270)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 159.10/22.83 % (2479270)CaDiCaL version: 2.1.3 % 159.10/22.83 % (2479270)Termination reason: Instruction limit % 159.10/22.83 % (2479270)Termination phase: Saturation % 159.10/22.83 % (2479270)Time elapsed: 3.405 s % 159.10/22.83 % (2479270)Peak memory usage: 16 MB % 159.10/22.83 % (2479270)Instructions burned: 9158 (million) % 159.10/22.83 % (2479288)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=1243506288:fmbsr=2:i=32576_2915 on theBenchmark for (2915ds/32576Mi) % 159.10/22.83 % (2479288)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 159.10/22.83 % (2479288)Terminated due to inappropriate strategy. % 159.10/22.83 % (2479288)------------------------------ % 159.10/22.83 % (2479288)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 159.10/22.83 % (2479288)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 159.10/22.83 % (2479288)CaDiCaL version: 2.1.3 % 159.10/22.83 % (2479288)Termination reason: Inappropriate % 159.10/22.83 % (2479288)Time elapsed: 0.053 s % 159.10/22.83 % (2479288)Peak memory usage: 10 MB % 159.10/22.83 % (2479288)Instructions burned: 118 (million) % 159.10/22.83 % (2479288)------------------------------ % 159.10/22.83 % (2479288)------------------------------ % 159.10/22.83 % (2479290)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=3420834290:i=11404_2914 on theBenchmark for (2914ds/11404Mi) % 159.10/22.83 % (2479267)Instruction limit reached! % 159.10/22.83 % (2479267)------------------------------ % 159.10/22.83 % (2479267)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 159.10/22.83 % (2479267)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 159.10/22.83 % (2479267)CaDiCaL version: 2.1.3 % 159.10/22.83 % (2479267)Termination reason: Instruction limit % 159.10/22.84 % (2479267)Termination phase: Saturation % 159.10/22.84 % (2479267)Time elapsed: 5.782 s % 159.10/22.84 % (2479267)Peak memory usage: 16 MB % 159.10/22.84 % (2479267)Instructions burned: 8174 (million) % 159.10/22.84 % (2479294)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=1909921462:i=14134_2895 on theBenchmark for (2895ds/14134Mi) % 159.10/22.84 % (2479290)Instruction limit reached! % 159.10/22.84 % (2479290)------------------------------ % 159.10/22.84 % (2479290)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 159.10/22.84 % (2479290)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 159.10/22.84 % (2479290)CaDiCaL version: 2.1.3 % 159.10/22.84 % (2479290)Termination reason: Instruction limit % 159.10/22.84 % (2479290)Termination phase: Saturation % 159.10/22.84 % (2479290)Time elapsed: 4.141 s % 159.10/22.84 % (2479290)Peak memory usage: 16 MB % 159.10/22.84 % (2479290)Instructions burned: 11404 (million) % 159.10/22.84 % (2479302)dis+33_16_sil=32000:sac=on:random_seed=3423198299:i=15851:nm=0_2872 on theBenchmark for (2872ds/15851Mi) % 159.10/22.84 % (2479302)Instruction limit reached! % 159.10/22.84 % (2479302)------------------------------ % 186.89/26.80 % (2479302)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 186.89/26.80 % (2479302)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 186.89/26.80 % (2479302)CaDiCaL version: 2.1.3 % 186.89/26.80 % (2479302)Termination reason: Instruction limit % 186.89/26.80 % (2479302)Termination phase: Saturation % 186.89/26.80 % (2479302)Time elapsed: 5.897 s % 186.89/26.80 % (2479302)Peak memory usage: 20 MB % 186.89/26.80 % (2479302)Instructions burned: 15854 (million) % 186.89/26.80 % (2479308)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=3426658491:avsq=on:i=17627:add=on:amm=off_2813 on theBenchmark for (2813ds/17627Mi) % 186.89/26.80 % (2479266)Instruction limit reached! % 186.89/26.80 % (2479266)------------------------------ % 186.89/26.80 % (2479266)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 186.89/26.80 % (2479266)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 186.89/26.80 % (2479266)CaDiCaL version: 2.1.3 % 186.89/26.80 % (2479266)Termination reason: Instruction limit % 186.89/26.80 % (2479266)Termination phase: Saturation % 186.89/26.80 % (2479266)Time elapsed: 15.347 s % 186.89/26.80 % (2479266)Peak memory usage: 17 MB % 186.89/26.80 % (2479266)Instructions burned: 22565 (million) % 186.89/26.80 % (2479324)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=688811651:s2a=on:i=53295_2800 on theBenchmark for (2800ds/53295Mi) % 186.89/26.80 % (2479294)Instruction limit reached! % 186.89/26.80 % (2479294)------------------------------ % 186.89/26.80 % (2479294)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 186.89/26.80 % (2479294)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 186.89/26.80 % (2479294)CaDiCaL version: 2.1.3 % 186.89/26.80 % (2479294)Termination reason: Instruction limit % 186.89/26.80 % (2479294)Termination phase: Saturation % 186.89/26.80 % (2479294)Time elapsed: 9.955 s % 186.89/26.80 % (2479294)Peak memory usage: 16 MB % 186.89/26.80 % (2479294)Instructions burned: 14135 (million) % 186.89/26.80 % (2479330)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=3350972800:i=26857:ins=20_2795 on theBenchmark for (2795ds/26857Mi) % 186.89/26.80 % (2479330)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 186.89/26.80 % (2479330)Terminated due to inappropriate strategy. % 186.89/26.80 % (2479330)------------------------------ % 186.89/26.80 % (2479330)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 186.89/26.80 % (2479330)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 186.89/26.80 % (2479330)CaDiCaL version: 2.1.3 % 186.89/26.80 % (2479330)Termination reason: Inappropriate % 186.89/26.80 % (2479330)Time elapsed: 0.055 s % 186.89/26.80 % (2479330)Peak memory usage: 11 MB % 186.89/26.80 % (2479330)Instructions burned: 118 (million) % 186.89/26.80 % (2479330)------------------------------ % 186.89/26.80 % (2479330)------------------------------ % 186.89/26.80 % (2479332)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=3101347585:i=28120:bs=on:fsr=off_2794 on theBenchmark for (2794ds/28120Mi) % 186.89/26.80 % (2479280)Instruction limit reached! % 186.89/26.80 % (2479280)------------------------------ % 186.89/26.80 % (2479280)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 186.89/26.80 % (2479280)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 186.89/26.80 % (2479280)CaDiCaL version: 2.1.3 % 186.89/26.80 % (2479280)Termination reason: Instruction limit % 186.89/26.80 % (2479280)Termination phase: Saturation % 186.89/26.80 % (2479280)Time elapsed: 14.156 s % 186.89/26.80 % (2479280)Peak memory usage: 18 MB % 186.89/26.80 % (2479280)Instructions burned: 20140 (million) % 186.89/26.80 % (2479347)fmb+10_1_sil=256000:fmbss=7:random_seed=3097637261:fmbsr=1.6:i=182295_2782 on theBenchmark for (2782ds/182295Mi) % 186.89/26.80 % (2479347)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 186.89/26.80 % (2479347)Terminated due to inappropriate strategy. % 186.89/26.80 % (2479347)------------------------------ % 186.89/26.80 % (2479347)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 186.89/26.80 % (2479347)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 186.89/26.80 % (2479347)CaDiCaL version: 2.1.3 % 186.89/26.80 % (2479347)Termination reason: Inappropriate % 186.89/26.80 % (2479347)Time elapsed: 0.097 s % 186.89/26.80 % (2479347)Peak memory usage: 10 MB % 186.89/26.80 % (2479347)Instructions burned: 118 (million) % 186.89/26.80 % (2479347)------------------------------ % 186.89/26.80 % (2479347)------------------------------ % 186.89/26.80 % (2479352)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=2989573394:i=44625:gsp=on_2781 on theBenchmark for (2781ds/44625Mi) % 197.30/28.17 % (2479352)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 197.30/28.17 % (2479352)Terminated due to inappropriate strategy. % 197.30/28.17 % (2479352)------------------------------ % 197.30/28.17 % (2479352)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 197.30/28.17 % (2479352)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 197.30/28.17 % (2479352)CaDiCaL version: 2.1.3 % 197.30/28.17 % (2479352)Termination reason: Inappropriate % 197.30/28.17 % (2479352)Time elapsed: 0.107 s % 197.30/28.17 % (2479352)Peak memory usage: 11 MB % 197.30/28.17 % (2479352)Instructions burned: 118 (million) % 197.30/28.17 % (2479352)------------------------------ % 197.30/28.17 % (2479352)------------------------------ % 197.30/28.17 % (2479356)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=3524830902:i=160505_2779 on theBenchmark for (2779ds/160505Mi) % 197.30/28.17 % (2479356)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 197.30/28.17 % (2479356)Terminated due to inappropriate strategy. % 197.30/28.17 % (2479356)------------------------------ % 197.30/28.17 % (2479356)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 197.30/28.17 % (2479356)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 197.30/28.17 % (2479356)CaDiCaL version: 2.1.3 % 197.30/28.17 % (2479356)Termination reason: Inappropriate % 197.30/28.17 % (2479356)Time elapsed: 0.055 s % 197.30/28.17 % (2479356)Peak memory usage: 11 MB % 197.30/28.17 % (2479356)Instructions burned: 118 (million) % 197.30/28.17 % (2479356)------------------------------ % 197.30/28.17 % (2479356)------------------------------ % 197.30/28.17 % (2479360)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=4033339897:fmbsr=1.3:i=225729_2779 on theBenchmark for (2779ds/225729Mi) % 197.30/28.17 % (2479360)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 197.30/28.17 % (2479360)Terminated due to inappropriate strategy. % 197.30/28.17 % (2479360)------------------------------ % 197.30/28.17 % (2479360)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 197.30/28.17 % (2479360)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 197.30/28.17 % (2479360)CaDiCaL version: 2.1.3 % 197.30/28.17 % (2479360)Termination reason: Inappropriate % 197.30/28.17 % (2479360)Time elapsed: 0.096 s % 197.30/28.17 % (2479360)Peak memory usage: 10 MB % 197.30/28.17 % (2479360)Instructions burned: 118 (million) % 197.30/28.17 % (2479360)------------------------------ % 197.30/28.17 % (2479360)------------------------------ % 197.30/28.17 % (2479364)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=1503183984:fmbsr=2:i=185024:ins=7_2777 on theBenchmark for (2777ds/185024Mi) % 197.30/28.17 % (2479364)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 197.30/28.17 % (2479364)Terminated due to inappropriate strategy. % 197.30/28.17 % (2479364)------------------------------ % 197.30/28.17 % (2479364)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 197.30/28.17 % (2479364)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 197.30/28.17 % (2479364)CaDiCaL version: 2.1.3 % 197.30/28.17 % (2479364)Termination reason: Inappropriate % 197.30/28.17 % (2479364)Time elapsed: 0.097 s % 197.30/28.17 % (2479364)Peak memory usage: 10 MB % 197.30/28.17 % (2479364)Instructions burned: 118 (million) % 197.30/28.17 % (2479364)------------------------------ % 197.30/28.17 % (2479364)------------------------------ % 197.30/28.17 % (2479367)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=1831502783:rtra=on_2776 on theBenchmark for (2776ds/0Mi) % 197.30/28.17 % (2479367)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 197.30/28.17 % (2479367)Terminated due to inappropriate strategy. % 197.30/28.17 % (2479367)------------------------------ % 197.30/28.17 % (2479367)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 197.30/28.17 % (2479367)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 197.30/28.17 % (2479367)CaDiCaL version: 2.1.3 % 197.30/28.17 % (2479367)Termination reason: Inappropriate % 197.30/28.17 % (2479367)Time elapsed: 0.096 s % 197.30/28.17 % (2479367)Peak memory usage: 10 MB % 197.30/28.17 % (2479367)Instructions burned: 118 (million) % 197.30/28.17 % (2479367)------------------------------ % 197.30/28.17 % (2479367)------------------------------ % 197.30/28.17 % (2479371)% WARNING: option uhcvi not known. % 197.30/28.17 % (2479371)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3346314715:i=271062:add=off:rtra=on:rawr=on_2774 on theBenchmark for (2774ds/271062Mi) % 206.43/29.56 % (2479256)Instruction limit reached! % 206.43/29.56 % (2479256)------------------------------ % 206.43/29.56 % (2479256)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 206.43/29.56 % (2479256)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 206.43/29.56 % (2479256)CaDiCaL version: 2.1.3 % 206.43/29.56 % (2479256)Termination reason: Instruction limit % 206.43/29.56 % (2479256)Termination phase: Saturation % 206.43/29.56 % (2479256)Time elapsed: 19.554 s % 206.43/29.56 % (2479256)Peak memory usage: 16 MB % 206.43/29.56 % (2479256)Instructions burned: 29340 (million) % 206.43/29.56 % (2479380)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2369397700:i=176048:add=on:rtra=on:rawr=on_2769 on theBenchmark for (2769ds/176048Mi) % 206.43/29.56 % (2479308)Instruction limit reached! % 206.43/29.56 % (2479308)------------------------------ % 206.43/29.56 % (2479308)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 206.43/29.56 % (2479308)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 206.43/29.56 % (2479308)CaDiCaL version: 2.1.3 % 206.43/29.56 % (2479308)Termination reason: Instruction limit % 206.43/29.56 % (2479308)Termination phase: Saturation % 206.43/29.56 % (2479308)Time elapsed: 7.299 s % 206.43/29.56 % (2479308)Peak memory usage: 92 MB % 206.43/29.56 % (2479308)Instructions burned: 17628 (million) % 206.43/29.56 % (2479408)dis+10_1_sil=32000:si=on:sp=arity:random_seed=2701995666:i=206:fgj=on:rtra=on_2740 on theBenchmark for (2740ds/206Mi) % 206.43/29.56 % (2479408)Instruction limit reached! % 206.43/29.56 % (2479408)------------------------------ % 206.43/29.56 % (2479408)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 206.43/29.56 % (2479408)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 206.43/29.56 % (2479408)CaDiCaL version: 2.1.3 % 206.43/29.56 % (2479408)Termination reason: Instruction limit % 206.43/29.56 % (2479408)Termination phase: Saturation % 206.43/29.56 % (2479408)Time elapsed: 0.092 s % 206.43/29.56 % (2479408)Peak memory usage: 13 MB % 206.43/29.56 % (2479408)Instructions burned: 208 (million) % 206.43/29.56 % (2479410)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=4029082390:i=232:rtra=on_2739 on theBenchmark for (2739ds/232Mi) % 206.43/29.56 % (2479410)Instruction limit reached! % 206.43/29.56 % (2479410)------------------------------ % 206.43/29.56 % (2479410)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 206.43/29.56 % (2479410)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 206.43/29.56 % (2479410)CaDiCaL version: 2.1.3 % 206.43/29.56 % (2479410)Termination reason: Instruction limit % 206.43/29.56 % (2479410)Termination phase: Saturation % 206.43/29.56 % (2479410)Time elapsed: 0.095 s % 206.43/29.56 % (2479410)Peak memory usage: 12 MB % 206.43/29.56 % (2479410)Instructions burned: 233 (million) % 206.43/29.56 % (2479413)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=2042869350:i=262:rtra=on_2737 on theBenchmark for (2737ds/262Mi) % 206.43/29.56 % (2479413)Instruction limit reached! % 206.43/29.56 % (2479413)------------------------------ % 206.43/29.56 % (2479413)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 206.43/29.56 % (2479413)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 206.43/29.56 % (2479413)CaDiCaL version: 2.1.3 % 206.43/29.56 % (2479413)Termination reason: Instruction limit % 206.43/29.56 % (2479413)Termination phase: Saturation % 206.43/29.56 % (2479413)Time elapsed: 0.112 s % 206.43/29.56 % (2479413)Peak memory usage: 14 MB % 206.43/29.56 % (2479413)Instructions burned: 264 (million) % 206.43/29.56 % (2479416)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=714501039:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2736 on theBenchmark for (2736ds/318Mi) % 206.43/29.56 % (2479416)Instruction limit reached! % 206.43/29.56 % (2479416)------------------------------ % 206.43/29.56 % (2479416)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 206.43/29.56 % (2479416)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 206.43/29.56 % (2479416)CaDiCaL version: 2.1.3 % 206.43/29.56 % (2479416)Termination reason: Instruction limit % 206.43/29.56 % (2479416)Termination phase: Saturation % 206.43/29.56 % (2479416)Time elapsed: 0.127 s % 206.43/29.56 % (2479416)Peak memory usage: 14 MB % 206.43/29.56 % (2479416)Instructions burned: 320 (million) % 206.43/29.56 % (2479419)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=1215718872:i=1428:nm=2:rtra=on_2735 on theBenchmark for (2735ds/1428Mi) % 226.68/32.40 % (2479419)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 226.68/32.40 % (2479419)Terminated due to inappropriate strategy. % 226.68/32.40 % (2479419)------------------------------ % 226.68/32.40 % (2479419)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 226.68/32.40 % (2479419)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 226.68/32.40 % (2479419)CaDiCaL version: 2.1.3 % 226.68/32.40 % (2479419)Termination reason: Inappropriate % 226.68/32.40 % (2479419)Time elapsed: 0.046 s % 226.68/32.40 % (2479419)Peak memory usage: 10 MB % 226.68/32.40 % (2479419)Instructions burned: 118 (million) % 226.68/32.40 % (2479419)------------------------------ % 226.68/32.40 % (2479419)------------------------------ % 226.68/32.40 % (2479422)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=1806906711:i=262:bd=preordered:rtra=on:fsd=on_2734 on theBenchmark for (2734ds/262Mi) % 226.68/32.40 % (2479422)Instruction limit reached! % 226.68/32.40 % (2479422)------------------------------ % 226.68/32.40 % (2479422)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 226.68/32.40 % (2479422)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 226.68/32.40 % (2479422)CaDiCaL version: 2.1.3 % 226.68/32.40 % (2479422)Termination reason: Instruction limit % 226.68/32.40 % (2479422)Termination phase: Saturation % 226.68/32.40 % (2479422)Time elapsed: 0.117 s % 226.68/32.40 % (2479422)Peak memory usage: 13 MB % 226.68/32.40 % (2479422)Instructions burned: 262 (million) % 226.68/32.40 % (2479424)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=3368265477:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2733 on theBenchmark for (2733ds/1368Mi) % 226.68/32.40 % (2479424)Instruction limit reached! % 226.68/32.40 % (2479424)------------------------------ % 226.68/32.40 % (2479424)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 226.68/32.40 % (2479424)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 226.68/32.40 % (2479424)CaDiCaL version: 2.1.3 % 226.68/32.40 % (2479424)Termination reason: Instruction limit % 226.68/32.40 % (2479424)Termination phase: Saturation % 226.68/32.40 % (2479424)Time elapsed: 0.544 s % 226.68/32.40 % (2479424)Peak memory usage: 16 MB % 226.68/32.40 % (2479424)Instructions burned: 1369 (million) % 226.68/32.40 % (2479428)ott-21_1_sil=16000:si=on:fs=off:random_seed=2439695553:i=360:av=off:fsr=off:rtra=on_2727 on theBenchmark for (2727ds/360Mi) % 226.68/32.40 % (2479428)Instruction limit reached! % 226.68/32.40 % (2479428)------------------------------ % 226.68/32.40 % (2479428)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 226.68/32.40 % (2479428)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 226.68/32.40 % (2479428)CaDiCaL version: 2.1.3 % 226.68/32.40 % (2479428)Termination reason: Instruction limit % 226.68/32.40 % (2479428)Termination phase: Saturation % 226.68/32.40 % (2479428)Time elapsed: 0.141 s % 226.68/32.40 % (2479428)Peak memory usage: 12 MB % 226.68/32.40 % (2479428)Instructions burned: 363 (million) % 226.68/32.40 % (2479430)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3760204116:i=954:bd=all:rtra=on_2725 on theBenchmark for (2725ds/954Mi) % 226.68/32.40 % (2479430)Instruction limit reached! % 226.68/32.40 % (2479430)------------------------------ % 226.68/32.40 % (2479430)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 226.68/32.40 % (2479430)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 226.68/32.40 % (2479430)CaDiCaL version: 2.1.3 % 226.68/32.40 % (2479430)Termination reason: Instruction limit % 226.68/32.40 % (2479430)Termination phase: Saturation % 226.68/32.40 % (2479430)Time elapsed: 0.365 s % 226.68/32.40 % (2479430)Peak memory usage: 14 MB % 226.68/32.40 % (2479430)Instructions burned: 956 (million) % 226.68/32.40 % (2479434)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=270827139:fmbsr=1.3:i=1730:ins=25:rtra=on_2721 on theBenchmark for (2721ds/1730Mi) % 226.68/32.40 % (2479434)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 226.68/32.40 % (2479434)Terminated due to inappropriate strategy. % 226.68/32.40 % (2479434)------------------------------ % 226.68/32.40 % (2479434)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 226.68/32.40 % (2479434)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 226.68/32.40 % (2479434)CaDiCaL version: 2.1.3 % 255.04/36.30 % (2479434)Termination reason: Inappropriate % 255.04/36.30 % (2479434)Time elapsed: 0.039 s % 255.04/36.30 % (2479434)Peak memory usage: 10 MB % 255.04/36.30 % (2479434)Instructions burned: 90 (million) % 255.04/36.30 % (2479434)------------------------------ % 255.04/36.30 % (2479434)------------------------------ % 255.04/36.30 % (2479436)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=2220119084:i=2358:rtra=on_2721 on theBenchmark for (2721ds/2358Mi) % 255.04/36.30 % (2479436)Instruction limit reached! % 255.04/36.30 % (2479436)------------------------------ % 255.04/36.30 % (2479436)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 255.04/36.30 % (2479436)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 255.04/36.30 % (2479436)CaDiCaL version: 2.1.3 % 255.04/36.30 % (2479436)Termination reason: Instruction limit % 255.04/36.30 % (2479436)Termination phase: Saturation % 255.04/36.30 % (2479436)Time elapsed: 0.602 s % 255.04/36.30 % (2479436)Peak memory usage: 13 MB % 255.04/36.30 % (2479436)Instructions burned: 2358 (million) % 255.04/36.30 % (2479480)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=206866034:i=1778:ins=1:rtra=on_2715 on theBenchmark for (2715ds/1778Mi) % 255.04/36.30 % (2479480)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 255.04/36.30 % (2479480)Terminated due to inappropriate strategy. % 255.04/36.30 % (2479480)------------------------------ % 255.04/36.30 % (2479480)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 255.04/36.30 % (2479480)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 255.04/36.30 % (2479480)CaDiCaL version: 2.1.3 % 255.04/36.30 % (2479480)Termination reason: Inappropriate % 255.04/36.30 % (2479480)Time elapsed: 0.019 s % 255.04/36.30 % (2479480)Peak memory usage: 10 MB % 255.04/36.30 % (2479480)Instructions burned: 90 (million) % 255.04/36.30 % (2479480)------------------------------ % 255.04/36.30 % (2479480)------------------------------ % 255.04/36.30 % (2479482)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=4057577230:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2714 on theBenchmark for (2714ds/1384Mi) % 255.04/36.30 % (2479482)Instruction limit reached! % 255.04/36.30 % (2479482)------------------------------ % 255.04/36.30 % (2479482)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 255.04/36.30 % (2479482)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 255.04/36.30 % (2479482)CaDiCaL version: 2.1.3 % 255.04/36.30 % (2479482)Termination reason: Instruction limit % 255.04/36.30 % (2479482)Termination phase: Saturation % 255.04/36.30 % (2479482)Time elapsed: 0.304 s % 255.04/36.30 % (2479482)Peak memory usage: 15 MB % 255.04/36.30 % (2479482)Instructions burned: 1384 (million) % 255.04/36.30 % (2479484)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=1346998391:i=1758:kws=inv_precedence:fsr=off:rtra=on_2711 on theBenchmark for (2711ds/1758Mi) % 255.04/36.30 % (2479484)Instruction limit reached! % 255.04/36.30 % (2479484)------------------------------ % 255.04/36.30 % (2479484)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 255.04/36.30 % (2479484)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 255.04/36.30 % (2479484)CaDiCaL version: 2.1.3 % 255.04/36.30 % (2479484)Termination reason: Instruction limit % 255.04/36.30 % (2479484)Termination phase: Saturation % 255.04/36.30 % (2479484)Time elapsed: 0.352 s % 255.04/36.30 % (2479484)Peak memory usage: 15 MB % 255.04/36.30 % (2479484)Instructions burned: 1759 (million) % 255.04/36.30 % (2479486)fmb+10_1_sil=64000:si=on:random_seed=3674143282:i=44122:nm=2:rtra=on:gsp=on_2707 on theBenchmark for (2707ds/44122Mi) % 255.04/36.30 % (2479486)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 255.04/36.30 % (2479486)Terminated due to inappropriate strategy. % 255.04/36.30 % (2479486)------------------------------ % 255.04/36.30 % (2479486)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 255.04/36.30 % (2479486)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 255.04/36.30 % (2479486)CaDiCaL version: 2.1.3 % 255.04/36.30 % (2479486)Termination reason: Inappropriate % 255.04/36.30 % (2479486)Time elapsed: 0.024 s % 255.04/36.30 % (2479486)Peak memory usage: 11 MB % 255.04/36.30 % (2479486)Instructions burned: 118 (million) % 255.04/36.30 % (2479486)------------------------------ % 255.04/36.30 % (2479486)------------------------------ % 255.04/36.30 % (2479488)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=3154619330:i=19030:nm=5:rtra=on_2707 on theBenchmark for (2707ds/19030Mi) % 289.83/41.29 % (2479488)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 289.83/41.29 % (2479488)Terminated due to inappropriate strategy. % 289.83/41.29 % (2479488)------------------------------ % 289.83/41.29 % (2479488)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 289.83/41.29 % (2479488)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 289.83/41.29 % (2479488)CaDiCaL version: 2.1.3 % 289.83/41.29 % (2479488)Termination reason: Inappropriate % 289.83/41.29 % (2479488)Time elapsed: 0.024 s % 289.83/41.29 % (2479488)Peak memory usage: 10 MB % 289.83/41.29 % (2479488)Instructions burned: 118 (million) % 289.83/41.29 % (2479488)------------------------------ % 289.83/41.29 % (2479488)------------------------------ % 289.83/41.29 % (2479490)fmb+10_1_sil=64000:sas=cadical:si=on:fmbss=8:random_seed=3858835665:fmbsr=1.7:i=1840:rtra=on_2707 on theBenchmark for (2707ds/1840Mi) % 289.83/41.29 % (2479490)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 289.83/41.29 % (2479490)Terminated due to inappropriate strategy. % 289.83/41.29 % (2479490)------------------------------ % 289.83/41.29 % (2479490)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 289.83/41.29 % (2479490)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 289.83/41.29 % (2479490)CaDiCaL version: 2.1.3 % 289.83/41.29 % (2479490)Termination reason: Inappropriate % 289.83/41.29 % (2479490)Time elapsed: 0.024 s % 289.83/41.29 % (2479490)Peak memory usage: 10 MB % 289.83/41.29 % (2479490)Instructions burned: 118 (million) % 289.83/41.29 % (2479490)------------------------------ % 289.83/41.29 % (2479490)------------------------------ % 289.83/41.29 % (2479492)dis-4_1_sil=16000:drc=ordering:si=on:sp=const_frequency:sac=on:newcnf=on:random_seed=553991:i=10262:rtra=on_2706 on theBenchmark for (2706ds/10262Mi) % 289.83/41.29 % (2479492)Instruction limit reached! % 289.83/41.29 % (2479492)------------------------------ % 289.83/41.29 % (2479492)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 289.83/41.29 % (2479492)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 289.83/41.29 % (2479492)CaDiCaL version: 2.1.3 % 289.83/41.29 % (2479492)Termination reason: Instruction limit % 289.83/41.29 % (2479492)Termination phase: Saturation % 289.83/41.29 % (2479492)Time elapsed: 2.084 s % 289.83/41.29 % (2479492)Peak memory usage: 18 MB % 289.83/41.29 % (2479492)Instructions burned: 10267 (million) % 289.83/41.29 % (2479494)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:si=on:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1901986312:i=2944:ins=7:rtra=on:fdi=8:gsp=on_2685 on theBenchmark for (2685ds/2944Mi) % 289.83/41.29 % (2479494)Instruction limit reached! % 289.83/41.29 % (2479494)------------------------------ % 289.83/41.29 % (2479494)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 289.83/41.29 % (2479494)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 289.83/41.29 % (2479494)CaDiCaL version: 2.1.3 % 289.83/41.29 % (2479494)Termination reason: Instruction limit % 289.83/41.29 % (2479494)Termination phase: Saturation % 289.83/41.29 % (2479494)Time elapsed: 0.595 s % 289.83/41.29 % (2479494)Peak memory usage: 15 MB % 289.83/41.29 % (2479494)Instructions burned: 2948 (million) % 289.83/41.29 % (2479496)fmb+10_1_sil=16000:sas=cadical:si=on:bce=on:fmbss=77:random_seed=3004479612:i=12648:rtra=on_2679 on theBenchmark for (2679ds/12648Mi) % 289.83/41.29 % (2479496)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 289.83/41.29 % (2479496)Terminated due to inappropriate strategy. % 289.83/41.29 % (2479496)------------------------------ % 289.83/41.29 % (2479496)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 289.83/41.29 % (2479496)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 289.83/41.29 % (2479496)CaDiCaL version: 2.1.3 % 289.83/41.29 % (2479496)Termination reason: Inappropriate % 289.83/41.29 % (2479496)Time elapsed: 0.024 s % 289.83/41.29 % (2479496)Peak memory usage: 10 MB % 289.83/41.29 % (2479496)Instructions burned: 118 (million) % 289.83/41.29 % (2479496)------------------------------ % 289.83/41.29 % (2479496)------------------------------ % 289.83/41.29 % (2479498)fmb+10_1_fmbas=function:sil=32000:sas=cadical:si=on:fmbss=16:random_seed=353421830:fmbsr=2.30978:i=4348:rtra=on_2679 on theBenchmark for (2679ds/4348Mi) % 289.83/41.29 % (2479498)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 289.83/41.29 % (2479498)Terminated due to inappropriate strategy. % 300.50/42.74 % (2479498)------------------------------ % 300.50/42.74 % (2479498)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.50/42.74 % (2479498)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.50/42.74 % (2479498)CaDiCaL version: 2.1.3 % 300.50/42.74 % (2479498)Termination reason: Inappropriate % 300.50/42.74 % (2479498)Time elapsed: 0.024 s % 300.50/42.74 % (2479498)Peak memory usage: 10 MB % 300.50/42.74 % (2479498)Instructions burned: 118 (million) % 300.50/42.74 % (2479498)------------------------------ % 300.50/42.74 % (2479498)------------------------------ % 300.50/42.74 % (2479500)ott-2_1_sil=16000:si=on:newcnf=on:random_seed=2257305147:avsq=on:i=1738:avsqr=1,16:kws=inv_arity_squared:rtra=on_2678 on theBenchmark for (2678ds/1738Mi) % 300.50/42.74 % (2479500)Instruction limit reached! % 300.50/42.74 % (2479500)------------------------------ % 300.50/42.74 % (2479500)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.50/42.74 % (2479500)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.50/42.74 % (2479500)CaDiCaL version: 2.1.3 % 300.50/42.74 % (2479500)Termination reason: Instruction limit % 300.50/42.74 % (2479500)Termination phase: Saturation % 300.50/42.74 % (2479500)Time elapsed: 0.348 s % 300.50/42.74 % (2479500)Peak memory usage: 13 MB % 300.50/42.74 % (2479500)Instructions burned: 1739 (million) % 300.50/42.74 % (2479502)ott+10_1_sil=32000:tgt=ground:si=on:random_seed=2705641472:i=10228:av=off:rtra=on_2675 on theBenchmark for (2675ds/10228Mi) % 300.50/42.74 % (2479502)Instruction limit reached! % 300.50/42.74 % (2479502)------------------------------ % 300.50/42.74 % (2479502)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.50/42.74 % (2479502)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.50/42.74 % (2479502)CaDiCaL version: 2.1.3 % 300.50/42.74 % (2479502)Termination reason: Instruction limit % 300.50/42.74 % (2479502)Termination phase: Saturation % 300.50/42.74 % (2479502)Time elapsed: 2.041 s % 300.50/42.74 % (2479502)Peak memory usage: 18 MB % 300.50/42.74 % (2479502)Instructions burned: 10230 (million) % 300.50/42.74 % (2479504)fmb+10_1_sil=64000:sas=cadical:si=on:bce=on:rp=on:random_seed=1217566468:i=108564:rtra=on_2654 on theBenchmark for (2654ds/108564Mi) % 300.50/42.74 % (2479504)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 300.50/42.74 % (2479504)Terminated due to inappropriate strategy. % 300.50/42.74 % (2479504)------------------------------ % 300.50/42.74 % (2479504)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.50/42.74 % (2479504)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.50/42.74 % (2479504)CaDiCaL version: 2.1.3 % 300.50/42.74 % (2479504)Termination reason: Inappropriate % 300.50/42.74 % (2479504)Time elapsed: 0.024 s % 300.50/42.74 % (2479504)Peak memory usage: 10 MB % 300.50/42.74 % (2479504)Instructions burned: 118 (million) % 300.50/42.74 % (2479504)------------------------------ % 300.50/42.74 % (2479504)------------------------------ % 300.50/42.74 % (2479506)dis-11_1_sil=16000:si=on:sp=reverse_frequency:alpa=true:random_seed=2828491484:i=7024:aac=none:rtra=on_2654 on theBenchmark for (2654ds/7024Mi) % 300.50/42.74 % (2479332)Instruction limit reached! % 300.50/42.74 % (2479332)------------------------------ % 300.50/42.74 % (2479332)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.50/42.74 % (2479332)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.50/42.74 % (2479332)CaDiCaL version: 2.1.3 % 300.50/42.74 % (2479332)Termination reason: Instruction limit % 300.50/42.74 % (2479332)Termination phase: Saturation % 300.50/42.74 % (2479332)Time elapsed: 14.032 s % 300.50/42.74 % (2479332)Peak memory usage: 16 MB % 300.50/42.74 % (2479332)Instructions burned: 28120 (million) % 300.50/42.74 % (2479508)dis+21_1_sil=32000:sas=cadical:si=on:random_seed=2958896886:i=7546:rtra=on:amm=off_2654 on theBenchmark for (2654ds/7546Mi) % 300.50/42.74 % (2479506)Instruction limit reached! % 300.50/42.74 % (2479506)------------------------------ % 300.50/42.74 % (2479506)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.50/42.74 % (2479506)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.50/42.74 % (2479506)CaDiCaL version: 2.1.3 % 300.50/42.74 % (2479506)Termination reason: Instruction limit % 300.50/42.74 % (2479506)Termination phase: Saturation % 300.50/42.74 % (2479506)Time elapsed: 1.433 s % 300.50/42.74 % (2479506)Peak memory usage: 20 MB % 300.50/42.74 % (2479506)Instructions burned: 7029 (million) % 300.50/42.74 % (2479510)ott+11_1_sil=16000:si=on:gs=on:random_seed=1799823612:s2a=on:i=4502:s2at=3:kws= % 300.50/42.74 Terminated % 300.50/42.74 % Vampire exiting %------------------------------------------------------------------------------