%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWV895-1 : TPTP v9.3.1. Released v4.1.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % Computer : n010.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:26:37 PM UTC 2026 % Result : Timeout 300.40s 42.63s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : SWV895-1 : TPTP v9.3.1. Released v4.1.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.06/0.17 % Computer : n010.cluster.edu % 0.06/0.17 % Model : x86_64 x86_64 % 0.06/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.06/0.17 % Memory : 8046.5625MB % 0.06/0.17 % OS : Linux 6.8.0-71-generic % 0.06/0.17 % CPULimit : 300 % 0.06/0.17 % WCLimit : 300 % 0.06/0.17 % DateTime : Mon Sep 28 12:52:17 UTC 2026 % 0.06/0.17 % CPUTime : % 0.06/0.17 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.06/0.20 Running first-order model finding % 0.06/0.20 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 % 7.31/1.35 % (1900459)Will run a generic schedule for satisfiability detection. % 7.31/1.35 % (1900468)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1852127912:i=116_2999 on theBenchmark for (2999ds/116Mi) % 7.31/1.35 % (1900465)% WARNING: option uhcvi not known. % 7.31/1.35 % (1900464)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=342955676_2999 on theBenchmark for (2999ds/0Mi) % 7.31/1.35 % (1900465)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=659128520:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 7.31/1.35 % (1900466)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2357242115:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 7.31/1.35 % (1900467)dis+10_1_sil=32000:sp=arity:random_seed=547431444:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 7.31/1.35 % (1900469)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3319233181:i=131_2999 on theBenchmark for (2999ds/131Mi) % 7.31/1.35 % (1900470)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=55546472:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 7.31/1.35 % (1900468)Instruction limit reached! % 7.31/1.35 % (1900468)------------------------------ % 7.31/1.35 % (1900468)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.31/1.35 % (1900468)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.31/1.35 % (1900468)CaDiCaL version: 2.1.3 % 7.31/1.35 % (1900468)Termination reason: Instruction limit % 7.31/1.35 % (1900468)Termination phase: Saturation % 7.31/1.35 % (1900468)Time elapsed: 0.037 s % 7.31/1.35 % (1900468)Peak memory usage: 13 MB % 7.31/1.35 % (1900468)Instructions burned: 116 (million) % 7.31/1.35 % (1900478)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2039037940:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 7.31/1.35 % (1900467)Instruction limit reached! % 7.31/1.35 % (1900467)------------------------------ % 7.31/1.35 % (1900467)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.31/1.35 % (1900467)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.31/1.35 % (1900467)CaDiCaL version: 2.1.3 % 7.31/1.35 % (1900467)Termination reason: Instruction limit % 7.31/1.35 % (1900467)Termination phase: Saturation % 7.31/1.35 % (1900467)Time elapsed: 0.059 s % 7.31/1.35 % (1900467)Peak memory usage: 12 MB % 7.31/1.35 % (1900467)Instructions burned: 103 (million) % 7.31/1.35 % (1900480)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3884437737:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi) % 7.31/1.35 % (1900469)Instruction limit reached! % 7.31/1.35 % (1900469)------------------------------ % 7.31/1.35 % (1900469)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.31/1.35 % (1900469)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.31/1.35 % (1900469)CaDiCaL version: 2.1.3 % 7.31/1.35 % (1900469)Termination reason: Instruction limit % 7.31/1.35 % (1900469)Termination phase: Saturation % 7.31/1.35 % (1900469)Time elapsed: 0.081 s % 7.31/1.35 % (1900469)Peak memory usage: 13 MB % 7.31/1.35 % (1900469)Instructions burned: 132 (million) % 7.31/1.35 % (1900470)Instruction limit reached! % 7.31/1.35 % (1900470)------------------------------ % 7.31/1.35 % (1900470)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.31/1.35 % (1900470)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.31/1.35 % (1900470)CaDiCaL version: 2.1.3 % 7.31/1.35 % (1900470)Termination reason: Instruction limit % 7.31/1.35 % (1900470)Termination phase: Saturation % 7.31/1.35 % (1900470)Time elapsed: 0.088 s % 7.31/1.35 % (1900470)Peak memory usage: 13 MB % 7.31/1.35 % (1900470)Instructions burned: 159 (million) % 7.31/1.35 % (1900482)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=4285244865:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi) % 7.31/1.35 % (1900483)ott-21_1_sil=16000:fs=off:random_seed=1053303846:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 7.31/1.35 % (1900480)Instruction limit reached! % 7.31/1.35 % (1900480)------------------------------ % 7.31/1.35 % (1900480)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.31/1.35 % (1900480)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.31/1.35 % (1900480)CaDiCaL version: 2.1.3 % 26.95/4.09 % (1900480)Termination reason: Instruction limit % 26.95/4.09 % (1900480)Termination phase: Saturation % 26.95/4.09 % (1900480)Time elapsed: 0.044 s % 26.95/4.09 % (1900480)Peak memory usage: 14 MB % 26.95/4.09 % (1900480)Instructions burned: 135 (million) % 26.95/4.09 % (1900486)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2629864099:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 26.95/4.09 % TRYING [1] % 26.95/4.09 % TRYING [2] % 26.95/4.09 % (1900483)Instruction limit reached! % 26.95/4.09 % (1900483)------------------------------ % 26.95/4.09 % (1900483)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 26.95/4.09 % (1900483)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.95/4.09 % (1900483)CaDiCaL version: 2.1.3 % 26.95/4.09 % (1900483)Termination reason: Instruction limit % 26.95/4.09 % (1900483)Termination phase: Saturation % 26.95/4.09 % (1900483)Time elapsed: 0.102 s % 26.95/4.09 % (1900483)Peak memory usage: 13 MB % 26.95/4.09 % (1900483)Instructions burned: 180 (million) % 26.95/4.09 % (1900488)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2293954917:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi) % 26.95/4.09 % TRYING [1] % 26.95/4.09 % TRYING [2] % 26.95/4.09 % (1900486)Instruction limit reached! % 26.95/4.09 % (1900486)------------------------------ % 26.95/4.09 % (1900486)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 26.95/4.09 % (1900486)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.95/4.09 % (1900486)CaDiCaL version: 2.1.3 % 26.95/4.09 % (1900486)Termination reason: Instruction limit % 26.95/4.09 % (1900486)Termination phase: Saturation % 26.95/4.09 % (1900486)Time elapsed: 0.167 s % 26.95/4.09 % (1900486)Peak memory usage: 14 MB % 26.95/4.09 % (1900486)Instructions burned: 481 (million) % 26.95/4.09 % (1900490)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2502645388:i=1179_2996 on theBenchmark for (2996ds/1179Mi) % 26.95/4.09 % TRYING [3] % 26.95/4.09 % (1900478)Instruction limit reached! % 26.95/4.09 % (1900478)------------------------------ % 26.95/4.09 % (1900478)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 26.95/4.09 % (1900478)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.95/4.09 % (1900478)CaDiCaL version: 2.1.3 % 26.95/4.09 % (1900478)Termination reason: Instruction limit % 26.95/4.09 % (1900478)Termination phase: Finite model building constraint generation % 26.95/4.09 % (1900478)Time elapsed: 0.310 s % 26.95/4.09 % (1900478)Peak memory usage: 23 MB % 26.95/4.09 % (1900478)Instructions burned: 714 (million) % 26.95/4.09 % (1900492)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1987641078:i=889:ins=1_2995 on theBenchmark for (2995ds/889Mi) % 26.95/4.09 % TRYING [1] % 26.95/4.09 % TRYING [2] % 26.95/4.09 % (1900482)Instruction limit reached! % 26.95/4.09 % (1900482)------------------------------ % 26.95/4.09 % (1900482)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 26.95/4.09 % (1900482)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.95/4.09 % (1900482)CaDiCaL version: 2.1.3 % 26.95/4.09 % (1900482)Termination reason: Instruction limit % 26.95/4.09 % (1900482)Termination phase: Saturation % 26.95/4.09 % (1900482)Time elapsed: 0.372 s % 26.95/4.09 % (1900482)Peak memory usage: 16 MB % 26.95/4.09 % (1900482)Instructions burned: 684 (million) % 26.95/4.09 % (1900494)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=1433779407: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) % 26.95/4.09 % (1900492)Cannot represent all propositional literals internally % 26.95/4.09 % (1900492)Refutation not found, incomplete strategy % 26.95/4.09 % (1900492)------------------------------ % 26.95/4.09 % (1900492)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 26.95/4.09 % (1900492)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.95/4.09 % (1900492)CaDiCaL version: 2.1.3 % 26.95/4.09 % (1900492)Termination reason: Refutation not found, incomplete strategy % 26.95/4.09 % (1900492)Time elapsed: 0.190 s % 26.95/4.09 % (1900492)Peak memory usage: 15 MB % 26.95/4.09 % (1900492)Instructions burned: 374 (million) % 26.95/4.09 % (1900492)------------------------------ % 26.95/4.09 % (1900492)------------------------------ % 26.95/4.09 % (1900496)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3246996919:i=879:kws=inv_precedence:fsr=off_2993 on theBenchmark for (2993ds/879Mi) % 26.95/4.09 % (1900488)Instruction limit reached! % 54.40/7.96 % (1900488)------------------------------ % 54.40/7.96 % (1900488)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 54.40/7.96 % (1900488)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 54.40/7.96 % (1900488)CaDiCaL version: 2.1.3 % 54.40/7.96 % (1900488)Termination reason: Instruction limit % 54.40/7.96 % (1900488)Termination phase: Finite model building SAT solving % 54.40/7.96 % (1900488)Time elapsed: 0.398 s % 54.40/7.96 % (1900488)Peak memory usage: 33 MB % 54.40/7.96 % (1900488)Instructions burned: 865 (million) % 54.40/7.96 % (1900498)fmb+10_1_sil=64000:random_seed=4008666039:i=22061:nm=2:gsp=on_2993 on theBenchmark for (2993ds/22061Mi) % 54.40/7.96 % (1900490)Instruction limit reached! % 54.40/7.96 % (1900490)------------------------------ % 54.40/7.96 % (1900490)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 54.40/7.96 % (1900490)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 54.40/7.96 % (1900490)CaDiCaL version: 2.1.3 % 54.40/7.96 % (1900490)Termination reason: Instruction limit % 54.40/7.96 % (1900490)Termination phase: Saturation % 54.40/7.96 % (1900490)Time elapsed: 0.371 s % 54.40/7.96 % (1900490)Peak memory usage: 26 MB % 54.40/7.96 % (1900490)Instructions burned: 1180 (million) % 54.40/7.96 % (1900500)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=294237388:i=9515:nm=5_2992 on theBenchmark for (2992ds/9515Mi) % 54.40/7.96 % (1900500)Cannot represent all propositional literals internally % 54.40/7.96 % (1900500)Refutation not found, incomplete strategy % 54.40/7.96 % (1900500)------------------------------ % 54.40/7.96 % (1900500)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 54.40/7.96 % (1900500)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 54.40/7.96 % (1900500)CaDiCaL version: 2.1.3 % 54.40/7.96 % (1900500)Termination reason: Refutation not found, incomplete strategy % 54.40/7.96 % (1900500)Time elapsed: 0.100 s % 54.40/7.96 % (1900500)Peak memory usage: 15 MB % 54.40/7.96 % (1900500)Instructions burned: 373 (million) % 54.40/7.96 % (1900500)------------------------------ % 54.40/7.96 % (1900500)------------------------------ % 54.40/7.96 % (1900502)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3575809876:fmbsr=1.7:i=920_2991 on theBenchmark for (2991ds/920Mi) % 54.40/7.96 % TRYING [1] % 54.40/7.96 % TRYING [2] % 54.40/7.96 % (1900494)Instruction limit reached! % 54.40/7.96 % (1900494)------------------------------ % 54.40/7.96 % (1900494)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 54.40/7.96 % (1900494)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 54.40/7.96 % (1900494)CaDiCaL version: 2.1.3 % 54.40/7.96 % (1900494)Termination reason: Instruction limit % 54.40/7.96 % (1900494)Termination phase: Saturation % 54.40/7.96 % (1900494)Time elapsed: 0.387 s % 54.40/7.96 % (1900494)Peak memory usage: 23 MB % 54.40/7.96 % (1900494)Instructions burned: 692 (million) % 54.40/7.96 % (1900504)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=3000320932:i=5131_2990 on theBenchmark for (2990ds/5131Mi) % 54.40/7.96 % (1900502)Cannot represent all propositional literals internally % 54.40/7.96 % (1900502)Refutation not found, incomplete strategy % 54.40/7.96 % (1900502)------------------------------ % 54.40/7.96 % (1900502)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 54.40/7.96 % (1900502)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 54.40/7.96 % (1900502)CaDiCaL version: 2.1.3 % 54.40/7.96 % (1900502)Termination reason: Refutation not found, incomplete strategy % 54.40/7.96 % (1900502)Time elapsed: 0.101 s % 54.40/7.96 % (1900502)Peak memory usage: 15 MB % 54.40/7.96 % (1900502)Instructions burned: 373 (million) % 54.40/7.96 % (1900502)------------------------------ % 54.40/7.96 % (1900502)------------------------------ % 54.40/7.96 % (1900506)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2084089804:i=1472:ins=7:fdi=8:gsp=on_2990 on theBenchmark for (2990ds/1472Mi) % 54.40/7.96 % (1900496)Instruction limit reached! % 54.40/7.96 % (1900496)------------------------------ % 54.40/7.96 % (1900496)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 54.40/7.96 % (1900496)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 54.40/7.96 % (1900496)CaDiCaL version: 2.1.3 % 54.40/7.96 % (1900496)Termination reason: Instruction limit % 54.40/7.96 % (1900496)Termination phase: Saturation % 54.40/7.96 % (1900496)Time elapsed: 0.489 s % 54.40/7.96 % (1900496)Peak memory usage: 19 MB % 54.40/7.96 % (1900496)Instructions burned: 880 (million) % 111.15/15.90 % (1900508)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=2856786441:i=6324_2988 on theBenchmark for (2988ds/6324Mi) % 111.15/15.90 % (1900508)Cannot represent all propositional literals internally % 111.15/15.90 % (1900508)Refutation not found, incomplete strategy % 111.15/15.90 % (1900508)------------------------------ % 111.15/15.90 % (1900508)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 111.15/15.90 % (1900508)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 111.15/15.90 % (1900508)CaDiCaL version: 2.1.3 % 111.15/15.90 % (1900508)Termination reason: Refutation not found, incomplete strategy % 111.15/15.90 % (1900508)Time elapsed: 0.198 s % 111.15/15.90 % (1900508)Peak memory usage: 15 MB % 111.15/15.90 % (1900508)Instructions burned: 379 (million) % 111.15/15.90 % (1900508)------------------------------ % 111.15/15.90 % (1900508)------------------------------ % 111.15/15.90 % (1900510)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1413826763:fmbsr=2.30978:i=2174_2986 on theBenchmark for (2986ds/2174Mi) % 111.15/15.90 % (1900506)Instruction limit reached! % 111.15/15.90 % (1900506)------------------------------ % 111.15/15.90 % (1900506)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 111.15/15.90 % (1900506)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 111.15/15.90 % (1900506)CaDiCaL version: 2.1.3 % 111.15/15.90 % (1900506)Termination reason: Instruction limit % 111.15/15.90 % (1900506)Termination phase: Saturation % 111.15/15.90 % (1900506)Time elapsed: 0.461 s % 111.15/15.90 % (1900506)Peak memory usage: 34 MB % 111.15/15.90 % (1900506)Instructions burned: 1473 (million) % 111.15/15.90 % (1900512)ott-2_1_sil=16000:newcnf=on:random_seed=1695302104:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2985 on theBenchmark for (2985ds/869Mi) % 111.15/15.90 % (1900512)Instruction limit reached! % 111.15/15.90 % (1900512)------------------------------ % 111.15/15.90 % (1900512)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 111.15/15.90 % (1900512)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 111.15/15.90 % (1900512)CaDiCaL version: 2.1.3 % 111.15/15.90 % (1900512)Termination reason: Instruction limit % 111.15/15.90 % (1900512)Termination phase: Saturation % 111.15/15.90 % (1900512)Time elapsed: 0.236 s % 111.15/15.90 % (1900512)Peak memory usage: 14 MB % 111.15/15.90 % (1900512)Instructions burned: 869 (million) % 111.15/15.90 % (1900514)ott+10_1_sil=32000:tgt=ground:random_seed=1264375466:i=5114:av=off_2983 on theBenchmark for (2983ds/5114Mi) % 111.15/15.90 % TRYING [3] % 111.15/15.90 % (1900510)Cannot represent all propositional literals internally % 111.15/15.90 % (1900510)Refutation not found, incomplete strategy % 111.15/15.90 % (1900510)------------------------------ % 111.15/15.90 % (1900510)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 111.15/15.90 % (1900510)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 111.15/15.90 % (1900510)CaDiCaL version: 2.1.3 % 111.15/15.90 % (1900510)Termination reason: Refutation not found, incomplete strategy % 111.15/15.90 % (1900510)Time elapsed: 0.831 s % 111.15/15.90 % (1900510)Peak memory usage: 23 MB % 111.15/15.90 % (1900510)Instructions burned: 1638 (million) % 111.15/15.90 % (1900510)------------------------------ % 111.15/15.90 % (1900510)------------------------------ % 111.15/15.90 % (1900516)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=3814984871:i=54282_2977 on theBenchmark for (2977ds/54282Mi) % 111.15/15.90 % TRYING [1] % 111.15/15.90 % TRYING [2] % 111.15/15.90 % TRYING [3] % 111.15/15.90 % (1900514)Instruction limit reached! % 111.15/15.90 % (1900514)------------------------------ % 111.15/15.90 % (1900514)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 111.15/15.90 % (1900514)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 111.15/15.90 % (1900514)CaDiCaL version: 2.1.3 % 111.15/15.90 % (1900514)Termination reason: Instruction limit % 111.15/15.90 % (1900514)Termination phase: Saturation % 111.15/15.90 % (1900514)Time elapsed: 1.682 s % 111.15/15.90 % (1900514)Peak memory usage: 44 MB % 111.15/15.90 % (1900514)Instructions burned: 5116 (million) % 111.15/15.90 % (1900518)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3024944087:i=3512:aac=none_2966 on theBenchmark for (2966ds/3512Mi) % 111.15/15.90 % (1900504)Instruction limit reached! % 111.15/15.90 % (1900504)------------------------------ % 111.15/15.90 % (1900504)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 111.15/15.90 % (1900504)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 111.15/15.90 % (1900504)CaDiCaL version: 2.1.3 % 111.15/15.90 % (1900504)Termination reason: Instruction limit % 143.77/23.58 % (1900504)Termination phase: Saturation % 143.77/23.58 % (1900504)Time elapsed: 2.927 s % 143.77/23.58 % (1900504)Peak memory usage: 42 MB % 143.77/23.58 % (1900504)Instructions burned: 5132 (million) % 143.77/23.58 % (1900520)dis+21_1_sil=32000:sas=cadical:random_seed=4012433331:i=3773:amm=off_2961 on theBenchmark for (2961ds/3773Mi) % 143.77/23.58 % (1900518)Instruction limit reached! % 143.77/23.58 % (1900518)------------------------------ % 143.77/23.58 % (1900518)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 143.77/23.58 % (1900518)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 143.77/23.58 % (1900518)CaDiCaL version: 2.1.3 % 143.77/23.58 % (1900518)Termination reason: Instruction limit % 143.77/23.58 % (1900518)Termination phase: Saturation % 143.77/23.58 % (1900518)Time elapsed: 1.069 s % 143.77/23.58 % (1900518)Peak memory usage: 35 MB % 143.77/23.58 % (1900518)Instructions burned: 3513 (million) % 143.77/23.58 % (1900522)ott+11_1_sil=16000:gs=on:random_seed=2720863563:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2955 on theBenchmark for (2955ds/2251Mi) % 143.77/23.58 % (1900522)Instruction limit reached! % 143.77/23.58 % (1900522)------------------------------ % 143.77/23.58 % (1900522)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 143.77/23.58 % (1900522)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 143.77/23.58 % (1900522)CaDiCaL version: 2.1.3 % 143.77/23.58 % (1900522)Termination reason: Instruction limit % 143.77/23.58 % (1900522)Termination phase: Saturation % 143.77/23.58 % (1900522)Time elapsed: 0.726 s % 143.77/23.58 % (1900522)Peak memory usage: 32 MB % 143.77/23.58 % (1900522)Instructions burned: 2252 (million) % 143.77/23.58 % (1900524)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=4127229775:fmbsr=1.6:i=67534_2947 on theBenchmark for (2947ds/67534Mi) % 143.77/23.58 % (1900524)Cannot represent all propositional literals internally % 143.77/23.58 % (1900524)Refutation not found, incomplete strategy % 143.77/23.58 % (1900524)------------------------------ % 143.77/23.58 % (1900524)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 143.77/23.58 % (1900524)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 143.77/23.58 % (1900524)CaDiCaL version: 2.1.3 % 143.77/23.58 % (1900524)Termination reason: Refutation not found, incomplete strategy % 143.77/23.58 % (1900524)Time elapsed: 0.103 s % 143.77/23.58 % (1900524)Peak memory usage: 15 MB % 143.77/23.58 % (1900524)Instructions burned: 388 (million) % 143.77/23.58 % (1900524)------------------------------ % 143.77/23.58 % (1900524)------------------------------ % 143.77/23.58 % (1900526)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=41105669:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2946 on theBenchmark for (2946ds/4591Mi) % 143.77/23.58 % (1900520)Instruction limit reached! % 143.77/23.58 % (1900520)------------------------------ % 143.77/23.58 % (1900520)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 143.77/23.58 % (1900520)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 143.77/23.58 % (1900520)CaDiCaL version: 2.1.3 % 143.77/23.58 % (1900520)Termination reason: Instruction limit % 143.77/23.58 % (1900520)Termination phase: Saturation % 143.77/23.58 % (1900520)Time elapsed: 2.187 s % 143.77/23.58 % (1900520)Peak memory usage: 36 MB % 143.77/23.58 % (1900520)Instructions burned: 3774 (million) % 143.77/23.58 % (1900528)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=4122447541:i=29340_2939 on theBenchmark for (2939ds/29340Mi) % 143.77/23.58 % (1900526)Instruction limit reached! % 143.77/23.58 % (1900526)------------------------------ % 143.77/23.58 % (1900526)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 143.77/23.58 % (1900526)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 143.77/23.58 % (1900526)CaDiCaL version: 2.1.3 % 143.77/23.58 % (1900526)Termination reason: Instruction limit % 143.77/23.58 % (1900526)Termination phase: Saturation % 143.77/23.58 % (1900526)Time elapsed: 0.900 s % 143.77/23.58 % (1900526)Peak memory usage: 25 MB % 143.77/23.58 % (1900526)Instructions burned: 4591 (million) % 143.77/23.58 % (1900530)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=1764802792:i=5211_2937 on theBenchmark for (2937ds/5211Mi) % 143.77/23.58 % (1900530)Instruction limit reached! % 143.77/23.58 % (1900530)------------------------------ % 143.77/23.58 % (1900530)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 143.77/23.58 % (1900530)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 208.84/29.71 % (1900530)CaDiCaL version: 2.1.3 % 208.84/29.71 % (1900530)Termination reason: Instruction limit % 208.84/29.71 % (1900530)Termination phase: Saturation % 208.84/29.71 % (1900530)Time elapsed: 1.495 s % 208.84/29.71 % (1900530)Peak memory usage: 49 MB % 208.84/29.71 % (1900530)Instructions burned: 5212 (million) % 208.84/29.71 % (1900532)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=3815175564:i=5497:nm=2_2922 on theBenchmark for (2922ds/5497Mi) % 208.84/29.71 % (1900532)Cannot represent all propositional literals internally % 208.84/29.71 % (1900532)Refutation not found, incomplete strategy % 208.84/29.71 % (1900532)------------------------------ % 208.84/29.71 % (1900532)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 208.84/29.71 % (1900532)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 208.84/29.71 % (1900532)CaDiCaL version: 2.1.3 % 208.84/29.71 % (1900532)Termination reason: Refutation not found, incomplete strategy % 208.84/29.71 % (1900532)Time elapsed: 0.102 s % 208.84/29.71 % (1900532)Peak memory usage: 15 MB % 208.84/29.71 % (1900532)Instructions burned: 379 (million) % 208.84/29.71 % (1900532)------------------------------ % 208.84/29.71 % (1900532)------------------------------ % 208.84/29.71 % (1900534)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=583821972:fmbsr=2:i=46332_2921 on theBenchmark for (2921ds/46332Mi) % 208.84/29.71 % (1900534)Cannot represent all propositional literals internally % 208.84/29.71 % (1900534)Refutation not found, incomplete strategy % 208.84/29.71 % (1900534)------------------------------ % 208.84/29.71 % (1900534)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 208.84/29.71 % (1900534)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 208.84/29.71 % (1900534)CaDiCaL version: 2.1.3 % 208.84/29.71 % (1900534)Termination reason: Refutation not found, incomplete strategy % 208.84/29.71 % (1900534)Time elapsed: 0.103 s % 208.84/29.71 % (1900534)Peak memory usage: 15 MB % 208.84/29.71 % (1900534)Instructions burned: 388 (million) % 208.84/29.71 % (1900534)------------------------------ % 208.84/29.71 % (1900534)------------------------------ % 208.84/29.71 % (1900536)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=1957352614:i=14071_2920 on theBenchmark for (2920ds/14071Mi) % 208.84/29.71 % (1900536)Cannot represent all propositional literals internally % 208.84/29.71 % (1900536)Refutation not found, incomplete strategy % 208.84/29.71 % (1900536)------------------------------ % 208.84/29.71 % (1900536)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 208.84/29.71 % (1900536)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 208.84/29.71 % (1900536)CaDiCaL version: 2.1.3 % 208.84/29.71 % (1900536)Termination reason: Refutation not found, incomplete strategy % 208.84/29.71 % (1900536)Time elapsed: 0.101 s % 208.84/29.71 % (1900536)Peak memory usage: 15 MB % 208.84/29.71 % (1900536)Instructions burned: 374 (million) % 208.84/29.71 % (1900536)------------------------------ % 208.84/29.71 % (1900536)------------------------------ % 208.84/29.71 % (1900538)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2766362883:i=22565:add=on:rawr=on_2919 on theBenchmark for (2919ds/22565Mi) % 208.84/29.71 % (1900498)Instruction limit reached! % 208.84/29.71 % (1900498)------------------------------ % 208.84/29.71 % (1900498)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 208.84/29.71 % (1900498)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 208.84/29.71 % (1900498)CaDiCaL version: 2.1.3 % 208.84/29.71 % (1900498)Termination reason: Instruction limit % 208.84/29.71 % (1900498)Termination phase: Finite model building constraint generation % 208.84/29.71 % (1900498)Time elapsed: 9.533 s % 208.84/29.71 % (1900498)Peak memory usage: 1011 MB % 208.84/29.71 % (1900498)Instructions burned: 22063 (million) % 208.84/29.71 % (1900540)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=963376310:i=8173:av=off_2896 on theBenchmark for (2896ds/8173Mi) % 208.84/29.71 % TRYING [4] % 208.84/29.71 % (1900540)Instruction limit reached! % 208.84/29.71 % (1900540)------------------------------ % 208.84/29.71 % (1900540)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 208.84/29.71 % (1900540)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 208.84/29.71 % (1900540)CaDiCaL version: 2.1.3 % 208.84/29.71 % (1900540)Termination reason: Instruction limit % 208.84/29.71 % (1900540)Termination phase: Saturation % 208.84/29.71 % (1900540)Time elapsed: 5.252 s % 208.84/29.71 % (1900540)Peak memory usage: 99 MB % 208.84/29.71 % (1900540)Instructions burned: 8173 (million) % 208.84/29.71 % (1900542)dis+10_16:1_sil=16000:random_seed=4073488568:i=9155:fsr=off_2843 on theBenchmark for (2843ds/9155Mi) % 259.40/38.61 % (1900538)Instruction limit reached! % 259.40/38.61 % (1900538)------------------------------ % 259.40/38.61 % (1900538)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 259.40/38.61 % (1900538)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 259.40/38.61 % (1900538)CaDiCaL version: 2.1.3 % 259.40/38.61 % (1900538)Termination reason: Instruction limit % 259.40/38.61 % (1900538)Termination phase: Saturation % 259.40/38.61 % (1900538)Time elapsed: 8.097 s % 259.40/38.61 % (1900538)Peak memory usage: 205 MB % 259.40/38.61 % (1900538)Instructions burned: 22566 (million) % 259.40/38.61 % (1900544)ott-3_8_sil=64000:random_seed=1518009597:i=20139:bs=on_2837 on theBenchmark for (2837ds/20139Mi) % 259.40/38.61 % TRYING [4] % 259.40/38.61 % (1900544)Instruction limit reached! % 259.40/38.61 % (1900544)------------------------------ % 259.40/38.61 % (1900544)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 259.40/38.61 % (1900544)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 259.40/38.61 % (1900544)CaDiCaL version: 2.1.3 % 259.40/38.61 % (1900544)Termination reason: Instruction limit % 259.40/38.61 % (1900544)Termination phase: Saturation % 259.40/38.61 % (1900544)Time elapsed: 4.414 s % 259.40/38.61 % (1900544)Peak memory usage: 20 MB % 259.40/38.61 % (1900544)Instructions burned: 20142 (million) % 259.40/38.61 % (1900546)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=2707993690:fmbsr=2:i=32576_2793 on theBenchmark for (2793ds/32576Mi) % 259.40/38.61 % (1900528)Instruction limit reached! % 259.40/38.61 % (1900528)------------------------------ % 259.40/38.61 % (1900528)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 259.40/38.61 % (1900528)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 259.40/38.61 % (1900528)CaDiCaL version: 2.1.3 % 259.40/38.61 % (1900528)Termination reason: Instruction limit % 259.40/38.61 % (1900528)Termination phase: Saturation % 259.40/38.61 % (1900528)Time elapsed: 14.609 s % 259.40/38.61 % (1900528)Peak memory usage: 310 MB % 259.40/38.61 % (1900528)Instructions burned: 29340 (million) % 259.40/38.61 % (1900546)Cannot represent all propositional literals internally % 259.40/38.61 % (1900546)Refutation not found, incomplete strategy % 259.40/38.61 % (1900546)------------------------------ % 259.40/38.61 % (1900546)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 259.40/38.61 % (1900546)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 259.40/38.61 % (1900546)CaDiCaL version: 2.1.3 % 259.40/38.61 % (1900546)Termination reason: Refutation not found, incomplete strategy % 259.40/38.61 % (1900546)Time elapsed: 0.102 s % 259.40/38.61 % (1900546)Peak memory usage: 15 MB % 259.40/38.61 % (1900546)Instructions burned: 380 (million) % 259.40/38.61 % (1900546)------------------------------ % 259.40/38.61 % (1900546)------------------------------ % 259.40/38.61 % (1900549)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=1087530472:i=14134_2792 on theBenchmark for (2792ds/14134Mi) % 259.40/38.61 % (1900548)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=2474981693:i=11404_2792 on theBenchmark for (2792ds/11404Mi) % 259.40/38.61 % (1900542)Instruction limit reached! % 259.40/38.61 % (1900542)------------------------------ % 259.40/38.61 % (1900542)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 259.40/38.61 % (1900542)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 259.40/38.61 % (1900542)CaDiCaL version: 2.1.3 % 259.40/38.61 % (1900542)Termination reason: Instruction limit % 259.40/38.61 % (1900542)Termination phase: Saturation % 259.40/38.61 % (1900542)Time elapsed: 5.100 s % 259.40/38.61 % (1900542)Peak memory usage: 63 MB % 259.40/38.61 % (1900542)Instructions burned: 9156 (million) % 259.40/38.61 % (1900552)dis+33_16_sil=32000:sac=on:random_seed=5685335:i=15851:nm=0_2792 on theBenchmark for (2792ds/15851Mi) % 259.40/38.61 % (1900516)Instruction limit reached! % 259.40/38.61 % (1900516)------------------------------ % 259.40/38.61 % (1900516)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 259.40/38.61 % (1900516)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 259.40/38.61 % (1900516)CaDiCaL version: 2.1.3 % 259.40/38.61 % (1900516)Termination reason: Instruction limit % 259.40/38.61 % (1900516)Termination phase: Finite model building constraint generation % 259.40/38.61 % (1900516)Time elapsed: 20.895 s % 259.40/38.61 % (1900516)Peak memory usage: 1710 MB % 259.40/38.61 % (1900516)Instructions burned: 54284 (million) % 259.40/38.61 % (1900554)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=3905811327:avsq=on:i=17627:add=on:amm=off_2766 on theBenchmark for (2766ds/17627Mi) % 300.40/42.63 % (1900549)Instruction limit reached! % 300.40/42.63 % (1900549)------------------------------ % 300.40/42.63 % (1900549)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.40/42.63 % (1900549)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.40/42.63 % (1900549)CaDiCaL version: 2.1.3 % 300.40/42.63 % (1900549)Termination reason: Instruction limit % 300.40/42.63 % (1900549)Termination phase: Saturation % 300.40/42.63 % (1900549)Time elapsed: 5.039 s % 300.40/42.63 % (1900549)Peak memory usage: 112 MB % 300.40/42.63 % (1900549)Instructions burned: 14136 (million) % 300.40/42.63 % (1900556)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=337173849:s2a=on:i=53295_2741 on theBenchmark for (2741ds/53295Mi) % 300.40/42.63 % (1900548)Instruction limit reached! % 300.40/42.63 % (1900548)------------------------------ % 300.40/42.63 % (1900548)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.40/42.63 % (1900548)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.40/42.63 % (1900548)CaDiCaL version: 2.1.3 % 300.40/42.63 % (1900548)Termination reason: Instruction limit % 300.40/42.63 % (1900548)Termination phase: Saturation % 300.40/42.63 % (1900548)Time elapsed: 7.615 s % 300.40/42.63 % (1900548)Peak memory usage: 119 MB % 300.40/42.63 % (1900548)Instructions burned: 11404 (million) % 300.40/42.63 % (1900558)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=1079284868:i=26857:ins=20_2715 on theBenchmark for (2715ds/26857Mi) % 300.40/42.63 % (1900558)Cannot represent all propositional literals internally % 300.40/42.63 % (1900558)Refutation not found, incomplete strategy % 300.40/42.63 % (1900558)------------------------------ % 300.40/42.63 % (1900558)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.40/42.63 % (1900558)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.40/42.63 % (1900558)CaDiCaL version: 2.1.3 % 300.40/42.63 % (1900558)Termination reason: Refutation not found, incomplete strategy % 300.40/42.63 % (1900558)Time elapsed: 0.191 s % 300.40/42.63 % (1900558)Peak memory usage: 15 MB % 300.40/42.63 % (1900558)Instructions burned: 373 (million) % 300.40/42.63 % (1900558)------------------------------ % 300.40/42.63 % (1900558)------------------------------ % 300.40/42.63 % (1900560)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=2757531478:i=28120:bs=on:fsr=off_2713 on theBenchmark for (2713ds/28120Mi) % 300.40/42.63 % (1900552)Instruction limit reached! % 300.40/42.63 % (1900552)------------------------------ % 300.40/42.63 % (1900552)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.40/42.63 % (1900552)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.40/42.63 % (1900552)CaDiCaL version: 2.1.3 % 300.40/42.63 % (1900552)Termination reason: Instruction limit % 300.40/42.63 % (1900552)Termination phase: Saturation % 300.40/42.63 % (1900552)Time elapsed: 8.227 s % 300.40/42.63 % (1900552)Peak memory usage: 144 MB % 300.40/42.63 % (1900552)Instructions burned: 15852 (million) % 300.40/42.63 % (1900562)fmb+10_1_sil=256000:fmbss=7:random_seed=1047726225:fmbsr=1.6:i=182295_2709 on theBenchmark for (2709ds/182295Mi) % 300.40/42.63 % (1900562)Cannot represent all propositional literals internally % 300.40/42.63 % (1900562)Refutation not found, incomplete strategy % 300.40/42.63 % (1900562)------------------------------ % 300.40/42.63 % (1900562)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.40/42.63 % (1900562)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.40/42.63 % (1900562)CaDiCaL version: 2.1.3 % 300.40/42.63 % (1900562)Termination reason: Refutation not found, incomplete strategy % 300.40/42.63 % (1900562)Time elapsed: 0.191 s % 300.40/42.63 % (1900562)Peak memory usage: 15 MB % 300.40/42.63 % (1900562)Instructions burned: 373 (million) % 300.40/42.63 % (1900562)------------------------------ % 300.40/42.63 % (1900562)------------------------------ % 300.40/42.63 % (1900564)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=2456505775:i=44625:gsp=on_2707 on theBenchmark for (2707ds/44625Mi) % 300.40/42.63 % (1900564)Cannot represent all propositional literals internally % 300.40/42.63 % (1900564)Refutation not found, incomplete strategy % 300.40/42.63 % (1900564)------------------------------ % 300.40/42.63 % (1900564)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.40/42.63 % (1900564)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.40/42.63 % (1900564)CaDiCaL version: 2.1.3 % 300.40/42.63 % (1900564)Termination reason: Refutation not found, incomplete strategy % 300.40/42.63 % (1900564)Time elapsed: 0.193 s % 300.40/42.63 % (1900564)Peak memory usage: 15 MB % 300.40/42.63 % (1900564)Instructions burned: 375 (million) % 300.40/42.63 % (1900564)------------------------------ % 300.40/42.63 % (1900564)------------------------------ % 300.40/42.63 % (1900566)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=1879164363:i=160505_2705 on theBenchmark for (2705ds/160505Mi) % 300.40/42.63 % (1900566)Cannot represent all propositional literals internally % 300.40/42.63 % (1900566)Refutation not found, incomplete strategy % 300.40/42.63 % (1900566)------------------------------ % 300.40/42.63 % (1900566)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.40/42.63 % (1900566)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.40/42.63 % (1900566)CaDiCaL version: 2.1.3 % 300.40/42.63 % (1900566)Termination reason: Refutation not found, incomplete strategy % 300.40/42.63 % (1900566)Time elapsed: 0.192 s % 300.40/42.63 % (1900566)Peak memory usage: 15 MB % 300.40/42.63 % (1900566)Instructions burned: 373 (million) % 300.40/42.63 % (1900566)------------------------------ % 300.40/42.63 % (1900566)------------------------------ % 300.40/42.63 % (1900568)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=2111414203:fmbsr=1.3:i=225729_2702 on theBenchmark for (2702ds/225729Mi) % 300.40/42.63 % (1900568)Cannot represent all propositional literals internally % 300.40/42.63 % (1900568)Refutation not found, incomplete strategy % 300.40/42.63 % (1900568)------------------------------ % 300.40/42.63 % (1900568)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.40/42.63 % (1900568)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.40/42.63 % (1900568)CaDiCaL version: 2.1.3 % 300.40/42.63 % (1900568)Termination reason: Refutation not found, incomplete strategy % 300.40/42.63 % (1900568)Time elapsed: 0.191 s % 300.40/42.63 % (1900568)Peak memory usage: 15 MB % 300.40/42.63 % (1900568)Instructions burned: 374 (million) % 300.40/42.63 % (1900568)------------------------------ % 300.40/42.63 % (1900568)------------------------------ % 300.40/42.63 % (1900570)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=2130096074:fmbsr=2:i=185024:ins=7_2700 on theBenchmark for (2700ds/185024Mi) % 300.40/42.63 % (1900570)Cannot represent all propositional literals internally % 300.40/42.63 % (1900570)Refutation not found, incomplete strategy % 300.40/42.63 % (1900570)------------------------------ % 300.40/42.63 % (1900570)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.40/42.63 % (1900570)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.40/42.63 % (1900570)CaDiCaL version: 2.1.3 % 300.40/42.63 % (1900570)Termination reason: Refutation not found, incomplete strategy % 300.40/42.63 % (1900570)Time elapsed: 0.192 s % 300.40/42.63 % (1900570)Peak memory usage: 15 MB % 300.40/42.63 % (1900570)Instructions burned: 374 (million) % 300.40/42.63 % (1900570)------------------------------ % 300.40/42.63 % (1900570)------------------------------ % 300.40/42.63 % (1900572)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=2787537278:rtra=on_2698 on theBenchmark for (2698ds/0Mi) % 300.40/42.63 % TRYING [1] % 300.40/42.63 % TRYING [2] % 300.40/42.63 % TRYING [3] % 300.40/42.63 % (1900554)Instruction limit reached! % 300.40/42.63 % (1900554)------------------------------ % 300.40/42.63 % (1900554)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.40/42.63 % (1900554)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.40/42.63 % (1900554)CaDiCaL version: 2.1.3 % 300.40/42.63 % (1900554)Termination reason: Instruction limit % 300.40/42.63 % (1900554)Termination phase: Saturation % 300.40/42.63 % (1900554)Time elapsed: 8.955 s % 300.40/42.63 % (1900554)Peak memory usage: 68 MB % 300.40/42.63 % (1900554)Instructions burned: 17629 (million) % 300.40/42.63 % (1900574)% WARNING: option uhcvi not known. % 300.40/42.63 % (1900574)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=804389787:i=271062:add=off:rtra=on:rawr=on_2676 on theBenchmark for (2676ds/271062Mi) % 300.40/42.63 % (1900556)Instruction limit reached! % 300.40/42.63 % (1900556)------------------------------ % 300.40/42.63 % (1900556)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.40/42.63 % (1900556)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.40/42.63 % (1900556)CaDiCaL version: 2.1.3 % 300.40/42.63 % (1900556)Termination reason: Instruction limit % 300.40/42.63 % (1900556)Termination phase: Saturation % 300.40/42.63 % (1900556)Time elapsed: 12.533 s % 300.40/42.63 % (1900556)Peak memory usage: 168 MB % 300.40/42.63 % (1900556)Instructions burned: 53299 (million) % 300.40/42.63 % (190057 % 300.40/42.63 Terminated % 300.40/42.63 % Vampire exiting % 300.40/42.64 Terminated %------------------------------------------------------------------------------