%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWW624_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 : n020.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:32 PM UTC 2026 % Result : Timeout 289.34s 41.07s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWW624_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.09/0.19 % Computer : n020.cluster.edu % 0.09/0.19 % Model : x86_64 x86_64 % 0.09/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.19 % Memory : 8046.5625MB % 0.09/0.19 % OS : Linux 6.8.0-71-generic % 0.09/0.19 % CPULimit : 300 % 0.09/0.19 % WCLimit : 300 % 0.09/0.19 % DateTime : Mon Sep 28 14:23:50 UTC 2026 % 0.09/0.19 % CPUTime : % 0.09/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.09/0.22 Running first-order model finding % 0.09/0.22 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 % 6.53/1.21 % (197605)Will run a generic schedule for satisfiability detection. % 6.53/1.21 % (197611)% WARNING: option uhcvi not known. % 6.53/1.21 % (197611)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=363272343:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 6.53/1.21 % (197610)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=279492975_2999 on theBenchmark for (2999ds/0Mi) % 6.53/1.21 % (197612)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2145380186:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 6.53/1.21 % (197613)dis+10_1_sil=32000:sp=arity:random_seed=408672306:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 6.53/1.21 % (197614)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3357865019:i=116_2999 on theBenchmark for (2999ds/116Mi) % 6.53/1.21 % (197610)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 6.53/1.21 % (197610)Terminated due to inappropriate strategy. % 6.53/1.21 % (197610)------------------------------ % 6.53/1.21 % (197610)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.53/1.21 % (197610)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.53/1.21 % (197610)CaDiCaL version: 2.1.3 % 6.53/1.21 % (197610)Termination reason: Inappropriate % 6.53/1.21 % (197610)Time elapsed: 0.005 s % 6.53/1.21 % (197610)Peak memory usage: 11 MB % 6.53/1.21 % (197610)Instructions burned: 9 (million) % 6.53/1.21 % (197610)------------------------------ % 6.53/1.21 % (197610)------------------------------ % 6.53/1.21 % (197615)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3692563146:i=131_2999 on theBenchmark for (2999ds/131Mi) % 6.53/1.21 % (197616)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=4013245093:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 6.53/1.21 % (197622)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3792122486:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 6.53/1.21 % (197622)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 6.53/1.21 % (197622)Terminated due to inappropriate strategy. % 6.53/1.21 % (197622)------------------------------ % 6.53/1.21 % (197622)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.53/1.21 % (197622)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.53/1.21 % (197622)CaDiCaL version: 2.1.3 % 6.53/1.21 % (197622)Termination reason: Inappropriate % 6.53/1.21 % (197622)Time elapsed: 0.004 s % 6.53/1.21 % (197622)Peak memory usage: 10 MB % 6.53/1.21 % (197622)Instructions burned: 8 (million) % 6.53/1.21 % (197622)------------------------------ % 6.53/1.21 % (197622)------------------------------ % 6.53/1.21 % (197626)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1360373707:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 6.53/1.21 % (197613)Instruction limit reached! % 6.53/1.21 % (197613)------------------------------ % 6.53/1.21 % (197613)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.53/1.21 % (197613)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.53/1.21 % (197613)CaDiCaL version: 2.1.3 % 6.53/1.21 % (197613)Termination reason: Instruction limit % 6.53/1.21 % (197613)Termination phase: Saturation % 6.53/1.21 % (197613)Time elapsed: 0.066 s % 6.53/1.21 % (197613)Peak memory usage: 13 MB % 6.53/1.21 % (197613)Instructions burned: 103 (million) % 6.53/1.21 % (197614)Instruction limit reached! % 6.53/1.21 % (197614)------------------------------ % 6.53/1.21 % (197614)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.53/1.21 % (197614)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.53/1.21 % (197614)CaDiCaL version: 2.1.3 % 6.53/1.21 % (197614)Termination reason: Instruction limit % 6.53/1.21 % (197614)Termination phase: Saturation % 6.53/1.21 % (197614)Time elapsed: 0.085 s % 6.53/1.21 % (197614)Peak memory usage: 13 MB % 6.53/1.21 % (197614)Instructions burned: 116 (million) % 6.53/1.21 % (197636)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=3912316897:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi) % 6.53/1.21 % (197637)ott-21_1_sil=16000:fs=off:random_seed=2831916658:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 6.53/1.21 % (197616)Instruction limit reached! % 6.53/1.21 % (197616)------------------------------ % 10.35/2.00 % (197616)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 10.35/2.00 % (197616)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.35/2.00 % (197616)CaDiCaL version: 2.1.3 % 10.35/2.00 % (197616)Termination reason: Instruction limit % 10.35/2.00 % (197616)Termination phase: Saturation % 10.35/2.00 % (197616)Time elapsed: 0.147 s % 10.35/2.00 % (197616)Peak memory usage: 14 MB % 10.35/2.00 % (197616)Instructions burned: 159 (million) % 10.35/2.00 % (197615)Instruction limit reached! % 10.35/2.00 % (197615)------------------------------ % 10.35/2.00 % (197615)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 10.35/2.00 % (197615)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.35/2.00 % (197615)CaDiCaL version: 2.1.3 % 10.35/2.00 % (197615)Termination reason: Instruction limit % 10.35/2.00 % (197615)Termination phase: Saturation % 10.35/2.00 % (197615)Time elapsed: 0.162 s % 10.35/2.00 % (197615)Peak memory usage: 13 MB % 10.35/2.00 % (197615)Instructions burned: 134 (million) % 10.35/2.00 % (197626)Instruction limit reached! % 10.35/2.00 % (197626)------------------------------ % 10.35/2.00 % (197626)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 10.35/2.00 % (197626)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.35/2.00 % (197626)CaDiCaL version: 2.1.3 % 10.35/2.00 % (197626)Termination reason: Instruction limit % 10.35/2.00 % (197626)Termination phase: Saturation % 10.35/2.00 % (197626)Time elapsed: 0.133 s % 10.35/2.00 % (197626)Peak memory usage: 13 MB % 10.35/2.00 % (197626)Instructions burned: 132 (million) % 10.35/2.00 % (197640)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=249999363:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 10.35/2.00 % (197641)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2880177578:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi) % 10.35/2.00 % (197641)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 10.35/2.00 % (197641)Terminated due to inappropriate strategy. % 10.35/2.00 % (197641)------------------------------ % 10.35/2.00 % (197641)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 10.35/2.00 % (197641)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.35/2.00 % (197641)CaDiCaL version: 2.1.3 % 10.35/2.00 % (197641)Termination reason: Inappropriate % 10.35/2.00 % (197641)Time elapsed: 0.007 s % 10.35/2.00 % (197641)Peak memory usage: 10 MB % 10.35/2.00 % (197641)Instructions burned: 8 (million) % 10.35/2.00 % (197641)------------------------------ % 10.35/2.00 % (197641)------------------------------ % 10.35/2.00 % (197642)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3421390987:i=1179_2997 on theBenchmark for (2997ds/1179Mi) % 10.35/2.00 % (197646)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1176877874:i=889:ins=1_2997 on theBenchmark for (2997ds/889Mi) % 10.35/2.00 % (197646)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 10.35/2.00 % (197646)Terminated due to inappropriate strategy. % 10.35/2.00 % (197646)------------------------------ % 10.35/2.00 % (197646)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 10.35/2.00 % (197646)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.35/2.00 % (197646)CaDiCaL version: 2.1.3 % 10.35/2.00 % (197646)Termination reason: Inappropriate % 10.35/2.00 % (197646)Time elapsed: 0.008 s % 10.35/2.00 % (197646)Peak memory usage: 11 MB % 10.35/2.00 % (197646)Instructions burned: 8 (million) % 10.35/2.00 % (197646)------------------------------ % 10.35/2.00 % (197646)------------------------------ % 10.35/2.00 % (197637)Instruction limit reached! % 10.35/2.00 % (197637)------------------------------ % 10.35/2.00 % (197637)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 10.35/2.00 % (197637)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.35/2.00 % (197637)CaDiCaL version: 2.1.3 % 10.35/2.00 % (197637)Termination reason: Instruction limit % 10.35/2.00 % (197637)Termination phase: Saturation % 10.35/2.00 % (197637)Time elapsed: 0.143 s % 10.35/2.00 % (197637)Peak memory usage: 12 MB % 10.35/2.00 % (197637)Instructions burned: 180 (million) % 10.35/2.00 % (197651)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=443273379:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2997 on theBenchmark for (2997ds/692Mi) % 37.27/5.54 % (197652)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2602237234:i=879:kws=inv_precedence:fsr=off_2996 on theBenchmark for (2996ds/879Mi) % 37.27/5.54 % (197640)Instruction limit reached! % 37.27/5.54 % (197640)------------------------------ % 37.27/5.54 % (197640)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 37.27/5.54 % (197640)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 37.27/5.54 % (197640)CaDiCaL version: 2.1.3 % 37.27/5.54 % (197640)Termination reason: Instruction limit % 37.27/5.54 % (197640)Termination phase: Saturation % 37.27/5.54 % (197640)Time elapsed: 0.524 s % 37.27/5.54 % (197640)Peak memory usage: 14 MB % 37.27/5.54 % (197640)Instructions burned: 477 (million) % 37.27/5.54 % (197636)Instruction limit reached! % 37.27/5.54 % (197636)------------------------------ % 37.27/5.54 % (197636)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 37.27/5.54 % (197636)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 37.27/5.54 % (197636)CaDiCaL version: 2.1.3 % 37.27/5.54 % (197636)Termination reason: Instruction limit % 37.27/5.54 % (197636)Termination phase: Saturation % 37.27/5.54 % (197636)Time elapsed: 0.615 s % 37.27/5.54 % (197636)Peak memory usage: 18 MB % 37.27/5.54 % (197636)Instructions burned: 684 (million) % 37.27/5.54 % (197679)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3906881284:i=9515:nm=5_2992 on theBenchmark for (2992ds/9515Mi) % 37.27/5.54 % (197678)fmb+10_1_sil=64000:random_seed=623082037:i=22061:nm=2:gsp=on_2992 on theBenchmark for (2992ds/22061Mi) % 37.27/5.54 % (197679)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 37.27/5.54 % (197679)Terminated due to inappropriate strategy. % 37.27/5.54 % (197679)------------------------------ % 37.27/5.54 % (197679)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 37.27/5.54 % (197679)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 37.27/5.54 % (197679)CaDiCaL version: 2.1.3 % 37.27/5.54 % (197679)Termination reason: Inappropriate % 37.27/5.54 % (197679)Time elapsed: 0.005 s % 37.27/5.54 % (197679)Peak memory usage: 10 MB % 37.27/5.54 % (197679)Instructions burned: 8 (million) % 37.27/5.54 % (197679)------------------------------ % 37.27/5.54 % (197679)------------------------------ % 37.27/5.54 % (197678)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 37.27/5.54 % (197678)Terminated due to inappropriate strategy. % 37.27/5.54 % (197678)------------------------------ % 37.27/5.54 % (197678)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 37.27/5.54 % (197678)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 37.27/5.54 % (197678)CaDiCaL version: 2.1.3 % 37.27/5.54 % (197678)Termination reason: Inappropriate % 37.27/5.54 % (197678)Time elapsed: 0.007 s % 37.27/5.54 % (197678)Peak memory usage: 11 MB % 37.27/5.54 % (197678)Instructions burned: 9 (million) % 37.27/5.54 % (197678)------------------------------ % 37.27/5.54 % (197678)------------------------------ % 37.27/5.54 % (197685)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1202506706:i=5131_2992 on theBenchmark for (2992ds/5131Mi) % 37.27/5.54 % (197684)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3992616845:fmbsr=1.7:i=920_2992 on theBenchmark for (2992ds/920Mi) % 37.27/5.54 % (197684)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 37.27/5.54 % (197684)Terminated due to inappropriate strategy. % 37.27/5.54 % (197684)------------------------------ % 37.27/5.54 % (197684)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 37.27/5.54 % (197684)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 37.27/5.54 % (197684)CaDiCaL version: 2.1.3 % 37.27/5.54 % (197684)Termination reason: Inappropriate % 37.27/5.54 % (197684)Time elapsed: 0.007 s % 37.27/5.54 % (197684)Peak memory usage: 10 MB % 37.27/5.54 % (197684)Instructions burned: 8 (million) % 37.27/5.54 % (197684)------------------------------ % 37.27/5.54 % (197684)------------------------------ % 37.27/5.54 % (197689)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1379732906:i=1472:ins=7:fdi=8:gsp=on_2991 on theBenchmark for (2991ds/1472Mi) % 37.27/5.54 % (197651)Instruction limit reached! % 37.27/5.54 % (197651)------------------------------ % 37.27/5.54 % (197651)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 37.27/5.54 % (197651)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 51.49/7.52 % (197651)CaDiCaL version: 2.1.3 % 51.49/7.52 % (197651)Termination reason: Instruction limit % 51.49/7.52 % (197651)Termination phase: Saturation % 51.49/7.52 % (197651)Time elapsed: 0.657 s % 51.49/7.52 % (197651)Peak memory usage: 20 MB % 51.49/7.52 % (197651)Instructions burned: 692 (million) % 51.49/7.52 % (197697)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3739562687:i=6324_2990 on theBenchmark for (2990ds/6324Mi) % 51.49/7.52 % (197697)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 51.49/7.52 % (197697)Terminated due to inappropriate strategy. % 51.49/7.52 % (197697)------------------------------ % 51.49/7.52 % (197697)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 51.49/7.52 % (197697)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 51.49/7.52 % (197697)CaDiCaL version: 2.1.3 % 51.49/7.52 % (197697)Termination reason: Inappropriate % 51.49/7.52 % (197697)Time elapsed: 0.005 s % 51.49/7.52 % (197697)Peak memory usage: 11 MB % 51.49/7.52 % (197697)Instructions burned: 9 (million) % 51.49/7.52 % (197697)------------------------------ % 51.49/7.52 % (197697)------------------------------ % 51.49/7.52 % (197701)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=493020574:fmbsr=2.30978:i=2174_2989 on theBenchmark for (2989ds/2174Mi) % 51.49/7.52 % (197701)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 51.49/7.52 % (197701)Terminated due to inappropriate strategy. % 51.49/7.52 % (197701)------------------------------ % 51.49/7.52 % (197701)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 51.49/7.52 % (197701)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 51.49/7.52 % (197701)CaDiCaL version: 2.1.3 % 51.49/7.52 % (197701)Termination reason: Inappropriate % 51.49/7.52 % (197701)Time elapsed: 0.008 s % 51.49/7.52 % (197701)Peak memory usage: 10 MB % 51.49/7.52 % (197701)Instructions burned: 8 (million) % 51.49/7.52 % (197701)------------------------------ % 51.49/7.52 % (197701)------------------------------ % 51.49/7.52 % (197652)Instruction limit reached! % 51.49/7.52 % (197652)------------------------------ % 51.49/7.52 % (197652)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 51.49/7.52 % (197652)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 51.49/7.52 % (197652)CaDiCaL version: 2.1.3 % 51.49/7.52 % (197652)Termination reason: Instruction limit % 51.49/7.52 % (197652)Termination phase: Saturation % 51.49/7.52 % (197652)Time elapsed: 0.760 s % 51.49/7.52 % (197652)Peak memory usage: 18 MB % 51.49/7.52 % (197652)Instructions burned: 879 (million) % 51.49/7.52 % (197708)ott-2_1_sil=16000:newcnf=on:random_seed=2968980854:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2989 on theBenchmark for (2989ds/869Mi) % 51.49/7.52 % (197709)ott+10_1_sil=32000:tgt=ground:random_seed=1429214477:i=5114:av=off_2989 on theBenchmark for (2989ds/5114Mi) % 51.49/7.52 % (197642)Instruction limit reached! % 51.49/7.52 % (197642)------------------------------ % 51.49/7.52 % (197642)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 51.49/7.52 % (197642)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 51.49/7.52 % (197642)CaDiCaL version: 2.1.3 % 51.49/7.52 % (197642)Termination reason: Instruction limit % 51.49/7.52 % (197642)Termination phase: Saturation % 51.49/7.52 % (197642)Time elapsed: 1.115 s % 51.49/7.52 % (197642)Peak memory usage: 22 MB % 51.49/7.52 % (197642)Instructions burned: 1180 (million) % 51.49/7.52 % (197724)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=1801442385:i=54282_2986 on theBenchmark for (2986ds/54282Mi) % 51.49/7.52 % (197724)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 51.49/7.52 % (197724)Terminated due to inappropriate strategy. % 51.49/7.52 % (197724)------------------------------ % 51.49/7.52 % (197724)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 51.49/7.52 % (197724)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 51.49/7.52 % (197724)CaDiCaL version: 2.1.3 % 51.49/7.52 % (197724)Termination reason: Inappropriate % 51.49/7.52 % (197724)Time elapsed: 0.008 s % 51.49/7.52 % (197724)Peak memory usage: 11 MB % 51.49/7.52 % (197724)Instructions burned: 9 (million) % 51.49/7.52 % (197724)------------------------------ % 51.49/7.52 % (197724)------------------------------ % 51.49/7.52 % (197726)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=1773028164:i=3512:aac=none_2985 on theBenchmark for (2985ds/3512Mi) % 51.49/7.52 % (197708)Instruction limit reached! % 123.78/18.82 % (197708)------------------------------ % 123.78/18.82 % (197708)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 123.78/18.82 % (197708)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 123.78/18.82 % (197708)CaDiCaL version: 2.1.3 % 123.78/18.82 % (197708)Termination reason: Instruction limit % 123.78/18.82 % (197708)Termination phase: Saturation % 123.78/18.82 % (197708)Time elapsed: 0.656 s % 123.78/18.82 % (197708)Peak memory usage: 15 MB % 123.78/18.82 % (197708)Instructions burned: 869 (million) % 123.78/18.82 % (197743)dis+21_1_sil=32000:sas=cadical:random_seed=3235540085:i=3773:amm=off_2982 on theBenchmark for (2982ds/3773Mi) % 123.78/18.82 % (197689)Instruction limit reached! % 123.78/18.82 % (197689)------------------------------ % 123.78/18.82 % (197689)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 123.78/18.82 % (197689)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 123.78/18.82 % (197689)CaDiCaL version: 2.1.3 % 123.78/18.82 % (197689)Termination reason: Instruction limit % 123.78/18.82 % (197689)Termination phase: Saturation % 123.78/18.82 % (197689)Time elapsed: 1.369 s % 123.78/18.82 % (197689)Peak memory usage: 27 MB % 123.78/18.82 % (197689)Instructions burned: 1472 (million) % 123.78/18.82 % (197758)ott+11_1_sil=16000:gs=on:random_seed=2627761608:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2977 on theBenchmark for (2977ds/2251Mi) % 123.78/18.82 % (197758)Instruction limit reached! % 123.78/18.82 % (197758)------------------------------ % 123.78/18.82 % (197758)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 123.78/18.82 % (197758)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 123.78/18.82 % (197758)CaDiCaL version: 2.1.3 % 123.78/18.82 % (197758)Termination reason: Instruction limit % 123.78/18.82 % (197758)Termination phase: Saturation % 123.78/18.82 % (197758)Time elapsed: 1.776 s % 123.78/18.82 % (197758)Peak memory usage: 20 MB % 123.78/18.82 % (197758)Instructions burned: 2252 (million) % 123.78/18.82 % (197805)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=2363826499:fmbsr=1.6:i=67534_2959 on theBenchmark for (2959ds/67534Mi) % 123.78/18.82 % (197805)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 123.78/18.82 % (197805)Terminated due to inappropriate strategy. % 123.78/18.82 % (197805)------------------------------ % 123.78/18.82 % (197805)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 123.78/18.82 % (197805)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 123.78/18.82 % (197805)CaDiCaL version: 2.1.3 % 123.78/18.82 % (197805)Termination reason: Inappropriate % 123.78/18.82 % (197805)Time elapsed: 0.006 s % 123.78/18.82 % (197805)Peak memory usage: 10 MB % 123.78/18.82 % (197805)Instructions burned: 8 (million) % 123.78/18.82 % (197805)------------------------------ % 123.78/18.82 % (197805)------------------------------ % 123.78/18.82 % (197808)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=207571275:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2958 on theBenchmark for (2958ds/4591Mi) % 123.78/18.82 % (197726)Instruction limit reached! % 123.78/18.82 % (197726)------------------------------ % 123.78/18.82 % (197726)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 123.78/18.82 % (197726)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 123.78/18.82 % (197726)CaDiCaL version: 2.1.3 % 123.78/18.82 % (197726)Termination reason: Instruction limit % 123.78/18.82 % (197726)Termination phase: Saturation % 123.78/18.82 % (197726)Time elapsed: 3.070 s % 123.78/18.82 % (197726)Peak memory usage: 30 MB % 123.78/18.82 % (197726)Instructions burned: 3512 (million) % 123.78/18.82 % (197820)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=2657736879:i=29340_2954 on theBenchmark for (2954ds/29340Mi) % 123.78/18.82 % (197685)Instruction limit reached! % 123.78/18.82 % (197685)------------------------------ % 123.78/18.82 % (197685)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 123.78/18.82 % (197685)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 123.78/18.82 % (197685)CaDiCaL version: 2.1.3 % 123.78/18.82 % (197685)Termination reason: Instruction limit % 123.78/18.82 % (197685)Termination phase: Saturation % 123.78/18.82 % (197685)Time elapsed: 4.369 s % 123.78/18.82 % (197685)Peak memory usage: 43 MB % 123.78/18.82 % (197685)Instructions burned: 5132 (million) % 123.78/18.82 % (197836)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=185843527:i=5211_2947 on theBenchmark for (2947ds/5211Mi) % 123.78/18.82 % (197743)Instruction limit reached! % 151.91/21.79 % (197743)------------------------------ % 151.91/21.79 % (197743)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 151.91/21.79 % (197743)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 151.91/21.79 % (197743)CaDiCaL version: 2.1.3 % 151.91/21.79 % (197743)Termination reason: Instruction limit % 151.91/21.79 % (197743)Termination phase: Saturation % 151.91/21.79 % (197743)Time elapsed: 3.516 s % 151.91/21.79 % (197743)Peak memory usage: 36 MB % 151.91/21.79 % (197743)Instructions burned: 3773 (million) % 151.91/21.79 % (197840)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=3071966584:i=5497:nm=2_2946 on theBenchmark for (2946ds/5497Mi) % 151.91/21.79 % (197840)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 151.91/21.79 % (197840)Terminated due to inappropriate strategy. % 151.91/21.79 % (197840)------------------------------ % 151.91/21.79 % (197840)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 151.91/21.79 % (197840)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 151.91/21.79 % (197840)CaDiCaL version: 2.1.3 % 151.91/21.79 % (197840)Termination reason: Inappropriate % 151.91/21.79 % (197840)Time elapsed: 0.005 s % 151.91/21.79 % (197840)Peak memory usage: 11 MB % 151.91/21.79 % (197840)Instructions burned: 9 (million) % 151.91/21.79 % (197840)------------------------------ % 151.91/21.79 % (197840)------------------------------ % 151.91/21.79 % (197842)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=1824816805:fmbsr=2:i=46332_2946 on theBenchmark for (2946ds/46332Mi) % 151.91/21.79 % (197842)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 151.91/21.79 % (197842)Terminated due to inappropriate strategy. % 151.91/21.79 % (197842)------------------------------ % 151.91/21.79 % (197842)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 151.91/21.79 % (197842)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 151.91/21.79 % (197842)CaDiCaL version: 2.1.3 % 151.91/21.79 % (197842)Termination reason: Inappropriate % 151.91/21.79 % (197842)Time elapsed: 0.010 s % 151.91/21.79 % (197842)Peak memory usage: 10 MB % 151.91/21.79 % (197842)Instructions burned: 8 (million) % 151.91/21.79 % (197842)------------------------------ % 151.91/21.79 % (197842)------------------------------ % 151.91/21.79 % (197844)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=3707322496:i=14071_2945 on theBenchmark for (2945ds/14071Mi) % 151.91/21.79 % (197844)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 151.91/21.79 % (197844)Terminated due to inappropriate strategy. % 151.91/21.79 % (197844)------------------------------ % 151.91/21.79 % (197844)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 151.91/21.79 % (197844)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 151.91/21.79 % (197844)CaDiCaL version: 2.1.3 % 151.91/21.79 % (197844)Termination reason: Inappropriate % 151.91/21.79 % (197844)Time elapsed: 0.009 s % 151.91/21.79 % (197844)Peak memory usage: 10 MB % 151.91/21.79 % (197844)Instructions burned: 8 (million) % 151.91/21.79 % (197844)------------------------------ % 151.91/21.79 % (197844)------------------------------ % 151.91/21.79 % (197847)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1387096916:i=22565:add=on:rawr=on_2945 on theBenchmark for (2945ds/22565Mi) % 151.91/21.79 % (197709)Instruction limit reached! % 151.91/21.79 % (197709)------------------------------ % 151.91/21.79 % (197709)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 151.91/21.79 % (197709)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 151.91/21.79 % (197709)CaDiCaL version: 2.1.3 % 151.91/21.79 % (197709)Termination reason: Instruction limit % 151.91/21.79 % (197709)Termination phase: Saturation % 151.91/21.79 % (197709)Time elapsed: 4.676 s % 151.91/21.79 % (197709)Peak memory usage: 46 MB % 151.91/21.79 % (197709)Instructions burned: 5115 (million) % 151.91/21.79 % (197852)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=2087577975:i=8173:av=off_2942 on theBenchmark for (2942ds/8173Mi) % 151.91/21.79 % (197808)Instruction limit reached! % 151.91/21.79 % (197808)------------------------------ % 151.91/21.79 % (197808)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 151.91/21.79 % (197808)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 151.91/21.79 % (197808)CaDiCaL version: 2.1.3 % 151.91/21.79 % (197808)Termination reason: Instruction limit % 151.91/21.79 % (197808)Termination phase: Saturation % 151.91/21.79 % (197808)Time elapsed: 3.145 s % 172.20/24.50 % (197808)Peak memory usage: 59 MB % 172.20/24.50 % (197808)Instructions burned: 4594 (million) % 172.20/24.50 % (198010)dis+10_16:1_sil=16000:random_seed=2869655813:i=9155:fsr=off_2927 on theBenchmark for (2927ds/9155Mi) % 172.20/24.50 % (197836)Instruction limit reached! % 172.20/24.50 % (197836)------------------------------ % 172.20/24.50 % (197836)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 172.20/24.50 % (197836)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 172.20/24.50 % (197836)CaDiCaL version: 2.1.3 % 172.20/24.50 % (197836)Termination reason: Instruction limit % 172.20/24.50 % (197836)Termination phase: Saturation % 172.20/24.50 % (197836)Time elapsed: 3.031 s % 172.20/24.50 % (197836)Peak memory usage: 53 MB % 172.20/24.50 % (197836)Instructions burned: 5212 (million) % 172.20/24.50 % (198012)ott-3_8_sil=64000:random_seed=3612770315:i=20139:bs=on_2917 on theBenchmark for (2917ds/20139Mi) % 172.20/24.50 % (197852)Instruction limit reached! % 172.20/24.50 % (197852)------------------------------ % 172.20/24.50 % (197852)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 172.20/24.50 % (197852)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 172.20/24.50 % (197852)CaDiCaL version: 2.1.3 % 172.20/24.50 % (197852)Termination reason: Instruction limit % 172.20/24.50 % (197852)Termination phase: Saturation % 172.20/24.50 % (197852)Time elapsed: 4.837 s % 172.20/24.50 % (197852)Peak memory usage: 62 MB % 172.20/24.50 % (197852)Instructions burned: 8174 (million) % 172.20/24.50 % (198014)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=2387576690:fmbsr=2:i=32576_2893 on theBenchmark for (2893ds/32576Mi) % 172.20/24.50 % (198014)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 172.20/24.50 % (198014)Terminated due to inappropriate strategy. % 172.20/24.50 % (198014)------------------------------ % 172.20/24.50 % (198014)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 172.20/24.50 % (198014)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 172.20/24.50 % (198014)CaDiCaL version: 2.1.3 % 172.20/24.50 % (198014)Termination reason: Inappropriate % 172.20/24.50 % (198014)Time elapsed: 0.005 s % 172.20/24.50 % (198014)Peak memory usage: 11 MB % 172.20/24.50 % (198014)Instructions burned: 9 (million) % 172.20/24.50 % (198014)------------------------------ % 172.20/24.50 % (198014)------------------------------ % 172.20/24.50 % (198016)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=3048916677:i=11404_2893 on theBenchmark for (2893ds/11404Mi) % 172.20/24.50 % (198010)Instruction limit reached! % 172.20/24.50 % (198010)------------------------------ % 172.20/24.50 % (198010)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 172.20/24.50 % (198010)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 172.20/24.50 % (198010)CaDiCaL version: 2.1.3 % 172.20/24.50 % (198010)Termination reason: Instruction limit % 172.20/24.50 % (198010)Termination phase: Saturation % 172.20/24.50 % (198010)Time elapsed: 4.867 s % 172.20/24.50 % (198010)Peak memory usage: 55 MB % 172.20/24.50 % (198010)Instructions burned: 9155 (million) % 172.20/24.50 % (198018)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=1517574536:i=14134_2878 on theBenchmark for (2878ds/14134Mi) % 172.20/24.50 % (197847)Instruction limit reached! % 172.20/24.50 % (197847)------------------------------ % 172.20/24.50 % (197847)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 172.20/24.50 % (197847)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 172.20/24.50 % (197847)CaDiCaL version: 2.1.3 % 172.20/24.50 % (197847)Termination reason: Instruction limit % 172.20/24.50 % (197847)Termination phase: Saturation % 172.20/24.50 % (197847)Time elapsed: 9.463 s % 172.20/24.50 % (197847)Peak memory usage: 35 MB % 172.20/24.50 % (197847)Instructions burned: 22566 (million) % 172.20/24.50 % (198290)dis+33_16_sil=32000:sac=on:random_seed=129596117:i=15851:nm=0_2850 on theBenchmark for (2850ds/15851Mi) % 172.20/24.50 % (198016)Instruction limit reached! % 172.20/24.50 % (198016)------------------------------ % 172.20/24.50 % (198016)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 172.20/24.50 % (198016)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 172.20/24.50 % (198016)CaDiCaL version: 2.1.3 % 172.20/24.50 % (198016)Termination reason: Instruction limit % 172.20/24.50 % (198016)Termination phase: Saturation % 172.20/24.50 % (198016)Time elapsed: 7.852 s % 172.20/24.50 % (198016)Peak memory usage: 91 MB % 172.20/24.50 % (198016)Instructions burned: 11405 (million) % 172.20/24.50 % (198463)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=2867098821:avsq=on:i=17627:add=on:amm=off_2814 on theBenchmark for (2814ds/17627Mi) % 202.54/28.89 % (197820)Instruction limit reached! % 202.54/28.89 % (197820)------------------------------ % 202.54/28.89 % (197820)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 202.54/28.89 % (197820)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 202.54/28.89 % (197820)CaDiCaL version: 2.1.3 % 202.54/28.89 % (197820)Termination reason: Instruction limit % 202.54/28.89 % (197820)Termination phase: Saturation % 202.54/28.89 % (197820)Time elapsed: 15.914 s % 202.54/28.89 % (197820)Peak memory usage: 98 MB % 202.54/28.89 % (197820)Instructions burned: 29340 (million) % 202.54/28.89 % (198465)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=1447788226:s2a=on:i=53295_2795 on theBenchmark for (2795ds/53295Mi) % 202.54/28.89 % (198012)Instruction limit reached! % 202.54/28.89 % (198012)------------------------------ % 202.54/28.89 % (198012)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 202.54/28.89 % (198012)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 202.54/28.89 % (198012)CaDiCaL version: 2.1.3 % 202.54/28.89 % (198012)Termination reason: Instruction limit % 202.54/28.89 % (198012)Termination phase: Saturation % 202.54/28.89 % (198012)Time elapsed: 12.739 s % 202.54/28.89 % (198012)Peak memory usage: 115 MB % 202.54/28.89 % (198012)Instructions burned: 20139 (million) % 202.54/28.89 % (198467)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=1713304679:i=26857:ins=20_2789 on theBenchmark for (2789ds/26857Mi) % 202.54/28.89 % (198467)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 202.54/28.89 % (198467)Terminated due to inappropriate strategy. % 202.54/28.89 % (198467)------------------------------ % 202.54/28.89 % (198467)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 202.54/28.89 % (198467)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 202.54/28.89 % (198467)CaDiCaL version: 2.1.3 % 202.54/28.89 % (198467)Termination reason: Inappropriate % 202.54/28.89 % (198467)Time elapsed: 0.004 s % 202.54/28.89 % (198467)Peak memory usage: 10 MB % 202.54/28.89 % (198467)Instructions burned: 8 (million) % 202.54/28.89 % (198467)------------------------------ % 202.54/28.89 % (198467)------------------------------ % 202.54/28.89 % (198469)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=3151503342:i=28120:bs=on:fsr=off_2789 on theBenchmark for (2789ds/28120Mi) % 202.54/28.89 % (198018)Instruction limit reached! % 202.54/28.89 % (198018)------------------------------ % 202.54/28.89 % (198018)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 202.54/28.89 % (198018)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 202.54/28.89 % (198018)CaDiCaL version: 2.1.3 % 202.54/28.89 % (198018)Termination reason: Instruction limit % 202.54/28.89 % (198018)Termination phase: Saturation % 202.54/28.89 % (198018)Time elapsed: 9.291 s % 202.54/28.89 % (198018)Peak memory usage: 90 MB % 202.54/28.89 % (198018)Instructions burned: 14134 (million) % 202.54/28.89 % (198471)fmb+10_1_sil=256000:fmbss=7:random_seed=546142566:fmbsr=1.6:i=182295_2784 on theBenchmark for (2784ds/182295Mi) % 202.54/28.89 % (198471)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 202.54/28.89 % (198471)Terminated due to inappropriate strategy. % 202.54/28.89 % (198471)------------------------------ % 202.54/28.89 % (198471)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 202.54/28.89 % (198471)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 202.54/28.89 % (198471)CaDiCaL version: 2.1.3 % 202.54/28.89 % (198471)Termination reason: Inappropriate % 202.54/28.89 % (198471)Time elapsed: 0.004 s % 202.54/28.89 % (198471)Peak memory usage: 10 MB % 202.54/28.89 % (198471)Instructions burned: 8 (million) % 202.54/28.89 % (198471)------------------------------ % 202.54/28.89 % (198471)------------------------------ % 202.54/28.89 % (198473)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=395525089:i=44625:gsp=on_2784 on theBenchmark for (2784ds/44625Mi) % 202.54/28.89 % (198473)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 202.54/28.89 % (198473)Terminated due to inappropriate strategy. % 202.54/28.89 % (198473)------------------------------ % 202.54/28.89 % (198473)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 202.54/28.89 % (198473)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 202.54/28.89 % (198473)CaDiCaL version: 2.1.3 % 202.54/28.89 % (198473)Termination reason: Inappropriate % 236.10/33.51 % (198473)Time elapsed: 0.005 s % 236.10/33.51 % (198473)Peak memory usage: 11 MB % 236.10/33.51 % (198473)Instructions burned: 8 (million) % 236.10/33.51 % (198473)------------------------------ % 236.10/33.51 % (198473)------------------------------ % 236.10/33.51 % (198475)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=1827714318:i=160505_2784 on theBenchmark for (2784ds/160505Mi) % 236.10/33.51 % (198475)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 236.10/33.51 % (198475)Terminated due to inappropriate strategy. % 236.10/33.51 % (198475)------------------------------ % 236.10/33.51 % (198475)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 236.10/33.51 % (198475)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 236.10/33.51 % (198475)CaDiCaL version: 2.1.3 % 236.10/33.51 % (198475)Termination reason: Inappropriate % 236.10/33.51 % (198475)Time elapsed: 0.004 s % 236.10/33.51 % (198475)Peak memory usage: 10 MB % 236.10/33.51 % (198475)Instructions burned: 8 (million) % 236.10/33.51 % (198475)------------------------------ % 236.10/33.51 % (198475)------------------------------ % 236.10/33.51 % (198477)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=2708333679:fmbsr=1.3:i=225729_2784 on theBenchmark for (2784ds/225729Mi) % 236.10/33.51 % (198477)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 236.10/33.51 % (198477)Terminated due to inappropriate strategy. % 236.10/33.51 % (198477)------------------------------ % 236.10/33.51 % (198477)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 236.10/33.51 % (198477)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 236.10/33.51 % (198477)CaDiCaL version: 2.1.3 % 236.10/33.51 % (198477)Termination reason: Inappropriate % 236.10/33.51 % (198477)Time elapsed: 0.004 s % 236.10/33.51 % (198477)Peak memory usage: 11 MB % 236.10/33.51 % (198477)Instructions burned: 8 (million) % 236.10/33.51 % (198477)------------------------------ % 236.10/33.51 % (198477)------------------------------ % 236.10/33.51 % (198479)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=863251378:fmbsr=2:i=185024:ins=7_2783 on theBenchmark for (2783ds/185024Mi) % 236.10/33.51 % (198479)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 236.10/33.51 % (198479)Terminated due to inappropriate strategy. % 236.10/33.51 % (198479)------------------------------ % 236.10/33.51 % (198479)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 236.10/33.51 % (198479)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 236.10/33.51 % (198479)CaDiCaL version: 2.1.3 % 236.10/33.51 % (198479)Termination reason: Inappropriate % 236.10/33.51 % (198479)Time elapsed: 0.004 s % 236.10/33.51 % (198479)Peak memory usage: 10 MB % 236.10/33.51 % (198479)Instructions burned: 8 (million) % 236.10/33.51 % (198479)------------------------------ % 236.10/33.51 % (198479)------------------------------ % 236.10/33.51 % (198481)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=864192826:rtra=on_2783 on theBenchmark for (2783ds/0Mi) % 236.10/33.51 % (198481)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 236.10/33.51 % (198481)Terminated due to inappropriate strategy. % 236.10/33.51 % (198481)------------------------------ % 236.10/33.51 % (198481)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 236.10/33.51 % (198481)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 236.10/33.51 % (198481)CaDiCaL version: 2.1.3 % 236.10/33.51 % (198481)Termination reason: Inappropriate % 236.10/33.51 % (198481)Time elapsed: 0.006 s % 236.10/33.51 % (198481)Peak memory usage: 11 MB % 236.10/33.51 % (198481)Instructions burned: 10 (million) % 236.10/33.51 % (198481)------------------------------ % 236.10/33.51 % (198481)------------------------------ % 236.10/33.51 % (198483)% WARNING: option uhcvi not known. % 236.10/33.51 % (198483)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3809006183:i=271062:add=off:rtra=on:rawr=on_2783 on theBenchmark for (2783ds/271062Mi) % 236.10/33.51 % (198290)Instruction limit reached! % 236.10/33.51 % (198290)------------------------------ % 236.10/33.51 % (198290)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 236.10/33.51 % (198290)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 236.10/33.51 % (198290)CaDiCaL version: 2.1.3 % 236.10/33.51 % (198290)Termination reason: Instruction limit % 236.10/33.51 % (198290)Termination phase: Saturation % 236.10/33.51 % (198290)Time elapsed: 9.234 s % 236.10/33.51 % (198290)Peak memory usage: 146 MB % 236.10/33.51 % (198290)Instructions burned: 15852 (million) % 236.10/33.51 % (198485)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=4134013483:i=176048:add=on:rtra=on:rawr=on_2757 on theBenchmark for (2757ds/176048Mi) % 256.02/36.33 % (198463)Instruction limit reached! % 256.02/36.33 % (198463)------------------------------ % 256.02/36.33 % (198463)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 256.02/36.33 % (198463)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 256.02/36.33 % (198463)CaDiCaL version: 2.1.3 % 256.02/36.33 % (198463)Termination reason: Instruction limit % 256.02/36.33 % (198463)Termination phase: Saturation % 256.02/36.33 % (198463)Time elapsed: 9.238 s % 256.02/36.33 % (198463)Peak memory usage: 333 MB % 256.02/36.33 % (198463)Instructions burned: 17628 (million) % 256.02/36.33 % (198487)dis+10_1_sil=32000:si=on:sp=arity:random_seed=1689175462:i=206:fgj=on:rtra=on_2721 on theBenchmark for (2721ds/206Mi) % 256.02/36.33 % (198487)Instruction limit reached! % 256.02/36.33 % (198487)------------------------------ % 256.02/36.33 % (198487)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 256.02/36.33 % (198487)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 256.02/36.33 % (198487)CaDiCaL version: 2.1.3 % 256.02/36.33 % (198487)Termination reason: Instruction limit % 256.02/36.33 % (198487)Termination phase: Saturation % 256.02/36.33 % (198487)Time elapsed: 0.130 s % 256.02/36.33 % (198487)Peak memory usage: 14 MB % 256.02/36.33 % (198487)Instructions burned: 206 (million) % 256.02/36.33 % (198489)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=317781231:i=232:rtra=on_2719 on theBenchmark for (2719ds/232Mi) % 256.02/36.33 % (198489)Instruction limit reached! % 256.02/36.33 % (198489)------------------------------ % 256.02/36.33 % (198489)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 256.02/36.33 % (198489)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 256.02/36.33 % (198489)CaDiCaL version: 2.1.3 % 256.02/36.33 % (198489)Termination reason: Instruction limit % 256.02/36.33 % (198489)Termination phase: Saturation % 256.02/36.33 % (198489)Time elapsed: 0.152 s % 256.02/36.33 % (198489)Peak memory usage: 14 MB % 256.02/36.33 % (198489)Instructions burned: 233 (million) % 256.02/36.33 % (198493)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=3058286544:i=262:rtra=on_2718 on theBenchmark for (2718ds/262Mi) % 256.02/36.33 % (198493)Instruction limit reached! % 256.02/36.33 % (198493)------------------------------ % 256.02/36.33 % (198493)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 256.02/36.33 % (198493)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 256.02/36.33 % (198493)CaDiCaL version: 2.1.3 % 256.02/36.33 % (198493)Termination reason: Instruction limit % 256.02/36.33 % (198493)Termination phase: Saturation % 256.02/36.33 % (198493)Time elapsed: 0.178 s % 256.02/36.33 % (198493)Peak memory usage: 14 MB % 256.02/36.33 % (198493)Instructions burned: 262 (million) % 256.02/36.33 % (198558)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=3108241390:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2716 on theBenchmark for (2716ds/318Mi) % 256.02/36.33 % (198558)Instruction limit reached! % 256.02/36.33 % (198558)------------------------------ % 256.02/36.33 % (198558)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 256.02/36.33 % (198558)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 256.02/36.33 % (198558)CaDiCaL version: 2.1.3 % 256.02/36.33 % (198558)Termination reason: Instruction limit % 256.02/36.33 % (198558)Termination phase: Saturation % 256.02/36.33 % (198558)Time elapsed: 0.219 s % 256.02/36.33 % (198558)Peak memory usage: 15 MB % 256.02/36.33 % (198558)Instructions burned: 319 (million) % 256.02/36.33 % (198627)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=3367030658:i=1428:nm=2:rtra=on_2713 on theBenchmark for (2713ds/1428Mi) % 256.02/36.33 % (198627)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 256.02/36.33 % (198627)Terminated due to inappropriate strategy. % 256.02/36.33 % (198627)------------------------------ % 256.02/36.33 % (198627)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 256.02/36.33 % (198627)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 256.02/36.33 % (198627)CaDiCaL version: 2.1.3 % 256.02/36.33 % (198627)Termination reason: Inappropriate % 256.02/36.33 % (198627)Time elapsed: 0.005 s % 256.02/36.33 % (198627)Peak memory usage: 10 MB % 256.02/36.33 % (198627)Instructions burned: 9 (million) % 256.02/36.33 % (198627)------------------------------ % 256.02/36.33 % (198627)------------------------------ % 289.34/41.07 % (198629)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=3465234511:i=262:bd=preordered:rtra=on:fsd=on_2713 on theBenchmark for (2713ds/262Mi) % 289.34/41.07 % (198629)Instruction limit reached! % 289.34/41.07 % (198629)------------------------------ % 289.34/41.07 % (198629)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 289.34/41.07 % (198629)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 289.34/41.07 % (198629)CaDiCaL version: 2.1.3 % 289.34/41.07 % (198629)Termination reason: Instruction limit % 289.34/41.07 % (198629)Termination phase: Saturation % 289.34/41.07 % (198629)Time elapsed: 0.178 s % 289.34/41.07 % (198629)Peak memory usage: 14 MB % 289.34/41.07 % (198629)Instructions burned: 263 (million) % 289.34/41.07 % (198631)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=2966937206:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2711 on theBenchmark for (2711ds/1368Mi) % 289.34/41.07 % (198631)Instruction limit reached! % 289.34/41.07 % (198631)------------------------------ % 289.34/41.07 % (198631)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 289.34/41.07 % (198631)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 289.34/41.07 % (198631)CaDiCaL version: 2.1.3 % 289.34/41.07 % (198631)Termination reason: Instruction limit % 289.34/41.07 % (198631)Termination phase: Saturation % 289.34/41.07 % (198631)Time elapsed: 0.873 s % 289.34/41.07 % (198631)Peak memory usage: 29 MB % 289.34/41.07 % (198631)Instructions burned: 1369 (million) % 289.34/41.07 % (198763)ott-21_1_sil=16000:si=on:fs=off:random_seed=2498263179:i=360:av=off:fsr=off:rtra=on_2702 on theBenchmark for (2702ds/360Mi) % 289.34/41.07 % (198763)Instruction limit reached! % 289.34/41.07 % (198763)------------------------------ % 289.34/41.07 % (198763)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 289.34/41.07 % (198763)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 289.34/41.07 % (198763)CaDiCaL version: 2.1.3 % 289.34/41.07 % (198763)Termination reason: Instruction limit % 289.34/41.07 % (198763)Termination phase: Saturation % 289.34/41.07 % (198763)Time elapsed: 0.187 s % 289.34/41.07 % (198763)Peak memory usage: 13 MB % 289.34/41.07 % (198763)Instructions burned: 361 (million) % 289.34/41.07 % (198765)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=425144292:i=954:bd=all:rtra=on_2700 on theBenchmark for (2700ds/954Mi) % 289.34/41.07 % (198765)Instruction limit reached! % 289.34/41.07 % (198765)------------------------------ % 289.34/41.07 % (198765)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 289.34/41.07 % (198765)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 289.34/41.07 % (198765)CaDiCaL version: 2.1.3 % 289.34/41.07 % (198765)Termination reason: Instruction limit % 289.34/41.07 % (198765)Termination phase: Saturation % 289.34/41.07 % (198765)Time elapsed: 0.904 s % 289.34/41.07 % (198765)Peak memory usage: 16 MB % 289.34/41.07 % (198765)Instructions burned: 955 (million) % 289.34/41.07 % (198807)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=2060164340:fmbsr=1.3:i=1730:ins=25:rtra=on_2691 on theBenchmark for (2691ds/1730Mi) % 289.34/41.07 % (198807)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 289.34/41.07 % (198807)Terminated due to inappropriate strategy. % 289.34/41.07 % (198807)------------------------------ % 289.34/41.07 % (198807)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 289.34/41.07 % (198807)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 289.34/41.07 % (198807)CaDiCaL version: 2.1.3 % 289.34/41.07 % (198807)Termination reason: Inappropriate % 289.34/41.07 % (198807)Time elapsed: 0.008 s % 289.34/41.07 % (198807)Peak memory usage: 10 MB % 289.34/41.07 % (198807)Instructions burned: 9 (million) % 289.34/41.07 % (198807)------------------------------ % 289.34/41.07 % (198807)------------------------------ % 289.34/41.07 % (198810)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=3267169794:i=2358:rtra=on_2690 on theBenchmark for (2690ds/2358Mi) % 289.34/41.07 % (198810)Instruction limit reached! % 289.34/41.07 % (198810)------------------------------ % 289.34/41.07 % (198810)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 289.34/41.07 % (198810)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 289.34/41.07 % (198810)CaDiCaL version: 2.1.3 % 289.34/41.07 % (198810)Termination reason: Instruction limit % 289.34/41.07 % (198810)TerminationTerminated % 300.02/42.54 % Vampire exiting %------------------------------------------------------------------------------