%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWW647_2 : TPTP v9.3.1. Released v6.1.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % Computer : n006.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.64s 42.64s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.04 % Problem : SWW647_2 : TPTP v9.3.1. Released v6.1.0. % 0.00/0.08 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.11/0.24 % Computer : n006.cluster.edu % 0.11/0.24 % Model : x86_64 x86_64 % 0.11/0.24 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.24 % Memory : 8046.5625MB % 0.11/0.24 % OS : Linux 6.8.0-71-generic % 0.11/0.24 % CPULimit : 300 % 0.11/0.24 % WCLimit : 300 % 0.11/0.24 % DateTime : Mon Sep 28 14:23:10 UTC 2026 % 0.11/0.25 % CPUTime : % 0.11/0.25 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.24/0.30 Running first-order model finding % 0.24/0.30 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 6.83/1.36 % (3999986)Will run a generic schedule for satisfiability detection. % 6.83/1.36 % (3999991)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1784051544_2999 on theBenchmark for (2999ds/0Mi) % 6.83/1.36 % (3999993)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1012412697:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 6.83/1.36 % (3999991)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 6.83/1.36 % (3999991)Terminated due to inappropriate strategy. % 6.83/1.36 % (3999991)------------------------------ % 6.83/1.36 % (3999991)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.83/1.36 % (3999991)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.83/1.36 % (3999991)CaDiCaL version: 2.1.3 % 6.83/1.36 % (3999991)Termination reason: Inappropriate % 6.83/1.36 % (3999991)Time elapsed: 0.004 s % 6.83/1.36 % (3999991)Peak memory usage: 11 MB % 6.83/1.36 % (3999991)Instructions burned: 8 (million) % 6.83/1.36 % (3999991)------------------------------ % 6.83/1.36 % (3999991)------------------------------ % 6.83/1.36 % (3999992)% WARNING: option uhcvi not known. % 6.83/1.36 % (3999997)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1033660995:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 6.83/1.36 % (3999992)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=4197691435:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 6.83/1.36 % (3999994)dis+10_1_sil=32000:sp=arity:random_seed=1842808104:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 6.83/1.36 % (3999995)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=365436831:i=116_2999 on theBenchmark for (2999ds/116Mi) % 6.83/1.36 % (3999996)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1498764673:i=131_2999 on theBenchmark for (2999ds/131Mi) % 6.83/1.36 % (4000000)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=330348273:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 6.83/1.36 % (4000000)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 6.83/1.36 % (4000000)Terminated due to inappropriate strategy. % 6.83/1.36 % (4000000)------------------------------ % 6.83/1.36 % (4000000)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.83/1.36 % (4000000)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.83/1.36 % (4000000)CaDiCaL version: 2.1.3 % 6.83/1.36 % (4000000)Termination reason: Inappropriate % 6.83/1.36 % (4000000)Time elapsed: 0.007 s % 6.83/1.36 % (4000000)Peak memory usage: 10 MB % 6.83/1.36 % (4000000)Instructions burned: 7 (million) % 6.83/1.36 % (4000000)------------------------------ % 6.83/1.36 % (4000000)------------------------------ % 6.83/1.36 % (4000007)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1885609320:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 6.83/1.36 % (3999994)Instruction limit reached! % 6.83/1.36 % (3999994)------------------------------ % 6.83/1.36 % (3999994)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.83/1.36 % (3999994)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.83/1.36 % (3999994)CaDiCaL version: 2.1.3 % 6.83/1.36 % (3999994)Termination reason: Instruction limit % 6.83/1.36 % (3999994)Termination phase: Saturation % 6.83/1.36 % (3999994)Time elapsed: 0.103 s % 6.83/1.36 % (3999994)Peak memory usage: 13 MB % 6.83/1.36 % (3999994)Instructions burned: 103 (million) % 6.83/1.36 % (3999995)Instruction limit reached! % 6.83/1.36 % (3999995)------------------------------ % 6.83/1.36 % (3999995)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.83/1.36 % (3999995)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.83/1.36 % (3999995)CaDiCaL version: 2.1.3 % 6.83/1.36 % (3999995)Termination reason: Instruction limit % 6.83/1.36 % (3999995)Termination phase: Saturation % 6.83/1.36 % (3999995)Time elapsed: 0.117 s % 6.83/1.36 % (3999995)Peak memory usage: 13 MB % 6.83/1.36 % (3999995)Instructions burned: 116 (million) % 6.83/1.36 % (3999996)Instruction limit reached! % 6.83/1.36 % (3999996)------------------------------ % 6.83/1.36 % (3999996)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.83/1.36 % (3999996)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.83/1.36 % (3999996)CaDiCaL version: 2.1.3 % 6.83/1.36 % (3999996)Termination reason: Instruction limit % 8.46/1.73 % (3999996)Termination phase: Saturation % 8.46/1.73 % (3999996)Time elapsed: 0.132 s % 8.46/1.73 % (3999996)Peak memory usage: 13 MB % 8.46/1.73 % (3999996)Instructions burned: 131 (million) % 8.46/1.73 % (4000009)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=3591793783:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi) % 8.46/1.73 % (3999997)Instruction limit reached! % 8.46/1.73 % (3999997)------------------------------ % 8.46/1.73 % (3999997)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.46/1.73 % (3999997)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.46/1.73 % (3999997)CaDiCaL version: 2.1.3 % 8.46/1.73 % (3999997)Termination reason: Instruction limit % 8.46/1.73 % (3999997)Termination phase: Saturation % 8.46/1.73 % (3999997)Time elapsed: 0.146 s % 8.46/1.73 % (3999997)Peak memory usage: 13 MB % 8.46/1.73 % (3999997)Instructions burned: 159 (million) % 8.46/1.73 % (4000010)ott-21_1_sil=16000:fs=off:random_seed=1648126883:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 8.46/1.73 % (4000013)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=4153587524:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 8.46/1.73 % (4000011)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3202135635:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 8.46/1.73 % (4000013)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 8.46/1.73 % (4000013)Terminated due to inappropriate strategy. % 8.46/1.73 % (4000013)------------------------------ % 8.46/1.73 % (4000013)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.46/1.73 % (4000013)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.46/1.73 % (4000013)CaDiCaL version: 2.1.3 % 8.46/1.73 % (4000013)Termination reason: Inappropriate % 8.46/1.73 % (4000013)Time elapsed: 0.004 s % 8.46/1.73 % (4000013)Peak memory usage: 10 MB % 8.46/1.73 % (4000013)Instructions burned: 7 (million) % 8.46/1.73 % (4000013)------------------------------ % 8.46/1.73 % (4000013)------------------------------ % 8.46/1.73 % (4000017)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3176599037:i=1179_2997 on theBenchmark for (2997ds/1179Mi) % 8.46/1.73 % (4000007)Instruction limit reached! % 8.46/1.73 % (4000007)------------------------------ % 8.46/1.73 % (4000007)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.46/1.73 % (4000007)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.46/1.73 % (4000007)CaDiCaL version: 2.1.3 % 8.46/1.73 % (4000007)Termination reason: Instruction limit % 8.46/1.73 % (4000007)Termination phase: Saturation % 8.46/1.73 % (4000007)Time elapsed: 0.145 s % 8.46/1.73 % (4000007)Peak memory usage: 13 MB % 8.46/1.73 % (4000007)Instructions burned: 131 (million) % 8.46/1.73 % (4000019)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2032431164:i=889:ins=1_2997 on theBenchmark for (2997ds/889Mi) % 8.46/1.73 % (4000019)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 8.46/1.73 % (4000019)Terminated due to inappropriate strategy. % 8.46/1.73 % (4000019)------------------------------ % 8.46/1.73 % (4000019)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.46/1.73 % (4000019)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.46/1.73 % (4000019)CaDiCaL version: 2.1.3 % 8.46/1.73 % (4000019)Termination reason: Inappropriate % 8.46/1.73 % (4000019)Time elapsed: 0.007 s % 8.46/1.73 % (4000019)Peak memory usage: 11 MB % 8.46/1.73 % (4000019)Instructions burned: 7 (million) % 8.46/1.73 % (4000019)------------------------------ % 8.46/1.73 % (4000019)------------------------------ % 8.46/1.73 % (4000021)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=2682321388: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.46/1.73 % (4000010)Instruction limit reached! % 8.46/1.73 % (4000010)------------------------------ % 8.46/1.73 % (4000010)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.46/1.73 % (4000010)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.46/1.73 % (4000010)CaDiCaL version: 2.1.3 % 8.46/1.73 % (4000010)Termination reason: Instruction limit % 8.46/1.73 % (4000010)Termination phase: Saturation % 39.17/5.86 % (4000010)Time elapsed: 0.170 s % 39.17/5.86 % (4000010)Peak memory usage: 13 MB % 39.17/5.86 % (4000010)Instructions burned: 180 (million) % 39.17/5.86 % (4000023)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3953172447:i=879:kws=inv_precedence:fsr=off_2996 on theBenchmark for (2996ds/879Mi) % 39.17/5.86 % (4000011)Instruction limit reached! % 39.17/5.86 % (4000011)------------------------------ % 39.17/5.86 % (4000011)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 39.17/5.86 % (4000011)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.17/5.86 % (4000011)CaDiCaL version: 2.1.3 % 39.17/5.86 % (4000011)Termination reason: Instruction limit % 39.17/5.86 % (4000011)Termination phase: Saturation % 39.17/5.86 % (4000011)Time elapsed: 0.455 s % 39.17/5.86 % (4000011)Peak memory usage: 13 MB % 39.17/5.86 % (4000011)Instructions burned: 477 (million) % 39.17/5.86 % (4000027)fmb+10_1_sil=64000:random_seed=594027764:i=22061:nm=2:gsp=on_2993 on theBenchmark for (2993ds/22061Mi) % 39.17/5.86 % (4000027)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 39.17/5.86 % (4000027)Terminated due to inappropriate strategy. % 39.17/5.86 % (4000027)------------------------------ % 39.17/5.86 % (4000027)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 39.17/5.86 % (4000027)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.17/5.86 % (4000027)CaDiCaL version: 2.1.3 % 39.17/5.86 % (4000027)Termination reason: Inappropriate % 39.17/5.86 % (4000027)Time elapsed: 0.008 s % 39.17/5.86 % (4000027)Peak memory usage: 10 MB % 39.17/5.86 % (4000027)Instructions burned: 8 (million) % 39.17/5.86 % (4000027)------------------------------ % 39.17/5.86 % (4000027)------------------------------ % 39.17/5.86 % (4000029)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2231645969:i=9515:nm=5_2992 on theBenchmark for (2992ds/9515Mi) % 39.17/5.86 % (4000029)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 39.17/5.86 % (4000029)Terminated due to inappropriate strategy. % 39.17/5.86 % (4000029)------------------------------ % 39.17/5.86 % (4000029)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 39.17/5.86 % (4000029)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.17/5.86 % (4000029)CaDiCaL version: 2.1.3 % 39.17/5.86 % (4000029)Termination reason: Inappropriate % 39.17/5.86 % (4000029)Time elapsed: 0.007 s % 39.17/5.86 % (4000029)Peak memory usage: 10 MB % 39.17/5.86 % (4000029)Instructions burned: 7 (million) % 39.17/5.86 % (4000029)------------------------------ % 39.17/5.86 % (4000029)------------------------------ % 39.17/5.86 % (4000031)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3404535255:fmbsr=1.7:i=920_2992 on theBenchmark for (2992ds/920Mi) % 39.17/5.86 % (4000031)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 39.17/5.86 % (4000031)Terminated due to inappropriate strategy. % 39.17/5.86 % (4000031)------------------------------ % 39.17/5.86 % (4000031)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 39.17/5.86 % (4000031)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.17/5.86 % (4000031)CaDiCaL version: 2.1.3 % 39.17/5.86 % (4000031)Termination reason: Inappropriate % 39.17/5.86 % (4000031)Time elapsed: 0.005 s % 39.17/5.86 % (4000031)Peak memory usage: 11 MB % 39.17/5.86 % (4000031)Instructions burned: 7 (million) % 39.17/5.86 % (4000031)------------------------------ % 39.17/5.86 % (4000031)------------------------------ % 39.17/5.86 % (4000033)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=3079209492:i=5131_2992 on theBenchmark for (2992ds/5131Mi) % 39.17/5.86 % (4000009)Instruction limit reached! % 39.17/5.86 % (4000009)------------------------------ % 39.17/5.86 % (4000009)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 39.17/5.86 % (4000009)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.17/5.86 % (4000009)CaDiCaL version: 2.1.3 % 39.17/5.86 % (4000009)Termination reason: Instruction limit % 39.17/5.86 % (4000009)Termination phase: Saturation % 39.17/5.86 % (4000009)Time elapsed: 0.648 s % 39.17/5.86 % (4000009)Peak memory usage: 17 MB % 39.17/5.86 % (4000009)Instructions burned: 684 (million) % 39.17/5.86 % (4000035)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=4267553799:i=1472:ins=7:fdi=8:gsp=on_2991 on theBenchmark for (2991ds/1472Mi) % 39.17/5.86 % (4000021)Instruction limit reached! % 39.17/5.86 % (4000021)------------------------------ % 62.21/9.07 % (4000021)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 62.21/9.07 % (4000021)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 62.21/9.07 % (4000021)CaDiCaL version: 2.1.3 % 62.21/9.07 % (4000021)Termination reason: Instruction limit % 62.21/9.07 % (4000021)Termination phase: Saturation % 62.21/9.07 % (4000021)Time elapsed: 0.731 s % 62.21/9.07 % (4000021)Peak memory usage: 18 MB % 62.21/9.07 % (4000021)Instructions burned: 693 (million) % 62.21/9.07 % (4000037)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=2254900889:i=6324_2989 on theBenchmark for (2989ds/6324Mi) % 62.21/9.07 % (4000037)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 62.21/9.07 % (4000037)Terminated due to inappropriate strategy. % 62.21/9.07 % (4000037)------------------------------ % 62.21/9.07 % (4000037)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 62.21/9.07 % (4000037)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 62.21/9.07 % (4000037)CaDiCaL version: 2.1.3 % 62.21/9.07 % (4000037)Termination reason: Inappropriate % 62.21/9.07 % (4000037)Time elapsed: 0.005 s % 62.21/9.07 % (4000037)Peak memory usage: 11 MB % 62.21/9.07 % (4000037)Instructions burned: 7 (million) % 62.21/9.07 % (4000037)------------------------------ % 62.21/9.07 % (4000037)------------------------------ % 62.21/9.07 % (4000039)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=4153646844:fmbsr=2.30978:i=2174_2989 on theBenchmark for (2989ds/2174Mi) % 62.21/9.07 % (4000039)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 62.21/9.07 % (4000039)Terminated due to inappropriate strategy. % 62.21/9.07 % (4000039)------------------------------ % 62.21/9.07 % (4000039)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 62.21/9.07 % (4000039)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 62.21/9.07 % (4000039)CaDiCaL version: 2.1.3 % 62.21/9.07 % (4000039)Termination reason: Inappropriate % 62.21/9.07 % (4000039)Time elapsed: 0.008 s % 62.21/9.07 % (4000039)Peak memory usage: 11 MB % 62.21/9.07 % (4000039)Instructions burned: 7 (million) % 62.21/9.07 % (4000039)------------------------------ % 62.21/9.07 % (4000039)------------------------------ % 62.21/9.07 % (4000041)ott-2_1_sil=16000:newcnf=on:random_seed=2456622536:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2988 on theBenchmark for (2988ds/869Mi) % 62.21/9.07 % (4000023)Instruction limit reached! % 62.21/9.07 % (4000023)------------------------------ % 62.21/9.07 % (4000023)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 62.21/9.07 % (4000023)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 62.21/9.07 % (4000023)CaDiCaL version: 2.1.3 % 62.21/9.07 % (4000023)Termination reason: Instruction limit % 62.21/9.07 % (4000023)Termination phase: Saturation % 62.21/9.07 % (4000023)Time elapsed: 0.855 s % 62.21/9.07 % (4000023)Peak memory usage: 19 MB % 62.21/9.07 % (4000023)Instructions burned: 879 (million) % 62.21/9.07 % (4000043)ott+10_1_sil=32000:tgt=ground:random_seed=3789165563:i=5114:av=off_2987 on theBenchmark for (2987ds/5114Mi) % 62.21/9.07 % (4000017)Instruction limit reached! % 62.21/9.07 % (4000017)------------------------------ % 62.21/9.07 % (4000017)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 62.21/9.07 % (4000017)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 62.21/9.07 % (4000017)CaDiCaL version: 2.1.3 % 62.21/9.07 % (4000017)Termination reason: Instruction limit % 62.21/9.07 % (4000017)Termination phase: Saturation % 62.21/9.07 % (4000017)Time elapsed: 1.141 s % 62.21/9.07 % (4000017)Peak memory usage: 21 MB % 62.21/9.07 % (4000017)Instructions burned: 1180 (million) % 62.21/9.07 % (4000045)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=986128141:i=54282_2986 on theBenchmark for (2986ds/54282Mi) % 62.21/9.07 % (4000045)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 62.21/9.07 % (4000045)Terminated due to inappropriate strategy. % 62.21/9.07 % (4000045)------------------------------ % 62.21/9.07 % (4000045)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 62.21/9.07 % (4000045)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 62.21/9.07 % (4000045)CaDiCaL version: 2.1.3 % 62.21/9.07 % (4000045)Termination reason: Inappropriate % 62.21/9.07 % (4000045)Time elapsed: 0.008 s % 62.21/9.07 % (4000045)Peak memory usage: 11 MB % 62.21/9.07 % (4000045)Instructions burned: 8 (million) % 152.86/21.87 % (4000045)------------------------------ % 152.86/21.87 % (4000045)------------------------------ % 152.86/21.87 % (4000047)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3846534346:i=3512:aac=none_2985 on theBenchmark for (2985ds/3512Mi) % 152.86/21.87 % (4000041)Instruction limit reached! % 152.86/21.87 % (4000041)------------------------------ % 152.86/21.87 % (4000041)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 152.86/21.87 % (4000041)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 152.86/21.87 % (4000041)CaDiCaL version: 2.1.3 % 152.86/21.87 % (4000041)Termination reason: Instruction limit % 152.86/21.87 % (4000041)Termination phase: Saturation % 152.86/21.87 % (4000041)Time elapsed: 0.872 s % 152.86/21.87 % (4000041)Peak memory usage: 18 MB % 152.86/21.87 % (4000041)Instructions burned: 869 (million) % 152.86/21.87 % (4000049)dis+21_1_sil=32000:sas=cadical:random_seed=2499955426:i=3773:amm=off_2979 on theBenchmark for (2979ds/3773Mi) % 152.86/21.87 % (4000035)Instruction limit reached! % 152.86/21.87 % (4000035)------------------------------ % 152.86/21.87 % (4000035)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 152.86/21.87 % (4000035)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 152.86/21.87 % (4000035)CaDiCaL version: 2.1.3 % 152.86/21.87 % (4000035)Termination reason: Instruction limit % 152.86/21.87 % (4000035)Termination phase: Saturation % 152.86/21.87 % (4000035)Time elapsed: 1.467 s % 152.86/21.87 % (4000035)Peak memory usage: 24 MB % 152.86/21.87 % (4000035)Instructions burned: 1472 (million) % 152.86/21.87 % (4000051)ott+11_1_sil=16000:gs=on:random_seed=2829767408:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2976 on theBenchmark for (2976ds/2251Mi) % 152.86/21.87 % (4000051)Instruction limit reached! % 152.86/21.87 % (4000051)------------------------------ % 152.86/21.87 % (4000051)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 152.86/21.87 % (4000051)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 152.86/21.87 % (4000051)CaDiCaL version: 2.1.3 % 152.86/21.87 % (4000051)Termination reason: Instruction limit % 152.86/21.87 % (4000051)Termination phase: Saturation % 152.86/21.87 % (4000051)Time elapsed: 2.037 s % 152.86/21.87 % (4000051)Peak memory usage: 18 MB % 152.86/21.87 % (4000051)Instructions burned: 2252 (million) % 152.86/21.87 % (4000057)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=3036964707:fmbsr=1.6:i=67534_2956 on theBenchmark for (2956ds/67534Mi) % 152.86/21.87 % (4000057)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 152.86/21.87 % (4000057)Terminated due to inappropriate strategy. % 152.86/21.87 % (4000057)------------------------------ % 152.86/21.87 % (4000057)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 152.86/21.87 % (4000057)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 152.86/21.87 % (4000057)CaDiCaL version: 2.1.3 % 152.86/21.87 % (4000057)Termination reason: Inappropriate % 152.86/21.87 % (4000057)Time elapsed: 0.005 s % 152.86/21.87 % (4000057)Peak memory usage: 11 MB % 152.86/21.87 % (4000057)Instructions burned: 7 (million) % 152.86/21.87 % (4000057)------------------------------ % 152.86/21.87 % (4000057)------------------------------ % 152.86/21.87 % (4000059)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=1273774024:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2955 on theBenchmark for (2955ds/4591Mi) % 152.86/21.87 % (4000047)Instruction limit reached! % 152.86/21.87 % (4000047)------------------------------ % 152.86/21.87 % (4000047)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 152.86/21.87 % (4000047)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 152.86/21.87 % (4000047)CaDiCaL version: 2.1.3 % 152.86/21.87 % (4000047)Termination reason: Instruction limit % 152.86/21.87 % (4000047)Termination phase: Saturation % 152.86/21.87 % (4000047)Time elapsed: 3.096 s % 152.86/21.87 % (4000047)Peak memory usage: 31 MB % 152.86/21.87 % (4000047)Instructions burned: 3512 (million) % 152.86/21.87 % (4000063)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=1712587172:i=29340_2954 on theBenchmark for (2954ds/29340Mi) % 152.86/21.87 % (4000033)Instruction limit reached! % 152.86/21.87 % (4000033)------------------------------ % 152.86/21.87 % (4000033)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 152.86/21.87 % (4000033)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 152.86/21.87 % (4000033)CaDiCaL version: 2.1.3 % 152.86/21.87 % (4000033)Termination reason: Instruction limit % 175.86/25.05 % (4000033)Termination phase: Saturation % 175.86/25.05 % (4000033)Time elapsed: 4.732 s % 175.86/25.05 % (4000033)Peak memory usage: 38 MB % 175.86/25.05 % (4000033)Instructions burned: 5132 (million) % 175.86/25.05 % (4000065)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=4083664884:i=5211_2944 on theBenchmark for (2944ds/5211Mi) % 175.86/25.05 % (4000049)Instruction limit reached! % 175.86/25.05 % (4000049)------------------------------ % 175.86/25.05 % (4000049)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 175.86/25.05 % (4000049)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 175.86/25.05 % (4000049)CaDiCaL version: 2.1.3 % 175.86/25.05 % (4000049)Termination reason: Instruction limit % 175.86/25.05 % (4000049)Termination phase: Saturation % 175.86/25.05 % (4000049)Time elapsed: 3.557 s % 175.86/25.05 % (4000049)Peak memory usage: 32 MB % 175.86/25.05 % (4000049)Instructions burned: 3774 (million) % 175.86/25.05 % (4000067)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=795903426:i=5497:nm=2_2943 on theBenchmark for (2943ds/5497Mi) % 175.86/25.05 % (4000067)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 175.86/25.05 % (4000067)Terminated due to inappropriate strategy. % 175.86/25.05 % (4000067)------------------------------ % 175.86/25.05 % (4000067)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 175.86/25.05 % (4000067)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 175.86/25.05 % (4000067)CaDiCaL version: 2.1.3 % 175.86/25.05 % (4000067)Termination reason: Inappropriate % 175.86/25.05 % (4000067)Time elapsed: 0.008 s % 175.86/25.05 % (4000067)Peak memory usage: 11 MB % 175.86/25.05 % (4000067)Instructions burned: 8 (million) % 175.86/25.05 % (4000067)------------------------------ % 175.86/25.05 % (4000067)------------------------------ % 175.86/25.05 % (4000069)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=2695906173:fmbsr=2:i=46332_2943 on theBenchmark for (2943ds/46332Mi) % 175.86/25.05 % (4000069)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 175.86/25.05 % (4000069)Terminated due to inappropriate strategy. % 175.86/25.05 % (4000069)------------------------------ % 175.86/25.05 % (4000069)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 175.86/25.05 % (4000069)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 175.86/25.05 % (4000069)CaDiCaL version: 2.1.3 % 175.86/25.05 % (4000069)Termination reason: Inappropriate % 175.86/25.05 % (4000069)Time elapsed: 0.009 s % 175.86/25.05 % (4000069)Peak memory usage: 10 MB % 175.86/25.05 % (4000069)Instructions burned: 7 (million) % 175.86/25.05 % (4000069)------------------------------ % 175.86/25.05 % (4000069)------------------------------ % 175.86/25.05 % (4000071)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=2821106992:i=14071_2942 on theBenchmark for (2942ds/14071Mi) % 175.86/25.05 % (4000071)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 175.86/25.05 % (4000071)Terminated due to inappropriate strategy. % 175.86/25.05 % (4000071)------------------------------ % 175.86/25.05 % (4000071)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 175.86/25.05 % (4000071)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 175.86/25.05 % (4000071)CaDiCaL version: 2.1.3 % 175.86/25.05 % (4000071)Termination reason: Inappropriate % 175.86/25.05 % (4000071)Time elapsed: 0.009 s % 175.86/25.05 % (4000071)Peak memory usage: 11 MB % 175.86/25.05 % (4000071)Instructions burned: 7 (million) % 175.86/25.05 % (4000071)------------------------------ % 175.86/25.05 % (4000071)------------------------------ % 175.86/25.05 % (4000073)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=816965822:i=22565:add=on:rawr=on_2942 on theBenchmark for (2942ds/22565Mi) % 175.86/25.05 % (4000043)Instruction limit reached! % 175.86/25.05 % (4000043)------------------------------ % 175.86/25.05 % (4000043)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 175.86/25.05 % (4000043)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 175.86/25.05 % (4000043)CaDiCaL version: 2.1.3 % 175.86/25.05 % (4000043)Termination reason: Instruction limit % 175.86/25.05 % (4000043)Termination phase: Saturation % 175.86/25.05 % (4000043)Time elapsed: 5.136 s % 175.86/25.05 % (4000043)Peak memory usage: 43 MB % 175.86/25.05 % (4000043)Instructions burned: 5115 (million) % 175.86/25.05 % (4000075)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=1165669934:i=8173:av=off_2935 on theBenchmark for (2935ds/8173Mi) % 175.86/25.05 % (4000059)Instruction limit reached! % 176.54/25.18 % (4000059)------------------------------ % 176.54/25.18 % (4000059)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 176.54/25.18 % (4000059)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 176.54/25.18 % (4000059)CaDiCaL version: 2.1.3 % 176.54/25.18 % (4000059)Termination reason: Instruction limit % 176.54/25.18 % (4000059)Termination phase: Saturation % 176.54/25.18 % (4000059)Time elapsed: 4.317 s % 176.54/25.18 % (4000059)Peak memory usage: 60 MB % 176.54/25.18 % (4000059)Instructions burned: 4591 (million) % 176.54/25.18 % (4000087)dis+10_16:1_sil=16000:random_seed=3007119424:i=9155:fsr=off_2912 on theBenchmark for (2912ds/9155Mi) % 176.54/25.18 % (4000065)Instruction limit reached! % 176.54/25.18 % (4000065)------------------------------ % 176.54/25.18 % (4000065)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 176.54/25.18 % (4000065)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 176.54/25.18 % (4000065)CaDiCaL version: 2.1.3 % 176.54/25.18 % (4000065)Termination reason: Instruction limit % 176.54/25.18 % (4000065)Termination phase: Saturation % 176.54/25.18 % (4000065)Time elapsed: 4.640 s % 176.54/25.18 % (4000065)Peak memory usage: 45 MB % 176.54/25.18 % (4000065)Instructions burned: 5211 (million) % 176.54/25.18 % (4000089)ott-3_8_sil=64000:random_seed=2017928254:i=20139:bs=on_2897 on theBenchmark for (2897ds/20139Mi) % 176.54/25.18 % (4000075)Instruction limit reached! % 176.54/25.18 % (4000075)------------------------------ % 176.54/25.18 % (4000075)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 176.54/25.18 % (4000075)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 176.54/25.18 % (4000075)CaDiCaL version: 2.1.3 % 176.54/25.18 % (4000075)Termination reason: Instruction limit % 176.54/25.18 % (4000075)Termination phase: Saturation % 176.54/25.18 % (4000075)Time elapsed: 7.613 s % 176.54/25.18 % (4000075)Peak memory usage: 59 MB % 176.54/25.18 % (4000075)Instructions burned: 8174 (million) % 176.54/25.18 % (4000249)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=2164494914:fmbsr=2:i=32576_2859 on theBenchmark for (2859ds/32576Mi) % 176.54/25.18 % (4000249)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 176.54/25.18 % (4000249)Terminated due to inappropriate strategy. % 176.54/25.18 % (4000249)------------------------------ % 176.54/25.18 % (4000249)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 176.54/25.18 % (4000249)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 176.54/25.18 % (4000249)CaDiCaL version: 2.1.3 % 176.54/25.18 % (4000249)Termination reason: Inappropriate % 176.54/25.18 % (4000249)Time elapsed: 0.004 s % 176.54/25.18 % (4000249)Peak memory usage: 11 MB % 176.54/25.18 % (4000249)Instructions burned: 8 (million) % 176.54/25.18 % (4000249)------------------------------ % 176.54/25.18 % (4000249)------------------------------ % 176.54/25.18 % (4000251)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=725574637:i=11404_2859 on theBenchmark for (2859ds/11404Mi) % 176.54/25.18 % (4000087)Instruction limit reached! % 176.54/25.18 % (4000087)------------------------------ % 176.54/25.18 % (4000087)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 176.54/25.18 % (4000087)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 176.54/25.18 % (4000087)CaDiCaL version: 2.1.3 % 176.54/25.18 % (4000087)Termination reason: Instruction limit % 176.54/25.18 % (4000087)Termination phase: Saturation % 176.54/25.18 % (4000087)Time elapsed: 6.795 s % 176.54/25.18 % (4000087)Peak memory usage: 54 MB % 176.54/25.18 % (4000087)Instructions burned: 9157 (million) % 176.54/25.18 % (4000253)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=1431460167:i=14134_2843 on theBenchmark for (2843ds/14134Mi) % 176.54/25.18 % (4000073)Instruction limit reached! % 176.54/25.18 % (4000073)------------------------------ % 176.54/25.18 % (4000073)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 176.54/25.18 % (4000073)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 176.54/25.18 % (4000073)CaDiCaL version: 2.1.3 % 176.54/25.18 % (4000073)Termination reason: Instruction limit % 176.54/25.18 % (4000073)Termination phase: Saturation % 176.54/25.18 % (4000073)Time elapsed: 13.200 s % 176.54/25.18 % (4000073)Peak memory usage: 53 MB % 176.54/25.18 % (4000073)Instructions burned: 22567 (million) % 176.54/25.18 % (4000255)dis+33_16_sil=32000:sac=on:random_seed=2777316184:i=15851:nm=0_2810 on theBenchmark for (2810ds/15851Mi) % 176.54/25.18 % (4000251)Instruction limit reached! % 176.54/25.18 % (4000251)------------------------------ % 176.54/25.18 % (4000251)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 210.37/30.03 % (4000251)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 210.37/30.03 % (4000251)CaDiCaL version: 2.1.3 % 210.37/30.03 % (4000251)Termination reason: Instruction limit % 210.37/30.03 % (4000251)Termination phase: Saturation % 210.37/30.03 % (4000251)Time elapsed: 7.459 s % 210.37/30.03 % (4000251)Peak memory usage: 94 MB % 210.37/30.03 % (4000251)Instructions burned: 11404 (million) % 210.37/30.03 % (4000257)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=3083899791:avsq=on:i=17627:add=on:amm=off_2784 on theBenchmark for (2784ds/17627Mi) % 210.37/30.03 % (4000063)Instruction limit reached! % 210.37/30.03 % (4000063)------------------------------ % 210.37/30.03 % (4000063)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 210.37/30.03 % (4000063)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 210.37/30.03 % (4000063)CaDiCaL version: 2.1.3 % 210.37/30.03 % (4000063)Termination reason: Instruction limit % 210.37/30.03 % (4000063)Termination phase: Saturation % 210.37/30.03 % (4000063)Time elapsed: 17.679 s % 210.37/30.03 % (4000063)Peak memory usage: 261 MB % 210.37/30.03 % (4000063)Instructions burned: 29341 (million) % 210.37/30.03 % (4000259)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=3923558580:s2a=on:i=53295_2776 on theBenchmark for (2776ds/53295Mi) % 210.37/30.03 % (4000253)Instruction limit reached! % 210.37/30.03 % (4000253)------------------------------ % 210.37/30.03 % (4000253)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 210.37/30.03 % (4000253)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 210.37/30.03 % (4000253)CaDiCaL version: 2.1.3 % 210.37/30.03 % (4000253)Termination reason: Instruction limit % 210.37/30.03 % (4000253)Termination phase: Saturation % 210.37/30.03 % (4000253)Time elapsed: 8.722 s % 210.37/30.03 % (4000253)Peak memory usage: 91 MB % 210.37/30.03 % (4000253)Instructions burned: 14134 (million) % 210.37/30.03 % (4000261)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=1465309736:i=26857:ins=20_2756 on theBenchmark for (2756ds/26857Mi) % 210.37/30.03 % (4000261)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 210.37/30.03 % (4000261)Terminated due to inappropriate strategy. % 210.37/30.03 % (4000261)------------------------------ % 210.37/30.03 % (4000261)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 210.37/30.03 % (4000261)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 210.37/30.03 % (4000261)CaDiCaL version: 2.1.3 % 210.37/30.03 % (4000261)Termination reason: Inappropriate % 210.37/30.03 % (4000261)Time elapsed: 0.004 s % 210.37/30.03 % (4000261)Peak memory usage: 10 MB % 210.37/30.03 % (4000261)Instructions burned: 7 (million) % 210.37/30.03 % (4000261)------------------------------ % 210.37/30.03 % (4000261)------------------------------ % 210.37/30.03 % (4000263)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=2318611253:i=28120:bs=on:fsr=off_2756 on theBenchmark for (2756ds/28120Mi) % 210.37/30.03 % (4000089)Instruction limit reached! % 210.37/30.03 % (4000089)------------------------------ % 210.37/30.03 % (4000089)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 210.37/30.03 % (4000089)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 210.37/30.03 % (4000089)CaDiCaL version: 2.1.3 % 210.37/30.03 % (4000089)Termination reason: Instruction limit % 210.37/30.03 % (4000089)Termination phase: Saturation % 210.37/30.03 % (4000089)Time elapsed: 14.423 s % 210.37/30.03 % (4000089)Peak memory usage: 112 MB % 210.37/30.03 % (4000089)Instructions burned: 20139 (million) % 210.37/30.03 % (4000265)fmb+10_1_sil=256000:fmbss=7:random_seed=307946118:fmbsr=1.6:i=182295_2752 on theBenchmark for (2752ds/182295Mi) % 210.37/30.03 % (4000265)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 210.37/30.03 % (4000265)Terminated due to inappropriate strategy. % 210.37/30.03 % (4000265)------------------------------ % 210.37/30.03 % (4000265)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 210.37/30.03 % (4000265)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 210.37/30.03 % (4000265)CaDiCaL version: 2.1.3 % 210.37/30.03 % (4000265)Termination reason: Inappropriate % 210.37/30.03 % (4000265)Time elapsed: 0.004 s % 210.37/30.03 % (4000265)Peak memory usage: 11 MB % 210.37/30.03 % (4000265)Instructions burned: 7 (million) % 210.37/30.03 % (4000265)------------------------------ % 210.37/30.03 % (4000265)------------------------------ % 210.37/30.03 % (4000267)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=214589796:i=44625:gsp=on_2752 on theBenchmark for (2752ds/44625Mi) % 225.60/32.10 % (4000267)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 225.60/32.10 % (4000267)Terminated due to inappropriate strategy. % 225.60/32.10 % (4000267)------------------------------ % 225.60/32.10 % (4000267)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 225.60/32.10 % (4000267)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 225.60/32.10 % (4000267)CaDiCaL version: 2.1.3 % 225.60/32.10 % (4000267)Termination reason: Inappropriate % 225.60/32.10 % (4000267)Time elapsed: 0.004 s % 225.60/32.10 % (4000267)Peak memory usage: 11 MB % 225.60/32.10 % (4000267)Instructions burned: 7 (million) % 225.60/32.10 % (4000267)------------------------------ % 225.60/32.10 % (4000267)------------------------------ % 225.60/32.10 % (4000269)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=207519465:i=160505_2752 on theBenchmark for (2752ds/160505Mi) % 225.60/32.10 % (4000269)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 225.60/32.10 % (4000269)Terminated due to inappropriate strategy. % 225.60/32.10 % (4000269)------------------------------ % 225.60/32.10 % (4000269)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 225.60/32.10 % (4000269)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 225.60/32.10 % (4000269)CaDiCaL version: 2.1.3 % 225.60/32.10 % (4000269)Termination reason: Inappropriate % 225.60/32.10 % (4000269)Time elapsed: 0.004 s % 225.60/32.10 % (4000269)Peak memory usage: 10 MB % 225.60/32.10 % (4000269)Instructions burned: 7 (million) % 225.60/32.10 % (4000269)------------------------------ % 225.60/32.10 % (4000269)------------------------------ % 225.60/32.10 % (4000271)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=4046681755:fmbsr=1.3:i=225729_2752 on theBenchmark for (2752ds/225729Mi) % 225.60/32.10 % (4000271)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 225.60/32.10 % (4000271)Terminated due to inappropriate strategy. % 225.60/32.10 % (4000271)------------------------------ % 225.60/32.10 % (4000271)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 225.60/32.10 % (4000271)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 225.60/32.10 % (4000271)CaDiCaL version: 2.1.3 % 225.60/32.10 % (4000271)Termination reason: Inappropriate % 225.60/32.10 % (4000271)Time elapsed: 0.004 s % 225.60/32.10 % (4000271)Peak memory usage: 10 MB % 225.60/32.10 % (4000271)Instructions burned: 7 (million) % 225.60/32.10 % (4000271)------------------------------ % 225.60/32.10 % (4000271)------------------------------ % 225.60/32.10 % (4000273)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=1689862496:fmbsr=2:i=185024:ins=7_2751 on theBenchmark for (2751ds/185024Mi) % 225.60/32.10 % (4000273)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 225.60/32.10 % (4000273)Terminated due to inappropriate strategy. % 225.60/32.10 % (4000273)------------------------------ % 225.60/32.10 % (4000273)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 225.60/32.10 % (4000273)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 225.60/32.10 % (4000273)CaDiCaL version: 2.1.3 % 225.60/32.10 % (4000273)Termination reason: Inappropriate % 225.60/32.10 % (4000273)Time elapsed: 0.004 s % 225.60/32.10 % (4000273)Peak memory usage: 11 MB % 225.60/32.10 % (4000273)Instructions burned: 7 (million) % 225.60/32.10 % (4000273)------------------------------ % 225.60/32.10 % (4000273)------------------------------ % 225.60/32.10 % (4000275)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=622594539:rtra=on_2751 on theBenchmark for (2751ds/0Mi) % 225.60/32.10 % (4000275)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 225.60/32.10 % (4000275)Terminated due to inappropriate strategy. % 225.60/32.10 % (4000275)------------------------------ % 225.60/32.10 % (4000275)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 225.60/32.10 % (4000275)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 225.60/32.10 % (4000275)CaDiCaL version: 2.1.3 % 225.60/32.10 % (4000275)Termination reason: Inappropriate % 225.60/32.10 % (4000275)Time elapsed: 0.005 s % 225.60/32.10 % (4000275)Peak memory usage: 11 MB % 225.60/32.10 % (4000275)Instructions burned: 8 (million) % 225.60/32.10 % (4000275)------------------------------ % 225.60/32.10 % (4000275)------------------------------ % 225.60/32.10 % (4000277)% WARNING: option uhcvi not known. % 225.60/32.10 % (4000277)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1398855204:i=271062:add=off:rtra=on:rawr=on_2751 on theBenchmark for (2751ds/271062Mi) % 247.57/35.20 % (4000255)Instruction limit reached! % 247.57/35.20 % (4000255)------------------------------ % 247.57/35.20 % (4000255)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 247.57/35.20 % (4000255)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 247.57/35.20 % (4000255)CaDiCaL version: 2.1.3 % 247.57/35.20 % (4000255)Termination reason: Instruction limit % 247.57/35.20 % (4000255)Termination phase: Saturation % 247.57/35.20 % (4000255)Time elapsed: 8.709 s % 247.57/35.20 % (4000255)Peak memory usage: 145 MB % 247.57/35.20 % (4000255)Instructions burned: 15851 (million) % 247.57/35.20 % (4000279)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2553716857:i=176048:add=on:rtra=on:rawr=on_2722 on theBenchmark for (2722ds/176048Mi) % 247.57/35.20 % (3999993)Instruction limit reached! % 247.57/35.20 % (3999993)------------------------------ % 247.57/35.20 % (3999993)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 247.57/35.20 % (3999993)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 247.57/35.20 % (3999993)CaDiCaL version: 2.1.3 % 247.57/35.20 % (3999993)Termination reason: Instruction limit % 247.57/35.20 % (3999993)Termination phase: Saturation % 247.57/35.20 % (3999993)Time elapsed: 29.263 s % 247.57/35.20 % (3999993)Peak memory usage: 240 MB % 247.57/35.20 % (3999993)Instructions burned: 88027 (million) % 247.57/35.20 % (4000413)dis+10_1_sil=32000:si=on:sp=arity:random_seed=885232321:i=206:fgj=on:rtra=on_2706 on theBenchmark for (2706ds/206Mi) % 247.57/35.20 % (4000413)Instruction limit reached! % 247.57/35.20 % (4000413)------------------------------ % 247.57/35.20 % (4000413)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 247.57/35.20 % (4000413)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 247.57/35.20 % (4000413)CaDiCaL version: 2.1.3 % 247.57/35.20 % (4000413)Termination reason: Instruction limit % 247.57/35.20 % (4000413)Termination phase: Saturation % 247.57/35.20 % (4000413)Time elapsed: 0.067 s % 247.57/35.20 % (4000413)Peak memory usage: 13 MB % 247.57/35.20 % (4000413)Instructions burned: 207 (million) % 247.57/35.20 % (4000415)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=238467326:i=232:rtra=on_2706 on theBenchmark for (2706ds/232Mi) % 247.57/35.20 % (4000415)Instruction limit reached! % 247.57/35.20 % (4000415)------------------------------ % 247.57/35.20 % (4000415)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 247.57/35.20 % (4000415)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 247.57/35.20 % (4000415)CaDiCaL version: 2.1.3 % 247.57/35.20 % (4000415)Termination reason: Instruction limit % 247.57/35.20 % (4000415)Termination phase: Saturation % 247.57/35.20 % (4000415)Time elapsed: 0.080 s % 247.57/35.20 % (4000415)Peak memory usage: 14 MB % 247.57/35.20 % (4000415)Instructions burned: 234 (million) % 247.57/35.20 % (4000417)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=3059416935:i=262:rtra=on_2705 on theBenchmark for (2705ds/262Mi) % 247.57/35.20 % (4000417)Instruction limit reached! % 247.57/35.20 % (4000417)------------------------------ % 247.57/35.20 % (4000417)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 247.57/35.20 % (4000417)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 247.57/35.20 % (4000417)CaDiCaL version: 2.1.3 % 247.57/35.20 % (4000417)Termination reason: Instruction limit % 247.57/35.20 % (4000417)Termination phase: Saturation % 247.57/35.20 % (4000417)Time elapsed: 0.090 s % 247.57/35.20 % (4000417)Peak memory usage: 15 MB % 247.57/35.20 % (4000417)Instructions burned: 263 (million) % 247.57/35.20 % (4000448)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=236377227:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2704 on theBenchmark for (2704ds/318Mi) % 247.57/35.20 % (4000448)Instruction limit reached! % 247.57/35.20 % (4000448)------------------------------ % 247.57/35.20 % (4000448)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 247.57/35.20 % (4000448)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 247.57/35.20 % (4000448)CaDiCaL version: 2.1.3 % 247.57/35.20 % (4000448)Termination reason: Instruction limit % 247.57/35.20 % (4000448)Termination phase: Saturation % 247.57/35.20 % (4000448)Time elapsed: 0.118 s % 247.57/35.20 % (4000448)Peak memory usage: 15 MB % 247.57/35.20 % (4000448)Instructions burned: 321 (million) % 247.57/35.20 % (4000500)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=825915847:i=1428:nm=2:rtra=on_2702 on theBenchmark for (2702ds/1428Mi) % 276.44/39.23 % (4000500)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 276.44/39.23 % (4000500)Terminated due to inappropriate strategy. % 276.44/39.23 % (4000500)------------------------------ % 276.44/39.23 % (4000500)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 276.44/39.23 % (4000500)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 276.44/39.23 % (4000500)CaDiCaL version: 2.1.3 % 276.44/39.23 % (4000500)Termination reason: Inappropriate % 276.44/39.23 % (4000500)Time elapsed: 0.002 s % 276.44/39.23 % (4000500)Peak memory usage: 10 MB % 276.44/39.23 % (4000500)Instructions burned: 8 (million) % 276.44/39.23 % (4000500)------------------------------ % 276.44/39.23 % (4000500)------------------------------ % 276.44/39.23 % (4000506)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=3692047452:i=262:bd=preordered:rtra=on:fsd=on_2702 on theBenchmark for (2702ds/262Mi) % 276.44/39.23 % (4000506)Instruction limit reached! % 276.44/39.23 % (4000506)------------------------------ % 276.44/39.23 % (4000506)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 276.44/39.23 % (4000506)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 276.44/39.23 % (4000506)CaDiCaL version: 2.1.3 % 276.44/39.23 % (4000506)Termination reason: Instruction limit % 276.44/39.23 % (4000506)Termination phase: Saturation % 276.44/39.23 % (4000506)Time elapsed: 0.098 s % 276.44/39.23 % (4000506)Peak memory usage: 14 MB % 276.44/39.23 % (4000506)Instructions burned: 264 (million) % 276.44/39.23 % (4000528)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=1524575863:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2701 on theBenchmark for (2701ds/1368Mi) % 276.44/39.23 % (4000528)Instruction limit reached! % 276.44/39.23 % (4000528)------------------------------ % 276.44/39.23 % (4000528)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 276.44/39.23 % (4000528)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 276.44/39.23 % (4000528)CaDiCaL version: 2.1.3 % 276.44/39.23 % (4000528)Termination reason: Instruction limit % 276.44/39.23 % (4000528)Termination phase: Saturation % 276.44/39.23 % (4000528)Time elapsed: 0.604 s % 276.44/39.23 % (4000528)Peak memory usage: 21 MB % 276.44/39.23 % (4000528)Instructions burned: 1370 (million) % 276.44/39.23 % (4000591)ott-21_1_sil=16000:si=on:fs=off:random_seed=953553001:i=360:av=off:fsr=off:rtra=on_2695 on theBenchmark for (2695ds/360Mi) % 276.44/39.23 % (4000591)Instruction limit reached! % 276.44/39.23 % (4000591)------------------------------ % 276.44/39.23 % (4000591)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 276.44/39.23 % (4000591)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 276.44/39.23 % (4000591)CaDiCaL version: 2.1.3 % 276.44/39.23 % (4000591)Termination reason: Instruction limit % 276.44/39.23 % (4000591)Termination phase: Saturation % 276.44/39.23 % (4000591)Time elapsed: 0.178 s % 276.44/39.23 % (4000591)Peak memory usage: 14 MB % 276.44/39.23 % (4000591)Instructions burned: 362 (million) % 276.44/39.23 % (4000600)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1077985226:i=954:bd=all:rtra=on_2693 on theBenchmark for (2693ds/954Mi) % 276.44/39.23 % (4000600)Instruction limit reached! % 276.44/39.23 % (4000600)------------------------------ % 276.44/39.23 % (4000600)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 276.44/39.23 % (4000600)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 276.44/39.23 % (4000600)CaDiCaL version: 2.1.3 % 276.44/39.23 % (4000600)Termination reason: Instruction limit % 276.44/39.23 % (4000600)Termination phase: Saturation % 276.44/39.23 % (4000600)Time elapsed: 1.056 s % 276.44/39.23 % (4000600)Peak memory usage: 16 MB % 276.44/39.23 % (4000600)Instructions burned: 954 (million) % 276.44/39.23 % (4000617)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=1237706166:fmbsr=1.3:i=1730:ins=25:rtra=on_2682 on theBenchmark for (2682ds/1730Mi) % 276.44/39.23 % (4000617)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 276.44/39.23 % (4000617)Terminated due to inappropriate strategy. % 276.44/39.23 % (4000617)------------------------------ % 276.44/39.23 % (4000617)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 276.44/39.23 % (4000617)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 276.44/39.23 % (4000617)CaDiCaL version: 2.1.3 % 276.44/39.23 % (4000617)Termination reason: Inappropriate % 276.44/39.23 % (Terminated % 300.64/42.64 % Vampire exiting % 300.64/42.64 Terminated %------------------------------------------------------------------------------