%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWC426_1 : TPTP v9.3.1. Bugfixed v9.1.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % Computer : n015.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:06:00 PM UTC 2026 % Result : Timeout 300.18s 42.63s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWC426_1 : TPTP v9.3.1. Bugfixed v9.1.0. % 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.09/0.20 % Computer : n015.cluster.edu % 0.09/0.20 % Model : x86_64 x86_64 % 0.09/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.20 % Memory : 8046.5625MB % 0.09/0.20 % OS : Linux 6.8.0-71-generic % 0.09/0.20 % CPULimit : 300 % 0.09/0.20 % WCLimit : 300 % 0.09/0.20 % DateTime : Mon Sep 28 09:39:46 UTC 2026 % 0.09/0.21 % CPUTime : % 0.09/0.21 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.09/0.24 Running first-order model finding % 0.09/0.24 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 % 3.79/0.85 % (2502992)Will run a generic schedule for satisfiability detection. % 3.79/0.85 % (2502998)% WARNING: option uhcvi not known. % 3.79/0.85 % (2503000)dis+10_1_sil=32000:sp=arity:random_seed=3095764275:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 3.79/0.85 % (2502997)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=4146681572_2999 on theBenchmark for (2999ds/0Mi) % 3.79/0.85 % (2502998)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2549212038:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 3.79/0.85 % (2502999)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=4200035806:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 3.79/0.85 % (2503001)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1138454933:i=116_2999 on theBenchmark for (2999ds/116Mi) % 3.79/0.85 % (2503002)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3626056984:i=131_2999 on theBenchmark for (2999ds/131Mi) % 3.79/0.85 % (2503003)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2694041277:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 3.79/0.85 % (2502997)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.79/0.85 % (2502997)Terminated due to inappropriate strategy. % 3.79/0.85 % (2502997)------------------------------ % 3.79/0.85 % (2502997)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.79/0.85 % (2502997)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.79/0.85 % (2502997)CaDiCaL version: 2.1.3 % 3.79/0.85 % (2502997)Termination reason: Inappropriate % 3.79/0.85 % (2502997)Time elapsed: 0.001 s % 3.79/0.85 % (2502997)Peak memory usage: 10 MB % 3.79/0.85 % (2502997)Instructions burned: 1 (million) % 3.79/0.85 % (2502997)------------------------------ % 3.79/0.85 % (2502997)------------------------------ % 3.79/0.85 % (2503011)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2485271551:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 3.79/0.85 % (2503011)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.79/0.85 % (2503011)Terminated due to inappropriate strategy. % 3.79/0.85 % (2503011)------------------------------ % 3.79/0.85 % (2503011)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.79/0.85 % (2503011)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.79/0.85 % (2503011)CaDiCaL version: 2.1.3 % 3.79/0.85 % (2503011)Termination reason: Inappropriate % 3.79/0.85 % (2503011)Time elapsed: 0.001 s % 3.79/0.85 % (2503011)Peak memory usage: 10 MB % 3.79/0.85 % (2503011)Instructions burned: 1 (million) % 3.79/0.85 % (2503011)------------------------------ % 3.79/0.85 % (2503011)------------------------------ % 3.79/0.85 % (2503013)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=237808988:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 3.79/0.85 % (2503000)Instruction limit reached! % 3.79/0.85 % (2503000)------------------------------ % 3.79/0.85 % (2503000)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.79/0.85 % (2503000)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.79/0.85 % (2503000)CaDiCaL version: 2.1.3 % 3.79/0.85 % (2503000)Termination reason: Instruction limit % 3.79/0.85 % (2503000)Termination phase: Saturation % 3.79/0.85 % (2503000)Time elapsed: 0.064 s % 3.79/0.85 % (2503000)Peak memory usage: 12 MB % 3.79/0.85 % (2503000)Instructions burned: 104 (million) % 3.79/0.85 % (2503001)Instruction limit reached! % 3.79/0.85 % (2503001)------------------------------ % 3.79/0.85 % (2503001)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.79/0.85 % (2503001)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.79/0.85 % (2503001)CaDiCaL version: 2.1.3 % 3.79/0.85 % (2503001)Termination reason: Instruction limit % 3.79/0.85 % (2503001)Termination phase: Saturation % 3.79/0.85 % (2503001)Time elapsed: 0.070 s % 3.79/0.85 % (2503001)Peak memory usage: 12 MB % 3.79/0.85 % (2503001)Instructions burned: 117 (million) % 3.79/0.85 % (2503002)Instruction limit reached! % 3.79/0.85 % (2503002)------------------------------ % 3.79/0.85 % (2503002)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.79/0.85 % (2503002)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.79/0.85 % (2503002)CaDiCaL version: 2.1.3 % 3.79/0.85 % (2503002)Termination reason: Instruction limit % 6.23/1.18 % (2503002)Termination phase: Saturation % 6.23/1.18 % (2503002)Time elapsed: 0.081 s % 6.23/1.18 % (2503002)Peak memory usage: 13 MB % 6.23/1.18 % (2503002)Instructions burned: 132 (million) % 6.23/1.18 % (2503015)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=1139584187:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi) % 6.23/1.18 % (2503016)ott-21_1_sil=16000:fs=off:random_seed=4074422221:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 6.23/1.18 % (2503018)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2245339786:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 6.23/1.18 % (2503003)Instruction limit reached! % 6.23/1.18 % (2503003)------------------------------ % 6.23/1.18 % (2503003)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.23/1.18 % (2503003)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.23/1.18 % (2503003)CaDiCaL version: 2.1.3 % 6.23/1.18 % (2503003)Termination reason: Instruction limit % 6.23/1.18 % (2503003)Termination phase: Saturation % 6.23/1.18 % (2503003)Time elapsed: 0.106 s % 6.23/1.18 % (2503003)Peak memory usage: 13 MB % 6.23/1.18 % (2503003)Instructions burned: 159 (million) % 6.23/1.18 % (2503021)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1412580007:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 6.23/1.18 % (2503021)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 6.23/1.18 % (2503021)Terminated due to inappropriate strategy. % 6.23/1.18 % (2503021)------------------------------ % 6.23/1.18 % (2503021)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.23/1.18 % (2503021)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.23/1.18 % (2503021)CaDiCaL version: 2.1.3 % 6.23/1.18 % (2503021)Termination reason: Inappropriate % 6.23/1.18 % (2503021)Time elapsed: 0.001 s % 6.23/1.18 % (2503021)Peak memory usage: 10 MB % 6.23/1.18 % (2503021)Instructions burned: 1 (million) % 6.23/1.18 % (2503021)------------------------------ % 6.23/1.18 % (2503021)------------------------------ % 6.23/1.18 % (2503013)Instruction limit reached! % 6.23/1.18 % (2503013)------------------------------ % 6.23/1.18 % (2503013)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.23/1.18 % (2503013)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.23/1.18 % (2503013)CaDiCaL version: 2.1.3 % 6.23/1.18 % (2503013)Termination reason: Instruction limit % 6.23/1.18 % (2503013)Termination phase: Saturation % 6.23/1.18 % (2503013)Time elapsed: 0.087 s % 6.23/1.18 % (2503013)Peak memory usage: 12 MB % 6.23/1.18 % (2503013)Instructions burned: 132 (million) % 6.23/1.18 % (2503023)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2304502812:i=1179_2998 on theBenchmark for (2998ds/1179Mi) % 6.23/1.18 % (2503024)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=284945866:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi) % 6.23/1.18 % (2503024)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 6.23/1.18 % (2503024)Terminated due to inappropriate strategy. % 6.23/1.18 % (2503024)------------------------------ % 6.23/1.18 % (2503024)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.23/1.18 % (2503024)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.23/1.18 % (2503024)CaDiCaL version: 2.1.3 % 6.23/1.18 % (2503024)Termination reason: Inappropriate % 6.23/1.18 % (2503024)Time elapsed: 0.001 s % 6.23/1.18 % (2503024)Peak memory usage: 10 MB % 6.23/1.18 % (2503024)Instructions burned: 1 (million) % 6.23/1.18 % (2503024)------------------------------ % 6.23/1.18 % (2503024)------------------------------ % 6.23/1.18 % (2503027)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=4251214047:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2998 on theBenchmark for (2998ds/692Mi) % 6.23/1.18 % (2503016)Instruction limit reached! % 6.23/1.18 % (2503016)------------------------------ % 6.23/1.18 % (2503016)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.23/1.18 % (2503016)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.23/1.18 % (2503016)CaDiCaL version: 2.1.3 % 6.23/1.18 % (2503016)Termination reason: Instruction limit % 6.23/1.18 % (2503016)Termination phase: Saturation % 22.00/3.45 % (2503016)Time elapsed: 0.079 s % 22.00/3.45 % (2503016)Peak memory usage: 12 MB % 22.00/3.45 % (2503016)Instructions burned: 181 (million) % 22.00/3.45 % (2503029)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3416186459:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi) % 22.00/3.45 % (2503018)Instruction limit reached! % 22.00/3.45 % (2503018)------------------------------ % 22.00/3.45 % (2503018)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.00/3.45 % (2503018)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.00/3.45 % (2503018)CaDiCaL version: 2.1.3 % 22.00/3.45 % (2503018)Termination reason: Instruction limit % 22.00/3.45 % (2503018)Termination phase: Saturation % 22.00/3.45 % (2503018)Time elapsed: 0.288 s % 22.00/3.45 % (2503018)Peak memory usage: 14 MB % 22.00/3.45 % (2503018)Instructions burned: 477 (million) % 22.00/3.45 % (2503031)fmb+10_1_sil=64000:random_seed=3057091524:i=22061:nm=2:gsp=on_2995 on theBenchmark for (2995ds/22061Mi) % 22.00/3.45 % (2503031)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 22.00/3.45 % (2503031)Terminated due to inappropriate strategy. % 22.00/3.45 % (2503031)------------------------------ % 22.00/3.45 % (2503031)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.00/3.45 % (2503031)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.00/3.45 % (2503031)CaDiCaL version: 2.1.3 % 22.00/3.45 % (2503031)Termination reason: Inappropriate % 22.00/3.45 % (2503031)Time elapsed: 0.001 s % 22.00/3.45 % (2503031)Peak memory usage: 10 MB % 22.00/3.45 % (2503031)Instructions burned: 1 (million) % 22.00/3.45 % (2503031)------------------------------ % 22.00/3.45 % (2503031)------------------------------ % 22.00/3.45 % (2503015)Instruction limit reached! % 22.00/3.45 % (2503015)------------------------------ % 22.00/3.45 % (2503015)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.00/3.45 % (2503015)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.00/3.45 % (2503015)CaDiCaL version: 2.1.3 % 22.00/3.45 % (2503015)Termination reason: Instruction limit % 22.00/3.45 % (2503015)Termination phase: Saturation % 22.00/3.45 % (2503015)Time elapsed: 0.340 s % 22.00/3.45 % (2503015)Peak memory usage: 17 MB % 22.00/3.45 % (2503015)Instructions burned: 684 (million) % 22.00/3.45 % (2503033)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2318405830:i=9515:nm=5_2995 on theBenchmark for (2995ds/9515Mi) % 22.00/3.45 % (2503033)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 22.00/3.45 % (2503033)Terminated due to inappropriate strategy. % 22.00/3.45 % (2503033)------------------------------ % 22.00/3.45 % (2503033)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.00/3.45 % (2503033)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.00/3.45 % (2503033)CaDiCaL version: 2.1.3 % 22.00/3.45 % (2503033)Termination reason: Inappropriate % 22.00/3.45 % (2503033)Time elapsed: 0.001 s % 22.00/3.45 % (2503033)Peak memory usage: 10 MB % 22.00/3.45 % (2503033)Instructions burned: 1 (million) % 22.00/3.45 % (2503033)------------------------------ % 22.00/3.45 % (2503033)------------------------------ % 22.00/3.45 % (2503034)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=4027849055:fmbsr=1.7:i=920_2995 on theBenchmark for (2995ds/920Mi) % 22.00/3.45 % (2503034)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 22.00/3.45 % (2503034)Terminated due to inappropriate strategy. % 22.00/3.45 % (2503034)------------------------------ % 22.00/3.45 % (2503034)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.00/3.45 % (2503034)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.00/3.45 % (2503034)CaDiCaL version: 2.1.3 % 22.00/3.45 % (2503034)Termination reason: Inappropriate % 22.00/3.45 % (2503034)Time elapsed: 0.001 s % 22.00/3.45 % (2503034)Peak memory usage: 10 MB % 22.00/3.45 % (2503034)Instructions burned: 1 (million) % 22.00/3.45 % (2503034)------------------------------ % 22.00/3.45 % (2503034)------------------------------ % 22.00/3.45 % (2503036)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1204429450:i=5131_2995 on theBenchmark for (2995ds/5131Mi) % 22.00/3.45 % (2503038)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=4287340329:i=1472:ins=7:fdi=8:gsp=on_2995 on theBenchmark for (2995ds/1472Mi) % 22.00/3.45 % (2503027)Instruction limit reached! % 22.00/3.45 % (2503027)------------------------------ % 34.68/5.20 % (2503027)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 34.68/5.20 % (2503027)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.68/5.20 % (2503027)CaDiCaL version: 2.1.3 % 34.68/5.20 % (2503027)Termination reason: Instruction limit % 34.68/5.20 % (2503027)Termination phase: Saturation % 34.68/5.20 % (2503027)Time elapsed: 0.393 s % 34.68/5.20 % (2503027)Peak memory usage: 19 MB % 34.68/5.20 % (2503027)Instructions burned: 692 (million) % 34.68/5.20 % (2503041)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=396310309:i=6324_2993 on theBenchmark for (2993ds/6324Mi) % 34.68/5.20 % (2503041)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 34.68/5.20 % (2503041)Terminated due to inappropriate strategy. % 34.68/5.20 % (2503041)------------------------------ % 34.68/5.20 % (2503041)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 34.68/5.20 % (2503041)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.68/5.20 % (2503041)CaDiCaL version: 2.1.3 % 34.68/5.20 % (2503041)Termination reason: Inappropriate % 34.68/5.20 % (2503041)Time elapsed: 0.001 s % 34.68/5.20 % (2503041)Peak memory usage: 10 MB % 34.68/5.20 % (2503041)Instructions burned: 1 (million) % 34.68/5.20 % (2503041)------------------------------ % 34.68/5.20 % (2503041)------------------------------ % 34.68/5.20 % (2503043)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=3316483123:fmbsr=2.30978:i=2174_2993 on theBenchmark for (2993ds/2174Mi) % 34.68/5.20 % (2503043)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 34.68/5.20 % (2503043)Terminated due to inappropriate strategy. % 34.68/5.20 % (2503043)------------------------------ % 34.68/5.20 % (2503043)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 34.68/5.20 % (2503043)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.68/5.20 % (2503043)CaDiCaL version: 2.1.3 % 34.68/5.20 % (2503043)Termination reason: Inappropriate % 34.68/5.20 % (2503043)Time elapsed: 0.001 s % 34.68/5.20 % (2503043)Peak memory usage: 11 MB % 34.68/5.20 % (2503043)Instructions burned: 1 (million) % 34.68/5.20 % (2503043)------------------------------ % 34.68/5.20 % (2503043)------------------------------ % 34.68/5.20 % (2503045)ott-2_1_sil=16000:newcnf=on:random_seed=2638217208:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2993 on theBenchmark for (2993ds/869Mi) % 34.68/5.20 % (2503029)Instruction limit reached! % 34.68/5.20 % (2503029)------------------------------ % 34.68/5.20 % (2503029)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 34.68/5.20 % (2503029)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.68/5.20 % (2503029)CaDiCaL version: 2.1.3 % 34.68/5.20 % (2503029)Termination reason: Instruction limit % 34.68/5.20 % (2503029)Termination phase: Saturation % 34.68/5.20 % (2503029)Time elapsed: 0.477 s % 34.68/5.20 % (2503029)Peak memory usage: 19 MB % 34.68/5.20 % (2503029)Instructions burned: 880 (million) % 34.68/5.20 % (2503047)ott+10_1_sil=32000:tgt=ground:random_seed=949868956:i=5114:av=off_2992 on theBenchmark for (2992ds/5114Mi) % 34.68/5.20 % (2503023)Instruction limit reached! % 34.68/5.20 % (2503023)------------------------------ % 34.68/5.20 % (2503023)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 34.68/5.20 % (2503023)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.68/5.20 % (2503023)CaDiCaL version: 2.1.3 % 34.68/5.20 % (2503023)Termination reason: Instruction limit % 34.68/5.20 % (2503023)Termination phase: Saturation % 34.68/5.20 % (2503023)Time elapsed: 0.726 s % 34.68/5.20 % (2503023)Peak memory usage: 20 MB % 34.68/5.20 % (2503023)Instructions burned: 1179 (million) % 34.68/5.20 % (2503049)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=143302908:i=54282_2990 on theBenchmark for (2990ds/54282Mi) % 34.68/5.20 % (2503049)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 34.68/5.20 % (2503049)Terminated due to inappropriate strategy. % 34.68/5.20 % (2503049)------------------------------ % 34.68/5.20 % (2503049)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 34.68/5.20 % (2503049)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.68/5.20 % (2503049)CaDiCaL version: 2.1.3 % 34.68/5.20 % (2503049)Termination reason: Inappropriate % 34.68/5.20 % (2503049)Time elapsed: 0.001 s % 34.68/5.20 % (2503049)Peak memory usage: 10 MB % 34.68/5.20 % (2503049)Instructions burned: 1 (million) % 110.42/15.87 % (2503049)------------------------------ % 110.42/15.87 % (2503049)------------------------------ % 110.42/15.87 % (2503051)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=1509201440:i=3512:aac=none_2990 on theBenchmark for (2990ds/3512Mi) % 110.42/15.87 % (2503045)Instruction limit reached! % 110.42/15.87 % (2503045)------------------------------ % 110.42/15.87 % (2503045)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 110.42/15.87 % (2503045)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 110.42/15.87 % (2503045)CaDiCaL version: 2.1.3 % 110.42/15.87 % (2503045)Termination reason: Instruction limit % 110.42/15.87 % (2503045)Termination phase: Saturation % 110.42/15.87 % (2503045)Time elapsed: 0.505 s % 110.42/15.87 % (2503045)Peak memory usage: 15 MB % 110.42/15.87 % (2503045)Instructions burned: 869 (million) % 110.42/15.87 % (2503053)dis+21_1_sil=32000:sas=cadical:random_seed=2935242501:i=3773:amm=off_2988 on theBenchmark for (2988ds/3773Mi) % 110.42/15.87 % (2503038)Instruction limit reached! % 110.42/15.87 % (2503038)------------------------------ % 110.42/15.87 % (2503038)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 110.42/15.87 % (2503038)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 110.42/15.87 % (2503038)CaDiCaL version: 2.1.3 % 110.42/15.87 % (2503038)Termination reason: Instruction limit % 110.42/15.87 % (2503038)Termination phase: Saturation % 110.42/15.87 % (2503038)Time elapsed: 0.830 s % 110.42/15.87 % (2503038)Peak memory usage: 24 MB % 110.42/15.87 % (2503038)Instructions burned: 1473 (million) % 110.42/15.87 % (2503055)ott+11_1_sil=16000:gs=on:random_seed=3928138947:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2986 on theBenchmark for (2986ds/2251Mi) % 110.42/15.87 % (2503055)Instruction limit reached! % 110.42/15.87 % (2503055)------------------------------ % 110.42/15.87 % (2503055)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 110.42/15.87 % (2503055)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 110.42/15.87 % (2503055)CaDiCaL version: 2.1.3 % 110.42/15.87 % (2503055)Termination reason: Instruction limit % 110.42/15.87 % (2503055)Termination phase: Saturation % 110.42/15.87 % (2503055)Time elapsed: 1.214 s % 110.42/15.87 % (2503055)Peak memory usage: 24 MB % 110.42/15.87 % (2503055)Instructions burned: 2253 (million) % 110.42/15.87 % (2503057)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=2826952834:fmbsr=1.6:i=67534_2974 on theBenchmark for (2974ds/67534Mi) % 110.42/15.87 % (2503057)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 110.42/15.87 % (2503057)Terminated due to inappropriate strategy. % 110.42/15.87 % (2503057)------------------------------ % 110.42/15.87 % (2503057)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 110.42/15.87 % (2503057)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 110.42/15.87 % (2503057)CaDiCaL version: 2.1.3 % 110.42/15.87 % (2503057)Termination reason: Inappropriate % 110.42/15.87 % (2503057)Time elapsed: 0.001 s % 110.42/15.87 % (2503057)Peak memory usage: 10 MB % 110.42/15.87 % (2503057)Instructions burned: 1 (million) % 110.42/15.87 % (2503057)------------------------------ % 110.42/15.87 % (2503057)------------------------------ % 110.42/15.87 % (2503059)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=353084885:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2974 on theBenchmark for (2974ds/4591Mi) % 110.42/15.87 % (2503051)Instruction limit reached! % 110.42/15.87 % (2503051)------------------------------ % 110.42/15.87 % (2503051)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 110.42/15.87 % (2503051)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 110.42/15.87 % (2503051)CaDiCaL version: 2.1.3 % 110.42/15.87 % (2503051)Termination reason: Instruction limit % 110.42/15.87 % (2503051)Termination phase: Saturation % 110.42/15.87 % (2503051)Time elapsed: 1.835 s % 110.42/15.87 % (2503051)Peak memory usage: 35 MB % 110.42/15.87 % (2503051)Instructions burned: 3512 (million) % 110.42/15.87 % (2503061)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=510640872:i=29340_2972 on theBenchmark for (2972ds/29340Mi) % 110.42/15.87 % (2503053)Instruction limit reached! % 110.42/15.87 % (2503053)------------------------------ % 110.42/15.87 % (2503053)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 110.42/15.87 % (2503053)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 110.42/15.87 % (2503053)CaDiCaL version: 2.1.3 % 110.42/15.87 % (2503053)Termination reason: Instruction limit % 130.30/18.63 % (2503053)Termination phase: Saturation % 130.30/18.63 % (2503053)Time elapsed: 2.016 s % 130.30/18.63 % (2503053)Peak memory usage: 31 MB % 130.30/18.63 % (2503053)Instructions burned: 3773 (million) % 130.30/18.63 % (2503063)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=1389642242:i=5211_2967 on theBenchmark for (2967ds/5211Mi) % 130.30/18.63 % (2503036)Instruction limit reached! % 130.30/18.63 % (2503036)------------------------------ % 130.30/18.63 % (2503036)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 130.30/18.63 % (2503036)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 130.30/18.63 % (2503036)CaDiCaL version: 2.1.3 % 130.30/18.63 % (2503036)Termination reason: Instruction limit % 130.30/18.63 % (2503036)Termination phase: Saturation % 130.30/18.63 % (2503036)Time elapsed: 2.744 s % 130.30/18.63 % (2503036)Peak memory usage: 41 MB % 130.30/18.63 % (2503036)Instructions burned: 5131 (million) % 130.30/18.63 % (2503065)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=3323827153:i=5497:nm=2_2967 on theBenchmark for (2967ds/5497Mi) % 130.30/18.63 % (2503065)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 130.30/18.63 % (2503065)Terminated due to inappropriate strategy. % 130.30/18.63 % (2503065)------------------------------ % 130.30/18.63 % (2503065)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 130.30/18.63 % (2503065)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 130.30/18.63 % (2503065)CaDiCaL version: 2.1.3 % 130.30/18.63 % (2503065)Termination reason: Inappropriate % 130.30/18.63 % (2503065)Time elapsed: 0.001 s % 130.30/18.63 % (2503065)Peak memory usage: 10 MB % 130.30/18.63 % (2503065)Instructions burned: 1 (million) % 130.30/18.63 % (2503065)------------------------------ % 130.30/18.63 % (2503065)------------------------------ % 130.30/18.63 % (2503067)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=1029083806:fmbsr=2:i=46332_2967 on theBenchmark for (2967ds/46332Mi) % 130.30/18.63 % (2503067)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 130.30/18.63 % (2503067)Terminated due to inappropriate strategy. % 130.30/18.63 % (2503067)------------------------------ % 130.30/18.63 % (2503067)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 130.30/18.63 % (2503067)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 130.30/18.63 % (2503067)CaDiCaL version: 2.1.3 % 130.30/18.63 % (2503067)Termination reason: Inappropriate % 130.30/18.63 % (2503067)Time elapsed: 0.001 s % 130.30/18.63 % (2503067)Peak memory usage: 10 MB % 130.30/18.63 % (2503067)Instructions burned: 1 (million) % 130.30/18.63 % (2503067)------------------------------ % 130.30/18.63 % (2503067)------------------------------ % 130.30/18.63 % (2503069)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=3199965148:i=14071_2967 on theBenchmark for (2967ds/14071Mi) % 130.30/18.63 % (2503069)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 130.30/18.63 % (2503069)Terminated due to inappropriate strategy. % 130.30/18.63 % (2503069)------------------------------ % 130.30/18.63 % (2503069)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 130.30/18.63 % (2503069)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 130.30/18.63 % (2503069)CaDiCaL version: 2.1.3 % 130.30/18.63 % (2503069)Termination reason: Inappropriate % 130.30/18.63 % (2503069)Time elapsed: 0.001 s % 130.30/18.63 % (2503069)Peak memory usage: 10 MB % 130.30/18.63 % (2503069)Instructions burned: 1 (million) % 130.30/18.63 % (2503069)------------------------------ % 130.30/18.63 % (2503069)------------------------------ % 130.30/18.63 % (2503071)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1517278453:i=22565:add=on:rawr=on_2966 on theBenchmark for (2966ds/22565Mi) % 130.30/18.63 % (2503047)Instruction limit reached! % 130.30/18.63 % (2503047)------------------------------ % 130.30/18.63 % (2503047)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 130.30/18.63 % (2503047)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 130.30/18.63 % (2503047)CaDiCaL version: 2.1.3 % 130.30/18.63 % (2503047)Termination reason: Instruction limit % 130.30/18.63 % (2503047)Termination phase: Saturation % 130.30/18.63 % (2503047)Time elapsed: 3.257 s % 130.30/18.63 % (2503047)Peak memory usage: 42 MB % 130.30/18.63 % (2503047)Instructions burned: 5115 (million) % 130.30/18.63 % (2503073)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=2055689464:i=8173:av=off_2960 on theBenchmark for (2960ds/8173Mi) % 130.30/18.63 % (2503059)Instruction limit reached! % 131.02/18.74 % (2503059)------------------------------ % 131.02/18.74 % (2503059)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 131.02/18.74 % (2503059)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 131.02/18.74 % (2503059)CaDiCaL version: 2.1.3 % 131.02/18.74 % (2503059)Termination reason: Instruction limit % 131.02/18.74 % (2503059)Termination phase: Saturation % 131.02/18.74 % (2503059)Time elapsed: 2.338 s % 131.02/18.74 % (2503059)Peak memory usage: 48 MB % 131.02/18.74 % (2503059)Instructions burned: 4592 (million) % 131.02/18.74 % (2503075)dis+10_16:1_sil=16000:random_seed=2586443752:i=9155:fsr=off_2950 on theBenchmark for (2950ds/9155Mi) % 131.02/18.74 % (2503063)Instruction limit reached! % 131.02/18.74 % (2503063)------------------------------ % 131.02/18.74 % (2503063)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 131.02/18.74 % (2503063)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 131.02/18.74 % (2503063)CaDiCaL version: 2.1.3 % 131.02/18.74 % (2503063)Termination reason: Instruction limit % 131.02/18.74 % (2503063)Termination phase: Saturation % 131.02/18.74 % (2503063)Time elapsed: 2.726 s % 131.02/18.74 % (2503063)Peak memory usage: 50 MB % 131.02/18.74 % (2503063)Instructions burned: 5213 (million) % 131.02/18.74 % (2503077)ott-3_8_sil=64000:random_seed=2024216556:i=20139:bs=on_2940 on theBenchmark for (2940ds/20139Mi) % 131.02/18.74 % (2503073)Instruction limit reached! % 131.02/18.74 % (2503073)------------------------------ % 131.02/18.74 % (2503073)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 131.02/18.74 % (2503073)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 131.02/18.74 % (2503073)CaDiCaL version: 2.1.3 % 131.02/18.74 % (2503073)Termination reason: Instruction limit % 131.02/18.74 % (2503073)Termination phase: Saturation % 131.02/18.74 % (2503073)Time elapsed: 5.076 s % 131.02/18.74 % (2503073)Peak memory usage: 52 MB % 131.02/18.74 % (2503073)Instructions burned: 8173 (million) % 131.02/18.74 % (2503079)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=3809333867:fmbsr=2:i=32576_2909 on theBenchmark for (2909ds/32576Mi) % 131.02/18.74 % (2503079)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 131.02/18.74 % (2503079)Terminated due to inappropriate strategy. % 131.02/18.74 % (2503079)------------------------------ % 131.02/18.74 % (2503079)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 131.02/18.74 % (2503079)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 131.02/18.74 % (2503079)CaDiCaL version: 2.1.3 % 131.02/18.74 % (2503079)Termination reason: Inappropriate % 131.02/18.74 % (2503079)Time elapsed: 0.001 s % 131.02/18.74 % (2503079)Peak memory usage: 10 MB % 131.02/18.74 % (2503079)Instructions burned: 1 (million) % 131.02/18.74 % (2503079)------------------------------ % 131.02/18.74 % (2503079)------------------------------ % 131.02/18.74 % (2503081)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=3307024124:i=11404_2908 on theBenchmark for (2908ds/11404Mi) % 131.02/18.74 % (2503075)Instruction limit reached! % 131.02/18.74 % (2503075)------------------------------ % 131.02/18.74 % (2503075)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 131.02/18.74 % (2503075)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 131.02/18.74 % (2503075)CaDiCaL version: 2.1.3 % 131.02/18.74 % (2503075)Termination reason: Instruction limit % 131.02/18.74 % (2503075)Termination phase: Saturation % 131.02/18.74 % (2503075)Time elapsed: 4.620 s % 131.02/18.74 % (2503075)Peak memory usage: 52 MB % 131.02/18.74 % (2503075)Instructions burned: 9155 (million) % 131.02/18.74 % (2503083)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=1624411150:i=14134_2903 on theBenchmark for (2903ds/14134Mi) % 131.02/18.74 % (2503071)Instruction limit reached! % 131.02/18.74 % (2503071)------------------------------ % 131.02/18.74 % (2503071)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 131.02/18.74 % (2503071)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 131.02/18.74 % (2503071)CaDiCaL version: 2.1.3 % 131.02/18.74 % (2503071)Termination reason: Instruction limit % 131.02/18.74 % (2503071)Termination phase: Saturation % 131.02/18.74 % (2503071)Time elapsed: 9.779 s % 131.02/18.74 % (2503071)Peak memory usage: 72 MB % 131.02/18.74 % (2503071)Instructions burned: 22566 (million) % 131.02/18.74 % (2503085)dis+33_16_sil=32000:sac=on:random_seed=1335390338:i=15851:nm=0_2868 on theBenchmark for (2868ds/15851Mi) % 131.02/18.74 % (2503061)Instruction limit reached! % 131.02/18.74 % (2503061)------------------------------ % 131.02/18.74 % (2503061)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 170.04/24.27 % (2503061)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 170.04/24.27 % (2503061)CaDiCaL version: 2.1.3 % 170.04/24.27 % (2503061)Termination reason: Instruction limit % 170.04/24.27 % (2503061)Termination phase: Saturation % 170.04/24.27 % (2503061)Time elapsed: 12.811 s % 170.04/24.27 % (2503061)Peak memory usage: 171 MB % 170.04/24.27 % (2503061)Instructions burned: 29342 (million) % 170.04/24.27 % (2503087)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=3333867628:avsq=on:i=17627:add=on:amm=off_2843 on theBenchmark for (2843ds/17627Mi) % 170.04/24.27 % (2503081)Instruction limit reached! % 170.04/24.27 % (2503081)------------------------------ % 170.04/24.27 % (2503081)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 170.04/24.27 % (2503081)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 170.04/24.27 % (2503081)CaDiCaL version: 2.1.3 % 170.04/24.27 % (2503081)Termination reason: Instruction limit % 170.04/24.27 % (2503081)Termination phase: Saturation % 170.04/24.27 % (2503081)Time elapsed: 7.064 s % 170.04/24.27 % (2503081)Peak memory usage: 71 MB % 170.04/24.27 % (2503081)Instructions burned: 11405 (million) % 170.04/24.27 % (2503089)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=901129246:s2a=on:i=53295_2837 on theBenchmark for (2837ds/53295Mi) % 170.04/24.27 % (2503077)Instruction limit reached! % 170.04/24.27 % (2503077)------------------------------ % 170.04/24.27 % (2503077)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 170.04/24.27 % (2503077)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 170.04/24.27 % (2503077)CaDiCaL version: 2.1.3 % 170.04/24.27 % (2503077)Termination reason: Instruction limit % 170.04/24.27 % (2503077)Termination phase: Saturation % 170.04/24.27 % (2503077)Time elapsed: 10.897 s % 170.04/24.27 % (2503077)Peak memory usage: 55 MB % 170.04/24.27 % (2503077)Instructions burned: 20139 (million) % 170.04/24.27 % (2503091)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=2022563154:i=26857:ins=20_2831 on theBenchmark for (2831ds/26857Mi) % 170.04/24.27 % (2503091)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 170.04/24.27 % (2503091)Terminated due to inappropriate strategy. % 170.04/24.27 % (2503091)------------------------------ % 170.04/24.27 % (2503091)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 170.04/24.27 % (2503091)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 170.04/24.27 % (2503091)CaDiCaL version: 2.1.3 % 170.04/24.27 % (2503091)Termination reason: Inappropriate % 170.04/24.27 % (2503091)Time elapsed: 0.001 s % 170.04/24.27 % (2503091)Peak memory usage: 10 MB % 170.04/24.27 % (2503091)Instructions burned: 1 (million) % 170.04/24.27 % (2503091)------------------------------ % 170.04/24.27 % (2503091)------------------------------ % 170.04/24.27 % (2503093)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=1744884626:i=28120:bs=on:fsr=off_2830 on theBenchmark for (2830ds/28120Mi) % 170.04/24.27 % (2503083)Instruction limit reached! % 170.04/24.27 % (2503083)------------------------------ % 170.04/24.27 % (2503083)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 170.04/24.27 % (2503083)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 170.04/24.27 % (2503083)CaDiCaL version: 2.1.3 % 170.04/24.27 % (2503083)Termination reason: Instruction limit % 170.04/24.27 % (2503083)Termination phase: Saturation % 170.04/24.27 % (2503083)Time elapsed: 8.716 s % 170.04/24.27 % (2503083)Peak memory usage: 73 MB % 170.04/24.27 % (2503083)Instructions burned: 14134 (million) % 170.04/24.27 % (2503095)fmb+10_1_sil=256000:fmbss=7:random_seed=651546655:fmbsr=1.6:i=182295_2816 on theBenchmark for (2816ds/182295Mi) % 170.04/24.27 % (2503095)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 170.04/24.27 % (2503095)Terminated due to inappropriate strategy. % 170.04/24.27 % (2503095)------------------------------ % 170.04/24.27 % (2503095)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 170.04/24.27 % (2503095)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 170.04/24.27 % (2503095)CaDiCaL version: 2.1.3 % 170.04/24.27 % (2503095)Termination reason: Inappropriate % 170.04/24.27 % (2503095)Time elapsed: 0.001 s % 170.04/24.27 % (2503095)Peak memory usage: 10 MB % 170.04/24.27 % (2503095)Instructions burned: 1 (million) % 170.04/24.27 % (2503095)------------------------------ % 170.04/24.27 % (2503095)------------------------------ % 170.04/24.27 % (2503097)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=2625939795:i=44625:gsp=on_2816 on theBenchmark for (2816ds/44625Mi) % 173.26/24.79 % (2503097)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 173.26/24.79 % (2503097)Terminated due to inappropriate strategy. % 173.26/24.79 % (2503097)------------------------------ % 173.26/24.79 % (2503097)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 173.26/24.79 % (2503097)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 173.26/24.79 % (2503097)CaDiCaL version: 2.1.3 % 173.26/24.79 % (2503097)Termination reason: Inappropriate % 173.26/24.79 % (2503097)Time elapsed: 0.001 s % 173.26/24.79 % (2503097)Peak memory usage: 10 MB % 173.26/24.79 % (2503097)Instructions burned: 1 (million) % 173.26/24.79 % (2503097)------------------------------ % 173.26/24.79 % (2503097)------------------------------ % 173.26/24.79 % (2503099)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=124392865:i=160505_2816 on theBenchmark for (2816ds/160505Mi) % 173.26/24.79 % (2503099)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 173.26/24.79 % (2503099)Terminated due to inappropriate strategy. % 173.26/24.79 % (2503099)------------------------------ % 173.26/24.79 % (2503099)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 173.26/24.79 % (2503099)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 173.26/24.79 % (2503099)CaDiCaL version: 2.1.3 % 173.26/24.79 % (2503099)Termination reason: Inappropriate % 173.26/24.79 % (2503099)Time elapsed: 0.001 s % 173.26/24.79 % (2503099)Peak memory usage: 10 MB % 173.26/24.79 % (2503099)Instructions burned: 1 (million) % 173.26/24.79 % (2503099)------------------------------ % 173.26/24.79 % (2503099)------------------------------ % 173.26/24.79 % (2503101)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=429385834:fmbsr=1.3:i=225729_2815 on theBenchmark for (2815ds/225729Mi) % 173.26/24.79 % (2503101)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 173.26/24.79 % (2503101)Terminated due to inappropriate strategy. % 173.26/24.79 % (2503101)------------------------------ % 173.26/24.79 % (2503101)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 173.26/24.79 % (2503101)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 173.26/24.79 % (2503101)CaDiCaL version: 2.1.3 % 173.26/24.79 % (2503101)Termination reason: Inappropriate % 173.26/24.79 % (2503101)Time elapsed: 0.001 s % 173.26/24.79 % (2503101)Peak memory usage: 11 MB % 173.26/24.79 % (2503101)Instructions burned: 1 (million) % 173.26/24.79 % (2503101)------------------------------ % 173.26/24.79 % (2503101)------------------------------ % 173.26/24.79 % (2503103)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=1330204099:fmbsr=2:i=185024:ins=7_2815 on theBenchmark for (2815ds/185024Mi) % 173.26/24.79 % (2503103)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 173.26/24.79 % (2503103)Terminated due to inappropriate strategy. % 173.26/24.79 % (2503103)------------------------------ % 173.26/24.79 % (2503103)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 173.26/24.79 % (2503103)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 173.26/24.79 % (2503103)CaDiCaL version: 2.1.3 % 173.26/24.79 % (2503103)Termination reason: Inappropriate % 173.26/24.79 % (2503103)Time elapsed: 0.002 s % 173.26/24.79 % (2503103)Peak memory usage: 10 MB % 173.26/24.79 % (2503103)Instructions burned: 1 (million) % 173.26/24.79 % (2503103)------------------------------ % 173.26/24.79 % (2503103)------------------------------ % 173.26/24.79 % (2503105)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=4156176659:rtra=on_2815 on theBenchmark for (2815ds/0Mi) % 173.26/24.79 % (2503105)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 173.26/24.79 % (2503105)Terminated due to inappropriate strategy. % 173.26/24.79 % (2503105)------------------------------ % 173.26/24.79 % (2503105)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 173.26/24.79 % (2503105)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 173.26/24.79 % (2503105)CaDiCaL version: 2.1.3 % 173.26/24.79 % (2503105)Termination reason: Inappropriate % 173.26/24.79 % (2503105)Time elapsed: 0.001 s % 173.26/24.79 % (2503105)Peak memory usage: 10 MB % 173.26/24.79 % (2503105)Instructions burned: 1 (million) % 173.26/24.79 % (2503105)------------------------------ % 173.26/24.79 % (2503105)------------------------------ % 173.26/24.79 % (2503107)% WARNING: option uhcvi not known. % 173.26/24.79 % (2503107)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=4085996552:i=271062:add=off:rtra=on:rawr=on_2815 on theBenchmark for (2815ds/271062Mi) % 183.06/26.10 % (2503085)Instruction limit reached! % 183.06/26.10 % (2503085)------------------------------ % 183.06/26.10 % (2503085)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 183.06/26.10 % (2503085)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 183.06/26.10 % (2503085)CaDiCaL version: 2.1.3 % 183.06/26.10 % (2503085)Termination reason: Instruction limit % 183.06/26.10 % (2503085)Termination phase: Saturation % 183.06/26.10 % (2503085)Time elapsed: 7.208 s % 183.06/26.10 % (2503085)Peak memory usage: 203 MB % 183.06/26.10 % (2503085)Instructions burned: 15852 (million) % 183.06/26.10 % (2503109)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1226668510:i=176048:add=on:rtra=on:rawr=on_2796 on theBenchmark for (2796ds/176048Mi) % 183.06/26.10 % (2502999)Instruction limit reached! % 183.06/26.10 % (2502999)------------------------------ % 183.06/26.10 % (2502999)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 183.06/26.10 % (2502999)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 183.06/26.10 % (2502999)CaDiCaL version: 2.1.3 % 183.06/26.10 % (2502999)Termination reason: Instruction limit % 183.06/26.10 % (2502999)Termination phase: Saturation % 183.06/26.10 % (2502999)Time elapsed: 23.528 s % 183.06/26.10 % (2502999)Peak memory usage: 2018 MB % 183.06/26.10 % (2502999)Instructions burned: 88025 (million) % 183.06/26.10 % (2503111)dis+10_1_sil=32000:si=on:sp=arity:random_seed=3965128907:i=206:fgj=on:rtra=on_2762 on theBenchmark for (2762ds/206Mi) % 183.06/26.10 % (2503111)Instruction limit reached! % 183.06/26.10 % (2503111)------------------------------ % 183.06/26.10 % (2503111)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 183.06/26.10 % (2503111)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 183.06/26.10 % (2503111)CaDiCaL version: 2.1.3 % 183.06/26.10 % (2503111)Termination reason: Instruction limit % 183.06/26.10 % (2503111)Termination phase: Saturation % 183.06/26.10 % (2503111)Time elapsed: 0.067 s % 183.06/26.10 % (2503111)Peak memory usage: 13 MB % 183.06/26.10 % (2503111)Instructions burned: 209 (million) % 183.06/26.10 % (2503113)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=2823328090:i=232:rtra=on_2761 on theBenchmark for (2761ds/232Mi) % 183.06/26.10 % (2503113)Instruction limit reached! % 183.06/26.10 % (2503113)------------------------------ % 183.06/26.10 % (2503113)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 183.06/26.10 % (2503113)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 183.06/26.10 % (2503113)CaDiCaL version: 2.1.3 % 183.06/26.10 % (2503113)Termination reason: Instruction limit % 183.06/26.10 % (2503113)Termination phase: Saturation % 183.06/26.10 % (2503113)Time elapsed: 0.078 s % 183.06/26.10 % (2503113)Peak memory usage: 13 MB % 183.06/26.10 % (2503113)Instructions burned: 232 (million) % 183.06/26.10 % (2503115)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=3815761419:i=262:rtra=on_2760 on theBenchmark for (2760ds/262Mi) % 183.06/26.10 % (2503087)Instruction limit reached! % 183.06/26.10 % (2503087)------------------------------ % 183.06/26.10 % (2503087)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 183.06/26.10 % (2503087)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 183.06/26.10 % (2503087)CaDiCaL version: 2.1.3 % 183.06/26.10 % (2503087)Termination reason: Instruction limit % 183.06/26.10 % (2503087)Termination phase: Saturation % 183.06/26.10 % (2503087)Time elapsed: 8.288 s % 183.06/26.10 % (2503087)Peak memory usage: 234 MB % 183.06/26.10 % (2503087)Instructions burned: 17630 (million) % 183.06/26.10 % (2503117)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=1375301260:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2760 on theBenchmark for (2760ds/318Mi) % 183.06/26.10 % (2503115)Instruction limit reached! % 183.06/26.10 % (2503115)------------------------------ % 183.06/26.10 % (2503115)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 183.06/26.10 % (2503115)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 183.06/26.10 % (2503115)CaDiCaL version: 2.1.3 % 183.06/26.10 % (2503115)Termination reason: Instruction limit % 183.06/26.10 % (2503115)Termination phase: Saturation % 183.06/26.10 % (2503115)Time elapsed: 0.087 s % 183.06/26.10 % (2503115)Peak memory usage: 14 MB % 183.06/26.10 % (2503115)Instructions burned: 266 (million) % 183.06/26.10 % (2503119)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=3644213346:i=1428:nm=2:rtra=on_2759 on theBenchmark for (2759ds/1428Mi) % 195.63/27.81 % (2503119)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 195.63/27.81 % (2503119)Terminated due to inappropriate strategy. % 195.63/27.81 % (2503119)------------------------------ % 195.63/27.81 % (2503119)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 195.63/27.81 % (2503119)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 195.63/27.81 % (2503119)CaDiCaL version: 2.1.3 % 195.63/27.81 % (2503119)Termination reason: Inappropriate % 195.63/27.81 % (2503119)Time elapsed: 0.0000 s % 195.63/27.81 % (2503119)Peak memory usage: 10 MB % 195.63/27.81 % (2503119)Instructions burned: 1 (million) % 195.63/27.81 % (2503119)------------------------------ % 195.63/27.81 % (2503119)------------------------------ % 195.63/27.81 % (2503121)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=1329255022:i=262:bd=preordered:rtra=on:fsd=on_2759 on theBenchmark for (2759ds/262Mi) % 195.63/27.81 % (2503121)Instruction limit reached! % 195.63/27.81 % (2503121)------------------------------ % 195.63/27.81 % (2503121)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 195.63/27.81 % (2503121)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 195.63/27.81 % (2503121)CaDiCaL version: 2.1.3 % 195.63/27.81 % (2503121)Termination reason: Instruction limit % 195.63/27.81 % (2503121)Termination phase: Saturation % 195.63/27.81 % (2503121)Time elapsed: 0.097 s % 195.63/27.81 % (2503121)Peak memory usage: 14 MB % 195.63/27.81 % (2503121)Instructions burned: 264 (million) % 195.63/27.81 % (2503123)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=561934556:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2758 on theBenchmark for (2758ds/1368Mi) % 195.63/27.81 % (2503117)Instruction limit reached! % 195.63/27.81 % (2503117)------------------------------ % 195.63/27.81 % (2503117)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 195.63/27.81 % (2503117)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 195.63/27.81 % (2503117)CaDiCaL version: 2.1.3 % 195.63/27.81 % (2503117)Termination reason: Instruction limit % 195.63/27.81 % (2503117)Termination phase: Saturation % 195.63/27.81 % (2503117)Time elapsed: 0.214 s % 195.63/27.81 % (2503117)Peak memory usage: 15 MB % 195.63/27.81 % (2503117)Instructions burned: 318 (million) % 195.63/27.81 % (2503125)ott-21_1_sil=16000:si=on:fs=off:random_seed=970265634:i=360:av=off:fsr=off:rtra=on_2757 on theBenchmark for (2757ds/360Mi) % 195.63/27.81 % (2503125)Instruction limit reached! % 195.63/27.81 % (2503125)------------------------------ % 195.63/27.81 % (2503125)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 195.63/27.81 % (2503125)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 195.63/27.81 % (2503125)CaDiCaL version: 2.1.3 % 195.63/27.81 % (2503125)Termination reason: Instruction limit % 195.63/27.81 % (2503125)Termination phase: Saturation % 195.63/27.81 % (2503125)Time elapsed: 0.160 s % 195.63/27.81 % (2503125)Peak memory usage: 13 MB % 195.63/27.81 % (2503125)Instructions burned: 360 (million) % 195.63/27.81 % (2503127)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1089863338:i=954:bd=all:rtra=on_2755 on theBenchmark for (2755ds/954Mi) % 195.63/27.81 % (2503123)Instruction limit reached! % 195.63/27.81 % (2503123)------------------------------ % 195.63/27.81 % (2503123)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 195.63/27.81 % (2503123)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 195.63/27.81 % (2503123)CaDiCaL version: 2.1.3 % 195.63/27.81 % (2503123)Termination reason: Instruction limit % 195.63/27.81 % (2503123)Termination phase: Saturation % 195.63/27.81 % (2503123)Time elapsed: 0.388 s % 195.63/27.81 % (2503123)Peak memory usage: 22 MB % 195.63/27.81 % (2503123)Instructions burned: 1369 (million) % 195.63/27.81 % (2503129)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=1262881764:fmbsr=1.3:i=1730:ins=25:rtra=on_2754 on theBenchmark for (2754ds/1730Mi) % 195.63/27.81 % (2503129)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 195.63/27.81 % (2503129)Terminated due to inappropriate strategy. % 195.63/27.81 % (2503129)------------------------------ % 195.63/27.81 % (2503129)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 195.63/27.81 % (2503129)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 195.63/27.81 % (2503129)CaDiCaL version: 2.1.3 % 195.63/27.81 % (2503129)Termination reason: Inappropriate % 221.90/31.56 % (2503129)Time elapsed: 0.0000 s % 221.90/31.56 % (2503129)Peak memory usage: 10 MB % 221.90/31.56 % (2503129)Instructions burned: 1 (million) % 221.90/31.56 % (2503129)------------------------------ % 221.90/31.56 % (2503129)------------------------------ % 221.90/31.56 % (2503131)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=4128845075:i=2358:rtra=on_2754 on theBenchmark for (2754ds/2358Mi) % 221.90/31.56 % (2503127)Instruction limit reached! % 221.90/31.56 % (2503127)------------------------------ % 221.90/31.56 % (2503127)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 221.90/31.56 % (2503127)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 221.90/31.56 % (2503127)CaDiCaL version: 2.1.3 % 221.90/31.56 % (2503127)Termination reason: Instruction limit % 221.90/31.56 % (2503127)Termination phase: Saturation % 221.90/31.56 % (2503127)Time elapsed: 0.580 s % 221.90/31.56 % (2503127)Peak memory usage: 16 MB % 221.90/31.56 % (2503127)Instructions burned: 954 (million) % 221.90/31.56 % (2503133)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=4284423125:i=1778:ins=1:rtra=on_2749 on theBenchmark for (2749ds/1778Mi) % 221.90/31.56 % (2503133)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 221.90/31.56 % (2503133)Terminated due to inappropriate strategy. % 221.90/31.56 % (2503133)------------------------------ % 221.90/31.56 % (2503133)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 221.90/31.56 % (2503133)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 221.90/31.56 % (2503133)CaDiCaL version: 2.1.3 % 221.90/31.56 % (2503133)Termination reason: Inappropriate % 221.90/31.56 % (2503133)Time elapsed: 0.001 s % 221.90/31.56 % (2503133)Peak memory usage: 10 MB % 221.90/31.56 % (2503133)Instructions burned: 1 (million) % 221.90/31.56 % (2503133)------------------------------ % 221.90/31.56 % (2503133)------------------------------ % 221.90/31.56 % (2503135)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:si=on:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=1723289645:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2749 on theBenchmark for (2749ds/1384Mi) % 221.90/31.56 % (2503131)Instruction limit reached! % 221.90/31.56 % (2503131)------------------------------ % 221.90/31.56 % (2503131)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 221.90/31.56 % (2503131)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 221.90/31.56 % (2503131)CaDiCaL version: 2.1.3 % 221.90/31.56 % (2503131)Termination reason: Instruction limit % 221.90/31.56 % (2503131)Termination phase: Saturation % 221.90/31.56 % (2503131)Time elapsed: 0.737 s % 221.90/31.56 % (2503131)Peak memory usage: 23 MB % 221.90/31.56 % (2503131)Instructions burned: 2363 (million) % 221.90/31.56 % (2503137)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=729108513:i=1758:kws=inv_precedence:fsr=off:rtra=on_2746 on theBenchmark for (2746ds/1758Mi) % 221.90/31.56 % (2503137)Instruction limit reached! % 221.90/31.56 % (2503137)------------------------------ % 221.90/31.56 % (2503137)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 221.90/31.56 % (2503137)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 221.90/31.56 % (2503137)CaDiCaL version: 2.1.3 % 221.90/31.56 % (2503137)Termination reason: Instruction limit % 221.90/31.56 % (2503137)Termination phase: Saturation % 221.90/31.56 % (2503137)Time elapsed: 0.520 s % 221.90/31.56 % (2503137)Peak memory usage: 25 MB % 221.90/31.56 % (2503137)Instructions burned: 1759 (million) % 221.90/31.56 % (2503139)fmb+10_1_sil=64000:si=on:random_seed=3601790565:i=44122:nm=2:rtra=on:gsp=on_2741 on theBenchmark for (2741ds/44122Mi) % 221.90/31.56 % (2503139)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 221.90/31.56 % (2503139)Terminated due to inappropriate strategy. % 221.90/31.56 % (2503139)------------------------------ % 221.90/31.56 % (2503139)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 221.90/31.56 % (2503139)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 221.90/31.56 % (2503139)CaDiCaL version: 2.1.3 % 221.90/31.56 % (2503139)Termination reason: Inappropriate % 221.90/31.56 % (2503139)Time elapsed: 0.0000 s % 221.90/31.56 % (2503139)Peak memory usage: 10 MB % 221.90/31.56 % (2503139)Instructions burned: 1 (million) % 221.90/31.56 % (2503139)------------------------------ % 221.90/31.56 % (2503139)------------------------------ % 221.90/31.56 % (2503141)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=2590204630:i=19030:nm=5:rtra=on_2741 on theBenchmark for (2741ds/19030Mi) % 269.01/38.15 % (2503141)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 269.01/38.15 % (2503141)Terminated due to inappropriate strategy. % 269.01/38.15 % (2503141)------------------------------ % 269.01/38.15 % (2503141)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 269.01/38.15 % (2503141)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 269.01/38.15 % (2503141)CaDiCaL version: 2.1.3 % 269.01/38.15 % (2503141)Termination reason: Inappropriate % 269.01/38.15 % (2503141)Time elapsed: 0.0000 s % 269.01/38.15 % (2503141)Peak memory usage: 10 MB % 269.01/38.15 % (2503141)Instructions burned: 1 (million) % 269.01/38.15 % (2503141)------------------------------ % 269.01/38.15 % (2503141)------------------------------ % 269.01/38.15 % (2503143)fmb+10_1_sil=64000:sas=cadical:si=on:fmbss=8:random_seed=3657523217:fmbsr=1.7:i=1840:rtra=on_2741 on theBenchmark for (2741ds/1840Mi) % 269.01/38.15 % (2503143)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 269.01/38.15 % (2503143)Terminated due to inappropriate strategy. % 269.01/38.15 % (2503143)------------------------------ % 269.01/38.15 % (2503143)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 269.01/38.15 % (2503143)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 269.01/38.15 % (2503143)CaDiCaL version: 2.1.3 % 269.01/38.15 % (2503143)Termination reason: Inappropriate % 269.01/38.15 % (2503143)Time elapsed: 0.0000 s % 269.01/38.15 % (2503143)Peak memory usage: 10 MB % 269.01/38.15 % (2503143)Instructions burned: 1 (million) % 269.01/38.15 % (2503143)------------------------------ % 269.01/38.15 % (2503143)------------------------------ % 269.01/38.15 % (2503145)dis-4_1_sil=16000:drc=ordering:si=on:sp=const_frequency:sac=on:newcnf=on:random_seed=2413856266:i=10262:rtra=on_2741 on theBenchmark for (2741ds/10262Mi) % 269.01/38.15 % (2503135)Instruction limit reached! % 269.01/38.15 % (2503135)------------------------------ % 269.01/38.15 % (2503135)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 269.01/38.15 % (2503135)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 269.01/38.15 % (2503135)CaDiCaL version: 2.1.3 % 269.01/38.15 % (2503135)Termination reason: Instruction limit % 269.01/38.15 % (2503135)Termination phase: Saturation % 269.01/38.15 % (2503135)Time elapsed: 0.885 s % 269.01/38.15 % (2503135)Peak memory usage: 22 MB % 269.01/38.15 % (2503135)Instructions burned: 1385 (million) % 269.01/38.15 % (2503147)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:si=on:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2328606400:i=2944:ins=7:rtra=on:fdi=8:gsp=on_2740 on theBenchmark for (2740ds/2944Mi) % 269.01/38.15 % (2503147)Instruction limit reached! % 269.01/38.15 % (2503147)------------------------------ % 269.01/38.15 % (2503147)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 269.01/38.15 % (2503147)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 269.01/38.15 % (2503147)CaDiCaL version: 2.1.3 % 269.01/38.15 % (2503147)Termination reason: Instruction limit % 269.01/38.15 % (2503147)Termination phase: Saturation % 269.01/38.15 % (2503147)Time elapsed: 1.571 s % 269.01/38.15 % (2503147)Peak memory usage: 34 MB % 269.01/38.15 % (2503147)Instructions burned: 2944 (million) % 269.01/38.15 % (2503149)fmb+10_1_sil=16000:sas=cadical:si=on:bce=on:fmbss=77:random_seed=4051171062:i=12648:rtra=on_2724 on theBenchmark for (2724ds/12648Mi) % 269.01/38.15 % (2503149)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 269.01/38.15 % (2503149)Terminated due to inappropriate strategy. % 269.01/38.15 % (2503149)------------------------------ % 269.01/38.15 % (2503149)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 269.01/38.15 % (2503149)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 269.01/38.15 % (2503149)CaDiCaL version: 2.1.3 % 269.01/38.15 % (2503149)Termination reason: Inappropriate % 269.01/38.15 % (2503149)Time elapsed: 0.001 s % 269.01/38.15 % (2503149)Peak memory usage: 11 MB % 269.01/38.15 % (2503149)Instructions burned: 1 (million) % 269.01/38.15 % (2503149)------------------------------ % 269.01/38.15 % (2503149)------------------------------ % 269.01/38.15 % (2503151)fmb+10_1_fmbas=function:sil=32000:sas=cadical:si=on:fmbss=16:random_seed=2895461167:fmbsr=2.30978:i=4348:rtra=on_2724 on theBenchmark for (2724ds/4348Mi) % 269.01/38.15 % (2503151)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 269.01/38.15 % (2503151)Terminated due to inappropriate strategy. % 269.01/38.15 % (2503151)------------------------------ % 269.01/38.15 % (2503151)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.18/42.63 % (2503151)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.18/42.63 % (2503151)CaDiCaL version: 2.1.3 % 300.18/42.63 % (2503151)Termination reason: Inappropriate % 300.18/42.63 % (2503151)Time elapsed: 0.001 s % 300.18/42.63 % (2503151)Peak memory usage: 10 MB % 300.18/42.63 % (2503151)Instructions burned: 1 (million) % 300.18/42.63 % (2503151)------------------------------ % 300.18/42.63 % (2503151)------------------------------ % 300.18/42.63 % (2503153)ott-2_1_sil=16000:si=on:newcnf=on:random_seed=3812290920:avsq=on:i=1738:avsqr=1,16:kws=inv_arity_squared:rtra=on_2724 on theBenchmark for (2724ds/1738Mi) % 300.18/42.63 % (2503093)Instruction limit reached! % 300.18/42.63 % (2503093)------------------------------ % 300.18/42.63 % (2503093)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.18/42.63 % (2503093)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.18/42.63 % (2503093)CaDiCaL version: 2.1.3 % 300.18/42.63 % (2503093)Termination reason: Instruction limit % 300.18/42.63 % (2503093)Termination phase: Saturation % 300.18/42.63 % (2503093)Time elapsed: 11.710 s % 300.18/42.63 % (2503093)Peak memory usage: 25 MB % 300.18/42.63 % (2503093)Instructions burned: 28122 (million) % 300.18/42.63 % (2503155)ott+10_1_sil=32000:tgt=ground:si=on:random_seed=4061188021:i=10228:av=off:rtra=on_2713 on theBenchmark for (2713ds/10228Mi) % 300.18/42.63 % (2503153)Instruction limit reached! % 300.18/42.63 % (2503153)------------------------------ % 300.18/42.63 % (2503153)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.18/42.63 % (2503153)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.18/42.63 % (2503153)CaDiCaL version: 2.1.3 % 300.18/42.63 % (2503153)Termination reason: Instruction limit % 300.18/42.63 % (2503153)Termination phase: Saturation % 300.18/42.63 % (2503153)Time elapsed: 1.115 s % 300.18/42.63 % (2503153)Peak memory usage: 18 MB % 300.18/42.63 % (2503153)Instructions burned: 1739 (million) % 300.18/42.63 % (2503157)fmb+10_1_sil=64000:sas=cadical:si=on:bce=on:rp=on:random_seed=4071044259:i=108564:rtra=on_2712 on theBenchmark for (2712ds/108564Mi) % 300.18/42.63 % (2503157)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 300.18/42.63 % (2503157)Terminated due to inappropriate strategy. % 300.18/42.63 % (2503157)------------------------------ % 300.18/42.63 % (2503157)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.18/42.63 % (2503157)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.18/42.63 % (2503157)CaDiCaL version: 2.1.3 % 300.18/42.63 % (2503157)Termination reason: Inappropriate % 300.18/42.63 % (2503157)Time elapsed: 0.001 s % 300.18/42.63 % (2503157)Peak memory usage: 10 MB % 300.18/42.63 % (2503157)Instructions burned: 1 (million) % 300.18/42.63 % (2503157)------------------------------ % 300.18/42.63 % (2503157)------------------------------ % 300.18/42.63 % (2503159)dis-11_1_sil=16000:si=on:sp=reverse_frequency:alpa=true:random_seed=655973480:i=7024:aac=none:rtra=on_2712 on theBenchmark for (2712ds/7024Mi) % 300.18/42.63 % (2503145)Instruction limit reached! % 300.18/42.63 % (2503145)------------------------------ % 300.18/42.63 % (2503145)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.18/42.63 % (2503145)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.18/42.63 % (2503145)CaDiCaL version: 2.1.3 % 300.18/42.63 % (2503145)Termination reason: Instruction limit % 300.18/42.63 % (2503145)Termination phase: Saturation % 300.18/42.63 % (2503145)Time elapsed: 3.117 s % 300.18/42.63 % (2503145)Peak memory usage: 67 MB % 300.18/42.63 % (2503145)Instructions burned: 10265 (million) % 300.18/42.63 % (2503161)dis+21_1_sil=32000:sas=cadical:si=on:random_seed=629602838:i=7546:rtra=on:amm=off_2709 on theBenchmark for (2709ds/7546Mi) % 300.18/42.63 % (2503161)Instruction limit reached! % 300.18/42.63 % (2503161)------------------------------ % 300.18/42.63 % (2503161)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.18/42.63 % (2503161)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.18/42.63 % (2503161)CaDiCaL version: 2.1.3 % 300.18/42.63 % (2503161)Termination reason: Instruction limit % 300.18/42.63 % (2503161)Termination phase: Saturation % 300.18/42.63 % (2503161)Time elapsed: 2.276 s % 300.18/42.63 % (2503161)Peak memory usage: 48 MB % 300.18/42.63 % (2503161)Instructions burned: 7546 (million) % 300.18/42.63 % (2503163)ott+11_1_sil=16000:si=on:gs=on:random_seed=204436017:s2a=on:i=4502:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:rtra=on:fsd=on_2687 on theBenc % 300.18/42.63 Terminated % 300.18/42.63 % Vampire exiting % 300.18/42.63 Terminated %------------------------------------------------------------------------------