%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWW663_2 : TPTP v9.3.1. Released v6.1.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % Computer : n006.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:40:36 PM UTC 2026 % Result : Timeout 300.39s 42.63s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWW663_2 : TPTP v9.3.1. Released v6.1.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.09/0.19 % Computer : n006.cluster.edu % 0.09/0.19 % Model : x86_64 x86_64 % 0.09/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.19 % Memory : 8046.5625MB % 0.09/0.19 % OS : Linux 6.8.0-71-generic % 0.09/0.19 % CPULimit : 300 % 0.09/0.19 % WCLimit : 300 % 0.09/0.19 % DateTime : Mon Sep 28 14:24:25 UTC 2026 % 0.09/0.19 % CPUTime : % 0.09/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.09/0.23 Running first-order model finding % 0.09/0.23 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 % 3.71/0.87 % (4001657)Will run a generic schedule for satisfiability detection. % 3.71/0.87 % (4001668)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2833476039:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 3.71/0.87 % (4001663)% WARNING: option uhcvi not known. % 3.71/0.87 % (4001662)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3290784220_2999 on theBenchmark for (2999ds/0Mi) % 3.71/0.87 % (4001666)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3898361819:i=116_2999 on theBenchmark for (2999ds/116Mi) % 3.71/0.87 % (4001663)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1375778259:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 3.71/0.87 % (4001665)dis+10_1_sil=32000:sp=arity:random_seed=136379548:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 3.71/0.87 % (4001664)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=4176331619:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 3.71/0.87 % (4001667)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2020864581:i=131_2999 on theBenchmark for (2999ds/131Mi) % 3.71/0.87 % (4001662)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.71/0.87 % (4001662)Terminated due to inappropriate strategy. % 3.71/0.87 % (4001662)------------------------------ % 3.71/0.87 % (4001662)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.71/0.87 % (4001662)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.71/0.87 % (4001662)CaDiCaL version: 2.1.3 % 3.71/0.87 % (4001662)Termination reason: Inappropriate % 3.71/0.87 % (4001662)Time elapsed: 0.005 s % 3.71/0.87 % (4001662)Peak memory usage: 11 MB % 3.71/0.87 % (4001662)Instructions burned: 8 (million) % 3.71/0.87 % (4001662)------------------------------ % 3.71/0.87 % (4001662)------------------------------ % 3.71/0.87 % (4001676)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2940059114:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 3.71/0.87 % (4001676)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.71/0.87 % (4001676)Terminated due to inappropriate strategy. % 3.71/0.87 % (4001676)------------------------------ % 3.71/0.87 % (4001676)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.71/0.87 % (4001676)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.71/0.87 % (4001676)CaDiCaL version: 2.1.3 % 3.71/0.87 % (4001676)Termination reason: Inappropriate % 3.71/0.87 % (4001676)Time elapsed: 0.004 s % 3.71/0.87 % (4001676)Peak memory usage: 10 MB % 3.71/0.87 % (4001676)Instructions burned: 7 (million) % 3.71/0.87 % (4001676)------------------------------ % 3.71/0.87 % (4001676)------------------------------ % 3.71/0.87 % (4001678)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3916085685:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 3.71/0.87 % (4001668)Instruction limit reached! % 3.71/0.87 % (4001668)------------------------------ % 3.71/0.87 % (4001668)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.71/0.87 % (4001668)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.71/0.87 % (4001668)CaDiCaL version: 2.1.3 % 3.71/0.87 % (4001668)Termination reason: Instruction limit % 3.71/0.87 % (4001668)Termination phase: Saturation % 3.71/0.87 % (4001668)Time elapsed: 0.060 s % 3.71/0.87 % (4001668)Peak memory usage: 14 MB % 3.71/0.87 % (4001668)Instructions burned: 160 (million) % 3.71/0.87 % (4001680)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=3413637516:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi) % 3.71/0.87 % (4001665)Instruction limit reached! % 3.71/0.87 % (4001665)------------------------------ % 3.71/0.87 % (4001665)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.71/0.87 % (4001665)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.71/0.87 % (4001665)CaDiCaL version: 2.1.3 % 3.71/0.87 % (4001665)Termination reason: Instruction limit % 3.71/0.87 % (4001665)Termination phase: Saturation % 3.71/0.87 % (4001665)Time elapsed: 0.067 s % 3.71/0.87 % (4001665)Peak memory usage: 13 MB % 3.71/0.87 % (4001665)Instructions burned: 107 (million) % 3.71/0.87 % (4001666)Instruction limit reached! % 3.71/0.87 % (4001666)------------------------------ % 3.71/0.87 % (4001666)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 4.19/1.01 % (4001666)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.19/1.01 % (4001666)CaDiCaL version: 2.1.3 % 4.19/1.01 % (4001666)Termination reason: Instruction limit % 4.19/1.01 % (4001666)Termination phase: Saturation % 4.19/1.01 % (4001666)Time elapsed: 0.072 s % 4.19/1.01 % (4001666)Peak memory usage: 13 MB % 4.19/1.01 % (4001666)Instructions burned: 116 (million) % 4.19/1.01 % (4001667)Instruction limit reached! % 4.19/1.01 % (4001667)------------------------------ % 4.19/1.01 % (4001667)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 4.19/1.01 % (4001667)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.19/1.01 % (4001667)CaDiCaL version: 2.1.3 % 4.19/1.01 % (4001667)Termination reason: Instruction limit % 4.19/1.01 % (4001667)Termination phase: Saturation % 4.19/1.01 % (4001667)Time elapsed: 0.083 s % 4.19/1.01 % (4001667)Peak memory usage: 13 MB % 4.19/1.01 % (4001667)Instructions burned: 132 (million) % 4.19/1.01 % (4001682)ott-21_1_sil=16000:fs=off:random_seed=1259021699:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi) % 4.19/1.01 % (4001683)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2115760415:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 4.19/1.01 % (4001684)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3630511858:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 4.19/1.01 % (4001684)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 4.19/1.01 % (4001684)Terminated due to inappropriate strategy. % 4.19/1.01 % (4001684)------------------------------ % 4.19/1.01 % (4001684)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 4.19/1.01 % (4001684)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.19/1.01 % (4001684)CaDiCaL version: 2.1.3 % 4.19/1.01 % (4001684)Termination reason: Inappropriate % 4.19/1.01 % (4001684)Time elapsed: 0.004 s % 4.19/1.01 % (4001684)Peak memory usage: 11 MB % 4.19/1.01 % (4001684)Instructions burned: 7 (million) % 4.19/1.01 % (4001684)------------------------------ % 4.19/1.01 % (4001684)------------------------------ % 4.19/1.01 % (4001688)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=493351652:i=1179_2998 on theBenchmark for (2998ds/1179Mi) % 4.19/1.01 % (4001678)Instruction limit reached! % 4.19/1.01 % (4001678)------------------------------ % 4.19/1.01 % (4001678)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 4.19/1.01 % (4001678)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.19/1.01 % (4001678)CaDiCaL version: 2.1.3 % 4.19/1.01 % (4001678)Termination reason: Instruction limit % 4.19/1.01 % (4001678)Termination phase: Saturation % 4.19/1.01 % (4001678)Time elapsed: 0.087 s % 4.19/1.01 % (4001678)Peak memory usage: 13 MB % 4.19/1.01 % (4001678)Instructions burned: 131 (million) % 4.19/1.01 % (4001690)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3055698932:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi) % 4.19/1.01 % (4001690)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 4.19/1.01 % (4001690)Terminated due to inappropriate strategy. % 4.19/1.01 % (4001690)------------------------------ % 4.19/1.01 % (4001690)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 4.19/1.01 % (4001690)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.19/1.01 % (4001690)CaDiCaL version: 2.1.3 % 4.19/1.01 % (4001690)Termination reason: Inappropriate % 4.19/1.01 % (4001690)Time elapsed: 0.004 s % 4.19/1.01 % (4001690)Peak memory usage: 10 MB % 4.19/1.01 % (4001690)Instructions burned: 7 (million) % 4.19/1.01 % (4001690)------------------------------ % 4.19/1.01 % (4001690)------------------------------ % 4.19/1.01 % (4001682)Instruction limit reached! % 4.19/1.01 % (4001682)------------------------------ % 4.19/1.01 % (4001682)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 4.19/1.01 % (4001682)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.19/1.01 % (4001682)CaDiCaL version: 2.1.3 % 4.19/1.01 % (4001682)Termination reason: Instruction limit % 4.19/1.01 % (4001682)Termination phase: Saturation % 4.19/1.01 % (4001682)Time elapsed: 0.088 s % 4.19/1.01 % (4001682)Peak memory usage: 13 MB % 4.19/1.01 % (4001682)Instructions burned: 181 (million) % 4.19/1.01 % (4001692)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=2137954611: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) % 18.77/2.97 % (4001693)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2286381483:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi) % 18.77/2.97 % (4001680)Instruction limit reached! % 18.77/2.97 % (4001680)------------------------------ % 18.77/2.97 % (4001680)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 18.77/2.97 % (4001680)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.77/2.97 % (4001680)CaDiCaL version: 2.1.3 % 18.77/2.97 % (4001680)Termination reason: Instruction limit % 18.77/2.97 % (4001680)Termination phase: Saturation % 18.77/2.97 % (4001680)Time elapsed: 0.210 s % 18.77/2.97 % (4001680)Peak memory usage: 18 MB % 18.77/2.97 % (4001680)Instructions burned: 685 (million) % 18.77/2.97 % (4001696)fmb+10_1_sil=64000:random_seed=4177678928:i=22061:nm=2:gsp=on_2996 on theBenchmark for (2996ds/22061Mi) % 18.77/2.97 % (4001696)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 18.77/2.97 % (4001696)Terminated due to inappropriate strategy. % 18.77/2.97 % (4001696)------------------------------ % 18.77/2.97 % (4001696)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 18.77/2.97 % (4001696)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.77/2.97 % (4001696)CaDiCaL version: 2.1.3 % 18.77/2.97 % (4001696)Termination reason: Inappropriate % 18.77/2.97 % (4001696)Time elapsed: 0.002 s % 18.77/2.97 % (4001696)Peak memory usage: 11 MB % 18.77/2.97 % (4001696)Instructions burned: 8 (million) % 18.77/2.97 % (4001696)------------------------------ % 18.77/2.97 % (4001696)------------------------------ % 18.77/2.97 % (4001698)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3584068060:i=9515:nm=5_2996 on theBenchmark for (2996ds/9515Mi) % 18.77/2.97 % (4001698)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 18.77/2.97 % (4001698)Terminated due to inappropriate strategy. % 18.77/2.97 % (4001698)------------------------------ % 18.77/2.97 % (4001698)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 18.77/2.97 % (4001698)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.77/2.97 % (4001698)CaDiCaL version: 2.1.3 % 18.77/2.97 % (4001698)Termination reason: Inappropriate % 18.77/2.97 % (4001698)Time elapsed: 0.002 s % 18.77/2.97 % (4001698)Peak memory usage: 11 MB % 18.77/2.97 % (4001698)Instructions burned: 7 (million) % 18.77/2.97 % (4001698)------------------------------ % 18.77/2.97 % (4001698)------------------------------ % 18.77/2.97 % (4001700)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=477589722:fmbsr=1.7:i=920_2996 on theBenchmark for (2996ds/920Mi) % 18.77/2.97 % (4001700)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 18.77/2.97 % (4001700)Terminated due to inappropriate strategy. % 18.77/2.97 % (4001700)------------------------------ % 18.77/2.97 % (4001700)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 18.77/2.97 % (4001700)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.77/2.97 % (4001700)CaDiCaL version: 2.1.3 % 18.77/2.97 % (4001700)Termination reason: Inappropriate % 18.77/2.97 % (4001700)Time elapsed: 0.002 s % 18.77/2.97 % (4001700)Peak memory usage: 11 MB % 18.77/2.97 % (4001700)Instructions burned: 7 (million) % 18.77/2.97 % (4001700)------------------------------ % 18.77/2.97 % (4001700)------------------------------ % 18.77/2.97 % (4001702)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1783112179:i=5131_2996 on theBenchmark for (2996ds/5131Mi) % 18.77/2.97 % (4001683)Instruction limit reached! % 18.77/2.97 % (4001683)------------------------------ % 18.77/2.97 % (4001683)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 18.77/2.97 % (4001683)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.77/2.97 % (4001683)CaDiCaL version: 2.1.3 % 18.77/2.97 % (4001683)Termination reason: Instruction limit % 18.77/2.97 % (4001683)Termination phase: Saturation % 18.77/2.97 % (4001683)Time elapsed: 0.300 s % 18.77/2.97 % (4001683)Peak memory usage: 14 MB % 18.77/2.97 % (4001683)Instructions burned: 477 (million) % 18.77/2.97 % (4001704)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=157195765:i=1472:ins=7:fdi=8:gsp=on_2995 on theBenchmark for (2995ds/1472Mi) % 18.77/2.97 % (4001692)Instruction limit reached! % 18.77/2.97 % (4001692)------------------------------ % 24.98/3.96 % (4001692)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 24.98/3.96 % (4001692)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.98/3.96 % (4001692)CaDiCaL version: 2.1.3 % 24.98/3.96 % (4001692)Termination reason: Instruction limit % 24.98/3.96 % (4001692)Termination phase: Saturation % 24.98/3.96 % (4001692)Time elapsed: 0.430 s % 24.98/3.96 % (4001692)Peak memory usage: 20 MB % 24.98/3.96 % (4001692)Instructions burned: 692 (million) % 24.98/3.96 % (4001706)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3684151172:i=6324_2993 on theBenchmark for (2993ds/6324Mi) % 24.98/3.96 % (4001706)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 24.98/3.96 % (4001706)Terminated due to inappropriate strategy. % 24.98/3.96 % (4001706)------------------------------ % 24.98/3.96 % (4001706)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 24.98/3.96 % (4001706)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.98/3.96 % (4001706)CaDiCaL version: 2.1.3 % 24.98/3.96 % (4001706)Termination reason: Inappropriate % 24.98/3.96 % (4001706)Time elapsed: 0.005 s % 24.98/3.96 % (4001706)Peak memory usage: 11 MB % 24.98/3.96 % (4001706)Instructions burned: 8 (million) % 24.98/3.96 % (4001706)------------------------------ % 24.98/3.96 % (4001706)------------------------------ % 24.98/3.96 % (4001708)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=2761360045:fmbsr=2.30978:i=2174_2993 on theBenchmark for (2993ds/2174Mi) % 24.98/3.96 % (4001708)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 24.98/3.96 % (4001708)Terminated due to inappropriate strategy. % 24.98/3.96 % (4001708)------------------------------ % 24.98/3.96 % (4001708)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 24.98/3.96 % (4001708)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.98/3.96 % (4001708)CaDiCaL version: 2.1.3 % 24.98/3.96 % (4001708)Termination reason: Inappropriate % 24.98/3.96 % (4001708)Time elapsed: 0.004 s % 24.98/3.96 % (4001708)Peak memory usage: 10 MB % 24.98/3.96 % (4001708)Instructions burned: 7 (million) % 24.98/3.96 % (4001708)------------------------------ % 24.98/3.96 % (4001708)------------------------------ % 24.98/3.96 % (4001688)Instruction limit reached! % 24.98/3.96 % (4001688)------------------------------ % 24.98/3.96 % (4001688)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 24.98/3.96 % (4001688)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.98/3.96 % (4001688)CaDiCaL version: 2.1.3 % 24.98/3.96 % (4001688)Termination reason: Instruction limit % 24.98/3.96 % (4001688)Termination phase: Saturation % 24.98/3.96 % (4001688)Time elapsed: 0.538 s % 24.98/3.96 % (4001688)Peak memory usage: 22 MB % 24.98/3.96 % (4001688)Instructions burned: 1181 (million) % 24.98/3.96 % (4001710)ott-2_1_sil=16000:newcnf=on:random_seed=1488346458:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2993 on theBenchmark for (2993ds/869Mi) % 24.98/3.96 % (4001711)ott+10_1_sil=32000:tgt=ground:random_seed=1371241208:i=5114:av=off_2993 on theBenchmark for (2993ds/5114Mi) % 24.98/3.96 % (4001693)Instruction limit reached! % 24.98/3.96 % (4001693)------------------------------ % 24.98/3.96 % (4001693)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 24.98/3.96 % (4001693)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.98/3.96 % (4001693)CaDiCaL version: 2.1.3 % 24.98/3.96 % (4001693)Termination reason: Instruction limit % 24.98/3.96 % (4001693)Termination phase: Saturation % 24.98/3.96 % (4001693)Time elapsed: 0.527 s % 24.98/3.96 % (4001693)Peak memory usage: 19 MB % 24.98/3.96 % (4001693)Instructions burned: 879 (million) % 24.98/3.96 % (4001714)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=1531193789:i=54282_2992 on theBenchmark for (2992ds/54282Mi) % 24.98/3.96 % (4001714)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 24.98/3.96 % (4001714)Terminated due to inappropriate strategy. % 24.98/3.96 % (4001714)------------------------------ % 24.98/3.96 % (4001714)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 24.98/3.96 % (4001714)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.98/3.96 % (4001714)CaDiCaL version: 2.1.3 % 24.98/3.96 % (4001714)Termination reason: Inappropriate % 24.98/3.96 % (4001714)Time elapsed: 0.005 s % 24.98/3.96 % (4001714)Peak memory usage: 11 MB % 24.98/3.96 % (4001714)Instructions burned: 8 (million) % 94.18/13.54 % (4001714)------------------------------ % 94.18/13.54 % (4001714)------------------------------ % 94.18/13.54 % (4001716)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3713002144:i=3512:aac=none_2992 on theBenchmark for (2992ds/3512Mi) % 94.18/13.54 % (4001710)Instruction limit reached! % 94.18/13.54 % (4001710)------------------------------ % 94.18/13.54 % (4001710)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 94.18/13.54 % (4001710)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 94.18/13.54 % (4001710)CaDiCaL version: 2.1.3 % 94.18/13.54 % (4001710)Termination reason: Instruction limit % 94.18/13.54 % (4001710)Termination phase: Saturation % 94.18/13.54 % (4001710)Time elapsed: 0.535 s % 94.18/13.54 % (4001710)Peak memory usage: 15 MB % 94.18/13.54 % (4001710)Instructions burned: 869 (million) % 94.18/13.54 % (4001718)dis+21_1_sil=32000:sas=cadical:random_seed=1642124703:i=3773:amm=off_2987 on theBenchmark for (2987ds/3773Mi) % 94.18/13.54 % (4001704)Instruction limit reached! % 94.18/13.54 % (4001704)------------------------------ % 94.18/13.54 % (4001704)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 94.18/13.54 % (4001704)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 94.18/13.54 % (4001704)CaDiCaL version: 2.1.3 % 94.18/13.54 % (4001704)Termination reason: Instruction limit % 94.18/13.54 % (4001704)Termination phase: Saturation % 94.18/13.54 % (4001704)Time elapsed: 0.856 s % 94.18/13.54 % (4001704)Peak memory usage: 25 MB % 94.18/13.54 % (4001704)Instructions burned: 1473 (million) % 94.18/13.54 % (4001720)ott+11_1_sil=16000:gs=on:random_seed=2995403248:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2986 on theBenchmark for (2986ds/2251Mi) % 94.18/13.54 % (4001702)Instruction limit reached! % 94.18/13.54 % (4001702)------------------------------ % 94.18/13.54 % (4001702)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 94.18/13.54 % (4001702)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 94.18/13.54 % (4001702)CaDiCaL version: 2.1.3 % 94.18/13.54 % (4001702)Termination reason: Instruction limit % 94.18/13.54 % (4001702)Termination phase: Saturation % 94.18/13.54 % (4001702)Time elapsed: 1.385 s % 94.18/13.54 % (4001702)Peak memory usage: 34 MB % 94.18/13.54 % (4001702)Instructions burned: 5134 (million) % 94.18/13.54 % (4001722)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=1327937845:fmbsr=1.6:i=67534_2982 on theBenchmark for (2982ds/67534Mi) % 94.18/13.54 % (4001722)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 94.18/13.54 % (4001722)Terminated due to inappropriate strategy. % 94.18/13.54 % (4001722)------------------------------ % 94.18/13.54 % (4001722)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 94.18/13.54 % (4001722)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 94.18/13.54 % (4001722)CaDiCaL version: 2.1.3 % 94.18/13.54 % (4001722)Termination reason: Inappropriate % 94.18/13.54 % (4001722)Time elapsed: 0.002 s % 94.18/13.54 % (4001722)Peak memory usage: 11 MB % 94.18/13.54 % (4001722)Instructions burned: 7 (million) % 94.18/13.54 % (4001722)------------------------------ % 94.18/13.54 % (4001722)------------------------------ % 94.18/13.54 % (4001724)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=1856074832:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2982 on theBenchmark for (2982ds/4591Mi) % 94.18/13.54 % (4001720)Instruction limit reached! % 94.18/13.54 % (4001720)------------------------------ % 94.18/13.54 % (4001720)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 94.18/13.54 % (4001720)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 94.18/13.54 % (4001720)CaDiCaL version: 2.1.3 % 94.18/13.54 % (4001720)Termination reason: Instruction limit % 94.18/13.54 % (4001720)Termination phase: Saturation % 94.18/13.54 % (4001720)Time elapsed: 1.158 s % 94.18/13.54 % (4001720)Peak memory usage: 20 MB % 94.18/13.54 % (4001720)Instructions burned: 2251 (million) % 94.18/13.54 % (4001726)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=1283367567:i=29340_2975 on theBenchmark for (2975ds/29340Mi) % 94.18/13.54 % (4001716)Instruction limit reached! % 94.18/13.54 % (4001716)------------------------------ % 94.18/13.54 % (4001716)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 94.18/13.54 % (4001716)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 94.18/13.54 % (4001716)CaDiCaL version: 2.1.3 % 94.18/13.54 % (4001716)Termination reason: Instruction limit % 121.18/17.35 % (4001716)Termination phase: Saturation % 121.18/17.35 % (4001716)Time elapsed: 1.943 s % 121.18/17.35 % (4001716)Peak memory usage: 33 MB % 121.18/17.35 % (4001716)Instructions burned: 3512 (million) % 121.18/17.35 % (4001728)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=858008276:i=5211_2972 on theBenchmark for (2972ds/5211Mi) % 121.18/17.35 % (4001724)Instruction limit reached! % 121.18/17.35 % (4001724)------------------------------ % 121.18/17.35 % (4001724)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 121.18/17.35 % (4001724)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 121.18/17.35 % (4001724)CaDiCaL version: 2.1.3 % 121.18/17.35 % (4001724)Termination reason: Instruction limit % 121.18/17.35 % (4001724)Termination phase: Saturation % 121.18/17.35 % (4001724)Time elapsed: 1.112 s % 121.18/17.35 % (4001724)Peak memory usage: 38 MB % 121.18/17.35 % (4001724)Instructions burned: 4592 (million) % 121.18/17.35 % (4001730)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=665890015:i=5497:nm=2_2971 on theBenchmark for (2971ds/5497Mi) % 121.18/17.35 % (4001730)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 121.18/17.35 % (4001730)Terminated due to inappropriate strategy. % 121.18/17.35 % (4001730)------------------------------ % 121.18/17.35 % (4001730)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 121.18/17.35 % (4001730)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 121.18/17.35 % (4001730)CaDiCaL version: 2.1.3 % 121.18/17.35 % (4001730)Termination reason: Inappropriate % 121.18/17.35 % (4001730)Time elapsed: 0.002 s % 121.18/17.35 % (4001730)Peak memory usage: 11 MB % 121.18/17.35 % (4001730)Instructions burned: 8 (million) % 121.18/17.35 % (4001730)------------------------------ % 121.18/17.35 % (4001730)------------------------------ % 121.18/17.35 % (4001732)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=3718053667:fmbsr=2:i=46332_2970 on theBenchmark for (2970ds/46332Mi) % 121.18/17.35 % (4001732)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 121.18/17.35 % (4001732)Terminated due to inappropriate strategy. % 121.18/17.35 % (4001732)------------------------------ % 121.18/17.35 % (4001732)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 121.18/17.35 % (4001732)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 121.18/17.35 % (4001732)CaDiCaL version: 2.1.3 % 121.18/17.35 % (4001732)Termination reason: Inappropriate % 121.18/17.35 % (4001732)Time elapsed: 0.002 s % 121.18/17.35 % (4001732)Peak memory usage: 11 MB % 121.18/17.35 % (4001732)Instructions burned: 7 (million) % 121.18/17.35 % (4001732)------------------------------ % 121.18/17.35 % (4001732)------------------------------ % 121.18/17.35 % (4001734)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=920796655:i=14071_2970 on theBenchmark for (2970ds/14071Mi) % 121.18/17.35 % (4001734)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 121.18/17.35 % (4001734)Terminated due to inappropriate strategy. % 121.18/17.35 % (4001734)------------------------------ % 121.18/17.35 % (4001734)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 121.18/17.35 % (4001734)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 121.18/17.35 % (4001734)CaDiCaL version: 2.1.3 % 121.18/17.35 % (4001734)Termination reason: Inappropriate % 121.18/17.35 % (4001734)Time elapsed: 0.002 s % 121.18/17.35 % (4001734)Peak memory usage: 11 MB % 121.18/17.35 % (4001734)Instructions burned: 7 (million) % 121.18/17.35 % (4001734)------------------------------ % 121.18/17.35 % (4001734)------------------------------ % 121.18/17.35 % (4001736)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=474538397:i=22565:add=on:rawr=on_2970 on theBenchmark for (2970ds/22565Mi) % 121.18/17.35 % (4001718)Instruction limit reached! % 121.18/17.35 % (4001718)------------------------------ % 121.18/17.35 % (4001718)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 121.18/17.35 % (4001718)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 121.18/17.35 % (4001718)CaDiCaL version: 2.1.3 % 121.18/17.35 % (4001718)Termination reason: Instruction limit % 121.18/17.35 % (4001718)Termination phase: Saturation % 121.18/17.35 % (4001718)Time elapsed: 2.066 s % 121.18/17.35 % (4001718)Peak memory usage: 33 MB % 121.18/17.35 % (4001718)Instructions burned: 3773 (million) % 121.18/17.35 % (4001738)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=1490794692:i=8173:av=off_2966 on theBenchmark for (2966ds/8173Mi) % 121.18/17.35 % (4001711)Instruction limit reached! % 121.89/17.49 % (4001711)------------------------------ % 121.89/17.49 % (4001711)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 121.89/17.49 % (4001711)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 121.89/17.49 % (4001711)CaDiCaL version: 2.1.3 % 121.89/17.49 % (4001711)Termination reason: Instruction limit % 121.89/17.49 % (4001711)Termination phase: Saturation % 121.89/17.49 % (4001711)Time elapsed: 3.007 s % 121.89/17.49 % (4001711)Peak memory usage: 38 MB % 121.89/17.49 % (4001711)Instructions burned: 5114 (million) % 121.89/17.49 % (4001740)dis+10_16:1_sil=16000:random_seed=2469167287:i=9155:fsr=off_2962 on theBenchmark for (2962ds/9155Mi) % 121.89/17.49 % (4001728)Instruction limit reached! % 121.89/17.49 % (4001728)------------------------------ % 121.89/17.49 % (4001728)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 121.89/17.49 % (4001728)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 121.89/17.49 % (4001728)CaDiCaL version: 2.1.3 % 121.89/17.49 % (4001728)Termination reason: Instruction limit % 121.89/17.49 % (4001728)Termination phase: Saturation % 121.89/17.49 % (4001728)Time elapsed: 2.771 s % 121.89/17.49 % (4001728)Peak memory usage: 54 MB % 121.89/17.49 % (4001728)Instructions burned: 5211 (million) % 121.89/17.49 % (4001742)ott-3_8_sil=64000:random_seed=3574903409:i=20139:bs=on_2944 on theBenchmark for (2944ds/20139Mi) % 121.89/17.49 % (4001738)Instruction limit reached! % 121.89/17.49 % (4001738)------------------------------ % 121.89/17.49 % (4001738)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 121.89/17.49 % (4001738)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 121.89/17.49 % (4001738)CaDiCaL version: 2.1.3 % 121.89/17.49 % (4001738)Termination reason: Instruction limit % 121.89/17.49 % (4001738)Termination phase: Saturation % 121.89/17.49 % (4001738)Time elapsed: 4.948 s % 121.89/17.49 % (4001738)Peak memory usage: 58 MB % 121.89/17.49 % (4001738)Instructions burned: 8174 (million) % 121.89/17.49 % (4001744)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=2615197910:fmbsr=2:i=32576_2916 on theBenchmark for (2916ds/32576Mi) % 121.89/17.49 % (4001744)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 121.89/17.49 % (4001744)Terminated due to inappropriate strategy. % 121.89/17.49 % (4001744)------------------------------ % 121.89/17.49 % (4001744)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 121.89/17.49 % (4001744)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 121.89/17.49 % (4001744)CaDiCaL version: 2.1.3 % 121.89/17.49 % (4001744)Termination reason: Inappropriate % 121.89/17.49 % (4001744)Time elapsed: 0.005 s % 121.89/17.49 % (4001744)Peak memory usage: 11 MB % 121.89/17.49 % (4001744)Instructions burned: 8 (million) % 121.89/17.49 % (4001744)------------------------------ % 121.89/17.49 % (4001744)------------------------------ % 121.89/17.49 % (4001746)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=3995853451:i=11404_2916 on theBenchmark for (2916ds/11404Mi) % 121.89/17.49 % (4001736)Instruction limit reached! % 121.89/17.49 % (4001736)------------------------------ % 121.89/17.49 % (4001736)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 121.89/17.49 % (4001736)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 121.89/17.49 % (4001736)CaDiCaL version: 2.1.3 % 121.89/17.49 % (4001736)Termination reason: Instruction limit % 121.89/17.49 % (4001736)Termination phase: Saturation % 121.89/17.49 % (4001736)Time elapsed: 5.592 s % 121.89/17.49 % (4001736)Peak memory usage: 108 MB % 121.89/17.49 % (4001736)Instructions burned: 22568 (million) % 121.89/17.49 % (4001740)Instruction limit reached! % 121.89/17.49 % (4001740)------------------------------ % 121.89/17.49 % (4001740)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 121.89/17.49 % (4001740)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 121.89/17.49 % (4001740)CaDiCaL version: 2.1.3 % 121.89/17.49 % (4001740)Termination reason: Instruction limit % 121.89/17.49 % (4001740)Termination phase: Saturation % 121.89/17.49 % (4001740)Time elapsed: 4.786 s % 121.89/17.49 % (4001740)Peak memory usage: 47 MB % 121.89/17.49 % (4001740)Instructions burned: 9156 (million) % 121.89/17.49 % (4001749)dis+33_16_sil=32000:sac=on:random_seed=1837289040:i=15851:nm=0_2914 on theBenchmark for (2914ds/15851Mi) % 121.89/17.49 % (4001748)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=3352898647:i=14134_2914 on theBenchmark for (2914ds/14134Mi) % 121.89/17.49 % (4001749)Instruction limit reached! % 121.89/17.49 % (4001749)------------------------------ % 121.89/17.49 % (4001749)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 136.01/19.48 % (4001749)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 136.01/19.48 % (4001749)CaDiCaL version: 2.1.3 % 136.01/19.48 % (4001749)Termination reason: Instruction limit % 136.01/19.48 % (4001749)Termination phase: Saturation % 136.01/19.48 % (4001749)Time elapsed: 4.754 s % 136.01/19.48 % (4001749)Peak memory usage: 124 MB % 136.01/19.48 % (4001749)Instructions burned: 15851 (million) % 136.01/19.48 % (4001754)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=3461733164:avsq=on:i=17627:add=on:amm=off_2866 on theBenchmark for (2866ds/17627Mi) % 136.01/19.48 % (4001726)Instruction limit reached! % 136.01/19.48 % (4001726)------------------------------ % 136.01/19.48 % (4001726)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 136.01/19.48 % (4001726)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 136.01/19.48 % (4001726)CaDiCaL version: 2.1.3 % 136.01/19.48 % (4001726)Termination reason: Instruction limit % 136.01/19.48 % (4001726)Termination phase: Saturation % 136.01/19.48 % (4001726)Time elapsed: 12.576 s % 136.01/19.48 % (4001726)Peak memory usage: 195 MB % 136.01/19.48 % (4001726)Instructions burned: 29342 (million) % 136.01/19.48 % (4002118)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=968486637:s2a=on:i=53295_2848 on theBenchmark for (2848ds/53295Mi) % 136.01/19.48 % (4001746)Instruction limit reached! % 136.01/19.48 % (4001746)------------------------------ % 136.01/19.48 % (4001746)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 136.01/19.48 % (4001746)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 136.01/19.48 % (4001746)CaDiCaL version: 2.1.3 % 136.01/19.48 % (4001746)Termination reason: Instruction limit % 136.01/19.48 % (4001746)Termination phase: Saturation % 136.01/19.48 % (4001746)Time elapsed: 7.204 s % 136.01/19.48 % (4001746)Peak memory usage: 72 MB % 136.01/19.48 % (4001746)Instructions burned: 11405 (million) % 136.01/19.48 % (4002120)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=2525864497:i=26857:ins=20_2844 on theBenchmark for (2844ds/26857Mi) % 136.01/19.48 % (4002120)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 136.01/19.48 % (4002120)Terminated due to inappropriate strategy. % 136.01/19.48 % (4002120)------------------------------ % 136.01/19.48 % (4002120)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 136.01/19.48 % (4002120)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 136.01/19.48 % (4002120)CaDiCaL version: 2.1.3 % 136.01/19.48 % (4002120)Termination reason: Inappropriate % 136.01/19.48 % (4002120)Time elapsed: 0.004 s % 136.01/19.48 % (4002120)Peak memory usage: 11 MB % 136.01/19.48 % (4002120)Instructions burned: 7 (million) % 136.01/19.48 % (4002120)------------------------------ % 136.01/19.48 % (4002120)------------------------------ % 136.01/19.48 % (4002122)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=4234780080:i=28120:bs=on:fsr=off_2844 on theBenchmark for (2844ds/28120Mi) % 136.01/19.48 % (4001748)Instruction limit reached! % 136.01/19.48 % (4001748)------------------------------ % 136.01/19.48 % (4001748)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 136.01/19.48 % (4001748)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 136.01/19.48 % (4001748)CaDiCaL version: 2.1.3 % 136.01/19.48 % (4001748)Termination reason: Instruction limit % 136.01/19.48 % (4001748)Termination phase: Saturation % 136.01/19.48 % (4001748)Time elapsed: 8.511 s % 136.01/19.48 % (4001748)Peak memory usage: 70 MB % 136.01/19.48 % (4001748)Instructions burned: 14135 (million) % 136.01/19.48 % (4002125)fmb+10_1_sil=256000:fmbss=7:random_seed=1920321036:fmbsr=1.6:i=182295_2829 on theBenchmark for (2829ds/182295Mi) % 136.01/19.48 % (4002125)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 136.01/19.48 % (4002125)Terminated due to inappropriate strategy. % 136.01/19.48 % (4002125)------------------------------ % 136.01/19.48 % (4002125)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 136.01/19.48 % (4002125)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 136.01/19.48 % (4002125)CaDiCaL version: 2.1.3 % 136.01/19.48 % (4002125)Termination reason: Inappropriate % 136.01/19.48 % (4002125)Time elapsed: 0.004 s % 136.01/19.48 % (4002125)Peak memory usage: 10 MB % 136.01/19.48 % (4002125)Instructions burned: 7 (million) % 136.01/19.48 % (4002125)------------------------------ % 136.01/19.48 % (4002125)------------------------------ % 136.01/19.48 % (4002127)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=3905725327:i=44625:gsp=on_2828 on theBenchmark for (2828ds/44625Mi) % 142.91/20.49 % (4002127)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 142.91/20.49 % (4002127)Terminated due to inappropriate strategy. % 142.91/20.49 % (4002127)------------------------------ % 142.91/20.49 % (4002127)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 142.91/20.49 % (4002127)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 142.91/20.49 % (4002127)CaDiCaL version: 2.1.3 % 142.91/20.49 % (4002127)Termination reason: Inappropriate % 142.91/20.49 % (4002127)Time elapsed: 0.005 s % 142.91/20.49 % (4002127)Peak memory usage: 11 MB % 142.91/20.49 % (4002127)Instructions burned: 10 (million) % 142.91/20.49 % (4002127)------------------------------ % 142.91/20.49 % (4002127)------------------------------ % 142.91/20.49 % (4002129)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=2665377714:i=160505_2828 on theBenchmark for (2828ds/160505Mi) % 142.91/20.49 % (4002129)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 142.91/20.49 % (4002129)Terminated due to inappropriate strategy. % 142.91/20.49 % (4002129)------------------------------ % 142.91/20.49 % (4002129)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 142.91/20.49 % (4002129)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 142.91/20.49 % (4002129)CaDiCaL version: 2.1.3 % 142.91/20.49 % (4002129)Termination reason: Inappropriate % 142.91/20.49 % (4002129)Time elapsed: 0.004 s % 142.91/20.49 % (4002129)Peak memory usage: 10 MB % 142.91/20.49 % (4002129)Instructions burned: 7 (million) % 142.91/20.49 % (4002129)------------------------------ % 142.91/20.49 % (4002129)------------------------------ % 142.91/20.49 % (4002131)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=541670988:fmbsr=1.3:i=225729_2828 on theBenchmark for (2828ds/225729Mi) % 142.91/20.49 % (4002131)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 142.91/20.49 % (4002131)Terminated due to inappropriate strategy. % 142.91/20.49 % (4002131)------------------------------ % 142.91/20.49 % (4002131)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 142.91/20.49 % (4002131)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 142.91/20.49 % (4002131)CaDiCaL version: 2.1.3 % 142.91/20.49 % (4002131)Termination reason: Inappropriate % 142.91/20.49 % (4002131)Time elapsed: 0.004 s % 142.91/20.49 % (4002131)Peak memory usage: 11 MB % 142.91/20.49 % (4002131)Instructions burned: 7 (million) % 142.91/20.49 % (4002131)------------------------------ % 142.91/20.49 % (4002131)------------------------------ % 142.91/20.49 % (4002133)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=2329655095:fmbsr=2:i=185024:ins=7_2828 on theBenchmark for (2828ds/185024Mi) % 142.91/20.49 % (4002133)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 142.91/20.49 % (4002133)Terminated due to inappropriate strategy. % 142.91/20.49 % (4002133)------------------------------ % 142.91/20.49 % (4002133)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 142.91/20.49 % (4002133)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 142.91/20.49 % (4002133)CaDiCaL version: 2.1.3 % 142.91/20.49 % (4002133)Termination reason: Inappropriate % 142.91/20.49 % (4002133)Time elapsed: 0.004 s % 142.91/20.49 % (4002133)Peak memory usage: 11 MB % 142.91/20.49 % (4002133)Instructions burned: 7 (million) % 142.91/20.49 % (4002133)------------------------------ % 142.91/20.49 % (4002133)------------------------------ % 142.91/20.49 % (4002135)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=4061571388:rtra=on_2827 on theBenchmark for (2827ds/0Mi) % 142.91/20.49 % (4002135)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 142.91/20.49 % (4002135)Terminated due to inappropriate strategy. % 142.91/20.49 % (4002135)------------------------------ % 142.91/20.49 % (4002135)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 142.91/20.49 % (4002135)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 142.91/20.49 % (4002135)CaDiCaL version: 2.1.3 % 142.91/20.49 % (4002135)Termination reason: Inappropriate % 142.91/20.49 % (4002135)Time elapsed: 0.005 s % 142.91/20.49 % (4002135)Peak memory usage: 11 MB % 142.91/20.49 % (4002135)Instructions burned: 9 (million) % 142.91/20.49 % (4002135)------------------------------ % 142.91/20.49 % (4002135)------------------------------ % 142.91/20.49 % (4002137)% WARNING: option uhcvi not known. % 142.91/20.49 % (4002137)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=64236724:i=271062:add=off:rtra=on:rawr=on_2827 on theBenchmark for (2827ds/271062Mi) % 156.64/22.36 % (4001742)Instruction limit reached! % 156.64/22.36 % (4001742)------------------------------ % 156.64/22.36 % (4001742)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 156.64/22.36 % (4001742)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 156.64/22.36 % (4001742)CaDiCaL version: 2.1.3 % 156.64/22.36 % (4001742)Termination reason: Instruction limit % 156.64/22.36 % (4001742)Termination phase: Saturation % 156.64/22.36 % (4001742)Time elapsed: 13.160 s % 156.64/22.36 % (4001742)Peak memory usage: 106 MB % 156.64/22.36 % (4001742)Instructions burned: 20140 (million) % 156.64/22.36 % (4002139)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2721196869:i=176048:add=on:rtra=on:rawr=on_2812 on theBenchmark for (2812ds/176048Mi) % 156.64/22.36 % (4001754)Instruction limit reached! % 156.64/22.36 % (4001754)------------------------------ % 156.64/22.36 % (4001754)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 156.64/22.36 % (4001754)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 156.64/22.36 % (4001754)CaDiCaL version: 2.1.3 % 156.64/22.36 % (4001754)Termination reason: Instruction limit % 156.64/22.36 % (4001754)Termination phase: Saturation % 156.64/22.36 % (4001754)Time elapsed: 5.503 s % 156.64/22.36 % (4001754)Peak memory usage: 121 MB % 156.64/22.36 % (4001754)Instructions burned: 17629 (million) % 156.64/22.36 % (4002141)dis+10_1_sil=32000:si=on:sp=arity:random_seed=2343406711:i=206:fgj=on:rtra=on_2811 on theBenchmark for (2811ds/206Mi) % 156.64/22.36 % (4002141)Instruction limit reached! % 156.64/22.36 % (4002141)------------------------------ % 156.64/22.36 % (4002141)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 156.64/22.36 % (4002141)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 156.64/22.36 % (4002141)CaDiCaL version: 2.1.3 % 156.64/22.36 % (4002141)Termination reason: Instruction limit % 156.64/22.36 % (4002141)Termination phase: Saturation % 156.64/22.36 % (4002141)Time elapsed: 0.069 s % 156.64/22.36 % (4002141)Peak memory usage: 13 MB % 156.64/22.36 % (4002141)Instructions burned: 208 (million) % 156.64/22.36 % (4002143)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=3582444343:i=232:rtra=on_2810 on theBenchmark for (2810ds/232Mi) % 156.64/22.36 % (4002143)Instruction limit reached! % 156.64/22.36 % (4002143)------------------------------ % 156.64/22.36 % (4002143)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 156.64/22.36 % (4002143)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 156.64/22.36 % (4002143)CaDiCaL version: 2.1.3 % 156.64/22.36 % (4002143)Termination reason: Instruction limit % 156.64/22.36 % (4002143)Termination phase: Saturation % 156.64/22.36 % (4002143)Time elapsed: 0.073 s % 156.64/22.36 % (4002143)Peak memory usage: 14 MB % 156.64/22.36 % (4002143)Instructions burned: 233 (million) % 156.64/22.36 % (4002145)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=3201646370:i=262:rtra=on_2809 on theBenchmark for (2809ds/262Mi) % 156.64/22.36 % (4002145)Instruction limit reached! % 156.64/22.36 % (4002145)------------------------------ % 156.64/22.36 % (4002145)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 156.64/22.36 % (4002145)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 156.64/22.36 % (4002145)CaDiCaL version: 2.1.3 % 156.64/22.36 % (4002145)Termination reason: Instruction limit % 156.64/22.36 % (4002145)Termination phase: Saturation % 156.64/22.36 % (4002145)Time elapsed: 0.088 s % 156.64/22.36 % (4002145)Peak memory usage: 14 MB % 156.64/22.36 % (4002145)Instructions burned: 265 (million) % 156.64/22.36 % (4002147)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=3316985100:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2808 on theBenchmark for (2808ds/318Mi) % 156.64/22.36 % (4002147)Instruction limit reached! % 156.64/22.36 % (4002147)------------------------------ % 156.64/22.36 % (4002147)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 156.64/22.36 % (4002147)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 156.64/22.36 % (4002147)CaDiCaL version: 2.1.3 % 156.64/22.36 % (4002147)Termination reason: Instruction limit % 156.64/22.36 % (4002147)Termination phase: Saturation % 156.64/22.36 % (4002147)Time elapsed: 0.121 s % 156.64/22.36 % (4002147)Peak memory usage: 15 MB % 156.64/22.36 % (4002147)Instructions burned: 320 (million) % 156.64/22.36 % (4002149)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=1103746092:i=1428:nm=2:rtra=on_2807 on theBenchmark for (2807ds/1428Mi) % 185.04/26.30 % (4002149)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 185.04/26.30 % (4002149)Terminated due to inappropriate strategy. % 185.04/26.30 % (4002149)------------------------------ % 185.04/26.30 % (4002149)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 185.04/26.30 % (4002149)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 185.04/26.30 % (4002149)CaDiCaL version: 2.1.3 % 185.04/26.30 % (4002149)Termination reason: Inappropriate % 185.04/26.30 % (4002149)Time elapsed: 0.002 s % 185.04/26.30 % (4002149)Peak memory usage: 10 MB % 185.04/26.30 % (4002149)Instructions burned: 8 (million) % 185.04/26.30 % (4002149)------------------------------ % 185.04/26.30 % (4002149)------------------------------ % 185.04/26.30 % (4002151)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=481853174:i=262:bd=preordered:rtra=on:fsd=on_2807 on theBenchmark for (2807ds/262Mi) % 185.04/26.30 % (4002151)Instruction limit reached! % 185.04/26.30 % (4002151)------------------------------ % 185.04/26.30 % (4002151)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 185.04/26.30 % (4002151)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 185.04/26.30 % (4002151)CaDiCaL version: 2.1.3 % 185.04/26.30 % (4002151)Termination reason: Instruction limit % 185.04/26.30 % (4002151)Termination phase: Saturation % 185.04/26.30 % (4002151)Time elapsed: 0.090 s % 185.04/26.30 % (4002151)Peak memory usage: 13 MB % 185.04/26.30 % (4002151)Instructions burned: 264 (million) % 185.04/26.30 % (4002153)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=2628540669:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2806 on theBenchmark for (2806ds/1368Mi) % 185.04/26.30 % (4002153)Instruction limit reached! % 185.04/26.30 % (4002153)------------------------------ % 185.04/26.30 % (4002153)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 185.04/26.30 % (4002153)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 185.04/26.30 % (4002153)CaDiCaL version: 2.1.3 % 185.04/26.30 % (4002153)Termination reason: Instruction limit % 185.04/26.30 % (4002153)Termination phase: Saturation % 185.04/26.30 % (4002153)Time elapsed: 0.423 s % 185.04/26.30 % (4002153)Peak memory usage: 25 MB % 185.04/26.30 % (4002153)Instructions burned: 1370 (million) % 185.04/26.30 % (4002155)ott-21_1_sil=16000:si=on:fs=off:random_seed=563998586:i=360:av=off:fsr=off:rtra=on_2802 on theBenchmark for (2802ds/360Mi) % 185.04/26.30 % (4002155)Instruction limit reached! % 185.04/26.30 % (4002155)------------------------------ % 185.04/26.30 % (4002155)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 185.04/26.30 % (4002155)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 185.04/26.30 % (4002155)CaDiCaL version: 2.1.3 % 185.04/26.30 % (4002155)Termination reason: Instruction limit % 185.04/26.30 % (4002155)Termination phase: Saturation % 185.04/26.30 % (4002155)Time elapsed: 0.096 s % 185.04/26.30 % (4002155)Peak memory usage: 14 MB % 185.04/26.30 % (4002155)Instructions burned: 364 (million) % 185.04/26.30 % (4002157)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2086564210:i=954:bd=all:rtra=on_2801 on theBenchmark for (2801ds/954Mi) % 185.04/26.30 % (4002157)Instruction limit reached! % 185.04/26.30 % (4002157)------------------------------ % 185.04/26.30 % (4002157)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 185.04/26.30 % (4002157)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 185.04/26.30 % (4002157)CaDiCaL version: 2.1.3 % 185.04/26.30 % (4002157)Termination reason: Instruction limit % 185.04/26.30 % (4002157)Termination phase: Saturation % 185.04/26.30 % (4002157)Time elapsed: 0.343 s % 185.04/26.30 % (4002157)Peak memory usage: 16 MB % 185.04/26.30 % (4002157)Instructions burned: 956 (million) % 185.04/26.30 % (4002159)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=1609266199:fmbsr=1.3:i=1730:ins=25:rtra=on_2797 on theBenchmark for (2797ds/1730Mi) % 185.04/26.30 % (4002159)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 185.04/26.30 % (4002159)Terminated due to inappropriate strategy. % 185.04/26.30 % (4002159)------------------------------ % 185.04/26.30 % (4002159)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 185.04/26.30 % (4002159)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 185.04/26.30 % (4002159)CaDiCaL version: 2.1.3 % 185.04/26.30 % (4002159)Termination reason: Inappropriate % 185.04/26.30 % (4002159)Time elapsed: 0.002 s % 231.19/32.84 % (4002159)Peak memory usage: 10 MB % 231.19/32.84 % (4002159)Instructions burned: 8 (million) % 231.19/32.84 % (4002159)------------------------------ % 231.19/32.84 % (4002159)------------------------------ % 231.19/32.84 % (4002161)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=718134266:i=2358:rtra=on_2797 on theBenchmark for (2797ds/2358Mi) % 231.19/32.84 % (4002161)Instruction limit reached! % 231.19/32.84 % (4002161)------------------------------ % 231.19/32.84 % (4002161)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 231.19/32.84 % (4002161)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 231.19/32.84 % (4002161)CaDiCaL version: 2.1.3 % 231.19/32.84 % (4002161)Termination reason: Instruction limit % 231.19/32.84 % (4002161)Termination phase: Saturation % 231.19/32.84 % (4002161)Time elapsed: 0.805 s % 231.19/32.84 % (4002161)Peak memory usage: 28 MB % 231.19/32.84 % (4002161)Instructions burned: 2358 (million) % 231.19/32.84 % (4002163)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=823612717:i=1778:ins=1:rtra=on_2789 on theBenchmark for (2789ds/1778Mi) % 231.19/32.84 % (4002163)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 231.19/32.84 % (4002163)Terminated due to inappropriate strategy. % 231.19/32.84 % (4002163)------------------------------ % 231.19/32.84 % (4002163)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 231.19/32.84 % (4002163)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 231.19/32.84 % (4002163)CaDiCaL version: 2.1.3 % 231.19/32.84 % (4002163)Termination reason: Inappropriate % 231.19/32.84 % (4002163)Time elapsed: 0.002 s % 231.19/32.84 % (4002163)Peak memory usage: 10 MB % 231.19/32.84 % (4002163)Instructions burned: 8 (million) % 231.19/32.84 % (4002163)------------------------------ % 231.19/32.84 % (4002163)------------------------------ % 231.19/32.84 % (4002165)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=2309096621:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2789 on theBenchmark for (2789ds/1384Mi) % 231.19/32.84 % (4002165)Instruction limit reached! % 231.19/32.84 % (4002165)------------------------------ % 231.19/32.84 % (4002165)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 231.19/32.84 % (4002165)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 231.19/32.84 % (4002165)CaDiCaL version: 2.1.3 % 231.19/32.84 % (4002165)Termination reason: Instruction limit % 231.19/32.84 % (4002165)Termination phase: Saturation % 231.19/32.84 % (4002165)Time elapsed: 0.420 s % 231.19/32.84 % (4002165)Peak memory usage: 35 MB % 231.19/32.84 % (4002165)Instructions burned: 1384 (million) % 231.19/32.84 % (4002167)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=565617381:i=1758:kws=inv_precedence:fsr=off:rtra=on_2784 on theBenchmark for (2784ds/1758Mi) % 231.19/32.84 % (4002167)Instruction limit reached! % 231.19/32.84 % (4002167)------------------------------ % 231.19/32.84 % (4002167)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 231.19/32.84 % (4002167)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 231.19/32.84 % (4002167)CaDiCaL version: 2.1.3 % 231.19/32.84 % (4002167)Termination reason: Instruction limit % 231.19/32.84 % (4002167)Termination phase: Saturation % 231.19/32.84 % (4002167)Time elapsed: 0.556 s % 231.19/32.84 % (4002167)Peak memory usage: 26 MB % 231.19/32.84 % (4002167)Instructions burned: 1761 (million) % 231.19/32.84 % (4002169)fmb+10_1_sil=64000:si=on:random_seed=3123458693:i=44122:nm=2:rtra=on:gsp=on_2778 on theBenchmark for (2778ds/44122Mi) % 231.19/32.84 % (4002169)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 231.19/32.84 % (4002169)Terminated due to inappropriate strategy. % 231.19/32.84 % (4002169)------------------------------ % 231.19/32.84 % (4002169)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 231.19/32.84 % (4002169)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 231.19/32.84 % (4002169)CaDiCaL version: 2.1.3 % 231.19/32.84 % (4002169)Termination reason: Inappropriate % 231.19/32.84 % (4002169)Time elapsed: 0.003 s % 231.19/32.84 % (4002169)Peak memory usage: 10 MB % 231.19/32.84 % (4002169)Instructions burned: 9 (million) % 231.19/32.84 % (4002169)------------------------------ % 231.19/32.84 % (4002169)------------------------------ % 231.19/32.84 % (4002171)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=1871334281:i=19030:nm=5:rtra=on_2778 on theBenchmark for (2778ds/19030Mi) % 257.29/36.50 % (4002171)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 257.29/36.50 % (4002171)Terminated due to inappropriate strategy. % 257.29/36.50 % (4002171)------------------------------ % 257.29/36.50 % (4002171)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 257.29/36.50 % (4002171)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 257.29/36.50 % (4002171)CaDiCaL version: 2.1.3 % 257.29/36.50 % (4002171)Termination reason: Inappropriate % 257.29/36.50 % (4002171)Time elapsed: 0.002 s % 257.29/36.50 % (4002171)Peak memory usage: 10 MB % 257.29/36.50 % (4002171)Instructions burned: 8 (million) % 257.29/36.50 % (4002171)------------------------------ % 257.29/36.50 % (4002171)------------------------------ % 257.29/36.50 % (4002173)fmb+10_1_sil=64000:sas=cadical:si=on:fmbss=8:random_seed=2730881002:fmbsr=1.7:i=1840:rtra=on_2778 on theBenchmark for (2778ds/1840Mi) % 257.29/36.50 % (4002173)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 257.29/36.50 % (4002173)Terminated due to inappropriate strategy. % 257.29/36.50 % (4002173)------------------------------ % 257.29/36.50 % (4002173)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 257.29/36.50 % (4002173)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 257.29/36.50 % (4002173)CaDiCaL version: 2.1.3 % 257.29/36.50 % (4002173)Termination reason: Inappropriate % 257.29/36.50 % (4002173)Time elapsed: 0.002 s % 257.29/36.50 % (4002173)Peak memory usage: 10 MB % 257.29/36.50 % (4002173)Instructions burned: 8 (million) % 257.29/36.50 % (4002173)------------------------------ % 257.29/36.50 % (4002173)------------------------------ % 257.29/36.50 % (4002175)dis-4_1_sil=16000:drc=ordering:si=on:sp=const_frequency:sac=on:newcnf=on:random_seed=3508759757:i=10262:rtra=on_2778 on theBenchmark for (2778ds/10262Mi) % 257.29/36.50 % (4002175)Instruction limit reached! % 257.29/36.50 % (4002175)------------------------------ % 257.29/36.50 % (4002175)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 257.29/36.50 % (4002175)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 257.29/36.50 % (4002175)CaDiCaL version: 2.1.3 % 257.29/36.50 % (4002175)Termination reason: Instruction limit % 257.29/36.50 % (4002175)Termination phase: Saturation % 257.29/36.50 % (4002175)Time elapsed: 3.067 s % 257.29/36.50 % (4002175)Peak memory usage: 66 MB % 257.29/36.50 % (4002175)Instructions burned: 10264 (million) % 257.29/36.50 % (4002177)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:si=on:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3006817497:i=2944:ins=7:rtra=on:fdi=8:gsp=on_2747 on theBenchmark for (2747ds/2944Mi) % 257.29/36.50 % (4002177)Instruction limit reached! % 257.29/36.50 % (4002177)------------------------------ % 257.29/36.50 % (4002177)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 257.29/36.50 % (4002177)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 257.29/36.50 % (4002177)CaDiCaL version: 2.1.3 % 257.29/36.50 % (4002177)Termination reason: Instruction limit % 257.29/36.50 % (4002177)Termination phase: Saturation % 257.29/36.50 % (4002177)Time elapsed: 0.795 s % 257.29/36.50 % (4002177)Peak memory usage: 36 MB % 257.29/36.50 % (4002177)Instructions burned: 2945 (million) % 257.29/36.50 % (4002179)fmb+10_1_sil=16000:sas=cadical:si=on:bce=on:fmbss=77:random_seed=1615958574:i=12648:rtra=on_2739 on theBenchmark for (2739ds/12648Mi) % 257.29/36.50 % (4002179)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 257.29/36.50 % (4002179)Terminated due to inappropriate strategy. % 257.29/36.50 % (4002179)------------------------------ % 257.29/36.50 % (4002179)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 257.29/36.50 % (4002179)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 257.29/36.50 % (4002179)CaDiCaL version: 2.1.3 % 257.29/36.50 % (4002179)Termination reason: Inappropriate % 257.29/36.50 % (4002179)Time elapsed: 0.003 s % 257.29/36.50 % (4002179)Peak memory usage: 11 MB % 257.29/36.50 % (4002179)Instructions burned: 9 (million) % 257.29/36.50 % (4002179)------------------------------ % 257.29/36.50 % (4002179)------------------------------ % 257.29/36.50 % (4002181)fmb+10_1_fmbas=function:sil=32000:sas=cadical:si=on:fmbss=16:random_seed=2673039782:fmbsr=2.30978:i=4348:rtra=on_2739 on theBenchmark for (2739ds/4348Mi) % 257.29/36.50 % (4002181)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 257.29/36.50 % (4002181)Terminated due to inappropriate strategy. % 257.29/36.50 % (4002181)------------------------------ % 257.29/36.50 % (4002181)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.39/42.63 % (4002181)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.39/42.63 % (4002181)CaDiCaL version: 2.1.3 % 300.39/42.63 % (4002181)Termination reason: Inappropriate % 300.39/42.63 % (4002181)Time elapsed: 0.002 s % 300.39/42.63 % (4002181)Peak memory usage: 10 MB % 300.39/42.63 % (4002181)Instructions burned: 8 (million) % 300.39/42.63 % (4002181)------------------------------ % 300.39/42.63 % (4002181)------------------------------ % 300.39/42.63 % (4002183)ott-2_1_sil=16000:si=on:newcnf=on:random_seed=2997567094:avsq=on:i=1738:avsqr=1,16:kws=inv_arity_squared:rtra=on_2739 on theBenchmark for (2739ds/1738Mi) % 300.39/42.63 % (4002183)Instruction limit reached! % 300.39/42.63 % (4002183)------------------------------ % 300.39/42.63 % (4002183)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.39/42.63 % (4002183)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.39/42.63 % (4002183)CaDiCaL version: 2.1.3 % 300.39/42.63 % (4002183)Termination reason: Instruction limit % 300.39/42.63 % (4002183)Termination phase: Saturation % 300.39/42.63 % (4002183)Time elapsed: 0.594 s % 300.39/42.63 % (4002183)Peak memory usage: 20 MB % 300.39/42.63 % (4002183)Instructions burned: 1741 (million) % 300.39/42.63 % (4002185)ott+10_1_sil=32000:tgt=ground:si=on:random_seed=1486127593:i=10228:av=off:rtra=on_2733 on theBenchmark for (2733ds/10228Mi) % 300.39/42.63 % (4002185)Instruction limit reached! % 300.39/42.63 % (4002185)------------------------------ % 300.39/42.63 % (4002185)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.39/42.63 % (4002185)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.39/42.63 % (4002185)CaDiCaL version: 2.1.3 % 300.39/42.63 % (4002185)Termination reason: Instruction limit % 300.39/42.63 % (4002185)Termination phase: Saturation % 300.39/42.63 % (4002185)Time elapsed: 3.665 s % 300.39/42.63 % (4002185)Peak memory usage: 60 MB % 300.39/42.63 % (4002185)Instructions burned: 10231 (million) % 300.39/42.63 % (4002249)fmb+10_1_sil=64000:sas=cadical:si=on:bce=on:rp=on:random_seed=3895384108:i=108564:rtra=on_2696 on theBenchmark for (2696ds/108564Mi) % 300.39/42.63 % (4002249)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 300.39/42.63 % (4002249)Terminated due to inappropriate strategy. % 300.39/42.63 % (4002249)------------------------------ % 300.39/42.63 % (4002249)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.39/42.63 % (4002249)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.39/42.63 % (4002249)CaDiCaL version: 2.1.3 % 300.39/42.63 % (4002249)Termination reason: Inappropriate % 300.39/42.63 % (4002249)Time elapsed: 0.003 s % 300.39/42.63 % (4002249)Peak memory usage: 11 MB % 300.39/42.63 % (4002249)Instructions burned: 9 (million) % 300.39/42.63 % (4002249)------------------------------ % 300.39/42.63 % (4002249)------------------------------ % 300.39/42.63 % (4002251)dis-11_1_sil=16000:si=on:sp=reverse_frequency:alpa=true:random_seed=4130263040:i=7024:aac=none:rtra=on_2696 on theBenchmark for (2696ds/7024Mi) % 300.39/42.63 % (4002122)Instruction limit reached! % 300.39/42.63 % (4002122)------------------------------ % 300.39/42.63 % (4002122)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.39/42.63 % (4002122)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.39/42.63 % (4002122)CaDiCaL version: 2.1.3 % 300.39/42.63 % (4002122)Termination reason: Instruction limit % 300.39/42.63 % (4002122)Termination phase: Saturation % 300.39/42.63 % (4002122)Time elapsed: 15.476 s % 300.39/42.63 % (4002122)Peak memory usage: 105 MB % 300.39/42.63 % (4002122)Instructions burned: 28121 (million) % 300.39/42.63 % (4002253)dis+21_1_sil=32000:sas=cadical:si=on:random_seed=3302876590:i=7546:rtra=on:amm=off_2688 on theBenchmark for (2688ds/7546Mi) % 300.39/42.63 % (4002251)Instruction limit reached! % 300.39/42.63 % (4002251)------------------------------ % 300.39/42.63 % (4002251)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.39/42.63 % (4002251)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.39/42.63 % (4002251)CaDiCaL version: 2.1.3 % 300.39/42.63 % (4002251)Termination reason: Instruction limit % 300.39/42.63 % (4002251)Termination phase: Saturation % 300.39/42.63 % (4002251)Time elapsed: 2.213 s % 300.39/42.63 % (4002251)Peak memory usage: 43 MB % 300.39/42.63 % (4002251)Instructions burned: 7027 (million) % 300.39/42.63 % (4002255)ott+11_1_sil=16000:si=on:gs=on:random_seed=1282379498:s2a=on:i=4502:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:rtra=on:fsd=on_2674 on theBenchmar % 300.39/42.63 Terminated % 300.39/42.63 % Vampire exiting % 300.39/42.63 Terminated %------------------------------------------------------------------------------