%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWW652_2 : TPTP v9.3.1. Released v6.1.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % Computer : n013.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:35 PM UTC 2026 % Result : Timeout 300.16s 42.54s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWW652_2 : TPTP v9.3.1. Released v6.1.0. % 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.10/0.22 % Computer : n013.cluster.edu % 0.10/0.22 % Model : x86_64 x86_64 % 0.10/0.22 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.22 % Memory : 8046.5625MB % 0.10/0.22 % OS : Linux 6.8.0-71-generic % 0.10/0.22 % CPULimit : 300 % 0.10/0.22 % WCLimit : 300 % 0.10/0.22 % DateTime : Mon Sep 28 14:23:21 UTC 2026 % 0.10/0.22 % CPUTime : % 0.10/0.22 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.10/0.27 Running first-order model finding % 0.10/0.28 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 6.99/1.31 % (1215995)Will run a generic schedule for satisfiability detection. % 6.99/1.31 % (1216002)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2949122956:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 6.99/1.31 % (1216000)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=882554405_2999 on theBenchmark for (2999ds/0Mi) % 6.99/1.31 % (1216000)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 6.99/1.31 % (1216000)Terminated due to inappropriate strategy. % 6.99/1.31 % (1216000)------------------------------ % 6.99/1.31 % (1216000)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.99/1.31 % (1216000)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.99/1.31 % (1216000)CaDiCaL version: 2.1.3 % 6.99/1.31 % (1216000)Termination reason: Inappropriate % 6.99/1.31 % (1216000)Time elapsed: 0.002 s % 6.99/1.31 % (1216000)Peak memory usage: 11 MB % 6.99/1.31 % (1216000)Instructions burned: 2 (million) % 6.99/1.31 % (1216000)------------------------------ % 6.99/1.31 % (1216000)------------------------------ % 6.99/1.31 % (1216001)% WARNING: option uhcvi not known. % 6.99/1.31 % (1216004)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3043485123:i=116_2999 on theBenchmark for (2999ds/116Mi) % 6.99/1.31 % (1216003)dis+10_1_sil=32000:sp=arity:random_seed=4032866580:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 6.99/1.31 % (1216006)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=500088028:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 6.99/1.31 % (1216005)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1479920813:i=131_2999 on theBenchmark for (2999ds/131Mi) % 6.99/1.31 % (1216001)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2527872889:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 6.99/1.31 % (1216009)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=966586759:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 6.99/1.31 % (1216009)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 6.99/1.31 % (1216009)Terminated due to inappropriate strategy. % 6.99/1.32 % (1216009)------------------------------ % 6.99/1.32 % (1216009)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.99/1.32 % (1216009)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.99/1.32 % (1216009)CaDiCaL version: 2.1.3 % 6.99/1.32 % (1216009)Termination reason: Inappropriate % 6.99/1.32 % (1216009)Time elapsed: 0.002 s % 6.99/1.32 % (1216009)Peak memory usage: 11 MB % 6.99/1.32 % (1216009)Instructions burned: 2 (million) % 6.99/1.32 % (1216009)------------------------------ % 6.99/1.32 % (1216009)------------------------------ % 6.99/1.32 % (1216016)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1780683733:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 6.99/1.32 % (1216003)Instruction limit reached! % 6.99/1.32 % (1216003)------------------------------ % 6.99/1.32 % (1216003)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.99/1.32 % (1216003)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.99/1.32 % (1216003)CaDiCaL version: 2.1.3 % 6.99/1.32 % (1216003)Termination reason: Instruction limit % 6.99/1.32 % (1216003)Termination phase: Saturation % 6.99/1.32 % (1216003)Time elapsed: 0.104 s % 6.99/1.32 % (1216003)Peak memory usage: 12 MB % 6.99/1.32 % (1216003)Instructions burned: 103 (million) % 6.99/1.32 % (1216004)Instruction limit reached! % 6.99/1.32 % (1216004)------------------------------ % 6.99/1.32 % (1216004)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.99/1.32 % (1216004)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.99/1.32 % (1216004)CaDiCaL version: 2.1.3 % 6.99/1.32 % (1216004)Termination reason: Instruction limit % 6.99/1.32 % (1216004)Termination phase: Saturation % 6.99/1.32 % (1216004)Time elapsed: 0.120 s % 6.99/1.32 % (1216004)Peak memory usage: 12 MB % 6.99/1.32 % (1216004)Instructions burned: 116 (million) % 6.99/1.32 % (1216018)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=224021958:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi) % 6.99/1.32 % (1216005)Instruction limit reached! % 6.99/1.32 % (1216005)------------------------------ % 6.99/1.32 % (1216005)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.55/1.79 % (1216005)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.55/1.79 % (1216005)CaDiCaL version: 2.1.3 % 8.55/1.79 % (1216005)Termination reason: Instruction limit % 8.55/1.79 % (1216005)Termination phase: Saturation % 8.55/1.79 % (1216005)Time elapsed: 0.141 s % 8.55/1.79 % (1216005)Peak memory usage: 13 MB % 8.55/1.79 % (1216005)Instructions burned: 131 (million) % 8.55/1.79 % (1216019)ott-21_1_sil=16000:fs=off:random_seed=836435380:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 8.55/1.79 % (1216021)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2632780719:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 8.55/1.79 % (1216006)Instruction limit reached! % 8.55/1.79 % (1216006)------------------------------ % 8.55/1.79 % (1216006)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.55/1.79 % (1216006)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.55/1.79 % (1216006)CaDiCaL version: 2.1.3 % 8.55/1.79 % (1216006)Termination reason: Instruction limit % 8.55/1.79 % (1216006)Termination phase: Saturation % 8.55/1.79 % (1216006)Time elapsed: 0.181 s % 8.55/1.79 % (1216006)Peak memory usage: 14 MB % 8.55/1.79 % (1216006)Instructions burned: 159 (million) % 8.55/1.79 % (1216016)Instruction limit reached! % 8.55/1.79 % (1216016)------------------------------ % 8.55/1.79 % (1216016)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.55/1.79 % (1216016)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.55/1.79 % (1216016)CaDiCaL version: 2.1.3 % 8.55/1.79 % (1216016)Termination reason: Instruction limit % 8.55/1.79 % (1216016)Termination phase: Saturation % 8.55/1.79 % (1216016)Time elapsed: 0.153 s % 8.55/1.79 % (1216016)Peak memory usage: 13 MB % 8.55/1.79 % (1216016)Instructions burned: 132 (million) % 8.55/1.79 % (1216024)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2754733140:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi) % 8.55/1.79 % (1216024)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 8.55/1.79 % (1216024)Terminated due to inappropriate strategy. % 8.55/1.79 % (1216024)------------------------------ % 8.55/1.79 % (1216024)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.55/1.79 % (1216024)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.55/1.79 % (1216024)CaDiCaL version: 2.1.3 % 8.55/1.79 % (1216024)Termination reason: Inappropriate % 8.55/1.79 % (1216024)Time elapsed: 0.002 s % 8.55/1.79 % (1216024)Peak memory usage: 10 MB % 8.55/1.79 % (1216024)Instructions burned: 1 (million) % 8.55/1.79 % (1216024)------------------------------ % 8.55/1.79 % (1216024)------------------------------ % 8.55/1.79 % (1216025)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2753689476:i=1179_2997 on theBenchmark for (2997ds/1179Mi) % 8.55/1.79 % (1216027)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1525999903:i=889:ins=1_2997 on theBenchmark for (2997ds/889Mi) % 8.55/1.79 % (1216027)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 8.55/1.79 % (1216027)Terminated due to inappropriate strategy. % 8.55/1.79 % (1216027)------------------------------ % 8.55/1.79 % (1216027)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.55/1.79 % (1216027)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.55/1.79 % (1216027)CaDiCaL version: 2.1.3 % 8.55/1.79 % (1216027)Termination reason: Inappropriate % 8.55/1.79 % (1216027)Time elapsed: 0.003 s % 8.55/1.79 % (1216027)Peak memory usage: 10 MB % 8.55/1.79 % (1216027)Instructions burned: 2 (million) % 8.55/1.79 % (1216027)------------------------------ % 8.55/1.79 % (1216027)------------------------------ % 8.55/1.79 % (1216030)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=2214014581: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) % 8.55/1.79 % (1216019)Instruction limit reached! % 8.55/1.79 % (1216019)------------------------------ % 8.55/1.79 % (1216019)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.55/1.79 % (1216019)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.55/1.79 % (1216019)CaDiCaL version: 2.1.3 % 8.55/1.79 % (1216019)Termination reason: Instruction limit % 8.55/1.79 % (1216019)Termination phase: Saturation % 38.80/5.89 % (1216019)Time elapsed: 0.152 s % 38.80/5.89 % (1216019)Peak memory usage: 12 MB % 38.80/5.89 % (1216019)Instructions burned: 181 (million) % 38.80/5.89 % (1216032)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=392686684:i=879:kws=inv_precedence:fsr=off_2996 on theBenchmark for (2996ds/879Mi) % 38.80/5.89 % (1216021)Instruction limit reached! % 38.80/5.89 % (1216021)------------------------------ % 38.80/5.89 % (1216021)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 38.80/5.89 % (1216021)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 38.80/5.89 % (1216021)CaDiCaL version: 2.1.3 % 38.80/5.89 % (1216021)Termination reason: Instruction limit % 38.80/5.89 % (1216021)Termination phase: Saturation % 38.80/5.89 % (1216021)Time elapsed: 0.541 s % 38.80/5.89 % (1216021)Peak memory usage: 14 MB % 38.80/5.89 % (1216021)Instructions burned: 478 (million) % 38.80/5.89 % (1216018)Instruction limit reached! % 38.80/5.89 % (1216018)------------------------------ % 38.80/5.89 % (1216018)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 38.80/5.89 % (1216018)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 38.80/5.89 % (1216018)CaDiCaL version: 2.1.3 % 38.80/5.89 % (1216018)Termination reason: Instruction limit % 38.80/5.89 % (1216018)Termination phase: Saturation % 38.80/5.89 % (1216018)Time elapsed: 0.614 s % 38.80/5.89 % (1216018)Peak memory usage: 16 MB % 38.80/5.89 % (1216018)Instructions burned: 684 (million) % 38.80/5.89 % (1216034)fmb+10_1_sil=64000:random_seed=320472524:i=22061:nm=2:gsp=on_2992 on theBenchmark for (2992ds/22061Mi) % 38.80/5.89 % (1216034)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 38.80/5.89 % (1216034)Terminated due to inappropriate strategy. % 38.80/5.89 % (1216034)------------------------------ % 38.80/5.89 % (1216034)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 38.80/5.89 % (1216034)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 38.80/5.89 % (1216034)CaDiCaL version: 2.1.3 % 38.80/5.89 % (1216034)Termination reason: Inappropriate % 38.80/5.89 % (1216034)Time elapsed: 0.003 s % 38.80/5.89 % (1216034)Peak memory usage: 11 MB % 38.80/5.89 % (1216034)Instructions burned: 2 (million) % 38.80/5.89 % (1216034)------------------------------ % 38.80/5.89 % (1216034)------------------------------ % 38.80/5.89 % (1216035)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3503158402:i=9515:nm=5_2992 on theBenchmark for (2992ds/9515Mi) % 38.80/5.89 % (1216035)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 38.80/5.89 % (1216035)Terminated due to inappropriate strategy. % 38.80/5.89 % (1216035)------------------------------ % 38.80/5.89 % (1216035)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 38.80/5.89 % (1216035)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 38.80/5.89 % (1216035)CaDiCaL version: 2.1.3 % 38.80/5.89 % (1216035)Termination reason: Inappropriate % 38.80/5.89 % (1216035)Time elapsed: 0.002 s % 38.80/5.89 % (1216035)Peak memory usage: 11 MB % 38.80/5.89 % (1216035)Instructions burned: 2 (million) % 38.80/5.89 % (1216035)------------------------------ % 38.80/5.89 % (1216035)------------------------------ % 38.80/5.89 % (1216037)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2679541080:fmbsr=1.7:i=920_2992 on theBenchmark for (2992ds/920Mi) % 38.80/5.89 % (1216037)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 38.80/5.89 % (1216037)Terminated due to inappropriate strategy. % 38.80/5.89 % (1216037)------------------------------ % 38.80/5.89 % (1216037)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 38.80/5.89 % (1216039)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1351359731:i=5131_2991 on theBenchmark for (2991ds/5131Mi) % 38.80/5.89 % (1216037)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 38.80/5.89 % (1216037)CaDiCaL version: 2.1.3 % 38.80/5.89 % (1216037)Termination reason: Inappropriate % 38.80/5.89 % (1216037)Time elapsed: 0.003 s % 38.80/5.89 % (1216037)Peak memory usage: 10 MB % 38.80/5.89 % (1216037)Instructions burned: 2 (million) % 38.80/5.89 % (1216037)------------------------------ % 38.80/5.89 % (1216037)------------------------------ % 38.80/5.89 % (1216042)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3575856018:i=1472:ins=7:fdi=8:gsp=on_2991 on theBenchmark for (2991ds/1472Mi) % 38.80/5.89 % (1216030)Instruction limit reached! % 38.80/5.89 % (1216030)------------------------------ % 60.04/8.78 % (1216030)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 60.04/8.78 % (1216030)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 60.04/8.78 % (1216030)CaDiCaL version: 2.1.3 % 60.04/8.78 % (1216030)Termination reason: Instruction limit % 60.04/8.78 % (1216030)Termination phase: Saturation % 60.04/8.78 % (1216030)Time elapsed: 0.704 s % 60.04/8.78 % (1216030)Peak memory usage: 18 MB % 60.04/8.78 % (1216030)Instructions burned: 692 (million) % 60.04/8.78 % (1216044)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=1263968610:i=6324_2989 on theBenchmark for (2989ds/6324Mi) % 60.04/8.78 % (1216044)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 60.04/8.78 % (1216044)Terminated due to inappropriate strategy. % 60.04/8.78 % (1216044)------------------------------ % 60.04/8.78 % (1216044)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 60.04/8.78 % (1216044)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 60.04/8.78 % (1216044)CaDiCaL version: 2.1.3 % 60.04/8.78 % (1216044)Termination reason: Inappropriate % 60.04/8.78 % (1216044)Time elapsed: 0.003 s % 60.04/8.78 % (1216044)Peak memory usage: 11 MB % 60.04/8.78 % (1216044)Instructions burned: 2 (million) % 60.04/8.78 % (1216044)------------------------------ % 60.04/8.78 % (1216044)------------------------------ % 60.04/8.78 % (1216046)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=474148701:fmbsr=2.30978:i=2174_2989 on theBenchmark for (2989ds/2174Mi) % 60.04/8.78 % (1216046)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 60.04/8.78 % (1216046)Terminated due to inappropriate strategy. % 60.04/8.78 % (1216046)------------------------------ % 60.04/8.78 % (1216046)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 60.04/8.78 % (1216046)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 60.04/8.78 % (1216046)CaDiCaL version: 2.1.3 % 60.04/8.78 % (1216046)Termination reason: Inappropriate % 60.04/8.78 % (1216046)Time elapsed: 0.002 s % 60.04/8.78 % (1216046)Peak memory usage: 10 MB % 60.04/8.78 % (1216046)Instructions burned: 2 (million) % 60.04/8.78 % (1216046)------------------------------ % 60.04/8.78 % (1216046)------------------------------ % 60.04/8.78 % (1216048)ott-2_1_sil=16000:newcnf=on:random_seed=1965755682:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2988 on theBenchmark for (2988ds/869Mi) % 60.04/8.78 % (1216032)Instruction limit reached! % 60.04/8.78 % (1216032)------------------------------ % 60.04/8.78 % (1216032)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 60.04/8.78 % (1216032)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 60.04/8.78 % (1216032)CaDiCaL version: 2.1.3 % 60.04/8.78 % (1216032)Termination reason: Instruction limit % 60.04/8.78 % (1216032)Termination phase: Saturation % 60.04/8.78 % (1216032)Time elapsed: 0.841 s % 60.04/8.78 % (1216032)Peak memory usage: 19 MB % 60.04/8.78 % (1216032)Instructions burned: 879 (million) % 60.04/8.78 % (1216050)ott+10_1_sil=32000:tgt=ground:random_seed=1636712501:i=5114:av=off_2987 on theBenchmark for (2987ds/5114Mi) % 60.04/8.78 % (1216025)Instruction limit reached! % 60.04/8.78 % (1216025)------------------------------ % 60.04/8.78 % (1216025)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 60.04/8.78 % (1216025)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 60.04/8.78 % (1216025)CaDiCaL version: 2.1.3 % 60.04/8.78 % (1216025)Termination reason: Instruction limit % 60.04/8.78 % (1216025)Termination phase: Saturation % 60.04/8.78 % (1216025)Time elapsed: 1.209 s % 60.04/8.78 % (1216025)Peak memory usage: 18 MB % 60.04/8.78 % (1216025)Instructions burned: 1180 (million) % 60.04/8.78 % (1216052)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=1121743483:i=54282_2985 on theBenchmark for (2985ds/54282Mi) % 60.04/8.78 % (1216052)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 60.04/8.78 % (1216052)Terminated due to inappropriate strategy. % 60.04/8.78 % (1216052)------------------------------ % 60.04/8.78 % (1216052)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 60.04/8.78 % (1216052)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 60.04/8.78 % (1216052)CaDiCaL version: 2.1.3 % 60.04/8.78 % (1216052)Termination reason: Inappropriate % 60.04/8.78 % (1216052)Time elapsed: 0.002 s % 60.04/8.78 % (1216052)Peak memory usage: 11 MB % 60.04/8.78 % (1216052)Instructions burned: 2 (million) % 151.74/21.69 % (1216052)------------------------------ % 151.74/21.69 % (1216052)------------------------------ % 151.74/21.69 % (1216054)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=2440803267:i=3512:aac=none_2984 on theBenchmark for (2984ds/3512Mi) % 151.74/21.69 % (1216048)Instruction limit reached! % 151.74/21.69 % (1216048)------------------------------ % 151.74/21.69 % (1216048)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 151.74/21.69 % (1216048)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 151.74/21.69 % (1216048)CaDiCaL version: 2.1.3 % 151.74/21.69 % (1216048)Termination reason: Instruction limit % 151.74/21.69 % (1216048)Termination phase: Saturation % 151.74/21.69 % (1216048)Time elapsed: 0.918 s % 151.74/21.69 % (1216048)Peak memory usage: 17 MB % 151.74/21.69 % (1216048)Instructions burned: 869 (million) % 151.74/21.69 % (1216058)dis+21_1_sil=32000:sas=cadical:random_seed=2368307416:i=3773:amm=off_2979 on theBenchmark for (2979ds/3773Mi) % 151.74/21.69 % (1216042)Instruction limit reached! % 151.74/21.69 % (1216042)------------------------------ % 151.74/21.69 % (1216042)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 151.74/21.69 % (1216042)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 151.74/21.69 % (1216042)CaDiCaL version: 2.1.3 % 151.74/21.69 % (1216042)Termination reason: Instruction limit % 151.74/21.69 % (1216042)Termination phase: Saturation % 151.74/21.69 % (1216042)Time elapsed: 1.437 s % 151.74/21.69 % (1216042)Peak memory usage: 29 MB % 151.74/21.69 % (1216042)Instructions burned: 1473 (million) % 151.74/21.69 % (1216060)ott+11_1_sil=16000:gs=on:random_seed=3379132077:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2976 on theBenchmark for (2976ds/2251Mi) % 151.74/21.69 % (1216060)Instruction limit reached! % 151.74/21.69 % (1216060)------------------------------ % 151.74/21.69 % (1216060)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 151.74/21.69 % (1216060)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 151.74/21.69 % (1216060)CaDiCaL version: 2.1.3 % 151.74/21.69 % (1216060)Termination reason: Instruction limit % 151.74/21.69 % (1216060)Termination phase: Saturation % 151.74/21.69 % (1216060)Time elapsed: 2.195 s % 151.74/21.69 % (1216060)Peak memory usage: 27 MB % 151.74/21.69 % (1216060)Instructions burned: 2251 (million) % 151.74/21.69 % (1216064)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=744946105:fmbsr=1.6:i=67534_2954 on theBenchmark for (2954ds/67534Mi) % 151.74/21.69 % (1216064)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 151.74/21.69 % (1216064)Terminated due to inappropriate strategy. % 151.74/21.69 % (1216064)------------------------------ % 151.74/21.69 % (1216064)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 151.74/21.69 % (1216064)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 151.74/21.69 % (1216064)CaDiCaL version: 2.1.3 % 151.74/21.69 % (1216064)Termination reason: Inappropriate % 151.74/21.69 % (1216064)Time elapsed: 0.002 s % 151.74/21.69 % (1216064)Peak memory usage: 11 MB % 151.74/21.69 % (1216064)Instructions burned: 2 (million) % 151.74/21.69 % (1216064)------------------------------ % 151.74/21.69 % (1216064)------------------------------ % 151.74/21.69 % (1216066)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=3929455467:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2954 on theBenchmark for (2954ds/4591Mi) % 151.74/21.69 % (1216054)Instruction limit reached! % 151.74/21.69 % (1216054)------------------------------ % 151.74/21.69 % (1216054)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 151.74/21.69 % (1216054)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 151.74/21.69 % (1216054)CaDiCaL version: 2.1.3 % 151.74/21.69 % (1216054)Termination reason: Instruction limit % 151.74/21.69 % (1216054)Termination phase: Saturation % 151.74/21.69 % (1216054)Time elapsed: 3.333 s % 151.74/21.69 % (1216054)Peak memory usage: 30 MB % 151.74/21.69 % (1216054)Instructions burned: 3512 (million) % 151.74/21.69 % (1216070)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=3389308445:i=29340_2951 on theBenchmark for (2951ds/29340Mi) % 151.74/21.69 % (1216058)Instruction limit reached! % 151.74/21.69 % (1216058)------------------------------ % 151.74/21.69 % (1216058)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 151.74/21.69 % (1216058)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 151.74/21.69 % (1216058)CaDiCaL version: 2.1.3 % 151.74/21.69 % (1216058)Termination reason: Instruction limit % 172.33/24.53 % (1216058)Termination phase: Saturation % 172.33/24.53 % (1216058)Time elapsed: 3.516 s % 172.33/24.53 % (1216058)Peak memory usage: 32 MB % 172.33/24.53 % (1216058)Instructions burned: 3773 (million) % 172.33/24.53 % (1216073)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=3649854991:i=5211_2943 on theBenchmark for (2943ds/5211Mi) % 172.33/24.53 % (1216039)Instruction limit reached! % 172.33/24.53 % (1216039)------------------------------ % 172.33/24.53 % (1216039)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 172.33/24.53 % (1216039)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 172.33/24.53 % (1216039)CaDiCaL version: 2.1.3 % 172.33/24.53 % (1216039)Termination reason: Instruction limit % 172.33/24.53 % (1216039)Termination phase: Saturation % 172.33/24.53 % (1216039)Time elapsed: 4.963 s % 172.33/24.53 % (1216039)Peak memory usage: 41 MB % 172.33/24.53 % (1216039)Instructions burned: 5132 (million) % 172.33/24.53 % (1216076)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=1037451893:i=5497:nm=2_2942 on theBenchmark for (2942ds/5497Mi) % 172.33/24.53 % (1216076)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 172.33/24.53 % (1216076)Terminated due to inappropriate strategy. % 172.33/24.53 % (1216076)------------------------------ % 172.33/24.53 % (1216076)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 172.33/24.53 % (1216076)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 172.33/24.53 % (1216076)CaDiCaL version: 2.1.3 % 172.33/24.53 % (1216076)Termination reason: Inappropriate % 172.33/24.53 % (1216076)Time elapsed: 0.002 s % 172.33/24.53 % (1216076)Peak memory usage: 11 MB % 172.33/24.53 % (1216076)Instructions burned: 2 (million) % 172.33/24.53 % (1216076)------------------------------ % 172.33/24.53 % (1216076)------------------------------ % 172.33/24.53 % (1216078)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=2871121684:fmbsr=2:i=46332_2941 on theBenchmark for (2941ds/46332Mi) % 172.33/24.53 % (1216078)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 172.33/24.53 % (1216078)Terminated due to inappropriate strategy. % 172.33/24.53 % (1216078)------------------------------ % 172.33/24.53 % (1216078)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 172.33/24.53 % (1216078)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 172.33/24.53 % (1216078)CaDiCaL version: 2.1.3 % 172.33/24.53 % (1216078)Termination reason: Inappropriate % 172.33/24.53 % (1216078)Time elapsed: 0.002 s % 172.33/24.53 % (1216078)Peak memory usage: 11 MB % 172.33/24.53 % (1216078)Instructions burned: 2 (million) % 172.33/24.53 % (1216078)------------------------------ % 172.33/24.53 % (1216078)------------------------------ % 172.33/24.53 % (1216080)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=2522529859:i=14071_2941 on theBenchmark for (2941ds/14071Mi) % 172.33/24.53 % (1216080)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 172.33/24.53 % (1216080)Terminated due to inappropriate strategy. % 172.33/24.53 % (1216080)------------------------------ % 172.33/24.53 % (1216080)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 172.33/24.53 % (1216080)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 172.33/24.53 % (1216080)CaDiCaL version: 2.1.3 % 172.33/24.53 % (1216080)Termination reason: Inappropriate % 172.33/24.53 % (1216080)Time elapsed: 0.003 s % 172.33/24.53 % (1216080)Peak memory usage: 10 MB % 172.33/24.53 % (1216080)Instructions burned: 2 (million) % 172.33/24.53 % (1216080)------------------------------ % 172.33/24.53 % (1216080)------------------------------ % 172.33/24.53 % (1216082)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1977886280:i=22565:add=on:rawr=on_2941 on theBenchmark for (2941ds/22565Mi) % 172.33/24.53 % (1216050)Instruction limit reached! % 172.33/24.53 % (1216050)------------------------------ % 172.33/24.53 % (1216050)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 172.33/24.53 % (1216050)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 172.33/24.53 % (1216050)CaDiCaL version: 2.1.3 % 172.33/24.53 % (1216050)Termination reason: Instruction limit % 172.33/24.53 % (1216050)Termination phase: Saturation % 172.33/24.53 % (1216050)Time elapsed: 5.205 s % 172.33/24.53 % (1216050)Peak memory usage: 38 MB % 172.33/24.53 % (1216050)Instructions burned: 5115 (million) % 172.33/24.53 % (1216085)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=2729662438:i=8173:av=off_2935 on theBenchmark for (2935ds/8173Mi) % 172.33/24.53 % (1216066)Instruction limit reached! % 173.03/24.65 % (1216066)------------------------------ % 173.03/24.65 % (1216066)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 173.03/24.65 % (1216066)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 173.03/24.65 % (1216066)CaDiCaL version: 2.1.3 % 173.03/24.65 % (1216066)Termination reason: Instruction limit % 173.03/24.65 % (1216066)Termination phase: Saturation % 173.03/24.65 % (1216066)Time elapsed: 3.913 s % 173.03/24.65 % (1216066)Peak memory usage: 46 MB % 173.03/24.65 % (1216066)Instructions burned: 4592 (million) % 173.03/24.65 % (1216090)dis+10_16:1_sil=16000:random_seed=712486368:i=9155:fsr=off_2914 on theBenchmark for (2914ds/9155Mi) % 173.03/24.65 % (1216073)Instruction limit reached! % 173.03/24.65 % (1216073)------------------------------ % 173.03/24.65 % (1216073)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 173.03/24.65 % (1216073)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 173.03/24.65 % (1216073)CaDiCaL version: 2.1.3 % 173.03/24.65 % (1216073)Termination reason: Instruction limit % 173.03/24.65 % (1216073)Termination phase: Saturation % 173.03/24.65 % (1216073)Time elapsed: 4.743 s % 173.03/24.65 % (1216073)Peak memory usage: 46 MB % 173.03/24.65 % (1216073)Instructions burned: 5212 (million) % 173.03/24.65 % (1216092)ott-3_8_sil=64000:random_seed=3820660722:i=20139:bs=on_2895 on theBenchmark for (2895ds/20139Mi) % 173.03/24.65 % (1216085)Instruction limit reached! % 173.03/24.65 % (1216085)------------------------------ % 173.03/24.65 % (1216085)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 173.03/24.65 % (1216085)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 173.03/24.65 % (1216085)CaDiCaL version: 2.1.3 % 173.03/24.65 % (1216085)Termination reason: Instruction limit % 173.03/24.65 % (1216085)Termination phase: Saturation % 173.03/24.65 % (1216085)Time elapsed: 7.648 s % 173.03/24.65 % (1216085)Peak memory usage: 49 MB % 173.03/24.65 % (1216085)Instructions burned: 8175 (million) % 173.03/24.65 % (1216253)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=2828852258:fmbsr=2:i=32576_2858 on theBenchmark for (2858ds/32576Mi) % 173.03/24.65 % (1216253)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 173.03/24.65 % (1216253)Terminated due to inappropriate strategy. % 173.03/24.65 % (1216253)------------------------------ % 173.03/24.65 % (1216253)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 173.03/24.65 % (1216253)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 173.03/24.65 % (1216253)CaDiCaL version: 2.1.3 % 173.03/24.65 % (1216253)Termination reason: Inappropriate % 173.03/24.65 % (1216253)Time elapsed: 0.002 s % 173.03/24.65 % (1216253)Peak memory usage: 11 MB % 173.03/24.65 % (1216253)Instructions burned: 2 (million) % 173.03/24.65 % (1216253)------------------------------ % 173.03/24.65 % (1216253)------------------------------ % 173.03/24.65 % (1216255)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=2047919389:i=11404_2858 on theBenchmark for (2858ds/11404Mi) % 173.03/24.65 % (1216090)Instruction limit reached! % 173.03/24.65 % (1216090)------------------------------ % 173.03/24.65 % (1216090)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 173.03/24.65 % (1216090)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 173.03/24.65 % (1216090)CaDiCaL version: 2.1.3 % 173.03/24.65 % (1216090)Termination reason: Instruction limit % 173.03/24.65 % (1216090)Termination phase: Saturation % 173.03/24.65 % (1216090)Time elapsed: 6.615 s % 173.03/24.65 % (1216090)Peak memory usage: 52 MB % 173.03/24.65 % (1216090)Instructions burned: 9155 (million) % 173.03/24.65 % (1216257)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=2033089237:i=14134_2848 on theBenchmark for (2848ds/14134Mi) % 173.03/24.65 % (1216082)Instruction limit reached! % 173.03/24.65 % (1216082)------------------------------ % 173.03/24.65 % (1216082)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 173.03/24.65 % (1216082)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 173.03/24.65 % (1216082)CaDiCaL version: 2.1.3 % 173.03/24.65 % (1216082)Termination reason: Instruction limit % 173.03/24.65 % (1216082)Termination phase: Saturation % 173.03/24.65 % (1216082)Time elapsed: 12.570 s % 173.03/24.65 % (1216082)Peak memory usage: 80 MB % 173.03/24.65 % (1216082)Instructions burned: 22565 (million) % 173.03/24.65 % (1216259)dis+33_16_sil=32000:sac=on:random_seed=3589217726:i=15851:nm=0_2815 on theBenchmark for (2815ds/15851Mi) % 173.03/24.65 % (1216255)Instruction limit reached! % 173.03/24.65 % (1216255)------------------------------ % 173.03/24.65 % (1216255)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 196.46/27.91 % (1216255)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 196.46/27.91 % (1216255)CaDiCaL version: 2.1.3 % 196.46/27.91 % (1216255)Termination reason: Instruction limit % 196.46/27.91 % (1216255)Termination phase: Saturation % 196.46/27.91 % (1216255)Time elapsed: 7.217 s % 196.46/27.91 % (1216255)Peak memory usage: 60 MB % 196.46/27.91 % (1216255)Instructions burned: 11405 (million) % 196.46/27.91 % (1216261)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=1399941337:avsq=on:i=17627:add=on:amm=off_2785 on theBenchmark for (2785ds/17627Mi) % 196.46/27.91 % (1216070)Instruction limit reached! % 196.46/27.91 % (1216070)------------------------------ % 196.46/27.91 % (1216070)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 196.46/27.91 % (1216070)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 196.46/27.91 % (1216070)CaDiCaL version: 2.1.3 % 196.46/27.91 % (1216070)Termination reason: Instruction limit % 196.46/27.91 % (1216070)Termination phase: Saturation % 196.46/27.91 % (1216070)Time elapsed: 17.580 s % 196.46/27.91 % (1216070)Peak memory usage: 188 MB % 196.46/27.91 % (1216070)Instructions burned: 29340 (million) % 196.46/27.91 % (1216263)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=2044324319:s2a=on:i=53295_2774 on theBenchmark for (2774ds/53295Mi) % 196.46/27.91 % (1216092)Instruction limit reached! % 196.46/27.91 % (1216092)------------------------------ % 196.46/27.91 % (1216092)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 196.46/27.91 % (1216092)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 196.46/27.91 % (1216092)CaDiCaL version: 2.1.3 % 196.46/27.91 % (1216092)Termination reason: Instruction limit % 196.46/27.91 % (1216092)Termination phase: Saturation % 196.46/27.91 % (1216092)Time elapsed: 13.162 s % 196.46/27.91 % (1216092)Peak memory usage: 83 MB % 196.46/27.91 % (1216092)Instructions burned: 20139 (million) % 196.46/27.91 % (1216265)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=2458873437:i=26857:ins=20_2763 on theBenchmark for (2763ds/26857Mi) % 196.46/27.91 % (1216265)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 196.46/27.91 % (1216265)Terminated due to inappropriate strategy. % 196.46/27.91 % (1216265)------------------------------ % 196.46/27.91 % (1216265)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 196.46/27.91 % (1216265)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 196.46/27.91 % (1216265)CaDiCaL version: 2.1.3 % 196.46/27.91 % (1216265)Termination reason: Inappropriate % 196.46/27.91 % (1216265)Time elapsed: 0.001 s % 196.46/27.91 % (1216265)Peak memory usage: 10 MB % 196.46/27.91 % (1216265)Instructions burned: 2 (million) % 196.46/27.91 % (1216265)------------------------------ % 196.46/27.91 % (1216265)------------------------------ % 196.46/27.91 % (1216267)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=3559847329:i=28120:bs=on:fsr=off_2763 on theBenchmark for (2763ds/28120Mi) % 196.46/27.91 % (1216257)Instruction limit reached! % 196.46/27.91 % (1216257)------------------------------ % 196.46/27.91 % (1216257)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 196.46/27.91 % (1216257)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 196.46/27.91 % (1216257)CaDiCaL version: 2.1.3 % 196.46/27.91 % (1216257)Termination reason: Instruction limit % 196.46/27.91 % (1216257)Termination phase: Saturation % 196.46/27.91 % (1216257)Time elapsed: 9.031 s % 196.46/27.91 % (1216257)Peak memory usage: 70 MB % 196.46/27.91 % (1216257)Instructions burned: 14134 (million) % 196.46/27.91 % (1216269)fmb+10_1_sil=256000:fmbss=7:random_seed=3383039501:fmbsr=1.6:i=182295_2757 on theBenchmark for (2757ds/182295Mi) % 196.46/27.91 % (1216269)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 196.46/27.91 % (1216269)Terminated due to inappropriate strategy. % 196.46/27.91 % (1216269)------------------------------ % 196.46/27.91 % (1216269)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 196.46/27.91 % (1216269)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 196.46/27.91 % (1216269)CaDiCaL version: 2.1.3 % 196.46/27.91 % (1216269)Termination reason: Inappropriate % 196.46/27.91 % (1216269)Time elapsed: 0.001 s % 196.46/27.91 % (1216269)Peak memory usage: 10 MB % 196.46/27.91 % (1216269)Instructions burned: 2 (million) % 196.46/27.91 % (1216269)------------------------------ % 196.46/27.91 % (1216269)------------------------------ % 196.46/27.91 % (1216271)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=2050816558:i=44625:gsp=on_2757 on theBenchmark for (2757ds/44625Mi) % 208.66/29.76 % (1216271)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 208.66/29.76 % (1216271)Terminated due to inappropriate strategy. % 208.66/29.76 % (1216271)------------------------------ % 208.66/29.76 % (1216271)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 208.66/29.76 % (1216271)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 208.66/29.76 % (1216271)CaDiCaL version: 2.1.3 % 208.66/29.76 % (1216271)Termination reason: Inappropriate % 208.66/29.76 % (1216271)Time elapsed: 0.002 s % 208.66/29.76 % (1216271)Peak memory usage: 10 MB % 208.66/29.76 % (1216271)Instructions burned: 3 (million) % 208.66/29.76 % (1216271)------------------------------ % 208.66/29.76 % (1216271)------------------------------ % 208.66/29.76 % (1216273)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=1553060031:i=160505_2757 on theBenchmark for (2757ds/160505Mi) % 208.66/29.76 % (1216273)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 208.66/29.76 % (1216273)Terminated due to inappropriate strategy. % 208.66/29.76 % (1216273)------------------------------ % 208.66/29.76 % (1216273)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 208.66/29.76 % (1216273)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 208.66/29.76 % (1216273)CaDiCaL version: 2.1.3 % 208.66/29.76 % (1216273)Termination reason: Inappropriate % 208.66/29.76 % (1216273)Time elapsed: 0.001 s % 208.66/29.76 % (1216273)Peak memory usage: 11 MB % 208.66/29.76 % (1216273)Instructions burned: 2 (million) % 208.66/29.76 % (1216273)------------------------------ % 208.66/29.76 % (1216273)------------------------------ % 208.66/29.76 % (1216275)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=4065282964:fmbsr=1.3:i=225729_2757 on theBenchmark for (2757ds/225729Mi) % 208.66/29.76 % (1216275)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 208.66/29.76 % (1216275)Terminated due to inappropriate strategy. % 208.66/29.76 % (1216275)------------------------------ % 208.66/29.76 % (1216275)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 208.66/29.76 % (1216275)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 208.66/29.76 % (1216275)CaDiCaL version: 2.1.3 % 208.66/29.76 % (1216275)Termination reason: Inappropriate % 208.66/29.76 % (1216275)Time elapsed: 0.001 s % 208.66/29.76 % (1216275)Peak memory usage: 10 MB % 208.66/29.76 % (1216275)Instructions burned: 2 (million) % 208.66/29.76 % (1216275)------------------------------ % 208.66/29.76 % (1216275)------------------------------ % 208.66/29.76 % (1216277)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=4024991525:fmbsr=2:i=185024:ins=7_2757 on theBenchmark for (2757ds/185024Mi) % 208.66/29.76 % (1216277)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 208.66/29.76 % (1216277)Terminated due to inappropriate strategy. % 208.66/29.76 % (1216277)------------------------------ % 208.66/29.76 % (1216277)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 208.66/29.76 % (1216277)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 208.66/29.76 % (1216277)CaDiCaL version: 2.1.3 % 208.66/29.76 % (1216277)Termination reason: Inappropriate % 208.66/29.76 % (1216277)Time elapsed: 0.001 s % 208.66/29.76 % (1216277)Peak memory usage: 10 MB % 208.66/29.76 % (1216277)Instructions burned: 2 (million) % 208.66/29.76 % (1216277)------------------------------ % 208.66/29.76 % (1216277)------------------------------ % 208.66/29.76 % (1216279)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=1076258596:rtra=on_2756 on theBenchmark for (2756ds/0Mi) % 208.66/29.76 % (1216279)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 208.66/29.76 % (1216279)Terminated due to inappropriate strategy. % 208.66/29.76 % (1216279)------------------------------ % 208.66/29.76 % (1216279)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 208.66/29.76 % (1216279)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 208.66/29.76 % (1216279)CaDiCaL version: 2.1.3 % 208.66/29.76 % (1216279)Termination reason: Inappropriate % 208.66/29.76 % (1216279)Time elapsed: 0.002 s % 208.66/29.76 % (1216279)Peak memory usage: 11 MB % 208.66/29.76 % (1216279)Instructions burned: 2 (million) % 208.66/29.76 % (1216279)------------------------------ % 208.66/29.76 % (1216279)------------------------------ % 208.66/29.76 % (1216281)% WARNING: option uhcvi not known. % 208.66/29.76 % (1216281)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2781674125:i=271062:add=off:rtra=on:rawr=on_2756 on theBenchmark for (2756ds/271062Mi) % 221.34/31.43 % (1216002)Instruction limit reached! % 221.34/31.43 % (1216002)------------------------------ % 221.34/31.43 % (1216002)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 221.34/31.43 % (1216002)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 221.34/31.43 % (1216002)CaDiCaL version: 2.1.3 % 221.34/31.43 % (1216002)Termination reason: Instruction limit % 221.34/31.43 % (1216002)Termination phase: Saturation % 221.34/31.43 % (1216002)Time elapsed: 25.171 s % 221.34/31.43 % (1216002)Peak memory usage: 158 MB % 221.34/31.43 % (1216002)Instructions burned: 88028 (million) % 221.34/31.43 % (1216283)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3916135270:i=176048:add=on:rtra=on:rawr=on_2747 on theBenchmark for (2747ds/176048Mi) % 221.34/31.43 % (1216259)Instruction limit reached! % 221.34/31.43 % (1216259)------------------------------ % 221.34/31.43 % (1216259)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 221.34/31.43 % (1216259)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 221.34/31.43 % (1216259)CaDiCaL version: 2.1.3 % 221.34/31.43 % (1216259)Termination reason: Instruction limit % 221.34/31.43 % (1216259)Termination phase: Saturation % 221.34/31.43 % (1216259)Time elapsed: 8.322 s % 221.34/31.43 % (1216259)Peak memory usage: 119 MB % 221.34/31.43 % (1216259)Instructions burned: 15851 (million) % 221.34/31.43 % (1216285)dis+10_1_sil=32000:si=on:sp=arity:random_seed=412556166:i=206:fgj=on:rtra=on_2731 on theBenchmark for (2731ds/206Mi) % 221.34/31.43 % (1216285)Instruction limit reached! % 221.34/31.43 % (1216285)------------------------------ % 221.34/31.43 % (1216285)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 221.34/31.43 % (1216285)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 221.34/31.43 % (1216285)CaDiCaL version: 2.1.3 % 221.34/31.43 % (1216285)Termination reason: Instruction limit % 221.34/31.43 % (1216285)Termination phase: Saturation % 221.34/31.43 % (1216285)Time elapsed: 0.132 s % 221.34/31.43 % (1216285)Peak memory usage: 13 MB % 221.34/31.43 % (1216285)Instructions burned: 207 (million) % 221.34/31.43 % (1216287)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=78662738:i=232:rtra=on_2730 on theBenchmark for (2730ds/232Mi) % 221.34/31.43 % (1216287)Instruction limit reached! % 221.34/31.43 % (1216287)------------------------------ % 221.34/31.43 % (1216287)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 221.34/31.43 % (1216287)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 221.34/31.43 % (1216287)CaDiCaL version: 2.1.3 % 221.34/31.43 % (1216287)Termination reason: Instruction limit % 221.34/31.43 % (1216287)Termination phase: Saturation % 221.34/31.43 % (1216287)Time elapsed: 0.150 s % 221.34/31.43 % (1216287)Peak memory usage: 13 MB % 221.34/31.43 % (1216287)Instructions burned: 233 (million) % 221.34/31.43 % (1216289)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=3496752631:i=262:rtra=on_2728 on theBenchmark for (2728ds/262Mi) % 221.34/31.43 % (1216289)Instruction limit reached! % 221.34/31.43 % (1216289)------------------------------ % 221.34/31.43 % (1216289)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 221.34/31.43 % (1216289)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 221.34/31.43 % (1216289)CaDiCaL version: 2.1.3 % 221.34/31.43 % (1216289)Termination reason: Instruction limit % 221.34/31.43 % (1216289)Termination phase: Saturation % 221.34/31.43 % (1216289)Time elapsed: 0.173 s % 221.34/31.43 % (1216289)Peak memory usage: 14 MB % 221.34/31.43 % (1216289)Instructions burned: 263 (million) % 221.34/31.43 % (1216291)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=2643005772:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2726 on theBenchmark for (2726ds/318Mi) % 221.34/31.43 % (1216291)Instruction limit reached! % 221.34/31.43 % (1216291)------------------------------ % 221.34/31.43 % (1216291)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 221.34/31.43 % (1216291)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 221.34/31.43 % (1216291)CaDiCaL version: 2.1.3 % 221.34/31.43 % (1216291)Termination reason: Instruction limit % 221.34/31.43 % (1216291)Termination phase: Saturation % 221.34/31.43 % (1216291)Time elapsed: 0.219 s % 221.34/31.43 % (1216291)Peak memory usage: 15 MB % 221.34/31.43 % (1216291)Instructions burned: 318 (million) % 221.34/31.43 % (1216293)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=1559103964:i=1428:nm=2:rtra=on_2723 on theBenchmark for (2723ds/1428Mi) % 251.26/35.69 % (1216293)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 251.26/35.69 % (1216293)Terminated due to inappropriate strategy. % 251.26/35.69 % (1216293)------------------------------ % 251.26/35.69 % (1216293)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 251.26/35.69 % (1216293)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 251.26/35.69 % (1216293)CaDiCaL version: 2.1.3 % 251.26/35.69 % (1216293)Termination reason: Inappropriate % 251.26/35.69 % (1216293)Time elapsed: 0.002 s % 251.26/35.69 % (1216293)Peak memory usage: 10 MB % 251.26/35.69 % (1216293)Instructions burned: 2 (million) % 251.26/35.69 % (1216293)------------------------------ % 251.26/35.69 % (1216293)------------------------------ % 251.26/35.69 % (1216295)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=1977385862:i=262:bd=preordered:rtra=on:fsd=on_2723 on theBenchmark for (2723ds/262Mi) % 251.26/35.69 % (1216295)Instruction limit reached! % 251.26/35.69 % (1216295)------------------------------ % 251.26/35.69 % (1216295)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 251.26/35.69 % (1216295)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 251.26/35.69 % (1216295)CaDiCaL version: 2.1.3 % 251.26/35.69 % (1216295)Termination reason: Instruction limit % 251.26/35.69 % (1216295)Termination phase: Saturation % 251.26/35.69 % (1216295)Time elapsed: 0.180 s % 251.26/35.69 % (1216295)Peak memory usage: 14 MB % 251.26/35.69 % (1216295)Instructions burned: 262 (million) % 251.26/35.69 % (1216297)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=1021439956:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2721 on theBenchmark for (2721ds/1368Mi) % 251.26/35.69 % (1216297)Instruction limit reached! % 251.26/35.69 % (1216297)------------------------------ % 251.26/35.69 % (1216297)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 251.26/35.69 % (1216297)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 251.26/35.69 % (1216297)CaDiCaL version: 2.1.3 % 251.26/35.69 % (1216297)Termination reason: Instruction limit % 251.26/35.69 % (1216297)Termination phase: Saturation % 251.26/35.69 % (1216297)Time elapsed: 0.761 s % 251.26/35.69 % (1216297)Peak memory usage: 20 MB % 251.26/35.69 % (1216297)Instructions burned: 1369 (million) % 251.26/35.69 % (1216299)ott-21_1_sil=16000:si=on:fs=off:random_seed=33984972:i=360:av=off:fsr=off:rtra=on_2713 on theBenchmark for (2713ds/360Mi) % 251.26/35.69 % (1216299)Instruction limit reached! % 251.26/35.69 % (1216299)------------------------------ % 251.26/35.69 % (1216299)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 251.26/35.69 % (1216299)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 251.26/35.69 % (1216299)CaDiCaL version: 2.1.3 % 251.26/35.69 % (1216299)Termination reason: Instruction limit % 251.26/35.69 % (1216299)Termination phase: Saturation % 251.26/35.69 % (1216299)Time elapsed: 0.166 s % 251.26/35.69 % (1216299)Peak memory usage: 13 MB % 251.26/35.69 % (1216299)Instructions burned: 360 (million) % 251.26/35.69 % (1216301)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1113996242:i=954:bd=all:rtra=on_2711 on theBenchmark for (2711ds/954Mi) % 251.26/35.69 % (1216301)Instruction limit reached! % 251.26/35.69 % (1216301)------------------------------ % 251.26/35.69 % (1216301)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 251.26/35.69 % (1216301)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 251.26/35.69 % (1216301)CaDiCaL version: 2.1.3 % 251.26/35.69 % (1216301)Termination reason: Instruction limit % 251.26/35.69 % (1216301)Termination phase: Saturation % 251.26/35.69 % (1216301)Time elapsed: 0.628 s % 251.26/35.69 % (1216301)Peak memory usage: 16 MB % 251.26/35.69 % (1216301)Instructions burned: 955 (million) % 251.26/35.69 % (1216419)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=2046772281:fmbsr=1.3:i=1730:ins=25:rtra=on_2705 on theBenchmark for (2705ds/1730Mi) % 251.26/35.69 % (1216419)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 251.26/35.69 % (1216419)Terminated due to inappropriate strategy. % 251.26/35.69 % (1216419)------------------------------ % 251.26/35.69 % (1216419)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 251.26/35.69 % (1216419)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 251.26/35.69 % (1216419)CaDiCaL version: 2.1.3 % 251.26/35.69 % (1216419)Termination reason: Inappropriate % 251.26/35.69 % (Terminated % 300.16/42.54 % Vampire exiting % 300.16/42.54 Terminated %------------------------------------------------------------------------------