%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWW067_1 : TPTP v9.3.1. Released v5.0.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % Computer : n011.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:39:03 PM UTC 2026 % Result : Timeout 300.68s 42.64s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWW067_1 : TPTP v9.3.1. Released v5.0.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.07/0.17 % Computer : n011.cluster.edu % 0.07/0.17 % Model : x86_64 x86_64 % 0.07/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.07/0.17 % Memory : 8046.5625MB % 0.07/0.17 % OS : Linux 6.8.0-71-generic % 0.07/0.17 % CPULimit : 300 % 0.07/0.17 % WCLimit : 300 % 0.07/0.17 % DateTime : Mon Sep 28 13:11:00 UTC 2026 % 0.07/0.17 % CPUTime : % 0.07/0.17 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.07/0.20 Running first-order model finding % 0.07/0.20 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 3.22/0.73 % (3375219)Will run a generic schedule for satisfiability detection. % 3.22/0.73 % (3375229)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=258416107:i=131_2999 on theBenchmark for (2999ds/131Mi) % 3.22/0.73 % (3375225)% WARNING: option uhcvi not known. % 3.22/0.73 % (3375224)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=290240009_2999 on theBenchmark for (2999ds/0Mi) % 3.22/0.73 % (3375225)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1086494089:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 3.22/0.73 % (3375226)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=4125405611:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 3.22/0.73 % (3375227)dis+10_1_sil=32000:sp=arity:random_seed=3802912929:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 3.22/0.73 % (3375228)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=660415718:i=116_2999 on theBenchmark for (2999ds/116Mi) % 3.22/0.73 % (3375230)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3000152489:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 3.22/0.73 % (3375229)Instruction limit reached! % 3.22/0.73 % (3375229)------------------------------ % 3.22/0.73 % (3375229)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.22/0.73 % (3375229)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.22/0.73 % (3375229)CaDiCaL version: 2.1.3 % 3.22/0.73 % (3375229)Termination reason: Instruction limit % 3.22/0.73 % (3375229)Termination phase: Saturation % 3.22/0.73 % (3375229)Time elapsed: 0.030 s % 3.22/0.73 % (3375229)Peak memory usage: 15 MB % 3.22/0.73 % (3375229)Instructions burned: 137 (million) % 3.22/0.73 % (3375224)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.22/0.73 % (3375224)Terminated due to inappropriate strategy. % 3.22/0.73 % (3375224)------------------------------ % 3.22/0.73 % (3375224)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.22/0.73 % (3375224)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.22/0.73 % (3375224)CaDiCaL version: 2.1.3 % 3.22/0.73 % (3375224)Termination reason: Inappropriate % 3.22/0.73 % (3375224)Time elapsed: 0.041 s % 3.22/0.73 % (3375224)Peak memory usage: 14 MB % 3.22/0.73 % (3375224)Instructions burned: 93 (million) % 3.22/0.73 % (3375224)------------------------------ % 3.22/0.73 % (3375224)------------------------------ % 3.22/0.73 % (3375238)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=611753399:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 3.22/0.73 % (3375227)Instruction limit reached! % 3.22/0.73 % (3375227)------------------------------ % 3.22/0.73 % (3375227)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.22/0.73 % (3375227)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.22/0.73 % (3375227)CaDiCaL version: 2.1.3 % 3.22/0.73 % (3375227)Termination reason: Instruction limit % 3.22/0.73 % (3375227)Termination phase: Saturation % 3.22/0.73 % (3375227)Time elapsed: 0.047 s % 3.22/0.73 % (3375227)Peak memory usage: 15 MB % 3.22/0.73 % (3375227)Instructions burned: 105 (million) % 3.22/0.73 % (3375228)Instruction limit reached! % 3.22/0.73 % (3375228)------------------------------ % 3.22/0.73 % (3375228)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.22/0.73 % (3375228)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.22/0.73 % (3375228)CaDiCaL version: 2.1.3 % 3.22/0.73 % (3375228)Termination reason: Instruction limit % 3.22/0.73 % (3375228)Termination phase: Saturation % 3.22/0.73 % (3375228)Time elapsed: 0.055 s % 3.22/0.73 % (3375228)Peak memory usage: 16 MB % 3.22/0.73 % (3375228)Instructions burned: 117 (million) % 3.22/0.73 % (3375239)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2094886412:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi) % 3.22/0.73 % (3375230)Instruction limit reached! % 3.22/0.73 % (3375230)------------------------------ % 3.22/0.73 % (3375230)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.22/0.73 % (3375230)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.22/0.73 % (3375241)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=334285506:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi) % 4.25/1.03 % (3375230)CaDiCaL version: 2.1.3 % 4.25/1.03 % (3375230)Termination reason: Instruction limit % 4.25/1.03 % (3375230)Termination phase: Saturation % 4.25/1.03 % (3375230)Time elapsed: 0.066 s % 4.25/1.03 % (3375230)Peak memory usage: 16 MB % 4.25/1.03 % (3375230)Instructions burned: 161 (million) % 4.25/1.03 % (3375238)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 4.25/1.03 % (3375238)Terminated due to inappropriate strategy. % 4.25/1.03 % (3375238)------------------------------ % 4.25/1.03 % (3375238)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 4.25/1.03 % (3375238)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.25/1.03 % (3375238)CaDiCaL version: 2.1.3 % 4.25/1.03 % (3375238)Termination reason: Inappropriate % 4.25/1.03 % (3375238)Time elapsed: 0.027 s % 4.25/1.03 % (3375238)Peak memory usage: 14 MB % 4.25/1.03 % (3375238)Instructions burned: 92 (million) % 4.25/1.03 % (3375238)------------------------------ % 4.25/1.03 % (3375238)------------------------------ % 4.25/1.03 % (3375242)ott-21_1_sil=16000:fs=off:random_seed=251465336:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 4.25/1.03 % (3375246)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=825090642:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 4.25/1.03 % (3375245)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3565284624:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 4.25/1.03 % (3375246)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 4.25/1.03 % (3375246)Terminated due to inappropriate strategy. % 4.25/1.03 % (3375246)------------------------------ % 4.25/1.03 % (3375246)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 4.25/1.03 % (3375246)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.25/1.03 % (3375246)CaDiCaL version: 2.1.3 % 4.25/1.03 % (3375246)Termination reason: Inappropriate % 4.25/1.03 % (3375246)Time elapsed: 0.022 s % 4.25/1.03 % (3375246)Peak memory usage: 14 MB % 4.25/1.03 % (3375246)Instructions burned: 91 (million) % 4.25/1.03 % (3375246)------------------------------ % 4.25/1.03 % (3375246)------------------------------ % 4.25/1.03 % (3375239)Instruction limit reached! % 4.25/1.03 % (3375239)------------------------------ % 4.25/1.03 % (3375239)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 4.25/1.03 % (3375239)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.25/1.03 % (3375239)CaDiCaL version: 2.1.3 % 4.25/1.03 % (3375239)Termination reason: Instruction limit % 4.25/1.03 % (3375239)Termination phase: Saturation % 4.25/1.03 % (3375239)Time elapsed: 0.056 s % 4.25/1.03 % (3375239)Peak memory usage: 15 MB % 4.25/1.03 % (3375239)Instructions burned: 131 (million) % 4.25/1.03 % (3375250)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1962738654:i=1179_2998 on theBenchmark for (2998ds/1179Mi) % 4.25/1.03 % (3375251)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2872587455:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi) % 4.25/1.03 % (3375242)Instruction limit reached! % 4.25/1.03 % (3375242)------------------------------ % 4.25/1.03 % (3375242)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 4.25/1.03 % (3375242)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.25/1.03 % (3375242)CaDiCaL version: 2.1.3 % 4.25/1.03 % (3375242)Termination reason: Instruction limit % 4.25/1.03 % (3375242)Termination phase: Saturation % 4.25/1.03 % (3375242)Time elapsed: 0.083 s % 4.25/1.03 % (3375242)Peak memory usage: 16 MB % 4.25/1.03 % (3375242)Instructions burned: 180 (million) % 4.25/1.03 % (3375254)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=856697599: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) % 4.25/1.03 % (3375251)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 4.25/1.03 % (3375251)Terminated due to inappropriate strategy. % 4.25/1.03 % (3375251)------------------------------ % 4.25/1.03 % (3375251)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 4.25/1.03 % (3375251)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.25/1.03 % (3375251)CaDiCaL version: 2.1.3 % 4.25/1.03 % (3375251)Termination reason: Inappropriate % 4.25/1.03 % (3375251)Time elapsed: 0.056 s % 4.25/1.03 % (3375251)Peak memory usage: 16 MB % 16.94/2.83 % (3375251)Instructions burned: 127 (million) % 16.94/2.83 % (3375251)------------------------------ % 16.94/2.83 % (3375251)------------------------------ % 16.94/2.83 % (3375256)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3131555979:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi) % 16.94/2.83 % (3375245)Instruction limit reached! % 16.94/2.83 % (3375245)------------------------------ % 16.94/2.83 % (3375245)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 16.94/2.83 % (3375245)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.94/2.83 % (3375245)CaDiCaL version: 2.1.3 % 16.94/2.83 % (3375245)Termination reason: Instruction limit % 16.94/2.83 % (3375245)Termination phase: Saturation % 16.94/2.83 % (3375245)Time elapsed: 0.238 s % 16.94/2.83 % (3375245)Peak memory usage: 17 MB % 16.94/2.83 % (3375245)Instructions burned: 477 (million) % 16.94/2.83 % (3375258)fmb+10_1_sil=64000:random_seed=1631435534:i=22061:nm=2:gsp=on_2996 on theBenchmark for (2996ds/22061Mi) % 16.94/2.83 % (3375258)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 16.94/2.83 % (3375258)Terminated due to inappropriate strategy. % 16.94/2.83 % (3375258)------------------------------ % 16.94/2.83 % (3375258)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 16.94/2.83 % (3375258)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.94/2.83 % (3375258)CaDiCaL version: 2.1.3 % 16.94/2.83 % (3375258)Termination reason: Inappropriate % 16.94/2.83 % (3375258)Time elapsed: 0.044 s % 16.94/2.83 % (3375258)Peak memory usage: 14 MB % 16.94/2.83 % (3375258)Instructions burned: 101 (million) % 16.94/2.83 % (3375258)------------------------------ % 16.94/2.83 % (3375258)------------------------------ % 16.94/2.83 % (3375241)Instruction limit reached! % 16.94/2.83 % (3375241)------------------------------ % 16.94/2.83 % (3375241)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 16.94/2.83 % (3375241)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.94/2.83 % (3375241)CaDiCaL version: 2.1.3 % 16.94/2.83 % (3375241)Termination reason: Instruction limit % 16.94/2.83 % (3375241)Termination phase: Saturation % 16.94/2.83 % (3375241)Time elapsed: 0.332 s % 16.94/2.83 % (3375241)Peak memory usage: 20 MB % 16.94/2.83 % (3375241)Instructions burned: 686 (million) % 16.94/2.83 % (3375260)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=664307578:i=9515:nm=5_2995 on theBenchmark for (2995ds/9515Mi) % 16.94/2.83 % (3375261)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=4011665741:fmbsr=1.7:i=920_2995 on theBenchmark for (2995ds/920Mi) % 16.94/2.83 % (3375250)Instruction limit reached! % 16.94/2.83 % (3375250)------------------------------ % 16.94/2.83 % (3375250)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 16.94/2.83 % (3375250)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.94/2.83 % (3375250)CaDiCaL version: 2.1.3 % 16.94/2.83 % (3375250)Termination reason: Instruction limit % 16.94/2.83 % (3375250)Termination phase: Saturation % 16.94/2.83 % (3375250)Time elapsed: 0.298 s % 16.94/2.83 % (3375250)Peak memory usage: 20 MB % 16.94/2.83 % (3375250)Instructions burned: 1183 (million) % 16.94/2.83 % (3375264)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2570028692:i=5131_2995 on theBenchmark for (2995ds/5131Mi) % 16.94/2.83 % (3375260)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 16.94/2.83 % (3375260)Terminated due to inappropriate strategy. % 16.94/2.83 % (3375260)------------------------------ % 16.94/2.83 % (3375260)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 16.94/2.83 % (3375260)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.94/2.83 % (3375260)CaDiCaL version: 2.1.3 % 16.94/2.83 % (3375260)Termination reason: Inappropriate % 16.94/2.83 % (3375260)Time elapsed: 0.039 s % 16.94/2.83 % (3375260)Peak memory usage: 14 MB % 16.94/2.83 % (3375260)Instructions burned: 92 (million) % 16.94/2.83 % (3375260)------------------------------ % 16.94/2.83 % (3375260)------------------------------ % 16.94/2.83 % (3375261)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 16.94/2.83 % (3375261)Terminated due to inappropriate strategy. % 16.94/2.83 % (3375261)------------------------------ % 16.94/2.83 % (3375261)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 16.94/2.83 % (3375261)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.16/3.86 % (3375261)CaDiCaL version: 2.1.3 % 24.16/3.86 % (3375261)Termination reason: Inappropriate % 24.16/3.86 % (3375261)Time elapsed: 0.040 s % 24.16/3.86 % (3375261)Peak memory usage: 14 MB % 24.16/3.86 % (3375261)Instructions burned: 92 (million) % 24.16/3.86 % (3375261)------------------------------ % 24.16/3.86 % (3375261)------------------------------ % 24.16/3.86 % (3375266)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=465342715:i=1472:ins=7:fdi=8:gsp=on_2994 on theBenchmark for (2994ds/1472Mi) % 24.16/3.86 % (3375267)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=1515323010:i=6324_2994 on theBenchmark for (2994ds/6324Mi) % 24.16/3.86 % (3375267)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 24.16/3.86 % (3375267)Terminated due to inappropriate strategy. % 24.16/3.86 % (3375267)------------------------------ % 24.16/3.86 % (3375267)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 24.16/3.86 % (3375267)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.16/3.86 % (3375267)CaDiCaL version: 2.1.3 % 24.16/3.86 % (3375267)Termination reason: Inappropriate % 24.16/3.86 % (3375267)Time elapsed: 0.040 s % 24.16/3.86 % (3375267)Peak memory usage: 14 MB % 24.16/3.86 % (3375267)Instructions burned: 92 (million) % 24.16/3.86 % (3375267)------------------------------ % 24.16/3.86 % (3375267)------------------------------ % 24.16/3.86 % (3375270)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1753528034:fmbsr=2.30978:i=2174_2994 on theBenchmark for (2994ds/2174Mi) % 24.16/3.86 % (3375254)Instruction limit reached! % 24.16/3.86 % (3375254)------------------------------ % 24.16/3.86 % (3375254)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 24.16/3.86 % (3375254)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.16/3.86 % (3375254)CaDiCaL version: 2.1.3 % 24.16/3.86 % (3375254)Termination reason: Instruction limit % 24.16/3.86 % (3375254)Termination phase: Saturation % 24.16/3.86 % (3375254)Time elapsed: 0.385 s % 24.16/3.86 % (3375254)Peak memory usage: 22 MB % 24.16/3.86 % (3375254)Instructions burned: 692 (million) % 24.16/3.86 % (3375270)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 24.16/3.86 % (3375270)Terminated due to inappropriate strategy. % 24.16/3.86 % (3375270)------------------------------ % 24.16/3.86 % (3375270)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 24.16/3.86 % (3375270)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.16/3.86 % (3375270)CaDiCaL version: 2.1.3 % 24.16/3.86 % (3375270)Termination reason: Inappropriate % 24.16/3.86 % (3375270)Time elapsed: 0.040 s % 24.16/3.86 % (3375270)Peak memory usage: 14 MB % 24.16/3.86 % (3375270)Instructions burned: 92 (million) % 24.16/3.86 % (3375270)------------------------------ % 24.16/3.86 % (3375270)------------------------------ % 24.16/3.86 % (3375272)ott-2_1_sil=16000:newcnf=on:random_seed=2955422636:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2993 on theBenchmark for (2993ds/869Mi) % 24.16/3.86 % (3375273)ott+10_1_sil=32000:tgt=ground:random_seed=1933829506:i=5114:av=off_2993 on theBenchmark for (2993ds/5114Mi) % 24.16/3.86 % (3375256)Instruction limit reached! % 24.16/3.86 % (3375256)------------------------------ % 24.16/3.86 % (3375256)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 24.16/3.86 % (3375256)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.16/3.86 % (3375256)CaDiCaL version: 2.1.3 % 24.16/3.86 % (3375256)Termination reason: Instruction limit % 24.16/3.86 % (3375256)Termination phase: Saturation % 24.16/3.86 % (3375256)Time elapsed: 0.473 s % 24.16/3.86 % (3375256)Peak memory usage: 21 MB % 24.16/3.86 % (3375256)Instructions burned: 879 (million) % 24.16/3.86 % (3375276)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2276647418:i=54282_2992 on theBenchmark for (2992ds/54282Mi) % 24.16/3.86 % (3375276)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 24.16/3.86 % (3375276)Terminated due to inappropriate strategy. % 24.16/3.86 % (3375276)------------------------------ % 24.16/3.86 % (3375276)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 24.16/3.86 % (3375276)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.16/3.86 % (3375276)CaDiCaL version: 2.1.3 % 24.16/3.86 % (3375276)Termination reason: Inappropriate % 24.16/3.86 % (3375276)Time elapsed: 0.040 s % 24.16/3.86 % (3375276)Peak memory usage: 14 MB % 24.16/3.86 % (3375276)Instructions burned: 92 (million) % 90.80/13.04 % (3375276)------------------------------ % 90.80/13.04 % (3375276)------------------------------ % 90.80/13.04 % (3375278)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=788295404:i=3512:aac=none_2991 on theBenchmark for (2991ds/3512Mi) % 90.80/13.04 % (3375266)Instruction limit reached! % 90.80/13.04 % (3375266)------------------------------ % 90.80/13.04 % (3375266)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 90.80/13.04 % (3375266)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 90.80/13.04 % (3375266)CaDiCaL version: 2.1.3 % 90.80/13.04 % (3375266)Termination reason: Instruction limit % 90.80/13.04 % (3375266)Termination phase: Saturation % 90.80/13.04 % (3375266)Time elapsed: 0.515 s % 90.80/13.04 % (3375266)Peak memory usage: 17 MB % 90.80/13.04 % (3375266)Instructions burned: 1472 (million) % 90.80/13.04 % (3375272)Instruction limit reached! % 90.80/13.04 % (3375272)------------------------------ % 90.80/13.04 % (3375272)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 90.80/13.04 % (3375272)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 90.80/13.04 % (3375272)CaDiCaL version: 2.1.3 % 90.80/13.04 % (3375272)Termination reason: Instruction limit % 90.80/13.04 % (3375272)Termination phase: Saturation % 90.80/13.04 % (3375272)Time elapsed: 0.418 s % 90.80/13.04 % (3375272)Peak memory usage: 20 MB % 90.80/13.04 % (3375272)Instructions burned: 871 (million) % 90.80/13.04 % (3375281)dis+21_1_sil=32000:sas=cadical:random_seed=2531614662:i=3773:amm=off_2989 on theBenchmark for (2989ds/3773Mi) % 90.80/13.04 % (3375282)ott+11_1_sil=16000:gs=on:random_seed=1598116293:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2989 on theBenchmark for (2989ds/2251Mi) % 90.80/13.04 % (3375282)Instruction limit reached! % 90.80/13.04 % (3375282)------------------------------ % 90.80/13.04 % (3375282)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 90.80/13.04 % (3375282)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 90.80/13.04 % (3375282)CaDiCaL version: 2.1.3 % 90.80/13.04 % (3375282)Termination reason: Instruction limit % 90.80/13.04 % (3375282)Termination phase: Saturation % 90.80/13.04 % (3375282)Time elapsed: 0.825 s % 90.80/13.04 % (3375282)Peak memory usage: 19 MB % 90.80/13.04 % (3375282)Instructions burned: 2254 (million) % 90.80/13.04 % (3375264)Instruction limit reached! % 90.80/13.04 % (3375264)------------------------------ % 90.80/13.04 % (3375264)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 90.80/13.04 % (3375264)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 90.80/13.04 % (3375264)CaDiCaL version: 2.1.3 % 90.80/13.04 % (3375264)Termination reason: Instruction limit % 90.80/13.04 % (3375264)Termination phase: Saturation % 90.80/13.04 % (3375264)Time elapsed: 1.435 s % 90.80/13.04 % (3375264)Peak memory usage: 43 MB % 90.80/13.04 % (3375264)Instructions burned: 5135 (million) % 90.80/13.04 % (3375285)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=2315849745:fmbsr=1.6:i=67534_2980 on theBenchmark for (2980ds/67534Mi) % 90.80/13.04 % (3375287)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=3743240641:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2980 on theBenchmark for (2980ds/4591Mi) % 90.80/13.04 % (3375285)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 90.80/13.04 % (3375285)Terminated due to inappropriate strategy. % 90.80/13.04 % (3375285)------------------------------ % 90.80/13.04 % (3375285)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 90.80/13.04 % (3375285)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 90.80/13.04 % (3375285)CaDiCaL version: 2.1.3 % 90.80/13.04 % (3375285)Termination reason: Inappropriate % 90.80/13.04 % (3375285)Time elapsed: 0.052 s % 90.80/13.04 % (3375285)Peak memory usage: 14 MB % 90.80/13.04 % (3375285)Instructions burned: 124 (million) % 90.80/13.04 % (3375285)------------------------------ % 90.80/13.04 % (3375285)------------------------------ % 90.80/13.04 % (3375289)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=3017514696:i=29340_2980 on theBenchmark for (2980ds/29340Mi) % 90.80/13.04 % (3375278)Instruction limit reached! % 90.80/13.04 % (3375278)------------------------------ % 90.80/13.04 % (3375278)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 90.80/13.04 % (3375278)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 90.80/13.04 % (3375278)CaDiCaL version: 2.1.3 % 90.80/13.04 % (3375278)Termination reason: Instruction limit % 121.08/17.38 % (3375278)Termination phase: Saturation % 121.08/17.38 % (3375278)Time elapsed: 1.785 s % 121.08/17.38 % (3375278)Peak memory usage: 31 MB % 121.08/17.38 % (3375278)Instructions burned: 3513 (million) % 121.08/17.38 % (3375291)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=3438774735:i=5211_2973 on theBenchmark for (2973ds/5211Mi) % 121.08/17.38 % (3375281)Instruction limit reached! % 121.08/17.38 % (3375281)------------------------------ % 121.08/17.38 % (3375281)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 121.08/17.38 % (3375281)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 121.08/17.38 % (3375281)CaDiCaL version: 2.1.3 % 121.08/17.38 % (3375281)Termination reason: Instruction limit % 121.08/17.38 % (3375281)Termination phase: Saturation % 121.08/17.38 % (3375281)Time elapsed: 1.655 s % 121.08/17.38 % (3375281)Peak memory usage: 25 MB % 121.08/17.38 % (3375281)Instructions burned: 3773 (million) % 121.08/17.38 % (3375293)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=67693290:i=5497:nm=2_2972 on theBenchmark for (2972ds/5497Mi) % 121.08/17.38 % (3375293)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 121.08/17.38 % (3375293)Terminated due to inappropriate strategy. % 121.08/17.38 % (3375293)------------------------------ % 121.08/17.38 % (3375293)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 121.08/17.38 % (3375293)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 121.08/17.38 % (3375293)CaDiCaL version: 2.1.3 % 121.08/17.38 % (3375293)Termination reason: Inappropriate % 121.08/17.38 % (3375293)Time elapsed: 0.039 s % 121.08/17.38 % (3375293)Peak memory usage: 14 MB % 121.08/17.38 % (3375293)Instructions burned: 92 (million) % 121.08/17.38 % (3375293)------------------------------ % 121.08/17.38 % (3375293)------------------------------ % 121.08/17.38 % (3375295)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=2812355495:fmbsr=2:i=46332_2972 on theBenchmark for (2972ds/46332Mi) % 121.08/17.38 % (3375295)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 121.08/17.38 % (3375295)Terminated due to inappropriate strategy. % 121.08/17.38 % (3375295)------------------------------ % 121.08/17.38 % (3375295)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 121.08/17.38 % (3375295)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 121.08/17.38 % (3375295)CaDiCaL version: 2.1.3 % 121.08/17.38 % (3375295)Termination reason: Inappropriate % 121.08/17.38 % (3375295)Time elapsed: 0.053 s % 121.08/17.38 % (3375295)Peak memory usage: 14 MB % 121.08/17.38 % (3375295)Instructions burned: 128 (million) % 121.08/17.38 % (3375295)------------------------------ % 121.08/17.38 % (3375295)------------------------------ % 121.08/17.38 % (3375297)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=864847217:i=14071_2971 on theBenchmark for (2971ds/14071Mi) % 121.08/17.38 % (3375297)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 121.08/17.38 % (3375297)Terminated due to inappropriate strategy. % 121.08/17.38 % (3375297)------------------------------ % 121.08/17.38 % (3375297)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 121.08/17.38 % (3375297)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 121.08/17.38 % (3375297)CaDiCaL version: 2.1.3 % 121.08/17.38 % (3375297)Termination reason: Inappropriate % 121.08/17.38 % (3375297)Time elapsed: 0.053 s % 121.08/17.38 % (3375297)Peak memory usage: 14 MB % 121.08/17.38 % (3375297)Instructions burned: 128 (million) % 121.08/17.38 % (3375297)------------------------------ % 121.08/17.38 % (3375297)------------------------------ % 121.08/17.38 % (3375299)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=927072663:i=22565:add=on:rawr=on_2970 on theBenchmark for (2970ds/22565Mi) % 121.08/17.38 % (3375287)Instruction limit reached! % 121.08/17.38 % (3375287)------------------------------ % 121.08/17.38 % (3375287)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 121.08/17.38 % (3375287)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 121.08/17.38 % (3375287)CaDiCaL version: 2.1.3 % 121.08/17.38 % (3375287)Termination reason: Instruction limit % 121.08/17.38 % (3375287)Termination phase: Saturation % 121.08/17.38 % (3375287)Time elapsed: 1.197 s % 121.08/17.38 % (3375287)Peak memory usage: 35 MB % 121.08/17.38 % (3375287)Instructions burned: 4593 (million) % 121.08/17.38 % (3375301)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=895049504:i=8173:av=off_2968 on theBenchmark for (2968ds/8173Mi) % 121.08/17.38 % (3375273)Instruction limit reached! % 122.40/17.57 % (3375273)------------------------------ % 122.40/17.57 % (3375273)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 122.40/17.57 % (3375273)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 122.40/17.57 % (3375273)CaDiCaL version: 2.1.3 % 122.40/17.57 % (3375273)Termination reason: Instruction limit % 122.40/17.57 % (3375273)Termination phase: Saturation % 122.40/17.57 % (3375273)Time elapsed: 2.977 s % 122.40/17.57 % (3375273)Peak memory usage: 32 MB % 122.40/17.57 % (3375273)Instructions burned: 5115 (million) % 122.40/17.57 % (3375303)dis+10_16:1_sil=16000:random_seed=3962016754:i=9155:fsr=off_2963 on theBenchmark for (2963ds/9155Mi) % 122.40/17.57 % (3375301)Instruction limit reached! % 122.40/17.57 % (3375301)------------------------------ % 122.40/17.57 % (3375301)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 122.40/17.57 % (3375301)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 122.40/17.57 % (3375301)CaDiCaL version: 2.1.3 % 122.40/17.57 % (3375301)Termination reason: Instruction limit % 122.40/17.57 % (3375301)Termination phase: Saturation % 122.40/17.57 % (3375301)Time elapsed: 1.781 s % 122.40/17.57 % (3375301)Peak memory usage: 36 MB % 122.40/17.57 % (3375301)Instructions burned: 8174 (million) % 122.40/17.57 % (3375305)ott-3_8_sil=64000:random_seed=2075678007:i=20139:bs=on_2950 on theBenchmark for (2950ds/20139Mi) % 122.40/17.57 % (3375291)Instruction limit reached! % 122.40/17.57 % (3375291)------------------------------ % 122.40/17.57 % (3375291)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 122.40/17.57 % (3375291)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 122.40/17.57 % (3375291)CaDiCaL version: 2.1.3 % 122.40/17.57 % (3375291)Termination reason: Instruction limit % 122.40/17.57 % (3375291)Termination phase: Saturation % 122.40/17.57 % (3375291)Time elapsed: 2.750 s % 122.40/17.57 % (3375291)Peak memory usage: 47 MB % 122.40/17.57 % (3375291)Instructions burned: 5211 (million) % 122.40/17.57 % (3375307)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=4104992538:fmbsr=2:i=32576_2946 on theBenchmark for (2946ds/32576Mi) % 122.40/17.57 % (3375307)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 122.40/17.57 % (3375307)Terminated due to inappropriate strategy. % 122.40/17.57 % (3375307)------------------------------ % 122.40/17.57 % (3375307)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 122.40/17.57 % (3375307)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 122.40/17.57 % (3375307)CaDiCaL version: 2.1.3 % 122.40/17.57 % (3375307)Termination reason: Inappropriate % 122.40/17.57 % (3375307)Time elapsed: 0.051 s % 122.40/17.57 % (3375307)Peak memory usage: 14 MB % 122.40/17.57 % (3375307)Instructions burned: 124 (million) % 122.40/17.57 % (3375307)------------------------------ % 122.40/17.57 % (3375307)------------------------------ % 122.40/17.57 % (3375309)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=3836370698:i=11404_2945 on theBenchmark for (2945ds/11404Mi) % 122.40/17.57 % (3375303)Instruction limit reached! % 122.40/17.57 % (3375303)------------------------------ % 122.40/17.57 % (3375303)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 122.40/17.57 % (3375303)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 122.40/17.57 % (3375303)CaDiCaL version: 2.1.3 % 122.40/17.57 % (3375303)Termination reason: Instruction limit % 122.40/17.57 % (3375303)Termination phase: Saturation % 122.40/17.57 % (3375303)Time elapsed: 4.711 s % 122.40/17.57 % (3375303)Peak memory usage: 56 MB % 122.40/17.57 % (3375303)Instructions burned: 9157 (million) % 122.40/17.57 % (3375311)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=4287854740:i=14134_2916 on theBenchmark for (2916ds/14134Mi) % 122.40/17.57 % (3375305)Instruction limit reached! % 122.40/17.57 % (3375305)------------------------------ % 122.40/17.57 % (3375305)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 122.40/17.57 % (3375305)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 122.40/17.57 % (3375305)CaDiCaL version: 2.1.3 % 122.40/17.57 % (3375305)Termination reason: Instruction limit % 122.40/17.57 % (3375305)Termination phase: Saturation % 122.40/17.57 % (3375305)Time elapsed: 5.801 s % 122.40/17.57 % (3375305)Peak memory usage: 71 MB % 122.40/17.57 % (3375305)Instructions burned: 20141 (million) % 122.40/17.57 % (3375313)dis+33_16_sil=32000:sac=on:random_seed=1620434008:i=15851:nm=0_2892 on theBenchmark for (2892ds/15851Mi) % 122.40/17.57 % (3375309)Instruction limit reached! % 122.40/17.57 % (3375309)------------------------------ % 122.40/17.57 % (3375309)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 167.79/23.94 % (3375309)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 167.79/23.94 % (3375309)CaDiCaL version: 2.1.3 % 167.79/23.94 % (3375309)Termination reason: Instruction limit % 167.79/23.94 % (3375309)Termination phase: Saturation % 167.79/23.94 % (3375309)Time elapsed: 7.334 s % 167.79/23.94 % (3375309)Peak memory usage: 48 MB % 167.79/23.94 % (3375309)Instructions burned: 11405 (million) % 167.79/23.94 % (3375315)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=826203114:avsq=on:i=17627:add=on:amm=off_2871 on theBenchmark for (2871ds/17627Mi) % 167.79/23.94 % (3375313)Instruction limit reached! % 167.79/23.94 % (3375313)------------------------------ % 167.79/23.94 % (3375313)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 167.79/23.94 % (3375313)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 167.79/23.94 % (3375313)CaDiCaL version: 2.1.3 % 167.79/23.94 % (3375313)Termination reason: Instruction limit % 167.79/23.94 % (3375313)Termination phase: Saturation % 167.79/23.94 % (3375313)Time elapsed: 3.605 s % 167.79/23.94 % (3375313)Peak memory usage: 34 MB % 167.79/23.94 % (3375313)Instructions burned: 15853 (million) % 167.79/23.94 % (3375317)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=3174248105:s2a=on:i=53295_2856 on theBenchmark for (2856ds/53295Mi) % 167.79/23.94 % (3375289)Instruction limit reached! % 167.79/23.94 % (3375289)------------------------------ % 167.79/23.94 % (3375289)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 167.79/23.94 % (3375289)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 167.79/23.94 % (3375289)CaDiCaL version: 2.1.3 % 167.79/23.94 % (3375289)Termination reason: Instruction limit % 167.79/23.94 % (3375289)Termination phase: Saturation % 167.79/23.94 % (3375289)Time elapsed: 13.875 s % 167.79/23.94 % (3375289)Peak memory usage: 43 MB % 167.79/23.94 % (3375289)Instructions burned: 29342 (million) % 167.79/23.94 % (3375319)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=520780961:i=26857:ins=20_2841 on theBenchmark for (2841ds/26857Mi) % 167.79/23.94 % (3375319)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 167.79/23.94 % (3375319)Terminated due to inappropriate strategy. % 167.79/23.94 % (3375319)------------------------------ % 167.79/23.94 % (3375319)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 167.79/23.94 % (3375319)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 167.79/23.94 % (3375319)CaDiCaL version: 2.1.3 % 167.79/23.94 % (3375319)Termination reason: Inappropriate % 167.79/23.94 % (3375319)Time elapsed: 0.042 s % 167.79/23.94 % (3375319)Peak memory usage: 14 MB % 167.79/23.94 % (3375319)Instructions burned: 93 (million) % 167.79/23.94 % (3375319)------------------------------ % 167.79/23.94 % (3375319)------------------------------ % 167.79/23.94 % (3375321)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=2563092770:i=28120:bs=on:fsr=off_2840 on theBenchmark for (2840ds/28120Mi) % 167.79/23.94 % (3375299)Instruction limit reached! % 167.79/23.94 % (3375299)------------------------------ % 167.79/23.94 % (3375299)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 167.79/23.94 % (3375299)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 167.79/23.94 % (3375299)CaDiCaL version: 2.1.3 % 167.79/23.94 % (3375299)Termination reason: Instruction limit % 167.79/23.94 % (3375299)Termination phase: Saturation % 167.79/23.94 % (3375299)Time elapsed: 14.129 s % 167.79/23.94 % (3375299)Peak memory usage: 115 MB % 167.79/23.94 % (3375299)Instructions burned: 22566 (million) % 167.79/23.94 % (3375323)fmb+10_1_sil=256000:fmbss=7:random_seed=2384816314:fmbsr=1.6:i=182295_2828 on theBenchmark for (2828ds/182295Mi) % 167.79/23.94 % (3375311)Instruction limit reached! % 167.79/23.94 % (3375311)------------------------------ % 167.79/23.94 % (3375311)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 167.79/23.94 % (3375311)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 167.79/23.94 % (3375311)CaDiCaL version: 2.1.3 % 167.79/23.94 % (3375311)Termination reason: Instruction limit % 167.79/23.94 % (3375311)Termination phase: Saturation % 167.79/23.94 % (3375311)Time elapsed: 8.735 s % 167.79/23.94 % (3375311)Peak memory usage: 54 MB % 167.79/23.94 % (3375311)Instructions burned: 14134 (million) % 167.79/23.94 % (3375323)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 167.79/23.94 % (3375323)Terminated due to inappropriate strategy. % 167.79/23.94 % (3375323)------------------------------ % 167.79/23.94 % (3375323)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 179.46/25.67 % (3375323)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 179.46/25.67 % (3375323)CaDiCaL version: 2.1.3 % 179.46/25.67 % (3375323)Termination reason: Inappropriate % 179.46/25.67 % (3375323)Time elapsed: 0.040 s % 179.46/25.67 % (3375323)Peak memory usage: 14 MB % 179.46/25.67 % (3375323)Instructions burned: 92 (million) % 179.46/25.67 % (3375325)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=1473389202:i=44625:gsp=on_2828 on theBenchmark for (2828ds/44625Mi) % 179.46/25.67 % (3375323)------------------------------ % 179.46/25.67 % (3375323)------------------------------ % 179.46/25.67 % (3375327)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=3025325121:i=160505_2828 on theBenchmark for (2828ds/160505Mi) % 179.46/25.67 % (3375325)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 179.46/25.67 % (3375325)Terminated due to inappropriate strategy. % 179.46/25.67 % (3375325)------------------------------ % 179.46/25.67 % (3375325)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 179.46/25.67 % (3375325)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 179.46/25.67 % (3375325)CaDiCaL version: 2.1.3 % 179.46/25.67 % (3375325)Termination reason: Inappropriate % 179.46/25.67 % (3375325)Time elapsed: 0.044 s % 179.46/25.67 % (3375325)Peak memory usage: 15 MB % 179.46/25.67 % (3375325)Instructions burned: 97 (million) % 179.46/25.67 % (3375325)------------------------------ % 179.46/25.67 % (3375325)------------------------------ % 179.46/25.67 % (3375327)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 179.46/25.67 % (3375327)Terminated due to inappropriate strategy. % 179.46/25.67 % (3375327)------------------------------ % 179.46/25.67 % (3375327)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 179.46/25.67 % (3375327)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 179.46/25.67 % (3375327)CaDiCaL version: 2.1.3 % 179.46/25.67 % (3375327)Termination reason: Inappropriate % 179.46/25.67 % (3375327)Time elapsed: 0.040 s % 179.46/25.67 % (3375327)Peak memory usage: 14 MB % 179.46/25.67 % (3375327)Instructions burned: 92 (million) % 179.46/25.67 % (3375327)------------------------------ % 179.46/25.67 % (3375327)------------------------------ % 179.46/25.67 % (3375329)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=3430291708:fmbsr=1.3:i=225729_2827 on theBenchmark for (2827ds/225729Mi) % 179.46/25.67 % (3375330)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=1863735972:fmbsr=2:i=185024:ins=7_2827 on theBenchmark for (2827ds/185024Mi) % 179.46/25.67 % (3375329)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 179.46/25.67 % (3375329)Terminated due to inappropriate strategy. % 179.46/25.67 % (3375329)------------------------------ % 179.46/25.67 % (3375329)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 179.46/25.67 % (3375329)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 179.46/25.67 % (3375329)CaDiCaL version: 2.1.3 % 179.46/25.67 % (3375329)Termination reason: Inappropriate % 179.46/25.67 % (3375329)Time elapsed: 0.053 s % 179.46/25.67 % (3375329)Peak memory usage: 14 MB % 179.46/25.67 % (3375329)Instructions burned: 128 (million) % 179.46/25.67 % (3375329)------------------------------ % 179.46/25.67 % (3375329)------------------------------ % 179.46/25.67 % (3375330)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 179.46/25.67 % (3375330)Terminated due to inappropriate strategy. % 179.46/25.67 % (3375330)------------------------------ % 179.46/25.67 % (3375330)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 179.46/25.67 % (3375330)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 179.46/25.67 % (3375330)CaDiCaL version: 2.1.3 % 179.46/25.67 % (3375330)Termination reason: Inappropriate % 179.46/25.67 % (3375330)Time elapsed: 0.053 s % 179.46/25.67 % (3375330)Peak memory usage: 14 MB % 179.46/25.67 % (3375330)Instructions burned: 128 (million) % 179.46/25.67 % (3375330)------------------------------ % 179.46/25.67 % (3375330)------------------------------ % 179.46/25.67 % (3375333)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=3278475507:rtra=on_2827 on theBenchmark for (2827ds/0Mi) % 179.46/25.67 % (3375334)% WARNING: option uhcvi not known. % 179.46/25.67 % (3375334)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=965241604:i=271062:add=off:rtra=on:rawr=on_2826 on theBenchmark for (2826ds/271062Mi) % 179.46/25.67 % (3375333)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 197.29/28.04 % (3375333)Terminated due to inappropriate strategy. % 197.29/28.04 % (3375333)------------------------------ % 197.29/28.04 % (3375333)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 197.29/28.04 % (3375333)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 197.29/28.04 % (3375333)CaDiCaL version: 2.1.3 % 197.29/28.04 % (3375333)Termination reason: Inappropriate % 197.29/28.04 % (3375333)Time elapsed: 0.051 s % 197.29/28.04 % (3375333)Peak memory usage: 15 MB % 197.29/28.04 % (3375333)Instructions burned: 108 (million) % 197.29/28.04 % (3375333)------------------------------ % 197.29/28.04 % (3375333)------------------------------ % 197.29/28.04 % (3375337)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=763782904:i=176048:add=on:rtra=on:rawr=on_2826 on theBenchmark for (2826ds/176048Mi) % 197.29/28.04 % (3375315)Instruction limit reached! % 197.29/28.04 % (3375315)------------------------------ % 197.29/28.04 % (3375315)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 197.29/28.04 % (3375315)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 197.29/28.04 % (3375315)CaDiCaL version: 2.1.3 % 197.29/28.04 % (3375315)Termination reason: Instruction limit % 197.29/28.04 % (3375315)Termination phase: Saturation % 197.29/28.04 % (3375315)Time elapsed: 10.265 s % 197.29/28.04 % (3375315)Peak memory usage: 141 MB % 197.29/28.04 % (3375315)Instructions burned: 17628 (million) % 197.29/28.04 % (3375339)dis+10_1_sil=32000:si=on:sp=arity:random_seed=438086315:i=206:fgj=on:rtra=on_2768 on theBenchmark for (2768ds/206Mi) % 197.29/28.04 % (3375339)Instruction limit reached! % 197.29/28.04 % (3375339)------------------------------ % 197.29/28.04 % (3375339)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 197.29/28.04 % (3375339)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 197.29/28.04 % (3375339)CaDiCaL version: 2.1.3 % 197.29/28.04 % (3375339)Termination reason: Instruction limit % 197.29/28.04 % (3375339)Termination phase: Saturation % 197.29/28.04 % (3375339)Time elapsed: 0.104 s % 197.29/28.04 % (3375339)Peak memory usage: 17 MB % 197.29/28.04 % (3375339)Instructions burned: 206 (million) % 197.29/28.04 % (3375341)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=1753154920:i=232:rtra=on_2767 on theBenchmark for (2767ds/232Mi) % 197.29/28.04 % (3375341)Instruction limit reached! % 197.29/28.04 % (3375341)------------------------------ % 197.29/28.04 % (3375341)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 197.29/28.04 % (3375341)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 197.29/28.04 % (3375341)CaDiCaL version: 2.1.3 % 197.29/28.04 % (3375341)Termination reason: Instruction limit % 197.29/28.04 % (3375341)Termination phase: Saturation % 197.29/28.04 % (3375341)Time elapsed: 0.109 s % 197.29/28.04 % (3375341)Peak memory usage: 17 MB % 197.29/28.04 % (3375341)Instructions burned: 234 (million) % 197.29/28.04 % (3375343)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=209361951:i=262:rtra=on_2766 on theBenchmark for (2766ds/262Mi) % 197.29/28.04 % (3375343)Instruction limit reached! % 197.29/28.04 % (3375343)------------------------------ % 197.29/28.04 % (3375343)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 197.29/28.04 % (3375343)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 197.29/28.04 % (3375343)CaDiCaL version: 2.1.3 % 197.29/28.04 % (3375343)Termination reason: Instruction limit % 197.29/28.04 % (3375343)Termination phase: Saturation % 197.29/28.04 % (3375343)Time elapsed: 0.125 s % 197.29/28.04 % (3375343)Peak memory usage: 18 MB % 197.29/28.04 % (3375343)Instructions burned: 263 (million) % 197.29/28.04 % (3375345)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=1936727821:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2764 on theBenchmark for (2764ds/318Mi) % 197.29/28.04 % (3375345)Instruction limit reached! % 197.29/28.04 % (3375345)------------------------------ % 197.29/28.04 % (3375345)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 197.29/28.04 % (3375345)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 197.29/28.04 % (3375345)CaDiCaL version: 2.1.3 % 197.29/28.04 % (3375345)Termination reason: Instruction limit % 197.29/28.04 % (3375345)Termination phase: Saturation % 197.29/28.04 % (3375345)Time elapsed: 0.153 s % 197.29/28.04 % (3375345)Peak memory usage: 19 MB % 197.29/28.04 % (3375345)Instructions burned: 318 (million) % 197.29/28.04 % (3375347)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=1720677371:i=1428:nm=2:rtra=on_2762 on theBenchmark for (2762ds/1428Mi) % 200.73/28.78 % (3375347)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 200.73/28.78 % (3375347)Terminated due to inappropriate strategy. % 200.73/28.78 % (3375347)------------------------------ % 200.73/28.78 % (3375347)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 200.73/28.78 % (3375347)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 200.73/28.78 % (3375347)CaDiCaL version: 2.1.3 % 200.73/28.78 % (3375347)Termination reason: Inappropriate % 200.73/28.78 % (3375347)Time elapsed: 0.051 s % 200.73/28.78 % (3375347)Peak memory usage: 15 MB % 200.73/28.78 % (3375347)Instructions burned: 107 (million) % 200.73/28.78 % (3375347)------------------------------ % 200.73/28.78 % (3375347)------------------------------ % 200.73/28.78 % (3375349)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=824086050:i=262:bd=preordered:rtra=on:fsd=on_2762 on theBenchmark for (2762ds/262Mi) % 200.73/28.78 % (3375349)Instruction limit reached! % 200.73/28.78 % (3375349)------------------------------ % 200.73/28.78 % (3375349)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 200.73/28.78 % (3375349)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 200.73/28.78 % (3375349)CaDiCaL version: 2.1.3 % 200.73/28.78 % (3375349)Termination reason: Instruction limit % 200.73/28.78 % (3375349)Termination phase: Saturation % 200.73/28.78 % (3375349)Time elapsed: 0.120 s % 200.73/28.78 % (3375349)Peak memory usage: 17 MB % 200.73/28.78 % (3375349)Instructions burned: 263 (million) % 200.73/28.78 % (3375351)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=3109395352:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2760 on theBenchmark for (2760ds/1368Mi) % 200.73/28.78 % (3375351)Instruction limit reached! % 200.73/28.78 % (3375351)------------------------------ % 200.73/28.78 % (3375351)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 200.73/28.78 % (3375351)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 200.73/28.78 % (3375351)CaDiCaL version: 2.1.3 % 200.73/28.78 % (3375351)Termination reason: Instruction limit % 200.73/28.78 % (3375351)Termination phase: Saturation % 200.73/28.78 % (3375351)Time elapsed: 0.717 s % 200.73/28.78 % (3375351)Peak memory usage: 25 MB % 200.73/28.78 % (3375351)Instructions burned: 1370 (million) % 200.73/28.78 % (3375353)ott-21_1_sil=16000:si=on:fs=off:random_seed=135240419:i=360:av=off:fsr=off:rtra=on_2753 on theBenchmark for (2753ds/360Mi) % 200.73/28.78 % (3375353)Instruction limit reached! % 200.73/28.78 % (3375353)------------------------------ % 200.73/28.78 % (3375353)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 200.73/28.78 % (3375353)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 200.73/28.78 % (3375353)CaDiCaL version: 2.1.3 % 200.73/28.78 % (3375353)Termination reason: Instruction limit % 200.73/28.78 % (3375353)Termination phase: Saturation % 200.73/28.78 % (3375353)Time elapsed: 0.178 s % 200.73/28.78 % (3375353)Peak memory usage: 17 MB % 200.73/28.78 % (3375353)Instructions burned: 360 (million) % 200.73/28.78 % (3375355)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3279251358:i=954:bd=all:rtra=on_2751 on theBenchmark for (2751ds/954Mi) % 200.73/28.78 % (3375355)Instruction limit reached! % 200.73/28.78 % (3375355)------------------------------ % 200.73/28.78 % (3375355)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 200.73/28.78 % (3375355)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 200.73/28.78 % (3375355)CaDiCaL version: 2.1.3 % 200.73/28.78 % (3375355)Termination reason: Instruction limit % 200.73/28.78 % (3375355)Termination phase: Saturation % 200.73/28.78 % (3375355)Time elapsed: 0.508 s % 200.73/28.78 % (3375355)Peak memory usage: 20 MB % 200.73/28.78 % (3375355)Instructions burned: 956 (million) % 200.73/28.78 % (3375357)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=3425985526:fmbsr=1.3:i=1730:ins=25:rtra=on_2746 on theBenchmark for (2746ds/1730Mi) % 200.73/28.78 % (3375357)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 200.73/28.78 % (3375357)Terminated due to inappropriate strategy. % 200.73/28.78 % (3375357)------------------------------ % 200.73/28.78 % (3375357)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 200.73/28.78 % (3375357)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 200.73/28.78 % (3375357)CaDiCaL version: 2.1.3 % 200.73/28.78 % (3375357)Termination reason: Inappropriate % 238.21/33.87 % (3375357)Time elapsed: 0.050 s % 238.21/33.87 % (3375357)Peak memory usage: 15 MB % 238.21/33.87 % (3375357)Instructions burned: 106 (million) % 238.21/33.87 % (3375357)------------------------------ % 238.21/33.87 % (3375357)------------------------------ % 238.21/33.87 % (3375359)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=3407213156:i=2358:rtra=on_2745 on theBenchmark for (2745ds/2358Mi) % 238.21/33.87 % (3375359)Instruction limit reached! % 238.21/33.87 % (3375359)------------------------------ % 238.21/33.87 % (3375359)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 238.21/33.87 % (3375359)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 238.21/33.87 % (3375359)CaDiCaL version: 2.1.3 % 238.21/33.87 % (3375359)Termination reason: Instruction limit % 238.21/33.87 % (3375359)Termination phase: Saturation % 238.21/33.87 % (3375359)Time elapsed: 1.375 s % 238.21/33.87 % (3375359)Peak memory usage: 27 MB % 238.21/33.87 % (3375359)Instructions burned: 2358 (million) % 238.21/33.87 % (3375361)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=19886446:i=1778:ins=1:rtra=on_2731 on theBenchmark for (2731ds/1778Mi) % 238.21/33.87 % (3375361)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 238.21/33.87 % (3375361)Terminated due to inappropriate strategy. % 238.21/33.87 % (3375361)------------------------------ % 238.21/33.87 % (3375361)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 238.21/33.87 % (3375361)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 238.21/33.87 % (3375361)CaDiCaL version: 2.1.3 % 238.21/33.87 % (3375361)Termination reason: Inappropriate % 238.21/33.87 % (3375361)Time elapsed: 0.072 s % 238.21/33.87 % (3375361)Peak memory usage: 17 MB % 238.21/33.87 % (3375361)Instructions burned: 143 (million) % 238.21/33.87 % (3375361)------------------------------ % 238.21/33.87 % (3375361)------------------------------ % 238.21/33.87 % (3375363)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=1771117645:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2730 on theBenchmark for (2730ds/1384Mi) % 238.21/33.87 % (3375321)Instruction limit reached! % 238.21/33.87 % (3375321)------------------------------ % 238.21/33.87 % (3375321)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 238.21/33.87 % (3375321)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 238.21/33.87 % (3375321)CaDiCaL version: 2.1.3 % 238.21/33.87 % (3375321)Termination reason: Instruction limit % 238.21/33.87 % (3375321)Termination phase: Saturation % 238.21/33.87 % (3375321)Time elapsed: 11.427 s % 238.21/33.87 % (3375321)Peak memory usage: 28 MB % 238.21/33.87 % (3375321)Instructions burned: 28122 (million) % 238.21/33.87 % (3375365)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=2705672026:i=1758:kws=inv_precedence:fsr=off:rtra=on_2725 on theBenchmark for (2725ds/1758Mi) % 238.21/33.87 % (3375317)Instruction limit reached! % 238.21/33.87 % (3375317)------------------------------ % 238.21/33.87 % (3375317)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 238.21/33.87 % (3375317)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 238.21/33.87 % (3375317)CaDiCaL version: 2.1.3 % 238.21/33.87 % (3375317)Termination reason: Instruction limit % 238.21/33.87 % (3375317)Termination phase: Saturation % 238.21/33.87 % (3375317)Time elapsed: 13.366 s % 238.21/33.87 % (3375317)Peak memory usage: 146 MB % 238.21/33.87 % (3375317)Instructions burned: 53296 (million) % 238.21/33.87 % (3375367)fmb+10_1_sil=64000:si=on:random_seed=3237326525:i=44122:nm=2:rtra=on:gsp=on_2722 on theBenchmark for (2722ds/44122Mi) % 238.21/33.87 % (3375367)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 238.21/33.87 % (3375367)Terminated due to inappropriate strategy. % 238.21/33.87 % (3375367)------------------------------ % 238.21/33.87 % (3375367)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 238.21/33.87 % (3375367)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 238.21/33.87 % (3375367)CaDiCaL version: 2.1.3 % 238.21/33.87 % (3375367)Termination reason: Inappropriate % 238.21/33.87 % (3375367)Time elapsed: 0.030 s % 238.21/33.87 % (3375367)Peak memory usage: 15 MB % 238.21/33.87 % (3375367)Instructions burned: 116 (million) % 238.21/33.87 % (3375367)------------------------------ % 238.21/33.87 % (3375367)------------------------------ % 238.21/33.87 % (3375369)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=211910243:i=19030:nm=5:rtra=on_2721 on theBenchmark for (2721ds/19030Mi) % 252.39/36.00 % (3375369)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 252.39/36.00 % (3375369)Terminated due to inappropriate strategy. % 252.39/36.00 % (3375369)------------------------------ % 252.39/36.00 % (3375369)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 252.39/36.00 % (3375369)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 252.39/36.00 % (3375369)CaDiCaL version: 2.1.3 % 252.39/36.00 % (3375369)Termination reason: Inappropriate % 252.39/36.00 % (3375369)Time elapsed: 0.028 s % 252.39/36.00 % (3375369)Peak memory usage: 16 MB % 252.39/36.00 % (3375369)Instructions burned: 107 (million) % 252.39/36.00 % (3375363)Instruction limit reached! % 252.39/36.00 % (3375363)------------------------------ % 252.39/36.00 % (3375363)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 252.39/36.00 % (3375363)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 252.39/36.00 % (3375363)CaDiCaL version: 2.1.3 % 252.39/36.00 % (3375363)Termination reason: Instruction limit % 252.39/36.00 % (3375363)Termination phase: Saturation % 252.39/36.00 % (3375363)Time elapsed: 0.874 s % 252.39/36.00 % (3375363)Peak memory usage: 27 MB % 252.39/36.00 % (3375363)Instructions burned: 1386 (million) % 252.39/36.00 % (3375369)------------------------------ % 252.39/36.00 % (3375369)------------------------------ % 252.39/36.00 % (3375371)fmb+10_1_sil=64000:sas=cadical:si=on:fmbss=8:random_seed=855245214:fmbsr=1.7:i=1840:rtra=on_2721 on theBenchmark for (2721ds/1840Mi) % 252.39/36.00 % (3375372)dis-4_1_sil=16000:drc=ordering:si=on:sp=const_frequency:sac=on:newcnf=on:random_seed=2851813795:i=10262:rtra=on_2721 on theBenchmark for (2721ds/10262Mi) % 252.39/36.00 % (3375371)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 252.39/36.00 % (3375371)Terminated due to inappropriate strategy. % 252.39/36.00 % (3375371)------------------------------ % 252.39/36.00 % (3375371)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 252.39/36.00 % (3375371)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 252.39/36.00 % (3375371)CaDiCaL version: 2.1.3 % 252.39/36.00 % (3375371)Termination reason: Inappropriate % 252.39/36.00 % (3375371)Time elapsed: 0.028 s % 252.39/36.00 % (3375371)Peak memory usage: 15 MB % 252.39/36.00 % (3375371)Instructions burned: 107 (million) % 252.39/36.00 % (3375371)------------------------------ % 252.39/36.00 % (3375371)------------------------------ % 252.39/36.00 % (3375375)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:si=on:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1375632206:i=2944:ins=7:rtra=on:fdi=8:gsp=on_2721 on theBenchmark for (2721ds/2944Mi) % 252.39/36.00 % (3375365)Instruction limit reached! % 252.39/36.00 % (3375365)------------------------------ % 252.39/36.00 % (3375365)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 252.39/36.00 % (3375365)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 252.39/36.00 % (3375365)CaDiCaL version: 2.1.3 % 252.39/36.00 % (3375365)Termination reason: Instruction limit % 252.39/36.00 % (3375365)Termination phase: Saturation % 252.39/36.00 % (3375365)Time elapsed: 0.994 s % 252.39/36.00 % (3375365)Peak memory usage: 28 MB % 252.39/36.00 % (3375365)Instructions burned: 1758 (million) % 252.39/36.00 % (3375377)fmb+10_1_sil=16000:sas=cadical:si=on:bce=on:fmbss=77:random_seed=730088766:i=12648:rtra=on_2715 on theBenchmark for (2715ds/12648Mi) % 252.39/36.00 % (3375377)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 252.39/36.00 % (3375377)Terminated due to inappropriate strategy. % 252.39/36.00 % (3375377)------------------------------ % 252.39/36.00 % (3375377)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 252.39/36.00 % (3375377)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 252.39/36.00 % (3375377)CaDiCaL version: 2.1.3 % 252.39/36.00 % (3375377)Termination reason: Inappropriate % 252.39/36.00 % (3375377)Time elapsed: 0.051 s % 252.39/36.00 % (3375377)Peak memory usage: 15 MB % 252.39/36.00 % (3375377)Instructions burned: 107 (million) % 252.39/36.00 % (3375377)------------------------------ % 252.39/36.00 % (3375377)------------------------------ % 252.39/36.00 % (3375379)fmb+10_1_fmbas=function:sil=32000:sas=cadical:si=on:fmbss=16:random_seed=3498428617:fmbsr=2.30978:i=4348:rtra=on_2715 on theBenchmark for (2715ds/4348Mi) % 252.39/36.00 % (3375379)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 252.39/36.00 % (3375379)Terminated due to inappropriate strategy. % 252.39/36.00 % (3375379)-------------Terminated % 300.68/42.64 % Vampire exiting %------------------------------------------------------------------------------