%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWV563-1.010 : TPTP v9.3.1. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % Computer : n020.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:25:58 PM UTC 2026 % Result : Timeout 300.43s 42.63s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWV563-1.010 : TPTP v9.3.1. Released v4.0.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.09/0.18 % Computer : n020.cluster.edu % 0.09/0.18 % Model : x86_64 x86_64 % 0.09/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.18 % Memory : 8046.5625MB % 0.09/0.18 % OS : Linux 6.8.0-71-generic % 0.09/0.18 % CPULimit : 300 % 0.09/0.18 % WCLimit : 300 % 0.09/0.18 % DateTime : Mon Sep 28 11:51:04 UTC 2026 % 0.09/0.19 % CPUTime : % 0.09/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.09/0.21 Running first-order model finding % 0.09/0.21 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 % 15.31/2.46 % (115727)Will run a generic schedule for satisfiability detection. % 15.31/2.46 % (115734)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1786848143:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 15.31/2.46 % (115733)% WARNING: option uhcvi not known. % 15.31/2.46 % (115732)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=624946571_2999 on theBenchmark for (2999ds/0Mi) % 15.31/2.46 % (115733)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2991871060:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 15.31/2.46 % (115735)dis+10_1_sil=32000:sp=arity:random_seed=2197852101:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 15.31/2.46 % (115736)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1687465215:i=116_2999 on theBenchmark for (2999ds/116Mi) % 15.31/2.46 % (115737)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2635178199:i=131_2999 on theBenchmark for (2999ds/131Mi) % 15.31/2.46 % (115738)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2001834459:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 15.31/2.46 % TRYING [1] % 15.31/2.46 % TRYING [2] % 15.31/2.46 % TRYING [3] % 15.31/2.46 % TRYING [4] % 15.31/2.46 % TRYING [5] % 15.31/2.46 % (115735)Instruction limit reached! % 15.31/2.46 % (115735)------------------------------ % 15.31/2.46 % (115735)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 15.31/2.46 % (115735)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.31/2.46 % (115735)CaDiCaL version: 2.1.3 % 15.31/2.46 % (115735)Termination reason: Instruction limit % 15.31/2.46 % (115735)Termination phase: Saturation % 15.31/2.46 % (115735)Time elapsed: 0.043 s % 15.31/2.46 % (115735)Peak memory usage: 13 MB % 15.31/2.46 % (115735)Instructions burned: 104 (million) % 15.31/2.46 % (115737)Instruction limit reached! % 15.31/2.46 % (115737)------------------------------ % 15.31/2.46 % (115737)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 15.31/2.46 % (115737)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.31/2.46 % (115737)CaDiCaL version: 2.1.3 % 15.31/2.46 % (115737)Termination reason: Instruction limit % 15.31/2.46 % (115737)Termination phase: Saturation % 15.31/2.46 % (115737)Time elapsed: 0.047 s % 15.31/2.46 % (115737)Peak memory usage: 12 MB % 15.31/2.46 % (115737)Instructions burned: 132 (million) % 15.31/2.46 % (115736)Instruction limit reached! % 15.31/2.46 % (115736)------------------------------ % 15.31/2.46 % (115736)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 15.31/2.46 % (115736)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.31/2.46 % (115736)CaDiCaL version: 2.1.3 % 15.31/2.46 % (115736)Termination reason: Instruction limit % 15.31/2.46 % (115736)Termination phase: Saturation % 15.31/2.46 % (115736)Time elapsed: 0.050 s % 15.31/2.46 % (115736)Peak memory usage: 13 MB % 15.31/2.46 % (115736)Instructions burned: 117 (million) % 15.31/2.46 % (115746)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2992289599:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 15.31/2.46 % (115747)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1138021495:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi) % 15.31/2.46 % TRYING [1] % 15.31/2.46 % TRYING [2] % 15.31/2.46 % TRYING [3] % 15.31/2.46 % (115748)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=1247308869:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi) % 15.31/2.46 % (115738)Instruction limit reached! % 15.31/2.46 % (115738)------------------------------ % 15.31/2.46 % (115738)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 15.31/2.46 % (115738)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.31/2.46 % (115738)CaDiCaL version: 2.1.3 % 15.31/2.46 % (115738)Termination reason: Instruction limit % 15.31/2.46 % (115738)Termination phase: Saturation % 15.31/2.46 % (115738)Time elapsed: 0.077 s % 15.31/2.46 % (115738)Peak memory usage: 16 MB % 15.31/2.46 % (115738)Instructions burned: 161 (million) % 15.31/2.46 % TRYING [4] % 15.31/2.46 % (115752)ott-21_1_sil=16000:fs=off:random_seed=3282809502:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 15.31/2.46 % TRYING [5] % 15.31/2.46 % TRYING [6] % 15.31/2.46 % (115747)Instruction limit reached! % 15.31/2.46 % (115747)------------------------------ % 15.31/2.46 % (115747)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 15.31/2.46 % (115747)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 57.71/8.42 % (115747)CaDiCaL version: 2.1.3 % 57.71/8.42 % (115747)Termination reason: Instruction limit % 57.71/8.42 % (115747)Termination phase: Saturation % 57.71/8.42 % (115747)Time elapsed: 0.059 s % 57.71/8.42 % (115747)Peak memory usage: 15 MB % 57.71/8.42 % (115747)Instructions burned: 133 (million) % 57.71/8.42 % (115754)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=525750523:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 57.71/8.42 % (115752)Instruction limit reached! % 57.71/8.42 % (115752)------------------------------ % 57.71/8.42 % (115752)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 57.71/8.42 % (115752)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 57.71/8.42 % (115752)CaDiCaL version: 2.1.3 % 57.71/8.42 % (115752)Termination reason: Instruction limit % 57.71/8.42 % (115752)Termination phase: Saturation % 57.71/8.42 % (115752)Time elapsed: 0.075 s % 57.71/8.42 % (115752)Peak memory usage: 13 MB % 57.71/8.42 % (115752)Instructions burned: 181 (million) % 57.71/8.42 % (115756)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1115913442:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi) % 57.71/8.42 % TRYING [1] % 57.71/8.42 % TRYING [2] % 57.71/8.42 % TRYING [3] % 57.71/8.42 % TRYING [4] % 57.71/8.42 % TRYING [6] % 57.71/8.42 % TRYING [5] % 57.71/8.42 % TRYING [7] % 57.71/8.42 % (115746)Instruction limit reached! % 57.71/8.42 % (115746)------------------------------ % 57.71/8.42 % (115746)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 57.71/8.42 % (115746)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 57.71/8.42 % (115746)CaDiCaL version: 2.1.3 % 57.71/8.42 % (115746)Termination reason: Instruction limit % 57.71/8.42 % (115746)Termination phase: Finite model building constraint generation % 57.71/8.42 % (115746)Time elapsed: 0.305 s % 57.71/8.42 % (115746)Peak memory usage: 27 MB % 57.71/8.42 % (115746)Instructions burned: 716 (million) % 57.71/8.42 % (115758)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1204053740:i=1179_2995 on theBenchmark for (2995ds/1179Mi) % 57.71/8.42 % (115754)Instruction limit reached! % 57.71/8.42 % (115754)------------------------------ % 57.71/8.42 % (115754)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 57.71/8.42 % (115754)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 57.71/8.42 % (115754)CaDiCaL version: 2.1.3 % 57.71/8.42 % (115754)Termination reason: Instruction limit % 57.71/8.42 % (115754)Termination phase: Saturation % 57.71/8.42 % (115754)Time elapsed: 0.269 s % 57.71/8.42 % (115754)Peak memory usage: 15 MB % 57.71/8.42 % (115754)Instructions burned: 479 (million) % 57.71/8.42 % (115760)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1271493949:i=889:ins=1_2995 on theBenchmark for (2995ds/889Mi) % 57.71/8.42 % (115748)Instruction limit reached! % 57.71/8.42 % (115748)------------------------------ % 57.71/8.42 % (115748)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 57.71/8.42 % (115748)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 57.71/8.42 % (115748)CaDiCaL version: 2.1.3 % 57.71/8.42 % (115748)Termination reason: Instruction limit % 57.71/8.42 % (115748)Termination phase: Saturation % 57.71/8.42 % (115748)Time elapsed: 0.415 s % 57.71/8.42 % (115748)Peak memory usage: 17 MB % 57.71/8.42 % (115748)Instructions burned: 686 (million) % 57.71/8.42 % (115756)Instruction limit reached! % 57.71/8.42 % (115756)------------------------------ % 57.71/8.42 % (115756)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 57.71/8.42 % (115756)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 57.71/8.42 % (115756)CaDiCaL version: 2.1.3 % 57.71/8.42 % (115756)Termination reason: Instruction limit % 57.71/8.42 % (115756)Termination phase: Finite model building SAT solving % 57.71/8.42 % (115756)Time elapsed: 0.311 s % 57.71/8.42 % (115756)Peak memory usage: 22 MB % 57.71/8.42 % (115756)Instructions burned: 868 (million) % 57.71/8.42 % (115762)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=561522592: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) % 57.71/8.42 % (115763)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=219718760:i=879:kws=inv_precedence:fsr=off_2994 on theBenchmark for (2994ds/879Mi) % 57.71/8.42 % TRYING [14] % 57.71/8.42 % (115760)Instruction limit reached! % 57.71/8.42 % (115760)------------------------------ % 57.71/8.42 % (115760)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 116.02/16.69 % (115760)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 116.02/16.69 % (115760)CaDiCaL version: 2.1.3 % 116.02/16.69 % (115760)Termination reason: Instruction limit % 116.02/16.69 % (115760)Termination phase: Finite model building constraint generation % 116.02/16.69 % (115760)Time elapsed: 0.386 s % 116.02/16.69 % (115760)Peak memory usage: 96 MB % 116.02/16.69 % (115760)Instructions burned: 893 (million) % 116.02/16.69 % (115766)fmb+10_1_sil=64000:random_seed=3374087665:i=22061:nm=2:gsp=on_2991 on theBenchmark for (2991ds/22061Mi) % 116.02/16.69 % TRYING [1] % 116.02/16.69 % TRYING [2] % 116.02/16.69 % TRYING [3] % 116.02/16.69 % TRYING [4] % 116.02/16.69 % (115758)Instruction limit reached! % 116.02/16.69 % (115758)------------------------------ % 116.02/16.69 % (115758)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 116.02/16.69 % (115758)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 116.02/16.69 % (115758)CaDiCaL version: 2.1.3 % 116.02/16.69 % (115758)Termination reason: Instruction limit % 116.02/16.69 % (115758)Termination phase: Saturation % 116.02/16.69 % (115758)Time elapsed: 0.513 s % 116.02/16.69 % (115758)Peak memory usage: 16 MB % 116.02/16.69 % (115758)Instructions burned: 1179 (million) % 116.02/16.69 % (115768)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=828030494:i=9515:nm=5_2990 on theBenchmark for (2990ds/9515Mi) % 116.02/16.69 % TRYING [20] % 116.02/16.69 % (115762)Instruction limit reached! % 116.02/16.69 % (115762)------------------------------ % 116.02/16.69 % (115762)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 116.02/16.69 % (115762)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 116.02/16.69 % (115762)CaDiCaL version: 2.1.3 % 116.02/16.69 % (115762)Termination reason: Instruction limit % 116.02/16.69 % (115762)Termination phase: Saturation % 116.02/16.69 % (115762)Time elapsed: 0.433 s % 116.02/16.69 % (115762)Peak memory usage: 21 MB % 116.02/16.69 % (115762)Instructions burned: 693 (million) % 116.02/16.69 % (115763)Instruction limit reached! % 116.02/16.69 % (115763)------------------------------ % 116.02/16.69 % (115763)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 116.02/16.69 % (115763)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 116.02/16.69 % (115763)CaDiCaL version: 2.1.3 % 116.02/16.69 % (115763)Termination reason: Instruction limit % 116.02/16.69 % (115763)Termination phase: Saturation % 116.02/16.69 % (115763)Time elapsed: 0.418 s % 116.02/16.69 % (115763)Peak memory usage: 15 MB % 116.02/16.69 % (115763)Instructions burned: 879 (million) % 116.02/16.69 % (115770)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3673610807:fmbsr=1.7:i=920_2990 on theBenchmark for (2990ds/920Mi) % 116.02/16.69 % (115771)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2316076388:i=5131_2989 on theBenchmark for (2989ds/5131Mi) % 116.02/16.69 % TRYING [8] % 116.02/16.69 % TRYING [5] % 116.02/16.69 % TRYING [8] % 116.02/16.69 % TRYING [6] % 116.02/16.69 % (115770)Instruction limit reached! % 116.02/16.69 % (115770)------------------------------ % 116.02/16.69 % (115770)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 116.02/16.69 % (115770)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 116.02/16.69 % (115770)CaDiCaL version: 2.1.3 % 116.02/16.69 % (115770)Termination reason: Instruction limit % 116.02/16.69 % (115770)Termination phase: Finite model building constraint generation % 116.02/16.69 % (115770)Time elapsed: 0.337 s % 116.02/16.69 % (115770)Peak memory usage: 77 MB % 116.02/16.69 % (115770)Instructions burned: 922 (million) % 116.02/16.69 % (115775)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=942388880:i=1472:ins=7:fdi=8:gsp=on_2986 on theBenchmark for (2986ds/1472Mi) % 116.02/16.69 % TRYING [7] % 116.02/16.69 % (115775)Instruction limit reached! % 116.02/16.69 % (115775)------------------------------ % 116.02/16.69 % (115775)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 116.02/16.69 % (115775)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 116.02/16.69 % (115775)CaDiCaL version: 2.1.3 % 116.02/16.69 % (115775)Termination reason: Instruction limit % 116.02/16.69 % (115775)Termination phase: Saturation % 116.02/16.69 % (115775)Time elapsed: 0.831 s % 116.02/16.69 % (115775)Peak memory usage: 31 MB % 116.02/16.69 % (115775)Instructions burned: 1473 (million) % 116.02/16.69 % (115777)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=270460880:i=6324_2977 on theBenchmark for (2977ds/6324Mi) % 116.02/16.69 % (115777)Cannot represent all propositional literals internally % 116.02/16.69 % (115777)Refutation not found, incomplete strategy % 116.02/16.69 % (115777)------------------------------ % 237.05/33.79 % (115777)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 237.05/33.79 % (115777)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 237.05/33.79 % (115777)CaDiCaL version: 2.1.3 % 237.05/33.79 % (115777)Termination reason: Refutation not found, incomplete strategy % 237.05/33.79 % (115777)Time elapsed: 0.003 s % 237.05/33.79 % (115777)Peak memory usage: 10 MB % 237.05/33.79 % (115777)Instructions burned: 6 (million) % 237.05/33.79 % (115777)------------------------------ % 237.05/33.79 % (115777)------------------------------ % 237.05/33.79 % (115779)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=2522694005:fmbsr=2.30978:i=2174_2977 on theBenchmark for (2977ds/2174Mi) % 237.05/33.79 % TRYING [16] % 237.05/33.79 % (115779)Instruction limit reached! % 237.05/33.79 % (115779)------------------------------ % 237.05/33.79 % (115779)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 237.05/33.79 % (115779)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 237.05/33.79 % (115779)CaDiCaL version: 2.1.3 % 237.05/33.79 % (115779)Termination reason: Instruction limit % 237.05/33.79 % (115779)Termination phase: Finite model building constraint generation % 237.05/33.79 % (115779)Time elapsed: 0.765 s % 237.05/33.79 % (115779)Peak memory usage: 144 MB % 237.05/33.79 % (115779)Instructions burned: 2175 (million) % 237.05/33.79 % (115781)ott-2_1_sil=16000:newcnf=on:random_seed=1587388069:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2969 on theBenchmark for (2969ds/869Mi) % 237.05/33.79 % TRYING [9] % 237.05/33.79 % (115781)Instruction limit reached! % 237.05/33.79 % (115781)------------------------------ % 237.05/33.79 % (115781)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 237.05/33.79 % (115781)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 237.05/33.79 % (115781)CaDiCaL version: 2.1.3 % 237.05/33.79 % (115781)Termination reason: Instruction limit % 237.05/33.79 % (115781)Termination phase: Saturation % 237.05/33.79 % (115781)Time elapsed: 0.498 s % 237.05/33.79 % (115781)Peak memory usage: 19 MB % 237.05/33.79 % (115781)Instructions burned: 870 (million) % 237.05/33.79 % (115783)ott+10_1_sil=32000:tgt=ground:random_seed=3308521883:i=5114:av=off_2964 on theBenchmark for (2964ds/5114Mi) % 237.05/33.79 % TRYING [8] % 237.05/33.79 % (115768)Instruction limit reached! % 237.05/33.79 % (115768)------------------------------ % 237.05/33.79 % (115768)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 237.05/33.79 % (115768)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 237.05/33.79 % (115768)CaDiCaL version: 2.1.3 % 237.05/33.79 % (115768)Termination reason: Instruction limit % 237.05/33.79 % (115768)Termination phase: Finite model building constraint generation % 237.05/33.79 % (115768)Time elapsed: 3.396 s % 237.05/33.79 % (115768)Peak memory usage: 614 MB % 237.05/33.79 % (115768)Instructions burned: 9516 (million) % 237.05/33.79 % (115785)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=97273019:i=54282_2955 on theBenchmark for (2955ds/54282Mi) % 237.05/33.79 % TRYING [1] % 237.05/33.79 % TRYING [2] % 237.05/33.79 % TRYING [3] % 237.05/33.79 % TRYING [4] % 237.05/33.79 % TRYING [5] % 237.05/33.79 % TRYING [6] % 237.05/33.79 % TRYING [7] % 237.05/33.79 % TRYING [8] % 237.05/33.79 % (115771)Instruction limit reached! % 237.05/33.79 % (115771)------------------------------ % 237.05/33.79 % (115771)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 237.05/33.79 % (115771)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 237.05/33.79 % (115771)CaDiCaL version: 2.1.3 % 237.05/33.79 % (115771)Termination reason: Instruction limit % 237.05/33.79 % (115771)Termination phase: Saturation % 237.05/33.79 % (115771)Time elapsed: 4.916 s % 237.05/33.79 % (115771)Peak memory usage: 25 MB % 237.05/33.79 % (115771)Instructions burned: 5131 (million) % 237.05/33.79 % (115787)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=734464201:i=3512:aac=none_2940 on theBenchmark for (2940ds/3512Mi) % 237.05/33.79 % TRYING [9] % 237.05/33.79 % (115783)Instruction limit reached! % 237.05/33.79 % (115783)------------------------------ % 237.05/33.79 % (115783)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 237.05/33.79 % (115783)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 237.05/33.79 % (115783)CaDiCaL version: 2.1.3 % 237.05/33.79 % (115783)Termination reason: Instruction limit % 237.05/33.79 % (115783)Termination phase: Saturation % 237.05/33.79 % (115783)Time elapsed: 4.441 s % 237.05/33.79 % (115783)Peak memory usage: 80 MB % 237.05/33.79 % (115783)Instructions burned: 5117 (million) % 237.05/33.79 % (115789)dis+21_1_sil=32000:sas=cadical:random_seed=642955432:i=3773:amm=off_2919 on theBenchmark for (2919ds/3773Mi) % 237.05/33.79 % (115787)Instruction limit reached! % 300.43/42.63 % (115787)------------------------------ % 300.43/42.63 % (115787)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.43/42.63 % (115787)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.43/42.63 % (115787)CaDiCaL version: 2.1.3 % 300.43/42.63 % (115787)Termination reason: Instruction limit % 300.43/42.63 % (115787)Termination phase: Saturation % 300.43/42.63 % (115787)Time elapsed: 2.245 s % 300.43/42.63 % (115787)Peak memory usage: 27 MB % 300.43/42.63 % (115787)Instructions burned: 3513 (million) % 300.43/42.63 % (115791)ott+11_1_sil=16000:gs=on:random_seed=1087718095:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2917 on theBenchmark for (2917ds/2251Mi) % 300.43/42.63 % (115766)Instruction limit reached! % 300.43/42.63 % (115766)------------------------------ % 300.43/42.63 % (115766)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.43/42.63 % (115766)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.43/42.63 % (115766)CaDiCaL version: 2.1.3 % 300.43/42.63 % (115766)Termination reason: Instruction limit % 300.43/42.63 % (115766)Termination phase: Finite model building SAT solving % 300.43/42.63 % (115766)Time elapsed: 8.024 s % 300.43/42.63 % (115766)Peak memory usage: 155 MB % 300.43/42.63 % (115766)Instructions burned: 22065 (million) % 300.43/42.63 % (115793)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=670172679:fmbsr=1.6:i=67534_2910 on theBenchmark for (2910ds/67534Mi) % 300.43/42.63 % TRYING [7] % 300.43/42.63 % (115791)Instruction limit reached! % 300.43/42.63 % (115791)------------------------------ % 300.43/42.63 % (115791)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.43/42.63 % (115791)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.43/42.63 % (115791)CaDiCaL version: 2.1.3 % 300.43/42.63 % (115791)Termination reason: Instruction limit % 300.43/42.63 % (115791)Termination phase: Saturation % 300.43/42.63 % (115791)Time elapsed: 1.047 s % 300.43/42.63 % (115791)Peak memory usage: 18 MB % 300.43/42.63 % (115791)Instructions burned: 2252 (million) % 300.43/42.63 % (115795)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=2330039007:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2907 on theBenchmark for (2907ds/4591Mi) % 300.43/42.63 % (115789)Instruction limit reached! % 300.43/42.63 % (115789)------------------------------ % 300.43/42.63 % (115789)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.43/42.63 % (115789)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.43/42.63 % (115789)CaDiCaL version: 2.1.3 % 300.43/42.63 % (115789)Termination reason: Instruction limit % 300.43/42.63 % (115789)Termination phase: Saturation % 300.43/42.63 % (115789)Time elapsed: 2.377 s % 300.43/42.63 % (115789)Peak memory usage: 28 MB % 300.43/42.63 % (115789)Instructions burned: 3773 (million) % 300.43/42.63 % (115797)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=1333891921:i=29340_2895 on theBenchmark for (2895ds/29340Mi) % 300.43/42.63 % (115795)Instruction limit reached! % 300.43/42.63 % (115795)------------------------------ % 300.43/42.63 % (115795)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.43/42.63 % (115795)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.43/42.63 % (115795)CaDiCaL version: 2.1.3 % 300.43/42.63 % (115795)Termination reason: Instruction limit % 300.43/42.63 % (115795)Termination phase: Saturation % 300.43/42.63 % (115795)Time elapsed: 2.338 s % 300.43/42.63 % (115795)Peak memory usage: 32 MB % 300.43/42.63 % (115795)Instructions burned: 4592 (million) % 300.43/42.63 % (115799)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=3094830764:i=5211_2883 on theBenchmark for (2883ds/5211Mi) % 300.43/42.63 % TRYING [8] % 300.43/42.63 % (115799)Instruction limit reached! % 300.43/42.63 % (115799)------------------------------ % 300.43/42.63 % (115799)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.43/42.63 % (115799)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.43/42.63 % (115799)CaDiCaL version: 2.1.3 % 300.43/42.63 % (115799)Termination reason: Instruction limit % 300.43/42.63 % (115799)Termination phase: Saturation % 300.43/42.63 % (115799)Time elapsed: 2.848 s % 300.43/42.63 % (115799)Peak memory usage: 24 MB % 300.43/42.63 % (115799)Instructions burned: 5211 (million) % 300.43/42.63 % (115801)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=4193967494:i=5497:nm=2_2854 on theBenchmark for (2854ds/5497Mi) % 300.43/42.63 % TRYING [17] % 300.43/42.63 % (115801)Instruction limit reached! % 300.43/42.63 % (115801)------------------------------ % 300.43/42.63 % (1158 % 300.43/42.64 Terminated % 300.43/42.64 % Vampire exiting %------------------------------------------------------------------------------