%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWV316-1 : TPTP v9.3.1. Released v3.2.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:20:52 PM UTC 2026 % Result : Timeout 300.29s 42.63s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : SWV316-1 : TPTP v9.3.1. Released v3.2.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.07/0.18 % Computer : n006.cluster.edu % 0.07/0.18 % Model : x86_64 x86_64 % 0.07/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.07/0.18 % Memory : 8046.5625MB % 0.07/0.18 % OS : Linux 6.8.0-71-generic % 0.07/0.18 % CPULimit : 300 % 0.07/0.18 % WCLimit : 300 % 0.07/0.18 % DateTime : Mon Sep 28 10:32:55 UTC 2026 % 0.07/0.19 % CPUTime : % 0.07/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.07/0.22 Running first-order model finding % 0.07/0.22 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 6.94/1.45 % (3873138)Will run a generic schedule for satisfiability detection. % 6.94/1.45 % (3873171)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=655498510:i=131_2999 on theBenchmark for (2999ds/131Mi) % 6.94/1.45 % (3873167)% WARNING: option uhcvi not known. % 6.94/1.45 % (3873166)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1996758424_2999 on theBenchmark for (2999ds/0Mi) % 6.94/1.45 % (3873167)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1181412789:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 6.94/1.45 % (3873168)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2528211448:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 6.94/1.45 % (3873169)dis+10_1_sil=32000:sp=arity:random_seed=2215885990:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 6.94/1.45 % (3873170)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1897554034:i=116_2999 on theBenchmark for (2999ds/116Mi) % 6.94/1.45 % (3873172)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3140999119:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 6.94/1.45 % (3873171)Instruction limit reached! % 6.94/1.45 % (3873171)------------------------------ % 6.94/1.45 % (3873171)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.94/1.45 % (3873171)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.94/1.45 % (3873171)CaDiCaL version: 2.1.3 % 6.94/1.45 % (3873171)Termination reason: Instruction limit % 6.94/1.45 % (3873171)Termination phase: Saturation % 6.94/1.45 % (3873171)Time elapsed: 0.042 s % 6.94/1.45 % (3873171)Peak memory usage: 16 MB % 6.94/1.45 % (3873171)Instructions burned: 131 (million) % 6.94/1.45 % (3873195)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=4215261783:i=714:nm=2_2998 on theBenchmark for (2998ds/714Mi) % 6.94/1.45 % (3873169)Instruction limit reached! % 6.94/1.45 % (3873169)------------------------------ % 6.94/1.45 % (3873169)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.94/1.45 % (3873169)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.94/1.45 % (3873169)CaDiCaL version: 2.1.3 % 6.94/1.45 % (3873169)Termination reason: Instruction limit % 6.94/1.45 % (3873169)Termination phase: Saturation % 6.94/1.45 % (3873169)Time elapsed: 0.063 s % 6.94/1.45 % (3873169)Peak memory usage: 15 MB % 6.94/1.45 % (3873169)Instructions burned: 104 (million) % 6.94/1.45 % (3873170)Instruction limit reached! % 6.94/1.45 % (3873170)------------------------------ % 6.94/1.45 % (3873170)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.94/1.45 % (3873170)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.94/1.45 % (3873170)CaDiCaL version: 2.1.3 % 6.94/1.45 % (3873170)Termination reason: Instruction limit % 6.94/1.45 % (3873170)Termination phase: Saturation % 6.94/1.45 % (3873170)Time elapsed: 0.065 s % 6.94/1.45 % (3873170)Peak memory usage: 16 MB % 6.94/1.45 % (3873170)Instructions burned: 117 (million) % 6.94/1.45 % (3873203)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=720982839:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi) % 6.94/1.45 % (3873204)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=2685813698:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi) % 6.94/1.45 % (3873172)Instruction limit reached! % 6.94/1.45 % (3873172)------------------------------ % 6.94/1.45 % (3873172)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.94/1.45 % (3873172)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.94/1.45 % (3873172)CaDiCaL version: 2.1.3 % 6.94/1.45 % (3873172)Termination reason: Instruction limit % 6.94/1.45 % (3873172)Termination phase: Saturation % 6.94/1.45 % (3873172)Time elapsed: 0.099 s % 6.94/1.45 % (3873172)Peak memory usage: 17 MB % 6.94/1.45 % (3873172)Instructions burned: 159 (million) % 6.94/1.45 % (3873218)ott-21_1_sil=16000:fs=off:random_seed=759452054:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 6.94/1.45 % (3873203)Instruction limit reached! % 6.94/1.45 % (3873203)------------------------------ % 6.94/1.45 % (3873203)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.94/1.45 % (3873203)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.94/1.45 % (3873203)CaDiCaL version: 2.1.3 % 29.23/4.48 % (3873203)Termination reason: Instruction limit % 29.23/4.48 % (3873203)Termination phase: Saturation % 29.23/4.48 % (3873203)Time elapsed: 0.076 s % 29.23/4.48 % (3873203)Peak memory usage: 16 MB % 29.23/4.48 % (3873203)Instructions burned: 132 (million) % 29.23/4.48 % (3873220)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3123395650:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi) % 29.23/4.48 % TRYING [1] % 29.23/4.48 % (3873218)Instruction limit reached! % 29.23/4.48 % (3873218)------------------------------ % 29.23/4.48 % (3873218)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 29.23/4.48 % (3873218)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.23/4.48 % (3873218)CaDiCaL version: 2.1.3 % 29.23/4.48 % (3873218)Termination reason: Instruction limit % 29.23/4.48 % (3873218)Termination phase: Saturation % 29.23/4.48 % (3873218)Time elapsed: 0.099 s % 29.23/4.48 % (3873218)Peak memory usage: 16 MB % 29.23/4.48 % (3873218)Instructions burned: 180 (million) % 29.23/4.48 % TRYING [2] % 29.23/4.48 % (3873195)Instruction limit reached! % 29.23/4.48 % (3873195)------------------------------ % 29.23/4.48 % (3873195)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 29.23/4.48 % (3873195)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.23/4.48 % (3873195)CaDiCaL version: 2.1.3 % 29.23/4.48 % (3873195)Termination reason: Instruction limit % 29.23/4.48 % (3873195)Termination phase: Finite model building constraint generation % 29.23/4.48 % (3873195)Time elapsed: 0.183 s % 29.23/4.48 % (3873195)Peak memory usage: 27 MB % 29.23/4.48 % (3873195)Instructions burned: 715 (million) % 29.23/4.48 % (3873228)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=156310063:i=1179_2996 on theBenchmark for (2996ds/1179Mi) % 29.23/4.48 % (3873227)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3559570178:fmbsr=1.3:i=865:ins=25_2996 on theBenchmark for (2996ds/865Mi) % 29.23/4.48 % TRYING [1] % 29.23/4.48 % TRYING [2] % 29.23/4.48 % (3873204)Instruction limit reached! % 29.23/4.48 % (3873204)------------------------------ % 29.23/4.48 % (3873204)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 29.23/4.48 % (3873204)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.23/4.48 % (3873204)CaDiCaL version: 2.1.3 % 29.23/4.48 % (3873204)Termination reason: Instruction limit % 29.23/4.48 % (3873204)Termination phase: Saturation % 29.23/4.48 % (3873204)Time elapsed: 0.342 s % 29.23/4.48 % (3873204)Peak memory usage: 20 MB % 29.23/4.48 % (3873204)Instructions burned: 685 (million) % 29.23/4.48 % (3873273)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=4249510363:i=889:ins=1_2994 on theBenchmark for (2994ds/889Mi) % 29.23/4.48 % (3873220)Instruction limit reached! % 29.23/4.48 % (3873220)------------------------------ % 29.23/4.48 % (3873220)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 29.23/4.48 % (3873220)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.23/4.48 % (3873220)CaDiCaL version: 2.1.3 % 29.23/4.48 % (3873220)Termination reason: Instruction limit % 29.23/4.48 % (3873220)Termination phase: Saturation % 29.23/4.48 % (3873220)Time elapsed: 0.292 s % 29.23/4.48 % (3873220)Peak memory usage: 17 MB % 29.23/4.48 % (3873220)Instructions burned: 477 (million) % 29.23/4.48 % (3873275)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=125197853:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2994 on theBenchmark for (2994ds/692Mi) % 29.23/4.48 % TRYING [1] % 29.23/4.48 % (3873228)Instruction limit reached! % 29.23/4.48 % (3873228)------------------------------ % 29.23/4.48 % (3873228)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 29.23/4.48 % (3873228)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.23/4.48 % (3873228)CaDiCaL version: 2.1.3 % 29.23/4.48 % (3873228)Termination reason: Instruction limit % 29.23/4.48 % (3873228)Termination phase: Saturation % 29.23/4.48 % (3873228)Time elapsed: 0.406 s % 29.23/4.48 % (3873228)Peak memory usage: 29 MB % 29.23/4.48 % (3873228)Instructions burned: 1181 (million) % 29.23/4.48 % (3873277)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2795238101:i=879:kws=inv_precedence:fsr=off_2992 on theBenchmark for (2992ds/879Mi) % 29.23/4.48 % (3873227)Instruction limit reached! % 29.23/4.48 % (3873227)------------------------------ % 29.23/4.48 % (3873227)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 29.23/4.48 % (3873227)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 59.01/8.61 % (3873227)CaDiCaL version: 2.1.3 % 59.01/8.61 % (3873227)Termination reason: Instruction limit % 59.01/8.61 % (3873227)Termination phase: Finite model building constraint generation % 59.01/8.61 % (3873227)Time elapsed: 0.427 s % 59.01/8.61 % (3873227)Peak memory usage: 42 MB % 59.01/8.61 % (3873227)Instructions burned: 866 (million) % 59.01/8.61 % (3873279)fmb+10_1_sil=64000:random_seed=3058922195:i=22061:nm=2:gsp=on_2992 on theBenchmark for (2992ds/22061Mi) % 59.01/8.61 % (3873273)Cannot represent all propositional literals internally % 59.01/8.61 % (3873273)Refutation not found, incomplete strategy % 59.01/8.61 % (3873273)------------------------------ % 59.01/8.61 % (3873273)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 59.01/8.61 % (3873273)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 59.01/8.61 % (3873273)CaDiCaL version: 2.1.3 % 59.01/8.61 % (3873273)Termination reason: Refutation not found, incomplete strategy % 59.01/8.61 % (3873273)Time elapsed: 0.312 s % 59.01/8.61 % (3873273)Peak memory usage: 25 MB % 59.01/8.61 % (3873273)Instructions burned: 632 (million) % 59.01/8.61 % (3873273)------------------------------ % 59.01/8.61 % (3873273)------------------------------ % 59.01/8.61 % (3873281)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=135297201:i=9515:nm=5_2991 on theBenchmark for (2991ds/9515Mi) % 59.01/8.61 % (3873277)Instruction limit reached! % 59.01/8.61 % (3873277)------------------------------ % 59.01/8.61 % (3873277)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 59.01/8.61 % (3873277)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 59.01/8.61 % (3873277)CaDiCaL version: 2.1.3 % 59.01/8.61 % (3873277)Termination reason: Instruction limit % 59.01/8.61 % (3873277)Termination phase: Saturation % 59.01/8.61 % (3873277)Time elapsed: 0.235 s % 59.01/8.61 % (3873277)Peak memory usage: 21 MB % 59.01/8.61 % (3873277)Instructions burned: 881 (million) % 59.01/8.61 % (3873283)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1060942570:fmbsr=1.7:i=920_2990 on theBenchmark for (2990ds/920Mi) % 59.01/8.61 % (3873275)Instruction limit reached! % 59.01/8.61 % (3873275)------------------------------ % 59.01/8.61 % (3873275)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 59.01/8.61 % (3873275)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 59.01/8.61 % (3873275)CaDiCaL version: 2.1.3 % 59.01/8.61 % (3873275)Termination reason: Instruction limit % 59.01/8.61 % (3873275)Termination phase: Saturation % 59.01/8.61 % (3873275)Time elapsed: 0.427 s % 59.01/8.61 % (3873275)Peak memory usage: 23 MB % 59.01/8.61 % (3873275)Instructions burned: 692 (million) % 59.01/8.61 % (3873285)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2793283340:i=5131_2989 on theBenchmark for (2989ds/5131Mi) % 59.01/8.61 % TRYING [1] % 59.01/8.61 % (3873283)Cannot represent all propositional literals internally % 59.01/8.61 % (3873283)Refutation not found, incomplete strategy % 59.01/8.61 % (3873283)------------------------------ % 59.01/8.61 % (3873283)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 59.01/8.61 % (3873283)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 59.01/8.61 % (3873283)CaDiCaL version: 2.1.3 % 59.01/8.61 % (3873283)Termination reason: Refutation not found, incomplete strategy % 59.01/8.61 % (3873283)Time elapsed: 0.168 s % 59.01/8.61 % (3873283)Peak memory usage: 24 MB % 59.01/8.61 % (3873283)Instructions burned: 629 (million) % 59.01/8.61 % (3873283)------------------------------ % 59.01/8.61 % (3873283)------------------------------ % 59.01/8.61 % (3873287)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=198201485:i=1472:ins=7:fdi=8:gsp=on_2988 on theBenchmark for (2988ds/1472Mi) % 59.01/8.61 % (3873281)Cannot represent all propositional literals internally % 59.01/8.61 % (3873281)Refutation not found, incomplete strategy % 59.01/8.61 % (3873281)------------------------------ % 59.01/8.61 % (3873281)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 59.01/8.61 % (3873281)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 59.01/8.61 % (3873281)CaDiCaL version: 2.1.3 % 59.01/8.61 % (3873281)Termination reason: Refutation not found, incomplete strategy % 59.01/8.61 % (3873281)Time elapsed: 0.313 s % 59.01/8.61 % (3873281)Peak memory usage: 25 MB % 59.01/8.61 % (3873281)Instructions burned: 629 (million) % 59.01/8.61 % (3873281)------------------------------ % 59.01/8.61 % (3873281)------------------------------ % 59.01/8.61 % (3873289)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3396976829:i=6324_2987 on theBenchmark for (2987ds/6324Mi) % 81.72/11.88 % (3873289)Cannot represent all propositional literals internally % 81.72/11.88 % (3873289)Refutation not found, incomplete strategy % 81.72/11.88 % (3873289)------------------------------ % 81.72/11.88 % (3873289)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 81.72/11.88 % (3873289)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 81.72/11.88 % (3873289)CaDiCaL version: 2.1.3 % 81.72/11.88 % (3873289)Termination reason: Refutation not found, incomplete strategy % 81.72/11.88 % (3873289)Time elapsed: 0.331 s % 81.72/11.88 % (3873289)Peak memory usage: 25 MB % 81.72/11.88 % (3873289)Instructions burned: 649 (million) % 81.72/11.88 % (3873289)------------------------------ % 81.72/11.88 % (3873289)------------------------------ % 81.72/11.88 % (3873291)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=3885593586:fmbsr=2.30978:i=2174_2984 on theBenchmark for (2984ds/2174Mi) % 81.72/11.88 % TRYING [2] % 81.72/11.88 % (3873287)Instruction limit reached! % 81.72/11.88 % (3873287)------------------------------ % 81.72/11.88 % (3873287)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 81.72/11.88 % (3873287)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 81.72/11.88 % (3873287)CaDiCaL version: 2.1.3 % 81.72/11.88 % (3873287)Termination reason: Instruction limit % 81.72/11.88 % (3873287)Termination phase: Saturation % 81.72/11.88 % (3873287)Time elapsed: 0.474 s % 81.72/11.88 % (3873287)Peak memory usage: 35 MB % 81.72/11.88 % (3873287)Instructions burned: 1473 (million) % 81.72/11.88 % (3873293)ott-2_1_sil=16000:newcnf=on:random_seed=3408577361:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2983 on theBenchmark for (2983ds/869Mi) % 81.72/11.88 % (3873293)Instruction limit reached! % 81.72/11.88 % (3873293)------------------------------ % 81.72/11.88 % (3873293)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 81.72/11.88 % (3873293)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 81.72/11.88 % (3873293)CaDiCaL version: 2.1.3 % 81.72/11.88 % (3873293)Termination reason: Instruction limit % 81.72/11.88 % (3873293)Termination phase: Saturation % 81.72/11.88 % (3873293)Time elapsed: 0.232 s % 81.72/11.88 % (3873293)Peak memory usage: 18 MB % 81.72/11.88 % (3873293)Instructions burned: 869 (million) % 81.72/11.88 % (3873295)ott+10_1_sil=32000:tgt=ground:random_seed=2885151461:i=5114:av=off_2980 on theBenchmark for (2980ds/5114Mi) % 81.72/11.88 % (3873291)Instruction limit reached! % 81.72/11.88 % (3873291)------------------------------ % 81.72/11.88 % (3873291)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 81.72/11.88 % (3873291)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 81.72/11.88 % (3873291)CaDiCaL version: 2.1.3 % 81.72/11.88 % (3873291)Termination reason: Instruction limit % 81.72/11.88 % (3873291)Termination phase: Finite model building preprocessing % 81.72/11.88 % (3873291)Time elapsed: 1.088 s % 81.72/11.88 % (3873291)Peak memory usage: 39 MB % 81.72/11.88 % (3873291)Instructions burned: 2175 (million) % 81.72/11.88 % (3873297)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=1292997106:i=54282_2973 on theBenchmark for (2973ds/54282Mi) % 81.72/11.88 % TRYING [1] % 81.72/11.88 % TRYING [2] % 81.72/11.88 % (3873295)Instruction limit reached! % 81.72/11.88 % (3873295)------------------------------ % 81.72/11.88 % (3873295)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 81.72/11.88 % (3873295)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 81.72/11.88 % (3873295)CaDiCaL version: 2.1.3 % 81.72/11.88 % (3873295)Termination reason: Instruction limit % 81.72/11.88 % (3873295)Termination phase: Saturation % 81.72/11.88 % (3873295)Time elapsed: 1.821 s % 81.72/11.88 % (3873295)Peak memory usage: 68 MB % 81.72/11.88 % (3873295)Instructions burned: 5117 (million) % 81.72/11.88 % (3873299)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=1404832301:i=3512:aac=none_2962 on theBenchmark for (2962ds/3512Mi) % 81.72/11.88 % (3873285)Instruction limit reached! % 81.72/11.88 % (3873285)------------------------------ % 81.72/11.88 % (3873285)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 81.72/11.88 % (3873285)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 81.72/11.88 % (3873285)CaDiCaL version: 2.1.3 % 81.72/11.88 % (3873285)Termination reason: Instruction limit % 81.72/11.88 % (3873285)Termination phase: Saturation % 81.72/11.88 % (3873285)Time elapsed: 3.220 s % 81.72/11.88 % (3873285)Peak memory usage: 52 MB % 81.72/11.88 % (3873285)Instructions burned: 5132 (million) % 143.49/20.59 % (3873301)dis+21_1_sil=32000:sas=cadical:random_seed=2618864113:i=3773:amm=off_2957 on theBenchmark for (2957ds/3773Mi) % 143.49/20.59 % (3873299)Instruction limit reached! % 143.49/20.59 % (3873299)------------------------------ % 143.49/20.59 % (3873299)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 143.49/20.59 % (3873299)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 143.49/20.59 % (3873299)CaDiCaL version: 2.1.3 % 143.49/20.59 % (3873299)Termination reason: Instruction limit % 143.49/20.59 % (3873299)Termination phase: Saturation % 143.49/20.59 % (3873299)Time elapsed: 1.213 s % 143.49/20.59 % (3873299)Peak memory usage: 47 MB % 143.49/20.59 % (3873299)Instructions burned: 3513 (million) % 143.49/20.59 % (3873303)ott+11_1_sil=16000:gs=on:random_seed=3112302801:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2950 on theBenchmark for (2950ds/2251Mi) % 143.49/20.59 % (3873303)Instruction limit reached! % 143.49/20.59 % (3873303)------------------------------ % 143.49/20.59 % (3873303)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 143.49/20.59 % (3873303)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 143.49/20.59 % (3873303)CaDiCaL version: 2.1.3 % 143.49/20.59 % (3873303)Termination reason: Instruction limit % 143.49/20.59 % (3873303)Termination phase: Saturation % 143.49/20.59 % (3873303)Time elapsed: 0.741 s % 143.49/20.59 % (3873303)Peak memory usage: 36 MB % 143.49/20.59 % (3873303)Instructions burned: 2251 (million) % 143.49/20.59 % (3873305)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=3277876587:fmbsr=1.6:i=67534_2942 on theBenchmark for (2942ds/67534Mi) % 143.49/20.59 % (3873305)Cannot represent all propositional literals internally % 143.49/20.59 % (3873305)Refutation not found, incomplete strategy % 143.49/20.59 % (3873305)------------------------------ % 143.49/20.59 % (3873305)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 143.49/20.59 % (3873305)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 143.49/20.59 % (3873305)CaDiCaL version: 2.1.3 % 143.49/20.59 % (3873305)Termination reason: Refutation not found, incomplete strategy % 143.49/20.59 % (3873305)Time elapsed: 0.172 s % 143.49/20.59 % (3873305)Peak memory usage: 23 MB % 143.49/20.59 % (3873305)Instructions burned: 657 (million) % 143.49/20.59 % (3873305)------------------------------ % 143.49/20.59 % (3873305)------------------------------ % 143.49/20.59 % (3873307)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=1534954253:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2940 on theBenchmark for (2940ds/4591Mi) % 143.49/20.59 % (3873301)Instruction limit reached! % 143.49/20.59 % (3873301)------------------------------ % 143.49/20.59 % (3873301)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 143.49/20.59 % (3873301)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 143.49/20.59 % (3873301)CaDiCaL version: 2.1.3 % 143.49/20.59 % (3873301)Termination reason: Instruction limit % 143.49/20.59 % (3873301)Termination phase: Saturation % 143.49/20.59 % (3873301)Time elapsed: 2.249 s % 143.49/20.59 % (3873301)Peak memory usage: 44 MB % 143.49/20.59 % (3873301)Instructions burned: 3773 (million) % 143.49/20.59 % (3873309)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=3272685501:i=29340_2934 on theBenchmark for (2934ds/29340Mi) % 143.49/20.59 % (3873307)Instruction limit reached! % 143.49/20.59 % (3873307)------------------------------ % 143.49/20.59 % (3873307)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 143.49/20.59 % (3873307)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 143.49/20.59 % (3873307)CaDiCaL version: 2.1.3 % 143.49/20.59 % (3873307)Termination reason: Instruction limit % 143.49/20.59 % (3873307)Termination phase: Saturation % 143.49/20.59 % (3873307)Time elapsed: 1.098 s % 143.49/20.59 % (3873307)Peak memory usage: 43 MB % 143.49/20.59 % (3873307)Instructions burned: 4593 (million) % 143.49/20.59 % (3873311)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=3080568402:i=5211_2929 on theBenchmark for (2929ds/5211Mi) % 143.49/20.59 % (3873166)Cannot represent all propositional literals internally % 143.49/20.59 % (3873311)Instruction limit reached! % 143.49/20.59 % (3873311)------------------------------ % 143.49/20.59 % (3873311)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 143.49/20.59 % (3873311)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 143.49/20.59 % (3873311)CaDiCaL version: 2.1.3 % 143.49/20.59 % (3873311)Termination reason: Instruction limit % 171.60/24.57 % (3873311)Termination phase: Saturation % 171.60/24.57 % (3873311)Time elapsed: 1.340 s % 171.60/24.57 % (3873311)Peak memory usage: 44 MB % 171.60/24.57 % (3873311)Instructions burned: 5216 (million) % 171.60/24.57 % (3873313)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=3196687861:i=5497:nm=2_2916 on theBenchmark for (2916ds/5497Mi) % 171.60/24.57 % (3873313)Cannot represent all propositional literals internally % 171.60/24.57 % (3873313)Refutation not found, incomplete strategy % 171.60/24.57 % (3873313)------------------------------ % 171.60/24.57 % (3873313)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 171.60/24.57 % (3873313)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 171.60/24.57 % (3873313)CaDiCaL version: 2.1.3 % 171.60/24.57 % (3873313)Termination reason: Refutation not found, incomplete strategy % 171.60/24.57 % (3873313)Time elapsed: 0.180 s % 171.60/24.57 % (3873313)Peak memory usage: 25 MB % 171.60/24.57 % (3873313)Instructions burned: 649 (million) % 171.60/24.57 % (3873313)------------------------------ % 171.60/24.57 % (3873313)------------------------------ % 171.60/24.57 % (3873315)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=2679808772:fmbsr=2:i=46332_2914 on theBenchmark for (2914ds/46332Mi) % 171.60/24.57 % (3873315)Cannot represent all propositional literals internally % 171.60/24.57 % (3873315)Refutation not found, incomplete strategy % 171.60/24.57 % (3873315)------------------------------ % 171.60/24.57 % (3873315)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 171.60/24.57 % (3873315)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 171.60/24.57 % (3873315)CaDiCaL version: 2.1.3 % 171.60/24.57 % (3873315)Termination reason: Refutation not found, incomplete strategy % 171.60/24.57 % (3873315)Time elapsed: 0.174 s % 171.60/24.57 % (3873315)Peak memory usage: 23 MB % 171.60/24.57 % (3873315)Instructions burned: 657 (million) % 171.60/24.57 % (3873315)------------------------------ % 171.60/24.57 % (3873315)------------------------------ % 171.60/24.57 % (3873317)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=3894010315:i=14071_2912 on theBenchmark for (2912ds/14071Mi) % 171.60/24.57 % (3873166)Refutation not found, incomplete strategy % 171.60/24.57 % (3873166)------------------------------ % 171.60/24.57 % (3873166)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 171.60/24.57 % (3873166)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 171.60/24.57 % (3873166)CaDiCaL version: 2.1.3 % 171.60/24.57 % (3873166)Termination reason: Refutation not found, incomplete strategy % 171.60/24.57 % (3873166)Time elapsed: 8.736 s % 171.60/24.57 % (3873166)Peak memory usage: 981 MB % 171.60/24.57 % (3873166)Instructions burned: 14784 (million) % 171.60/24.57 % (3873166)------------------------------ % 171.60/24.57 % (3873166)------------------------------ % 171.60/24.57 % (3873319)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1672021768:i=22565:add=on:rawr=on_2910 on theBenchmark for (2910ds/22565Mi) % 171.60/24.57 % (3873317)Cannot represent all propositional literals internally % 171.60/24.57 % (3873317)Refutation not found, incomplete strategy % 171.60/24.57 % (3873317)------------------------------ % 171.60/24.57 % (3873317)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 171.60/24.57 % (3873317)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 171.60/24.57 % (3873317)CaDiCaL version: 2.1.3 % 171.60/24.57 % (3873317)Termination reason: Refutation not found, incomplete strategy % 171.60/24.57 % (3873317)Time elapsed: 0.172 s % 171.60/24.57 % (3873317)Peak memory usage: 25 MB % 171.60/24.57 % (3873317)Instructions burned: 630 (million) % 171.60/24.57 % (3873317)------------------------------ % 171.60/24.57 % (3873317)------------------------------ % 171.60/24.57 % (3873321)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=2696103626:i=8173:av=off_2910 on theBenchmark for (2910ds/8173Mi) % 171.60/24.57 % (3873297)Cannot represent all propositional literals internally % 171.60/24.57 % (3873297)Refutation not found, incomplete strategy % 171.60/24.57 % (3873297)------------------------------ % 171.60/24.57 % (3873297)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 171.60/24.57 % (3873297)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 171.60/24.57 % (3873297)CaDiCaL version: 2.1.3 % 171.60/24.57 % (3873297)Termination reason: Refutation not found, incomplete strategy % 171.60/24.57 % (3873297)Time elapsed: 8.944 s % 171.60/24.57 % (3873297)Peak memory usage: 981 MB % 171.60/24.57 % (3873297)Instructions burned: 14784 (million) % 171.60/24.57 % (3873297)------------------------------ % 208.05/29.67 % (3873297)------------------------------ % 208.05/29.67 % (3873323)dis+10_16:1_sil=16000:random_seed=129970633:i=9155:fsr=off_2882 on theBenchmark for (2882ds/9155Mi) % 208.05/29.67 % (3873321)Instruction limit reached! % 208.05/29.67 % (3873321)------------------------------ % 208.05/29.67 % (3873321)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 208.05/29.67 % (3873321)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 208.05/29.67 % (3873321)CaDiCaL version: 2.1.3 % 208.05/29.67 % (3873321)Termination reason: Instruction limit % 208.05/29.67 % (3873321)Termination phase: Saturation % 208.05/29.67 % (3873321)Time elapsed: 3.034 s % 208.05/29.67 % (3873321)Peak memory usage: 108 MB % 208.05/29.67 % (3873321)Instructions burned: 8174 (million) % 208.05/29.67 % (3873325)ott-3_8_sil=64000:random_seed=1287123983:i=20139:bs=on_2879 on theBenchmark for (2879ds/20139Mi) % 208.05/29.67 % (3873279)Instruction limit reached! % 208.05/29.67 % (3873279)------------------------------ % 208.05/29.67 % (3873279)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 208.05/29.67 % (3873279)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 208.05/29.67 % (3873279)CaDiCaL version: 2.1.3 % 208.05/29.67 % (3873279)Termination reason: Instruction limit % 208.05/29.67 % (3873279)Termination phase: Finite model building SAT solving % 208.05/29.67 % (3873279)Time elapsed: 13.716 s % 208.05/29.67 % (3873279)Peak memory usage: 741 MB % 208.05/29.67 % (3873279)Instructions burned: 22063 (million) % 208.05/29.67 % (3873558)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=2787431793:fmbsr=2:i=32576_2853 on theBenchmark for (2853ds/32576Mi) % 208.05/29.67 % (3873558)Cannot represent all propositional literals internally % 208.05/29.67 % (3873558)Refutation not found, incomplete strategy % 208.05/29.67 % (3873558)------------------------------ % 208.05/29.67 % (3873558)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 208.05/29.67 % (3873558)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 208.05/29.67 % (3873558)CaDiCaL version: 2.1.3 % 208.05/29.67 % (3873558)Termination reason: Refutation not found, incomplete strategy % 208.05/29.67 % (3873558)Time elapsed: 0.332 s % 208.05/29.67 % (3873558)Peak memory usage: 25 MB % 208.05/29.67 % (3873558)Instructions burned: 650 (million) % 208.05/29.67 % (3873558)------------------------------ % 208.05/29.67 % (3873558)------------------------------ % 208.05/29.67 % (3873591)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=1432068167:i=11404_2850 on theBenchmark for (2850ds/11404Mi) % 208.05/29.67 % (3873323)Instruction limit reached! % 208.05/29.67 % (3873323)------------------------------ % 208.05/29.67 % (3873323)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 208.05/29.67 % (3873323)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 208.05/29.67 % (3873323)CaDiCaL version: 2.1.3 % 208.05/29.67 % (3873323)Termination reason: Instruction limit % 208.05/29.67 % (3873323)Termination phase: Saturation % 208.05/29.67 % (3873323)Time elapsed: 5.454 s % 208.05/29.67 % (3873323)Peak memory usage: 90 MB % 208.05/29.67 % (3873323)Instructions burned: 9156 (million) % 208.05/29.67 % (3873762)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=169454495:i=14134_2827 on theBenchmark for (2827ds/14134Mi) % 208.05/29.67 % (3873325)Instruction limit reached! % 208.05/29.67 % (3873325)------------------------------ % 208.05/29.67 % (3873325)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 208.05/29.67 % (3873325)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 208.05/29.67 % (3873325)CaDiCaL version: 2.1.3 % 208.05/29.67 % (3873325)Termination reason: Instruction limit % 208.05/29.67 % (3873325)Termination phase: Saturation % 208.05/29.67 % (3873325)Time elapsed: 7.147 s % 208.05/29.67 % (3873325)Peak memory usage: 119 MB % 208.05/29.67 % (3873325)Instructions burned: 20140 (million) % 208.05/29.67 % (3873764)dis+33_16_sil=32000:sac=on:random_seed=796420392:i=15851:nm=0_2808 on theBenchmark for (2808ds/15851Mi) % 208.05/29.67 % (3873309)Instruction limit reached! % 208.05/29.67 % (3873309)------------------------------ % 208.05/29.67 % (3873309)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 208.05/29.67 % (3873309)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 208.05/29.67 % (3873309)CaDiCaL version: 2.1.3 % 208.05/29.67 % (3873309)Termination reason: Instruction limit % 208.05/29.67 % (3873309)Termination phase: Saturation % 208.05/29.67 % (3873309)Time elapsed: 13.727 s % 208.05/29.67 % (3873309)Peak memory usage: 446 MB % 208.05/29.67 % (3873309)Instructions burned: 29340 (million) % 208.05/29.67 % (3873766)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=4024912337:avsq=on:i=17627:add=on:amm=off_2796 on theBenchmark for (2796ds/17627Mi) % 260.77/37.04 % (3873591)Instruction limit reached! % 260.77/37.04 % (3873591)------------------------------ % 260.77/37.04 % (3873591)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 260.77/37.04 % (3873591)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 260.77/37.04 % (3873591)CaDiCaL version: 2.1.3 % 260.77/37.04 % (3873591)Termination reason: Instruction limit % 260.77/37.04 % (3873591)Termination phase: Saturation % 260.77/37.04 % (3873591)Time elapsed: 7.682 s % 260.77/37.04 % (3873591)Peak memory usage: 134 MB % 260.77/37.04 % (3873591)Instructions burned: 11404 (million) % 260.77/37.04 % (3873768)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=2754153796:s2a=on:i=53295_2773 on theBenchmark for (2773ds/53295Mi) % 260.77/37.04 % (3873319)Instruction limit reached! % 260.77/37.04 % (3873319)------------------------------ % 260.77/37.04 % (3873319)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 260.77/37.04 % (3873319)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 260.77/37.04 % (3873319)CaDiCaL version: 2.1.3 % 260.77/37.04 % (3873319)Termination reason: Instruction limit % 260.77/37.04 % (3873319)Termination phase: Saturation % 260.77/37.04 % (3873319)Time elapsed: 14.317 s % 260.77/37.04 % (3873319)Peak memory usage: 439 MB % 260.77/37.04 % (3873319)Instructions burned: 22567 (million) % 260.77/37.04 % (3873770)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=2114445939:i=26857:ins=20_2766 on theBenchmark for (2766ds/26857Mi) % 260.77/37.04 % (3873764)Instruction limit reached! % 260.77/37.04 % (3873764)------------------------------ % 260.77/37.04 % (3873764)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 260.77/37.04 % (3873764)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 260.77/37.04 % (3873764)CaDiCaL version: 2.1.3 % 260.77/37.04 % (3873764)Termination reason: Instruction limit % 260.77/37.04 % (3873764)Termination phase: Saturation % 260.77/37.04 % (3873764)Time elapsed: 4.262 s % 260.77/37.04 % (3873764)Peak memory usage: 169 MB % 260.77/37.04 % (3873764)Instructions burned: 15853 (million) % 260.77/37.04 % (3873772)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=3690368218:i=28120:bs=on:fsr=off_2765 on theBenchmark for (2765ds/28120Mi) % 260.77/37.04 % (3873770)Cannot represent all propositional literals internally % 260.77/37.04 % (3873770)Refutation not found, incomplete strategy % 260.77/37.04 % (3873770)------------------------------ % 260.77/37.04 % (3873770)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 260.77/37.04 % (3873770)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 260.77/37.04 % (3873770)CaDiCaL version: 2.1.3 % 260.77/37.04 % (3873770)Termination reason: Refutation not found, incomplete strategy % 260.77/37.04 % (3873770)Time elapsed: 0.310 s % 260.77/37.04 % (3873770)Peak memory usage: 24 MB % 260.77/37.04 % (3873770)Instructions burned: 629 (million) % 260.77/37.04 % (3873770)------------------------------ % 260.77/37.04 % (3873770)------------------------------ % 260.77/37.04 % (3873774)fmb+10_1_sil=256000:fmbss=7:random_seed=1049607609:fmbsr=1.6:i=182295_2763 on theBenchmark for (2763ds/182295Mi) % 260.77/37.04 % (3873774)Cannot represent all propositional literals internally % 260.77/37.04 % (3873774)Refutation not found, incomplete strategy % 260.77/37.04 % (3873774)------------------------------ % 260.77/37.04 % (3873774)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 260.77/37.04 % (3873774)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 260.77/37.04 % (3873774)CaDiCaL version: 2.1.3 % 260.77/37.04 % (3873774)Termination reason: Refutation not found, incomplete strategy % 260.77/37.04 % (3873774)Time elapsed: 0.310 s % 260.77/37.04 % (3873774)Peak memory usage: 25 MB % 260.77/37.04 % (3873774)Instructions burned: 629 (million) % 260.77/37.04 % (3873774)------------------------------ % 260.77/37.04 % (3873774)------------------------------ % 260.77/37.04 % (3873776)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=864405262:i=44625:gsp=on_2759 on theBenchmark for (2759ds/44625Mi) % 260.77/37.04 % (3873776)Cannot represent all propositional literals internally % 260.77/37.04 % (3873776)Refutation not found, incomplete strategy % 260.77/37.04 % (3873776)------------------------------ % 260.77/37.04 % (3873776)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 260.77/37.04 % (3873776)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 269.05/38.21 % (3873776)CaDiCaL version: 2.1.3 % 269.05/38.21 % (3873776)Termination reason: Refutation not found, incomplete strategy % 269.05/38.21 % (3873776)Time elapsed: 0.314 s % 269.05/38.21 % (3873776)Peak memory usage: 24 MB % 269.05/38.21 % (3873776)Instructions burned: 636 (million) % 269.05/38.21 % (3873776)------------------------------ % 269.05/38.21 % (3873776)------------------------------ % 269.05/38.21 % (3873778)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=3419253513:i=160505_2756 on theBenchmark for (2756ds/160505Mi) % 269.05/38.21 % (3873778)Cannot represent all propositional literals internally % 269.05/38.21 % (3873778)Refutation not found, incomplete strategy % 269.05/38.21 % (3873778)------------------------------ % 269.05/38.21 % (3873778)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 269.05/38.21 % (3873778)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 269.05/38.21 % (3873778)CaDiCaL version: 2.1.3 % 269.05/38.21 % (3873778)Termination reason: Refutation not found, incomplete strategy % 269.05/38.21 % (3873778)Time elapsed: 0.315 s % 269.05/38.21 % (3873778)Peak memory usage: 24 MB % 269.05/38.21 % (3873778)Instructions burned: 629 (million) % 269.05/38.21 % (3873778)------------------------------ % 269.05/38.21 % (3873778)------------------------------ % 269.05/38.21 % (3873780)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=2880946937:fmbsr=1.3:i=225729_2753 on theBenchmark for (2753ds/225729Mi) % 269.05/38.21 % (3873780)Cannot represent all propositional literals internally % 269.05/38.21 % (3873780)Refutation not found, incomplete strategy % 269.05/38.21 % (3873780)------------------------------ % 269.05/38.21 % (3873780)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 269.05/38.21 % (3873780)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 269.05/38.21 % (3873780)CaDiCaL version: 2.1.3 % 269.05/38.21 % (3873780)Termination reason: Refutation not found, incomplete strategy % 269.05/38.21 % (3873780)Time elapsed: 0.316 s % 269.05/38.21 % (3873780)Peak memory usage: 25 MB % 269.05/38.21 % (3873780)Instructions burned: 630 (million) % 269.05/38.21 % (3873780)------------------------------ % 269.05/38.21 % (3873780)------------------------------ % 269.05/38.21 % (3873782)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=2923836544:fmbsr=2:i=185024:ins=7_2749 on theBenchmark for (2749ds/185024Mi) % 269.05/38.21 % (3873782)Cannot represent all propositional literals internally % 269.05/38.21 % (3873782)Refutation not found, incomplete strategy % 269.05/38.21 % (3873782)------------------------------ % 269.05/38.21 % (3873782)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 269.05/38.21 % (3873782)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 269.05/38.21 % (3873782)CaDiCaL version: 2.1.3 % 269.05/38.21 % (3873782)Termination reason: Refutation not found, incomplete strategy % 269.05/38.21 % (3873782)Time elapsed: 0.317 s % 269.05/38.21 % (3873782)Peak memory usage: 25 MB % 269.05/38.21 % (3873782)Instructions burned: 630 (million) % 269.05/38.21 % (3873782)------------------------------ % 269.05/38.21 % (3873782)------------------------------ % 269.05/38.21 % (3873784)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=4003489534:rtra=on_2746 on theBenchmark for (2746ds/0Mi) % 269.05/38.21 % TRYING [1] % 269.05/38.21 % TRYING [2] % 269.05/38.21 % (3873762)Instruction limit reached! % 269.05/38.21 % (3873762)------------------------------ % 269.05/38.21 % (3873762)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 269.05/38.21 % (3873762)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 269.05/38.21 % (3873762)CaDiCaL version: 2.1.3 % 269.05/38.21 % (3873762)Termination reason: Instruction limit % 269.05/38.21 % (3873762)Termination phase: Saturation % 269.05/38.21 % (3873762)Time elapsed: 9.241 s % 269.05/38.21 % (3873762)Peak memory usage: 129 MB % 269.05/38.21 % (3873762)Instructions burned: 14134 (million) % 269.05/38.21 % (3873786)% WARNING: option uhcvi not known. % 269.05/38.21 % (3873786)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3384477777:i=271062:add=off:rtra=on:rawr=on_2734 on theBenchmark for (2734ds/271062Mi) % 269.05/38.21 % (3873766)Instruction limit reached! % 269.05/38.21 % (3873766)------------------------------ % 269.05/38.21 % (3873766)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 269.05/38.21 % (3873766)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 269.05/38.21 % (3873766)CaDiCaL version: 2.1.3 % 269.05/38.21 % (3873766)Termination reason: Instruction limit % 269.05/38.21 % (3873766)Termination phase: Saturation % 269.05/38.21 % (3873766)Time elapsed: 9.087 s % 269.05/38.21 % (3873766)Peak memory usage: 121 MB % 269.05/38.21 % (3873766)Instructions burned: 17627 (million) % 282.82/40.15 % (3874003)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3413161553:i=176048:add=on:rtra=on:rawr=on_2705 on theBenchmark for (2705ds/176048Mi) % 282.82/40.15 % (3873784)Cannot represent all propositional literals internally % 282.82/40.15 % (3873772)Instruction limit reached! % 282.82/40.15 % (3873772)------------------------------ % 282.82/40.15 % (3873772)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 282.82/40.15 % (3873772)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 282.82/40.15 % (3873772)CaDiCaL version: 2.1.3 % 282.82/40.15 % (3873772)Termination reason: Instruction limit % 282.82/40.15 % (3873772)Termination phase: Saturation % 282.82/40.15 % (3873772)Time elapsed: 12.744 s % 282.82/40.15 % (3873772)Peak memory usage: 767 MB % 282.82/40.15 % (3873772)Instructions burned: 28121 (million) % 282.82/40.15 % (3874225)dis+10_1_sil=32000:si=on:sp=arity:random_seed=2989193165:i=206:fgj=on:rtra=on_2637 on theBenchmark for (2637ds/206Mi) % 282.82/40.15 % (3874225)Instruction limit reached! % 282.82/40.15 % (3874225)------------------------------ % 282.82/40.15 % (3874225)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 282.82/40.15 % (3874225)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 282.82/40.15 % (3874225)CaDiCaL version: 2.1.3 % 282.82/40.15 % (3874225)Termination reason: Instruction limit % 282.82/40.15 % (3874225)Termination phase: Saturation % 282.82/40.15 % (3874225)Time elapsed: 0.073 s % 282.82/40.15 % (3874225)Peak memory usage: 17 MB % 282.82/40.15 % (3874225)Instructions burned: 207 (million) % 282.82/40.15 % (3874227)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=124260035:i=232:rtra=on_2636 on theBenchmark for (2636ds/232Mi) % 282.82/40.15 % (3874227)Instruction limit reached! % 282.82/40.15 % (3874227)------------------------------ % 282.82/40.15 % (3874227)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 282.82/40.15 % (3874227)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 282.82/40.15 % (3874227)CaDiCaL version: 2.1.3 % 282.82/40.15 % (3874227)Termination reason: Instruction limit % 282.82/40.15 % (3874227)Termination phase: Saturation % 282.82/40.15 % (3874227)Time elapsed: 0.116 s % 282.82/40.15 % (3874227)Peak memory usage: 17 MB % 282.82/40.15 % (3874227)Instructions burned: 235 (million) % 282.82/40.15 % (3874229)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=257449029:i=262:rtra=on_2634 on theBenchmark for (2634ds/262Mi) % 282.82/40.15 % (3874229)Instruction limit reached! % 282.82/40.15 % (3874229)------------------------------ % 282.82/40.15 % (3874229)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 282.82/40.15 % (3874229)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 282.82/40.15 % (3874229)CaDiCaL version: 2.1.3 % 282.82/40.15 % (3874229)Termination reason: Instruction limit % 282.82/40.15 % (3874229)Termination phase: Saturation % 282.82/40.15 % (3874229)Time elapsed: 0.088 s % 282.82/40.15 % (3874229)Peak memory usage: 19 MB % 282.82/40.15 % (3874229)Instructions burned: 262 (million) % 282.82/40.15 % (3874231)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=737561008:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2633 on theBenchmark for (2633ds/318Mi) % 282.82/40.15 % (3874231)Instruction limit reached! % 282.82/40.15 % (3874231)------------------------------ % 282.82/40.15 % (3874231)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 282.82/40.15 % (3874231)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 282.82/40.15 % (3874231)CaDiCaL version: 2.1.3 % 282.82/40.15 % (3874231)Termination reason: Instruction limit % 282.82/40.15 % (3874231)Termination phase: Saturation % 282.82/40.15 % (3874231)Time elapsed: 0.117 s % 282.82/40.15 % (3874231)Peak memory usage: 19 MB % 282.82/40.15 % (3874231)Instructions burned: 319 (million) % 282.82/40.15 % (3874233)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=3325151746:i=1428:nm=2:rtra=on_2632 on theBenchmark for (2632ds/1428Mi) % 282.82/40.15 % (3873784)Refutation not found, incomplete strategy % 282.82/40.15 % (3873784)------------------------------ % 282.82/40.15 % (3873784)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 282.82/40.15 % (3873784)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 282.82/40.15 % (3873784)CaDiCaL version: 2.1.3 % 282.82/40.15 % (3873784)Termination reason: Refutation not found, incomplete strategy % 282.82/40.15 % (3873784)Time elapsed: 11.416 s % 282.82/40.15 % (3873784)Peak memory usage: 911 MB % 300.29/42.63 % (3873784)Instructions burned: 15141 (million) % 300.29/42.63 % (3873784)------------------------------ % 300.29/42.63 % (3873784)------------------------------ % 300.29/42.63 % (3874235)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=2352372156:i=262:bd=preordered:rtra=on:fsd=on_2630 on theBenchmark for (2630ds/262Mi) % 300.29/42.63 % TRYING [1] % 300.29/42.63 % TRYING [2] % 300.29/42.63 % (3874233)Instruction limit reached! % 300.29/42.63 % (3874233)------------------------------ % 300.29/42.63 % (3874233)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.29/42.63 % (3874233)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.29/42.63 % (3874233)CaDiCaL version: 2.1.3 % 300.29/42.63 % (3874233)Termination reason: Instruction limit % 300.29/42.63 % (3874233)Termination phase: Finite model building constraint generation % 300.29/42.63 % (3874233)Time elapsed: 0.340 s % 300.29/42.63 % (3874233)Peak memory usage: 61 MB % 300.29/42.63 % (3874233)Instructions burned: 1431 (million) % 300.29/42.63 % (3874237)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=1543280944:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2629 on theBenchmark for (2629ds/1368Mi) % 300.29/42.63 % (3874235)Instruction limit reached! % 300.29/42.63 % (3874235)------------------------------ % 300.29/42.63 % (3874235)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.29/42.63 % (3874235)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.29/42.63 % (3874235)CaDiCaL version: 2.1.3 % 300.29/42.63 % (3874235)Termination reason: Instruction limit % 300.29/42.63 % (3874235)Termination phase: Saturation % 300.29/42.63 % (3874235)Time elapsed: 0.179 s % 300.29/42.63 % (3874235)Peak memory usage: 18 MB % 300.29/42.63 % (3874235)Instructions burned: 263 (million) % 300.29/42.63 % (3874239)ott-21_1_sil=16000:si=on:fs=off:random_seed=3025926703:i=360:av=off:fsr=off:rtra=on_2628 on theBenchmark for (2628ds/360Mi) % 300.29/42.63 % (3874239)Instruction limit reached! % 300.29/42.63 % (3874239)------------------------------ % 300.29/42.63 % (3874239)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.29/42.63 % (3874239)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.29/42.64 % (3874239)CaDiCaL version: 2.1.3 % 300.29/42.64 % (3874239)Termination reason: Instruction limit % 300.29/42.64 % (3874239)Termination phase: Saturation % 300.29/42.64 % (3874239)Time elapsed: 0.208 s % 300.29/42.64 % (3874239)Peak memory usage: 18 MB % 300.29/42.64 % (3874239)Instructions burned: 360 (million) % 300.29/42.64 % (3874241)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=142442733:i=954:bd=all:rtra=on_2626 on theBenchmark for (2626ds/954Mi) % 300.29/42.64 % (3874237)Instruction limit reached! % 300.29/42.64 % (3874237)------------------------------ % 300.29/42.64 % (3874237)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.29/42.64 % (3874237)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.29/42.64 % (3874237)CaDiCaL version: 2.1.3 % 300.29/42.64 % (3874237)Termination reason: Instruction limit % 300.29/42.64 % (3874237)Termination phase: Saturation % 300.29/42.64 % (3874237)Time elapsed: 0.392 s % 300.29/42.64 % (3874237)Peak memory usage: 24 MB % 300.29/42.64 % (3874237)Instructions burned: 1370 (million) % 300.29/42.64 % (3874243)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=3091677846:fmbsr=1.3:i=1730:ins=25:rtra=on_2625 on theBenchmark for (2625ds/1730Mi) % 300.29/42.64 % TRYING [1] % 300.29/42.64 % (3874241)Instruction limit reached! % 300.29/42.64 % (3874241)------------------------------ % 300.29/42.64 % (3874241)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.29/42.64 % (3874241)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.29/42.64 % (3874241)CaDiCaL version: 2.1.3 % 300.29/42.64 % (3874241)Termination reason: Instruction limit % 300.29/42.64 % (3874241)Termination phase: Saturation % 300.29/42.64 % (3874241)Time elapsed: 0.603 s % 300.29/42.64 % (3874241)Peak memory usage: 19 MB % 300.29/42.64 % (3874241)Instructions burned: 956 (million) % 300.29/42.64 % (3874243)Instruction limit reached! % 300.29/42.64 % (3874243)------------------------------ % 300.29/42.64 % (3874243)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.29/42.64 % (3874243)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.29/42.64 % (3874243)CaDiCaL version: 2.1.3 % 300.29/42.64 % (3874243)Termination reason: Instruction limit % 300.29/42.64 % (3874243)Termination phase: Finite model building constraint generat % 300.29/42.64 Terminated % 300.29/42.64 % Vampire exiting % 300.29/42.64 Terminated %------------------------------------------------------------------------------