%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWX111_1 : TPTP v9.3.1. Released v9.1.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % Computer : n018.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:30 PM UTC 2026 % Result : Timeout 300.10s 42.54s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWX111_1 : TPTP v9.3.1. Released v9.1.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.09/0.18 % Computer : n018.cluster.edu % 0.09/0.18 % Model : x86_64 x86_64 % 0.09/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.18 % Memory : 8046.5625MB % 0.09/0.18 % OS : Linux 6.8.0-71-generic % 0.09/0.18 % CPULimit : 300 % 0.09/0.18 % WCLimit : 300 % 0.09/0.18 % DateTime : Mon Sep 28 15:04:10 UTC 2026 % 0.09/0.18 % CPUTime : % 0.09/0.18 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.09/0.21 Running first-order model finding % 0.09/0.21 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 % 3.32/0.71 % (3466220)Will run a generic schedule for satisfiability detection. % 3.32/0.71 % (3466225)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2382721898_2999 on theBenchmark for (2999ds/0Mi) % 3.32/0.71 % (3466225)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.32/0.71 % (3466225)Terminated due to inappropriate strategy. % 3.32/0.71 % (3466225)------------------------------ % 3.32/0.71 % (3466225)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.32/0.71 % (3466225)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.32/0.71 % (3466225)CaDiCaL version: 2.1.3 % 3.32/0.71 % (3466225)Termination reason: Inappropriate % 3.32/0.71 % (3466225)Time elapsed: 0.001 s % 3.32/0.71 % (3466225)Peak memory usage: 11 MB % 3.32/0.71 % (3466225)Instructions burned: 1 (million) % 3.32/0.71 % (3466225)------------------------------ % 3.32/0.71 % (3466225)------------------------------ % 3.32/0.71 % (3466226)% WARNING: option uhcvi not known. % 3.32/0.71 % (3466226)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2371692385:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 3.32/0.71 % (3466227)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=884039474:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 3.32/0.71 % (3466228)dis+10_1_sil=32000:sp=arity:random_seed=2348180970:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 3.32/0.71 % (3466230)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=4067633652:i=131_2999 on theBenchmark for (2999ds/131Mi) % 3.32/0.71 % (3466229)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=4278768913:i=116_2999 on theBenchmark for (2999ds/116Mi) % 3.32/0.71 % (3466231)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=393154463:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 3.32/0.71 % (3466233)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3193219333:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 3.32/0.71 % (3466233)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.32/0.71 % (3466233)Terminated due to inappropriate strategy. % 3.32/0.71 % (3466233)------------------------------ % 3.32/0.71 % (3466233)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.32/0.71 % (3466233)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.32/0.71 % (3466233)CaDiCaL version: 2.1.3 % 3.32/0.71 % (3466233)Termination reason: Inappropriate % 3.32/0.71 % (3466233)Time elapsed: 0.0000 s % 3.32/0.71 % (3466233)Peak memory usage: 11 MB % 3.32/0.71 % (3466233)Instructions burned: 1 (million) % 3.32/0.71 % (3466233)------------------------------ % 3.32/0.71 % (3466233)------------------------------ % 3.32/0.71 % (3466241)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2399322874:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 3.32/0.71 % (3466228)Instruction limit reached! % 3.32/0.71 % (3466228)------------------------------ % 3.32/0.71 % (3466228)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.32/0.71 % (3466228)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.32/0.71 % (3466228)CaDiCaL version: 2.1.3 % 3.32/0.71 % (3466228)Termination reason: Instruction limit % 3.32/0.71 % (3466228)Termination phase: Saturation % 3.32/0.71 % (3466228)Time elapsed: 0.065 s % 3.32/0.71 % (3466228)Peak memory usage: 12 MB % 3.32/0.71 % (3466228)Instructions burned: 103 (million) % 3.32/0.71 % (3466241)Instruction limit reached! % 3.32/0.71 % (3466241)------------------------------ % 3.32/0.71 % (3466241)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.32/0.71 % (3466241)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.32/0.71 % (3466241)CaDiCaL version: 2.1.3 % 3.32/0.71 % (3466241)Termination reason: Instruction limit % 3.32/0.71 % (3466241)Termination phase: Saturation % 3.32/0.71 % (3466241)Time elapsed: 0.049 s % 3.32/0.71 % (3466241)Peak memory usage: 13 MB % 3.32/0.71 % (3466241)Instructions burned: 132 (million) % 3.32/0.71 % (3466244)ott-21_1_sil=16000:fs=off:random_seed=299769783:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi) % 3.32/0.71 % (3466229)Instruction limit reached! % 3.32/0.71 % (3466229)------------------------------ % 3.32/0.71 % (3466229)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.32/0.71 % (3466229)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.74/1.12 % (3466229)CaDiCaL version: 2.1.3 % 5.74/1.12 % (3466229)Termination reason: Instruction limit % 5.74/1.12 % (3466229)Termination phase: Saturation % 5.74/1.12 % (3466229)Time elapsed: 0.076 s % 5.74/1.12 % (3466229)Peak memory usage: 12 MB % 5.74/1.12 % (3466229)Instructions burned: 121 (million) % 5.74/1.12 % (3466230)Instruction limit reached! % 5.74/1.12 % (3466230)------------------------------ % 5.74/1.12 % (3466230)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.74/1.12 % (3466230)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.74/1.12 % (3466230)CaDiCaL version: 2.1.3 % 5.74/1.12 % (3466230)Termination reason: Instruction limit % 5.74/1.12 % (3466230)Termination phase: Saturation % 5.74/1.12 % (3466230)Time elapsed: 0.079 s % 5.74/1.12 % (3466230)Peak memory usage: 13 MB % 5.74/1.12 % (3466230)Instructions burned: 131 (million) % 5.74/1.12 % (3466243)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=794489225:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi) % 5.74/1.12 % (3466246)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2723981931:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 5.74/1.12 % (3466247)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3362963950:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 5.74/1.12 % (3466247)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 5.74/1.12 % (3466247)Terminated due to inappropriate strategy. % 5.74/1.12 % (3466247)------------------------------ % 5.74/1.12 % (3466247)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.74/1.12 % (3466247)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.74/1.12 % (3466247)CaDiCaL version: 2.1.3 % 5.74/1.12 % (3466247)Termination reason: Inappropriate % 5.74/1.12 % (3466247)Time elapsed: 0.001 s % 5.74/1.12 % (3466247)Peak memory usage: 10 MB % 5.74/1.12 % (3466247)Instructions burned: 1 (million) % 5.74/1.12 % (3466247)------------------------------ % 5.74/1.12 % (3466247)------------------------------ % 5.74/1.12 % (3466231)Instruction limit reached! % 5.74/1.12 % (3466231)------------------------------ % 5.74/1.12 % (3466231)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.74/1.12 % (3466231)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.74/1.12 % (3466231)CaDiCaL version: 2.1.3 % 5.74/1.12 % (3466231)Termination reason: Instruction limit % 5.74/1.12 % (3466231)Termination phase: Saturation % 5.74/1.12 % (3466231)Time elapsed: 0.110 s % 5.74/1.12 % (3466231)Peak memory usage: 13 MB % 5.74/1.12 % (3466231)Instructions burned: 160 (million) % 5.74/1.12 % (3466251)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3233268203:i=1179_2998 on theBenchmark for (2998ds/1179Mi) % 5.74/1.12 % (3466244)Instruction limit reached! % 5.74/1.12 % (3466244)------------------------------ % 5.74/1.12 % (3466244)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.74/1.12 % (3466244)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.74/1.12 % (3466244)CaDiCaL version: 2.1.3 % 5.74/1.12 % (3466244)Termination reason: Instruction limit % 5.74/1.12 % (3466244)Termination phase: Saturation % 5.74/1.12 % (3466244)Time elapsed: 0.044 s % 5.74/1.12 % (3466244)Peak memory usage: 12 MB % 5.74/1.12 % (3466244)Instructions burned: 185 (million) % 5.74/1.12 % (3466252)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1828573985:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi) % 5.74/1.12 % (3466252)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 5.74/1.12 % (3466252)Terminated due to inappropriate strategy. % 5.74/1.12 % (3466252)------------------------------ % 5.74/1.12 % (3466252)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.74/1.12 % (3466252)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.74/1.12 % (3466252)CaDiCaL version: 2.1.3 % 5.74/1.12 % (3466252)Termination reason: Inappropriate % 5.74/1.12 % (3466252)Time elapsed: 0.001 s % 5.74/1.12 % (3466252)Peak memory usage: 10 MB % 5.74/1.12 % (3466252)Instructions burned: 1 (million) % 5.74/1.12 % (3466254)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=2966139557: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.19/3.02 % (3466252)------------------------------ % 18.19/3.02 % (3466252)------------------------------ % 18.19/3.02 % (3466257)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2503020433:i=879:kws=inv_precedence:fsr=off_2998 on theBenchmark for (2998ds/879Mi) % 18.19/3.02 % (3466254)Instruction limit reached! % 18.19/3.02 % (3466254)------------------------------ % 18.19/3.02 % (3466254)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 18.19/3.02 % (3466254)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.19/3.02 % (3466254)CaDiCaL version: 2.1.3 % 18.19/3.02 % (3466254)Termination reason: Instruction limit % 18.19/3.02 % (3466254)Termination phase: Saturation % 18.19/3.02 % (3466254)Time elapsed: 0.218 s % 18.19/3.02 % (3466254)Peak memory usage: 18 MB % 18.19/3.02 % (3466254)Instructions burned: 696 (million) % 18.19/3.02 % (3466259)fmb+10_1_sil=64000:random_seed=2761258197:i=22061:nm=2:gsp=on_2996 on theBenchmark for (2996ds/22061Mi) % 18.19/3.02 % (3466259)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 18.19/3.02 % (3466259)Terminated due to inappropriate strategy. % 18.19/3.02 % (3466259)------------------------------ % 18.19/3.02 % (3466259)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 18.19/3.02 % (3466259)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.19/3.02 % (3466259)CaDiCaL version: 2.1.3 % 18.19/3.02 % (3466259)Termination reason: Inappropriate % 18.19/3.02 % (3466259)Time elapsed: 0.0000 s % 18.19/3.02 % (3466259)Peak memory usage: 10 MB % 18.19/3.02 % (3466259)Instructions burned: 1 (million) % 18.19/3.02 % (3466259)------------------------------ % 18.19/3.02 % (3466259)------------------------------ % 18.19/3.02 % (3466261)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2932679903:i=9515:nm=5_2996 on theBenchmark for (2996ds/9515Mi) % 18.19/3.02 % (3466261)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 18.19/3.02 % (3466261)Terminated due to inappropriate strategy. % 18.19/3.02 % (3466261)------------------------------ % 18.19/3.02 % (3466261)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 18.19/3.02 % (3466261)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.19/3.02 % (3466261)CaDiCaL version: 2.1.3 % 18.19/3.02 % (3466261)Termination reason: Inappropriate % 18.19/3.02 % (3466261)Time elapsed: 0.0000 s % 18.19/3.02 % (3466261)Peak memory usage: 10 MB % 18.19/3.02 % (3466261)Instructions burned: 1 (million) % 18.19/3.02 % (3466261)------------------------------ % 18.19/3.02 % (3466261)------------------------------ % 18.19/3.02 % (3466263)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2760143343:fmbsr=1.7:i=920_2995 on theBenchmark for (2995ds/920Mi) % 18.19/3.02 % (3466263)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 18.19/3.02 % (3466263)Terminated due to inappropriate strategy. % 18.19/3.02 % (3466263)------------------------------ % 18.19/3.02 % (3466263)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 18.19/3.02 % (3466263)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.19/3.02 % (3466263)CaDiCaL version: 2.1.3 % 18.19/3.02 % (3466263)Termination reason: Inappropriate % 18.19/3.02 % (3466263)Time elapsed: 0.0000 s % 18.19/3.02 % (3466263)Peak memory usage: 10 MB % 18.19/3.02 % (3466263)Instructions burned: 1 (million) % 18.19/3.02 % (3466263)------------------------------ % 18.19/3.02 % (3466263)------------------------------ % 18.19/3.02 % (3466265)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=4003483323:i=5131_2995 on theBenchmark for (2995ds/5131Mi) % 18.19/3.02 % (3466246)Instruction limit reached! % 18.19/3.02 % (3466246)------------------------------ % 18.19/3.02 % (3466246)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 18.19/3.02 % (3466246)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.19/3.02 % (3466246)CaDiCaL version: 2.1.3 % 18.19/3.02 % (3466246)Termination reason: Instruction limit % 18.19/3.02 % (3466246)Termination phase: Saturation % 18.19/3.02 % (3466246)Time elapsed: 0.309 s % 18.19/3.02 % (3466246)Peak memory usage: 13 MB % 18.19/3.02 % (3466246)Instructions burned: 478 (million) % 18.19/3.02 % (3466267)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=152632710:i=1472:ins=7:fdi=8:gsp=on_2995 on theBenchmark for (2995ds/1472Mi) % 18.19/3.02 % (3466243)Instruction limit reached! % 18.19/3.02 % (3466243)------------------------------ % 28.22/4.20 % (3466243)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 28.22/4.20 % (3466243)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.22/4.20 % (3466243)CaDiCaL version: 2.1.3 % 28.22/4.20 % (3466243)Termination reason: Instruction limit % 28.22/4.20 % (3466243)Termination phase: Saturation % 28.22/4.20 % (3466243)Time elapsed: 0.371 s % 28.22/4.20 % (3466243)Peak memory usage: 17 MB % 28.22/4.20 % (3466243)Instructions burned: 684 (million) % 28.22/4.20 % (3466269)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=4225952385:i=6324_2995 on theBenchmark for (2995ds/6324Mi) % 28.22/4.20 % (3466269)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 28.22/4.20 % (3466269)Terminated due to inappropriate strategy. % 28.22/4.20 % (3466269)------------------------------ % 28.22/4.20 % (3466269)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 28.22/4.20 % (3466269)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.22/4.20 % (3466269)CaDiCaL version: 2.1.3 % 28.22/4.20 % (3466269)Termination reason: Inappropriate % 28.22/4.20 % (3466269)Time elapsed: 0.001 s % 28.22/4.20 % (3466269)Peak memory usage: 11 MB % 28.22/4.20 % (3466269)Instructions burned: 1 (million) % 28.22/4.20 % (3466269)------------------------------ % 28.22/4.20 % (3466269)------------------------------ % 28.22/4.20 % (3466271)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=563796461:fmbsr=2.30978:i=2174_2994 on theBenchmark for (2994ds/2174Mi) % 28.22/4.20 % (3466271)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 28.22/4.20 % (3466271)Terminated due to inappropriate strategy. % 28.22/4.20 % (3466271)------------------------------ % 28.22/4.20 % (3466271)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 28.22/4.20 % (3466271)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.22/4.20 % (3466271)CaDiCaL version: 2.1.3 % 28.22/4.20 % (3466271)Termination reason: Inappropriate % 28.22/4.20 % (3466271)Time elapsed: 0.001 s % 28.22/4.20 % (3466271)Peak memory usage: 10 MB % 28.22/4.20 % (3466271)Instructions burned: 1 (million) % 28.22/4.20 % (3466271)------------------------------ % 28.22/4.20 % (3466271)------------------------------ % 28.22/4.20 % (3466273)ott-2_1_sil=16000:newcnf=on:random_seed=2388652328:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2994 on theBenchmark for (2994ds/869Mi) % 28.22/4.20 % (3466257)Instruction limit reached! % 28.22/4.20 % (3466257)------------------------------ % 28.22/4.20 % (3466257)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 28.22/4.20 % (3466257)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.22/4.20 % (3466257)CaDiCaL version: 2.1.3 % 28.22/4.20 % (3466257)Termination reason: Instruction limit % 28.22/4.20 % (3466257)Termination phase: Saturation % 28.22/4.20 % (3466257)Time elapsed: 0.505 s % 28.22/4.20 % (3466257)Peak memory usage: 19 MB % 28.22/4.20 % (3466257)Instructions burned: 880 (million) % 28.22/4.20 % (3466275)ott+10_1_sil=32000:tgt=ground:random_seed=1146064705:i=5114:av=off_2993 on theBenchmark for (2993ds/5114Mi) % 28.22/4.20 % (3466251)Instruction limit reached! % 28.22/4.20 % (3466251)------------------------------ % 28.22/4.20 % (3466251)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 28.22/4.20 % (3466251)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.22/4.20 % (3466251)CaDiCaL version: 2.1.3 % 28.22/4.20 % (3466251)Termination reason: Instruction limit % 28.22/4.20 % (3466251)Termination phase: Saturation % 28.22/4.20 % (3466251)Time elapsed: 0.724 s % 28.22/4.20 % (3466251)Peak memory usage: 20 MB % 28.22/4.20 % (3466251)Instructions burned: 1180 (million) % 28.22/4.20 % (3466277)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2287669469:i=54282_2991 on theBenchmark for (2991ds/54282Mi) % 28.22/4.20 % (3466277)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 28.22/4.20 % (3466277)Terminated due to inappropriate strategy. % 28.22/4.20 % (3466277)------------------------------ % 28.22/4.20 % (3466277)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 28.22/4.20 % (3466277)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.22/4.20 % (3466277)CaDiCaL version: 2.1.3 % 28.22/4.20 % (3466277)Termination reason: Inappropriate % 28.22/4.20 % (3466277)Time elapsed: 0.001 s % 28.22/4.20 % (3466277)Peak memory usage: 11 MB % 28.22/4.20 % (3466277)Instructions burned: 1 (million) % 83.86/12.07 % (3466277)------------------------------ % 83.86/12.07 % (3466277)------------------------------ % 83.86/12.07 % (3466279)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3761177173:i=3512:aac=none_2990 on theBenchmark for (2990ds/3512Mi) % 83.86/12.07 % (3466273)Instruction limit reached! % 83.86/12.07 % (3466273)------------------------------ % 83.86/12.07 % (3466273)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 83.86/12.07 % (3466273)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 83.86/12.07 % (3466273)CaDiCaL version: 2.1.3 % 83.86/12.07 % (3466273)Termination reason: Instruction limit % 83.86/12.07 % (3466273)Termination phase: Saturation % 83.86/12.07 % (3466273)Time elapsed: 0.454 s % 83.86/12.07 % (3466273)Peak memory usage: 19 MB % 83.86/12.07 % (3466273)Instructions burned: 871 (million) % 83.86/12.07 % (3466281)dis+21_1_sil=32000:sas=cadical:random_seed=3109885870:i=3773:amm=off_2989 on theBenchmark for (2989ds/3773Mi) % 83.86/12.07 % (3466267)Instruction limit reached! % 83.86/12.07 % (3466267)------------------------------ % 83.86/12.07 % (3466267)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 83.86/12.07 % (3466267)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 83.86/12.07 % (3466267)CaDiCaL version: 2.1.3 % 83.86/12.07 % (3466267)Termination reason: Instruction limit % 83.86/12.07 % (3466267)Termination phase: Saturation % 83.86/12.07 % (3466267)Time elapsed: 0.896 s % 83.86/12.07 % (3466267)Peak memory usage: 25 MB % 83.86/12.07 % (3466267)Instructions burned: 1473 (million) % 83.86/12.07 % (3466283)ott+11_1_sil=16000:gs=on:random_seed=3315512043:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2986 on theBenchmark for (2986ds/2251Mi) % 83.86/12.07 % (3466265)Instruction limit reached! % 83.86/12.07 % (3466265)------------------------------ % 83.86/12.07 % (3466265)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 83.86/12.07 % (3466265)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 83.86/12.07 % (3466265)CaDiCaL version: 2.1.3 % 83.86/12.07 % (3466265)Termination reason: Instruction limit % 83.86/12.07 % (3466265)Termination phase: Saturation % 83.86/12.07 % (3466265)Time elapsed: 1.493 s % 83.86/12.07 % (3466265)Peak memory usage: 42 MB % 83.86/12.07 % (3466265)Instructions burned: 5134 (million) % 83.86/12.07 % (3466285)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=2710242370:fmbsr=1.6:i=67534_2980 on theBenchmark for (2980ds/67534Mi) % 83.86/12.07 % (3466285)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 83.86/12.07 % (3466285)Terminated due to inappropriate strategy. % 83.86/12.07 % (3466285)------------------------------ % 83.86/12.07 % (3466285)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 83.86/12.07 % (3466285)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 83.86/12.07 % (3466285)CaDiCaL version: 2.1.3 % 83.86/12.07 % (3466285)Termination reason: Inappropriate % 83.86/12.07 % (3466285)Time elapsed: 0.0000 s % 83.86/12.07 % (3466285)Peak memory usage: 10 MB % 83.86/12.07 % (3466285)Instructions burned: 1 (million) % 83.86/12.07 % (3466285)------------------------------ % 83.86/12.07 % (3466285)------------------------------ % 83.86/12.07 % (3466287)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=919849461:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2980 on theBenchmark for (2980ds/4591Mi) % 83.86/12.07 % (3466283)Instruction limit reached! % 83.86/12.07 % (3466283)------------------------------ % 83.86/12.07 % (3466283)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 83.86/12.07 % (3466283)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 83.86/12.07 % (3466283)CaDiCaL version: 2.1.3 % 83.86/12.07 % (3466283)Termination reason: Instruction limit % 83.86/12.07 % (3466283)Termination phase: Saturation % 83.86/12.07 % (3466283)Time elapsed: 1.224 s % 83.86/12.07 % (3466283)Peak memory usage: 21 MB % 83.86/12.07 % (3466283)Instructions burned: 2252 (million) % 83.86/12.07 % (3466289)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=2173887680:i=29340_2973 on theBenchmark for (2973ds/29340Mi) % 83.86/12.07 % (3466279)Instruction limit reached! % 83.86/12.07 % (3466279)------------------------------ % 83.86/12.07 % (3466279)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 83.86/12.07 % (3466279)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 83.86/12.07 % (3466279)CaDiCaL version: 2.1.3 % 83.86/12.07 % (3466279)Termination reason: Instruction limit % 120.54/17.21 % (3466279)Termination phase: Saturation % 120.54/17.21 % (3466279)Time elapsed: 1.872 s % 120.54/17.21 % (3466279)Peak memory usage: 35 MB % 120.54/17.21 % (3466279)Instructions burned: 3514 (million) % 120.54/17.21 % (3466291)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=1799790381:i=5211_2972 on theBenchmark for (2972ds/5211Mi) % 120.54/17.21 % (3466281)Instruction limit reached! % 120.54/17.21 % (3466281)------------------------------ % 120.54/17.21 % (3466281)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 120.54/17.21 % (3466281)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 120.54/17.21 % (3466281)CaDiCaL version: 2.1.3 % 120.54/17.21 % (3466281)Termination reason: Instruction limit % 120.54/17.21 % (3466281)Termination phase: Saturation % 120.54/17.21 % (3466281)Time elapsed: 2.050 s % 120.54/17.21 % (3466281)Peak memory usage: 33 MB % 120.54/17.21 % (3466281)Instructions burned: 3774 (million) % 120.54/17.21 % (3466293)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=4108966489:i=5497:nm=2_2969 on theBenchmark for (2969ds/5497Mi) % 120.54/17.21 % (3466293)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 120.54/17.22 % (3466293)Terminated due to inappropriate strategy. % 120.54/17.22 % (3466293)------------------------------ % 120.54/17.22 % (3466293)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 120.54/17.22 % (3466293)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 120.54/17.22 % (3466293)CaDiCaL version: 2.1.3 % 120.54/17.22 % (3466293)Termination reason: Inappropriate % 120.54/17.22 % (3466293)Time elapsed: 0.001 s % 120.54/17.22 % (3466293)Peak memory usage: 11 MB % 120.54/17.22 % (3466293)Instructions burned: 1 (million) % 120.54/17.22 % (3466293)------------------------------ % 120.54/17.22 % (3466293)------------------------------ % 120.54/17.22 % (3466295)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=3594188071:fmbsr=2:i=46332_2968 on theBenchmark for (2968ds/46332Mi) % 120.54/17.22 % (3466295)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 120.54/17.22 % (3466295)Terminated due to inappropriate strategy. % 120.54/17.22 % (3466295)------------------------------ % 120.54/17.22 % (3466295)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 120.54/17.22 % (3466295)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 120.54/17.22 % (3466295)CaDiCaL version: 2.1.3 % 120.54/17.22 % (3466295)Termination reason: Inappropriate % 120.54/17.22 % (3466295)Time elapsed: 0.001 s % 120.54/17.22 % (3466295)Peak memory usage: 11 MB % 120.54/17.22 % (3466295)Instructions burned: 1 (million) % 120.54/17.22 % (3466295)------------------------------ % 120.54/17.22 % (3466295)------------------------------ % 120.54/17.22 % (3466287)Instruction limit reached! % 120.54/17.22 % (3466287)------------------------------ % 120.54/17.22 % (3466287)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 120.54/17.22 % (3466287)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 120.54/17.22 % (3466287)CaDiCaL version: 2.1.3 % 120.54/17.22 % (3466287)Termination reason: Instruction limit % 120.54/17.22 % (3466287)Termination phase: Saturation % 120.54/17.22 % (3466287)Time elapsed: 1.194 s % 120.54/17.22 % (3466287)Peak memory usage: 40 MB % 120.54/17.22 % (3466287)Instructions burned: 4593 (million) % 120.54/17.22 % (3466297)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=713628025:i=14071_2968 on theBenchmark for (2968ds/14071Mi) % 120.54/17.22 % (3466297)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 120.54/17.22 % (3466297)Terminated due to inappropriate strategy. % 120.54/17.22 % (3466297)------------------------------ % 120.54/17.22 % (3466297)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 120.54/17.22 % (3466297)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 120.54/17.22 % (3466297)CaDiCaL version: 2.1.3 % 120.54/17.22 % (3466297)Termination reason: Inappropriate % 120.54/17.22 % (3466297)Time elapsed: 0.001 s % 120.54/17.22 % (3466297)Peak memory usage: 11 MB % 120.54/17.22 % (3466297)Instructions burned: 1 (million) % 120.54/17.22 % (3466297)------------------------------ % 120.54/17.22 % (3466297)------------------------------ % 120.54/17.22 % (3466299)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2110618914:i=22565:add=on:rawr=on_2968 on theBenchmark for (2968ds/22565Mi) % 120.54/17.22 % (3466300)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=3893892322:i=8173:av=off_2968 on theBenchmark for (2968ds/8173Mi) % 120.54/17.22 % (3466275)Instruction limit reached! % 112.34/17.30 % (3466275)------------------------------ % 112.34/17.30 % (3466275)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 112.34/17.30 % (3466275)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 112.34/17.30 % (3466275)CaDiCaL version: 2.1.3 % 112.34/17.30 % (3466275)Termination reason: Instruction limit % 112.34/17.30 % (3466275)Termination phase: Saturation % 112.34/17.30 % (3466275)Time elapsed: 3.268 s % 112.34/17.30 % (3466275)Peak memory usage: 34 MB % 112.34/17.30 % (3466275)Instructions burned: 5115 (million) % 112.34/17.30 % (3466303)dis+10_16:1_sil=16000:random_seed=3869781312:i=9155:fsr=off_2960 on theBenchmark for (2960ds/9155Mi) % 112.34/17.30 % (3466291)Instruction limit reached! % 112.34/17.30 % (3466291)------------------------------ % 112.34/17.30 % (3466291)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 112.34/17.30 % (3466291)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 112.34/17.30 % (3466291)CaDiCaL version: 2.1.3 % 112.34/17.30 % (3466291)Termination reason: Instruction limit % 112.34/17.30 % (3466291)Termination phase: Saturation % 112.34/17.30 % (3466291)Time elapsed: 2.667 s % 112.34/17.30 % (3466291)Peak memory usage: 45 MB % 112.34/17.30 % (3466291)Instructions burned: 5213 (million) % 112.34/17.30 % (3466305)ott-3_8_sil=64000:random_seed=1785111153:i=20139:bs=on_2945 on theBenchmark for (2945ds/20139Mi) % 112.34/17.30 % (3466299)Instruction limit reached! % 112.34/17.30 % (3466299)------------------------------ % 112.34/17.30 % (3466299)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 112.34/17.30 % (3466299)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 112.34/17.30 % (3466299)CaDiCaL version: 2.1.3 % 112.34/17.30 % (3466299)Termination reason: Instruction limit % 112.34/17.30 % (3466299)Termination phase: Saturation % 112.34/17.30 % (3466299)Time elapsed: 4.771 s % 112.34/17.30 % (3466299)Peak memory usage: 99 MB % 112.34/17.30 % (3466299)Instructions burned: 22570 (million) % 112.34/17.30 % (3466307)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=2916112145:fmbsr=2:i=32576_2920 on theBenchmark for (2920ds/32576Mi) % 112.34/17.30 % (3466307)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 112.34/17.30 % (3466307)Terminated due to inappropriate strategy. % 112.34/17.30 % (3466307)------------------------------ % 112.34/17.30 % (3466307)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 112.34/17.30 % (3466307)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 112.34/17.30 % (3466307)CaDiCaL version: 2.1.3 % 112.34/17.30 % (3466307)Termination reason: Inappropriate % 112.34/17.30 % (3466307)Time elapsed: 0.001 s % 112.34/17.30 % (3466307)Peak memory usage: 11 MB % 112.34/17.30 % (3466307)Instructions burned: 1 (million) % 112.34/17.30 % (3466307)------------------------------ % 112.34/17.30 % (3466307)------------------------------ % 112.34/17.30 % (3466309)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=1896681629:i=11404_2920 on theBenchmark for (2920ds/11404Mi) % 112.34/17.30 % (3466300)Instruction limit reached! % 112.34/17.30 % (3466300)------------------------------ % 112.34/17.30 % (3466300)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 112.34/17.30 % (3466300)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 112.34/17.30 % (3466300)CaDiCaL version: 2.1.3 % 112.34/17.30 % (3466300)Termination reason: Instruction limit % 112.34/17.30 % (3466300)Termination phase: Saturation % 112.34/17.30 % (3466300)Time elapsed: 5.105 s % 112.34/17.30 % (3466300)Peak memory usage: 52 MB % 112.34/17.30 % (3466300)Instructions burned: 8175 (million) % 112.34/17.30 % (3466311)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=3272774238:i=14134_2917 on theBenchmark for (2917ds/14134Mi) % 112.34/17.30 % (3466303)Instruction limit reached! % 112.34/17.30 % (3466303)------------------------------ % 112.34/17.30 % (3466303)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 112.34/17.30 % (3466303)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 112.34/17.30 % (3466303)CaDiCaL version: 2.1.3 % 112.34/17.30 % (3466303)Termination reason: Instruction limit % 112.34/17.30 % (3466303)Termination phase: Saturation % 112.34/17.30 % (3466303)Time elapsed: 4.658 s % 112.34/17.30 % (3466303)Peak memory usage: 52 MB % 112.34/17.30 % (3466303)Instructions burned: 9156 (million) % 112.34/17.30 % (3466313)dis+33_16_sil=32000:sac=on:random_seed=4291801029:i=15851:nm=0_2913 on theBenchmark for (2913ds/15851Mi) % 112.34/17.30 % (3466309)Instruction limit reached! % 112.34/17.30 % (3466309)------------------------------ % 112.34/17.30 % (3466309)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 130.46/18.61 % (3466309)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 130.46/18.61 % (3466309)CaDiCaL version: 2.1.3 % 130.46/18.61 % (3466309)Termination reason: Instruction limit % 130.46/18.61 % (3466309)Termination phase: Saturation % 130.46/18.61 % (3466309)Time elapsed: 3.891 s % 130.46/18.61 % (3466309)Peak memory usage: 71 MB % 130.46/18.61 % (3466309)Instructions burned: 11405 (million) % 130.46/18.61 % (3466316)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=2506675391:avsq=on:i=17627:add=on:amm=off_2881 on theBenchmark for (2881ds/17627Mi) % 130.46/18.61 % (3466289)Instruction limit reached! % 130.46/18.61 % (3466289)------------------------------ % 130.46/18.61 % (3466289)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 130.46/18.61 % (3466289)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 130.46/18.61 % (3466289)CaDiCaL version: 2.1.3 % 130.46/18.61 % (3466289)Termination reason: Instruction limit % 130.46/18.61 % (3466289)Termination phase: Saturation % 130.46/18.61 % (3466289)Time elapsed: 13.742 s % 130.46/18.61 % (3466289)Peak memory usage: 149 MB % 130.46/18.61 % (3466289)Instructions burned: 29340 (million) % 130.46/18.61 % (3466318)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=2524661160:s2a=on:i=53295_2836 on theBenchmark for (2836ds/53295Mi) % 130.46/18.61 % (3466313)Instruction limit reached! % 130.46/18.61 % (3466313)------------------------------ % 130.46/18.61 % (3466313)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 130.46/18.61 % (3466313)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 130.46/18.61 % (3466313)CaDiCaL version: 2.1.3 % 130.46/18.61 % (3466313)Termination reason: Instruction limit % 130.46/18.61 % (3466313)Termination phase: Saturation % 130.46/18.61 % (3466313)Time elapsed: 7.727 s % 130.46/18.61 % (3466313)Peak memory usage: 162 MB % 130.46/18.61 % (3466313)Instructions burned: 15852 (million) % 130.46/18.61 % (3466320)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=728497400:i=26857:ins=20_2835 on theBenchmark for (2835ds/26857Mi) % 130.46/18.61 % (3466320)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 130.46/18.61 % (3466320)Terminated due to inappropriate strategy. % 130.46/18.61 % (3466320)------------------------------ % 130.46/18.61 % (3466320)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 130.46/18.61 % (3466320)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 130.46/18.61 % (3466320)CaDiCaL version: 2.1.3 % 130.46/18.61 % (3466320)Termination reason: Inappropriate % 130.46/18.61 % (3466320)Time elapsed: 0.001 s % 130.46/18.61 % (3466320)Peak memory usage: 10 MB % 130.46/18.61 % (3466320)Instructions burned: 1 (million) % 130.46/18.61 % (3466320)------------------------------ % 130.46/18.61 % (3466320)------------------------------ % 130.46/18.61 % (3466322)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=2873333402:i=28120:bs=on:fsr=off_2835 on theBenchmark for (2835ds/28120Mi) % 130.46/18.61 % (3466316)Instruction limit reached! % 130.46/18.61 % (3466316)------------------------------ % 130.46/18.61 % (3466316)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 130.46/18.61 % (3466316)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 130.46/18.61 % (3466316)CaDiCaL version: 2.1.3 % 130.46/18.61 % (3466316)Termination reason: Instruction limit % 130.46/18.61 % (3466316)Termination phase: Saturation % 130.46/18.61 % (3466316)Time elapsed: 5.094 s % 130.46/18.61 % (3466316)Peak memory usage: 104 MB % 130.46/18.61 % (3466316)Instructions burned: 17629 (million) % 130.46/18.61 % (3466324)fmb+10_1_sil=256000:fmbss=7:random_seed=3186579226:fmbsr=1.6:i=182295_2830 on theBenchmark for (2830ds/182295Mi) % 130.46/18.61 % (3466324)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 130.46/18.61 % (3466324)Terminated due to inappropriate strategy. % 130.46/18.61 % (3466324)------------------------------ % 130.46/18.61 % (3466324)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 130.46/18.61 % (3466324)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 130.46/18.61 % (3466324)CaDiCaL version: 2.1.3 % 130.46/18.61 % (3466324)Termination reason: Inappropriate % 130.46/18.61 % (3466324)Time elapsed: 0.0000 s % 130.46/18.61 % (3466324)Peak memory usage: 10 MB % 130.46/18.61 % (3466324)Instructions burned: 1 (million) % 130.46/18.61 % (3466324)------------------------------ % 130.46/18.61 % (3466324)------------------------------ % 130.46/18.61 % (3466326)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=64870896:i=44625:gsp=on_2830 on theBenchmark for (2830ds/44625Mi) % 143.23/20.48 % (3466326)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 143.23/20.48 % (3466326)Terminated due to inappropriate strategy. % 143.23/20.48 % (3466326)------------------------------ % 143.23/20.48 % (3466326)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 143.23/20.48 % (3466326)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 143.23/20.48 % (3466326)CaDiCaL version: 2.1.3 % 143.23/20.48 % (3466326)Termination reason: Inappropriate % 143.23/20.48 % (3466326)Time elapsed: 0.001 s % 143.23/20.48 % (3466326)Peak memory usage: 11 MB % 143.23/20.48 % (3466326)Instructions burned: 1 (million) % 143.23/20.48 % (3466326)------------------------------ % 143.23/20.48 % (3466326)------------------------------ % 143.23/20.48 % (3466328)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=1786992781:i=160505_2830 on theBenchmark for (2830ds/160505Mi) % 143.23/20.48 % (3466328)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 143.23/20.48 % (3466328)Terminated due to inappropriate strategy. % 143.23/20.48 % (3466328)------------------------------ % 143.23/20.48 % (3466328)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 143.23/20.48 % (3466328)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 143.23/20.48 % (3466328)CaDiCaL version: 2.1.3 % 143.23/20.48 % (3466328)Termination reason: Inappropriate % 143.23/20.48 % (3466328)Time elapsed: 0.001 s % 143.23/20.48 % (3466328)Peak memory usage: 11 MB % 143.23/20.48 % (3466328)Instructions burned: 1 (million) % 143.23/20.48 % (3466328)------------------------------ % 143.23/20.48 % (3466328)------------------------------ % 143.23/20.48 % (3466330)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=2248181731:fmbsr=1.3:i=225729_2829 on theBenchmark for (2829ds/225729Mi) % 143.23/20.48 % (3466330)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 143.23/20.48 % (3466330)Terminated due to inappropriate strategy. % 143.23/20.48 % (3466330)------------------------------ % 143.23/20.48 % (3466330)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 143.23/20.48 % (3466330)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 143.23/20.48 % (3466330)CaDiCaL version: 2.1.3 % 143.23/20.48 % (3466330)Termination reason: Inappropriate % 143.23/20.48 % (3466330)Time elapsed: 0.001 s % 143.23/20.48 % (3466330)Peak memory usage: 11 MB % 143.23/20.48 % (3466330)Instructions burned: 1 (million) % 143.23/20.48 % (3466330)------------------------------ % 143.23/20.48 % (3466330)------------------------------ % 143.23/20.48 % (3466332)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=3285153878:fmbsr=2:i=185024:ins=7_2829 on theBenchmark for (2829ds/185024Mi) % 143.23/20.48 % (3466332)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 143.23/20.48 % (3466332)Terminated due to inappropriate strategy. % 143.23/20.48 % (3466332)------------------------------ % 143.23/20.48 % (3466332)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 143.23/20.48 % (3466332)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 143.23/20.48 % (3466332)CaDiCaL version: 2.1.3 % 143.23/20.48 % (3466332)Termination reason: Inappropriate % 143.23/20.48 % (3466332)Time elapsed: 0.001 s % 143.23/20.48 % (3466332)Peak memory usage: 11 MB % 143.23/20.48 % (3466332)Instructions burned: 1 (million) % 143.23/20.48 % (3466332)------------------------------ % 143.23/20.48 % (3466332)------------------------------ % 143.23/20.48 % (3466311)Instruction limit reached! % 143.23/20.48 % (3466311)------------------------------ % 143.23/20.48 % (3466311)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 143.23/20.48 % (3466311)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 143.23/20.48 % (3466311)CaDiCaL version: 2.1.3 % 143.23/20.48 % (3466311)Termination reason: Instruction limit % 143.23/20.48 % (3466311)Termination phase: Saturation % 143.23/20.48 % (3466311)Time elapsed: 8.778 s % 143.23/20.48 % (3466311)Peak memory usage: 75 MB % 143.23/20.48 % (3466311)Instructions burned: 14134 (million) % 143.23/20.48 % (3466334)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=929447989:rtra=on_2829 on theBenchmark for (2829ds/0Mi) % 143.23/20.48 % (3466334)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 143.23/20.48 % (3466334)Terminated due to inappropriate strategy. % 143.23/20.48 % (3466334)------------------------------ % 143.23/20.48 % (3466334)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 143.23/20.48 % (3466334)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 168.10/24.01 % (3466334)CaDiCaL version: 2.1.3 % 168.10/24.01 % (3466334)Termination reason: Inappropriate % 168.10/24.01 % (3466334)Time elapsed: 0.001 s % 168.10/24.01 % (3466334)Peak memory usage: 10 MB % 168.10/24.01 % (3466334)Instructions burned: 2 (million) % 168.10/24.01 % (3466334)------------------------------ % 168.10/24.01 % (3466334)------------------------------ % 168.10/24.01 % (3466336)% WARNING: option uhcvi not known. % 168.10/24.01 % (3466336)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2900668870:i=271062:add=off:rtra=on:rawr=on_2829 on theBenchmark for (2829ds/271062Mi) % 168.10/24.01 % (3466337)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=362832299:i=176048:add=on:rtra=on:rawr=on_2829 on theBenchmark for (2829ds/176048Mi) % 168.10/24.01 % (3466305)Instruction limit reached! % 168.10/24.01 % (3466305)------------------------------ % 168.10/24.01 % (3466305)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 168.10/24.01 % (3466305)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 168.10/24.01 % (3466305)CaDiCaL version: 2.1.3 % 168.10/24.01 % (3466305)Termination reason: Instruction limit % 168.10/24.01 % (3466305)Termination phase: Saturation % 168.10/24.01 % (3466305)Time elapsed: 12.106 s % 168.10/24.01 % (3466305)Peak memory usage: 70 MB % 168.10/24.01 % (3466305)Instructions burned: 20139 (million) % 168.10/24.01 % (3466340)dis+10_1_sil=32000:si=on:sp=arity:random_seed=2450576505:i=206:fgj=on:rtra=on_2823 on theBenchmark for (2823ds/206Mi) % 168.10/24.01 % (3466340)Instruction limit reached! % 168.10/24.01 % (3466340)------------------------------ % 168.10/24.01 % (3466340)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 168.10/24.01 % (3466340)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 168.10/24.01 % (3466340)CaDiCaL version: 2.1.3 % 168.10/24.01 % (3466340)Termination reason: Instruction limit % 168.10/24.01 % (3466340)Termination phase: Saturation % 168.10/24.01 % (3466340)Time elapsed: 0.130 s % 168.10/24.01 % (3466340)Peak memory usage: 13 MB % 168.10/24.01 % (3466340)Instructions burned: 206 (million) % 168.10/24.01 % (3466342)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=2178682276:i=232:rtra=on_2822 on theBenchmark for (2822ds/232Mi) % 168.10/24.01 % (3466342)Instruction limit reached! % 168.10/24.01 % (3466342)------------------------------ % 168.10/24.01 % (3466342)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 168.10/24.01 % (3466342)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 168.10/24.01 % (3466342)CaDiCaL version: 2.1.3 % 168.10/24.01 % (3466342)Termination reason: Instruction limit % 168.10/24.01 % (3466342)Termination phase: Saturation % 168.10/24.01 % (3466342)Time elapsed: 0.149 s % 168.10/24.01 % (3466342)Peak memory usage: 13 MB % 168.10/24.01 % (3466342)Instructions burned: 233 (million) % 168.10/24.01 % (3466344)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=1020412170:i=262:rtra=on_2820 on theBenchmark for (2820ds/262Mi) % 168.10/24.01 % (3466344)Instruction limit reached! % 168.10/24.01 % (3466344)------------------------------ % 168.10/24.01 % (3466344)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 168.10/24.01 % (3466344)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 168.10/24.01 % (3466344)CaDiCaL version: 2.1.3 % 168.10/24.01 % (3466344)Termination reason: Instruction limit % 168.10/24.01 % (3466344)Termination phase: Saturation % 168.10/24.01 % (3466344)Time elapsed: 0.165 s % 168.10/24.01 % (3466344)Peak memory usage: 14 MB % 168.10/24.01 % (3466344)Instructions burned: 263 (million) % 168.10/24.01 % (3466346)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=4080202738:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2818 on theBenchmark for (2818ds/318Mi) % 168.10/24.01 % (3466346)Instruction limit reached! % 168.10/24.01 % (3466346)------------------------------ % 168.10/24.01 % (3466346)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 168.10/24.01 % (3466346)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 168.10/24.01 % (3466346)CaDiCaL version: 2.1.3 % 168.10/24.01 % (3466346)Termination reason: Instruction limit % 168.10/24.01 % (3466346)Termination phase: Saturation % 168.10/24.01 % (3466346)Time elapsed: 0.219 s % 168.10/24.01 % (3466346)Peak memory usage: 15 MB % 168.10/24.01 % (3466346)Instructions burned: 319 (million) % 168.10/24.01 % (3466348)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=1667857144:i=1428:nm=2:rtra=on_2816 on theBenchmark for (2816ds/1428Mi) % 205.58/30.08 % (3466348)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 205.58/30.08 % (3466348)Terminated due to inappropriate strategy. % 205.58/30.08 % (3466348)------------------------------ % 205.58/30.08 % (3466348)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 205.58/30.08 % (3466348)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 205.58/30.08 % (3466348)CaDiCaL version: 2.1.3 % 205.58/30.08 % (3466348)Termination reason: Inappropriate % 205.58/30.08 % (3466348)Time elapsed: 0.001 s % 205.58/30.08 % (3466348)Peak memory usage: 10 MB % 205.58/30.08 % (3466348)Instructions burned: 1 (million) % 205.58/30.08 % (3466348)------------------------------ % 205.58/30.08 % (3466348)------------------------------ % 205.58/30.08 % (3466350)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=3063444283:i=262:bd=preordered:rtra=on:fsd=on_2816 on theBenchmark for (2816ds/262Mi) % 205.58/30.08 % (3466350)Instruction limit reached! % 205.58/30.08 % (3466350)------------------------------ % 205.58/30.08 % (3466350)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 205.58/30.08 % (3466350)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 205.58/30.08 % (3466350)CaDiCaL version: 2.1.3 % 205.58/30.08 % (3466350)Termination reason: Instruction limit % 205.58/30.08 % (3466350)Termination phase: Saturation % 205.58/30.08 % (3466350)Time elapsed: 0.188 s % 205.58/30.08 % (3466350)Peak memory usage: 14 MB % 205.58/30.08 % (3466350)Instructions burned: 262 (million) % 205.58/30.08 % (3466352)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=2802773388:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2814 on theBenchmark for (2814ds/1368Mi) % 205.58/30.08 % (3466352)Instruction limit reached! % 205.58/30.08 % (3466352)------------------------------ % 205.58/30.08 % (3466352)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 205.58/30.08 % (3466352)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 205.58/30.08 % (3466352)CaDiCaL version: 2.1.3 % 205.58/30.08 % (3466352)Termination reason: Instruction limit % 205.58/30.08 % (3466352)Termination phase: Saturation % 205.58/30.08 % (3466352)Time elapsed: 0.777 s % 205.58/30.08 % (3466352)Peak memory usage: 21 MB % 205.58/30.08 % (3466352)Instructions burned: 1369 (million) % 205.58/30.08 % (3466354)ott-21_1_sil=16000:si=on:fs=off:random_seed=2841244037:i=360:av=off:fsr=off:rtra=on_2806 on theBenchmark for (2806ds/360Mi) % 205.58/30.08 % (3466354)Instruction limit reached! % 205.58/30.08 % (3466354)------------------------------ % 205.58/30.08 % (3466354)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 205.58/30.08 % (3466354)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 205.58/30.08 % (3466354)CaDiCaL version: 2.1.3 % 205.58/30.08 % (3466354)Termination reason: Instruction limit % 205.58/30.08 % (3466354)Termination phase: Saturation % 205.58/30.08 % (3466354)Time elapsed: 0.163 s % 205.58/30.08 % (3466354)Peak memory usage: 13 MB % 205.58/30.08 % (3466354)Instructions burned: 361 (million) % 205.58/30.08 % (3466356)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1980595443:i=954:bd=all:rtra=on_2804 on theBenchmark for (2804ds/954Mi) % 205.58/30.08 % (3466356)Instruction limit reached! % 205.58/30.08 % (3466356)------------------------------ % 205.58/30.08 % (3466356)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 205.58/30.08 % (3466356)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 205.58/30.08 % (3466356)CaDiCaL version: 2.1.3 % 205.58/30.08 % (3466356)Termination reason: Instruction limit % 205.58/30.08 % (3466356)Termination phase: Saturation % 205.58/30.08 % (3466356)Time elapsed: 0.635 s % 205.58/30.08 % (3466356)Peak memory usage: 15 MB % 205.58/30.08 % (3466356)Instructions burned: 955 (million) % 205.58/30.08 % (3466358)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=3782106532:fmbsr=1.3:i=1730:ins=25:rtra=on_2797 on theBenchmark for (2797ds/1730Mi) % 205.58/30.08 % (3466358)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 205.58/30.08 % (3466358)Terminated due to inappropriate strategy. % 205.58/30.08 % (3466358)------------------------------ % 205.58/30.08 % (3466358)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 205.58/30.08 % (3466358)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 205.58/30.08 % (3466358)CaDiCaL version: 2.1.3 % 205.58/30.08 % (3466358)Termination reason: Inappropriate % 270.32/38.31 % (3466358)Time elapsed: 0.001 s % 270.32/38.31 % (3466358)Peak memory usage: 10 MB % 270.32/38.31 % (3466358)Instructions burned: 1 (million) % 270.32/38.31 % (3466358)------------------------------ % 270.32/38.31 % (3466358)------------------------------ % 270.32/38.31 % (3466360)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=3941809951:i=2358:rtra=on_2797 on theBenchmark for (2797ds/2358Mi) % 270.32/38.31 % (3466360)Instruction limit reached! % 270.32/38.31 % (3466360)------------------------------ % 270.32/38.31 % (3466360)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 270.32/38.31 % (3466360)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 270.32/38.31 % (3466360)CaDiCaL version: 2.1.3 % 270.32/38.31 % (3466360)Termination reason: Instruction limit % 270.32/38.31 % (3466360)Termination phase: Saturation % 270.32/38.31 % (3466360)Time elapsed: 1.574 s % 270.32/38.31 % (3466360)Peak memory usage: 24 MB % 270.32/38.31 % (3466360)Instructions burned: 2358 (million) % 270.32/38.31 % (3466362)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=555646729:i=1778:ins=1:rtra=on_2781 on theBenchmark for (2781ds/1778Mi) % 270.32/38.31 % (3466362)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 270.32/38.31 % (3466362)Terminated due to inappropriate strategy. % 270.32/38.31 % (3466362)------------------------------ % 270.32/38.31 % (3466362)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 270.32/38.31 % (3466362)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 270.32/38.31 % (3466362)CaDiCaL version: 2.1.3 % 270.32/38.31 % (3466362)Termination reason: Inappropriate % 270.32/38.31 % (3466362)Time elapsed: 0.001 s % 270.32/38.31 % (3466362)Peak memory usage: 10 MB % 270.32/38.31 % (3466362)Instructions burned: 1 (million) % 270.32/38.31 % (3466362)------------------------------ % 270.32/38.31 % (3466362)------------------------------ % 270.32/38.31 % (3466364)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=3359506481:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2781 on theBenchmark for (2781ds/1384Mi) % 270.32/38.31 % (3466364)Instruction limit reached! % 270.32/38.31 % (3466364)------------------------------ % 270.32/38.31 % (3466364)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 270.32/38.31 % (3466364)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 270.32/38.31 % (3466364)CaDiCaL version: 2.1.3 % 270.32/38.31 % (3466364)Termination reason: Instruction limit % 270.32/38.31 % (3466364)Termination phase: Saturation % 270.32/38.31 % (3466364)Time elapsed: 0.815 s % 270.32/38.31 % (3466364)Peak memory usage: 22 MB % 270.32/38.31 % (3466364)Instructions burned: 1386 (million) % 270.32/38.31 % (3466366)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=2178092553:i=1758:kws=inv_precedence:fsr=off:rtra=on_2772 on theBenchmark for (2772ds/1758Mi) % 270.32/38.31 % (3466366)Instruction limit reached! % 270.32/38.31 % (3466366)------------------------------ % 270.32/38.31 % (3466366)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 270.32/38.31 % (3466366)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 270.32/38.31 % (3466366)CaDiCaL version: 2.1.3 % 270.32/38.31 % (3466366)Termination reason: Instruction limit % 270.32/38.31 % (3466366)Termination phase: Saturation % 270.32/38.31 % (3466366)Time elapsed: 1.007 s % 270.32/38.31 % (3466366)Peak memory usage: 25 MB % 270.32/38.31 % (3466366)Instructions burned: 1760 (million) % 270.32/38.31 % (3466368)fmb+10_1_sil=64000:si=on:random_seed=3471535329:i=44122:nm=2:rtra=on:gsp=on_2762 on theBenchmark for (2762ds/44122Mi) % 270.32/38.31 % (3466368)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 270.32/38.31 % (3466368)Terminated due to inappropriate strategy. % 270.32/38.31 % (3466368)------------------------------ % 270.32/38.31 % (3466368)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 270.32/38.31 % (3466368)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 270.32/38.31 % (3466368)CaDiCaL version: 2.1.3 % 270.32/38.31 % (3466368)Termination reason: Inappropriate % 270.32/38.31 % (3466368)Time elapsed: 0.001 s % 270.32/38.31 % (3466368)Peak memory usage: 10 MB % 270.32/38.31 % (3466368)Instructions burned: 1 (million) % 270.32/38.31 % (3466368)------------------------------ % 270.32/38.31 % (3466368)------------------------------ % 270.32/38.31 % (3466370)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=3571329312:i=19030:nm=5:rtra=on_2762 on theBenTerminated % 300.10/42.54 % Vampire exiting %------------------------------------------------------------------------------