%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWC434_1 : TPTP v9.3.1. Released v9.0.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/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:06:00 PM UTC 2026 % Result : Timeout 300.69s 42.63s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWC434_1 : TPTP v9.3.1. Released v9.0.0. % 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.10/0.20 % Computer : n006.cluster.edu % 0.10/0.20 % Model : x86_64 x86_64 % 0.10/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.20 % Memory : 8046.5625MB % 0.10/0.20 % OS : Linux 6.8.0-71-generic % 0.10/0.20 % CPULimit : 300 % 0.10/0.20 % WCLimit : 300 % 0.10/0.20 % DateTime : Mon Sep 28 09:37:10 UTC 2026 % 0.10/0.20 % CPUTime : % 0.10/0.20 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.10/0.23 Running first-order model finding % 0.10/0.23 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.60/0.85 % (3841720)Will run a generic schedule for satisfiability detection. % 3.60/0.85 % (3841734)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1930129357:i=131_2999 on theBenchmark for (2999ds/131Mi) % 3.60/0.85 % (3841729)% WARNING: option uhcvi not known. % 3.60/0.85 % (3841732)dis+10_1_sil=32000:sp=arity:random_seed=2318376643:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 3.60/0.85 % (3841728)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=558824837_2999 on theBenchmark for (2999ds/0Mi) % 3.60/0.85 % (3841730)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3846735621:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 3.60/0.85 % (3841733)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1441216421:i=116_2999 on theBenchmark for (2999ds/116Mi) % 3.60/0.85 % (3841729)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2404515462:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 3.60/0.85 % (3841735)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1127693936:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 3.60/0.85 % (3841728)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.60/0.85 % (3841728)Terminated due to inappropriate strategy. % 3.60/0.85 % (3841728)------------------------------ % 3.60/0.85 % (3841728)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.60/0.85 % (3841728)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.60/0.85 % (3841728)CaDiCaL version: 2.1.3 % 3.60/0.85 % (3841728)Termination reason: Inappropriate % 3.60/0.85 % (3841728)Time elapsed: 0.001 s % 3.60/0.85 % (3841728)Peak memory usage: 10 MB % 3.60/0.85 % (3841728)Instructions burned: 1 (million) % 3.60/0.85 % (3841728)------------------------------ % 3.60/0.85 % (3841728)------------------------------ % 3.60/0.85 % (3841744)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3124494796:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 3.60/0.85 % (3841744)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.60/0.85 % (3841744)Terminated due to inappropriate strategy. % 3.60/0.85 % (3841744)------------------------------ % 3.60/0.85 % (3841744)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.60/0.85 % (3841744)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.60/0.85 % (3841744)CaDiCaL version: 2.1.3 % 3.60/0.85 % (3841744)Termination reason: Inappropriate % 3.60/0.85 % (3841744)Time elapsed: 0.001 s % 3.60/0.85 % (3841744)Peak memory usage: 11 MB % 3.60/0.85 % (3841744)Instructions burned: 1 (million) % 3.60/0.85 % (3841744)------------------------------ % 3.60/0.85 % (3841744)------------------------------ % 3.60/0.85 % (3841734)Instruction limit reached! % 3.60/0.85 % (3841734)------------------------------ % 3.60/0.85 % (3841734)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.60/0.85 % (3841734)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.60/0.85 % (3841734)CaDiCaL version: 2.1.3 % 3.60/0.85 % (3841734)Termination reason: Instruction limit % 3.60/0.85 % (3841734)Termination phase: Saturation % 3.60/0.85 % (3841734)Time elapsed: 0.043 s % 3.60/0.85 % (3841734)Peak memory usage: 13 MB % 3.60/0.85 % (3841734)Instructions burned: 132 (million) % 3.60/0.85 % (3841754)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1324038351:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 3.60/0.85 % (3841759)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=189103411:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi) % 3.60/0.85 % (3841732)Instruction limit reached! % 3.60/0.85 % (3841732)------------------------------ % 3.60/0.85 % (3841732)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.60/0.85 % (3841732)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.60/0.85 % (3841732)CaDiCaL version: 2.1.3 % 3.60/0.85 % (3841732)Termination reason: Instruction limit % 3.60/0.85 % (3841732)Termination phase: Saturation % 3.60/0.85 % (3841732)Time elapsed: 0.064 s % 3.60/0.85 % (3841732)Peak memory usage: 12 MB % 3.60/0.85 % (3841732)Instructions burned: 104 (million) % 3.60/0.85 % (3841733)Instruction limit reached! % 3.60/0.85 % (3841733)------------------------------ % 3.60/0.85 % (3841733)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.63/1.10 % (3841733)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.63/1.10 % (3841733)CaDiCaL version: 2.1.3 % 5.63/1.10 % (3841733)Termination reason: Instruction limit % 5.63/1.10 % (3841733)Termination phase: Saturation % 5.63/1.10 % (3841733)Time elapsed: 0.072 s % 5.63/1.10 % (3841733)Peak memory usage: 12 MB % 5.63/1.10 % (3841733)Instructions burned: 117 (million) % 5.63/1.10 % (3841765)ott-21_1_sil=16000:fs=off:random_seed=3456030038:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi) % 5.63/1.10 % (3841769)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1173947198:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 5.63/1.10 % (3841735)Instruction limit reached! % 5.63/1.10 % (3841735)------------------------------ % 5.63/1.10 % (3841735)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.63/1.10 % (3841735)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.63/1.10 % (3841735)CaDiCaL version: 2.1.3 % 5.63/1.10 % (3841735)Termination reason: Instruction limit % 5.63/1.10 % (3841735)Termination phase: Saturation % 5.63/1.10 % (3841735)Time elapsed: 0.103 s % 5.63/1.10 % (3841735)Peak memory usage: 13 MB % 5.63/1.10 % (3841735)Instructions burned: 159 (million) % 5.63/1.10 % (3841788)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2639500172:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 5.63/1.10 % (3841788)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 5.63/1.10 % (3841788)Terminated due to inappropriate strategy. % 5.63/1.10 % (3841788)------------------------------ % 5.63/1.10 % (3841788)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.63/1.10 % (3841788)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.63/1.10 % (3841788)CaDiCaL version: 2.1.3 % 5.63/1.10 % (3841788)Termination reason: Inappropriate % 5.63/1.10 % (3841788)Time elapsed: 0.001 s % 5.63/1.10 % (3841788)Peak memory usage: 10 MB % 5.63/1.10 % (3841788)Instructions burned: 1 (million) % 5.63/1.10 % (3841754)Instruction limit reached! % 5.63/1.10 % (3841754)------------------------------ % 5.63/1.10 % (3841754)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.63/1.10 % (3841754)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.63/1.10 % (3841754)CaDiCaL version: 2.1.3 % 5.63/1.10 % (3841754)Termination reason: Instruction limit % 5.63/1.10 % (3841754)Termination phase: Saturation % 5.63/1.10 % (3841754)Time elapsed: 0.081 s % 5.63/1.10 % (3841754)Peak memory usage: 13 MB % 5.63/1.10 % (3841754)Instructions burned: 132 (million) % 5.63/1.10 % (3841788)------------------------------ % 5.63/1.10 % (3841788)------------------------------ % 5.63/1.10 % (3841802)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2974625808:i=1179_2998 on theBenchmark for (2998ds/1179Mi) % 5.63/1.10 % (3841803)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3884464068:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi) % 5.63/1.10 % (3841803)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 5.63/1.10 % (3841803)Terminated due to inappropriate strategy. % 5.63/1.10 % (3841803)------------------------------ % 5.63/1.10 % (3841803)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.63/1.10 % (3841803)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.63/1.10 % (3841803)CaDiCaL version: 2.1.3 % 5.63/1.10 % (3841803)Termination reason: Inappropriate % 5.63/1.10 % (3841803)Time elapsed: 0.001 s % 5.63/1.10 % (3841803)Peak memory usage: 10 MB % 5.63/1.10 % (3841803)Instructions burned: 1 (million) % 5.63/1.10 % (3841803)------------------------------ % 5.63/1.10 % (3841803)------------------------------ % 5.63/1.10 % (3841813)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=241983133: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) % 5.63/1.10 % (3841765)Instruction limit reached! % 5.63/1.10 % (3841765)------------------------------ % 5.63/1.10 % (3841765)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.63/1.10 % (3841765)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.63/1.10 % (3841765)CaDiCaL version: 2.1.3 % 5.63/1.10 % (3841765)Termination reason: Instruction limit % 5.63/1.10 % (3841765)Termination phase: Saturation % 17.89/3.01 % (3841765)Time elapsed: 0.082 s % 17.89/3.01 % (3841765)Peak memory usage: 12 MB % 17.89/3.01 % (3841765)Instructions burned: 180 (million) % 17.89/3.01 % (3841819)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3310830466:i=879:kws=inv_precedence:fsr=off_2998 on theBenchmark for (2998ds/879Mi) % 17.89/3.01 % (3841759)Instruction limit reached! % 17.89/3.01 % (3841759)------------------------------ % 17.89/3.01 % (3841759)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 17.89/3.01 % (3841759)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.89/3.01 % (3841759)CaDiCaL version: 2.1.3 % 17.89/3.01 % (3841759)Termination reason: Instruction limit % 17.89/3.01 % (3841759)Termination phase: Saturation % 17.89/3.01 % (3841759)Time elapsed: 0.195 s % 17.89/3.01 % (3841759)Peak memory usage: 17 MB % 17.89/3.01 % (3841759)Instructions burned: 687 (million) % 17.89/3.01 % (3841821)fmb+10_1_sil=64000:random_seed=2209976394:i=22061:nm=2:gsp=on_2997 on theBenchmark for (2997ds/22061Mi) % 17.89/3.01 % (3841821)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 17.89/3.01 % (3841821)Terminated due to inappropriate strategy. % 17.89/3.01 % (3841821)------------------------------ % 17.89/3.01 % (3841821)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 17.89/3.01 % (3841821)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.89/3.01 % (3841821)CaDiCaL version: 2.1.3 % 17.89/3.01 % (3841821)Termination reason: Inappropriate % 17.89/3.01 % (3841821)Time elapsed: 0.0000 s % 17.89/3.01 % (3841821)Peak memory usage: 10 MB % 17.89/3.01 % (3841821)Instructions burned: 1 (million) % 17.89/3.01 % (3841821)------------------------------ % 17.89/3.01 % (3841821)------------------------------ % 17.89/3.01 % (3841823)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=4137106353:i=9515:nm=5_2997 on theBenchmark for (2997ds/9515Mi) % 17.89/3.01 % (3841823)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 17.89/3.01 % (3841823)Terminated due to inappropriate strategy. % 17.89/3.01 % (3841823)------------------------------ % 17.89/3.01 % (3841823)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 17.89/3.01 % (3841823)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.89/3.01 % (3841823)CaDiCaL version: 2.1.3 % 17.89/3.01 % (3841823)Termination reason: Inappropriate % 17.89/3.01 % (3841823)Time elapsed: 0.0000 s % 17.89/3.01 % (3841823)Peak memory usage: 10 MB % 17.89/3.01 % (3841823)Instructions burned: 1 (million) % 17.89/3.01 % (3841823)------------------------------ % 17.89/3.01 % (3841823)------------------------------ % 17.89/3.01 % (3841825)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1288818543:fmbsr=1.7:i=920_2997 on theBenchmark for (2997ds/920Mi) % 17.89/3.01 % (3841825)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 17.89/3.01 % (3841825)Terminated due to inappropriate strategy. % 17.89/3.01 % (3841825)------------------------------ % 17.89/3.01 % (3841825)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 17.89/3.01 % (3841825)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.89/3.01 % (3841825)CaDiCaL version: 2.1.3 % 17.89/3.01 % (3841825)Termination reason: Inappropriate % 17.89/3.01 % (3841825)Time elapsed: 0.0000 s % 17.89/3.01 % (3841825)Peak memory usage: 11 MB % 17.89/3.01 % (3841825)Instructions burned: 1 (million) % 17.89/3.01 % (3841825)------------------------------ % 17.89/3.01 % (3841825)------------------------------ % 17.89/3.01 % (3841827)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1787582008:i=5131_2996 on theBenchmark for (2996ds/5131Mi) % 17.89/3.01 % (3841769)Instruction limit reached! % 17.89/3.01 % (3841769)------------------------------ % 17.89/3.01 % (3841769)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 17.89/3.01 % (3841769)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.89/3.01 % (3841769)CaDiCaL version: 2.1.3 % 17.89/3.01 % (3841769)Termination reason: Instruction limit % 17.89/3.01 % (3841769)Termination phase: Saturation % 17.89/3.01 % (3841769)Time elapsed: 0.300 s % 17.89/3.01 % (3841769)Peak memory usage: 15 MB % 17.89/3.01 % (3841769)Instructions burned: 478 (million) % 17.89/3.01 % (3841829)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1964599261:i=1472:ins=7:fdi=8:gsp=on_2995 on theBenchmark for (2995ds/1472Mi) % 17.89/3.01 % (3841813)Instruction limit reached! % 17.89/3.01 % (3841813)------------------------------ % 28.09/4.21 % (3841813)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 28.09/4.21 % (3841813)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.09/4.21 % (3841813)CaDiCaL version: 2.1.3 % 28.09/4.21 % (3841813)Termination reason: Instruction limit % 28.09/4.21 % (3841813)Termination phase: Saturation % 28.09/4.21 % (3841813)Time elapsed: 0.414 s % 28.09/4.21 % (3841813)Peak memory usage: 19 MB % 28.09/4.21 % (3841813)Instructions burned: 693 (million) % 28.09/4.21 % (3841831)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=713835408:i=6324_2993 on theBenchmark for (2993ds/6324Mi) % 28.09/4.21 % (3841831)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 28.09/4.21 % (3841831)Terminated due to inappropriate strategy. % 28.09/4.21 % (3841831)------------------------------ % 28.09/4.21 % (3841831)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 28.09/4.21 % (3841831)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.09/4.21 % (3841831)CaDiCaL version: 2.1.3 % 28.09/4.21 % (3841831)Termination reason: Inappropriate % 28.09/4.21 % (3841831)Time elapsed: 0.001 s % 28.09/4.21 % (3841831)Peak memory usage: 10 MB % 28.09/4.21 % (3841831)Instructions burned: 1 (million) % 28.09/4.21 % (3841831)------------------------------ % 28.09/4.21 % (3841831)------------------------------ % 28.09/4.21 % (3841833)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1236933610:fmbsr=2.30978:i=2174_2993 on theBenchmark for (2993ds/2174Mi) % 28.09/4.21 % (3841833)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 28.09/4.21 % (3841833)Terminated due to inappropriate strategy. % 28.09/4.21 % (3841833)------------------------------ % 28.09/4.21 % (3841833)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 28.09/4.21 % (3841833)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.09/4.21 % (3841833)CaDiCaL version: 2.1.3 % 28.09/4.21 % (3841833)Termination reason: Inappropriate % 28.09/4.21 % (3841833)Time elapsed: 0.001 s % 28.09/4.21 % (3841833)Peak memory usage: 10 MB % 28.09/4.21 % (3841833)Instructions burned: 1 (million) % 28.09/4.21 % (3841833)------------------------------ % 28.09/4.21 % (3841833)------------------------------ % 28.09/4.21 % (3841835)ott-2_1_sil=16000:newcnf=on:random_seed=2889980637:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2993 on theBenchmark for (2993ds/869Mi) % 28.09/4.21 % (3841819)Instruction limit reached! % 28.09/4.21 % (3841819)------------------------------ % 28.09/4.21 % (3841819)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 28.09/4.21 % (3841819)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.09/4.21 % (3841819)CaDiCaL version: 2.1.3 % 28.09/4.21 % (3841819)Termination reason: Instruction limit % 28.09/4.21 % (3841819)Termination phase: Saturation % 28.09/4.21 % (3841819)Time elapsed: 0.497 s % 28.09/4.21 % (3841819)Peak memory usage: 18 MB % 28.09/4.21 % (3841819)Instructions burned: 880 (million) % 28.09/4.21 % (3841837)ott+10_1_sil=32000:tgt=ground:random_seed=460691941:i=5114:av=off_2992 on theBenchmark for (2992ds/5114Mi) % 28.09/4.21 % (3841802)Instruction limit reached! % 28.09/4.21 % (3841802)------------------------------ % 28.09/4.21 % (3841802)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 28.09/4.21 % (3841802)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.09/4.21 % (3841802)CaDiCaL version: 2.1.3 % 28.09/4.21 % (3841802)Termination reason: Instruction limit % 28.09/4.21 % (3841802)Termination phase: Saturation % 28.09/4.21 % (3841802)Time elapsed: 0.664 s % 28.09/4.21 % (3841802)Peak memory usage: 19 MB % 28.09/4.21 % (3841802)Instructions burned: 1179 (million) % 28.09/4.21 % (3841839)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=1324009935:i=54282_2991 on theBenchmark for (2991ds/54282Mi) % 28.09/4.21 % (3841839)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 28.09/4.21 % (3841839)Terminated due to inappropriate strategy. % 28.09/4.21 % (3841839)------------------------------ % 28.09/4.21 % (3841839)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 28.09/4.21 % (3841839)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.09/4.21 % (3841839)CaDiCaL version: 2.1.3 % 28.09/4.21 % (3841839)Termination reason: Inappropriate % 28.09/4.21 % (3841839)Time elapsed: 0.001 s % 28.09/4.21 % (3841839)Peak memory usage: 10 MB % 28.09/4.21 % (3841839)Instructions burned: 1 (million) % 84.88/12.27 % (3841839)------------------------------ % 84.88/12.27 % (3841839)------------------------------ % 84.88/12.27 % (3841841)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3083326864:i=3512:aac=none_2991 on theBenchmark for (2991ds/3512Mi) % 84.88/12.27 % (3841835)Instruction limit reached! % 84.88/12.27 % (3841835)------------------------------ % 84.88/12.27 % (3841835)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 84.88/12.27 % (3841835)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 84.88/12.27 % (3841835)CaDiCaL version: 2.1.3 % 84.88/12.27 % (3841835)Termination reason: Instruction limit % 84.88/12.27 % (3841835)Termination phase: Saturation % 84.88/12.27 % (3841835)Time elapsed: 0.489 s % 84.88/12.27 % (3841835)Peak memory usage: 15 MB % 84.88/12.27 % (3841835)Instructions burned: 870 (million) % 84.88/12.27 % (3841843)dis+21_1_sil=32000:sas=cadical:random_seed=2702297484:i=3773:amm=off_2988 on theBenchmark for (2988ds/3773Mi) % 84.88/12.27 % (3841829)Instruction limit reached! % 84.88/12.27 % (3841829)------------------------------ % 84.88/12.27 % (3841829)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 84.88/12.27 % (3841829)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 84.88/12.27 % (3841829)CaDiCaL version: 2.1.3 % 84.88/12.27 % (3841829)Termination reason: Instruction limit % 84.88/12.27 % (3841829)Termination phase: Saturation % 84.88/12.27 % (3841829)Time elapsed: 0.813 s % 84.88/12.27 % (3841829)Peak memory usage: 24 MB % 84.88/12.27 % (3841829)Instructions burned: 1473 (million) % 84.88/12.27 % (3841845)ott+11_1_sil=16000:gs=on:random_seed=716757884:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2987 on theBenchmark for (2987ds/2251Mi) % 84.88/12.27 % (3841827)Instruction limit reached! % 84.88/12.27 % (3841827)------------------------------ % 84.88/12.27 % (3841827)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 84.88/12.27 % (3841827)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 84.88/12.27 % (3841827)CaDiCaL version: 2.1.3 % 84.88/12.27 % (3841827)Termination reason: Instruction limit % 84.88/12.27 % (3841827)Termination phase: Saturation % 84.88/12.27 % (3841827)Time elapsed: 1.488 s % 84.88/12.27 % (3841827)Peak memory usage: 42 MB % 84.88/12.27 % (3841827)Instructions burned: 5132 (million) % 84.88/12.27 % (3841847)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=2698839770:fmbsr=1.6:i=67534_2981 on theBenchmark for (2981ds/67534Mi) % 84.88/12.27 % (3841847)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 84.88/12.27 % (3841847)Terminated due to inappropriate strategy. % 84.88/12.27 % (3841847)------------------------------ % 84.88/12.27 % (3841847)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 84.88/12.27 % (3841847)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 84.88/12.27 % (3841847)CaDiCaL version: 2.1.3 % 84.88/12.27 % (3841847)Termination reason: Inappropriate % 84.88/12.27 % (3841847)Time elapsed: 0.0000 s % 84.88/12.27 % (3841847)Peak memory usage: 10 MB % 84.88/12.27 % (3841847)Instructions burned: 1 (million) % 84.88/12.27 % (3841847)------------------------------ % 84.88/12.27 % (3841847)------------------------------ % 84.88/12.27 % (3841849)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=3023068246:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2981 on theBenchmark for (2981ds/4591Mi) % 84.88/12.27 % (3841845)Instruction limit reached! % 84.88/12.27 % (3841845)------------------------------ % 84.88/12.27 % (3841845)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 84.88/12.27 % (3841845)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 84.88/12.27 % (3841845)CaDiCaL version: 2.1.3 % 84.88/12.27 % (3841845)Termination reason: Instruction limit % 84.88/12.27 % (3841845)Termination phase: Saturation % 84.88/12.27 % (3841845)Time elapsed: 1.223 s % 84.88/12.27 % (3841845)Peak memory usage: 21 MB % 84.88/12.27 % (3841845)Instructions burned: 2252 (million) % 84.88/12.27 % (3841851)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=2651934110:i=29340_2974 on theBenchmark for (2974ds/29340Mi) % 84.88/12.27 % (3841841)Instruction limit reached! % 84.88/12.27 % (3841841)------------------------------ % 84.88/12.27 % (3841841)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 84.88/12.27 % (3841841)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 84.88/12.27 % (3841841)CaDiCaL version: 2.1.3 % 84.88/12.27 % (3841841)Termination reason: Instruction limit % 123.87/17.72 % (3841841)Termination phase: Saturation % 123.87/17.72 % (3841841)Time elapsed: 1.891 s % 123.87/17.72 % (3841841)Peak memory usage: 32 MB % 123.87/17.72 % (3841841)Instructions burned: 3512 (million) % 123.87/17.72 % (3841853)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=3328790953:i=5211_2972 on theBenchmark for (2972ds/5211Mi) % 123.87/17.72 % (3841849)Instruction limit reached! % 123.87/17.72 % (3841849)------------------------------ % 123.87/17.72 % (3841849)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 123.87/17.72 % (3841849)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 123.87/17.72 % (3841849)CaDiCaL version: 2.1.3 % 123.87/17.72 % (3841849)Termination reason: Instruction limit % 123.87/17.72 % (3841849)Termination phase: Saturation % 123.87/17.72 % (3841849)Time elapsed: 1.279 s % 123.87/17.72 % (3841849)Peak memory usage: 47 MB % 123.87/17.72 % (3841849)Instructions burned: 4595 (million) % 123.87/17.72 % (3841855)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=2871947390:i=5497:nm=2_2968 on theBenchmark for (2968ds/5497Mi) % 123.87/17.72 % (3841855)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 123.87/17.72 % (3841855)Terminated due to inappropriate strategy. % 123.87/17.72 % (3841855)------------------------------ % 123.87/17.72 % (3841855)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 123.87/17.72 % (3841855)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 123.87/17.72 % (3841855)CaDiCaL version: 2.1.3 % 123.87/17.72 % (3841855)Termination reason: Inappropriate % 123.87/17.72 % (3841855)Time elapsed: 0.0000 s % 123.87/17.72 % (3841855)Peak memory usage: 10 MB % 123.87/17.72 % (3841855)Instructions burned: 1 (million) % 123.87/17.72 % (3841855)------------------------------ % 123.87/17.72 % (3841855)------------------------------ % 123.87/17.72 % (3841857)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=1690468291:fmbsr=2:i=46332_2968 on theBenchmark for (2968ds/46332Mi) % 123.87/17.72 % (3841857)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 123.87/17.72 % (3841857)Terminated due to inappropriate strategy. % 123.87/17.72 % (3841857)------------------------------ % 123.87/17.72 % (3841857)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 123.87/17.72 % (3841857)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 123.87/17.72 % (3841857)CaDiCaL version: 2.1.3 % 123.87/17.72 % (3841857)Termination reason: Inappropriate % 123.87/17.72 % (3841857)Time elapsed: 0.0000 s % 123.87/17.72 % (3841857)Peak memory usage: 10 MB % 123.87/17.72 % (3841857)Instructions burned: 1 (million) % 123.87/17.72 % (3841857)------------------------------ % 123.87/17.72 % (3841857)------------------------------ % 123.87/17.72 % (3841859)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=3030282166:i=14071_2968 on theBenchmark for (2968ds/14071Mi) % 123.87/17.72 % (3841859)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 123.87/17.72 % (3841859)Terminated due to inappropriate strategy. % 123.87/17.72 % (3841859)------------------------------ % 123.87/17.72 % (3841859)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 123.87/17.72 % (3841859)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 123.87/17.72 % (3841859)CaDiCaL version: 2.1.3 % 123.87/17.72 % (3841859)Termination reason: Inappropriate % 123.87/17.72 % (3841859)Time elapsed: 0.0000 s % 123.87/17.72 % (3841859)Peak memory usage: 10 MB % 123.87/17.72 % (3841859)Instructions burned: 1 (million) % 123.87/17.72 % (3841859)------------------------------ % 123.87/17.72 % (3841859)------------------------------ % 123.87/17.72 % (3841861)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1379643017:i=22565:add=on:rawr=on_2968 on theBenchmark for (2968ds/22565Mi) % 123.87/17.72 % (3841843)Instruction limit reached! % 123.87/17.72 % (3841843)------------------------------ % 123.87/17.72 % (3841843)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 123.87/17.72 % (3841843)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 123.87/17.72 % (3841843)CaDiCaL version: 2.1.3 % 123.87/17.72 % (3841843)Termination reason: Instruction limit % 123.87/17.72 % (3841843)Termination phase: Saturation % 123.87/17.72 % (3841843)Time elapsed: 2.098 s % 123.87/17.72 % (3841843)Peak memory usage: 33 MB % 123.87/17.72 % (3841843)Instructions burned: 3773 (million) % 123.87/17.72 % (3841863)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=2431999947:i=8173:av=off_2967 on theBenchmark for (2967ds/8173Mi) % 123.87/17.72 % (3841837)Instruction limit reached! % 124.47/17.82 % (3841837)------------------------------ % 124.47/17.82 % (3841837)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 124.47/17.82 % (3841837)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 124.47/17.82 % (3841837)CaDiCaL version: 2.1.3 % 124.47/17.82 % (3841837)Termination reason: Instruction limit % 124.47/17.82 % (3841837)Termination phase: Saturation % 124.47/17.82 % (3841837)Time elapsed: 3.230 s % 124.47/17.82 % (3841837)Peak memory usage: 33 MB % 124.47/17.82 % (3841837)Instructions burned: 5114 (million) % 124.47/17.82 % (3841865)dis+10_16:1_sil=16000:random_seed=547676222:i=9155:fsr=off_2960 on theBenchmark for (2960ds/9155Mi) % 124.47/17.82 % (3841853)Instruction limit reached! % 124.47/17.82 % (3841853)------------------------------ % 124.47/17.82 % (3841853)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 124.47/17.82 % (3841853)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 124.47/17.82 % (3841853)CaDiCaL version: 2.1.3 % 124.47/17.82 % (3841853)Termination reason: Instruction limit % 124.47/17.82 % (3841853)Termination phase: Saturation % 124.47/17.82 % (3841853)Time elapsed: 2.738 s % 124.47/17.82 % (3841853)Peak memory usage: 53 MB % 124.47/17.82 % (3841853)Instructions burned: 5213 (million) % 124.47/17.82 % (3841867)ott-3_8_sil=64000:random_seed=748459180:i=20139:bs=on_2944 on theBenchmark for (2944ds/20139Mi) % 124.47/17.82 % (3841861)Instruction limit reached! % 124.47/17.82 % (3841861)------------------------------ % 124.47/17.82 % (3841861)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 124.47/17.82 % (3841861)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 124.47/17.82 % (3841861)CaDiCaL version: 2.1.3 % 124.47/17.82 % (3841861)Termination reason: Instruction limit % 124.47/17.82 % (3841861)Termination phase: Saturation % 124.47/17.82 % (3841861)Time elapsed: 5.012 s % 124.47/17.82 % (3841861)Peak memory usage: 20 MB % 124.47/17.82 % (3841861)Instructions burned: 22567 (million) % 124.47/17.82 % (3841869)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=205540809:fmbsr=2:i=32576_2918 on theBenchmark for (2918ds/32576Mi) % 124.47/17.82 % (3841869)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 124.47/17.82 % (3841869)Terminated due to inappropriate strategy. % 124.47/17.82 % (3841869)------------------------------ % 124.47/17.82 % (3841869)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 124.47/17.82 % (3841869)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 124.47/17.82 % (3841869)CaDiCaL version: 2.1.3 % 124.47/17.82 % (3841869)Termination reason: Inappropriate % 124.47/17.82 % (3841869)Time elapsed: 0.0000 s % 124.47/17.82 % (3841869)Peak memory usage: 10 MB % 124.47/17.82 % (3841869)Instructions burned: 1 (million) % 124.47/17.82 % (3841869)------------------------------ % 124.47/17.82 % (3841869)------------------------------ % 124.47/17.82 % (3841871)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=1227373091:i=11404_2918 on theBenchmark for (2918ds/11404Mi) % 124.47/17.82 % (3841863)Instruction limit reached! % 124.47/17.82 % (3841863)------------------------------ % 124.47/17.82 % (3841863)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 124.47/17.82 % (3841863)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 124.47/17.82 % (3841863)CaDiCaL version: 2.1.3 % 124.47/17.82 % (3841863)Termination reason: Instruction limit % 124.47/17.82 % (3841863)Termination phase: Saturation % 124.47/17.82 % (3841863)Time elapsed: 5.083 s % 124.47/17.82 % (3841863)Peak memory usage: 55 MB % 124.47/17.82 % (3841863)Instructions burned: 8174 (million) % 124.47/17.82 % (3841873)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=3098266501:i=14134_2916 on theBenchmark for (2916ds/14134Mi) % 124.47/17.82 % (3841865)Instruction limit reached! % 124.47/17.82 % (3841865)------------------------------ % 124.47/17.82 % (3841865)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 124.47/17.82 % (3841865)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 124.47/17.82 % (3841865)CaDiCaL version: 2.1.3 % 124.47/17.82 % (3841865)Termination reason: Instruction limit % 124.47/17.82 % (3841865)Termination phase: Saturation % 124.47/17.82 % (3841865)Time elapsed: 4.683 s % 124.47/17.82 % (3841865)Peak memory usage: 53 MB % 124.47/17.82 % (3841865)Instructions burned: 9156 (million) % 124.47/17.82 % (3841875)dis+33_16_sil=32000:sac=on:random_seed=3030105654:i=15851:nm=0_2913 on theBenchmark for (2913ds/15851Mi) % 124.47/17.82 % (3841871)Instruction limit reached! % 124.47/17.82 % (3841871)------------------------------ % 124.47/17.82 % (3841871)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 134.15/19.16 % (3841871)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 134.15/19.16 % (3841871)CaDiCaL version: 2.1.3 % 134.15/19.16 % (3841871)Termination reason: Instruction limit % 134.15/19.16 % (3841871)Termination phase: Saturation % 134.15/19.16 % (3841871)Time elapsed: 3.830 s % 134.15/19.16 % (3841871)Peak memory usage: 61 MB % 134.15/19.16 % (3841871)Instructions burned: 11406 (million) % 134.15/19.16 % (3841877)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=3383700264:avsq=on:i=17627:add=on:amm=off_2879 on theBenchmark for (2879ds/17627Mi) % 134.15/19.16 % (3841851)Instruction limit reached! % 134.15/19.16 % (3841851)------------------------------ % 134.15/19.16 % (3841851)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 134.15/19.16 % (3841851)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 134.15/19.16 % (3841851)CaDiCaL version: 2.1.3 % 134.15/19.16 % (3841851)Termination reason: Instruction limit % 134.15/19.16 % (3841851)Termination phase: Saturation % 134.15/19.16 % (3841851)Time elapsed: 11.903 s % 134.15/19.16 % (3841851)Peak memory usage: 118 MB % 134.15/19.16 % (3841851)Instructions burned: 29340 (million) % 134.15/19.16 % (3842010)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=1618130641:s2a=on:i=53295_2855 on theBenchmark for (2855ds/53295Mi) % 134.15/19.16 % (3841875)Instruction limit reached! % 134.15/19.16 % (3841875)------------------------------ % 134.15/19.16 % (3841875)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 134.15/19.16 % (3841875)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 134.15/19.16 % (3841875)CaDiCaL version: 2.1.3 % 134.15/19.16 % (3841875)Termination reason: Instruction limit % 134.15/19.16 % (3841875)Termination phase: Saturation % 134.15/19.16 % (3841875)Time elapsed: 8.619 s % 134.15/19.16 % (3841875)Peak memory usage: 140 MB % 134.15/19.16 % (3841875)Instructions burned: 15853 (million) % 134.15/19.16 % (3842225)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=2885707314:i=26857:ins=20_2826 on theBenchmark for (2826ds/26857Mi) % 134.15/19.16 % (3842225)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 134.15/19.16 % (3842225)Terminated due to inappropriate strategy. % 134.15/19.16 % (3842225)------------------------------ % 134.15/19.16 % (3842225)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 134.15/19.16 % (3842225)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 134.15/19.16 % (3842225)CaDiCaL version: 2.1.3 % 134.15/19.16 % (3842225)Termination reason: Inappropriate % 134.15/19.16 % (3842225)Time elapsed: 0.001 s % 134.15/19.16 % (3842225)Peak memory usage: 10 MB % 134.15/19.16 % (3842225)Instructions burned: 1 (million) % 134.15/19.16 % (3842225)------------------------------ % 134.15/19.16 % (3842225)------------------------------ % 134.15/19.16 % (3842227)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=4012066227:i=28120:bs=on:fsr=off_2826 on theBenchmark for (2826ds/28120Mi) % 134.15/19.16 % (3841877)Instruction limit reached! % 134.15/19.16 % (3841877)------------------------------ % 134.15/19.16 % (3841877)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 134.15/19.16 % (3841877)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 134.15/19.16 % (3841877)CaDiCaL version: 2.1.3 % 134.15/19.16 % (3841877)Termination reason: Instruction limit % 134.15/19.16 % (3841877)Termination phase: Saturation % 134.15/19.16 % (3841877)Time elapsed: 5.398 s % 134.15/19.16 % (3841877)Peak memory usage: 111 MB % 134.15/19.16 % (3841877)Instructions burned: 17629 (million) % 134.15/19.16 % (3842229)fmb+10_1_sil=256000:fmbss=7:random_seed=3124319386:fmbsr=1.6:i=182295_2825 on theBenchmark for (2825ds/182295Mi) % 134.15/19.16 % (3842229)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 134.15/19.16 % (3842229)Terminated due to inappropriate strategy. % 134.15/19.16 % (3842229)------------------------------ % 134.15/19.16 % (3842229)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 134.15/19.16 % (3842229)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 134.15/19.16 % (3842229)CaDiCaL version: 2.1.3 % 134.15/19.16 % (3842229)Termination reason: Inappropriate % 134.15/19.16 % (3842229)Time elapsed: 0.0000 s % 134.15/19.16 % (3842229)Peak memory usage: 10 MB % 134.15/19.16 % (3842229)Instructions burned: 1 (million) % 134.15/19.16 % (3842229)------------------------------ % 134.15/19.16 % (3842229)------------------------------ % 134.15/19.16 % (3842231)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=641981943:i=44625:gsp=on_2825 on theBenchmark for (2825ds/44625Mi) % 146.08/20.98 % (3842231)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 146.08/20.98 % (3842231)Terminated due to inappropriate strategy. % 146.08/20.98 % (3842231)------------------------------ % 146.08/20.98 % (3842231)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 146.08/20.98 % (3842231)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 146.08/20.98 % (3842231)CaDiCaL version: 2.1.3 % 146.08/20.98 % (3842231)Termination reason: Inappropriate % 146.08/20.98 % (3842231)Time elapsed: 0.001 s % 146.08/20.98 % (3842231)Peak memory usage: 10 MB % 146.08/20.98 % (3842231)Instructions burned: 1 (million) % 146.08/20.98 % (3842231)------------------------------ % 146.08/20.98 % (3842231)------------------------------ % 146.08/20.98 % (3842233)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=4011883051:i=160505_2825 on theBenchmark for (2825ds/160505Mi) % 146.08/20.98 % (3842233)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 146.08/20.98 % (3842233)Terminated due to inappropriate strategy. % 146.08/20.98 % (3842233)------------------------------ % 146.08/20.98 % (3842233)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 146.08/20.98 % (3842233)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 146.08/20.98 % (3842233)CaDiCaL version: 2.1.3 % 146.08/20.98 % (3842233)Termination reason: Inappropriate % 146.08/20.98 % (3842233)Time elapsed: 0.001 s % 146.08/20.98 % (3842233)Peak memory usage: 10 MB % 146.08/20.98 % (3842233)Instructions burned: 1 (million) % 146.08/20.98 % (3842233)------------------------------ % 146.08/20.98 % (3842233)------------------------------ % 146.08/20.98 % (3842235)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=1762874096:fmbsr=1.3:i=225729_2824 on theBenchmark for (2824ds/225729Mi) % 146.08/20.98 % (3842235)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 146.08/20.98 % (3842235)Terminated due to inappropriate strategy. % 146.08/20.98 % (3842235)------------------------------ % 146.08/20.98 % (3842235)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 146.08/20.98 % (3842235)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 146.08/20.98 % (3842235)CaDiCaL version: 2.1.3 % 146.08/20.98 % (3842235)Termination reason: Inappropriate % 146.08/20.98 % (3842235)Time elapsed: 0.001 s % 146.08/20.98 % (3842235)Peak memory usage: 10 MB % 146.08/20.98 % (3842235)Instructions burned: 1 (million) % 146.08/20.98 % (3842235)------------------------------ % 146.08/20.98 % (3842235)------------------------------ % 146.08/20.98 % (3842237)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=1294724057:fmbsr=2:i=185024:ins=7_2824 on theBenchmark for (2824ds/185024Mi) % 146.08/20.98 % (3842237)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 146.08/20.98 % (3842237)Terminated due to inappropriate strategy. % 146.08/20.98 % (3842237)------------------------------ % 146.08/20.98 % (3842237)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 146.08/20.98 % (3842237)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 146.08/20.98 % (3842237)CaDiCaL version: 2.1.3 % 146.08/20.98 % (3842237)Termination reason: Inappropriate % 146.08/20.98 % (3842237)Time elapsed: 0.001 s % 146.08/20.98 % (3842237)Peak memory usage: 10 MB % 146.08/20.98 % (3842237)Instructions burned: 1 (million) % 146.08/20.98 % (3842237)------------------------------ % 146.08/20.98 % (3842237)------------------------------ % 146.08/20.98 % (3842239)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=548985920:rtra=on_2824 on theBenchmark for (2824ds/0Mi) % 146.08/20.98 % (3842239)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 146.08/20.98 % (3842239)Terminated due to inappropriate strategy. % 146.08/20.98 % (3842239)------------------------------ % 146.08/20.98 % (3842239)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 146.08/20.98 % (3842239)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 146.08/20.98 % (3842239)CaDiCaL version: 2.1.3 % 146.08/20.98 % (3842239)Termination reason: Inappropriate % 146.08/20.98 % (3842239)Time elapsed: 0.0000 s % 146.08/20.98 % (3842239)Peak memory usage: 10 MB % 146.08/20.98 % (3842239)Instructions burned: 1 (million) % 146.08/20.98 % (3842239)------------------------------ % 146.08/20.98 % (3842239)------------------------------ % 146.08/20.98 % (3842241)% WARNING: option uhcvi not known. % 146.08/20.98 % (3842241)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1915174642:i=271062:add=off:rtra=on:rawr=on_2824 on theBenchmark for (2824ds/271062Mi) % 168.92/24.06 % (3841873)Instruction limit reached! % 168.92/24.06 % (3841873)------------------------------ % 168.92/24.06 % (3841873)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 168.92/24.06 % (3841873)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 168.92/24.06 % (3841873)CaDiCaL version: 2.1.3 % 168.92/24.06 % (3841873)Termination reason: Instruction limit % 168.92/24.06 % (3841873)Termination phase: Saturation % 168.92/24.06 % (3841873)Time elapsed: 9.263 s % 168.92/24.06 % (3841873)Peak memory usage: 75 MB % 168.92/24.06 % (3841873)Instructions burned: 14135 (million) % 168.92/24.06 % (3842243)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3072953434:i=176048:add=on:rtra=on:rawr=on_2823 on theBenchmark for (2823ds/176048Mi) % 168.92/24.06 % (3841867)Instruction limit reached! % 168.92/24.06 % (3841867)------------------------------ % 168.92/24.06 % (3841867)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 168.92/24.06 % (3841867)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 168.92/24.06 % (3841867)CaDiCaL version: 2.1.3 % 168.92/24.06 % (3841867)Termination reason: Instruction limit % 168.92/24.06 % (3841867)Termination phase: Saturation % 168.92/24.06 % (3841867)Time elapsed: 12.610 s % 168.92/24.06 % (3841867)Peak memory usage: 69 MB % 168.92/24.06 % (3841867)Instructions burned: 20140 (million) % 168.92/24.06 % (3842245)dis+10_1_sil=32000:si=on:sp=arity:random_seed=518536119:i=206:fgj=on:rtra=on_2818 on theBenchmark for (2818ds/206Mi) % 168.92/24.06 % (3842245)Instruction limit reached! % 168.92/24.06 % (3842245)------------------------------ % 168.92/24.06 % (3842245)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 168.92/24.06 % (3842245)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 168.92/24.06 % (3842245)CaDiCaL version: 2.1.3 % 168.92/24.06 % (3842245)Termination reason: Instruction limit % 168.92/24.06 % (3842245)Termination phase: Saturation % 168.92/24.06 % (3842245)Time elapsed: 0.125 s % 168.92/24.06 % (3842245)Peak memory usage: 13 MB % 168.92/24.06 % (3842245)Instructions burned: 207 (million) % 168.92/24.06 % (3842247)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=466496022:i=232:rtra=on_2816 on theBenchmark for (2816ds/232Mi) % 168.92/24.06 % (3842247)Instruction limit reached! % 168.92/24.06 % (3842247)------------------------------ % 168.92/24.06 % (3842247)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 168.92/24.06 % (3842247)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 168.92/24.06 % (3842247)CaDiCaL version: 2.1.3 % 168.92/24.06 % (3842247)Termination reason: Instruction limit % 168.92/24.06 % (3842247)Termination phase: Saturation % 168.92/24.06 % (3842247)Time elapsed: 0.145 s % 168.92/24.06 % (3842247)Peak memory usage: 13 MB % 168.92/24.06 % (3842247)Instructions burned: 232 (million) % 168.92/24.06 % (3842249)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=2784713013:i=262:rtra=on_2815 on theBenchmark for (2815ds/262Mi) % 168.92/24.06 % (3842249)Instruction limit reached! % 168.92/24.06 % (3842249)------------------------------ % 168.92/24.06 % (3842249)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 168.92/24.06 % (3842249)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 168.92/24.06 % (3842249)CaDiCaL version: 2.1.3 % 168.92/24.06 % (3842249)Termination reason: Instruction limit % 168.92/24.06 % (3842249)Termination phase: Saturation % 168.92/24.06 % (3842249)Time elapsed: 0.155 s % 168.92/24.06 % (3842249)Peak memory usage: 13 MB % 168.92/24.06 % (3842249)Instructions burned: 262 (million) % 168.92/24.06 % (3842251)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=2150433212:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2813 on theBenchmark for (2813ds/318Mi) % 168.92/24.06 % (3842251)Instruction limit reached! % 168.92/24.06 % (3842251)------------------------------ % 168.92/24.06 % (3842251)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 168.92/24.06 % (3842251)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 168.92/24.06 % (3842251)CaDiCaL version: 2.1.3 % 168.92/24.06 % (3842251)Termination reason: Instruction limit % 168.92/24.06 % (3842251)Termination phase: Saturation % 168.92/24.06 % (3842251)Time elapsed: 0.212 s % 168.92/24.06 % (3842251)Peak memory usage: 15 MB % 168.92/24.06 % (3842251)Instructions burned: 318 (million) % 168.92/24.06 % (3842253)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=1031612111:i=1428:nm=2:rtra=on_2811 on theBenchmark for (2811ds/1428Mi) % 211.48/30.08 % (3842253)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 211.48/30.08 % (3842253)Terminated due to inappropriate strategy. % 211.48/30.08 % (3842253)------------------------------ % 211.48/30.08 % (3842253)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 211.48/30.08 % (3842253)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 211.48/30.08 % (3842253)CaDiCaL version: 2.1.3 % 211.48/30.08 % (3842253)Termination reason: Inappropriate % 211.48/30.08 % (3842253)Time elapsed: 0.001 s % 211.48/30.08 % (3842253)Peak memory usage: 10 MB % 211.48/30.08 % (3842253)Instructions burned: 1 (million) % 211.48/30.08 % (3842253)------------------------------ % 211.48/30.08 % (3842253)------------------------------ % 211.48/30.08 % (3842255)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=2551811078:i=262:bd=preordered:rtra=on:fsd=on_2810 on theBenchmark for (2810ds/262Mi) % 211.48/30.08 % (3842255)Instruction limit reached! % 211.48/30.08 % (3842255)------------------------------ % 211.48/30.08 % (3842255)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 211.48/30.08 % (3842255)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 211.48/30.08 % (3842255)CaDiCaL version: 2.1.3 % 211.48/30.08 % (3842255)Termination reason: Instruction limit % 211.48/30.08 % (3842255)Termination phase: Saturation % 211.48/30.08 % (3842255)Time elapsed: 0.165 s % 211.48/30.08 % (3842255)Peak memory usage: 13 MB % 211.48/30.08 % (3842255)Instructions burned: 262 (million) % 211.48/30.08 % (3842257)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=1869058164:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2808 on theBenchmark for (2808ds/1368Mi) % 211.48/30.08 % (3842257)Instruction limit reached! % 211.48/30.08 % (3842257)------------------------------ % 211.48/30.08 % (3842257)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 211.48/30.08 % (3842257)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 211.48/30.08 % (3842257)CaDiCaL version: 2.1.3 % 211.48/30.08 % (3842257)Termination reason: Instruction limit % 211.48/30.08 % (3842257)Termination phase: Saturation % 211.48/30.08 % (3842257)Time elapsed: 0.774 s % 211.48/30.08 % (3842257)Peak memory usage: 22 MB % 211.48/30.08 % (3842257)Instructions burned: 1369 (million) % 211.48/30.08 % (3842372)ott-21_1_sil=16000:si=on:fs=off:random_seed=4216798400:i=360:av=off:fsr=off:rtra=on_2801 on theBenchmark for (2801ds/360Mi) % 211.48/30.08 % (3842372)Instruction limit reached! % 211.48/30.08 % (3842372)------------------------------ % 211.48/30.08 % (3842372)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 211.48/30.08 % (3842372)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 211.48/30.08 % (3842372)CaDiCaL version: 2.1.3 % 211.48/30.08 % (3842372)Termination reason: Instruction limit % 211.48/30.08 % (3842372)Termination phase: Saturation % 211.48/30.08 % (3842372)Time elapsed: 0.157 s % 211.48/30.08 % (3842372)Peak memory usage: 12 MB % 211.48/30.08 % (3842372)Instructions burned: 360 (million) % 211.48/30.08 % (3842374)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1179048751:i=954:bd=all:rtra=on_2799 on theBenchmark for (2799ds/954Mi) % 211.48/30.08 % (3842374)Instruction limit reached! % 211.48/30.08 % (3842374)------------------------------ % 211.48/30.08 % (3842374)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 211.48/30.08 % (3842374)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 211.48/30.08 % (3842374)CaDiCaL version: 2.1.3 % 211.48/30.08 % (3842374)Termination reason: Instruction limit % 211.48/30.08 % (3842374)Termination phase: Saturation % 211.48/30.08 % (3842374)Time elapsed: 0.622 s % 211.48/30.08 % (3842374)Peak memory usage: 16 MB % 211.48/30.08 % (3842374)Instructions burned: 954 (million) % 211.48/30.08 % (3842376)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=1457154770:fmbsr=1.3:i=1730:ins=25:rtra=on_2792 on theBenchmark for (2792ds/1730Mi) % 211.48/30.08 % (3842376)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 211.48/30.08 % (3842376)Terminated due to inappropriate strategy. % 211.48/30.08 % (3842376)------------------------------ % 211.48/30.08 % (3842376)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 211.48/30.08 % (3842376)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 211.48/30.08 % (3842376)CaDiCaL version: 2.1.3 % 211.48/30.08 % (3842376)Termination reason: Inappropriate % 224.56/37.15 % (3842376)Time elapsed: 0.001 s % 224.56/37.15 % (3842376)Peak memory usage: 10 MB % 224.56/37.15 % (3842376)Instructions burned: 1 (million) % 224.56/37.15 % (3842376)------------------------------ % 224.56/37.15 % (3842376)------------------------------ % 224.56/37.15 % (3842378)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=4032706156:i=2358:rtra=on_2792 on theBenchmark for (2792ds/2358Mi) % 224.56/37.15 % (3842378)Instruction limit reached! % 224.56/37.15 % (3842378)------------------------------ % 224.56/37.15 % (3842378)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 224.56/37.15 % (3842378)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 224.56/37.15 % (3842378)CaDiCaL version: 2.1.3 % 224.56/37.15 % (3842378)Termination reason: Instruction limit % 224.56/37.15 % (3842378)Termination phase: Saturation % 224.56/37.15 % (3842378)Time elapsed: 1.123 s % 224.56/37.15 % (3842378)Peak memory usage: 20 MB % 224.56/37.15 % (3842378)Instructions burned: 2358 (million) % 224.56/37.15 % (3842380)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=2460360177:i=1778:ins=1:rtra=on_2781 on theBenchmark for (2781ds/1778Mi) % 224.56/37.15 % (3842380)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 224.56/37.15 % (3842380)Terminated due to inappropriate strategy. % 224.56/37.15 % (3842380)------------------------------ % 224.56/37.15 % (3842380)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 224.56/37.15 % (3842380)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 224.56/37.15 % (3842380)CaDiCaL version: 2.1.3 % 224.56/37.15 % (3842380)Termination reason: Inappropriate % 224.56/37.15 % (3842380)Time elapsed: 0.001 s % 224.56/37.15 % (3842380)Peak memory usage: 10 MB % 224.56/37.15 % (3842380)Instructions burned: 1 (million) % 224.56/37.15 % (3842380)------------------------------ % 224.56/37.15 % (3842380)------------------------------ % 224.56/37.15 % (3842382)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=709454135:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2780 on theBenchmark for (2780ds/1384Mi) % 224.56/37.15 % (3842382)Instruction limit reached! % 224.56/37.15 % (3842382)------------------------------ % 224.56/37.15 % (3842382)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 224.56/37.15 % (3842382)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 224.56/37.15 % (3842382)CaDiCaL version: 2.1.3 % 224.56/37.15 % (3842382)Termination reason: Instruction limit % 224.56/37.15 % (3842382)Termination phase: Saturation % 224.56/37.15 % (3842382)Time elapsed: 0.835 s % 224.56/37.15 % (3842382)Peak memory usage: 23 MB % 224.56/37.15 % (3842382)Instructions burned: 1386 (million) % 224.56/37.15 % (3842384)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=3524013290:i=1758:kws=inv_precedence:fsr=off:rtra=on_2772 on theBenchmark for (2772ds/1758Mi) % 224.56/37.15 % (3842384)Instruction limit reached! % 224.56/37.15 % (3842384)------------------------------ % 224.56/37.15 % (3842384)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 224.56/37.15 % (3842384)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 224.56/37.15 % (3842384)CaDiCaL version: 2.1.3 % 224.56/37.15 % (3842384)Termination reason: Instruction limit % 224.56/37.15 % (3842384)Termination phase: Saturation % 224.56/37.15 % (3842384)Time elapsed: 0.992 s % 224.56/37.15 % (3842384)Peak memory usage: 27 MB % 224.56/37.15 % (3842384)Instructions burned: 1759 (million) % 224.56/37.15 % (3842386)fmb+10_1_sil=64000:si=on:random_seed=124848402:i=44122:nm=2:rtra=on:gsp=on_2762 on theBenchmark for (2762ds/44122Mi) % 224.56/37.15 % (3842386)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 224.56/37.15 % (3842386)Terminated due to inappropriate strategy. % 224.56/37.15 % (3842386)------------------------------ % 224.56/37.15 % (3842386)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 224.56/37.15 % (3842386)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 224.56/37.15 % (3842386)CaDiCaL version: 2.1.3 % 224.56/37.15 % (3842386)Termination reason: Inappropriate % 224.56/37.15 % (3842386)Time elapsed: 0.001 s % 224.56/37.15 % (3842386)Peak memory usage: 11 MB % 224.56/37.15 % (3842386)Instructions burned: 1 (million) % 224.56/37.15 % (3842386)------------------------------ % 224.56/37.15 % (3842386)------------------------------ % 224.56/37.15 % (3842388)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=2988814837:i=19030:nm=5:rtra=on_2762 on theBenchmark for (2762ds/19030Mi) % 280.78/39.81 % (3842388)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 280.78/39.81 % (3842388)Terminated due to inappropriate strategy. % 280.78/39.81 % (3842388)------------------------------ % 280.78/39.81 % (3842388)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 280.78/39.81 % (3842388)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 280.78/39.81 % (3842388)CaDiCaL version: 2.1.3 % 280.78/39.81 % (3842388)Termination reason: Inappropriate % 280.78/39.81 % (3842388)Time elapsed: 0.001 s % 280.78/39.81 % (3842388)Peak memory usage: 10 MB % 280.78/39.81 % (3842388)Instructions burned: 1 (million) % 280.78/39.81 % (3842388)------------------------------ % 280.78/39.81 % (3842388)------------------------------ % 280.78/39.81 % (3842390)fmb+10_1_sil=64000:sas=cadical:si=on:fmbss=8:random_seed=2807252223:fmbsr=1.7:i=1840:rtra=on_2761 on theBenchmark for (2761ds/1840Mi) % 280.78/39.81 % (3842390)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 280.78/39.81 % (3842390)Terminated due to inappropriate strategy. % 280.78/39.81 % (3842390)------------------------------ % 280.78/39.81 % (3842390)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 280.78/39.81 % (3842390)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 280.78/39.81 % (3842390)CaDiCaL version: 2.1.3 % 280.78/39.81 % (3842390)Termination reason: Inappropriate % 280.78/39.81 % (3842390)Time elapsed: 0.001 s % 280.78/39.81 % (3842390)Peak memory usage: 10 MB % 280.78/39.81 % (3842390)Instructions burned: 1 (million) % 280.78/39.81 % (3842390)------------------------------ % 280.78/39.81 % (3842390)------------------------------ % 280.78/39.81 % (3842392)dis-4_1_sil=16000:drc=ordering:si=on:sp=const_frequency:sac=on:newcnf=on:random_seed=1380619213:i=10262:rtra=on_2761 on theBenchmark for (2761ds/10262Mi) % 280.78/39.81 % (3842227)Instruction limit reached! % 280.78/39.81 % (3842227)------------------------------ % 280.78/39.81 % (3842227)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 280.78/39.81 % (3842227)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 280.78/39.81 % (3842227)CaDiCaL version: 2.1.3 % 280.78/39.81 % (3842227)Termination reason: Instruction limit % 280.78/39.81 % (3842227)Termination phase: Saturation % 280.78/39.81 % (3842227)Time elapsed: 11.930 s % 280.78/39.81 % (3842227)Peak memory usage: 28 MB % 280.78/39.81 % (3842227)Instructions burned: 28121 (million) % 280.78/39.81 % (3842595)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:si=on:sp=arity:spb=units:lsd=10:nwc=3:random_seed=46373646:i=2944:ins=7:rtra=on:fdi=8:gsp=on_2706 on theBenchmark for (2706ds/2944Mi) % 280.78/39.81 % (3842392)Instruction limit reached! % 280.78/39.81 % (3842392)------------------------------ % 280.78/39.81 % (3842392)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 280.78/39.81 % (3842392)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 280.78/39.81 % (3842392)CaDiCaL version: 2.1.3 % 280.78/39.81 % (3842392)Termination reason: Instruction limit % 280.78/39.81 % (3842392)Termination phase: Saturation % 280.78/39.81 % (3842392)Time elapsed: 5.933 s % 280.78/39.81 % (3842392)Peak memory usage: 68 MB % 280.78/39.81 % (3842392)Instructions burned: 10263 (million) % 280.78/39.81 % (3842739)fmb+10_1_sil=16000:sas=cadical:si=on:bce=on:fmbss=77:random_seed=300733262:i=12648:rtra=on_2701 on theBenchmark for (2701ds/12648Mi) % 280.78/39.81 % (3842739)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 280.78/39.81 % (3842739)Terminated due to inappropriate strategy. % 280.78/39.81 % (3842739)------------------------------ % 280.78/39.81 % (3842739)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 280.78/39.81 % (3842739)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 280.78/39.81 % (3842739)CaDiCaL version: 2.1.3 % 280.78/39.81 % (3842739)Termination reason: Inappropriate % 280.78/39.81 % (3842739)Time elapsed: 0.001 s % 280.78/39.81 % (3842739)Peak memory usage: 10 MB % 280.78/39.81 % (3842739)Instructions burned: 1 (million) % 280.78/39.81 % (3842739)------------------------------ % 280.78/39.81 % (3842739)------------------------------ % 280.78/39.81 % (3842741)fmb+10_1_fmbas=function:sil=32000:sas=cadical:si=on:fmbss=16:random_seed=500919999:fmbsr=2.30978:i=4348:rtra=on_2701 on theBenchmark for (2701ds/4348Mi) % 280.78/39.81 % (3842741)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 280.78/39.81 % (3842741)Terminated due to inappropriate strategy. % 280.78/39.81 % (3842741)------------------------------ % 280.78/39.81 % (3842741)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.69/42.63 % (3842741)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.69/42.63 % (3842741)CaDiCaL version: 2.1.3 % 300.69/42.63 % (3842741)Termination reason: Inappropriate % 300.69/42.63 % (3842741)Time elapsed: 0.001 s % 300.69/42.63 % (3842741)Peak memory usage: 10 MB % 300.69/42.63 % (3842741)Instructions burned: 1 (million) % 300.69/42.63 % (3842741)------------------------------ % 300.69/42.63 % (3842741)------------------------------ % 300.69/42.63 % (3842743)ott-2_1_sil=16000:si=on:newcnf=on:random_seed=1062176672:avsq=on:i=1738:avsqr=1,16:kws=inv_arity_squared:rtra=on_2701 on theBenchmark for (2701ds/1738Mi) % 300.69/42.63 % (3842743)Instruction limit reached! % 300.69/42.63 % (3842743)------------------------------ % 300.69/42.63 % (3842743)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.69/42.63 % (3842743)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.69/42.63 % (3842743)CaDiCaL version: 2.1.3 % 300.69/42.63 % (3842743)Termination reason: Instruction limit % 300.69/42.63 % (3842743)Termination phase: Saturation % 300.69/42.63 % (3842743)Time elapsed: 1.089 s % 300.69/42.63 % (3842743)Peak memory usage: 16 MB % 300.69/42.63 % (3842743)Instructions burned: 1738 (million) % 300.69/42.63 % (3842745)ott+10_1_sil=32000:tgt=ground:si=on:random_seed=2266321532:i=10228:av=off:rtra=on_2690 on theBenchmark for (2690ds/10228Mi) % 300.69/42.63 % (3842595)Instruction limit reached! % 300.69/42.63 % (3842595)------------------------------ % 300.69/42.63 % (3842595)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.69/42.63 % (3842595)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.69/42.63 % (3842595)CaDiCaL version: 2.1.3 % 300.69/42.63 % (3842595)Termination reason: Instruction limit % 300.69/42.63 % (3842595)Termination phase: Saturation % 300.69/42.63 % (3842595)Time elapsed: 1.679 s % 300.69/42.63 % (3842595)Peak memory usage: 26 MB % 300.69/42.63 % (3842595)Instructions burned: 2944 (million) % 300.69/42.63 % (3842747)fmb+10_1_sil=64000:sas=cadical:si=on:bce=on:rp=on:random_seed=1499518310:i=108564:rtra=on_2689 on theBenchmark for (2689ds/108564Mi) % 300.69/42.63 % (3842747)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 300.69/42.63 % (3842747)Terminated due to inappropriate strategy. % 300.69/42.63 % (3842747)------------------------------ % 300.69/42.63 % (3842747)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.69/42.63 % (3842747)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.69/42.63 % (3842747)CaDiCaL version: 2.1.3 % 300.69/42.63 % (3842747)Termination reason: Inappropriate % 300.69/42.63 % (3842747)Time elapsed: 0.001 s % 300.69/42.63 % (3842747)Peak memory usage: 10 MB % 300.69/42.63 % (3842747)Instructions burned: 1 (million) % 300.69/42.63 % (3842747)------------------------------ % 300.69/42.63 % (3842747)------------------------------ % 300.69/42.63 % (3842749)dis-11_1_sil=16000:si=on:sp=reverse_frequency:alpa=true:random_seed=1826780535:i=7024:aac=none:rtra=on_2689 on theBenchmark for (2689ds/7024Mi) % 300.69/42.63 % (3842749)Instruction limit reached! % 300.69/42.63 % (3842749)------------------------------ % 300.69/42.63 % (3842749)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.69/42.63 % (3842749)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.69/42.63 % (3842749)CaDiCaL version: 2.1.3 % 300.69/42.63 % (3842749)Termination reason: Instruction limit % 300.69/42.63 % (3842749)Termination phase: Saturation % 300.69/42.63 % (3842749)Time elapsed: 4.039 s % 300.69/42.63 % (3842749)Peak memory usage: 49 MB % 300.69/42.63 % (3842749)Instructions burned: 7024 (million) % 300.69/42.63 % (3842753)dis+21_1_sil=32000:sas=cadical:si=on:random_seed=675605376:i=7546:rtra=on:amm=off_2648 on theBenchmark for (2648ds/7546Mi) % 300.69/42.63 % (3841730)Instruction limit reached! % 300.69/42.63 % (3841730)------------------------------ % 300.69/42.63 % (3841730)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.69/42.63 % (3841730)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.69/42.63 % (3841730)CaDiCaL version: 2.1.3 % 300.69/42.63 % (3841730)Termination reason: Instruction limit % 300.69/42.63 % (3841730)Termination phase: Saturation % 300.69/42.63 % (3841730)Time elapsed: 36.803 s % 300.69/42.63 % (3841730)Peak memory usage: 453 MB % 300.69/42.63 % (3841730)Instructions burned: 88026 (million) % 300.69/42.63 % (3842755)ott+11_1_sil=16000:si=on:gs=on:random_seed=2227596501:s2a=on:i=4502:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:rtra=on:fsd=on_2631 on theBen % 300.69/42.64 Terminated % 300.69/42.64 % Vampire exiting % 300.69/42.64 Terminated %------------------------------------------------------------------------------