%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWW016_1 : TPTP v9.3.1. Released v5.0.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % Computer : n010.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:38:18 PM UTC 2026 % Result : Timeout 300.09s 42.54s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : SWW016_1 : TPTP v9.3.1. Released v5.0.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.11/0.17 % Computer : n010.cluster.edu % 0.11/0.17 % Model : x86_64 x86_64 % 0.11/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.17 % Memory : 8046.5625MB % 0.11/0.17 % OS : Linux 6.8.0-71-generic % 0.11/0.17 % CPULimit : 300 % 0.11/0.17 % WCLimit : 300 % 0.11/0.17 % DateTime : Mon Sep 28 13:09:17 UTC 2026 % 0.11/0.17 % CPUTime : % 0.11/0.17 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.11/0.20 Running first-order model finding % 0.11/0.20 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.69/0.83 % (1910298)Will run a generic schedule for satisfiability detection. % 3.69/0.83 % (1910304)% WARNING: option uhcvi not known. % 3.69/0.83 % (1910304)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1828428715:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 3.69/0.83 % (1910306)dis+10_1_sil=32000:sp=arity:random_seed=2564395167:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 3.69/0.83 % (1910305)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3666931323:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 3.69/0.83 % (1910307)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2187760861:i=116_2999 on theBenchmark for (2999ds/116Mi) % 3.69/0.83 % (1910308)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=4225234800:i=131_2999 on theBenchmark for (2999ds/131Mi) % 3.69/0.83 % (1910309)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1900101846:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 3.69/0.83 % (1910303)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=4278398441_2999 on theBenchmark for (2999ds/0Mi) % 3.69/0.83 % (1910303)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.69/0.83 % (1910303)Terminated due to inappropriate strategy. % 3.69/0.83 % (1910303)------------------------------ % 3.69/0.83 % (1910303)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.69/0.83 % (1910303)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.69/0.83 % (1910303)CaDiCaL version: 2.1.3 % 3.69/0.83 % (1910303)Termination reason: Inappropriate % 3.69/0.83 % (1910303)Time elapsed: 0.016 s % 3.69/0.83 % (1910303)Peak memory usage: 13 MB % 3.69/0.83 % (1910303)Instructions burned: 70 (million) % 3.69/0.83 % (1910303)------------------------------ % 3.69/0.83 % (1910303)------------------------------ % 3.69/0.83 % (1910317)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=459333584:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 3.69/0.83 % (1910306)Instruction limit reached! % 3.69/0.83 % (1910306)------------------------------ % 3.69/0.83 % (1910306)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.69/0.83 % (1910306)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.69/0.83 % (1910306)CaDiCaL version: 2.1.3 % 3.69/0.83 % (1910306)Termination reason: Instruction limit % 3.69/0.83 % (1910306)Termination phase: Saturation % 3.69/0.83 % (1910306)Time elapsed: 0.047 s % 3.69/0.83 % (1910306)Peak memory usage: 14 MB % 3.69/0.83 % (1910306)Instructions burned: 103 (million) % 3.69/0.83 % (1910317)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.69/0.83 % (1910317)Terminated due to inappropriate strategy. % 3.69/0.83 % (1910317)------------------------------ % 3.69/0.83 % (1910317)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.69/0.83 % (1910317)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.69/0.83 % (1910317)CaDiCaL version: 2.1.3 % 3.69/0.83 % (1910317)Termination reason: Inappropriate % 3.69/0.83 % (1910317)Time elapsed: 0.016 s % 3.69/0.83 % (1910317)Peak memory usage: 13 MB % 3.69/0.83 % (1910317)Instructions burned: 69 (million) % 3.69/0.83 % (1910317)------------------------------ % 3.69/0.83 % (1910317)------------------------------ % 3.69/0.83 % (1910307)Instruction limit reached! % 3.69/0.83 % (1910307)------------------------------ % 3.69/0.83 % (1910307)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.69/0.83 % (1910307)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.69/0.83 % (1910307)CaDiCaL version: 2.1.3 % 3.69/0.83 % (1910307)Termination reason: Instruction limit % 3.69/0.83 % (1910307)Termination phase: Saturation % 3.69/0.83 % (1910307)Time elapsed: 0.052 s % 3.69/0.83 % (1910307)Peak memory usage: 15 MB % 3.69/0.83 % (1910307)Instructions burned: 118 (million) % 3.69/0.83 % (1910308)Instruction limit reached! % 3.69/0.83 % (1910308)------------------------------ % 3.69/0.83 % (1910308)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.69/0.83 % (1910308)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.69/0.83 % (1910308)CaDiCaL version: 2.1.3 % 3.69/0.83 % (1910308)Termination reason: Instruction limit % 3.69/0.83 % (1910308)Termination phase: Saturation % 3.69/0.83 % (1910308)Time elapsed: 0.055 s % 3.69/0.83 % (1910308)Peak memory usage: 14 MB % 3.69/0.83 % (1910308)Instructions burned: 132 (million) % 4.20/0.98 % (1910320)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=1310924365:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi) % 4.20/0.98 % (1910319)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3066458239:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 4.20/0.98 % (1910309)Instruction limit reached! % 4.20/0.98 % (1910309)------------------------------ % 4.20/0.98 % (1910309)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 4.20/0.98 % (1910309)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.20/0.98 % (1910309)CaDiCaL version: 2.1.3 % 4.20/0.98 % (1910309)Termination reason: Instruction limit % 4.20/0.98 % (1910309)Termination phase: Saturation % 4.20/0.98 % (1910309)Time elapsed: 0.067 s % 4.20/0.98 % (1910309)Peak memory usage: 15 MB % 4.20/0.98 % (1910309)Instructions burned: 160 (million) % 4.20/0.98 % (1910321)ott-21_1_sil=16000:fs=off:random_seed=2647658434:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi) % 4.20/0.98 % (1910322)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=4003249736:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 4.20/0.98 % (1910325)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1095054408:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 4.20/0.98 % (1910325)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 4.20/0.98 % (1910325)Terminated due to inappropriate strategy. % 4.20/0.98 % (1910325)------------------------------ % 4.20/0.98 % (1910325)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 4.20/0.98 % (1910325)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.20/0.98 % (1910325)CaDiCaL version: 2.1.3 % 4.20/0.98 % (1910325)Termination reason: Inappropriate % 4.20/0.98 % (1910325)Time elapsed: 0.030 s % 4.20/0.98 % (1910325)Peak memory usage: 13 MB % 4.20/0.98 % (1910325)Instructions burned: 69 (million) % 4.20/0.98 % (1910325)------------------------------ % 4.20/0.98 % (1910325)------------------------------ % 4.20/0.98 % (1910319)Instruction limit reached! % 4.20/0.98 % (1910319)------------------------------ % 4.20/0.98 % (1910319)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 4.20/0.98 % (1910319)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.20/0.98 % (1910319)CaDiCaL version: 2.1.3 % 4.20/0.98 % (1910319)Termination reason: Instruction limit % 4.20/0.98 % (1910319)Termination phase: Saturation % 4.20/0.98 % (1910319)Time elapsed: 0.055 s % 4.20/0.98 % (1910319)Peak memory usage: 14 MB % 4.20/0.98 % (1910319)Instructions burned: 133 (million) % 4.20/0.98 % (1910329)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=4010332392:i=1179_2998 on theBenchmark for (2998ds/1179Mi) % 4.20/0.98 % (1910330)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1930825468:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi) % 4.20/0.98 % (1910321)Instruction limit reached! % 4.20/0.98 % (1910321)------------------------------ % 4.20/0.98 % (1910321)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 4.20/0.98 % (1910321)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.20/0.98 % (1910321)CaDiCaL version: 2.1.3 % 4.20/0.98 % (1910321)Termination reason: Instruction limit % 4.20/0.98 % (1910321)Termination phase: Saturation % 4.20/0.98 % (1910321)Time elapsed: 0.082 s % 4.20/0.98 % (1910321)Peak memory usage: 14 MB % 4.20/0.98 % (1910321)Instructions burned: 181 (million) % 4.20/0.98 % (1910333)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=2757318407: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) % 4.20/0.98 % (1910330)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 4.20/0.98 % (1910330)Terminated due to inappropriate strategy. % 4.20/0.98 % (1910330)------------------------------ % 4.20/0.98 % (1910330)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 4.20/0.98 % (1910330)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.20/0.98 % (1910330)CaDiCaL version: 2.1.3 % 4.20/0.98 % (1910330)Termination reason: Inappropriate % 4.20/0.98 % (1910330)Time elapsed: 0.042 s % 4.20/0.98 % (1910330)Peak memory usage: 14 MB % 18.25/2.84 % (1910330)Instructions burned: 97 (million) % 18.25/2.84 % (1910330)------------------------------ % 18.25/2.84 % (1910330)------------------------------ % 18.25/2.84 % (1910335)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2355776929:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi) % 18.25/2.84 % (1910320)Instruction limit reached! % 18.25/2.84 % (1910320)------------------------------ % 18.25/2.84 % (1910320)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 18.25/2.84 % (1910320)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.25/2.84 % (1910320)CaDiCaL version: 2.1.3 % 18.25/2.84 % (1910320)Termination reason: Instruction limit % 18.25/2.84 % (1910320)Termination phase: Saturation % 18.25/2.84 % (1910320)Time elapsed: 0.177 s % 18.25/2.84 % (1910320)Peak memory usage: 19 MB % 18.25/2.84 % (1910320)Instructions burned: 689 (million) % 18.25/2.84 % (1910337)fmb+10_1_sil=64000:random_seed=2985259166:i=22061:nm=2:gsp=on_2997 on theBenchmark for (2997ds/22061Mi) % 18.25/2.84 % (1910337)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 18.25/2.84 % (1910337)Terminated due to inappropriate strategy. % 18.25/2.84 % (1910337)------------------------------ % 18.25/2.84 % (1910337)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 18.25/2.84 % (1910337)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.25/2.84 % (1910337)CaDiCaL version: 2.1.3 % 18.25/2.84 % (1910337)Termination reason: Inappropriate % 18.25/2.84 % (1910337)Time elapsed: 0.017 s % 18.25/2.84 % (1910337)Peak memory usage: 13 MB % 18.25/2.84 % (1910337)Instructions burned: 76 (million) % 18.25/2.84 % (1910337)------------------------------ % 18.25/2.84 % (1910337)------------------------------ % 18.25/2.84 % (1910339)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2564505742:i=9515:nm=5_2996 on theBenchmark for (2996ds/9515Mi) % 18.25/2.84 % (1910339)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 18.25/2.84 % (1910339)Terminated due to inappropriate strategy. % 18.25/2.84 % (1910339)------------------------------ % 18.25/2.84 % (1910339)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 18.25/2.84 % (1910339)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.25/2.84 % (1910339)CaDiCaL version: 2.1.3 % 18.25/2.84 % (1910339)Termination reason: Inappropriate % 18.25/2.84 % (1910339)Time elapsed: 0.015 s % 18.25/2.84 % (1910339)Peak memory usage: 13 MB % 18.25/2.84 % (1910339)Instructions burned: 69 (million) % 18.25/2.84 % (1910339)------------------------------ % 18.25/2.84 % (1910339)------------------------------ % 18.25/2.84 % (1910341)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3617453316:fmbsr=1.7:i=920_2996 on theBenchmark for (2996ds/920Mi) % 18.25/2.84 % (1910322)Instruction limit reached! % 18.25/2.84 % (1910322)------------------------------ % 18.25/2.84 % (1910322)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 18.25/2.84 % (1910322)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.25/2.84 % (1910322)CaDiCaL version: 2.1.3 % 18.25/2.84 % (1910322)Termination reason: Instruction limit % 18.25/2.84 % (1910322)Termination phase: Saturation % 18.25/2.84 % (1910322)Time elapsed: 0.241 s % 18.25/2.84 % (1910322)Peak memory usage: 15 MB % 18.25/2.84 % (1910322)Instructions burned: 477 (million) % 18.25/2.84 % (1910341)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 18.25/2.84 % (1910341)Terminated due to inappropriate strategy. % 18.25/2.84 % (1910341)------------------------------ % 18.25/2.84 % (1910341)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 18.25/2.84 % (1910341)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.25/2.84 % (1910341)CaDiCaL version: 2.1.3 % 18.25/2.84 % (1910341)Termination reason: Inappropriate % 18.25/2.84 % (1910341)Time elapsed: 0.015 s % 18.25/2.84 % (1910341)Peak memory usage: 13 MB % 18.25/2.84 % (1910341)Instructions burned: 69 (million) % 18.25/2.84 % (1910341)------------------------------ % 18.25/2.84 % (1910341)------------------------------ % 18.25/2.84 % (1910344)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3867730856:i=1472:ins=7:fdi=8:gsp=on_2996 on theBenchmark for (2996ds/1472Mi) % 18.25/2.84 % (1910343)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2556630353:i=5131_2996 on theBenchmark for (2996ds/5131Mi) % 18.25/2.84 % (1910333)Instruction limit reached! % 18.25/2.84 % (1910333)------------------------------ % 21.68/3.31 % (1910333)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 21.68/3.31 % (1910333)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.68/3.31 % (1910333)CaDiCaL version: 2.1.3 % 21.68/3.31 % (1910333)Termination reason: Instruction limit % 21.68/3.31 % (1910333)Termination phase: Saturation % 21.68/3.31 % (1910333)Time elapsed: 0.408 s % 21.68/3.31 % (1910333)Peak memory usage: 21 MB % 21.68/3.31 % (1910333)Instructions burned: 693 (million) % 21.68/3.31 % (1910347)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=1852963668:i=6324_2993 on theBenchmark for (2993ds/6324Mi) % 21.68/3.31 % (1910347)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 21.68/3.31 % (1910347)Terminated due to inappropriate strategy. % 21.68/3.31 % (1910347)------------------------------ % 21.68/3.31 % (1910347)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 21.68/3.31 % (1910347)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.68/3.31 % (1910347)CaDiCaL version: 2.1.3 % 21.68/3.31 % (1910347)Termination reason: Inappropriate % 21.68/3.31 % (1910347)Time elapsed: 0.030 s % 21.68/3.31 % (1910347)Peak memory usage: 13 MB % 21.68/3.31 % (1910347)Instructions burned: 70 (million) % 21.68/3.31 % (1910347)------------------------------ % 21.68/3.31 % (1910347)------------------------------ % 21.68/3.31 % (1910349)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1021909951:fmbsr=2.30978:i=2174_2993 on theBenchmark for (2993ds/2174Mi) % 21.68/3.31 % (1910344)Instruction limit reached! % 21.68/3.31 % (1910344)------------------------------ % 21.68/3.31 % (1910344)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 21.68/3.31 % (1910344)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.68/3.31 % (1910344)CaDiCaL version: 2.1.3 % 21.68/3.31 % (1910344)Termination reason: Instruction limit % 21.68/3.31 % (1910344)Termination phase: Saturation % 21.68/3.31 % (1910344)Time elapsed: 0.325 s % 21.68/3.31 % (1910344)Peak memory usage: 19 MB % 21.68/3.31 % (1910344)Instructions burned: 1476 (million) % 21.68/3.31 % (1910351)ott-2_1_sil=16000:newcnf=on:random_seed=3946093916:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2992 on theBenchmark for (2992ds/869Mi) % 21.68/3.31 % (1910335)Instruction limit reached! % 21.68/3.31 % (1910335)------------------------------ % 21.68/3.31 % (1910335)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 21.68/3.31 % (1910335)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.68/3.31 % (1910335)CaDiCaL version: 2.1.3 % 21.68/3.31 % (1910335)Termination reason: Instruction limit % 21.68/3.31 % (1910335)Termination phase: Saturation % 21.68/3.31 % (1910335)Time elapsed: 0.476 s % 21.68/3.31 % (1910335)Peak memory usage: 20 MB % 21.68/3.31 % (1910335)Instructions burned: 880 (million) % 21.68/3.31 % (1910349)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 21.68/3.31 % (1910349)Terminated due to inappropriate strategy. % 21.68/3.31 % (1910349)------------------------------ % 21.68/3.31 % (1910349)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 21.68/3.31 % (1910349)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.68/3.31 % (1910349)CaDiCaL version: 2.1.3 % 21.68/3.31 % (1910349)Termination reason: Inappropriate % 21.68/3.31 % (1910349)Time elapsed: 0.029 s % 21.68/3.31 % (1910349)Peak memory usage: 13 MB % 21.68/3.31 % (1910349)Instructions burned: 69 (million) % 21.68/3.31 % (1910349)------------------------------ % 21.68/3.31 % (1910349)------------------------------ % 21.68/3.31 % (1910353)ott+10_1_sil=32000:tgt=ground:random_seed=1632232093:i=5114:av=off_2992 on theBenchmark for (2992ds/5114Mi) % 21.68/3.31 % (1910354)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2191357017:i=54282_2992 on theBenchmark for (2992ds/54282Mi) % 21.68/3.31 % (1910354)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 21.68/3.31 % (1910354)Terminated due to inappropriate strategy. % 21.68/3.31 % (1910354)------------------------------ % 21.68/3.31 % (1910354)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 21.68/3.31 % (1910354)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.68/3.31 % (1910354)CaDiCaL version: 2.1.3 % 21.68/3.31 % (1910354)Termination reason: Inappropriate % 21.68/3.31 % (1910354)Time elapsed: 0.029 s % 21.68/3.31 % (1910354)Peak memory usage: 13 MB % 21.68/3.31 % (1910354)Instructions burned: 70 (million) % 90.94/13.11 % (1910354)------------------------------ % 90.94/13.11 % (1910354)------------------------------ % 90.94/13.11 % (1910357)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3025549149:i=3512:aac=none_2992 on theBenchmark for (2992ds/3512Mi) % 90.94/13.11 % (1910329)Instruction limit reached! % 90.94/13.11 % (1910329)------------------------------ % 90.94/13.11 % (1910329)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 90.94/13.11 % (1910329)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 90.94/13.11 % (1910329)CaDiCaL version: 2.1.3 % 90.94/13.11 % (1910329)Termination reason: Instruction limit % 90.94/13.11 % (1910329)Termination phase: Saturation % 90.94/13.11 % (1910329)Time elapsed: 0.616 s % 90.94/13.11 % (1910329)Peak memory usage: 20 MB % 90.94/13.11 % (1910329)Instructions burned: 1179 (million) % 90.94/13.11 % (1910359)dis+21_1_sil=32000:sas=cadical:random_seed=1083619135:i=3773:amm=off_2991 on theBenchmark for (2991ds/3773Mi) % 90.94/13.11 % (1910351)Instruction limit reached! % 90.94/13.11 % (1910351)------------------------------ % 90.94/13.11 % (1910351)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 90.94/13.11 % (1910351)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 90.94/13.11 % (1910351)CaDiCaL version: 2.1.3 % 90.94/13.11 % (1910351)Termination reason: Instruction limit % 90.94/13.11 % (1910351)Termination phase: Saturation % 90.94/13.11 % (1910351)Time elapsed: 0.252 s % 90.94/13.11 % (1910351)Peak memory usage: 19 MB % 90.94/13.11 % (1910351)Instructions burned: 870 (million) % 90.94/13.11 % (1910361)ott+11_1_sil=16000:gs=on:random_seed=1941816388:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2990 on theBenchmark for (2990ds/2251Mi) % 90.94/13.11 % (1910361)Instruction limit reached! % 90.94/13.11 % (1910361)------------------------------ % 90.94/13.11 % (1910361)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 90.94/13.11 % (1910361)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 90.94/13.11 % (1910361)CaDiCaL version: 2.1.3 % 90.94/13.11 % (1910361)Termination reason: Instruction limit % 90.94/13.11 % (1910361)Termination phase: Saturation % 90.94/13.11 % (1910361)Time elapsed: 0.505 s % 90.94/13.11 % (1910361)Peak memory usage: 21 MB % 90.94/13.11 % (1910361)Instructions burned: 2252 (million) % 90.94/13.11 % (1910363)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=4140776081:fmbsr=1.6:i=67534_2985 on theBenchmark for (2985ds/67534Mi) % 90.94/13.11 % (1910363)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 90.94/13.11 % (1910363)Terminated due to inappropriate strategy. % 90.94/13.11 % (1910363)------------------------------ % 90.94/13.11 % (1910363)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 90.94/13.11 % (1910363)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 90.94/13.11 % (1910363)CaDiCaL version: 2.1.3 % 90.94/13.11 % (1910363)Termination reason: Inappropriate % 90.94/13.11 % (1910363)Time elapsed: 0.020 s % 90.94/13.11 % (1910363)Peak memory usage: 13 MB % 90.94/13.11 % (1910363)Instructions burned: 94 (million) % 90.94/13.11 % (1910363)------------------------------ % 90.94/13.11 % (1910363)------------------------------ % 90.94/13.11 % (1910365)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=3310683701:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2984 on theBenchmark for (2984ds/4591Mi) % 90.94/13.11 % (1910359)Instruction limit reached! % 90.94/13.11 % (1910359)------------------------------ % 90.94/13.11 % (1910359)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 90.94/13.11 % (1910359)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 90.94/13.11 % (1910359)CaDiCaL version: 2.1.3 % 90.94/13.11 % (1910359)Termination reason: Instruction limit % 90.94/13.11 % (1910359)Termination phase: Saturation % 90.94/13.11 % (1910359)Time elapsed: 1.685 s % 90.94/13.11 % (1910359)Peak memory usage: 21 MB % 90.94/13.11 % (1910359)Instructions burned: 3774 (million) % 90.94/13.11 % (1910367)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=4207563054:i=29340_2974 on theBenchmark for (2974ds/29340Mi) % 90.94/13.11 % (1910357)Instruction limit reached! % 90.94/13.11 % (1910357)------------------------------ % 90.94/13.11 % (1910357)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 90.94/13.11 % (1910357)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 90.94/13.11 % (1910357)CaDiCaL version: 2.1.3 % 90.94/13.11 % (1910357)Termination reason: Instruction limit % 115.80/16.66 % (1910357)Termination phase: Saturation % 115.80/16.66 % (1910357)Time elapsed: 1.834 s % 115.80/16.66 % (1910357)Peak memory usage: 31 MB % 115.80/16.66 % (1910357)Instructions burned: 3513 (million) % 115.80/16.66 % (1910369)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=953687404:i=5211_2973 on theBenchmark for (2973ds/5211Mi) % 115.80/16.66 % (1910365)Instruction limit reached! % 115.80/16.66 % (1910365)------------------------------ % 115.80/16.66 % (1910365)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 115.80/16.66 % (1910365)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 115.80/16.66 % (1910365)CaDiCaL version: 2.1.3 % 115.80/16.66 % (1910365)Termination reason: Instruction limit % 115.80/16.66 % (1910365)Termination phase: Saturation % 115.80/16.66 % (1910365)Time elapsed: 1.272 s % 115.80/16.66 % (1910365)Peak memory usage: 49 MB % 115.80/16.66 % (1910365)Instructions burned: 4594 (million) % 115.80/16.66 % (1910371)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=1056784075:i=5497:nm=2_2971 on theBenchmark for (2971ds/5497Mi) % 115.80/16.66 % (1910371)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 115.80/16.66 % (1910371)Terminated due to inappropriate strategy. % 115.80/16.66 % (1910371)------------------------------ % 115.80/16.66 % (1910371)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 115.80/16.66 % (1910371)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 115.80/16.66 % (1910371)CaDiCaL version: 2.1.3 % 115.80/16.66 % (1910371)Termination reason: Inappropriate % 115.80/16.66 % (1910371)Time elapsed: 0.016 s % 115.80/16.66 % (1910371)Peak memory usage: 13 MB % 115.80/16.66 % (1910371)Instructions burned: 70 (million) % 115.80/16.66 % (1910371)------------------------------ % 115.80/16.66 % (1910371)------------------------------ % 115.80/16.66 % (1910373)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=3665010382:fmbsr=2:i=46332_2971 on theBenchmark for (2971ds/46332Mi) % 115.80/16.66 % (1910373)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 115.80/16.66 % (1910373)Terminated due to inappropriate strategy. % 115.80/16.66 % (1910373)------------------------------ % 115.80/16.66 % (1910373)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 115.80/16.66 % (1910373)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 115.80/16.66 % (1910373)CaDiCaL version: 2.1.3 % 115.80/16.66 % (1910373)Termination reason: Inappropriate % 115.80/16.66 % (1910373)Time elapsed: 0.021 s % 115.80/16.66 % (1910373)Peak memory usage: 13 MB % 115.80/16.66 % (1910373)Instructions burned: 97 (million) % 115.80/16.66 % (1910373)------------------------------ % 115.80/16.66 % (1910373)------------------------------ % 115.80/16.66 % (1910375)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=1619417927:i=14071_2971 on theBenchmark for (2971ds/14071Mi) % 115.80/16.66 % (1910375)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 115.80/16.66 % (1910375)Terminated due to inappropriate strategy. % 115.80/16.66 % (1910375)------------------------------ % 115.80/16.66 % (1910375)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 115.80/16.66 % (1910375)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 115.80/16.66 % (1910375)CaDiCaL version: 2.1.3 % 115.80/16.66 % (1910375)Termination reason: Inappropriate % 115.80/16.66 % (1910375)Time elapsed: 0.021 s % 115.80/16.66 % (1910375)Peak memory usage: 13 MB % 115.80/16.66 % (1910375)Instructions burned: 97 (million) % 115.80/16.66 % (1910375)------------------------------ % 115.80/16.66 % (1910375)------------------------------ % 115.80/16.66 % (1910377)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=419598331:i=22565:add=on:rawr=on_2970 on theBenchmark for (2970ds/22565Mi) % 115.80/16.66 % (1910343)Instruction limit reached! % 115.80/16.66 % (1910343)------------------------------ % 115.80/16.66 % (1910343)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 115.80/16.66 % (1910343)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 115.80/16.66 % (1910343)CaDiCaL version: 2.1.3 % 115.80/16.66 % (1910343)Termination reason: Instruction limit % 115.80/16.66 % (1910343)Termination phase: Saturation % 115.80/16.66 % (1910343)Time elapsed: 2.704 s % 115.80/16.66 % (1910343)Peak memory usage: 43 MB % 115.80/16.66 % (1910343)Instructions burned: 5133 (million) % 115.80/16.66 % (1910379)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=1125077755:i=8173:av=off_2969 on theBenchmark for (2969ds/8173Mi) % 116.96/16.83 % (1910353)Instruction limit reached! % 116.96/16.83 % (1910353)------------------------------ % 116.96/16.83 % (1910353)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 116.96/16.83 % (1910353)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 116.96/16.83 % (1910353)CaDiCaL version: 2.1.3 % 116.96/16.83 % (1910353)Termination reason: Instruction limit % 116.96/16.83 % (1910353)Termination phase: Saturation % 116.96/16.83 % (1910353)Time elapsed: 3.029 s % 116.96/16.83 % (1910353)Peak memory usage: 32 MB % 116.96/16.83 % (1910353)Instructions burned: 5115 (million) % 116.96/16.83 % (1910381)dis+10_16:1_sil=16000:random_seed=584391174:i=9155:fsr=off_2962 on theBenchmark for (2962ds/9155Mi) % 116.96/16.83 % (1910369)Instruction limit reached! % 116.96/16.83 % (1910369)------------------------------ % 116.96/16.83 % (1910369)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 116.96/16.83 % (1910369)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 116.96/16.83 % (1910369)CaDiCaL version: 2.1.3 % 116.96/16.83 % (1910369)Termination reason: Instruction limit % 116.96/16.83 % (1910369)Termination phase: Saturation % 116.96/16.83 % (1910369)Time elapsed: 2.724 s % 116.96/16.83 % (1910369)Peak memory usage: 46 MB % 116.96/16.83 % (1910369)Instructions burned: 5213 (million) % 116.96/16.83 % (1910383)ott-3_8_sil=64000:random_seed=2515737228:i=20139:bs=on_2946 on theBenchmark for (2946ds/20139Mi) % 116.96/16.83 % (1910379)Instruction limit reached! % 116.96/16.83 % (1910379)------------------------------ % 116.96/16.83 % (1910379)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 116.96/16.83 % (1910379)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 116.96/16.83 % (1910379)CaDiCaL version: 2.1.3 % 116.96/16.83 % (1910379)Termination reason: Instruction limit % 116.96/16.83 % (1910379)Termination phase: Saturation % 116.96/16.83 % (1910379)Time elapsed: 3.622 s % 116.96/16.83 % (1910379)Peak memory usage: 32 MB % 116.96/16.83 % (1910379)Instructions burned: 8175 (million) % 116.96/16.83 % (1910385)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=335469947:fmbsr=2:i=32576_2932 on theBenchmark for (2932ds/32576Mi) % 116.96/16.83 % (1910385)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 116.96/16.83 % (1910385)Terminated due to inappropriate strategy. % 116.96/16.83 % (1910385)------------------------------ % 116.96/16.83 % (1910385)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 116.96/16.83 % (1910385)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 116.96/16.83 % (1910385)CaDiCaL version: 2.1.3 % 116.96/16.83 % (1910385)Termination reason: Inappropriate % 116.96/16.83 % (1910385)Time elapsed: 0.039 s % 116.96/16.83 % (1910385)Peak memory usage: 13 MB % 116.96/16.83 % (1910385)Instructions burned: 94 (million) % 116.96/16.83 % (1910385)------------------------------ % 116.96/16.83 % (1910385)------------------------------ % 116.96/16.83 % (1910387)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=2328919560:i=11404_2932 on theBenchmark for (2932ds/11404Mi) % 116.96/16.83 % (1910377)Instruction limit reached! % 116.96/16.83 % (1910377)------------------------------ % 116.96/16.83 % (1910377)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 116.96/16.83 % (1910377)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 116.96/16.83 % (1910377)CaDiCaL version: 2.1.3 % 116.96/16.83 % (1910377)Termination reason: Instruction limit % 116.96/16.83 % (1910377)Termination phase: Saturation % 116.96/16.83 % (1910377)Time elapsed: 5.023 s % 116.96/16.83 % (1910377)Peak memory usage: 25 MB % 116.96/16.83 % (1910377)Instructions burned: 22567 (million) % 116.96/16.83 % (1910389)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=1659107995:i=14134_2920 on theBenchmark for (2920ds/14134Mi) % 116.96/16.83 % (1910381)Instruction limit reached! % 116.96/16.83 % (1910381)------------------------------ % 116.96/16.83 % (1910381)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 116.96/16.83 % (1910381)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 116.96/16.83 % (1910381)CaDiCaL version: 2.1.3 % 116.96/16.83 % (1910381)Termination reason: Instruction limit % 116.96/16.83 % (1910381)Termination phase: Saturation % 116.96/16.83 % (1910381)Time elapsed: 4.715 s % 116.96/16.83 % (1910381)Peak memory usage: 55 MB % 116.96/16.83 % (1910381)Instructions burned: 9155 (million) % 116.96/16.83 % (1910391)dis+33_16_sil=32000:sac=on:random_seed=1447833355:i=15851:nm=0_2914 on theBenchmark for (2914ds/15851Mi) % 116.96/16.83 % (1910389)Instruction limit reached! % 116.96/16.83 % (1910389)------------------------------ % 116.96/16.83 % (1910389)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 131.80/18.84 % (1910389)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 131.80/18.84 % (1910389)CaDiCaL version: 2.1.3 % 131.80/18.84 % (1910389)Termination reason: Instruction limit % 131.80/18.84 % (1910389)Termination phase: Saturation % 131.80/18.84 % (1910389)Time elapsed: 4.953 s % 131.80/18.84 % (1910389)Peak memory usage: 53 MB % 131.80/18.84 % (1910389)Instructions burned: 14134 (million) % 131.80/18.84 % (1910393)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=1417395124:avsq=on:i=17627:add=on:amm=off_2870 on theBenchmark for (2870ds/17627Mi) % 131.80/18.84 % (1910387)Instruction limit reached! % 131.80/18.84 % (1910387)------------------------------ % 131.80/18.84 % (1910387)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 131.80/18.84 % (1910387)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 131.80/18.84 % (1910387)CaDiCaL version: 2.1.3 % 131.80/18.84 % (1910387)Termination reason: Instruction limit % 131.80/18.84 % (1910387)Termination phase: Saturation % 131.80/18.84 % (1910387)Time elapsed: 7.436 s % 131.80/18.84 % (1910387)Peak memory usage: 48 MB % 131.80/18.84 % (1910387)Instructions burned: 11405 (million) % 131.80/18.84 % (1910395)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=4011512686:s2a=on:i=53295_2857 on theBenchmark for (2857ds/53295Mi) % 131.80/18.84 % (1910391)Instruction limit reached! % 131.80/18.84 % (1910391)------------------------------ % 131.80/18.84 % (1910391)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 131.80/18.84 % (1910391)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 131.80/18.84 % (1910391)CaDiCaL version: 2.1.3 % 131.80/18.84 % (1910391)Termination reason: Instruction limit % 131.80/18.84 % (1910391)Termination phase: Saturation % 131.80/18.84 % (1910391)Time elapsed: 7.296 s % 131.80/18.84 % (1910391)Peak memory usage: 35 MB % 131.80/18.84 % (1910391)Instructions burned: 15851 (million) % 131.80/18.84 % (1910397)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=2327825374:i=26857:ins=20_2841 on theBenchmark for (2841ds/26857Mi) % 131.80/18.84 % (1910397)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 131.80/18.84 % (1910397)Terminated due to inappropriate strategy. % 131.80/18.84 % (1910397)------------------------------ % 131.80/18.84 % (1910397)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 131.80/18.84 % (1910397)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 131.80/18.84 % (1910397)CaDiCaL version: 2.1.3 % 131.80/18.84 % (1910397)Termination reason: Inappropriate % 131.80/18.84 % (1910397)Time elapsed: 0.030 s % 131.80/18.84 % (1910397)Peak memory usage: 13 MB % 131.80/18.84 % (1910397)Instructions burned: 70 (million) % 131.80/18.84 % (1910397)------------------------------ % 131.80/18.84 % (1910397)------------------------------ % 131.80/18.84 % (1910399)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=1345847587:i=28120:bs=on:fsr=off_2841 on theBenchmark for (2841ds/28120Mi) % 131.80/18.84 % (1910367)Instruction limit reached! % 131.80/18.84 % (1910367)------------------------------ % 131.80/18.84 % (1910367)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 131.80/18.84 % (1910367)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 131.80/18.84 % (1910367)CaDiCaL version: 2.1.3 % 131.80/18.84 % (1910367)Termination reason: Instruction limit % 131.80/18.84 % (1910367)Termination phase: Saturation % 131.80/18.84 % (1910367)Time elapsed: 13.871 s % 131.80/18.84 % (1910367)Peak memory usage: 47 MB % 131.80/18.84 % (1910367)Instructions burned: 29342 (million) % 131.80/18.84 % (1910401)fmb+10_1_sil=256000:fmbss=7:random_seed=1285514499:fmbsr=1.6:i=182295_2835 on theBenchmark for (2835ds/182295Mi) % 131.80/18.84 % (1910383)Instruction limit reached! % 131.80/18.84 % (1910383)------------------------------ % 131.80/18.84 % (1910383)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 131.80/18.84 % (1910383)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 131.80/18.84 % (1910383)CaDiCaL version: 2.1.3 % 131.80/18.84 % (1910383)Termination reason: Instruction limit % 131.80/18.84 % (1910383)Termination phase: Saturation % 131.80/18.84 % (1910383)Time elapsed: 11.033 s % 131.80/18.84 % (1910383)Peak memory usage: 55 MB % 131.80/18.84 % (1910383)Instructions burned: 20140 (million) % 131.80/18.84 % (1910401)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 131.80/18.84 % (1910401)Terminated due to inappropriate strategy. % 131.80/18.84 % (1910401)------------------------------ % 138.97/19.80 % (1910401)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 138.97/19.80 % (1910401)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 138.97/19.80 % (1910401)CaDiCaL version: 2.1.3 % 138.97/19.80 % (1910401)Termination reason: Inappropriate % 138.97/19.80 % (1910401)Time elapsed: 0.030 s % 138.97/19.80 % (1910401)Peak memory usage: 13 MB % 138.97/19.80 % (1910401)Instructions burned: 69 (million) % 138.97/19.80 % (1910401)------------------------------ % 138.97/19.80 % (1910401)------------------------------ % 138.97/19.80 % (1910403)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=374629423:i=44625:gsp=on_2835 on theBenchmark for (2835ds/44625Mi) % 138.97/19.80 % (1910404)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=3687817448:i=160505_2835 on theBenchmark for (2835ds/160505Mi) % 138.97/19.80 % (1910404)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 138.97/19.80 % (1910404)Terminated due to inappropriate strategy. % 138.97/19.80 % (1910404)------------------------------ % 138.97/19.80 % (1910404)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 138.97/19.80 % (1910404)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 138.97/19.80 % (1910404)CaDiCaL version: 2.1.3 % 138.97/19.80 % (1910404)Termination reason: Inappropriate % 138.97/19.80 % (1910404)Time elapsed: 0.030 s % 138.97/19.80 % (1910404)Peak memory usage: 13 MB % 138.97/19.80 % (1910404)Instructions burned: 69 (million) % 138.97/19.80 % (1910404)------------------------------ % 138.97/19.80 % (1910404)------------------------------ % 138.97/19.80 % (1910403)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 138.97/19.80 % (1910403)Terminated due to inappropriate strategy. % 138.97/19.80 % (1910403)------------------------------ % 138.97/19.80 % (1910403)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 138.97/19.80 % (1910403)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 138.97/19.80 % (1910403)CaDiCaL version: 2.1.3 % 138.97/19.80 % (1910403)Termination reason: Inappropriate % 138.97/19.80 % (1910403)Time elapsed: 0.042 s % 138.97/19.80 % (1910403)Peak memory usage: 13 MB % 138.97/19.80 % (1910403)Instructions burned: 73 (million) % 138.97/19.80 % (1910403)------------------------------ % 138.97/19.80 % (1910403)------------------------------ % 138.97/19.80 % (1910407)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=3271346997:fmbsr=1.3:i=225729_2834 on theBenchmark for (2834ds/225729Mi) % 138.97/19.80 % (1910408)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=4162826876:fmbsr=2:i=185024:ins=7_2834 on theBenchmark for (2834ds/185024Mi) % 138.97/19.80 % (1910407)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 138.97/19.80 % (1910407)Terminated due to inappropriate strategy. % 138.97/19.80 % (1910407)------------------------------ % 138.97/19.80 % (1910407)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 138.97/19.80 % (1910407)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 138.97/19.80 % (1910407)CaDiCaL version: 2.1.3 % 138.97/19.80 % (1910407)Termination reason: Inappropriate % 138.97/19.80 % (1910407)Time elapsed: 0.040 s % 138.97/19.80 % (1910407)Peak memory usage: 13 MB % 138.97/19.80 % (1910407)Instructions burned: 97 (million) % 138.97/19.80 % (1910407)------------------------------ % 138.97/19.80 % (1910407)------------------------------ % 138.97/19.80 % (1910408)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 138.97/19.80 % (1910408)Terminated due to inappropriate strategy. % 138.97/19.80 % (1910408)------------------------------ % 138.97/19.80 % (1910408)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 138.97/19.80 % (1910408)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 138.97/19.80 % (1910408)CaDiCaL version: 2.1.3 % 138.97/19.80 % (1910408)Termination reason: Inappropriate % 138.97/19.80 % (1910408)Time elapsed: 0.040 s % 138.97/19.80 % (1910408)Peak memory usage: 13 MB % 138.97/19.80 % (1910408)Instructions burned: 97 (million) % 138.97/19.80 % (1910408)------------------------------ % 138.97/19.80 % (1910408)------------------------------ % 138.97/19.80 % (1910412)% WARNING: option uhcvi not known. % 138.97/19.80 % (1910412)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3321803882:i=271062:add=off:rtra=on:rawr=on_2834 on theBenchmark for (2834ds/271062Mi) % 138.97/19.80 % (1910411)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=224737583:rtra=on_2834 on theBenchmark for (2834ds/0Mi) % 138.97/19.80 % (1910411)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 151.24/21.68 % (1910411)Terminated due to inappropriate strategy. % 151.24/21.68 % (1910411)------------------------------ % 151.24/21.68 % (1910411)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 151.24/21.68 % (1910411)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 151.24/21.68 % (1910411)CaDiCaL version: 2.1.3 % 151.24/21.68 % (1910411)Termination reason: Inappropriate % 151.24/21.68 % (1910411)Time elapsed: 0.039 s % 151.24/21.68 % (1910411)Peak memory usage: 14 MB % 151.24/21.68 % (1910411)Instructions burned: 82 (million) % 151.24/21.68 % (1910411)------------------------------ % 151.24/21.68 % (1910411)------------------------------ % 151.24/21.68 % (1910415)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2542431164:i=176048:add=on:rtra=on:rawr=on_2833 on theBenchmark for (2833ds/176048Mi) % 151.24/21.68 % (1910393)Instruction limit reached! % 151.24/21.68 % (1910393)------------------------------ % 151.24/21.68 % (1910393)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 151.24/21.68 % (1910393)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 151.24/21.68 % (1910393)CaDiCaL version: 2.1.3 % 151.24/21.68 % (1910393)Termination reason: Instruction limit % 151.24/21.68 % (1910393)Termination phase: Saturation % 151.24/21.68 % (1910393)Time elapsed: 5.360 s % 151.24/21.68 % (1910393)Peak memory usage: 93 MB % 151.24/21.68 % (1910393)Instructions burned: 17628 (million) % 151.24/21.68 % (1910417)dis+10_1_sil=32000:si=on:sp=arity:random_seed=3338351871:i=206:fgj=on:rtra=on_2817 on theBenchmark for (2817ds/206Mi) % 151.24/21.68 % (1910417)Instruction limit reached! % 151.24/21.68 % (1910417)------------------------------ % 151.24/21.68 % (1910417)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 151.24/21.68 % (1910417)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 151.24/21.68 % (1910417)CaDiCaL version: 2.1.3 % 151.24/21.68 % (1910417)Termination reason: Instruction limit % 151.24/21.68 % (1910417)Termination phase: Saturation % 151.24/21.68 % (1910417)Time elapsed: 0.057 s % 151.24/21.68 % (1910417)Peak memory usage: 16 MB % 151.24/21.68 % (1910417)Instructions burned: 207 (million) % 151.24/21.68 % (1910419)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=2987266955:i=232:rtra=on_2816 on theBenchmark for (2816ds/232Mi) % 151.24/21.68 % (1910419)Instruction limit reached! % 151.24/21.68 % (1910419)------------------------------ % 151.24/21.68 % (1910419)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 151.24/21.68 % (1910419)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 151.24/21.68 % (1910419)CaDiCaL version: 2.1.3 % 151.24/21.68 % (1910419)Termination reason: Instruction limit % 151.24/21.68 % (1910419)Termination phase: Saturation % 151.24/21.68 % (1910419)Time elapsed: 0.064 s % 151.24/21.68 % (1910419)Peak memory usage: 15 MB % 151.24/21.68 % (1910419)Instructions burned: 234 (million) % 151.24/21.68 % (1910421)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=3600680535:i=262:rtra=on_2815 on theBenchmark for (2815ds/262Mi) % 151.24/21.68 % (1910421)Instruction limit reached! % 151.24/21.68 % (1910421)------------------------------ % 151.24/21.68 % (1910421)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 151.24/21.68 % (1910421)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 151.24/21.68 % (1910421)CaDiCaL version: 2.1.3 % 151.24/21.68 % (1910421)Termination reason: Instruction limit % 151.24/21.68 % (1910421)Termination phase: Saturation % 151.24/21.68 % (1910421)Time elapsed: 0.065 s % 151.24/21.68 % (1910421)Peak memory usage: 17 MB % 151.24/21.68 % (1910421)Instructions burned: 264 (million) % 151.24/21.68 % (1910423)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=1323144786:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2814 on theBenchmark for (2814ds/318Mi) % 151.24/21.68 % (1910423)Instruction limit reached! % 151.24/21.68 % (1910423)------------------------------ % 151.24/21.68 % (1910423)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 151.24/21.68 % (1910423)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 151.24/21.68 % (1910423)CaDiCaL version: 2.1.3 % 151.24/21.68 % (1910423)Termination reason: Instruction limit % 151.24/21.68 % (1910423)Termination phase: Saturation % 151.24/21.68 % (1910423)Time elapsed: 0.091 s % 151.24/21.68 % (1910423)Peak memory usage: 18 MB % 151.24/21.68 % (1910423)Instructions burned: 318 (million) % 151.24/21.68 % (1910425)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=2110959612:i=1428:nm=2:rtra=on_2813 on theBenchmark for (2813ds/1428Mi) % 181.58/25.81 % (1910425)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 181.58/25.81 % (1910425)Terminated due to inappropriate strategy. % 181.58/25.81 % (1910425)------------------------------ % 181.58/25.81 % (1910425)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 181.58/25.81 % (1910425)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 181.58/25.81 % (1910425)CaDiCaL version: 2.1.3 % 181.58/25.81 % (1910425)Termination reason: Inappropriate % 181.58/25.81 % (1910425)Time elapsed: 0.021 s % 181.58/25.81 % (1910425)Peak memory usage: 14 MB % 181.58/25.81 % (1910425)Instructions burned: 82 (million) % 181.58/25.81 % (1910425)------------------------------ % 181.58/25.81 % (1910425)------------------------------ % 181.58/25.81 % (1910427)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=345149358:i=262:bd=preordered:rtra=on:fsd=on_2813 on theBenchmark for (2813ds/262Mi) % 181.58/25.81 % (1910427)Instruction limit reached! % 181.58/25.81 % (1910427)------------------------------ % 181.58/25.81 % (1910427)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 181.58/25.81 % (1910427)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 181.58/25.81 % (1910427)CaDiCaL version: 2.1.3 % 181.58/25.81 % (1910427)Termination reason: Instruction limit % 181.58/25.81 % (1910427)Termination phase: Saturation % 181.58/25.81 % (1910427)Time elapsed: 0.064 s % 181.58/25.81 % (1910427)Peak memory usage: 16 MB % 181.58/25.81 % (1910427)Instructions burned: 264 (million) % 181.58/25.81 % (1910429)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=2498308140:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2812 on theBenchmark for (2812ds/1368Mi) % 181.58/25.81 % (1910429)Instruction limit reached! % 181.58/25.81 % (1910429)------------------------------ % 181.58/25.81 % (1910429)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 181.58/25.81 % (1910429)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 181.58/25.81 % (1910429)CaDiCaL version: 2.1.3 % 181.58/25.81 % (1910429)Termination reason: Instruction limit % 181.58/25.81 % (1910429)Termination phase: Saturation % 181.58/25.81 % (1910429)Time elapsed: 0.397 s % 181.58/25.81 % (1910429)Peak memory usage: 30 MB % 181.58/25.81 % (1910429)Instructions burned: 1370 (million) % 181.58/25.81 % (1910431)ott-21_1_sil=16000:si=on:fs=off:random_seed=1151449435:i=360:av=off:fsr=off:rtra=on_2808 on theBenchmark for (2808ds/360Mi) % 181.58/25.81 % (1910431)Instruction limit reached! % 181.58/25.81 % (1910431)------------------------------ % 181.58/25.81 % (1910431)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 181.58/25.81 % (1910431)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 181.58/25.81 % (1910431)CaDiCaL version: 2.1.3 % 181.58/25.81 % (1910431)Termination reason: Instruction limit % 181.58/25.81 % (1910431)Termination phase: Saturation % 181.58/25.81 % (1910431)Time elapsed: 0.095 s % 181.58/25.81 % (1910431)Peak memory usage: 16 MB % 181.58/25.81 % (1910431)Instructions burned: 361 (million) % 181.58/25.81 % (1910433)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2923251618:i=954:bd=all:rtra=on_2807 on theBenchmark for (2807ds/954Mi) % 181.58/25.81 % (1910433)Instruction limit reached! % 181.58/25.81 % (1910433)------------------------------ % 181.58/25.81 % (1910433)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 181.58/25.81 % (1910433)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 181.58/25.81 % (1910433)CaDiCaL version: 2.1.3 % 181.58/25.81 % (1910433)Termination reason: Instruction limit % 181.58/25.81 % (1910433)Termination phase: Saturation % 181.58/25.81 % (1910433)Time elapsed: 0.294 s % 181.58/25.81 % (1910433)Peak memory usage: 19 MB % 181.58/25.81 % (1910433)Instructions burned: 955 (million) % 181.58/25.81 % (1910435)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=369318409:fmbsr=1.3:i=1730:ins=25:rtra=on_2804 on theBenchmark for (2804ds/1730Mi) % 181.58/25.81 % (1910435)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 181.58/25.81 % (1910435)Terminated due to inappropriate strategy. % 181.58/25.81 % (1910435)------------------------------ % 181.58/25.81 % (1910435)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 181.58/25.81 % (1910435)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 181.58/25.81 % (1910435)CaDiCaL version: 2.1.3 % 181.58/25.81 % (1910435)Termination reason: Inappropriate % 220.61/31.38 % (1910435)Time elapsed: 0.021 s % 220.61/31.38 % (1910435)Peak memory usage: 14 MB % 220.61/31.38 % (1910435)Instructions burned: 81 (million) % 220.61/31.38 % (1910435)------------------------------ % 220.61/31.38 % (1910435)------------------------------ % 220.61/31.38 % (1910437)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=8104086:i=2358:rtra=on_2803 on theBenchmark for (2803ds/2358Mi) % 220.61/31.38 % (1910437)Instruction limit reached! % 220.61/31.38 % (1910437)------------------------------ % 220.61/31.38 % (1910437)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 220.61/31.38 % (1910437)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 220.61/31.38 % (1910437)CaDiCaL version: 2.1.3 % 220.61/31.38 % (1910437)Termination reason: Instruction limit % 220.61/31.38 % (1910437)Termination phase: Saturation % 220.61/31.38 % (1910437)Time elapsed: 0.768 s % 220.61/31.38 % (1910437)Peak memory usage: 25 MB % 220.61/31.38 % (1910437)Instructions burned: 2360 (million) % 220.61/31.38 % (1910439)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=1428968193:i=1778:ins=1:rtra=on_2796 on theBenchmark for (2796ds/1778Mi) % 220.61/31.38 % (1910439)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 220.61/31.38 % (1910439)Terminated due to inappropriate strategy. % 220.61/31.38 % (1910439)------------------------------ % 220.61/31.38 % (1910439)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 220.61/31.38 % (1910439)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 220.61/31.38 % (1910439)CaDiCaL version: 2.1.3 % 220.61/31.38 % (1910439)Termination reason: Inappropriate % 220.61/31.38 % (1910439)Time elapsed: 0.028 s % 220.61/31.38 % (1910439)Peak memory usage: 16 MB % 220.61/31.38 % (1910439)Instructions burned: 109 (million) % 220.61/31.38 % (1910439)------------------------------ % 220.61/31.38 % (1910439)------------------------------ % 220.61/31.38 % (1910441)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=975060351:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2795 on theBenchmark for (2795ds/1384Mi) % 220.61/31.38 % (1910441)Instruction limit reached! % 220.61/31.38 % (1910441)------------------------------ % 220.61/31.38 % (1910441)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 220.61/31.38 % (1910441)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 220.61/31.38 % (1910441)CaDiCaL version: 2.1.3 % 220.61/31.38 % (1910441)Termination reason: Instruction limit % 220.61/31.38 % (1910441)Termination phase: Saturation % 220.61/31.38 % (1910441)Time elapsed: 0.438 s % 220.61/31.38 % (1910441)Peak memory usage: 24 MB % 220.61/31.38 % (1910441)Instructions burned: 1387 (million) % 220.61/31.38 % (1910443)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=3885025615:i=1758:kws=inv_precedence:fsr=off:rtra=on_2791 on theBenchmark for (2791ds/1758Mi) % 220.61/31.38 % (1910443)Instruction limit reached! % 220.61/31.38 % (1910443)------------------------------ % 220.61/31.38 % (1910443)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 220.61/31.38 % (1910443)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 220.61/31.38 % (1910443)CaDiCaL version: 2.1.3 % 220.61/31.38 % (1910443)Termination reason: Instruction limit % 220.61/31.38 % (1910443)Termination phase: Saturation % 220.61/31.38 % (1910443)Time elapsed: 0.535 s % 220.61/31.38 % (1910443)Peak memory usage: 27 MB % 220.61/31.38 % (1910443)Instructions burned: 1759 (million) % 220.61/31.38 % (1910445)fmb+10_1_sil=64000:si=on:random_seed=1122629506:i=44122:nm=2:rtra=on:gsp=on_2785 on theBenchmark for (2785ds/44122Mi) % 220.61/31.38 % (1910445)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 220.61/31.38 % (1910445)Terminated due to inappropriate strategy. % 220.61/31.38 % (1910445)------------------------------ % 220.61/31.38 % (1910445)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 220.61/31.38 % (1910445)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 220.61/31.38 % (1910445)CaDiCaL version: 2.1.3 % 220.61/31.38 % (1910445)Termination reason: Inappropriate % 220.61/31.38 % (1910445)Time elapsed: 0.023 s % 220.61/31.38 % (1910445)Peak memory usage: 14 MB % 220.61/31.38 % (1910445)Instructions burned: 89 (million) % 220.61/31.38 % (1910445)------------------------------ % 220.61/31.38 % (1910445)------------------------------ % 220.61/31.38 % (1910447)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=1550987029:i=19030:nm=5:rtra=on_2785 on theBenchmark for (2785ds/19030Mi) % 268.38/38.04 % (1910447)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 268.38/38.04 % (1910447)Terminated due to inappropriate strategy. % 268.38/38.04 % (1910447)------------------------------ % 268.38/38.04 % (1910447)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 268.38/38.04 % (1910447)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 268.38/38.04 % (1910447)CaDiCaL version: 2.1.3 % 268.38/38.04 % (1910447)Termination reason: Inappropriate % 268.38/38.04 % (1910447)Time elapsed: 0.021 s % 268.38/38.04 % (1910447)Peak memory usage: 14 MB % 268.38/38.04 % (1910447)Instructions burned: 82 (million) % 268.38/38.04 % (1910447)------------------------------ % 268.38/38.04 % (1910447)------------------------------ % 268.38/38.04 % (1910449)fmb+10_1_sil=64000:sas=cadical:si=on:fmbss=8:random_seed=2812638435:fmbsr=1.7:i=1840:rtra=on_2785 on theBenchmark for (2785ds/1840Mi) % 268.38/38.04 % (1910449)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 268.38/38.04 % (1910449)Terminated due to inappropriate strategy. % 268.38/38.04 % (1910449)------------------------------ % 268.38/38.04 % (1910449)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 268.38/38.04 % (1910449)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 268.38/38.04 % (1910449)CaDiCaL version: 2.1.3 % 268.38/38.04 % (1910449)Termination reason: Inappropriate % 268.38/38.04 % (1910449)Time elapsed: 0.021 s % 268.38/38.04 % (1910449)Peak memory usage: 14 MB % 268.38/38.04 % (1910449)Instructions burned: 82 (million) % 268.38/38.04 % (1910449)------------------------------ % 268.38/38.04 % (1910449)------------------------------ % 268.38/38.04 % (1910451)dis-4_1_sil=16000:drc=ordering:si=on:sp=const_frequency:sac=on:newcnf=on:random_seed=2038230642:i=10262:rtra=on_2784 on theBenchmark for (2784ds/10262Mi) % 268.38/38.04 % (1910451)Instruction limit reached! % 268.38/38.04 % (1910451)------------------------------ % 268.38/38.04 % (1910451)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 268.38/38.04 % (1910451)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 268.38/38.04 % (1910451)CaDiCaL version: 2.1.3 % 268.38/38.04 % (1910451)Termination reason: Instruction limit % 268.38/38.04 % (1910451)Termination phase: Saturation % 268.38/38.04 % (1910451)Time elapsed: 3.154 s % 268.38/38.04 % (1910451)Peak memory usage: 71 MB % 268.38/38.04 % (1910451)Instructions burned: 10265 (million) % 268.38/38.04 % (1910453)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:si=on:sp=arity:spb=units:lsd=10:nwc=3:random_seed=97836321:i=2944:ins=7:rtra=on:fdi=8:gsp=on_2752 on theBenchmark for (2752ds/2944Mi) % 268.38/38.04 % (1910453)Instruction limit reached! % 268.38/38.04 % (1910453)------------------------------ % 268.38/38.04 % (1910453)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 268.38/38.04 % (1910453)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 268.38/38.04 % (1910453)CaDiCaL version: 2.1.3 % 268.38/38.04 % (1910453)Termination reason: Instruction limit % 268.38/38.04 % (1910453)Termination phase: Saturation % 268.38/38.04 % (1910453)Time elapsed: 0.820 s % 268.38/38.04 % (1910453)Peak memory usage: 31 MB % 268.38/38.04 % (1910453)Instructions burned: 2945 (million) % 268.38/38.04 % (1910455)fmb+10_1_sil=16000:sas=cadical:si=on:bce=on:fmbss=77:random_seed=1558582757:i=12648:rtra=on_2744 on theBenchmark for (2744ds/12648Mi) % 268.38/38.04 % (1910455)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 268.38/38.04 % (1910455)Terminated due to inappropriate strategy. % 268.38/38.04 % (1910455)------------------------------ % 268.38/38.04 % (1910455)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 268.38/38.04 % (1910455)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 268.38/38.04 % (1910455)CaDiCaL version: 2.1.3 % 268.38/38.04 % (1910455)Termination reason: Inappropriate % 268.38/38.04 % (1910455)Time elapsed: 0.021 s % 268.38/38.04 % (1910455)Peak memory usage: 14 MB % 268.38/38.04 % (1910455)Instructions burned: 82 (million) % 268.38/38.04 % (1910455)------------------------------ % 268.38/38.04 % (1910455)------------------------------ % 268.38/38.04 % (1910457)fmb+10_1_fmbas=function:sil=32000:sas=cadical:si=on:fmbss=16:random_seed=554252738:fmbsr=2.30978:i=4348:rtra=on_2744 on theBenchmark for (2744ds/4348Mi) % 268.38/38.04 % (1910457)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 268.38/38.04 % (1910457)Terminated due to inappropriate strategy. % 268.38/38.04 % (1910457)----------------------Terminated % 300.09/42.54 % Vampire exiting % 300.09/42.54 Terminated %------------------------------------------------------------------------------