%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWW609_2 : TPTP v9.3.1. Released v6.1.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % Computer : 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:40:31 PM UTC 2026 % Result : Timeout 300.14s 42.53s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : SWW609_2 : TPTP v9.3.1. Released v6.1.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.06/0.17 % Computer : n010.cluster.edu % 0.06/0.17 % Model : x86_64 x86_64 % 0.06/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.06/0.17 % Memory : 8046.5625MB % 0.06/0.17 % OS : Linux 6.8.0-71-generic % 0.06/0.17 % CPULimit : 300 % 0.06/0.17 % WCLimit : 300 % 0.06/0.17 % DateTime : Mon Sep 28 14:23:05 UTC 2026 % 0.06/0.18 % CPUTime : % 0.06/0.18 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.06/0.20 Running first-order model finding % 0.06/0.20 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 4.04/0.82 % (1953000)Will run a generic schedule for satisfiability detection. % 4.04/0.82 % (1953007)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=16375655:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 4.04/0.82 % (1953006)% WARNING: option uhcvi not known. % 4.04/0.82 % (1953006)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2137902375:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 4.04/0.82 % (1953008)dis+10_1_sil=32000:sp=arity:random_seed=1157966349:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 4.04/0.82 % (1953009)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3652093165:i=116_2999 on theBenchmark for (2999ds/116Mi) % 4.04/0.82 % (1953010)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2557917919:i=131_2999 on theBenchmark for (2999ds/131Mi) % 4.04/0.82 % (1953011)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3027068297:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 4.04/0.82 % (1953005)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2294585421_2999 on theBenchmark for (2999ds/0Mi) % 4.04/0.82 % (1953005)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 4.04/0.82 % (1953005)Terminated due to inappropriate strategy. % 4.04/0.82 % (1953005)------------------------------ % 4.04/0.82 % (1953005)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 4.04/0.82 % (1953005)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.04/0.82 % (1953005)CaDiCaL version: 2.1.3 % 4.04/0.82 % (1953005)Termination reason: Inappropriate % 4.04/0.82 % (1953005)Time elapsed: 0.002 s % 4.04/0.82 % (1953005)Peak memory usage: 11 MB % 4.04/0.82 % (1953005)Instructions burned: 2 (million) % 4.04/0.82 % (1953005)------------------------------ % 4.04/0.82 % (1953005)------------------------------ % 4.04/0.82 % (1953019)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1985142950:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 4.04/0.82 % (1953019)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 4.04/0.82 % (1953019)Terminated due to inappropriate strategy. % 4.04/0.82 % (1953019)------------------------------ % 4.04/0.82 % (1953019)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 4.04/0.82 % (1953019)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.04/0.82 % (1953019)CaDiCaL version: 2.1.3 % 4.04/0.82 % (1953019)Termination reason: Inappropriate % 4.04/0.82 % (1953019)Time elapsed: 0.001 s % 4.04/0.82 % (1953019)Peak memory usage: 10 MB % 4.04/0.82 % (1953019)Instructions burned: 2 (million) % 4.04/0.82 % (1953019)------------------------------ % 4.04/0.82 % (1953019)------------------------------ % 4.04/0.82 % (1953021)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=810377263:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 4.04/0.82 % (1953008)Instruction limit reached! % 4.04/0.82 % (1953008)------------------------------ % 4.04/0.82 % (1953008)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 4.04/0.82 % (1953008)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.04/0.82 % (1953008)CaDiCaL version: 2.1.3 % 4.04/0.82 % (1953008)Termination reason: Instruction limit % 4.04/0.82 % (1953008)Termination phase: Saturation % 4.04/0.82 % (1953008)Time elapsed: 0.066 s % 4.04/0.82 % (1953008)Peak memory usage: 12 MB % 4.04/0.82 % (1953008)Instructions burned: 104 (million) % 4.04/0.82 % (1953009)Instruction limit reached! % 4.04/0.82 % (1953009)------------------------------ % 4.04/0.82 % (1953009)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 4.04/0.82 % (1953009)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.04/0.82 % (1953009)CaDiCaL version: 2.1.3 % 4.04/0.82 % (1953009)Termination reason: Instruction limit % 4.04/0.82 % (1953009)Termination phase: Saturation % 4.04/0.82 % (1953009)Time elapsed: 0.073 s % 4.04/0.82 % (1953009)Peak memory usage: 12 MB % 4.04/0.82 % (1953009)Instructions burned: 116 (million) % 4.04/0.82 % (1953023)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=2211612887:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi) % 4.04/0.82 % (1953010)Instruction limit reached! % 4.04/0.82 % (1953010)------------------------------ % 4.04/0.82 % (1953010)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.52/1.14 % (1953010)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.52/1.14 % (1953010)CaDiCaL version: 2.1.3 % 6.52/1.14 % (1953010)Termination reason: Instruction limit % 6.52/1.14 % (1953010)Termination phase: Saturation % 6.52/1.14 % (1953010)Time elapsed: 0.086 s % 6.52/1.14 % (1953010)Peak memory usage: 13 MB % 6.52/1.14 % (1953010)Instructions burned: 132 (million) % 6.52/1.14 % (1953024)ott-21_1_sil=16000:fs=off:random_seed=1879556836:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 6.52/1.14 % (1953026)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3998965383:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 6.52/1.14 % (1953011)Instruction limit reached! % 6.52/1.14 % (1953011)------------------------------ % 6.52/1.14 % (1953011)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.52/1.14 % (1953011)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.52/1.14 % (1953011)CaDiCaL version: 2.1.3 % 6.52/1.14 % (1953011)Termination reason: Instruction limit % 6.52/1.14 % (1953011)Termination phase: Saturation % 6.52/1.14 % (1953011)Time elapsed: 0.117 s % 6.52/1.14 % (1953011)Peak memory usage: 13 MB % 6.52/1.14 % (1953011)Instructions burned: 160 (million) % 6.52/1.14 % (1953021)Instruction limit reached! % 6.52/1.14 % (1953021)------------------------------ % 6.52/1.14 % (1953021)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.52/1.14 % (1953021)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.52/1.14 % (1953021)CaDiCaL version: 2.1.3 % 6.52/1.14 % (1953021)Termination reason: Instruction limit % 6.52/1.14 % (1953021)Termination phase: Saturation % 6.52/1.14 % (1953021)Time elapsed: 0.082 s % 6.52/1.14 % (1953021)Peak memory usage: 12 MB % 6.52/1.14 % (1953021)Instructions burned: 131 (million) % 6.52/1.14 % (1953029)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1838799875:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 6.52/1.14 % (1953029)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 6.52/1.14 % (1953029)Terminated due to inappropriate strategy. % 6.52/1.14 % (1953029)------------------------------ % 6.52/1.14 % (1953029)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.52/1.14 % (1953029)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.52/1.14 % (1953029)CaDiCaL version: 2.1.3 % 6.52/1.14 % (1953029)Termination reason: Inappropriate % 6.52/1.14 % (1953029)Time elapsed: 0.001 s % 6.52/1.14 % (1953029)Peak memory usage: 10 MB % 6.52/1.14 % (1953029)Instructions burned: 2 (million) % 6.52/1.14 % (1953029)------------------------------ % 6.52/1.14 % (1953029)------------------------------ % 6.52/1.14 % (1953030)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=4097526208:i=1179_2998 on theBenchmark for (2998ds/1179Mi) % 6.52/1.14 % (1953032)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2220601513:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi) % 6.52/1.14 % (1953032)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 6.52/1.14 % (1953032)Terminated due to inappropriate strategy. % 6.52/1.14 % (1953032)------------------------------ % 6.52/1.14 % (1953032)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.52/1.14 % (1953032)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.52/1.14 % (1953032)CaDiCaL version: 2.1.3 % 6.52/1.14 % (1953032)Termination reason: Inappropriate % 6.52/1.14 % (1953032)Time elapsed: 0.001 s % 6.52/1.14 % (1953032)Peak memory usage: 10 MB % 6.52/1.14 % (1953032)Instructions burned: 2 (million) % 6.52/1.14 % (1953032)------------------------------ % 6.52/1.14 % (1953032)------------------------------ % 6.52/1.14 % (1953035)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=1511641756: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) % 6.52/1.14 % (1953024)Instruction limit reached! % 6.52/1.14 % (1953024)------------------------------ % 6.52/1.14 % (1953024)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.52/1.14 % (1953024)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.52/1.14 % (1953024)CaDiCaL version: 2.1.3 % 6.52/1.14 % (1953024)Termination reason: Instruction limit % 6.52/1.14 % (1953024)Termination phase: Saturation % 22.99/3.53 % (1953024)Time elapsed: 0.089 s % 22.99/3.53 % (1953024)Peak memory usage: 12 MB % 22.99/3.53 % (1953024)Instructions burned: 181 (million) % 22.99/3.53 % (1953037)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=176286739:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi) % 22.99/3.53 % (1953026)Instruction limit reached! % 22.99/3.53 % (1953026)------------------------------ % 22.99/3.53 % (1953026)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.99/3.53 % (1953026)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.99/3.53 % (1953026)CaDiCaL version: 2.1.3 % 22.99/3.53 % (1953026)Termination reason: Instruction limit % 22.99/3.53 % (1953026)Termination phase: Saturation % 22.99/3.53 % (1953026)Time elapsed: 0.317 s % 22.99/3.53 % (1953026)Peak memory usage: 14 MB % 22.99/3.53 % (1953026)Instructions burned: 479 (million) % 22.99/3.53 % (1953039)fmb+10_1_sil=64000:random_seed=432427062:i=22061:nm=2:gsp=on_2995 on theBenchmark for (2995ds/22061Mi) % 22.99/3.53 % (1953039)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 22.99/3.53 % (1953039)Terminated due to inappropriate strategy. % 22.99/3.53 % (1953039)------------------------------ % 22.99/3.53 % (1953039)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.99/3.53 % (1953039)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.99/3.53 % (1953039)CaDiCaL version: 2.1.3 % 22.99/3.53 % (1953039)Termination reason: Inappropriate % 22.99/3.53 % (1953039)Time elapsed: 0.001 s % 22.99/3.53 % (1953039)Peak memory usage: 10 MB % 22.99/3.53 % (1953039)Instructions burned: 2 (million) % 22.99/3.53 % (1953039)------------------------------ % 22.99/3.53 % (1953039)------------------------------ % 22.99/3.53 % (1953023)Instruction limit reached! % 22.99/3.53 % (1953023)------------------------------ % 22.99/3.53 % (1953023)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.99/3.53 % (1953023)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.99/3.53 % (1953023)CaDiCaL version: 2.1.3 % 22.99/3.53 % (1953023)Termination reason: Instruction limit % 22.99/3.53 % (1953023)Termination phase: Saturation % 22.99/3.53 % (1953023)Time elapsed: 0.379 s % 22.99/3.53 % (1953023)Peak memory usage: 16 MB % 22.99/3.53 % (1953023)Instructions burned: 684 (million) % 22.99/3.53 % (1953041)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1133266629:i=9515:nm=5_2995 on theBenchmark for (2995ds/9515Mi) % 22.99/3.53 % (1953041)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 22.99/3.53 % (1953041)Terminated due to inappropriate strategy. % 22.99/3.53 % (1953041)------------------------------ % 22.99/3.53 % (1953041)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.99/3.53 % (1953041)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.99/3.53 % (1953041)CaDiCaL version: 2.1.3 % 22.99/3.53 % (1953041)Termination reason: Inappropriate % 22.99/3.53 % (1953041)Time elapsed: 0.001 s % 22.99/3.53 % (1953041)Peak memory usage: 10 MB % 22.99/3.53 % (1953041)Instructions burned: 2 (million) % 22.99/3.53 % (1953041)------------------------------ % 22.99/3.53 % (1953041)------------------------------ % 22.99/3.53 % (1953043)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=585124790:fmbsr=1.7:i=920_2995 on theBenchmark for (2995ds/920Mi) % 22.99/3.53 % (1953043)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 22.99/3.53 % (1953043)Terminated due to inappropriate strategy. % 22.99/3.53 % (1953043)------------------------------ % 22.99/3.53 % (1953043)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.99/3.53 % (1953043)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.99/3.53 % (1953043)CaDiCaL version: 2.1.3 % 22.99/3.53 % (1953043)Termination reason: Inappropriate % 22.99/3.53 % (1953043)Time elapsed: 0.001 s % 22.99/3.53 % (1953043)Peak memory usage: 10 MB % 22.99/3.53 % (1953043)Instructions burned: 2 (million) % 22.99/3.53 % (1953043)------------------------------ % 22.99/3.53 % (1953043)------------------------------ % 22.99/3.53 % (1953044)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=923637393:i=5131_2994 on theBenchmark for (2994ds/5131Mi) % 22.99/3.53 % (1953047)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2758630955:i=1472:ins=7:fdi=8:gsp=on_2994 on theBenchmark for (2994ds/1472Mi) % 22.99/3.53 % (1953035)Instruction limit reached! % 22.99/3.53 % (1953035)------------------------------ % 36.09/5.39 % (1953035)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 36.09/5.39 % (1953035)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 36.09/5.39 % (1953035)CaDiCaL version: 2.1.3 % 36.09/5.39 % (1953035)Termination reason: Instruction limit % 36.09/5.39 % (1953035)Termination phase: Saturation % 36.09/5.39 % (1953035)Time elapsed: 0.401 s % 36.09/5.39 % (1953035)Peak memory usage: 18 MB % 36.09/5.39 % (1953035)Instructions burned: 692 (million) % 36.09/5.39 % (1953049)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=929379653:i=6324_2993 on theBenchmark for (2993ds/6324Mi) % 36.09/5.39 % (1953049)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 36.09/5.39 % (1953049)Terminated due to inappropriate strategy. % 36.09/5.39 % (1953049)------------------------------ % 36.09/5.39 % (1953049)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 36.09/5.39 % (1953049)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 36.09/5.39 % (1953049)CaDiCaL version: 2.1.3 % 36.09/5.39 % (1953049)Termination reason: Inappropriate % 36.09/5.39 % (1953049)Time elapsed: 0.001 s % 36.09/5.39 % (1953049)Peak memory usage: 10 MB % 36.09/5.39 % (1953049)Instructions burned: 2 (million) % 36.09/5.39 % (1953049)------------------------------ % 36.09/5.39 % (1953049)------------------------------ % 36.09/5.39 % (1953051)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=2585051518:fmbsr=2.30978:i=2174_2993 on theBenchmark for (2993ds/2174Mi) % 36.09/5.39 % (1953051)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 36.09/5.39 % (1953051)Terminated due to inappropriate strategy. % 36.09/5.39 % (1953051)------------------------------ % 36.09/5.39 % (1953051)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 36.09/5.39 % (1953051)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 36.09/5.39 % (1953051)CaDiCaL version: 2.1.3 % 36.09/5.39 % (1953051)Termination reason: Inappropriate % 36.09/5.39 % (1953051)Time elapsed: 0.001 s % 36.09/5.39 % (1953051)Peak memory usage: 10 MB % 36.09/5.39 % (1953051)Instructions burned: 2 (million) % 36.09/5.39 % (1953051)------------------------------ % 36.09/5.39 % (1953051)------------------------------ % 36.09/5.39 % (1953053)ott-2_1_sil=16000:newcnf=on:random_seed=884669293:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2993 on theBenchmark for (2993ds/869Mi) % 36.09/5.39 % (1953037)Instruction limit reached! % 36.09/5.39 % (1953037)------------------------------ % 36.09/5.39 % (1953037)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 36.09/5.39 % (1953037)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 36.09/5.39 % (1953037)CaDiCaL version: 2.1.3 % 36.09/5.39 % (1953037)Termination reason: Instruction limit % 36.09/5.39 % (1953037)Termination phase: Saturation % 36.09/5.39 % (1953037)Time elapsed: 0.518 s % 36.09/5.39 % (1953037)Peak memory usage: 20 MB % 36.09/5.39 % (1953037)Instructions burned: 880 (million) % 36.09/5.39 % (1953055)ott+10_1_sil=32000:tgt=ground:random_seed=2438388854:i=5114:av=off_2992 on theBenchmark for (2992ds/5114Mi) % 36.09/5.39 % (1953030)Instruction limit reached! % 36.09/5.39 % (1953030)------------------------------ % 36.09/5.39 % (1953030)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 36.09/5.39 % (1953030)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 36.09/5.39 % (1953030)CaDiCaL version: 2.1.3 % 36.09/5.39 % (1953030)Termination reason: Instruction limit % 36.09/5.39 % (1953030)Termination phase: Saturation % 36.09/5.39 % (1953030)Time elapsed: 0.725 s % 36.09/5.39 % (1953030)Peak memory usage: 20 MB % 36.09/5.39 % (1953030)Instructions burned: 1179 (million) % 36.09/5.39 % (1953057)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=69138845:i=54282_2990 on theBenchmark for (2990ds/54282Mi) % 36.09/5.39 % (1953057)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 36.09/5.39 % (1953057)Terminated due to inappropriate strategy. % 36.09/5.39 % (1953057)------------------------------ % 36.09/5.39 % (1953057)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 36.09/5.39 % (1953057)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 36.09/5.39 % (1953057)CaDiCaL version: 2.1.3 % 36.09/5.39 % (1953057)Termination reason: Inappropriate % 36.09/5.39 % (1953057)Time elapsed: 0.002 s % 36.09/5.39 % (1953057)Peak memory usage: 10 MB % 36.09/5.39 % (1953057)Instructions burned: 2 (million) % 108.50/15.58 % (1953057)------------------------------ % 108.50/15.58 % (1953057)------------------------------ % 108.50/15.58 % (1953059)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=857713725:i=3512:aac=none_2990 on theBenchmark for (2990ds/3512Mi) % 108.50/15.58 % (1953053)Instruction limit reached! % 108.50/15.58 % (1953053)------------------------------ % 108.50/15.58 % (1953053)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 108.50/15.58 % (1953053)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 108.50/15.58 % (1953053)CaDiCaL version: 2.1.3 % 108.50/15.58 % (1953053)Termination reason: Instruction limit % 108.50/15.58 % (1953053)Termination phase: Saturation % 108.50/15.58 % (1953053)Time elapsed: 0.497 s % 108.50/15.58 % (1953053)Peak memory usage: 15 MB % 108.50/15.58 % (1953053)Instructions burned: 869 (million) % 108.50/15.58 % (1953061)dis+21_1_sil=32000:sas=cadical:random_seed=2333947442:i=3773:amm=off_2988 on theBenchmark for (2988ds/3773Mi) % 108.50/15.58 % (1953047)Instruction limit reached! % 108.50/15.58 % (1953047)------------------------------ % 108.50/15.58 % (1953047)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 108.50/15.58 % (1953047)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 108.50/15.58 % (1953047)CaDiCaL version: 2.1.3 % 108.50/15.58 % (1953047)Termination reason: Instruction limit % 108.50/15.58 % (1953047)Termination phase: Saturation % 108.50/15.58 % (1953047)Time elapsed: 0.855 s % 108.50/15.58 % (1953047)Peak memory usage: 24 MB % 108.50/15.58 % (1953047)Instructions burned: 1472 (million) % 108.50/15.58 % (1953063)ott+11_1_sil=16000:gs=on:random_seed=946120386:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2986 on theBenchmark for (2986ds/2251Mi) % 108.50/15.58 % (1953063)Instruction limit reached! % 108.50/15.58 % (1953063)------------------------------ % 108.50/15.58 % (1953063)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 108.50/15.58 % (1953063)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 108.50/15.58 % (1953063)CaDiCaL version: 2.1.3 % 108.50/15.58 % (1953063)Termination reason: Instruction limit % 108.50/15.58 % (1953063)Termination phase: Saturation % 108.50/15.58 % (1953063)Time elapsed: 1.052 s % 108.50/15.58 % (1953063)Peak memory usage: 16 MB % 108.50/15.58 % (1953063)Instructions burned: 2251 (million) % 108.50/15.58 % (1953065)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=3623693038:fmbsr=1.6:i=67534_2975 on theBenchmark for (2975ds/67534Mi) % 108.50/15.58 % (1953065)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 108.50/15.58 % (1953065)Terminated due to inappropriate strategy. % 108.50/15.58 % (1953065)------------------------------ % 108.50/15.58 % (1953065)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 108.50/15.58 % (1953065)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 108.50/15.58 % (1953065)CaDiCaL version: 2.1.3 % 108.50/15.58 % (1953065)Termination reason: Inappropriate % 108.50/15.58 % (1953065)Time elapsed: 0.001 s % 108.50/15.58 % (1953065)Peak memory usage: 10 MB % 108.50/15.58 % (1953065)Instructions burned: 2 (million) % 108.50/15.58 % (1953065)------------------------------ % 108.50/15.58 % (1953065)------------------------------ % 108.50/15.58 % (1953067)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=1438936743:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2975 on theBenchmark for (2975ds/4591Mi) % 108.50/15.58 % (1953059)Instruction limit reached! % 108.50/15.58 % (1953059)------------------------------ % 108.50/15.58 % (1953059)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 108.50/15.58 % (1953059)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 108.50/15.58 % (1953059)CaDiCaL version: 2.1.3 % 108.50/15.58 % (1953059)Termination reason: Instruction limit % 108.50/15.58 % (1953059)Termination phase: Saturation % 108.50/15.58 % (1953059)Time elapsed: 1.971 s % 108.50/15.58 % (1953059)Peak memory usage: 32 MB % 108.50/15.58 % (1953059)Instructions burned: 3513 (million) % 108.50/15.58 % (1953069)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=1469430812:i=29340_2970 on theBenchmark for (2970ds/29340Mi) % 108.50/15.58 % (1953061)Instruction limit reached! % 108.50/15.58 % (1953061)------------------------------ % 108.50/15.58 % (1953061)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 108.50/15.58 % (1953061)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 108.50/15.58 % (1953061)CaDiCaL version: 2.1.3 % 108.50/15.58 % (1953061)Termination reason: Instruction limit % 126.29/19.34 % (1953061)Termination phase: Saturation % 126.29/19.34 % (1953061)Time elapsed: 2.123 s % 126.29/19.34 % (1953061)Peak memory usage: 33 MB % 126.29/19.34 % (1953061)Instructions burned: 3773 (million) % 126.29/19.34 % (1953044)Instruction limit reached! % 126.29/19.34 % (1953044)------------------------------ % 126.29/19.34 % (1953044)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 126.29/19.34 % (1953044)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 126.29/19.34 % (1953044)CaDiCaL version: 2.1.3 % 126.29/19.34 % (1953044)Termination reason: Instruction limit % 126.29/19.34 % (1953044)Termination phase: Saturation % 126.29/19.34 % (1953044)Time elapsed: 2.809 s % 126.29/19.34 % (1953044)Peak memory usage: 42 MB % 126.29/19.34 % (1953044)Instructions burned: 5132 (million) % 126.29/19.34 % (1953071)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=431284796:i=5211_2966 on theBenchmark for (2966ds/5211Mi) % 126.29/19.34 % (1953072)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=2611649532:i=5497:nm=2_2966 on theBenchmark for (2966ds/5497Mi) % 126.29/19.34 % (1953072)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 126.29/19.34 % (1953072)Terminated due to inappropriate strategy. % 126.29/19.34 % (1953072)------------------------------ % 126.29/19.34 % (1953072)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 126.29/19.34 % (1953072)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 126.29/19.34 % (1953072)CaDiCaL version: 2.1.3 % 126.29/19.34 % (1953072)Termination reason: Inappropriate % 126.29/19.34 % (1953072)Time elapsed: 0.001 s % 126.29/19.34 % (1953072)Peak memory usage: 10 MB % 126.29/19.34 % (1953072)Instructions burned: 2 (million) % 126.29/19.34 % (1953072)------------------------------ % 126.29/19.34 % (1953072)------------------------------ % 126.29/19.34 % (1953075)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=1155268032:fmbsr=2:i=46332_2966 on theBenchmark for (2966ds/46332Mi) % 126.29/19.34 % (1953075)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 126.29/19.34 % (1953075)Terminated due to inappropriate strategy. % 126.29/19.34 % (1953075)------------------------------ % 126.29/19.34 % (1953075)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 126.29/19.34 % (1953075)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 126.29/19.34 % (1953075)CaDiCaL version: 2.1.3 % 126.29/19.34 % (1953075)Termination reason: Inappropriate % 126.29/19.34 % (1953075)Time elapsed: 0.001 s % 126.29/19.34 % (1953075)Peak memory usage: 10 MB % 126.29/19.34 % (1953075)Instructions burned: 2 (million) % 126.29/19.34 % (1953075)------------------------------ % 126.29/19.34 % (1953075)------------------------------ % 126.29/19.34 % (1953077)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=3567979169:i=14071_2966 on theBenchmark for (2966ds/14071Mi) % 126.29/19.34 % (1953077)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 126.29/19.34 % (1953077)Terminated due to inappropriate strategy. % 126.29/19.34 % (1953077)------------------------------ % 126.29/19.34 % (1953077)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 126.29/19.34 % (1953077)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 126.29/19.34 % (1953077)CaDiCaL version: 2.1.3 % 126.29/19.34 % (1953077)Termination reason: Inappropriate % 126.29/19.34 % (1953077)Time elapsed: 0.001 s % 126.29/19.34 % (1953077)Peak memory usage: 10 MB % 126.29/19.34 % (1953077)Instructions burned: 2 (million) % 126.29/19.34 % (1953077)------------------------------ % 126.29/19.34 % (1953077)------------------------------ % 126.29/19.34 % (1953079)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3708047169:i=22565:add=on:rawr=on_2966 on theBenchmark for (2966ds/22565Mi) % 126.29/19.34 % (1953055)Instruction limit reached! % 126.29/19.34 % (1953055)------------------------------ % 126.29/19.34 % (1953055)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 126.29/19.34 % (1953055)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 126.29/19.34 % (1953055)CaDiCaL version: 2.1.3 % 126.29/19.34 % (1953055)Termination reason: Instruction limit % 126.29/19.34 % (1953055)Termination phase: Saturation % 126.29/19.34 % (1953055)Time elapsed: 2.867 s % 126.29/19.34 % (1953055)Peak memory usage: 30 MB % 126.29/19.34 % (1953055)Instructions burned: 5115 (million) % 126.29/19.34 % (1953081)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=1451670192:i=8173:av=off_2963 on theBenchmark for (2963ds/8173Mi) % 126.29/19.34 % (1953067)Instruction limit reached! % 136.20/19.45 % (1953067)------------------------------ % 136.20/19.45 % (1953067)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 136.20/19.45 % (1953067)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 136.20/19.45 % (1953067)CaDiCaL version: 2.1.3 % 136.20/19.45 % (1953067)Termination reason: Instruction limit % 136.20/19.45 % (1953067)Termination phase: Saturation % 136.20/19.45 % (1953067)Time elapsed: 2.674 s % 136.20/19.45 % (1953067)Peak memory usage: 53 MB % 136.20/19.45 % (1953067)Instructions burned: 4592 (million) % 136.20/19.45 % (1953083)dis+10_16:1_sil=16000:random_seed=2084309489:i=9155:fsr=off_2948 on theBenchmark for (2948ds/9155Mi) % 136.20/19.45 % (1953071)Instruction limit reached! % 136.20/19.45 % (1953071)------------------------------ % 136.20/19.45 % (1953071)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 136.20/19.45 % (1953071)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 136.20/19.45 % (1953071)CaDiCaL version: 2.1.3 % 136.20/19.45 % (1953071)Termination reason: Instruction limit % 136.20/19.45 % (1953071)Termination phase: Saturation % 136.20/19.45 % (1953071)Time elapsed: 2.885 s % 136.20/19.45 % (1953071)Peak memory usage: 65 MB % 136.20/19.45 % (1953071)Instructions burned: 5211 (million) % 136.20/19.45 % (1953085)ott-3_8_sil=64000:random_seed=2782002866:i=20139:bs=on_2937 on theBenchmark for (2937ds/20139Mi) % 136.20/19.45 % (1953081)Instruction limit reached! % 136.20/19.45 % (1953081)------------------------------ % 136.20/19.45 % (1953081)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 136.20/19.45 % (1953081)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 136.20/19.45 % (1953081)CaDiCaL version: 2.1.3 % 136.20/19.45 % (1953081)Termination reason: Instruction limit % 136.20/19.45 % (1953081)Termination phase: Saturation % 136.20/19.45 % (1953081)Time elapsed: 4.600 s % 136.20/19.45 % (1953081)Peak memory usage: 53 MB % 136.20/19.45 % (1953081)Instructions burned: 8173 (million) % 136.20/19.45 % (1953087)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=398620821:fmbsr=2:i=32576_2917 on theBenchmark for (2917ds/32576Mi) % 136.20/19.45 % (1953087)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 136.20/19.45 % (1953087)Terminated due to inappropriate strategy. % 136.20/19.45 % (1953087)------------------------------ % 136.20/19.45 % (1953087)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 136.20/19.45 % (1953087)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 136.20/19.45 % (1953087)CaDiCaL version: 2.1.3 % 136.20/19.45 % (1953087)Termination reason: Inappropriate % 136.20/19.45 % (1953087)Time elapsed: 0.002 s % 136.20/19.45 % (1953087)Peak memory usage: 10 MB % 136.20/19.45 % (1953087)Instructions burned: 2 (million) % 136.20/19.45 % (1953087)------------------------------ % 136.20/19.45 % (1953087)------------------------------ % 136.20/19.45 % (1953089)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=2130879197:i=11404_2917 on theBenchmark for (2917ds/11404Mi) % 136.20/19.45 % (1953083)Instruction limit reached! % 136.20/19.45 % (1953083)------------------------------ % 136.20/19.45 % (1953083)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 136.20/19.45 % (1953083)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 136.20/19.45 % (1953083)CaDiCaL version: 2.1.3 % 136.20/19.45 % (1953083)Termination reason: Instruction limit % 136.20/19.45 % (1953083)Termination phase: Saturation % 136.20/19.45 % (1953083)Time elapsed: 4.791 s % 136.20/19.45 % (1953083)Peak memory usage: 55 MB % 136.20/19.45 % (1953083)Instructions burned: 9155 (million) % 136.20/19.45 % (1953091)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=1643887875:i=14134_2899 on theBenchmark for (2899ds/14134Mi) % 136.20/19.45 % (1953079)Instruction limit reached! % 136.20/19.45 % (1953079)------------------------------ % 136.20/19.45 % (1953079)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 136.20/19.45 % (1953079)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 136.20/19.45 % (1953079)CaDiCaL version: 2.1.3 % 136.20/19.45 % (1953079)Termination reason: Instruction limit % 136.20/19.45 % (1953079)Termination phase: Saturation % 136.20/19.45 % (1953079)Time elapsed: 9.129 s % 136.20/19.45 % (1953079)Peak memory usage: 36 MB % 136.20/19.45 % (1953079)Instructions burned: 22567 (million) % 136.20/19.45 % (1953420)dis+33_16_sil=32000:sac=on:random_seed=2337216228:i=15851:nm=0_2874 on theBenchmark for (2874ds/15851Mi) % 136.20/19.45 % (1953089)Instruction limit reached! % 136.20/19.45 % (1953089)------------------------------ % 136.20/19.45 % (1953089)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 160.01/22.99 % (1953089)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 160.01/22.99 % (1953089)CaDiCaL version: 2.1.3 % 160.01/22.99 % (1953089)Termination reason: Instruction limit % 160.01/22.99 % (1953089)Termination phase: Saturation % 160.01/22.99 % (1953089)Time elapsed: 7.056 s % 160.01/22.99 % (1953089)Peak memory usage: 71 MB % 160.01/22.99 % (1953089)Instructions burned: 11405 (million) % 160.01/22.99 % (1953454)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=3368077952:avsq=on:i=17627:add=on:amm=off_2846 on theBenchmark for (2846ds/17627Mi) % 160.01/22.99 % (1953069)Instruction limit reached! % 160.01/22.99 % (1953069)------------------------------ % 160.01/22.99 % (1953069)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 160.01/22.99 % (1953069)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 160.01/22.99 % (1953069)CaDiCaL version: 2.1.3 % 160.01/22.99 % (1953069)Termination reason: Instruction limit % 160.01/22.99 % (1953069)Termination phase: Saturation % 160.01/22.99 % (1953069)Time elapsed: 14.597 s % 160.01/22.99 % (1953069)Peak memory usage: 181 MB % 160.01/22.99 % (1953069)Instructions burned: 29342 (million) % 160.01/22.99 % (1953456)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=1945527013:s2a=on:i=53295_2824 on theBenchmark for (2824ds/53295Mi) % 160.01/22.99 % (1953085)Instruction limit reached! % 160.01/22.99 % (1953085)------------------------------ % 160.01/22.99 % (1953085)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 160.01/22.99 % (1953085)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 160.01/22.99 % (1953085)CaDiCaL version: 2.1.3 % 160.01/22.99 % (1953085)Termination reason: Instruction limit % 160.01/22.99 % (1953085)Termination phase: Saturation % 160.01/22.99 % (1953085)Time elapsed: 12.164 s % 160.01/22.99 % (1953085)Peak memory usage: 102 MB % 160.01/22.99 % (1953085)Instructions burned: 20140 (million) % 160.01/22.99 % (1953458)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=911881133:i=26857:ins=20_2815 on theBenchmark for (2815ds/26857Mi) % 160.01/22.99 % (1953458)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 160.01/22.99 % (1953458)Terminated due to inappropriate strategy. % 160.01/22.99 % (1953458)------------------------------ % 160.01/22.99 % (1953458)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 160.01/22.99 % (1953458)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 160.01/22.99 % (1953458)CaDiCaL version: 2.1.3 % 160.01/22.99 % (1953458)Termination reason: Inappropriate % 160.01/22.99 % (1953458)Time elapsed: 0.001 s % 160.01/22.99 % (1953458)Peak memory usage: 10 MB % 160.01/22.99 % (1953458)Instructions burned: 2 (million) % 160.01/22.99 % (1953458)------------------------------ % 160.01/22.99 % (1953458)------------------------------ % 160.01/22.99 % (1953460)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=1126641999:i=28120:bs=on:fsr=off_2815 on theBenchmark for (2815ds/28120Mi) % 160.01/22.99 % (1953091)Instruction limit reached! % 160.01/22.99 % (1953091)------------------------------ % 160.01/22.99 % (1953091)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 160.01/22.99 % (1953091)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 160.01/22.99 % (1953091)CaDiCaL version: 2.1.3 % 160.01/22.99 % (1953091)Termination reason: Instruction limit % 160.01/22.99 % (1953091)Termination phase: Saturation % 160.01/22.99 % (1953091)Time elapsed: 9.051 s % 160.01/22.99 % (1953091)Peak memory usage: 80 MB % 160.01/22.99 % (1953091)Instructions burned: 14134 (million) % 160.01/22.99 % (1953463)fmb+10_1_sil=256000:fmbss=7:random_seed=51874386:fmbsr=1.6:i=182295_2809 on theBenchmark for (2809ds/182295Mi) % 160.01/22.99 % (1953463)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 160.01/22.99 % (1953463)Terminated due to inappropriate strategy. % 160.01/22.99 % (1953463)------------------------------ % 160.01/22.99 % (1953463)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 160.01/22.99 % (1953463)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 160.01/22.99 % (1953463)CaDiCaL version: 2.1.3 % 160.01/22.99 % (1953463)Termination reason: Inappropriate % 160.01/22.99 % (1953463)Time elapsed: 0.001 s % 160.01/22.99 % (1953463)Peak memory usage: 10 MB % 160.01/22.99 % (1953463)Instructions burned: 2 (million) % 160.01/22.99 % (1953463)------------------------------ % 160.01/22.99 % (1953463)------------------------------ % 160.01/22.99 % (1953465)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=1771422602:i=44625:gsp=on_2808 on theBenchmark for (2808ds/44625Mi) % 169.06/24.04 % (1953465)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 169.06/24.04 % (1953465)Terminated due to inappropriate strategy. % 169.06/24.04 % (1953465)------------------------------ % 169.06/24.04 % (1953465)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 169.06/24.04 % (1953465)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 169.06/24.04 % (1953465)CaDiCaL version: 2.1.3 % 169.06/24.04 % (1953465)Termination reason: Inappropriate % 169.06/24.04 % (1953465)Time elapsed: 0.001 s % 169.06/24.04 % (1953465)Peak memory usage: 10 MB % 169.06/24.04 % (1953465)Instructions burned: 2 (million) % 169.06/24.04 % (1953465)------------------------------ % 169.06/24.04 % (1953465)------------------------------ % 169.06/24.04 % (1953467)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=1453367625:i=160505_2808 on theBenchmark for (2808ds/160505Mi) % 169.06/24.04 % (1953467)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 169.06/24.04 % (1953467)Terminated due to inappropriate strategy. % 169.06/24.04 % (1953467)------------------------------ % 169.06/24.04 % (1953467)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 169.06/24.04 % (1953467)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 169.06/24.04 % (1953467)CaDiCaL version: 2.1.3 % 169.06/24.04 % (1953467)Termination reason: Inappropriate % 169.06/24.04 % (1953467)Time elapsed: 0.001 s % 169.06/24.04 % (1953467)Peak memory usage: 10 MB % 169.06/24.04 % (1953467)Instructions burned: 2 (million) % 169.06/24.04 % (1953467)------------------------------ % 169.06/24.04 % (1953467)------------------------------ % 169.06/24.04 % (1953469)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=3179768627:fmbsr=1.3:i=225729_2808 on theBenchmark for (2808ds/225729Mi) % 169.06/24.04 % (1953469)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 169.06/24.04 % (1953469)Terminated due to inappropriate strategy. % 169.06/24.04 % (1953469)------------------------------ % 169.06/24.04 % (1953469)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 169.06/24.04 % (1953469)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 169.06/24.04 % (1953469)CaDiCaL version: 2.1.3 % 169.06/24.04 % (1953469)Termination reason: Inappropriate % 169.06/24.04 % (1953469)Time elapsed: 0.002 s % 169.06/24.04 % (1953469)Peak memory usage: 10 MB % 169.06/24.04 % (1953469)Instructions burned: 2 (million) % 169.06/24.04 % (1953469)------------------------------ % 169.06/24.04 % (1953469)------------------------------ % 169.06/24.04 % (1953471)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=2286278254:fmbsr=2:i=185024:ins=7_2808 on theBenchmark for (2808ds/185024Mi) % 169.06/24.04 % (1953471)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 169.06/24.04 % (1953471)Terminated due to inappropriate strategy. % 169.06/24.04 % (1953471)------------------------------ % 169.06/24.04 % (1953471)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 169.06/24.04 % (1953471)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 169.06/24.04 % (1953471)CaDiCaL version: 2.1.3 % 169.06/24.04 % (1953471)Termination reason: Inappropriate % 169.06/24.04 % (1953471)Time elapsed: 0.001 s % 169.06/24.04 % (1953471)Peak memory usage: 10 MB % 169.06/24.04 % (1953471)Instructions burned: 2 (million) % 169.06/24.04 % (1953471)------------------------------ % 169.06/24.04 % (1953471)------------------------------ % 169.06/24.04 % (1953473)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=424816087:rtra=on_2807 on theBenchmark for (2807ds/0Mi) % 169.06/24.04 % (1953473)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 169.06/24.04 % (1953473)Terminated due to inappropriate strategy. % 169.06/24.04 % (1953473)------------------------------ % 169.06/24.04 % (1953473)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 169.06/24.04 % (1953473)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 169.06/24.04 % (1953473)CaDiCaL version: 2.1.3 % 169.06/24.04 % (1953473)Termination reason: Inappropriate % 169.06/24.04 % (1953473)Time elapsed: 0.002 s % 169.06/24.04 % (1953473)Peak memory usage: 10 MB % 169.06/24.04 % (1953473)Instructions burned: 2 (million) % 169.06/24.04 % (1953473)------------------------------ % 169.06/24.04 % (1953473)------------------------------ % 169.06/24.04 % (1953475)% WARNING: option uhcvi not known. % 169.06/24.04 % (1953475)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1417354445:i=271062:add=off:rtra=on:rawr=on_2807 on theBenchmark for (2807ds/271062Mi) % 179.81/25.66 % (1953007)Instruction limit reached! % 179.81/25.66 % (1953007)------------------------------ % 179.81/25.66 % (1953007)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 179.81/25.66 % (1953007)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 179.81/25.66 % (1953007)CaDiCaL version: 2.1.3 % 179.81/25.66 % (1953007)Termination reason: Instruction limit % 179.81/25.66 % (1953007)Termination phase: Saturation % 179.81/25.66 % (1953007)Time elapsed: 21.799 s % 179.81/25.66 % (1953007)Peak memory usage: 79 MB % 179.81/25.66 % (1953007)Instructions burned: 88025 (million) % 179.81/25.66 % (1953477)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1691201030:i=176048:add=on:rtra=on:rawr=on_2781 on theBenchmark for (2781ds/176048Mi) % 179.81/25.66 % (1953420)Instruction limit reached! % 179.81/25.66 % (1953420)------------------------------ % 179.81/25.66 % (1953420)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 179.81/25.66 % (1953420)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 179.81/25.66 % (1953420)CaDiCaL version: 2.1.3 % 179.81/25.66 % (1953420)Termination reason: Instruction limit % 179.81/25.66 % (1953420)Termination phase: Saturation % 179.81/25.66 % (1953420)Time elapsed: 9.411 s % 179.81/25.66 % (1953420)Peak memory usage: 165 MB % 179.81/25.66 % (1953420)Instructions burned: 15852 (million) % 179.81/25.66 % (1953479)dis+10_1_sil=32000:si=on:sp=arity:random_seed=2034719147:i=206:fgj=on:rtra=on_2779 on theBenchmark for (2779ds/206Mi) % 179.81/25.66 % (1953479)Instruction limit reached! % 179.81/25.66 % (1953479)------------------------------ % 179.81/25.66 % (1953479)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 179.81/25.66 % (1953479)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 179.81/25.66 % (1953479)CaDiCaL version: 2.1.3 % 179.81/25.66 % (1953479)Termination reason: Instruction limit % 179.81/25.66 % (1953479)Termination phase: Saturation % 179.81/25.66 % (1953479)Time elapsed: 0.130 s % 179.81/25.66 % (1953479)Peak memory usage: 13 MB % 179.81/25.66 % (1953479)Instructions burned: 207 (million) % 179.81/25.66 % (1953481)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=4199366168:i=232:rtra=on_2778 on theBenchmark for (2778ds/232Mi) % 179.81/25.66 % (1953481)Instruction limit reached! % 179.81/25.66 % (1953481)------------------------------ % 179.81/25.66 % (1953481)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 179.81/25.66 % (1953481)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 179.81/25.66 % (1953481)CaDiCaL version: 2.1.3 % 179.81/25.66 % (1953481)Termination reason: Instruction limit % 179.81/25.66 % (1953481)Termination phase: Saturation % 179.81/25.66 % (1953481)Time elapsed: 0.153 s % 179.81/25.66 % (1953481)Peak memory usage: 13 MB % 179.81/25.66 % (1953481)Instructions burned: 232 (million) % 179.81/25.66 % (1953483)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=3268104760:i=262:rtra=on_2776 on theBenchmark for (2776ds/262Mi) % 179.81/25.66 % (1953483)Instruction limit reached! % 179.81/25.66 % (1953483)------------------------------ % 179.81/25.66 % (1953483)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 179.81/25.66 % (1953483)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 179.81/25.66 % (1953483)CaDiCaL version: 2.1.3 % 179.81/25.66 % (1953483)Termination reason: Instruction limit % 179.81/25.66 % (1953483)Termination phase: Saturation % 179.81/25.66 % (1953483)Time elapsed: 0.167 s % 179.81/25.66 % (1953483)Peak memory usage: 14 MB % 179.81/25.66 % (1953483)Instructions burned: 263 (million) % 179.81/25.66 % (1953485)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=2505426741:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2774 on theBenchmark for (2774ds/318Mi) % 179.81/25.66 % (1953485)Instruction limit reached! % 179.81/25.66 % (1953485)------------------------------ % 179.81/25.66 % (1953485)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 179.81/25.66 % (1953485)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 179.81/25.66 % (1953485)CaDiCaL version: 2.1.3 % 179.81/25.66 % (1953485)Termination reason: Instruction limit % 179.81/25.66 % (1953485)Termination phase: Saturation % 179.81/25.66 % (1953485)Time elapsed: 0.223 s % 179.81/25.66 % (1953485)Peak memory usage: 15 MB % 179.81/25.66 % (1953485)Instructions burned: 319 (million) % 179.81/25.66 % (1953487)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=195802261:i=1428:nm=2:rtra=on_2772 on theBenchmark for (2772ds/1428Mi) % 196.53/27.93 % (1953487)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 196.53/27.93 % (1953487)Terminated due to inappropriate strategy. % 196.53/27.93 % (1953487)------------------------------ % 196.53/27.93 % (1953487)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 196.53/27.93 % (1953487)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 196.53/27.93 % (1953487)CaDiCaL version: 2.1.3 % 196.53/27.93 % (1953487)Termination reason: Inappropriate % 196.53/27.93 % (1953487)Time elapsed: 0.002 s % 196.53/27.93 % (1953487)Peak memory usage: 10 MB % 196.53/27.93 % (1953487)Instructions burned: 2 (million) % 196.53/27.93 % (1953487)------------------------------ % 196.53/27.93 % (1953487)------------------------------ % 196.53/27.93 % (1953489)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=1937614797:i=262:bd=preordered:rtra=on:fsd=on_2772 on theBenchmark for (2772ds/262Mi) % 196.53/27.93 % (1953489)Instruction limit reached! % 196.53/27.93 % (1953489)------------------------------ % 196.53/27.93 % (1953489)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 196.53/27.93 % (1953489)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 196.53/27.93 % (1953489)CaDiCaL version: 2.1.3 % 196.53/27.93 % (1953489)Termination reason: Instruction limit % 196.53/27.93 % (1953489)Termination phase: Saturation % 196.53/27.93 % (1953489)Time elapsed: 0.171 s % 196.53/27.93 % (1953489)Peak memory usage: 13 MB % 196.53/27.93 % (1953489)Instructions burned: 262 (million) % 196.53/27.93 % (1953491)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=2390064659:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2770 on theBenchmark for (2770ds/1368Mi) % 196.53/27.93 % (1953454)Instruction limit reached! % 196.53/27.93 % (1953454)------------------------------ % 196.53/27.93 % (1953454)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 196.53/27.93 % (1953454)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 196.53/27.93 % (1953454)CaDiCaL version: 2.1.3 % 196.53/27.93 % (1953454)Termination reason: Instruction limit % 196.53/27.93 % (1953454)Termination phase: Saturation % 196.53/27.93 % (1953454)Time elapsed: 7.836 s % 196.53/27.93 % (1953454)Peak memory usage: 92 MB % 196.53/27.93 % (1953454)Instructions burned: 17628 (million) % 196.53/27.93 % (1953493)ott-21_1_sil=16000:si=on:fs=off:random_seed=3224351734:i=360:av=off:fsr=off:rtra=on_2767 on theBenchmark for (2767ds/360Mi) % 196.53/27.93 % (1953493)Instruction limit reached! % 196.53/27.93 % (1953493)------------------------------ % 196.53/27.93 % (1953493)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 196.53/27.93 % (1953493)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 196.53/27.93 % (1953493)CaDiCaL version: 2.1.3 % 196.53/27.93 % (1953493)Termination reason: Instruction limit % 196.53/27.93 % (1953493)Termination phase: Saturation % 196.53/27.93 % (1953493)Time elapsed: 0.164 s % 196.53/27.93 % (1953493)Peak memory usage: 13 MB % 196.53/27.93 % (1953493)Instructions burned: 360 (million) % 196.53/27.93 % (1953495)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=527886184:i=954:bd=all:rtra=on_2765 on theBenchmark for (2765ds/954Mi) % 196.53/27.93 % (1953491)Instruction limit reached! % 196.53/27.93 % (1953491)------------------------------ % 196.53/27.93 % (1953491)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 196.53/27.93 % (1953491)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 196.53/27.93 % (1953491)CaDiCaL version: 2.1.3 % 196.53/27.93 % (1953491)Termination reason: Instruction limit % 196.53/27.93 % (1953491)Termination phase: Saturation % 196.53/27.93 % (1953491)Time elapsed: 0.815 s % 196.53/27.93 % (1953491)Peak memory usage: 20 MB % 196.53/27.93 % (1953491)Instructions burned: 1368 (million) % 196.53/27.93 % (1953497)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=3493719391:fmbsr=1.3:i=1730:ins=25:rtra=on_2761 on theBenchmark for (2761ds/1730Mi) % 196.53/27.93 % (1953497)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 196.53/27.93 % (1953497)Terminated due to inappropriate strategy. % 196.53/27.93 % (1953497)------------------------------ % 196.53/27.93 % (1953497)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 196.53/27.93 % (1953497)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 196.53/27.93 % (1953497)CaDiCaL version: 2.1.3 % 196.53/27.93 % (1953497)Termination reason: Inappropriate % 196.53/27.93 % (1953497)Time elapsed: 0.001 s % 251.86/35.79 % (1953497)Peak memory usage: 10 MB % 251.86/35.79 % (1953497)Instructions burned: 2 (million) % 251.86/35.79 % (1953497)------------------------------ % 251.86/35.79 % (1953497)------------------------------ % 251.86/35.79 % (1953499)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=2753954985:i=2358:rtra=on_2761 on theBenchmark for (2761ds/2358Mi) % 251.86/35.79 % (1953495)Instruction limit reached! % 251.86/35.79 % (1953495)------------------------------ % 251.86/35.79 % (1953495)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 251.86/35.79 % (1953495)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 251.86/35.79 % (1953495)CaDiCaL version: 2.1.3 % 251.86/35.79 % (1953495)Termination reason: Instruction limit % 251.86/35.79 % (1953495)Termination phase: Saturation % 251.86/35.79 % (1953495)Time elapsed: 0.635 s % 251.86/35.79 % (1953495)Peak memory usage: 16 MB % 251.86/35.79 % (1953495)Instructions burned: 954 (million) % 251.86/35.79 % (1953501)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=507602120:i=1778:ins=1:rtra=on_2759 on theBenchmark for (2759ds/1778Mi) % 251.86/35.79 % (1953501)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 251.86/35.79 % (1953501)Terminated due to inappropriate strategy. % 251.86/35.79 % (1953501)------------------------------ % 251.86/35.79 % (1953501)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 251.86/35.79 % (1953501)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 251.86/35.79 % (1953501)CaDiCaL version: 2.1.3 % 251.86/35.79 % (1953501)Termination reason: Inappropriate % 251.86/35.79 % (1953501)Time elapsed: 0.002 s % 251.86/35.79 % (1953501)Peak memory usage: 10 MB % 251.86/35.79 % (1953501)Instructions burned: 2 (million) % 251.86/35.79 % (1953501)------------------------------ % 251.86/35.79 % (1953501)------------------------------ % 251.86/35.79 % (1953503)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=1571815544:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2758 on theBenchmark for (2758ds/1384Mi) % 251.86/35.79 % (1953503)Instruction limit reached! % 251.86/35.79 % (1953503)------------------------------ % 251.86/35.79 % (1953503)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 251.86/35.79 % (1953503)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 251.86/35.79 % (1953503)CaDiCaL version: 2.1.3 % 251.86/35.79 % (1953503)Termination reason: Instruction limit % 251.86/35.79 % (1953503)Termination phase: Saturation % 251.86/35.79 % (1953503)Time elapsed: 0.884 s % 251.86/35.79 % (1953503)Peak memory usage: 26 MB % 251.86/35.79 % (1953503)Instructions burned: 1384 (million) % 251.86/35.79 % (1953505)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=238659748:i=1758:kws=inv_precedence:fsr=off:rtra=on_2749 on theBenchmark for (2749ds/1758Mi) % 251.86/35.79 % (1953499)Instruction limit reached! % 251.86/35.79 % (1953499)------------------------------ % 251.86/35.79 % (1953499)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 251.86/35.79 % (1953499)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 251.86/35.79 % (1953499)CaDiCaL version: 2.1.3 % 251.86/35.79 % (1953499)Termination reason: Instruction limit % 251.86/35.79 % (1953499)Termination phase: Saturation % 251.86/35.79 % (1953499)Time elapsed: 1.551 s % 251.86/35.79 % (1953499)Peak memory usage: 27 MB % 251.86/35.79 % (1953499)Instructions burned: 2358 (million) % 251.86/35.79 % (1953507)fmb+10_1_sil=64000:si=on:random_seed=2842724728:i=44122:nm=2:rtra=on:gsp=on_2745 on theBenchmark for (2745ds/44122Mi) % 251.86/35.79 % (1953507)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 251.86/35.79 % (1953507)Terminated due to inappropriate strategy. % 251.86/35.79 % (1953507)------------------------------ % 251.86/35.79 % (1953507)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 251.86/35.79 % (1953507)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 251.86/35.79 % (1953507)CaDiCaL version: 2.1.3 % 251.86/35.79 % (1953507)Termination reason: Inappropriate % 251.86/35.79 % (1953507)Time elapsed: 0.002 s % 251.86/35.79 % (1953507)Peak memory usage: 10 MB % 251.86/35.79 % (1953507)Instructions burned: 2 (million) % 251.86/35.79 % (1953507)------------------------------ % 251.86/35.79 % (1953507)------------------------------ % 251.86/35.79 % (1953509)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=3336544221:i=19030:nm=5:rtra=on_2745 on theBenchmark for (2745ds/19030Mi) % 263.57/40.66 % (1953509)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 263.57/40.66 % (1953509)Terminated due to inappropriate strategy. % 263.57/40.66 % (1953509)------------------------------ % 263.57/40.66 % (1953509)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 263.57/40.66 % (1953509)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 263.57/40.66 % (1953509)CaDiCaL version: 2.1.3 % 263.57/40.66 % (1953509)Termination reason: Inappropriate % 263.57/40.66 % (1953509)Time elapsed: 0.002 s % 263.57/40.66 % (1953509)Peak memory usage: 10 MB % 263.57/40.66 % (1953509)Instructions burned: 2 (million) % 263.57/40.66 % (1953509)------------------------------ % 263.57/40.66 % (1953509)------------------------------ % 263.57/40.66 % (1953511)fmb+10_1_sil=64000:sas=cadical:si=on:fmbss=8:random_seed=206024056:fmbsr=1.7:i=1840:rtra=on_2745 on theBenchmark for (2745ds/1840Mi) % 263.57/40.66 % (1953511)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 263.57/40.66 % (1953511)Terminated due to inappropriate strategy. % 263.57/40.66 % (1953511)------------------------------ % 263.57/40.66 % (1953511)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 263.57/40.66 % (1953511)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 263.57/40.66 % (1953511)CaDiCaL version: 2.1.3 % 263.57/40.66 % (1953511)Termination reason: Inappropriate % 263.57/40.66 % (1953511)Time elapsed: 0.002 s % 263.57/40.66 % (1953511)Peak memory usage: 10 MB % 263.57/40.66 % (1953511)Instructions burned: 2 (million) % 263.57/40.66 % (1953511)------------------------------ % 263.57/40.66 % (1953511)------------------------------ % 263.57/40.66 % (1953513)dis-4_1_sil=16000:drc=ordering:si=on:sp=const_frequency:sac=on:newcnf=on:random_seed=1664863218:i=10262:rtra=on_2745 on theBenchmark for (2745ds/10262Mi) % 263.57/40.66 % (1953505)Instruction limit reached! % 263.57/40.66 % (1953505)------------------------------ % 263.57/40.66 % (1953505)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 263.57/40.66 % (1953505)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 263.57/40.66 % (1953505)CaDiCaL version: 2.1.3 % 263.57/40.66 % (1953505)Termination reason: Instruction limit % 263.57/40.66 % (1953505)Termination phase: Saturation % 263.57/40.66 % (1953505)Time elapsed: 1.009 s % 263.57/40.66 % (1953505)Peak memory usage: 29 MB % 263.57/40.66 % (1953505)Instructions burned: 1759 (million) % 263.57/40.66 % (1953545)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:si=on:sp=arity:spb=units:lsd=10:nwc=3:random_seed=225627436:i=2944:ins=7:rtra=on:fdi=8:gsp=on_2739 on theBenchmark for (2739ds/2944Mi) % 263.57/40.66 % (1953545)Instruction limit reached! % 263.57/40.66 % (1953545)------------------------------ % 263.57/40.66 % (1953545)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 263.57/40.66 % (1953545)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 263.57/40.66 % (1953545)CaDiCaL version: 2.1.3 % 263.57/40.66 % (1953545)Termination reason: Instruction limit % 263.57/40.66 % (1953545)Termination phase: Saturation % 263.57/40.66 % (1953545)Time elapsed: 1.610 s % 263.57/40.66 % (1953545)Peak memory usage: 29 MB % 263.57/40.66 % (1953545)Instructions burned: 2945 (million) % 263.57/40.66 % (1953876)fmb+10_1_sil=16000:sas=cadical:si=on:bce=on:fmbss=77:random_seed=1399705682:i=12648:rtra=on_2723 on theBenchmark for (2723ds/12648Mi) % 263.57/40.66 % (1953876)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 263.57/40.66 % (1953876)Terminated due to inappropriate strategy. % 263.57/40.66 % (1953876)------------------------------ % 263.57/40.66 % (1953876)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 263.57/40.66 % (1953876)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 263.57/40.66 % (1953876)CaDiCaL version: 2.1.3 % 263.57/40.66 % (1953876)Termination reason: Inappropriate % 263.57/40.66 % (1953876)Time elapsed: 0.002 s % 263.57/40.66 % (1953876)Peak memory usage: 11 MB % 263.57/40.66 % (1953876)Instructions burned: 2 (million) % 263.57/40.66 % (1953876)------------------------------ % 263.57/40.66 % (1953876)------------------------------ % 263.57/40.66 % (1953878)fmb+10_1_fmbas=function:sil=32000:sas=cadical:si=on:fmbss=16:random_seed=1727308529:fmbsr=2.30978:i=4348:rtra=on_2722 on theBenchmark for (2722ds/4348Mi) % 263.57/40.66 % (1953878)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 263.57/40.66 % (1953878)Terminated due to inappropriate strategy. % 263.57/40.66 % (1953878)------------------------------ % 263.57/40.66 % (1953878)Version: VampirTerminated % 300.14/42.53 % Vampire exiting %------------------------------------------------------------------------------