%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWV035+1 : TPTP v9.3.1. Bugfixed v3.3.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % Computer : n019.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:02 PM UTC 2026 % Result : Timeout 300.70s 42.74s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.05 % Problem : SWV035+1 : TPTP v9.3.1. Bugfixed v3.3.0. % 0.00/0.09 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.28/0.31 % Computer : n019.cluster.edu % 0.28/0.31 % Model : x86_64 x86_64 % 0.28/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.28/0.31 % Memory : 8046.5625MB % 0.28/0.31 % OS : Linux 6.8.0-71-generic % 0.28/0.31 % CPULimit : 300 % 0.28/0.31 % WCLimit : 300 % 0.28/0.31 % DateTime : Mon Sep 28 09:43:48 UTC 2026 % 0.28/0.31 % CPUTime : % 0.28/0.31 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.28/0.37 Running first-order model finding % 0.28/0.37 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 % 27.96/4.38 % (3888017)Will run a generic schedule for satisfiability detection. % 27.96/4.38 % (3888026)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=314550955:i=116_2999 on theBenchmark for (2999ds/116Mi) % 27.96/4.38 % (3888023)% WARNING: option uhcvi not known. % 27.96/4.38 % (3888028)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3307187785:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 27.96/4.38 % (3888027)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3788485305:i=131_2999 on theBenchmark for (2999ds/131Mi) % 27.96/4.38 % (3888024)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=643594820:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 27.96/4.38 % (3888025)dis+10_1_sil=32000:sp=arity:random_seed=2021079213:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 27.96/4.38 % (3888023)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3593697043:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 27.96/4.38 % (3888022)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1729685606_2999 on theBenchmark for (2999ds/0Mi) % 27.96/4.38 % (3888026)Instruction limit reached! % 27.96/4.38 % (3888026)------------------------------ % 27.96/4.38 % (3888026)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 27.96/4.38 % (3888026)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.96/4.38 % (3888026)CaDiCaL version: 2.1.3 % 27.96/4.38 % (3888026)Termination reason: Instruction limit % 27.96/4.38 % (3888026)Termination phase: Saturation % 27.96/4.38 % (3888026)Time elapsed: 0.061 s % 27.96/4.38 % (3888026)Peak memory usage: 13 MB % 27.96/4.38 % (3888026)Instructions burned: 117 (million) % 27.96/4.38 % (3888036)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2644862007:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 27.96/4.38 % TRYING [1] % 27.96/4.38 % TRYING [2] % 27.96/4.38 % TRYING [1] % 27.96/4.38 % TRYING [2] % 27.96/4.38 % (3888025)Instruction limit reached! % 27.96/4.38 % (3888025)------------------------------ % 27.96/4.38 % (3888025)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 27.96/4.38 % (3888025)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.96/4.38 % (3888025)CaDiCaL version: 2.1.3 % 27.96/4.38 % (3888025)Termination reason: Instruction limit % 27.96/4.38 % (3888025)Termination phase: Saturation % 27.96/4.38 % (3888025)Time elapsed: 0.098 s % 27.96/4.38 % (3888025)Peak memory usage: 12 MB % 27.96/4.38 % (3888025)Instructions burned: 104 (million) % 27.96/4.38 % TRYING [3] % 27.96/4.38 % (3888027)Instruction limit reached! % 27.96/4.38 % (3888027)------------------------------ % 27.96/4.38 % (3888027)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 27.96/4.38 % (3888027)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.96/4.38 % (3888027)CaDiCaL version: 2.1.3 % 27.96/4.38 % (3888027)Termination reason: Instruction limit % 27.96/4.38 % (3888027)Termination phase: Saturation % 27.96/4.38 % (3888027)Time elapsed: 0.126 s % 27.96/4.38 % (3888027)Peak memory usage: 12 MB % 27.96/4.38 % (3888027)Instructions burned: 131 (million) % 27.96/4.38 % TRYING [3] % 27.96/4.38 % TRYING [4] % 27.96/4.38 % (3888038)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1253408421:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi) % 27.96/4.38 % (3888028)Instruction limit reached! % 27.96/4.38 % (3888028)------------------------------ % 27.96/4.38 % (3888028)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 27.96/4.38 % (3888028)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.96/4.38 % (3888028)CaDiCaL version: 2.1.3 % 27.96/4.38 % (3888028)Termination reason: Instruction limit % 27.96/4.38 % (3888028)Termination phase: Saturation % 27.96/4.38 % (3888028)Time elapsed: 0.168 s % 27.96/4.38 % (3888028)Peak memory usage: 14 MB % 27.96/4.38 % (3888028)Instructions burned: 160 (million) % 27.96/4.38 % (3888039)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=978382931:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi) % 27.96/4.38 % (3888041)ott-21_1_sil=16000:fs=off:random_seed=2339352310:i=180:av=off:fsr=off_2997 on theBenchmark for (2997ds/180Mi) % 27.96/4.38 % (3888038)Instruction limit reached! % 27.96/4.38 % (3888038)------------------------------ % 27.96/4.38 % (3888038)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 27.96/4.38 % (3888038)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 70.62/10.31 % (3888038)CaDiCaL version: 2.1.3 % 70.62/10.31 % (3888038)Termination reason: Instruction limit % 70.62/10.31 % (3888038)Termination phase: Saturation % 70.62/10.31 % (3888038)Time elapsed: 0.142 s % 70.62/10.31 % (3888038)Peak memory usage: 13 MB % 70.62/10.31 % (3888038)Instructions burned: 131 (million) % 70.62/10.31 % TRYING [5] % 70.62/10.31 % (3888044)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2018595695:i=477:bd=all_2996 on theBenchmark for (2996ds/477Mi) % 70.62/10.31 % TRYING [4] % 70.62/10.31 % (3888036)Instruction limit reached! % 70.62/10.31 % (3888036)------------------------------ % 70.62/10.31 % (3888036)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 70.62/10.31 % (3888036)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 70.62/10.31 % (3888036)CaDiCaL version: 2.1.3 % 70.62/10.31 % (3888036)Termination reason: Instruction limit % 70.62/10.31 % (3888036)Termination phase: Finite model building constraint generation % 70.62/10.31 % (3888036)Time elapsed: 0.285 s % 70.62/10.31 % (3888036)Peak memory usage: 36 MB % 70.62/10.31 % (3888036)Instructions burned: 715 (million) % 70.62/10.31 % (3888041)Instruction limit reached! % 70.62/10.31 % (3888041)------------------------------ % 70.62/10.31 % (3888041)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 70.62/10.31 % (3888041)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 70.62/10.31 % (3888041)CaDiCaL version: 2.1.3 % 70.62/10.31 % (3888041)Termination reason: Instruction limit % 70.62/10.31 % (3888041)Termination phase: Saturation % 70.62/10.31 % (3888041)Time elapsed: 0.163 s % 70.62/10.31 % (3888041)Peak memory usage: 13 MB % 70.62/10.31 % (3888041)Instructions burned: 180 (million) % 70.62/10.31 % (3888046)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=406330851:fmbsr=1.3:i=865:ins=25_2995 on theBenchmark for (2995ds/865Mi) % 70.62/10.31 % TRYING [1] % 70.62/10.31 % (3888047)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3518232644:i=1179_2995 on theBenchmark for (2995ds/1179Mi) % 70.62/10.31 % TRYING [2] % 70.62/10.31 % TRYING [3] % 70.62/10.31 % TRYING [4] % 70.62/10.31 % (3888046)Instruction limit reached! % 70.62/10.31 % (3888046)------------------------------ % 70.62/10.31 % (3888046)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 70.62/10.31 % (3888046)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 70.62/10.31 % (3888046)CaDiCaL version: 2.1.3 % 70.62/10.31 % (3888046)Termination reason: Instruction limit % 70.62/10.31 % (3888046)Termination phase: Finite model building constraint generation % 70.62/10.31 % (3888046)Time elapsed: 0.373 s % 70.62/10.31 % (3888046)Peak memory usage: 33 MB % 70.62/10.31 % (3888046)Instructions burned: 874 (million) % 70.62/10.31 % (3888050)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=4192128690:i=889:ins=1_2991 on theBenchmark for (2991ds/889Mi) % 70.62/10.31 % (3888044)Instruction limit reached! % 70.62/10.31 % (3888044)------------------------------ % 70.62/10.31 % (3888044)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 70.62/10.31 % (3888044)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 70.62/10.31 % (3888044)CaDiCaL version: 2.1.3 % 70.62/10.31 % (3888044)Termination reason: Instruction limit % 70.62/10.31 % (3888044)Termination phase: Saturation % 70.62/10.31 % (3888044)Time elapsed: 0.522 s % 70.62/10.31 % (3888044)Peak memory usage: 15 MB % 70.62/10.31 % (3888044)Instructions burned: 478 (million) % 70.62/10.31 % (3888039)Instruction limit reached! % 70.62/10.31 % (3888039)------------------------------ % 70.62/10.31 % (3888039)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 70.62/10.31 % (3888039)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 70.62/10.31 % (3888039)CaDiCaL version: 2.1.3 % 70.62/10.31 % (3888039)Termination reason: Instruction limit % 70.62/10.31 % (3888039)Termination phase: Saturation % 70.62/10.31 % (3888039)Time elapsed: 0.694 s % 70.62/10.31 % (3888039)Peak memory usage: 18 MB % 70.62/10.31 % (3888039)Instructions burned: 684 (million) % 70.62/10.31 % (3888052)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=1660704382:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2990 on theBenchmark for (2990ds/692Mi) % 70.62/10.31 % (3888053)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3387465597:i=879:kws=inv_precedence:fsr=off_2990 on theBenchmark for (2990ds/879Mi) % 70.62/10.31 % TRYING [5] % 70.62/10.31 % (3888050)Instruction limit reached! % 70.62/10.31 % (3888050)------------------------------ % 114.01/16.42 % (3888050)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 114.01/16.42 % (3888050)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 114.01/16.42 % (3888050)CaDiCaL version: 2.1.3 % 114.01/16.42 % (3888050)Termination reason: Instruction limit % 114.01/16.42 % (3888050)Termination phase: Finite model building constraint generation % 114.01/16.42 % (3888050)Time elapsed: 0.452 s % 114.01/16.42 % (3888050)Peak memory usage: 101 MB % 114.01/16.42 % (3888050)Instructions burned: 890 (million) % 114.01/16.42 % (3888056)fmb+10_1_sil=64000:random_seed=643912740:i=22061:nm=2:gsp=on_2986 on theBenchmark for (2986ds/22061Mi) % 114.01/16.42 % TRYING [1] % 114.01/16.42 % TRYING [2] % 114.01/16.42 % TRYING [3] % 114.01/16.42 % TRYING [4] % 114.01/16.42 % (3888047)Instruction limit reached! % 114.01/16.42 % (3888047)------------------------------ % 114.01/16.42 % (3888047)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 114.01/16.42 % (3888047)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 114.01/16.42 % (3888047)CaDiCaL version: 2.1.3 % 114.01/16.42 % (3888047)Termination reason: Instruction limit % 114.01/16.42 % (3888047)Termination phase: Saturation % 114.01/16.42 % (3888047)Time elapsed: 1.090 s % 114.01/16.42 % (3888047)Peak memory usage: 19 MB % 114.01/16.42 % (3888047)Instructions burned: 1179 (million) % 114.01/16.42 % (3888058)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2454811400:i=9515:nm=5_2984 on theBenchmark for (2984ds/9515Mi) % 114.01/16.42 % TRYING [20] % 114.01/16.42 % (3888052)Instruction limit reached! % 114.01/16.42 % (3888052)------------------------------ % 114.01/16.42 % (3888052)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 114.01/16.42 % (3888052)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 114.01/16.42 % (3888052)CaDiCaL version: 2.1.3 % 114.01/16.42 % (3888052)Termination reason: Instruction limit % 114.01/16.42 % (3888052)Termination phase: Saturation % 114.01/16.42 % (3888052)Time elapsed: 0.809 s % 114.01/16.42 % (3888052)Peak memory usage: 18 MB % 114.01/16.42 % (3888052)Instructions burned: 692 (million) % 114.01/16.42 % (3888053)Instruction limit reached! % 114.01/16.42 % (3888053)------------------------------ % 114.01/16.42 % (3888053)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 114.01/16.42 % (3888053)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 114.01/16.42 % (3888053)CaDiCaL version: 2.1.3 % 114.01/16.42 % (3888053)Termination reason: Instruction limit % 114.01/16.42 % (3888053)Termination phase: Saturation % 114.01/16.42 % (3888053)Time elapsed: 0.802 s % 114.01/16.42 % (3888053)Peak memory usage: 20 MB % 114.01/16.42 % (3888053)Instructions burned: 879 (million) % 114.01/16.42 % (3888060)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3241690235:fmbsr=1.7:i=920_2982 on theBenchmark for (2982ds/920Mi) % 114.01/16.42 % (3888061)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=4207224060:i=5131_2982 on theBenchmark for (2982ds/5131Mi) % 114.01/16.42 % TRYING [8] % 114.01/16.42 % TRYING [5] % 114.01/16.42 % (3888060)Instruction limit reached! % 114.01/16.42 % (3888060)------------------------------ % 114.01/16.42 % (3888060)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 114.01/16.42 % (3888060)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 114.01/16.42 % (3888060)CaDiCaL version: 2.1.3 % 114.01/16.42 % (3888060)Termination reason: Instruction limit % 114.01/16.42 % (3888060)Termination phase: Finite model building constraint generation % 114.01/16.42 % (3888060)Time elapsed: 0.642 s % 114.01/16.42 % (3888060)Peak memory usage: 62 MB % 114.01/16.42 % (3888060)Instructions burned: 921 (million) % 114.01/16.42 % (3888064)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3910600470:i=1472:ins=7:fdi=8:gsp=on_2975 on theBenchmark for (2975ds/1472Mi) % 114.01/16.42 % TRYING [6] % 114.01/16.42 % (3888064)Instruction limit reached! % 114.01/16.42 % (3888064)------------------------------ % 114.01/16.42 % (3888064)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 114.01/16.42 % (3888064)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 114.01/16.42 % (3888064)CaDiCaL version: 2.1.3 % 114.01/16.42 % (3888064)Termination reason: Instruction limit % 114.01/16.42 % (3888064)Termination phase: Saturation % 114.01/16.42 % (3888064)Time elapsed: 1.346 s % 114.01/16.42 % (3888064)Peak memory usage: 23 MB % 114.01/16.42 % (3888064)Instructions burned: 1472 (million) % 114.01/16.42 % (3888066)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=4066773975:i=6324_2961 on theBenchmark for (2961ds/6324Mi) % 114.01/16.42 % (3888066)Cannot represent all propositional literals internally % 262.38/37.39 % (3888066)Refutation not found, incomplete strategy % 262.38/37.39 % (3888066)------------------------------ % 262.38/37.39 % (3888066)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 262.38/37.39 % (3888066)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 262.38/37.39 % (3888066)CaDiCaL version: 2.1.3 % 262.38/37.39 % (3888066)Termination reason: Refutation not found, incomplete strategy % 262.38/37.39 % (3888066)Time elapsed: 0.082 s % 262.38/37.39 % (3888066)Peak memory usage: 12 MB % 262.38/37.39 % (3888066)Instructions burned: 97 (million) % 262.38/37.39 % (3888066)------------------------------ % 262.38/37.39 % (3888066)------------------------------ % 262.38/37.39 % (3888068)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=3075171322:fmbsr=2.30978:i=2174_2959 on theBenchmark for (2959ds/2174Mi) % 262.38/37.39 % TRYING [6] % 262.38/37.39 % TRYING [16] % 262.38/37.39 % (3888068)Instruction limit reached! % 262.38/37.39 % (3888068)------------------------------ % 262.38/37.39 % (3888068)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 262.38/37.39 % (3888068)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 262.38/37.39 % (3888068)CaDiCaL version: 2.1.3 % 262.38/37.39 % (3888068)Termination reason: Instruction limit % 262.38/37.39 % (3888068)Termination phase: Finite model building constraint generation % 262.38/37.39 % (3888068)Time elapsed: 1.574 s % 262.38/37.39 % (3888068)Peak memory usage: 132 MB % 262.38/37.39 % (3888068)Instructions burned: 2175 (million) % 262.38/37.39 % (3888070)ott-2_1_sil=16000:newcnf=on:random_seed=3520836131:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2943 on theBenchmark for (2943ds/869Mi) % 262.38/37.39 % (3888061)Instruction limit reached! % 262.38/37.39 % (3888061)------------------------------ % 262.38/37.39 % (3888061)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 262.38/37.39 % (3888061)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 262.38/37.39 % (3888061)CaDiCaL version: 2.1.3 % 262.38/37.39 % (3888061)Termination reason: Instruction limit % 262.38/37.39 % (3888061)Termination phase: Saturation % 262.38/37.39 % (3888061)Time elapsed: 4.254 s % 262.38/37.39 % (3888061)Peak memory usage: 26 MB % 262.38/37.39 % (3888061)Instructions burned: 5131 (million) % 262.38/37.39 % (3888072)ott+10_1_sil=32000:tgt=ground:random_seed=3429013540:i=5114:av=off_2939 on theBenchmark for (2939ds/5114Mi) % 262.38/37.39 % (3888070)Instruction limit reached! % 262.38/37.39 % (3888070)------------------------------ % 262.38/37.39 % (3888070)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 262.38/37.39 % (3888070)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 262.38/37.39 % (3888070)CaDiCaL version: 2.1.3 % 262.38/37.39 % (3888070)Termination reason: Instruction limit % 262.38/37.39 % (3888070)Termination phase: Saturation % 262.38/37.39 % (3888070)Time elapsed: 0.835 s % 262.38/37.39 % (3888070)Peak memory usage: 18 MB % 262.38/37.39 % (3888070)Instructions burned: 869 (million) % 262.38/37.39 % (3888074)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=3541550895:i=54282_2934 on theBenchmark for (2934ds/54282Mi) % 262.38/37.39 % TRYING [1] % 262.38/37.39 % TRYING [2] % 262.38/37.39 % TRYING [3] % 262.38/37.39 % TRYING [4] % 262.38/37.39 % TRYING [5] % 262.38/37.39 % (3888058)Instruction limit reached! % 262.38/37.39 % (3888058)------------------------------ % 262.38/37.39 % (3888058)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 262.38/37.39 % (3888058)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 262.38/37.39 % (3888058)CaDiCaL version: 2.1.3 % 262.38/37.39 % (3888058)Termination reason: Instruction limit % 262.38/37.39 % (3888058)Termination phase: Finite model building constraint generation % 262.38/37.39 % (3888058)Time elapsed: 6.682 s % 262.38/37.39 % (3888058)Peak memory usage: 562 MB % 262.38/37.39 % (3888058)Instructions burned: 9515 (million) % 262.38/37.39 % (3888076)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=680801619:i=3512:aac=none_2915 on theBenchmark for (2915ds/3512Mi) % 262.38/37.39 % (3888056)Instruction limit reached! % 262.38/37.39 % (3888056)------------------------------ % 262.38/37.39 % (3888056)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 262.38/37.39 % (3888056)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 262.38/37.39 % (3888056)CaDiCaL version: 2.1.3 % 262.38/37.39 % (3888056)Termination reason: Instruction limit % 262.38/37.39 % (3888056)Termination phase: Finite model building SAT solving % 262.38/37.39 % (3888056)Time elapsed: 8.516 s % 262.38/37.39 % (3888056)Peak memory usage: 211 MB % 262.38/37.39 % (3888056)Instructions burned: 22061 (million) % 262.38/37.39 % (3888078)dis+21_1_sil=32000:sas=cadical:random_seed=1877802787:i=3773:amm=off_2901 on theBenchmark for (2901ds/3773Mi) % 300.70/42.74 % TRYING [6] % 300.70/42.74 % TRYING [7] % 300.70/42.74 % (3888072)Instruction limit reached! % 300.70/42.74 % (3888072)------------------------------ % 300.70/42.74 % (3888072)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.70/42.74 % (3888072)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.70/42.74 % (3888072)CaDiCaL version: 2.1.3 % 300.70/42.74 % (3888072)Termination reason: Instruction limit % 300.70/42.74 % (3888072)Termination phase: Saturation % 300.70/42.74 % (3888072)Time elapsed: 4.827 s % 300.70/42.74 % (3888072)Peak memory usage: 54 MB % 300.70/42.74 % (3888072)Instructions burned: 5114 (million) % 300.70/42.74 % (3888080)ott+11_1_sil=16000:gs=on:random_seed=306637855:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2890 on theBenchmark for (2890ds/2251Mi) % 300.70/42.74 % (3888076)Instruction limit reached! % 300.70/42.74 % (3888076)------------------------------ % 300.70/42.74 % (3888076)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.70/42.74 % (3888076)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.70/42.74 % (3888076)CaDiCaL version: 2.1.3 % 300.70/42.74 % (3888076)Termination reason: Instruction limit % 300.70/42.74 % (3888076)Termination phase: Saturation % 300.70/42.74 % (3888076)Time elapsed: 2.877 s % 300.70/42.74 % (3888076)Peak memory usage: 25 MB % 300.70/42.74 % (3888076)Instructions burned: 3513 (million) % 300.70/42.74 % (3888082)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=2244667281:fmbsr=1.6:i=67534_2886 on theBenchmark for (2886ds/67534Mi) % 300.70/42.74 % (3888078)Instruction limit reached! % 300.70/42.74 % (3888078)------------------------------ % 300.70/42.74 % (3888078)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.70/42.74 % (3888078)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.70/42.74 % (3888078)CaDiCaL version: 2.1.3 % 300.70/42.74 % (3888078)Termination reason: Instruction limit % 300.70/42.74 % (3888078)Termination phase: Saturation % 300.70/42.74 % (3888078)Time elapsed: 1.690 s % 300.70/42.74 % (3888078)Peak memory usage: 30 MB % 300.70/42.74 % (3888078)Instructions burned: 3774 (million) % 300.70/42.74 % (3888084)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=3989469851:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2883 on theBenchmark for (2883ds/4591Mi) % 300.70/42.74 % TRYING [7] % 300.70/42.74 % (3888080)Instruction limit reached! % 300.70/42.74 % (3888080)------------------------------ % 300.70/42.74 % (3888080)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.70/42.74 % (3888080)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.70/42.74 % (3888080)CaDiCaL version: 2.1.3 % 300.70/42.74 % (3888080)Termination reason: Instruction limit % 300.70/42.74 % (3888080)Termination phase: Saturation % 300.70/42.74 % (3888080)Time elapsed: 2.311 s % 300.70/42.74 % (3888080)Peak memory usage: 28 MB % 300.70/42.74 % (3888080)Instructions burned: 2251 (million) % 300.70/42.74 % (3888086)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=3295793688:i=29340_2866 on theBenchmark for (2866ds/29340Mi) % 300.70/42.74 % (3888084)Instruction limit reached! % 300.70/42.74 % (3888084)------------------------------ % 300.70/42.74 % (3888084)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.70/42.74 % (3888084)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.70/42.74 % (3888084)CaDiCaL version: 2.1.3 % 300.70/42.74 % (3888084)Termination reason: Instruction limit % 300.70/42.74 % (3888084)Termination phase: Saturation % 300.70/42.74 % (3888084)Time elapsed: 2.082 s % 300.70/42.74 % (3888084)Peak memory usage: 35 MB % 300.70/42.74 % (3888084)Instructions burned: 4593 (million) % 300.70/42.74 % (3888088)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=2273801179:i=5211_2862 on theBenchmark for (2862ds/5211Mi) % 300.70/42.74 % (3888088)Instruction limit reached! % 300.70/42.74 % (3888088)------------------------------ % 300.70/42.74 % (3888088)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.70/42.74 % (3888088)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.70/42.74 % (3888088)CaDiCaL version: 2.1.3 % 300.70/42.74 % (3888088)Termination reason: Instruction limit % 300.70/42.74 % (3888088)Termination phase: Saturation % 300.70/42.74 % (3888088)Time elapsed: 2.244 s % 300.70/42.74 % (3888088)Peak memory usage: 23 MB % 300.70/42.74 % (3888088)Instructions burned: 5211 (million) % 300.70/42.74 % (3888099)fmb+10_1_sil=32000:sas=cadical: % 300.70/42.74 Terminated % 300.70/42.74 % Vampire exiting %------------------------------------------------------------------------------