%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWX099_1 : TPTP v9.3.1. Released v9.1.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % Computer : n012.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 29 01:46:29 PM UTC 2026 % Result : Timeout 300.25s 42.73s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.01 % Problem : SWX099_1 : TPTP v9.3.1. Released v9.1.0. % 0.00/0.02 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.00/0.10 % Computer : n012.cluster.edu % 0.00/0.10 % Model : x86_64 x86_64 % 0.00/0.10 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.00/0.10 % Memory : 8046.5625MB % 0.00/0.10 % OS : Linux 6.8.0-71-generic % 0.00/0.10 % CPULimit : 300 % 0.00/0.10 % WCLimit : 300 % 0.00/0.10 % DateTime : Mon Sep 28 15:01:04 UTC 2026 % 0.00/0.10 % CPUTime : % 0.00/0.10 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.09/0.12 Running first-order model finding % 0.09/0.12 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 % 2.16/0.47 % (3438054)Will run a generic schedule for satisfiability detection. % 2.16/0.47 % (3438060)% WARNING: option uhcvi not known. % 2.16/0.47 % (3438059)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2262374600_2999 on theBenchmark for (2999ds/0Mi) % 2.16/0.47 % (3438060)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1335986531:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 2.16/0.47 % (3438061)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3560528198:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 2.16/0.47 % (3438062)dis+10_1_sil=32000:sp=arity:random_seed=82800587:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 2.16/0.47 % (3438063)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1177375889:i=116_2999 on theBenchmark for (2999ds/116Mi) % 2.16/0.47 % (3438064)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1821326462:i=131_2999 on theBenchmark for (2999ds/131Mi) % 2.16/0.47 % (3438065)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2517859518:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 2.16/0.47 % (3438059)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 2.16/0.47 % (3438059)Terminated due to inappropriate strategy. % 2.16/0.47 % (3438059)------------------------------ % 2.16/0.47 % (3438059)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 2.16/0.47 % (3438059)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 2.16/0.47 % (3438059)CaDiCaL version: 2.1.3 % 2.16/0.47 % (3438059)Termination reason: Inappropriate % 2.16/0.47 % (3438059)Time elapsed: 0.001 s % 2.16/0.47 % (3438059)Peak memory usage: 11 MB % 2.16/0.47 % (3438059)Instructions burned: 2 (million) % 2.16/0.47 % (3438059)------------------------------ % 2.16/0.47 % (3438059)------------------------------ % 2.16/0.47 % (3438073)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=4211984089:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 2.16/0.47 % (3438073)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 2.16/0.47 % (3438073)Terminated due to inappropriate strategy. % 2.16/0.47 % (3438073)------------------------------ % 2.16/0.47 % (3438073)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 2.16/0.47 % (3438073)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 2.16/0.47 % (3438073)CaDiCaL version: 2.1.3 % 2.16/0.47 % (3438073)Termination reason: Inappropriate % 2.16/0.47 % (3438073)Time elapsed: 0.0000 s % 2.16/0.47 % (3438073)Peak memory usage: 10 MB % 2.16/0.47 % (3438073)Instructions burned: 2 (million) % 2.16/0.47 % (3438073)------------------------------ % 2.16/0.47 % (3438073)------------------------------ % 2.16/0.47 % (3438075)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3348977015:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 2.16/0.47 % (3438062)Instruction limit reached! % 2.16/0.47 % (3438062)------------------------------ % 2.16/0.47 % (3438062)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 2.16/0.47 % (3438062)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 2.16/0.47 % (3438062)CaDiCaL version: 2.1.3 % 2.16/0.47 % (3438062)Termination reason: Instruction limit % 2.16/0.47 % (3438062)Termination phase: Saturation % 2.16/0.47 % (3438062)Time elapsed: 0.035 s % 2.16/0.47 % (3438062)Peak memory usage: 13 MB % 2.16/0.47 % (3438062)Instructions burned: 105 (million) % 2.16/0.47 % (3438063)Instruction limit reached! % 2.16/0.47 % (3438063)------------------------------ % 2.16/0.47 % (3438063)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 2.16/0.47 % (3438063)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 2.16/0.47 % (3438063)CaDiCaL version: 2.1.3 % 2.16/0.47 % (3438063)Termination reason: Instruction limit % 2.16/0.47 % (3438063)Termination phase: Saturation % 2.16/0.47 % (3438063)Time elapsed: 0.038 s % 2.16/0.47 % (3438063)Peak memory usage: 12 MB % 2.16/0.47 % (3438063)Instructions burned: 118 (million) % 2.16/0.47 % (3438064)Instruction limit reached! % 2.16/0.47 % (3438064)------------------------------ % 2.16/0.47 % (3438064)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 2.16/0.47 % (3438064)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 2.16/0.47 % (3438064)CaDiCaL version: 2.1.3 % 2.16/0.47 % (3438064)Termination reason: Instruction limit % 3.44/0.64 % (3438064)Termination phase: Saturation % 3.44/0.64 % (3438064)Time elapsed: 0.043 s % 3.44/0.64 % (3438064)Peak memory usage: 13 MB % 3.44/0.64 % (3438064)Instructions burned: 133 (million) % 3.44/0.64 % (3438077)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=2421751281:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi) % 3.44/0.64 % (3438078)ott-21_1_sil=16000:fs=off:random_seed=3359199945:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi) % 3.44/0.64 % (3438079)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2396236746:i=477:bd=all_2999 on theBenchmark for (2999ds/477Mi) % 3.44/0.64 % (3438065)Instruction limit reached! % 3.44/0.64 % (3438065)------------------------------ % 3.44/0.64 % (3438065)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.44/0.64 % (3438065)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.44/0.64 % (3438065)CaDiCaL version: 2.1.3 % 3.44/0.64 % (3438065)Termination reason: Instruction limit % 3.44/0.64 % (3438065)Termination phase: Saturation % 3.44/0.64 % (3438065)Time elapsed: 0.060 s % 3.44/0.64 % (3438065)Peak memory usage: 13 MB % 3.44/0.64 % (3438065)Instructions burned: 161 (million) % 3.44/0.64 % (3438083)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1420626888:fmbsr=1.3:i=865:ins=25_2999 on theBenchmark for (2999ds/865Mi) % 3.44/0.64 % (3438075)Instruction limit reached! % 3.44/0.64 % (3438075)------------------------------ % 3.44/0.64 % (3438075)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.44/0.64 % (3438075)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.44/0.64 % (3438075)CaDiCaL version: 2.1.3 % 3.44/0.64 % (3438075)Termination reason: Instruction limit % 3.44/0.64 % (3438075)Termination phase: Saturation % 3.44/0.64 % (3438075)Time elapsed: 0.048 s % 3.44/0.64 % (3438075)Peak memory usage: 13 MB % 3.44/0.64 % (3438075)Instructions burned: 131 (million) % 3.44/0.64 % (3438083)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.44/0.64 % (3438083)Terminated due to inappropriate strategy. % 3.44/0.64 % (3438083)------------------------------ % 3.44/0.64 % (3438083)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.44/0.64 % (3438083)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.44/0.64 % (3438083)CaDiCaL version: 2.1.3 % 3.44/0.64 % (3438083)Termination reason: Inappropriate % 3.44/0.64 % (3438083)Time elapsed: 0.001 s % 3.44/0.64 % (3438083)Peak memory usage: 10 MB % 3.44/0.64 % (3438083)Instructions burned: 3 (million) % 3.44/0.64 % (3438083)------------------------------ % 3.44/0.64 % (3438083)------------------------------ % 3.44/0.64 % (3438085)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1509009071:i=1179_2999 on theBenchmark for (2999ds/1179Mi) % 3.44/0.64 % (3438086)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3118309209:i=889:ins=1_2999 on theBenchmark for (2999ds/889Mi) % 3.44/0.64 % (3438086)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.44/0.64 % (3438086)Terminated due to inappropriate strategy. % 3.44/0.64 % (3438086)------------------------------ % 3.44/0.64 % (3438086)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.44/0.64 % (3438086)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.44/0.64 % (3438086)CaDiCaL version: 2.1.3 % 3.44/0.64 % (3438086)Termination reason: Inappropriate % 3.44/0.64 % (3438086)Time elapsed: 0.0000 s % 3.44/0.64 % (3438086)Peak memory usage: 10 MB % 3.44/0.64 % (3438086)Instructions burned: 1 (million) % 3.44/0.64 % (3438086)------------------------------ % 3.44/0.64 % (3438086)------------------------------ % 3.44/0.64 % (3438078)Instruction limit reached! % 3.44/0.64 % (3438078)------------------------------ % 3.44/0.64 % (3438078)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.44/0.64 % (3438078)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.44/0.64 % (3438078)CaDiCaL version: 2.1.3 % 3.44/0.64 % (3438078)Termination reason: Instruction limit % 3.44/0.64 % (3438078)Termination phase: Saturation % 3.44/0.64 % (3438078)Time elapsed: 0.043 s % 3.44/0.64 % (3438078)Peak memory usage: 12 MB % 3.44/0.64 % (3438078)Instructions burned: 184 (million) % 3.44/0.64 % (3438089)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=147155128: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) % 11.41/1.89 % (3438090)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=4122029426:i=879:kws=inv_precedence:fsr=off_2998 on theBenchmark for (2998ds/879Mi) % 11.41/1.89 % (3438079)Instruction limit reached! % 11.41/1.89 % (3438079)------------------------------ % 11.41/1.89 % (3438079)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 11.41/1.89 % (3438079)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.41/1.89 % (3438079)CaDiCaL version: 2.1.3 % 11.41/1.89 % (3438079)Termination reason: Instruction limit % 11.41/1.89 % (3438079)Termination phase: Saturation % 11.41/1.89 % (3438079)Time elapsed: 0.159 s % 11.41/1.89 % (3438079)Peak memory usage: 14 MB % 11.41/1.89 % (3438079)Instructions burned: 479 (million) % 11.41/1.89 % (3438093)fmb+10_1_sil=64000:random_seed=3206651656:i=22061:nm=2:gsp=on_2997 on theBenchmark for (2997ds/22061Mi) % 11.41/1.89 % (3438093)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 11.41/1.89 % (3438093)Terminated due to inappropriate strategy. % 11.41/1.89 % (3438093)------------------------------ % 11.41/1.89 % (3438093)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 11.41/1.89 % (3438093)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.41/1.89 % (3438093)CaDiCaL version: 2.1.3 % 11.41/1.89 % (3438093)Termination reason: Inappropriate % 11.41/1.89 % (3438093)Time elapsed: 0.001 s % 11.41/1.89 % (3438093)Peak memory usage: 10 MB % 11.41/1.89 % (3438093)Instructions burned: 2 (million) % 11.41/1.89 % (3438093)------------------------------ % 11.41/1.89 % (3438093)------------------------------ % 11.41/1.89 % (3438095)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2474319391:i=9515:nm=5_2997 on theBenchmark for (2997ds/9515Mi) % 11.41/1.89 % (3438095)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 11.41/1.89 % (3438095)Terminated due to inappropriate strategy. % 11.41/1.89 % (3438095)------------------------------ % 11.41/1.89 % (3438095)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 11.41/1.89 % (3438095)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.41/1.89 % (3438095)CaDiCaL version: 2.1.3 % 11.41/1.89 % (3438095)Termination reason: Inappropriate % 11.41/1.89 % (3438095)Time elapsed: 0.0000 s % 11.41/1.89 % (3438095)Peak memory usage: 10 MB % 11.41/1.89 % (3438095)Instructions burned: 2 (million) % 11.41/1.89 % (3438095)------------------------------ % 11.41/1.89 % (3438095)------------------------------ % 11.41/1.89 % (3438077)Instruction limit reached! % 11.41/1.89 % (3438077)------------------------------ % 11.41/1.89 % (3438077)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 11.41/1.89 % (3438077)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.41/1.89 % (3438077)CaDiCaL version: 2.1.3 % 11.41/1.89 % (3438077)Termination reason: Instruction limit % 11.41/1.89 % (3438077)Termination phase: Saturation % 11.41/1.89 % (3438077)Time elapsed: 0.200 s % 11.41/1.89 % (3438077)Peak memory usage: 14 MB % 11.41/1.89 % (3438077)Instructions burned: 686 (million) % 11.41/1.89 % (3438097)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1014434388:fmbsr=1.7:i=920_2997 on theBenchmark for (2997ds/920Mi) % 11.41/1.89 % (3438097)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 11.41/1.89 % (3438097)Terminated due to inappropriate strategy. % 11.41/1.89 % (3438097)------------------------------ % 11.41/1.89 % (3438097)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 11.41/1.89 % (3438097)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.41/1.89 % (3438097)CaDiCaL version: 2.1.3 % 11.41/1.89 % (3438097)Termination reason: Inappropriate % 11.41/1.89 % (3438097)Time elapsed: 0.0000 s % 11.41/1.89 % (3438097)Peak memory usage: 10 MB % 11.41/1.89 % (3438097)Instructions burned: 2 (million) % 11.41/1.89 % (3438097)------------------------------ % 11.41/1.89 % (3438097)------------------------------ % 11.41/1.89 % (3438098)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1769775157:i=5131_2997 on theBenchmark for (2997ds/5131Mi) % 11.41/1.89 % (3438100)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=378912633:i=1472:ins=7:fdi=8:gsp=on_2997 on theBenchmark for (2997ds/1472Mi) % 11.41/1.89 % (3438089)Instruction limit reached! % 11.41/1.89 % (3438089)------------------------------ % 17.12/2.68 % (3438089)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 17.12/2.68 % (3438089)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.12/2.68 % (3438089)CaDiCaL version: 2.1.3 % 17.12/2.68 % (3438089)Termination reason: Instruction limit % 17.12/2.68 % (3438089)Termination phase: Saturation % 17.12/2.68 % (3438089)Time elapsed: 0.238 s % 17.12/2.68 % (3438089)Peak memory usage: 18 MB % 17.12/2.68 % (3438089)Instructions burned: 692 (million) % 17.12/2.68 % (3438103)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=429212339:i=6324_2996 on theBenchmark for (2996ds/6324Mi) % 17.12/2.68 % (3438103)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 17.12/2.68 % (3438103)Terminated due to inappropriate strategy. % 17.12/2.68 % (3438103)------------------------------ % 17.12/2.68 % (3438103)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 17.12/2.68 % (3438103)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.12/2.68 % (3438103)CaDiCaL version: 2.1.3 % 17.12/2.68 % (3438103)Termination reason: Inappropriate % 17.12/2.68 % (3438103)Time elapsed: 0.001 s % 17.12/2.68 % (3438103)Peak memory usage: 11 MB % 17.12/2.68 % (3438103)Instructions burned: 2 (million) % 17.12/2.68 % (3438103)------------------------------ % 17.12/2.68 % (3438103)------------------------------ % 17.12/2.68 % (3438105)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=596100648:fmbsr=2.30978:i=2174_2996 on theBenchmark for (2996ds/2174Mi) % 17.12/2.68 % (3438105)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 17.12/2.68 % (3438105)Terminated due to inappropriate strategy. % 17.12/2.68 % (3438105)------------------------------ % 17.12/2.68 % (3438105)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 17.12/2.68 % (3438105)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.12/2.68 % (3438105)CaDiCaL version: 2.1.3 % 17.12/2.68 % (3438105)Termination reason: Inappropriate % 17.12/2.68 % (3438105)Time elapsed: 0.0000 s % 17.12/2.68 % (3438105)Peak memory usage: 10 MB % 17.12/2.68 % (3438105)Instructions burned: 2 (million) % 17.12/2.68 % (3438105)------------------------------ % 17.12/2.68 % (3438105)------------------------------ % 17.12/2.68 % (3438090)Instruction limit reached! % 17.12/2.68 % (3438090)------------------------------ % 17.12/2.68 % (3438090)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 17.12/2.68 % (3438090)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.12/2.68 % (3438090)CaDiCaL version: 2.1.3 % 17.12/2.68 % (3438090)Termination reason: Instruction limit % 17.12/2.68 % (3438090)Termination phase: Saturation % 17.12/2.68 % (3438090)Time elapsed: 0.263 s % 17.12/2.68 % (3438090)Peak memory usage: 19 MB % 17.12/2.68 % (3438090)Instructions burned: 880 (million) % 17.12/2.68 % (3438107)ott-2_1_sil=16000:newcnf=on:random_seed=3129292025:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2996 on theBenchmark for (2996ds/869Mi) % 17.12/2.68 % (3438108)ott+10_1_sil=32000:tgt=ground:random_seed=1675194640:i=5114:av=off_2996 on theBenchmark for (2996ds/5114Mi) % 17.12/2.68 % (3438085)Instruction limit reached! % 17.12/2.68 % (3438085)------------------------------ % 17.12/2.68 % (3438085)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 17.12/2.68 % (3438085)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.12/2.68 % (3438085)CaDiCaL version: 2.1.3 % 17.12/2.68 % (3438085)Termination reason: Instruction limit % 17.12/2.68 % (3438085)Termination phase: Saturation % 17.12/2.68 % (3438085)Time elapsed: 0.404 s % 17.12/2.68 % (3438085)Peak memory usage: 20 MB % 17.12/2.68 % (3438085)Instructions burned: 1179 (million) % 17.12/2.68 % (3438111)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2662037786:i=54282_2994 on theBenchmark for (2994ds/54282Mi) % 17.12/2.68 % (3438111)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 17.12/2.68 % (3438111)Terminated due to inappropriate strategy. % 17.12/2.68 % (3438111)------------------------------ % 17.12/2.68 % (3438111)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 17.12/2.68 % (3438111)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.12/2.68 % (3438111)CaDiCaL version: 2.1.3 % 17.12/2.68 % (3438111)Termination reason: Inappropriate % 17.12/2.68 % (3438111)Time elapsed: 0.001 s % 17.12/2.68 % (3438111)Peak memory usage: 11 MB % 17.12/2.68 % (3438111)Instructions burned: 2 (million) % 63.40/9.16 % (3438111)------------------------------ % 63.40/9.16 % (3438111)------------------------------ % 63.40/9.16 % (3438113)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3410089862:i=3512:aac=none_2994 on theBenchmark for (2994ds/3512Mi) % 63.40/9.16 % (3438107)Instruction limit reached! % 63.40/9.16 % (3438107)------------------------------ % 63.40/9.16 % (3438107)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 63.40/9.16 % (3438107)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 63.40/9.16 % (3438107)CaDiCaL version: 2.1.3 % 63.40/9.16 % (3438107)Termination reason: Instruction limit % 63.40/9.16 % (3438107)Termination phase: Saturation % 63.40/9.16 % (3438107)Time elapsed: 0.279 s % 63.40/9.16 % (3438107)Peak memory usage: 16 MB % 63.40/9.16 % (3438107)Instructions burned: 870 (million) % 63.40/9.16 % (3438115)dis+21_1_sil=32000:sas=cadical:random_seed=3829897176:i=3773:amm=off_2993 on theBenchmark for (2993ds/3773Mi) % 63.40/9.16 % (3438100)Instruction limit reached! % 63.40/9.16 % (3438100)------------------------------ % 63.40/9.16 % (3438100)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 63.40/9.16 % (3438100)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 63.40/9.16 % (3438100)CaDiCaL version: 2.1.3 % 63.40/9.16 % (3438100)Termination reason: Instruction limit % 63.40/9.16 % (3438100)Termination phase: Saturation % 63.40/9.16 % (3438100)Time elapsed: 0.455 s % 63.40/9.16 % (3438100)Peak memory usage: 29 MB % 63.40/9.16 % (3438100)Instructions burned: 1472 (million) % 63.40/9.16 % (3438117)ott+11_1_sil=16000:gs=on:random_seed=3000797292:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2992 on theBenchmark for (2992ds/2251Mi) % 63.40/9.16 % (3438117)Instruction limit reached! % 63.40/9.16 % (3438117)------------------------------ % 63.40/9.16 % (3438117)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 63.40/9.16 % (3438117)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 63.40/9.16 % (3438117)CaDiCaL version: 2.1.3 % 63.40/9.16 % (3438117)Termination reason: Instruction limit % 63.40/9.16 % (3438117)Termination phase: Saturation % 63.40/9.16 % (3438117)Time elapsed: 0.685 s % 63.40/9.16 % (3438117)Peak memory usage: 23 MB % 63.40/9.16 % (3438117)Instructions burned: 2251 (million) % 63.40/9.16 % (3438119)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=2592942693:fmbsr=1.6:i=67534_2985 on theBenchmark for (2985ds/67534Mi) % 63.40/9.16 % (3438119)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 63.40/9.16 % (3438119)Terminated due to inappropriate strategy. % 63.40/9.16 % (3438119)------------------------------ % 63.40/9.16 % (3438119)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 63.40/9.16 % (3438119)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 63.40/9.16 % (3438119)CaDiCaL version: 2.1.3 % 63.40/9.16 % (3438119)Termination reason: Inappropriate % 63.40/9.16 % (3438119)Time elapsed: 0.001 s % 63.40/9.16 % (3438119)Peak memory usage: 10 MB % 63.40/9.16 % (3438119)Instructions burned: 2 (million) % 63.40/9.16 % (3438119)------------------------------ % 63.40/9.16 % (3438119)------------------------------ % 63.40/9.16 % (3438121)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=4160102524:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2985 on theBenchmark for (2985ds/4591Mi) % 63.40/9.16 % (3438113)Instruction limit reached! % 63.40/9.16 % (3438113)------------------------------ % 63.40/9.16 % (3438113)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 63.40/9.16 % (3438113)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 63.40/9.16 % (3438113)CaDiCaL version: 2.1.3 % 63.40/9.16 % (3438113)Termination reason: Instruction limit % 63.40/9.16 % (3438113)Termination phase: Saturation % 63.40/9.16 % (3438113)Time elapsed: 1.026 s % 63.40/9.16 % (3438113)Peak memory usage: 30 MB % 63.40/9.16 % (3438113)Instructions burned: 3515 (million) % 63.40/9.16 % (3438123)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=929979805:i=29340_2984 on theBenchmark for (2984ds/29340Mi) % 63.40/9.16 % (3438115)Instruction limit reached! % 63.40/9.16 % (3438115)------------------------------ % 63.40/9.16 % (3438115)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 63.40/9.16 % (3438115)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 63.40/9.16 % (3438115)CaDiCaL version: 2.1.3 % 63.40/9.16 % (3438115)Termination reason: Instruction limit % 71.63/10.30 % (3438115)Termination phase: Saturation % 71.63/10.30 % (3438115)Time elapsed: 1.091 s % 71.63/10.30 % (3438115)Peak memory usage: 32 MB % 71.63/10.30 % (3438115)Instructions burned: 3777 (million) % 71.63/10.30 % (3438125)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=4249214182:i=5211_2982 on theBenchmark for (2982ds/5211Mi) % 71.63/10.30 % (3438098)Instruction limit reached! % 71.63/10.30 % (3438098)------------------------------ % 71.63/10.30 % (3438098)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 71.63/10.30 % (3438098)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 71.63/10.30 % (3438098)CaDiCaL version: 2.1.3 % 71.63/10.30 % (3438098)Termination reason: Instruction limit % 71.63/10.30 % (3438098)Termination phase: Saturation % 71.63/10.30 % (3438098)Time elapsed: 1.513 s % 71.63/10.30 % (3438098)Peak memory usage: 43 MB % 71.63/10.30 % (3438098)Instructions burned: 5134 (million) % 71.63/10.30 % (3438127)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=1469454083:i=5497:nm=2_2982 on theBenchmark for (2982ds/5497Mi) % 71.63/10.30 % (3438127)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 71.63/10.30 % (3438127)Terminated due to inappropriate strategy. % 71.63/10.30 % (3438127)------------------------------ % 71.63/10.30 % (3438127)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 71.63/10.30 % (3438127)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 71.63/10.30 % (3438127)CaDiCaL version: 2.1.3 % 71.63/10.30 % (3438127)Termination reason: Inappropriate % 71.63/10.30 % (3438127)Time elapsed: 0.001 s % 71.63/10.30 % (3438127)Peak memory usage: 11 MB % 71.63/10.30 % (3438127)Instructions burned: 2 (million) % 71.63/10.30 % (3438127)------------------------------ % 71.63/10.30 % (3438127)------------------------------ % 71.63/10.30 % (3438129)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=3200069467:fmbsr=2:i=46332_2981 on theBenchmark for (2981ds/46332Mi) % 71.63/10.30 % (3438129)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 71.63/10.30 % (3438129)Terminated due to inappropriate strategy. % 71.63/10.30 % (3438129)------------------------------ % 71.63/10.30 % (3438129)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 71.63/10.30 % (3438129)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 71.63/10.30 % (3438129)CaDiCaL version: 2.1.3 % 71.63/10.30 % (3438129)Termination reason: Inappropriate % 71.63/10.30 % (3438129)Time elapsed: 0.001 s % 71.63/10.30 % (3438129)Peak memory usage: 11 MB % 71.63/10.30 % (3438129)Instructions burned: 2 (million) % 71.63/10.30 % (3438129)------------------------------ % 71.63/10.30 % (3438129)------------------------------ % 71.63/10.30 % (3438131)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=3443552921:i=14071_2981 on theBenchmark for (2981ds/14071Mi) % 71.63/10.30 % (3438131)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 71.63/10.30 % (3438131)Terminated due to inappropriate strategy. % 71.63/10.30 % (3438131)------------------------------ % 71.63/10.30 % (3438131)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 71.63/10.30 % (3438131)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 71.63/10.30 % (3438131)CaDiCaL version: 2.1.3 % 71.63/10.30 % (3438131)Termination reason: Inappropriate % 71.63/10.30 % (3438131)Time elapsed: 0.001 s % 71.63/10.30 % (3438131)Peak memory usage: 10 MB % 71.63/10.30 % (3438131)Instructions burned: 2 (million) % 71.63/10.30 % (3438131)------------------------------ % 71.63/10.30 % (3438131)------------------------------ % 71.63/10.30 % (3438133)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=776862356:i=22565:add=on:rawr=on_2981 on theBenchmark for (2981ds/22565Mi) % 71.63/10.30 % (3438108)Instruction limit reached! % 71.63/10.30 % (3438108)------------------------------ % 71.63/10.30 % (3438108)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 71.63/10.30 % (3438108)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 71.63/10.30 % (3438108)CaDiCaL version: 2.1.3 % 71.63/10.30 % (3438108)Termination reason: Instruction limit % 71.63/10.30 % (3438108)Termination phase: Saturation % 71.63/10.30 % (3438108)Time elapsed: 1.804 s % 71.63/10.30 % (3438108)Peak memory usage: 34 MB % 71.63/10.30 % (3438108)Instructions burned: 5116 (million) % 71.63/10.30 % (3438135)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=1081302821:i=8173:av=off_2977 on theBenchmark for (2977ds/8173Mi) % 71.63/10.30 % (3438121)Instruction limit reached! % 71.63/10.37 % (3438121)------------------------------ % 71.63/10.37 % (3438121)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 71.63/10.37 % (3438121)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 71.63/10.37 % (3438121)CaDiCaL version: 2.1.3 % 71.63/10.37 % (3438121)Termination reason: Instruction limit % 71.63/10.37 % (3438121)Termination phase: Saturation % 71.63/10.37 % (3438121)Time elapsed: 1.099 s % 71.63/10.37 % (3438121)Peak memory usage: 35 MB % 71.63/10.37 % (3438121)Instructions burned: 4595 (million) % 71.63/10.37 % (3438137)dis+10_16:1_sil=16000:random_seed=2036276148:i=9155:fsr=off_2974 on theBenchmark for (2974ds/9155Mi) % 71.63/10.37 % (3438125)Instruction limit reached! % 71.63/10.37 % (3438125)------------------------------ % 71.63/10.37 % (3438125)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 71.63/10.37 % (3438125)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 71.63/10.37 % (3438125)CaDiCaL version: 2.1.3 % 71.63/10.37 % (3438125)Termination reason: Instruction limit % 71.63/10.37 % (3438125)Termination phase: Saturation % 71.63/10.37 % (3438125)Time elapsed: 1.507 s % 71.63/10.37 % (3438125)Peak memory usage: 48 MB % 71.63/10.37 % (3438125)Instructions burned: 5213 (million) % 71.63/10.37 % (3438139)ott-3_8_sil=64000:random_seed=3072872712:i=20139:bs=on_2967 on theBenchmark for (2967ds/20139Mi) % 71.63/10.37 % (3438135)Instruction limit reached! % 71.63/10.37 % (3438135)------------------------------ % 71.63/10.37 % (3438135)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 71.63/10.37 % (3438135)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 71.63/10.37 % (3438135)CaDiCaL version: 2.1.3 % 71.63/10.37 % (3438135)Termination reason: Instruction limit % 71.63/10.37 % (3438135)Termination phase: Saturation % 71.63/10.37 % (3438135)Time elapsed: 2.815 s % 71.63/10.37 % (3438135)Peak memory usage: 55 MB % 71.63/10.37 % (3438135)Instructions burned: 8174 (million) % 71.63/10.37 % (3438141)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=2627597932:fmbsr=2:i=32576_2949 on theBenchmark for (2949ds/32576Mi) % 71.63/10.37 % (3438141)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 71.63/10.37 % (3438141)Terminated due to inappropriate strategy. % 71.63/10.37 % (3438141)------------------------------ % 71.63/10.37 % (3438141)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 71.63/10.37 % (3438141)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 71.63/10.37 % (3438141)CaDiCaL version: 2.1.3 % 71.63/10.37 % (3438141)Termination reason: Inappropriate % 71.63/10.37 % (3438141)Time elapsed: 0.001 s % 71.63/10.37 % (3438141)Peak memory usage: 11 MB % 71.63/10.37 % (3438141)Instructions burned: 2 (million) % 71.63/10.37 % (3438141)------------------------------ % 71.63/10.37 % (3438141)------------------------------ % 71.63/10.37 % (3438143)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=1408596660:i=11404_2949 on theBenchmark for (2949ds/11404Mi) % 71.63/10.37 % (3438137)Instruction limit reached! % 71.63/10.37 % (3438137)------------------------------ % 71.63/10.37 % (3438137)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 71.63/10.37 % (3438137)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 71.63/10.37 % (3438137)CaDiCaL version: 2.1.3 % 71.63/10.37 % (3438137)Termination reason: Instruction limit % 71.63/10.37 % (3438137)Termination phase: Saturation % 71.63/10.37 % (3438137)Time elapsed: 2.505 s % 71.63/10.37 % (3438137)Peak memory usage: 52 MB % 71.63/10.37 % (3438137)Instructions burned: 9158 (million) % 71.63/10.37 % (3438145)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=1184840260:i=14134_2949 on theBenchmark for (2949ds/14134Mi) % 71.63/10.37 % (3438133)Instruction limit reached! % 71.63/10.37 % (3438133)------------------------------ % 71.63/10.37 % (3438133)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 71.63/10.37 % (3438133)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 71.63/10.37 % (3438133)CaDiCaL version: 2.1.3 % 71.63/10.37 % (3438133)Termination reason: Instruction limit % 71.63/10.37 % (3438133)Termination phase: Saturation % 71.63/10.37 % (3438133)Time elapsed: 5.139 s % 71.63/10.37 % (3438133)Peak memory usage: 74 MB % 71.63/10.37 % (3438133)Instructions burned: 22567 (million) % 71.63/10.37 % (3438147)dis+33_16_sil=32000:sac=on:random_seed=1782913387:i=15851:nm=0_2930 on theBenchmark for (2930ds/15851Mi) % 71.63/10.37 % (3438143)Instruction limit reached! % 71.63/10.37 % (3438143)------------------------------ % 71.63/10.37 % (3438143)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 111.14/15.96 % (3438143)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 111.14/15.96 % (3438143)CaDiCaL version: 2.1.3 % 111.14/15.96 % (3438143)Termination reason: Instruction limit % 111.14/15.96 % (3438143)Termination phase: Saturation % 111.14/15.96 % (3438143)Time elapsed: 3.983 s % 111.14/15.96 % (3438143)Peak memory usage: 60 MB % 111.14/15.96 % (3438143)Instructions burned: 11405 (million) % 111.14/15.96 % (3438149)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=3914091453:avsq=on:i=17627:add=on:amm=off_2909 on theBenchmark for (2909ds/17627Mi) % 111.14/15.96 % (3438123)Instruction limit reached! % 111.14/15.96 % (3438123)------------------------------ % 111.14/15.96 % (3438123)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 111.14/15.96 % (3438123)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 111.14/15.96 % (3438123)CaDiCaL version: 2.1.3 % 111.14/15.96 % (3438123)Termination reason: Instruction limit % 111.14/15.96 % (3438123)Termination phase: Saturation % 111.14/15.96 % (3438123)Time elapsed: 7.961 s % 111.14/15.96 % (3438123)Peak memory usage: 180 MB % 111.14/15.96 % (3438123)Instructions burned: 29343 (million) % 111.14/15.96 % (3438151)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=1837229854:s2a=on:i=53295_2904 on theBenchmark for (2904ds/53295Mi) % 111.14/15.96 % (3438139)Instruction limit reached! % 111.14/15.96 % (3438139)------------------------------ % 111.14/15.96 % (3438139)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 111.14/15.96 % (3438139)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 111.14/15.96 % (3438139)CaDiCaL version: 2.1.3 % 111.14/15.96 % (3438139)Termination reason: Instruction limit % 111.14/15.96 % (3438139)Termination phase: Saturation % 111.14/15.96 % (3438139)Time elapsed: 6.751 s % 111.14/15.96 % (3438139)Peak memory usage: 85 MB % 111.14/15.96 % (3438139)Instructions burned: 20139 (million) % 111.14/15.96 % (3438153)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=3223547862:i=26857:ins=20_2899 on theBenchmark for (2899ds/26857Mi) % 111.14/15.96 % (3438153)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 111.14/15.96 % (3438153)Terminated due to inappropriate strategy. % 111.14/15.96 % (3438153)------------------------------ % 111.14/15.96 % (3438153)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 111.14/15.96 % (3438153)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 111.14/15.96 % (3438153)CaDiCaL version: 2.1.3 % 111.14/15.96 % (3438153)Termination reason: Inappropriate % 111.14/15.96 % (3438153)Time elapsed: 0.001 s % 111.14/15.96 % (3438153)Peak memory usage: 10 MB % 111.14/15.96 % (3438153)Instructions burned: 2 (million) % 111.14/15.96 % (3438153)------------------------------ % 111.14/15.96 % (3438153)------------------------------ % 111.14/15.96 % (3438155)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=1126835553:i=28120:bs=on:fsr=off_2899 on theBenchmark for (2899ds/28120Mi) % 111.14/15.96 % (3438145)Instruction limit reached! % 111.14/15.96 % (3438145)------------------------------ % 111.14/15.96 % (3438145)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 111.14/15.96 % (3438145)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 111.14/15.96 % (3438145)CaDiCaL version: 2.1.3 % 111.14/15.96 % (3438145)Termination reason: Instruction limit % 111.14/15.96 % (3438145)Termination phase: Saturation % 111.14/15.96 % (3438145)Time elapsed: 5.061 s % 111.14/15.96 % (3438145)Peak memory usage: 70 MB % 111.14/15.96 % (3438145)Instructions burned: 14136 (million) % 111.14/15.96 % (3438157)fmb+10_1_sil=256000:fmbss=7:random_seed=4013574867:fmbsr=1.6:i=182295_2898 on theBenchmark for (2898ds/182295Mi) % 111.14/15.96 % (3438157)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 111.14/15.96 % (3438157)Terminated due to inappropriate strategy. % 111.14/15.96 % (3438157)------------------------------ % 111.14/15.96 % (3438157)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 111.14/15.96 % (3438157)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 111.14/15.96 % (3438157)CaDiCaL version: 2.1.3 % 111.14/15.96 % (3438157)Termination reason: Inappropriate % 111.14/15.96 % (3438157)Time elapsed: 0.001 s % 111.14/15.96 % (3438157)Peak memory usage: 10 MB % 111.14/15.96 % (3438157)Instructions burned: 2 (million) % 111.14/15.96 % (3438157)------------------------------ % 111.14/15.96 % (3438157)------------------------------ % 111.14/15.96 % (3438159)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=3590733089:i=44625:gsp=on_2898 on theBenchmark for (2898ds/44625Mi) % 117.98/16.99 % (3438159)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 117.98/16.99 % (3438159)Terminated due to inappropriate strategy. % 117.98/16.99 % (3438159)------------------------------ % 117.98/16.99 % (3438159)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 117.98/16.99 % (3438159)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 117.98/16.99 % (3438159)CaDiCaL version: 2.1.3 % 117.98/16.99 % (3438159)Termination reason: Inappropriate % 117.98/16.99 % (3438159)Time elapsed: 0.001 s % 117.98/16.99 % (3438159)Peak memory usage: 10 MB % 117.98/16.99 % (3438159)Instructions burned: 2 (million) % 117.98/16.99 % (3438159)------------------------------ % 117.98/16.99 % (3438159)------------------------------ % 117.98/16.99 % (3438161)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=2338865681:i=160505_2898 on theBenchmark for (2898ds/160505Mi) % 117.98/16.99 % (3438161)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 117.98/16.99 % (3438161)Terminated due to inappropriate strategy. % 117.98/16.99 % (3438161)------------------------------ % 117.98/16.99 % (3438161)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 117.98/16.99 % (3438161)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 117.98/16.99 % (3438161)CaDiCaL version: 2.1.3 % 117.98/16.99 % (3438161)Termination reason: Inappropriate % 117.98/16.99 % (3438161)Time elapsed: 0.001 s % 117.98/16.99 % (3438161)Peak memory usage: 10 MB % 117.98/16.99 % (3438161)Instructions burned: 2 (million) % 117.98/16.99 % (3438161)------------------------------ % 117.98/16.99 % (3438161)------------------------------ % 117.98/16.99 % (3438163)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=4269880445:fmbsr=1.3:i=225729_2898 on theBenchmark for (2898ds/225729Mi) % 117.98/16.99 % (3438163)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 117.98/16.99 % (3438163)Terminated due to inappropriate strategy. % 117.98/16.99 % (3438163)------------------------------ % 117.98/16.99 % (3438163)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 117.98/16.99 % (3438163)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 117.98/16.99 % (3438163)CaDiCaL version: 2.1.3 % 117.98/16.99 % (3438163)Termination reason: Inappropriate % 117.98/16.99 % (3438163)Time elapsed: 0.001 s % 117.98/16.99 % (3438163)Peak memory usage: 10 MB % 117.98/16.99 % (3438163)Instructions burned: 2 (million) % 117.98/16.99 % (3438163)------------------------------ % 117.98/16.99 % (3438163)------------------------------ % 117.98/16.99 % (3438165)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=12521235:fmbsr=2:i=185024:ins=7_2897 on theBenchmark for (2897ds/185024Mi) % 117.98/16.99 % (3438165)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 117.98/16.99 % (3438165)Terminated due to inappropriate strategy. % 117.98/16.99 % (3438165)------------------------------ % 117.98/16.99 % (3438165)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 117.98/16.99 % (3438165)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 117.98/16.99 % (3438165)CaDiCaL version: 2.1.3 % 117.98/16.99 % (3438165)Termination reason: Inappropriate % 117.98/16.99 % (3438165)Time elapsed: 0.001 s % 117.98/16.99 % (3438165)Peak memory usage: 10 MB % 117.98/16.99 % (3438165)Instructions burned: 2 (million) % 117.98/16.99 % (3438165)------------------------------ % 117.98/16.99 % (3438165)------------------------------ % 117.98/16.99 % (3438167)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=793062838:rtra=on_2897 on theBenchmark for (2897ds/0Mi) % 117.98/16.99 % (3438167)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 117.98/16.99 % (3438167)Terminated due to inappropriate strategy. % 117.98/16.99 % (3438167)------------------------------ % 117.98/16.99 % (3438167)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 117.98/16.99 % (3438167)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 117.98/16.99 % (3438167)CaDiCaL version: 2.1.3 % 117.98/16.99 % (3438167)Termination reason: Inappropriate % 117.98/16.99 % (3438167)Time elapsed: 0.001 s % 117.98/16.99 % (3438167)Peak memory usage: 11 MB % 117.98/16.99 % (3438167)Instructions burned: 2 (million) % 117.98/16.99 % (3438167)------------------------------ % 117.98/16.99 % (3438167)------------------------------ % 117.98/16.99 % (3438169)% WARNING: option uhcvi not known. % 117.98/16.99 % (3438169)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1524068305:i=271062:add=off:rtra=on:rawr=on_2897 on theBenchmark for (2897ds/271062Mi) % 127.86/18.31 % (3438147)Instruction limit reached! % 127.86/18.31 % (3438147)------------------------------ % 127.86/18.31 % (3438147)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 127.86/18.31 % (3438147)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 127.86/18.31 % (3438147)CaDiCaL version: 2.1.3 % 127.86/18.31 % (3438147)Termination reason: Instruction limit % 127.86/18.31 % (3438147)Termination phase: Saturation % 127.86/18.31 % (3438147)Time elapsed: 4.697 s % 127.86/18.31 % (3438147)Peak memory usage: 116 MB % 127.86/18.31 % (3438147)Instructions burned: 15851 (million) % 127.86/18.31 % (3438171)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1040809095:i=176048:add=on:rtra=on:rawr=on_2882 on theBenchmark for (2882ds/176048Mi) % 127.86/18.31 % (3438149)Instruction limit reached! % 127.86/18.31 % (3438149)------------------------------ % 127.86/18.31 % (3438149)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 127.86/18.31 % (3438149)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 127.86/18.31 % (3438149)CaDiCaL version: 2.1.3 % 127.86/18.31 % (3438149)Termination reason: Instruction limit % 127.86/18.31 % (3438149)Termination phase: Saturation % 127.86/18.31 % (3438149)Time elapsed: 6.346 s % 127.86/18.31 % (3438149)Peak memory usage: 92 MB % 127.86/18.31 % (3438149)Instructions burned: 17628 (million) % 127.86/18.31 % (3438173)dis+10_1_sil=32000:si=on:sp=arity:random_seed=246449995:i=206:fgj=on:rtra=on_2845 on theBenchmark for (2845ds/206Mi) % 127.86/18.31 % (3438173)Instruction limit reached! % 127.86/18.31 % (3438173)------------------------------ % 127.86/18.31 % (3438173)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 127.86/18.31 % (3438173)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 127.86/18.31 % (3438173)CaDiCaL version: 2.1.3 % 127.86/18.31 % (3438173)Termination reason: Instruction limit % 127.86/18.31 % (3438173)Termination phase: Saturation % 127.86/18.31 % (3438173)Time elapsed: 0.071 s % 127.86/18.31 % (3438173)Peak memory usage: 13 MB % 127.86/18.31 % (3438173)Instructions burned: 207 (million) % 127.86/18.31 % (3438175)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=150640725:i=232:rtra=on_2845 on theBenchmark for (2845ds/232Mi) % 127.86/18.31 % (3438175)Instruction limit reached! % 127.86/18.31 % (3438175)------------------------------ % 127.86/18.31 % (3438175)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 127.86/18.31 % (3438175)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 127.86/18.31 % (3438175)CaDiCaL version: 2.1.3 % 127.86/18.31 % (3438175)Termination reason: Instruction limit % 127.86/18.31 % (3438175)Termination phase: Saturation % 127.86/18.31 % (3438175)Time elapsed: 0.080 s % 127.86/18.31 % (3438175)Peak memory usage: 13 MB % 127.86/18.31 % (3438175)Instructions burned: 232 (million) % 127.86/18.31 % (3438177)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=4060702562:i=262:rtra=on_2844 on theBenchmark for (2844ds/262Mi) % 127.86/18.31 % (3438177)Instruction limit reached! % 127.86/18.31 % (3438177)------------------------------ % 127.86/18.31 % (3438177)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 127.86/18.31 % (3438177)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 127.86/18.31 % (3438177)CaDiCaL version: 2.1.3 % 127.86/18.31 % (3438177)Termination reason: Instruction limit % 127.86/18.31 % (3438177)Termination phase: Saturation % 127.86/18.31 % (3438177)Time elapsed: 0.089 s % 127.86/18.31 % (3438177)Peak memory usage: 14 MB % 127.86/18.31 % (3438177)Instructions burned: 264 (million) % 127.86/18.31 % (3438179)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=2582837810:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2843 on theBenchmark for (2843ds/318Mi) % 127.86/18.31 % (3438179)Instruction limit reached! % 127.86/18.31 % (3438179)------------------------------ % 127.86/18.31 % (3438179)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 127.86/18.31 % (3438179)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 127.86/18.31 % (3438179)CaDiCaL version: 2.1.3 % 127.86/18.31 % (3438179)Termination reason: Instruction limit % 127.86/18.31 % (3438179)Termination phase: Saturation % 127.86/18.31 % (3438179)Time elapsed: 0.124 s % 127.86/18.31 % (3438179)Peak memory usage: 15 MB % 127.86/18.31 % (3438179)Instructions burned: 319 (million) % 127.86/18.31 % (3438181)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=4148952328:i=1428:nm=2:rtra=on_2841 on theBenchmark for (2841ds/1428Mi) % 137.31/19.69 % (3438181)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 137.31/19.69 % (3438181)Terminated due to inappropriate strategy. % 137.31/19.69 % (3438181)------------------------------ % 137.31/19.69 % (3438181)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 137.31/19.69 % (3438181)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 137.31/19.69 % (3438181)CaDiCaL version: 2.1.3 % 137.31/19.69 % (3438181)Termination reason: Inappropriate % 137.31/19.69 % (3438181)Time elapsed: 0.001 s % 137.31/19.69 % (3438181)Peak memory usage: 11 MB % 137.31/19.69 % (3438181)Instructions burned: 2 (million) % 137.31/19.69 % (3438181)------------------------------ % 137.31/19.69 % (3438181)------------------------------ % 137.31/19.69 % (3438183)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=4254311472:i=262:bd=preordered:rtra=on:fsd=on_2841 on theBenchmark for (2841ds/262Mi) % 137.31/19.69 % (3438183)Instruction limit reached! % 137.31/19.69 % (3438183)------------------------------ % 137.31/19.69 % (3438183)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 137.31/19.69 % (3438183)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 137.31/19.69 % (3438183)CaDiCaL version: 2.1.3 % 137.31/19.69 % (3438183)Termination reason: Instruction limit % 137.31/19.69 % (3438183)Termination phase: Saturation % 137.31/19.69 % (3438183)Time elapsed: 0.100 s % 137.31/19.69 % (3438183)Peak memory usage: 14 MB % 137.31/19.69 % (3438183)Instructions burned: 262 (million) % 137.31/19.69 % (3438185)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=3119139392:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2840 on theBenchmark for (2840ds/1368Mi) % 137.31/19.69 % (3438185)Instruction limit reached! % 137.31/19.69 % (3438185)------------------------------ % 137.31/19.69 % (3438185)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 137.31/19.69 % (3438185)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 137.31/19.69 % (3438185)CaDiCaL version: 2.1.3 % 137.31/19.69 % (3438185)Termination reason: Instruction limit % 137.31/19.69 % (3438185)Termination phase: Saturation % 137.31/19.69 % (3438185)Time elapsed: 0.423 s % 137.31/19.69 % (3438185)Peak memory usage: 18 MB % 137.31/19.69 % (3438185)Instructions burned: 1371 (million) % 137.31/19.69 % (3438187)ott-21_1_sil=16000:si=on:fs=off:random_seed=2338749979:i=360:av=off:fsr=off:rtra=on_2836 on theBenchmark for (2836ds/360Mi) % 137.31/19.69 % (3438187)Instruction limit reached! % 137.31/19.69 % (3438187)------------------------------ % 137.31/19.69 % (3438187)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 137.31/19.69 % (3438187)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 137.31/19.69 % (3438187)CaDiCaL version: 2.1.3 % 137.31/19.69 % (3438187)Termination reason: Instruction limit % 137.31/19.69 % (3438187)Termination phase: Saturation % 137.31/19.69 % (3438187)Time elapsed: 0.086 s % 137.31/19.69 % (3438187)Peak memory usage: 13 MB % 137.31/19.69 % (3438187)Instructions burned: 362 (million) % 137.31/19.69 % (3438189)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=922875338:i=954:bd=all:rtra=on_2835 on theBenchmark for (2835ds/954Mi) % 137.31/19.69 % (3438189)Instruction limit reached! % 137.31/19.69 % (3438189)------------------------------ % 137.31/19.69 % (3438189)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 137.31/19.69 % (3438189)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 137.31/19.69 % (3438189)CaDiCaL version: 2.1.3 % 137.31/19.69 % (3438189)Termination reason: Instruction limit % 137.31/19.69 % (3438189)Termination phase: Saturation % 137.31/19.69 % (3438189)Time elapsed: 0.358 s % 137.31/19.69 % (3438189)Peak memory usage: 16 MB % 137.31/19.69 % (3438189)Instructions burned: 956 (million) % 137.31/19.69 % (3438191)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=1582037536:fmbsr=1.3:i=1730:ins=25:rtra=on_2831 on theBenchmark for (2831ds/1730Mi) % 137.31/19.69 % (3438191)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 137.31/19.69 % (3438191)Terminated due to inappropriate strategy. % 137.31/19.69 % (3438191)------------------------------ % 137.31/19.69 % (3438191)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 137.31/19.69 % (3438191)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 137.31/19.69 % (3438191)CaDiCaL version: 2.1.3 % 137.31/19.69 % (3438191)Termination reason: Inappropriate % 137.31/19.69 % (3438191)Time elapsed: 0.001 s % 166.79/23.87 % (3438191)Peak memory usage: 10 MB % 166.79/23.87 % (3438191)Instructions burned: 4 (million) % 166.79/23.87 % (3438191)------------------------------ % 166.79/23.87 % (3438191)------------------------------ % 166.79/23.87 % (3438193)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=1486766773:i=2358:rtra=on_2831 on theBenchmark for (2831ds/2358Mi) % 166.79/23.87 % (3438193)Instruction limit reached! % 166.79/23.87 % (3438193)------------------------------ % 166.79/23.87 % (3438193)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 166.79/23.87 % (3438193)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 166.79/23.87 % (3438193)CaDiCaL version: 2.1.3 % 166.79/23.87 % (3438193)Termination reason: Instruction limit % 166.79/23.87 % (3438193)Termination phase: Saturation % 166.79/23.87 % (3438193)Time elapsed: 0.801 s % 166.79/23.87 % (3438193)Peak memory usage: 24 MB % 166.79/23.87 % (3438193)Instructions burned: 2358 (million) % 166.79/23.87 % (3438195)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=1347479603:i=1778:ins=1:rtra=on_2823 on theBenchmark for (2823ds/1778Mi) % 166.79/23.87 % (3438195)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 166.79/23.87 % (3438195)Terminated due to inappropriate strategy. % 166.79/23.87 % (3438195)------------------------------ % 166.79/23.87 % (3438195)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 166.79/23.87 % (3438195)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 166.79/23.87 % (3438195)CaDiCaL version: 2.1.3 % 166.79/23.87 % (3438195)Termination reason: Inappropriate % 166.79/23.87 % (3438195)Time elapsed: 0.001 s % 166.79/23.87 % (3438195)Peak memory usage: 10 MB % 166.79/23.87 % (3438195)Instructions burned: 2 (million) % 166.79/23.87 % (3438195)------------------------------ % 166.79/23.87 % (3438195)------------------------------ % 166.79/23.87 % (3438197)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=4216904454:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2823 on theBenchmark for (2823ds/1384Mi) % 166.79/23.87 % (3438155)Instruction limit reached! % 166.79/23.87 % (3438155)------------------------------ % 166.79/23.87 % (3438155)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 166.79/23.87 % (3438155)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 166.79/23.87 % (3438155)CaDiCaL version: 2.1.3 % 166.79/23.87 % (3438155)Termination reason: Instruction limit % 166.79/23.87 % (3438155)Termination phase: Saturation % 166.79/23.87 % (3438155)Time elapsed: 7.792 s % 166.79/23.87 % (3438155)Peak memory usage: 37 MB % 166.79/23.87 % (3438155)Instructions burned: 28123 (million) % 166.79/23.87 % (3438199)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=1426970328:i=1758:kws=inv_precedence:fsr=off:rtra=on_2821 on theBenchmark for (2821ds/1758Mi) % 166.79/23.87 % (3438197)Instruction limit reached! % 166.79/23.87 % (3438197)------------------------------ % 166.79/23.87 % (3438197)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 166.79/23.87 % (3438197)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 166.79/23.87 % (3438197)CaDiCaL version: 2.1.3 % 166.79/23.87 % (3438197)Termination reason: Instruction limit % 166.79/23.87 % (3438197)Termination phase: Saturation % 166.79/23.87 % (3438197)Time elapsed: 0.456 s % 166.79/23.87 % (3438197)Peak memory usage: 20 MB % 166.79/23.87 % (3438197)Instructions burned: 1386 (million) % 166.79/23.87 % (3438201)fmb+10_1_sil=64000:si=on:random_seed=1073648143:i=44122:nm=2:rtra=on:gsp=on_2818 on theBenchmark for (2818ds/44122Mi) % 166.79/23.87 % (3438201)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 166.79/23.87 % (3438201)Terminated due to inappropriate strategy. % 166.79/23.87 % (3438201)------------------------------ % 166.79/23.87 % (3438201)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 166.79/23.87 % (3438201)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 166.79/23.87 % (3438201)CaDiCaL version: 2.1.3 % 166.79/23.87 % (3438201)Termination reason: Inappropriate % 166.79/23.87 % (3438201)Time elapsed: 0.001 s % 166.79/23.87 % (3438201)Peak memory usage: 10 MB % 166.79/23.87 % (3438201)Instructions burned: 2 (million) % 166.79/23.87 % (3438201)------------------------------ % 166.79/23.87 % (3438201)------------------------------ % 166.79/23.87 % (3438203)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=1507360315:i=19030:nm=5:rtra=on_2818 on theBenchmark for (2818ds/19030Mi) % 181.22/26.00 % (3438203)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 181.22/26.00 % (3438203)Terminated due to inappropriate strategy. % 181.22/26.00 % (3438203)------------------------------ % 181.22/26.00 % (3438203)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 181.22/26.00 % (3438203)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 181.22/26.00 % (3438203)CaDiCaL version: 2.1.3 % 181.22/26.00 % (3438203)Termination reason: Inappropriate % 181.22/26.00 % (3438203)Time elapsed: 0.001 s % 181.22/26.00 % (3438203)Peak memory usage: 10 MB % 181.22/26.00 % (3438203)Instructions burned: 2 (million) % 181.22/26.00 % (3438203)------------------------------ % 181.22/26.00 % (3438203)------------------------------ % 181.22/26.00 % (3438205)fmb+10_1_sil=64000:sas=cadical:si=on:fmbss=8:random_seed=357039140:fmbsr=1.7:i=1840:rtra=on_2818 on theBenchmark for (2818ds/1840Mi) % 181.22/26.00 % (3438205)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 181.22/26.00 % (3438205)Terminated due to inappropriate strategy. % 181.22/26.00 % (3438205)------------------------------ % 181.22/26.00 % (3438205)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 181.22/26.00 % (3438205)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 181.22/26.00 % (3438205)CaDiCaL version: 2.1.3 % 181.22/26.00 % (3438205)Termination reason: Inappropriate % 181.22/26.00 % (3438205)Time elapsed: 0.001 s % 181.22/26.00 % (3438205)Peak memory usage: 10 MB % 181.22/26.00 % (3438205)Instructions burned: 2 (million) % 181.22/26.00 % (3438205)------------------------------ % 181.22/26.00 % (3438205)------------------------------ % 181.22/26.00 % (3438207)dis-4_1_sil=16000:drc=ordering:si=on:sp=const_frequency:sac=on:newcnf=on:random_seed=804995010:i=10262:rtra=on_2817 on theBenchmark for (2817ds/10262Mi) % 181.22/26.00 % (3438199)Instruction limit reached! % 181.22/26.00 % (3438199)------------------------------ % 181.22/26.00 % (3438199)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 181.22/26.00 % (3438199)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 181.22/26.00 % (3438199)CaDiCaL version: 2.1.3 % 181.22/26.00 % (3438199)Termination reason: Instruction limit % 181.22/26.00 % (3438199)Termination phase: Saturation % 181.22/26.00 % (3438199)Time elapsed: 0.556 s % 181.22/26.00 % (3438199)Peak memory usage: 28 MB % 181.22/26.00 % (3438199)Instructions burned: 1760 (million) % 181.22/26.00 % (3438209)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:si=on:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3482450773:i=2944:ins=7:rtra=on:fdi=8:gsp=on_2815 on theBenchmark for (2815ds/2944Mi) % 181.22/26.00 % (3438209)Instruction limit reached! % 181.22/26.00 % (3438209)------------------------------ % 181.22/26.00 % (3438209)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 181.22/26.00 % (3438209)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 181.22/26.00 % (3438209)CaDiCaL version: 2.1.3 % 181.22/26.00 % (3438209)Termination reason: Instruction limit % 181.22/26.00 % (3438209)Termination phase: Saturation % 181.22/26.00 % (3438209)Time elapsed: 1.076 s % 181.22/26.00 % (3438209)Peak memory usage: 31 MB % 181.22/26.00 % (3438209)Instructions burned: 2946 (million) % 181.22/26.00 % (3438212)fmb+10_1_sil=16000:sas=cadical:si=on:bce=on:fmbss=77:random_seed=2155383552:i=12648:rtra=on_2804 on theBenchmark for (2804ds/12648Mi) % 181.22/26.00 % (3438212)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 181.22/26.00 % (3438212)Terminated due to inappropriate strategy. % 181.22/26.00 % (3438212)------------------------------ % 181.22/26.00 % (3438212)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 181.22/26.00 % (3438212)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 181.22/26.00 % (3438212)CaDiCaL version: 2.1.3 % 181.22/26.00 % (3438212)Termination reason: Inappropriate % 181.22/26.00 % (3438212)Time elapsed: 0.001 s % 181.22/26.00 % (3438212)Peak memory usage: 11 MB % 181.22/26.00 % (3438212)Instructions burned: 2 (million) % 181.22/26.00 % (3438212)------------------------------ % 181.22/26.00 % (3438212)------------------------------ % 181.22/26.00 % (3438214)fmb+10_1_fmbas=function:sil=32000:sas=cadical:si=on:fmbss=16:random_seed=57135853:fmbsr=2.30978:i=4348:rtra=on_2804 on theBenchmark for (2804ds/4348Mi) % 181.22/26.00 % (3438214)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 181.22/26.00 % (3438214)Terminated due to inappropriate strategy. % 181.22/26.00 % (3438214)------------------------------ % 181.22/26.00 % (3438214)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 238.18/33.98 % (3438214)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 238.18/33.98 % (3438214)CaDiCaL version: 2.1.3 % 238.18/33.98 % (3438214)Termination reason: Inappropriate % 238.18/33.98 % (3438214)Time elapsed: 0.001 s % 238.18/33.98 % (3438214)Peak memory usage: 10 MB % 238.18/33.98 % (3438214)Instructions burned: 2 (million) % 238.18/33.98 % (3438214)------------------------------ % 238.18/33.98 % (3438214)------------------------------ % 238.18/33.98 % (3438216)ott-2_1_sil=16000:si=on:newcnf=on:random_seed=2082179776:avsq=on:i=1738:avsqr=1,16:kws=inv_arity_squared:rtra=on_2804 on theBenchmark for (2804ds/1738Mi) % 238.18/33.98 % (3438216)Instruction limit reached! % 238.18/33.98 % (3438216)------------------------------ % 238.18/33.98 % (3438216)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 238.18/33.98 % (3438216)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 238.18/33.98 % (3438216)CaDiCaL version: 2.1.3 % 238.18/33.98 % (3438216)Termination reason: Instruction limit % 238.18/33.98 % (3438216)Termination phase: Saturation % 238.18/33.98 % (3438216)Time elapsed: 0.551 s % 238.18/33.98 % (3438216)Peak memory usage: 19 MB % 238.18/33.98 % (3438216)Instructions burned: 1739 (million) % 238.18/33.98 % (3438218)ott+10_1_sil=32000:tgt=ground:si=on:random_seed=1061468331:i=10228:av=off:rtra=on_2798 on theBenchmark for (2798ds/10228Mi) % 238.18/33.98 % (3438207)Instruction limit reached! % 238.18/33.98 % (3438207)------------------------------ % 238.18/33.98 % (3438207)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 238.18/33.98 % (3438207)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 238.18/33.98 % (3438207)CaDiCaL version: 2.1.3 % 238.18/33.98 % (3438207)Termination reason: Instruction limit % 238.18/33.98 % (3438207)Termination phase: Saturation % 238.18/33.98 % (3438207)Time elapsed: 3.309 s % 238.18/33.98 % (3438207)Peak memory usage: 68 MB % 238.18/33.98 % (3438207)Instructions burned: 10262 (million) % 238.18/33.98 % (3438220)fmb+10_1_sil=64000:sas=cadical:si=on:bce=on:rp=on:random_seed=227183899:i=108564:rtra=on_2784 on theBenchmark for (2784ds/108564Mi) % 238.18/33.98 % (3438220)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 238.18/33.98 % (3438220)Terminated due to inappropriate strategy. % 238.18/33.98 % (3438220)------------------------------ % 238.18/33.98 % (3438220)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 238.18/33.98 % (3438220)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 238.18/33.98 % (3438220)CaDiCaL version: 2.1.3 % 238.18/33.98 % (3438220)Termination reason: Inappropriate % 238.18/33.98 % (3438220)Time elapsed: 0.001 s % 238.18/33.98 % (3438220)Peak memory usage: 11 MB % 238.18/33.98 % (3438220)Instructions burned: 2 (million) % 238.18/33.98 % (3438220)------------------------------ % 238.18/33.98 % (3438220)------------------------------ % 238.18/33.98 % (3438222)dis-11_1_sil=16000:si=on:sp=reverse_frequency:alpa=true:random_seed=1933992000:i=7024:aac=none:rtra=on_2784 on theBenchmark for (2784ds/7024Mi) % 238.18/33.98 % (3438061)Instruction limit reached! % 238.18/33.98 % (3438061)------------------------------ % 238.18/33.98 % (3438061)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 238.18/33.98 % (3438061)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 238.18/33.98 % (3438061)CaDiCaL version: 2.1.3 % 238.18/33.98 % (3438061)Termination reason: Instruction limit % 238.18/33.98 % (3438061)Termination phase: Saturation % 238.18/33.98 % (3438061)Time elapsed: 23.325 s % 238.18/33.98 % (3438061)Peak memory usage: 1895 MB % 238.18/33.98 % (3438061)Instructions burned: 88025 (million) % 238.18/33.98 % (3438224)dis+21_1_sil=32000:sas=cadical:si=on:random_seed=2425351099:i=7546:rtra=on:amm=off_2764 on theBenchmark for (2764ds/7546Mi) % 238.18/33.98 % (3438222)Instruction limit reached! % 238.18/33.98 % (3438222)------------------------------ % 238.18/33.98 % (3438222)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 238.18/33.98 % (3438222)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 238.18/33.98 % (3438222)CaDiCaL version: 2.1.3 % 238.18/33.98 % (3438222)Termination reason: Instruction limit % 238.18/33.98 % (3438222)Termination phase: Saturation % 238.18/33.98 % (3438222)Time elapsed: 2.184 s % 238.18/33.98 % (3438222)Peak memory usage: 48 MB % 238.18/33.98 % (3438222)Instructions burned: 7024 (million) % 238.18/33.98 % (3438226)ott+11_1_sil=16000:si=on:gs=on:random_seed=2828979140:s2a=on:i=4502:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:rtra=on:fsd=on_2762 on theBenchmark Terminated % 300.25/42.73 % Vampire exiting %------------------------------------------------------------------------------