%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWV970-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 : n012.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:45 PM UTC 2026 % Result : Timeout 300.33s 42.83s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.01 % Problem : SWV970-1 : TPTP v9.3.1. Released v4.1.0. % 0.00/0.03 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.00/0.10 % Computer : n012.cluster.edu % 0.00/0.10 % Model : x86_64 x86_64 % 0.00/0.10 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.00/0.10 % Memory : 8046.5625MB % 0.00/0.10 % OS : Linux 6.8.0-71-generic % 0.00/0.10 % CPULimit : 300 % 0.00/0.10 % WCLimit : 300 % 0.00/0.10 % DateTime : Mon Sep 28 13:03:04 UTC 2026 % 0.00/0.10 % CPUTime : % 0.00/0.10 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.09/0.12 Running first-order model finding % 0.09/0.12 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 % 3.84/0.71 % (3361283)Will run a generic schedule for satisfiability detection. % 3.84/0.71 % (3361289)% WARNING: option uhcvi not known. % 3.84/0.71 % (3361294)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3758154730:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 3.84/0.71 % (3361291)dis+10_1_sil=32000:sp=arity:random_seed=115782293:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 3.84/0.71 % (3361290)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=439684984:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 3.84/0.71 % (3361289)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=421623975:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 3.84/0.71 % (3361288)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1086904965_2999 on theBenchmark for (2999ds/0Mi) % 3.84/0.71 % (3361292)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2025395250:i=116_2999 on theBenchmark for (2999ds/116Mi) % 3.84/0.71 % (3361293)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1835402462:i=131_2999 on theBenchmark for (2999ds/131Mi) % 3.84/0.71 % (3361292)Instruction limit reached! % 3.84/0.71 % (3361292)------------------------------ % 3.84/0.71 % (3361292)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.84/0.71 % (3361292)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.84/0.71 % (3361292)CaDiCaL version: 2.1.3 % 3.84/0.71 % (3361292)Termination reason: Instruction limit % 3.84/0.71 % (3361292)Termination phase: Saturation % 3.84/0.71 % (3361292)Time elapsed: 0.029 s % 3.84/0.71 % (3361292)Peak memory usage: 12 MB % 3.84/0.71 % (3361292)Instructions burned: 119 (million) % 3.84/0.71 % TRYING [1] % 3.84/0.71 % TRYING [2] % 3.84/0.71 % (3361294)Instruction limit reached! % 3.84/0.71 % (3361294)------------------------------ % 3.84/0.71 % (3361294)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.84/0.71 % (3361294)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.84/0.71 % (3361294)CaDiCaL version: 2.1.3 % 3.84/0.71 % (3361294)Termination reason: Instruction limit % 3.84/0.71 % (3361294)Termination phase: Saturation % 3.84/0.71 % (3361294)Time elapsed: 0.032 s % 3.84/0.71 % (3361294)Peak memory usage: 11 MB % 3.84/0.71 % (3361294)Instructions burned: 162 (million) % 3.84/0.71 % (3361291)Instruction limit reached! % 3.84/0.71 % (3361291)------------------------------ % 3.84/0.71 % (3361291)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.84/0.71 % (3361291)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.84/0.71 % (3361291)CaDiCaL version: 2.1.3 % 3.84/0.71 % (3361291)Termination reason: Instruction limit % 3.84/0.71 % (3361291)Termination phase: Saturation % 3.84/0.71 % (3361291)Time elapsed: 0.034 s % 3.84/0.71 % (3361291)Peak memory usage: 12 MB % 3.84/0.71 % (3361291)Instructions burned: 104 (million) % 3.84/0.71 % (3361302)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1349131035:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 3.84/0.71 % (3361303)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=569772552:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 3.84/0.71 % (3361304)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=4194272688:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi) % 3.84/0.71 % (3361293)Instruction limit reached! % 3.84/0.71 % (3361293)------------------------------ % 3.84/0.71 % (3361293)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.84/0.71 % (3361293)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.84/0.71 % (3361293)CaDiCaL version: 2.1.3 % 3.84/0.71 % (3361293)Termination reason: Instruction limit % 3.84/0.71 % (3361293)Termination phase: Saturation % 3.84/0.71 % (3361293)Time elapsed: 0.048 s % 3.84/0.71 % (3361293)Peak memory usage: 13 MB % 3.84/0.71 % (3361293)Instructions burned: 132 (million) % 3.84/0.71 % (3361308)ott-21_1_sil=16000:fs=off:random_seed=40379607:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi) % 3.84/0.71 % TRYING [1] % 3.84/0.71 % TRYING [2] % 3.84/0.71 % (3361303)Instruction limit reached! % 3.84/0.71 % (3361303)------------------------------ % 3.84/0.71 % (3361303)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.84/0.71 % (3361303)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.82/2.66 % (3361303)CaDiCaL version: 2.1.3 % 16.82/2.66 % (3361303)Termination reason: Instruction limit % 16.82/2.66 % (3361303)Termination phase: Saturation % 16.82/2.66 % (3361303)Time elapsed: 0.042 s % 16.82/2.66 % (3361303)Peak memory usage: 13 MB % 16.82/2.66 % (3361303)Instructions burned: 131 (million) % 16.82/2.66 % (3361310)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=407220989:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 16.82/2.66 % (3361308)Instruction limit reached! % 16.82/2.66 % (3361308)------------------------------ % 16.82/2.66 % (3361308)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 16.82/2.66 % (3361308)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.82/2.66 % (3361308)CaDiCaL version: 2.1.3 % 16.82/2.66 % (3361308)Termination reason: Instruction limit % 16.82/2.66 % (3361308)Termination phase: Saturation % 16.82/2.66 % (3361308)Time elapsed: 0.049 s % 16.82/2.66 % (3361308)Peak memory usage: 12 MB % 16.82/2.66 % (3361308)Instructions burned: 181 (million) % 16.82/2.66 % (3361312)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1893962847:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 16.82/2.66 % TRYING [1] % 16.82/2.66 % (3361302)Instruction limit reached! % 16.82/2.66 % (3361302)------------------------------ % 16.82/2.66 % (3361302)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 16.82/2.66 % (3361302)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.82/2.66 % (3361302)CaDiCaL version: 2.1.3 % 16.82/2.66 % (3361302)Termination reason: Instruction limit % 16.82/2.66 % (3361302)Termination phase: Finite model building constraint generation % 16.82/2.66 % (3361302)Time elapsed: 0.136 s % 16.82/2.66 % (3361302)Peak memory usage: 21 MB % 16.82/2.66 % (3361302)Instructions burned: 714 (million) % 16.82/2.66 % (3361314)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=126837028:i=1179_2997 on theBenchmark for (2997ds/1179Mi) % 16.82/2.66 % (3361304)Instruction limit reached! % 16.82/2.66 % (3361304)------------------------------ % 16.82/2.66 % (3361304)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 16.82/2.66 % (3361304)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.82/2.66 % (3361304)CaDiCaL version: 2.1.3 % 16.82/2.66 % (3361304)Termination reason: Instruction limit % 16.82/2.66 % (3361304)Termination phase: Saturation % 16.82/2.66 % (3361304)Time elapsed: 0.172 s % 16.82/2.66 % (3361304)Peak memory usage: 18 MB % 16.82/2.66 % (3361304)Instructions burned: 689 (million) % 16.82/2.66 % (3361316)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2390597276:i=889:ins=1_2997 on theBenchmark for (2997ds/889Mi) % 16.82/2.66 % (3361310)Instruction limit reached! % 16.82/2.66 % (3361310)------------------------------ % 16.82/2.66 % (3361310)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 16.82/2.66 % (3361310)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.82/2.66 % (3361310)CaDiCaL version: 2.1.3 % 16.82/2.66 % (3361310)Termination reason: Instruction limit % 16.82/2.66 % (3361310)Termination phase: Saturation % 16.82/2.66 % (3361310)Time elapsed: 0.143 s % 16.82/2.66 % (3361310)Peak memory usage: 14 MB % 16.82/2.66 % (3361310)Instructions burned: 479 (million) % 16.82/2.66 % (3361318)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=4122597667:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2997 on theBenchmark for (2997ds/692Mi) % 16.82/2.66 % (3361316)Cannot represent all propositional literals internally % 16.82/2.66 % (3361316)Refutation not found, incomplete strategy % 16.82/2.66 % (3361316)------------------------------ % 16.82/2.66 % (3361316)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 16.82/2.66 % (3361316)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.82/2.66 % (3361316)CaDiCaL version: 2.1.3 % 16.82/2.66 % (3361316)Termination reason: Refutation not found, incomplete strategy % 16.82/2.66 % (3361316)Time elapsed: 0.029 s % 16.82/2.66 % (3361316)Peak memory usage: 12 MB % 16.82/2.66 % (3361316)Instructions burned: 105 (million) % 16.82/2.66 % (3361316)------------------------------ % 16.82/2.66 % (3361316)------------------------------ % 16.82/2.66 % (3361320)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1026109122:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi) % 16.82/2.66 % TRYING [2] % 16.82/2.66 % (3361312)Instruction limit reached! % 16.82/2.66 % (3361312)------------------------------ % 32.69/4.90 % (3361312)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 32.69/4.90 % (3361312)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.69/4.90 % (3361312)CaDiCaL version: 2.1.3 % 32.69/4.90 % (3361312)Termination reason: Instruction limit % 32.69/4.90 % (3361312)Termination phase: Finite model building constraint generation % 32.69/4.90 % (3361312)Time elapsed: 0.218 s % 32.69/4.90 % (3361312)Peak memory usage: 77 MB % 32.69/4.90 % (3361312)Instructions burned: 868 (million) % 32.69/4.90 % (3361322)fmb+10_1_sil=64000:random_seed=435193331:i=22061:nm=2:gsp=on_2996 on theBenchmark for (2996ds/22061Mi) % 32.69/4.90 % TRYING [1] % 32.69/4.90 % (3361318)Instruction limit reached! % 32.69/4.90 % (3361318)------------------------------ % 32.69/4.90 % (3361318)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 32.69/4.90 % (3361318)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.69/4.90 % (3361318)CaDiCaL version: 2.1.3 % 32.69/4.90 % (3361318)Termination reason: Instruction limit % 32.69/4.90 % (3361318)Termination phase: Saturation % 32.69/4.90 % (3361318)Time elapsed: 0.218 s % 32.69/4.90 % (3361318)Peak memory usage: 20 MB % 32.69/4.90 % (3361318)Instructions burned: 695 (million) % 32.69/4.90 % (3361324)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=713716081:i=9515:nm=5_2994 on theBenchmark for (2994ds/9515Mi) % 32.69/4.90 % (3361320)Instruction limit reached! % 32.69/4.90 % (3361320)------------------------------ % 32.69/4.90 % (3361320)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 32.69/4.90 % (3361320)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.69/4.90 % (3361320)CaDiCaL version: 2.1.3 % 32.69/4.90 % (3361320)Termination reason: Instruction limit % 32.69/4.90 % (3361320)Termination phase: Saturation % 32.69/4.90 % (3361320)Time elapsed: 0.230 s % 32.69/4.90 % (3361320)Peak memory usage: 15 MB % 32.69/4.90 % (3361320)Instructions burned: 884 (million) % 32.69/4.90 % (3361324)Cannot represent all propositional literals internally % 32.69/4.90 % (3361324)Refutation not found, incomplete strategy % 32.69/4.90 % (3361324)------------------------------ % 32.69/4.90 % (3361324)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 32.69/4.90 % (3361324)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.69/4.90 % (3361324)CaDiCaL version: 2.1.3 % 32.69/4.90 % (3361324)Termination reason: Refutation not found, incomplete strategy % 32.69/4.90 % (3361324)Time elapsed: 0.028 s % 32.69/4.90 % (3361324)Peak memory usage: 12 MB % 32.69/4.90 % (3361324)Instructions burned: 101 (million) % 32.69/4.90 % (3361324)------------------------------ % 32.69/4.90 % (3361324)------------------------------ % 32.69/4.90 % (3361326)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3263575514:fmbsr=1.7:i=920_2994 on theBenchmark for (2994ds/920Mi) % 32.69/4.90 % (3361327)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=3058605380:i=5131_2994 on theBenchmark for (2994ds/5131Mi) % 32.69/4.90 % TRYING [2] % 32.69/4.90 % (3361326)Cannot represent all propositional literals internally % 32.69/4.90 % (3361326)Refutation not found, incomplete strategy % 32.69/4.90 % (3361326)------------------------------ % 32.69/4.90 % (3361326)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 32.69/4.90 % (3361326)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.69/4.90 % (3361326)CaDiCaL version: 2.1.3 % 32.69/4.90 % (3361326)Termination reason: Refutation not found, incomplete strategy % 32.69/4.90 % (3361326)Time elapsed: 0.028 s % 32.69/4.90 % (3361326)Peak memory usage: 12 MB % 32.69/4.90 % (3361326)Instructions burned: 101 (million) % 32.69/4.90 % (3361326)------------------------------ % 32.69/4.90 % (3361326)------------------------------ % 32.69/4.90 % (3361314)Instruction limit reached! % 32.69/4.90 % (3361314)------------------------------ % 32.69/4.90 % (3361314)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 32.69/4.90 % (3361314)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.69/4.90 % (3361314)CaDiCaL version: 2.1.3 % 32.69/4.90 % (3361314)Termination reason: Instruction limit % 32.69/4.90 % (3361314)Termination phase: Saturation % 32.69/4.90 % (3361314)Time elapsed: 0.362 s % 32.69/4.90 % (3361314)Peak memory usage: 22 MB % 32.69/4.90 % (3361314)Instructions burned: 1182 (million) % 32.69/4.90 % (3361330)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=603151412:i=1472:ins=7:fdi=8:gsp=on_2994 on theBenchmark for (2994ds/1472Mi) % 39.04/5.86 % (3361331)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=2851453295:i=6324_2994 on theBenchmark for (2994ds/6324Mi) % 39.04/5.86 % (3361331)Cannot represent all propositional literals internally % 39.04/5.86 % (3361331)Refutation not found, incomplete strategy % 39.04/5.86 % (3361331)------------------------------ % 39.04/5.86 % (3361331)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 39.04/5.86 % (3361331)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.04/5.86 % (3361331)CaDiCaL version: 2.1.3 % 39.04/5.86 % (3361331)Termination reason: Refutation not found, incomplete strategy % 39.04/5.86 % (3361331)Time elapsed: 0.030 s % 39.04/5.86 % (3361331)Peak memory usage: 12 MB % 39.04/5.86 % (3361331)Instructions burned: 108 (million) % 39.04/5.86 % (3361331)------------------------------ % 39.04/5.86 % (3361331)------------------------------ % 39.04/5.86 % (3361334)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=3970171275:fmbsr=2.30978:i=2174_2993 on theBenchmark for (2993ds/2174Mi) % 39.04/5.86 % (3361334)Cannot represent all propositional literals internally % 39.04/5.87 % (3361334)Refutation not found, incomplete strategy % 39.04/5.87 % (3361334)------------------------------ % 39.04/5.87 % (3361334)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 39.04/5.87 % (3361334)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.04/5.87 % (3361334)CaDiCaL version: 2.1.3 % 39.04/5.87 % (3361334)Termination reason: Refutation not found, incomplete strategy % 39.04/5.87 % (3361334)Time elapsed: 0.144 s % 39.04/5.87 % (3361334)Peak memory usage: 16 MB % 39.04/5.87 % (3361334)Instructions burned: 554 (million) % 39.04/5.87 % (3361334)------------------------------ % 39.04/5.87 % (3361334)------------------------------ % 39.04/5.87 % (3361336)ott-2_1_sil=16000:newcnf=on:random_seed=1152428969:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2992 on theBenchmark for (2992ds/869Mi) % 39.04/5.87 % (3361336)Instruction limit reached! % 39.04/5.87 % (3361336)------------------------------ % 39.04/5.87 % (3361336)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 39.04/5.87 % (3361336)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.04/5.87 % (3361336)CaDiCaL version: 2.1.3 % 39.04/5.87 % (3361336)Termination reason: Instruction limit % 39.04/5.87 % (3361336)Termination phase: Saturation % 39.04/5.87 % (3361336)Time elapsed: 0.180 s % 39.04/5.87 % (3361336)Peak memory usage: 13 MB % 39.04/5.87 % (3361336)Instructions burned: 875 (million) % 39.04/5.87 % (3361338)ott+10_1_sil=32000:tgt=ground:random_seed=1490586061:i=5114:av=off_2990 on theBenchmark for (2990ds/5114Mi) % 39.04/5.87 % (3361330)Instruction limit reached! % 39.04/5.87 % (3361330)------------------------------ % 39.04/5.87 % (3361330)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 39.04/5.87 % (3361330)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.04/5.87 % (3361330)CaDiCaL version: 2.1.3 % 39.04/5.87 % (3361330)Termination reason: Instruction limit % 39.04/5.87 % (3361330)Termination phase: Saturation % 39.04/5.87 % (3361330)Time elapsed: 0.427 s % 39.04/5.87 % (3361330)Peak memory usage: 28 MB % 39.04/5.87 % (3361330)Instructions burned: 1474 (million) % 39.04/5.87 % (3361340)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2079345501:i=54282_2989 on theBenchmark for (2989ds/54282Mi) % 39.04/5.87 % TRYING [1] % 39.04/5.87 % TRYING [2] % 39.04/5.87 % (3361327)Instruction limit reached! % 39.04/5.87 % (3361327)------------------------------ % 39.04/5.87 % (3361327)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 39.04/5.87 % (3361327)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.04/5.87 % (3361327)CaDiCaL version: 2.1.3 % 39.04/5.87 % (3361327)Termination reason: Instruction limit % 39.04/5.87 % (3361327)Termination phase: Saturation % 39.04/5.87 % (3361327)Time elapsed: 1.433 s % 39.04/5.87 % (3361327)Peak memory usage: 26 MB % 39.04/5.87 % (3361327)Instructions burned: 5134 (million) % 39.04/5.87 % (3361342)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3063610641:i=3512:aac=none_2980 on theBenchmark for (2980ds/3512Mi) % 39.04/5.87 % (3361338)Instruction limit reached! % 39.04/5.87 % (3361338)------------------------------ % 39.04/5.87 % (3361338)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 39.04/5.87 % (3361338)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.04/5.87 % (3361338)CaDiCaL version: 2.1.3 % 39.04/5.87 % (3361338)Termination reason: Instruction limit % 76.66/11.03 % (3361338)Termination phase: Saturation % 76.66/11.03 % (3361338)Time elapsed: 1.553 s % 76.66/11.03 % (3361338)Peak memory usage: 56 MB % 76.66/11.03 % (3361338)Instructions burned: 5116 (million) % 76.66/11.03 % (3361344)dis+21_1_sil=32000:sas=cadical:random_seed=2787042115:i=3773:amm=off_2974 on theBenchmark for (2974ds/3773Mi) % 76.66/11.03 % (3361342)Instruction limit reached! % 76.66/11.03 % (3361342)------------------------------ % 76.66/11.03 % (3361342)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 76.66/11.03 % (3361342)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 76.66/11.03 % (3361342)CaDiCaL version: 2.1.3 % 76.66/11.03 % (3361342)Termination reason: Instruction limit % 76.66/11.03 % (3361342)Termination phase: Saturation % 76.66/11.03 % (3361342)Time elapsed: 0.991 s % 76.66/11.03 % (3361342)Peak memory usage: 22 MB % 76.66/11.03 % (3361342)Instructions burned: 3518 (million) % 76.66/11.03 % (3361346)ott+11_1_sil=16000:gs=on:random_seed=6576176:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2970 on theBenchmark for (2970ds/2251Mi) % 76.66/11.03 % (3361344)Instruction limit reached! % 76.66/11.03 % (3361344)------------------------------ % 76.66/11.03 % (3361344)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 76.66/11.03 % (3361344)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 76.66/11.03 % (3361344)CaDiCaL version: 2.1.3 % 76.66/11.03 % (3361344)Termination reason: Instruction limit % 76.66/11.03 % (3361344)Termination phase: Saturation % 76.66/11.03 % (3361344)Time elapsed: 0.980 s % 76.66/11.03 % (3361344)Peak memory usage: 27 MB % 76.66/11.03 % (3361344)Instructions burned: 3774 (million) % 76.66/11.03 % (3361348)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=1180918915:fmbsr=1.6:i=67534_2964 on theBenchmark for (2964ds/67534Mi) % 76.66/11.03 % (3361348)Cannot represent all propositional literals internally % 76.66/11.03 % (3361348)Refutation not found, incomplete strategy % 76.66/11.03 % (3361348)------------------------------ % 76.66/11.03 % (3361348)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 76.66/11.03 % (3361348)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 76.66/11.03 % (3361348)CaDiCaL version: 2.1.3 % 76.66/11.03 % (3361348)Termination reason: Refutation not found, incomplete strategy % 76.66/11.03 % (3361348)Time elapsed: 0.034 s % 76.66/11.03 % (3361348)Peak memory usage: 12 MB % 76.66/11.03 % (3361348)Instructions burned: 131 (million) % 76.66/11.03 % (3361348)------------------------------ % 76.66/11.03 % (3361348)------------------------------ % 76.66/11.03 % (3361350)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=4241413153:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2964 on theBenchmark for (2964ds/4591Mi) % 76.66/11.03 % (3361346)Instruction limit reached! % 76.66/11.03 % (3361346)------------------------------ % 76.66/11.03 % (3361346)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 76.66/11.03 % (3361346)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 76.66/11.03 % (3361346)CaDiCaL version: 2.1.3 % 76.66/11.03 % (3361346)Termination reason: Instruction limit % 76.66/11.03 % (3361346)Termination phase: Saturation % 76.66/11.03 % (3361346)Time elapsed: 0.652 s % 76.66/11.03 % (3361346)Peak memory usage: 31 MB % 76.66/11.03 % (3361346)Instructions burned: 2253 (million) % 76.66/11.03 % (3361352)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=739328131:i=29340_2963 on theBenchmark for (2963ds/29340Mi) % 76.66/11.03 % (3361288)Cannot represent all propositional literals internally % 76.66/11.03 % (3361350)Instruction limit reached! % 76.66/11.03 % (3361350)------------------------------ % 76.66/11.03 % (3361350)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 76.66/11.03 % (3361350)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 76.66/11.03 % (3361350)CaDiCaL version: 2.1.3 % 76.66/11.03 % (3361350)Termination reason: Instruction limit % 76.66/11.03 % (3361350)Termination phase: Saturation % 76.66/11.03 % (3361350)Time elapsed: 0.926 s % 76.66/11.03 % (3361350)Peak memory usage: 25 MB % 76.66/11.03 % (3361350)Instructions burned: 4593 (million) % 76.66/11.03 % (3361354)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=1431458910:i=5211_2954 on theBenchmark for (2954ds/5211Mi) % 76.66/11.03 % (3361288)Refutation not found, incomplete strategy % 76.66/11.03 % (3361288)------------------------------ % 76.66/11.03 % (3361288)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 76.66/11.03 % (3361288)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 84.43/12.15 % (3361288)CaDiCaL version: 2.1.3 % 84.43/12.15 % (3361288)Termination reason: Refutation not found, incomplete strategy % 84.43/12.15 % (3361288)Time elapsed: 4.743 s % 84.43/12.15 % (3361288)Peak memory usage: 714 MB % 84.43/12.15 % (3361288)Instructions burned: 12190 (million) % 84.43/12.15 % (3361288)------------------------------ % 84.43/12.15 % (3361288)------------------------------ % 84.43/12.15 % (3361356)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=3190302345:i=5497:nm=2_2951 on theBenchmark for (2951ds/5497Mi) % 84.43/12.15 % (3361356)Cannot represent all propositional literals internally % 84.43/12.15 % (3361356)Refutation not found, incomplete strategy % 84.43/12.15 % (3361356)------------------------------ % 84.43/12.15 % (3361356)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 84.43/12.15 % (3361356)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 84.43/12.15 % (3361356)CaDiCaL version: 2.1.3 % 84.43/12.15 % (3361356)Termination reason: Refutation not found, incomplete strategy % 84.43/12.15 % (3361356)Time elapsed: 0.030 s % 84.43/12.15 % (3361356)Peak memory usage: 12 MB % 84.43/12.15 % (3361356)Instructions burned: 108 (million) % 84.43/12.15 % (3361356)------------------------------ % 84.43/12.15 % (3361356)------------------------------ % 84.43/12.15 % (3361358)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=1051686446:fmbsr=2:i=46332_2951 on theBenchmark for (2951ds/46332Mi) % 84.43/12.15 % (3361358)Cannot represent all propositional literals internally % 84.43/12.15 % (3361358)Refutation not found, incomplete strategy % 84.43/12.15 % (3361358)------------------------------ % 84.43/12.15 % (3361358)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 84.43/12.15 % (3361358)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 84.43/12.15 % (3361358)CaDiCaL version: 2.1.3 % 84.43/12.15 % (3361358)Termination reason: Refutation not found, incomplete strategy % 84.43/12.15 % (3361358)Time elapsed: 0.034 s % 84.43/12.15 % (3361358)Peak memory usage: 12 MB % 84.43/12.15 % (3361358)Instructions burned: 131 (million) % 84.43/12.15 % (3361358)------------------------------ % 84.43/12.15 % (3361358)------------------------------ % 84.43/12.15 % (3361360)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=3531421877:i=14071_2950 on theBenchmark for (2950ds/14071Mi) % 84.43/12.15 % (3361360)Cannot represent all propositional literals internally % 84.43/12.15 % (3361360)Refutation not found, incomplete strategy % 84.43/12.15 % (3361360)------------------------------ % 84.43/12.15 % (3361360)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 84.43/12.15 % (3361360)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 84.43/12.15 % (3361360)CaDiCaL version: 2.1.3 % 84.43/12.15 % (3361360)Termination reason: Refutation not found, incomplete strategy % 84.43/12.15 % (3361360)Time elapsed: 0.030 s % 84.43/12.15 % (3361360)Peak memory usage: 12 MB % 84.43/12.15 % (3361360)Instructions burned: 108 (million) % 84.43/12.15 % (3361360)------------------------------ % 84.43/12.15 % (3361360)------------------------------ % 84.43/12.15 % (3361362)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2074720027:i=22565:add=on:rawr=on_2950 on theBenchmark for (2950ds/22565Mi) % 84.43/12.15 % (3361340)Cannot represent all propositional literals internally % 84.43/12.15 % (3361354)Instruction limit reached! % 84.43/12.15 % (3361354)------------------------------ % 84.43/12.15 % (3361354)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 84.43/12.15 % (3361354)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 84.43/12.15 % (3361354)CaDiCaL version: 2.1.3 % 84.43/12.15 % (3361354)Termination reason: Instruction limit % 84.43/12.15 % (3361354)Termination phase: Saturation % 84.43/12.15 % (3361354)Time elapsed: 1.015 s % 84.43/12.15 % (3361354)Peak memory usage: 16 MB % 84.43/12.15 % (3361354)Instructions burned: 5216 (million) % 84.43/12.15 % (3361364)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=1314751949:i=8173:av=off_2944 on theBenchmark for (2944ds/8173Mi) % 84.43/12.15 % (3361340)Refutation not found, incomplete strategy % 84.43/12.15 % (3361340)------------------------------ % 84.43/12.15 % (3361340)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 84.43/12.15 % (3361340)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 84.43/12.15 % (3361340)CaDiCaL version: 2.1.3 % 84.43/12.15 % (3361340)Termination reason: Refutation not found, incomplete strategy % 96.96/13.90 % (3361340)Time elapsed: 4.711 s % 96.96/13.90 % (3361340)Peak memory usage: 714 MB % 96.96/13.90 % (3361340)Instructions burned: 12190 (million) % 96.96/13.90 % (3361340)------------------------------ % 96.96/13.90 % (3361340)------------------------------ % 96.96/13.90 % (3361366)dis+10_16:1_sil=16000:random_seed=2598278880:i=9155:fsr=off_2942 on theBenchmark for (2942ds/9155Mi) % 96.96/13.90 % (3361364)Instruction limit reached! % 96.96/13.90 % (3361364)------------------------------ % 96.96/13.90 % (3361364)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 96.96/13.90 % (3361364)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 96.96/13.90 % (3361364)CaDiCaL version: 2.1.3 % 96.96/13.90 % (3361364)Termination reason: Instruction limit % 96.96/13.90 % (3361364)Termination phase: Saturation % 96.96/13.90 % (3361364)Time elapsed: 2.192 s % 96.96/13.90 % (3361364)Peak memory usage: 85 MB % 96.96/13.90 % (3361364)Instructions burned: 8177 (million) % 96.96/13.90 % (3361368)ott-3_8_sil=64000:random_seed=2422575779:i=20139:bs=on_2922 on theBenchmark for (2922ds/20139Mi) % 96.96/13.90 % (3361366)Instruction limit reached! % 96.96/13.90 % (3361366)------------------------------ % 96.96/13.90 % (3361366)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 96.96/13.90 % (3361366)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 96.96/13.90 % (3361366)CaDiCaL version: 2.1.3 % 96.96/13.90 % (3361366)Termination reason: Instruction limit % 96.96/13.90 % (3361366)Termination phase: Saturation % 96.96/13.90 % (3361366)Time elapsed: 2.412 s % 96.96/13.90 % (3361366)Peak memory usage: 54 MB % 96.96/13.90 % (3361366)Instructions burned: 9158 (million) % 96.96/13.90 % (3361370)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=3739059837:fmbsr=2:i=32576_2917 on theBenchmark for (2917ds/32576Mi) % 96.96/13.90 % (3361370)Cannot represent all propositional literals internally % 96.96/13.90 % (3361370)Refutation not found, incomplete strategy % 96.96/13.90 % (3361370)------------------------------ % 96.96/13.90 % (3361370)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 96.96/13.90 % (3361370)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 96.96/13.90 % (3361370)CaDiCaL version: 2.1.3 % 96.96/13.90 % (3361370)Termination reason: Refutation not found, incomplete strategy % 96.96/13.90 % (3361370)Time elapsed: 0.031 s % 96.96/13.90 % (3361370)Peak memory usage: 12 MB % 96.96/13.90 % (3361370)Instructions burned: 111 (million) % 96.96/13.90 % (3361370)------------------------------ % 96.96/13.90 % (3361370)------------------------------ % 96.96/13.90 % (3361372)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=1568046629:i=11404_2917 on theBenchmark for (2917ds/11404Mi) % 96.96/13.90 % (3361362)Instruction limit reached! % 96.96/13.90 % (3361362)------------------------------ % 96.96/13.90 % (3361362)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 96.96/13.90 % (3361362)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 96.96/13.90 % (3361362)CaDiCaL version: 2.1.3 % 96.96/13.90 % (3361362)Termination reason: Instruction limit % 96.96/13.90 % (3361362)Termination phase: Saturation % 96.96/13.90 % (3361362)Time elapsed: 3.516 s % 96.96/13.90 % (3361362)Peak memory usage: 39 MB % 96.96/13.90 % (3361362)Instructions burned: 22570 (million) % 96.96/13.90 % (3361374)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=1695164889:i=14134_2915 on theBenchmark for (2915ds/14134Mi) % 96.96/13.90 % (3361322)Instruction limit reached! % 96.96/13.90 % (3361322)------------------------------ % 96.96/13.90 % (3361322)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 96.96/13.90 % (3361322)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 96.96/13.90 % (3361322)CaDiCaL version: 2.1.3 % 96.96/13.90 % (3361322)Termination reason: Instruction limit % 96.96/13.90 % (3361322)Termination phase: Finite model building SAT solving % 96.96/13.90 % (3361322)Time elapsed: 8.470 s % 96.96/13.90 % (3361322)Peak memory usage: 685 MB % 96.96/13.90 % (3361322)Instructions burned: 22062 (million) % 96.96/13.90 % (3361376)dis+33_16_sil=32000:sac=on:random_seed=2039395412:i=15851:nm=0_2910 on theBenchmark for (2910ds/15851Mi) % 96.96/13.90 % (3361368)Instruction limit reached! % 96.96/13.90 % (3361368)------------------------------ % 96.96/13.90 % (3361368)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 96.96/13.90 % (3361368)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 96.96/13.90 % (3361368)CaDiCaL version: 2.1.3 % 96.96/13.90 % (3361368)Termination reason: Instruction limit % 96.96/13.90 % (3361368)Termination phase: Saturation % 103.88/15.01 % (3361368)Time elapsed: 3.114 s % 103.88/15.01 % (3361368)Peak memory usage: 13 MB % 103.88/15.01 % (3361368)Instructions burned: 20140 (million) % 103.88/15.01 % (3361378)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=2559760766:avsq=on:i=17627:add=on:amm=off_2890 on theBenchmark for (2890ds/17627Mi) % 103.88/15.01 % (3361352)Instruction limit reached! % 103.88/15.01 % (3361352)------------------------------ % 103.88/15.01 % (3361352)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 103.88/15.01 % (3361352)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 103.88/15.01 % (3361352)CaDiCaL version: 2.1.3 % 103.88/15.01 % (3361352)Termination reason: Instruction limit % 103.88/15.01 % (3361352)Termination phase: Saturation % 103.88/15.01 % (3361352)Time elapsed: 7.928 s % 103.88/15.01 % (3361352)Peak memory usage: 268 MB % 103.88/15.01 % (3361352)Instructions burned: 29341 (million) % 103.88/15.01 % (3361380)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=3832269469:s2a=on:i=53295_2883 on theBenchmark for (2883ds/53295Mi) % 103.88/15.01 % (3361372)Instruction limit reached! % 103.88/15.01 % (3361372)------------------------------ % 103.88/15.01 % (3361372)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 103.88/15.01 % (3361372)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 103.88/15.01 % (3361372)CaDiCaL version: 2.1.3 % 103.88/15.01 % (3361372)Termination reason: Instruction limit % 103.88/15.01 % (3361372)Termination phase: Saturation % 103.88/15.01 % (3361372)Time elapsed: 3.484 s % 103.88/15.01 % (3361372)Peak memory usage: 114 MB % 103.88/15.01 % (3361372)Instructions burned: 11407 (million) % 103.88/15.01 % (3361382)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=4154098166:i=26857:ins=20_2882 on theBenchmark for (2882ds/26857Mi) % 103.88/15.01 % (3361382)Cannot represent all propositional literals internally % 103.88/15.01 % (3361382)Refutation not found, incomplete strategy % 103.88/15.01 % (3361382)------------------------------ % 103.88/15.01 % (3361382)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 103.88/15.01 % (3361382)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 103.88/15.01 % (3361382)CaDiCaL version: 2.1.3 % 103.88/15.01 % (3361382)Termination reason: Refutation not found, incomplete strategy % 103.88/15.01 % (3361382)Time elapsed: 0.028 s % 103.88/15.01 % (3361382)Peak memory usage: 12 MB % 103.88/15.01 % (3361382)Instructions burned: 101 (million) % 103.88/15.01 % (3361382)------------------------------ % 103.88/15.01 % (3361382)------------------------------ % 103.88/15.01 % (3361384)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=416618915:i=28120:bs=on:fsr=off_2881 on theBenchmark for (2881ds/28120Mi) % 103.88/15.01 % (3361374)Instruction limit reached! % 103.88/15.01 % (3361374)------------------------------ % 103.88/15.01 % (3361374)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 103.88/15.01 % (3361374)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 103.88/15.01 % (3361374)CaDiCaL version: 2.1.3 % 103.88/15.01 % (3361374)Termination reason: Instruction limit % 103.88/15.01 % (3361374)Termination phase: Saturation % 103.88/15.01 % (3361374)Time elapsed: 3.435 s % 103.88/15.01 % (3361374)Peak memory usage: 49 MB % 103.88/15.01 % (3361374)Instructions burned: 14136 (million) % 103.88/15.01 % (3361386)fmb+10_1_sil=256000:fmbss=7:random_seed=779935961:fmbsr=1.6:i=182295_2880 on theBenchmark for (2880ds/182295Mi) % 103.88/15.01 % (3361386)Cannot represent all propositional literals internally % 103.88/15.01 % (3361386)Refutation not found, incomplete strategy % 103.88/15.01 % (3361386)------------------------------ % 103.88/15.01 % (3361386)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 103.88/15.01 % (3361386)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 103.88/15.01 % (3361386)CaDiCaL version: 2.1.3 % 103.88/15.01 % (3361386)Termination reason: Refutation not found, incomplete strategy % 103.88/15.01 % (3361386)Time elapsed: 0.028 s % 103.88/15.01 % (3361386)Peak memory usage: 12 MB % 103.88/15.01 % (3361386)Instructions burned: 101 (million) % 103.88/15.01 % (3361386)------------------------------ % 103.88/15.01 % (3361386)------------------------------ % 103.88/15.01 % (3361388)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=1846787913:i=44625:gsp=on_2880 on theBenchmark for (2880ds/44625Mi) % 103.88/15.01 % (3361388)Cannot represent all propositional literals internally % 103.88/15.01 % (3361388)Refutation not found, incomplete strategy % 103.88/15.01 % (3361388)------------------------------ % 103.88/15.01 % (3361388)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 118.94/17.05 % (3361388)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 118.94/17.05 % (3361388)CaDiCaL version: 2.1.3 % 118.94/17.05 % (3361388)Termination reason: Refutation not found, incomplete strategy % 118.94/17.05 % (3361388)Time elapsed: 0.027 s % 118.94/17.05 % (3361388)Peak memory usage: 12 MB % 118.94/17.05 % (3361388)Instructions burned: 100 (million) % 118.94/17.05 % (3361388)------------------------------ % 118.94/17.05 % (3361388)------------------------------ % 118.94/17.05 % (3361390)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=2815783633:i=160505_2879 on theBenchmark for (2879ds/160505Mi) % 118.94/17.05 % (3361390)Cannot represent all propositional literals internally % 118.94/17.05 % (3361390)Refutation not found, incomplete strategy % 118.94/17.05 % (3361390)------------------------------ % 118.94/17.05 % (3361390)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 118.94/17.05 % (3361390)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 118.94/17.05 % (3361390)CaDiCaL version: 2.1.3 % 118.94/17.05 % (3361390)Termination reason: Refutation not found, incomplete strategy % 118.94/17.05 % (3361390)Time elapsed: 0.028 s % 118.94/17.05 % (3361390)Peak memory usage: 12 MB % 118.94/17.05 % (3361390)Instructions burned: 101 (million) % 118.94/17.05 % (3361390)------------------------------ % 118.94/17.05 % (3361390)------------------------------ % 118.94/17.05 % (3361392)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=1399091743:fmbsr=1.3:i=225729_2879 on theBenchmark for (2879ds/225729Mi) % 118.94/17.05 % (3361392)Cannot represent all propositional literals internally % 118.94/17.05 % (3361392)Refutation not found, incomplete strategy % 118.94/17.05 % (3361392)------------------------------ % 118.94/17.05 % (3361392)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 118.94/17.05 % (3361392)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 118.94/17.05 % (3361392)CaDiCaL version: 2.1.3 % 118.94/17.05 % (3361392)Termination reason: Refutation not found, incomplete strategy % 118.94/17.05 % (3361392)Time elapsed: 0.030 s % 118.94/17.05 % (3361392)Peak memory usage: 12 MB % 118.94/17.05 % (3361392)Instructions burned: 108 (million) % 118.94/17.05 % (3361392)------------------------------ % 118.94/17.05 % (3361392)------------------------------ % 118.94/17.05 % (3361394)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=4110130130:fmbsr=2:i=185024:ins=7_2878 on theBenchmark for (2878ds/185024Mi) % 118.94/17.05 % (3361394)Cannot represent all propositional literals internally % 118.94/17.05 % (3361394)Refutation not found, incomplete strategy % 118.94/17.05 % (3361394)------------------------------ % 118.94/17.05 % (3361394)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 118.94/17.05 % (3361394)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 118.94/17.05 % (3361394)CaDiCaL version: 2.1.3 % 118.94/17.05 % (3361394)Termination reason: Refutation not found, incomplete strategy % 118.94/17.05 % (3361394)Time elapsed: 0.029 s % 118.94/17.05 % (3361394)Peak memory usage: 12 MB % 118.94/17.05 % (3361394)Instructions burned: 108 (million) % 118.94/17.05 % (3361394)------------------------------ % 118.94/17.05 % (3361394)------------------------------ % 118.94/17.05 % (3361396)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=3126226692:rtra=on_2878 on theBenchmark for (2878ds/0Mi) % 118.94/17.05 % TRYING [1] % 118.94/17.05 % TRYING [2] % 118.94/17.05 % (3361290)Instruction limit reached! % 118.94/17.05 % (3361290)------------------------------ % 118.94/17.05 % (3361290)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 118.94/17.05 % (3361290)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 118.94/17.05 % (3361290)CaDiCaL version: 2.1.3 % 118.94/17.05 % (3361290)Termination reason: Instruction limit % 118.94/17.05 % (3361290)Termination phase: Saturation % 118.94/17.05 % (3361290)Time elapsed: 12.692 s % 118.94/17.05 % (3361290)Peak memory usage: 54 MB % 118.94/17.05 % (3361290)Instructions burned: 88025 (million) % 118.94/17.05 % (3361398)% WARNING: option uhcvi not known. % 118.94/17.05 % (3361398)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1100511903:i=271062:add=off:rtra=on:rawr=on_2872 on theBenchmark for (2872ds/271062Mi) % 118.94/17.05 % (3361376)Instruction limit reached! % 118.94/17.05 % (3361376)------------------------------ % 118.94/17.05 % (3361376)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 118.94/17.05 % (3361376)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 118.94/17.05 % (3361376)CaDiCaL version: 2.1.3 % 118.94/17.05 % (3361376)Termination reason: Instruction limit % 120.84/18.19 % (3361376)Termination phase: Saturation % 120.84/18.19 % (3361376)Time elapsed: 4.856 s % 120.84/18.19 % (3361376)Peak memory usage: 146 MB % 120.84/18.19 % (3361376)Instructions burned: 15852 (million) % 120.84/18.19 % (3361400)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3050048146:i=176048:add=on:rtra=on:rawr=on_2862 on theBenchmark for (2862ds/176048Mi) % 120.84/18.19 % (3361378)Instruction limit reached! % 120.84/18.19 % (3361378)------------------------------ % 120.84/18.19 % (3361378)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 120.84/18.19 % (3361378)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 120.84/18.19 % (3361378)CaDiCaL version: 2.1.3 % 120.84/18.19 % (3361378)Termination reason: Instruction limit % 120.84/18.19 % (3361378)Termination phase: Saturation % 120.84/18.19 % (3361378)Time elapsed: 3.355 s % 120.84/18.19 % (3361378)Peak memory usage: 63 MB % 120.84/18.19 % (3361378)Instructions burned: 17630 (million) % 120.84/18.19 % (3361402)dis+10_1_sil=32000:si=on:sp=arity:random_seed=3380179538:i=206:fgj=on:rtra=on_2857 on theBenchmark for (2857ds/206Mi) % 120.84/18.19 % (3361402)Instruction limit reached! % 120.84/18.19 % (3361402)------------------------------ % 120.84/18.19 % (3361402)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 120.84/18.19 % (3361402)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 120.84/18.19 % (3361402)CaDiCaL version: 2.1.3 % 120.84/18.19 % (3361402)Termination reason: Instruction limit % 120.84/18.19 % (3361402)Termination phase: Saturation % 120.84/18.19 % (3361402)Time elapsed: 0.066 s % 120.84/18.19 % (3361402)Peak memory usage: 13 MB % 120.84/18.19 % (3361402)Instructions burned: 207 (million) % 120.84/18.19 % (3361404)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=2107899908:i=232:rtra=on_2856 on theBenchmark for (2856ds/232Mi) % 120.84/18.19 % (3361404)Instruction limit reached! % 120.84/18.19 % (3361404)------------------------------ % 120.84/18.19 % (3361404)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 120.84/18.19 % (3361404)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 120.84/18.19 % (3361404)CaDiCaL version: 2.1.3 % 120.84/18.19 % (3361404)Termination reason: Instruction limit % 120.84/18.19 % (3361404)Termination phase: Saturation % 120.84/18.19 % (3361404)Time elapsed: 0.056 s % 120.84/18.19 % (3361404)Peak memory usage: 12 MB % 120.84/18.19 % (3361404)Instructions burned: 232 (million) % 120.84/18.19 % (3361406)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=3110340211:i=262:rtra=on_2855 on theBenchmark for (2855ds/262Mi) % 120.84/18.19 % (3361406)Instruction limit reached! % 120.84/18.19 % (3361406)------------------------------ % 120.84/18.19 % (3361406)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 120.84/18.19 % (3361406)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 120.84/18.19 % (3361406)CaDiCaL version: 2.1.3 % 120.84/18.19 % (3361406)Termination reason: Instruction limit % 120.84/18.19 % (3361406)Termination phase: Saturation % 120.84/18.19 % (3361406)Time elapsed: 0.087 s % 120.84/18.19 % (3361406)Peak memory usage: 15 MB % 120.84/18.19 % (3361406)Instructions burned: 262 (million) % 120.84/18.19 % (3361408)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=3263905157:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2854 on theBenchmark for (2854ds/318Mi) % 120.84/18.19 % (3361408)Instruction limit reached! % 120.84/18.19 % (3361408)------------------------------ % 120.84/18.19 % (3361408)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 120.84/18.19 % (3361408)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 120.84/18.19 % (3361408)CaDiCaL version: 2.1.3 % 120.84/18.19 % (3361408)Termination reason: Instruction limit % 120.84/18.19 % (3361408)Termination phase: Saturation % 120.84/18.19 % (3361408)Time elapsed: 0.060 s % 120.84/18.19 % (3361408)Peak memory usage: 12 MB % 120.84/18.19 % (3361408)Instructions burned: 324 (million) % 120.84/18.19 % (3361410)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=3130393707:i=1428:nm=2:rtra=on_2853 on theBenchmark for (2853ds/1428Mi) % 120.84/18.19 % TRYING [1] % 120.84/18.19 % TRYING [2] % 120.84/18.19 % (3361410)Instruction limit reached! % 120.84/18.19 % (3361410)------------------------------ % 120.84/18.19 % (3361410)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 120.84/18.19 % (3361410)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 120.84/18.19 % (3361410)CaDiCaL version: 2.1.3 % 120.84/18.19 % (3361410)Termination reason: Instruction limit % 120.84/18.19 % (3361410)Termination phase: Finite model building constraint generation % 154.22/22.09 % (3361410)Time elapsed: 0.267 s % 154.22/22.09 % (3361410)Peak memory usage: 31 MB % 154.22/22.09 % (3361410)Instructions burned: 1432 (million) % 154.22/22.09 % (3361412)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=188088792:i=262:bd=preordered:rtra=on:fsd=on_2851 on theBenchmark for (2851ds/262Mi) % 154.22/22.09 % (3361412)Instruction limit reached! % 154.22/22.09 % (3361412)------------------------------ % 154.22/22.09 % (3361412)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 154.22/22.09 % (3361412)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 154.22/22.09 % (3361412)CaDiCaL version: 2.1.3 % 154.22/22.09 % (3361412)Termination reason: Instruction limit % 154.22/22.09 % (3361412)Termination phase: Saturation % 154.22/22.09 % (3361412)Time elapsed: 0.087 s % 154.22/22.09 % (3361412)Peak memory usage: 16 MB % 154.22/22.09 % (3361412)Instructions burned: 264 (million) % 154.22/22.09 % (3361414)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:si=on:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=2269851388:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2850 on theBenchmark for (2850ds/1368Mi) % 154.22/22.09 % (3361414)Instruction limit reached! % 154.22/22.09 % (3361414)------------------------------ % 154.22/22.09 % (3361414)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 154.22/22.09 % (3361414)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 154.22/22.09 % (3361414)CaDiCaL version: 2.1.3 % 154.22/22.09 % (3361414)Termination reason: Instruction limit % 154.22/22.09 % (3361414)Termination phase: Saturation % 154.22/22.09 % (3361414)Time elapsed: 0.355 s % 154.22/22.09 % (3361414)Peak memory usage: 23 MB % 154.22/22.09 % (3361414)Instructions burned: 1369 (million) % 154.22/22.09 % (3361416)ott-21_1_sil=16000:si=on:fs=off:random_seed=2663131373:i=360:av=off:fsr=off:rtra=on_2846 on theBenchmark for (2846ds/360Mi) % 154.22/22.09 % (3361416)Instruction limit reached! % 154.22/22.09 % (3361416)------------------------------ % 154.22/22.09 % (3361416)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 154.22/22.09 % (3361416)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 154.22/22.09 % (3361416)CaDiCaL version: 2.1.3 % 154.22/22.09 % (3361416)Termination reason: Instruction limit % 154.22/22.09 % (3361416)Termination phase: Saturation % 154.22/22.09 % (3361416)Time elapsed: 0.099 s % 154.22/22.09 % (3361416)Peak memory usage: 12 MB % 154.22/22.09 % (3361416)Instructions burned: 364 (million) % 154.22/22.09 % (3361418)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1393915798:i=954:bd=all:rtra=on_2845 on theBenchmark for (2845ds/954Mi) % 154.22/22.09 % (3361418)Instruction limit reached! % 154.22/22.09 % (3361418)------------------------------ % 154.22/22.09 % (3361418)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 154.22/22.09 % (3361418)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 154.22/22.09 % (3361418)CaDiCaL version: 2.1.3 % 154.22/22.09 % (3361418)Termination reason: Instruction limit % 154.22/22.09 % (3361418)Termination phase: Saturation % 154.22/22.09 % (3361418)Time elapsed: 0.275 s % 154.22/22.09 % (3361418)Peak memory usage: 17 MB % 154.22/22.09 % (3361418)Instructions burned: 955 (million) % 154.22/22.09 % (3361420)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=1385746186:fmbsr=1.3:i=1730:ins=25:rtra=on_2842 on theBenchmark for (2842ds/1730Mi) % 154.22/22.09 % TRYING [1] % 154.22/22.09 % TRYING [2] % 154.22/22.09 % (3361420)Instruction limit reached! % 154.22/22.09 % (3361420)------------------------------ % 154.22/22.09 % (3361420)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 154.22/22.09 % (3361420)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 154.22/22.09 % (3361420)CaDiCaL version: 2.1.3 % 154.22/22.09 % (3361420)Termination reason: Instruction limit % 154.22/22.09 % (3361420)Termination phase: Finite model building constraint generation % 154.22/22.09 % (3361420)Time elapsed: 0.386 s % 154.22/22.09 % (3361420)Peak memory usage: 116 MB % 154.22/22.09 % (3361420)Instructions burned: 1732 (million) % 154.22/22.09 % (3361422)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=544529190:i=2358:rtra=on_2838 on theBenchmark for (2838ds/2358Mi) % 154.22/22.09 % (3361422)Instruction limit reached! % 154.22/22.09 % (3361422)------------------------------ % 154.22/22.09 % (3361422)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 154.22/22.09 % (3361422)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 191.90/28.23 % (3361422)CaDiCaL version: 2.1.3 % 191.90/28.23 % (3361422)Termination reason: Instruction limit % 191.90/28.23 % (3361422)Termination phase: Saturation % 191.90/28.23 % (3361422)Time elapsed: 0.747 s % 191.90/28.23 % (3361422)Peak memory usage: 31 MB % 191.90/28.23 % (3361422)Instructions burned: 2361 (million) % 191.90/28.23 % (3361424)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=3097051441:i=1778:ins=1:rtra=on_2830 on theBenchmark for (2830ds/1778Mi) % 191.90/28.23 % (3361424)Cannot represent all propositional literals internally % 191.90/28.23 % (3361424)Refutation not found, incomplete strategy % 191.90/28.23 % (3361424)------------------------------ % 191.90/28.23 % (3361424)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 191.90/28.23 % (3361424)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 191.90/28.23 % (3361424)CaDiCaL version: 2.1.3 % 191.90/28.23 % (3361424)Termination reason: Refutation not found, incomplete strategy % 191.90/28.23 % (3361424)Time elapsed: 0.029 s % 191.90/28.23 % (3361424)Peak memory usage: 12 MB % 191.90/28.23 % (3361424)Instructions burned: 106 (million) % 191.90/28.23 % (3361424)------------------------------ % 191.90/28.23 % (3361424)------------------------------ % 191.90/28.23 % (3361426)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:si=on:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=942690738:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2830 on theBenchmark for (2830ds/1384Mi) % 191.90/28.23 % (3361396)Cannot represent all propositional literals internally % 191.90/28.23 % (3361426)Instruction limit reached! % 191.90/28.23 % (3361426)------------------------------ % 191.90/28.23 % (3361426)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 191.90/28.23 % (3361426)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 191.90/28.23 % (3361426)CaDiCaL version: 2.1.3 % 191.90/28.23 % (3361426)Termination reason: Instruction limit % 191.90/28.23 % (3361426)Termination phase: Saturation % 191.90/28.23 % (3361426)Time elapsed: 0.451 s % 191.90/28.23 % (3361426)Peak memory usage: 26 MB % 191.90/28.23 % (3361426)Instructions burned: 1384 (million) % 191.90/28.23 % (3361428)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=563308303:i=1758:kws=inv_precedence:fsr=off:rtra=on_2825 on theBenchmark for (2825ds/1758Mi) % 191.90/28.23 % (3361428)Instruction limit reached! % 191.90/28.23 % (3361428)------------------------------ % 191.90/28.23 % (3361428)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 191.90/28.23 % (3361428)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 191.90/28.23 % (3361428)CaDiCaL version: 2.1.3 % 191.90/28.23 % (3361428)Termination reason: Instruction limit % 191.90/28.23 % (3361428)Termination phase: Saturation % 191.90/28.23 % (3361428)Time elapsed: 0.400 s % 191.90/28.23 % (3361428)Peak memory usage: 16 MB % 191.90/28.23 % (3361428)Instructions burned: 1759 (million) % 191.90/28.23 % (3361430)fmb+10_1_sil=64000:si=on:random_seed=3954970809:i=44122:nm=2:rtra=on:gsp=on_2821 on theBenchmark for (2821ds/44122Mi) % 191.90/28.23 % TRYING [1] % 191.90/28.23 % (3361396)Refutation not found, incomplete strategy % 191.90/28.23 % (3361396)------------------------------ % 191.90/28.23 % (3361396)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 191.90/28.23 % (3361396)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 191.90/28.23 % (3361396)CaDiCaL version: 2.1.3 % 191.90/28.23 % (3361396)Termination reason: Refutation not found, incomplete strategy % 191.90/28.23 % (3361396)Time elapsed: 5.789 s % 191.90/28.23 % (3361396)Peak memory usage: 695 MB % 191.90/28.23 % (3361396)Instructions burned: 12509 (million) % 191.90/28.23 % (3361396)------------------------------ % 191.90/28.23 % (3361396)------------------------------ % 191.90/28.23 % (3361432)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=30826532:i=19030:nm=5:rtra=on_2819 on theBenchmark for (2819ds/19030Mi) % 191.90/28.23 % TRYING [2] % 191.90/28.23 % (3361432)Cannot represent all propositional literals internally % 191.90/28.23 % (3361432)Refutation not found, incomplete strategy % 191.90/28.23 % (3361432)------------------------------ % 191.90/28.23 % (3361432)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 191.90/28.23 % (3361432)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 191.90/28.23 % (3361432)CaDiCaL version: 2.1.3 % 191.90/28.23 % (3361432)Termination reason: Refutation not found, incomplete strategy % 191.90/28.23 % (3361432)Time elapsed: 0.029 s % 191.90/28.23 % (3361432)Peak memory usage: 12 MB % 191.90/28.23 % (3361432)Instructions burned: 102 (million) % 211.33/30.18 % (3361432)------------------------------ % 211.33/30.18 % (3361432)------------------------------ % 211.33/30.18 % (3361434)fmb+10_1_sil=64000:sas=cadical:si=on:fmbss=8:random_seed=3672220419:fmbsr=1.7:i=1840:rtra=on_2819 on theBenchmark for (2819ds/1840Mi) % 211.33/30.18 % (3361434)Cannot represent all propositional literals internally % 211.33/30.18 % (3361434)Refutation not found, incomplete strategy % 211.33/30.18 % (3361434)------------------------------ % 211.33/30.18 % (3361434)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 211.33/30.18 % (3361434)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 211.33/30.18 % (3361434)CaDiCaL version: 2.1.3 % 211.33/30.18 % (3361434)Termination reason: Refutation not found, incomplete strategy % 211.33/30.18 % (3361434)Time elapsed: 0.029 s % 211.33/30.18 % (3361434)Peak memory usage: 12 MB % 211.33/30.18 % (3361434)Instructions burned: 102 (million) % 211.33/30.18 % (3361434)------------------------------ % 211.33/30.18 % (3361434)------------------------------ % 211.33/30.18 % (3361436)dis-4_1_sil=16000:drc=ordering:si=on:sp=const_frequency:sac=on:newcnf=on:random_seed=1717209162:i=10262:rtra=on_2818 on theBenchmark for (2818ds/10262Mi) % 211.33/30.18 % (3361436)Instruction limit reached! % 211.33/30.18 % (3361436)------------------------------ % 211.33/30.18 % (3361436)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 211.33/30.18 % (3361436)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 211.33/30.18 % (3361436)CaDiCaL version: 2.1.3 % 211.33/30.18 % (3361436)Termination reason: Instruction limit % 211.33/30.18 % (3361436)Termination phase: Saturation % 211.33/30.18 % (3361436)Time elapsed: 2.833 s % 211.33/30.18 % (3361436)Peak memory usage: 36 MB % 211.33/30.18 % (3361436)Instructions burned: 10265 (million) % 211.33/30.18 % (3361438)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:si=on:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2775679792:i=2944:ins=7:rtra=on:fdi=8:gsp=on_2790 on theBenchmark for (2790ds/2944Mi) % 211.33/30.18 % (3361384)Instruction limit reached! % 211.33/30.18 % (3361384)------------------------------ % 211.33/30.18 % (3361384)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 211.33/30.18 % (3361384)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 211.33/30.18 % (3361384)CaDiCaL version: 2.1.3 % 211.33/30.18 % (3361384)Termination reason: Instruction limit % 211.33/30.18 % (3361384)Termination phase: Saturation % 211.33/30.18 % (3361384)Time elapsed: 9.932 s % 211.33/30.18 % (3361384)Peak memory usage: 167 MB % 211.33/30.18 % (3361384)Instructions burned: 28122 (million) % 211.33/30.18 % (3361440)fmb+10_1_sil=16000:sas=cadical:si=on:bce=on:fmbss=77:random_seed=3107785317:i=12648:rtra=on_2782 on theBenchmark for (2782ds/12648Mi) % 211.33/30.18 % (3361438)Instruction limit reached! % 211.33/30.18 % (3361438)------------------------------ % 211.33/30.18 % (3361438)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 211.33/30.18 % (3361438)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 211.33/30.18 % (3361438)CaDiCaL version: 2.1.3 % 211.33/30.18 % (3361438)Termination reason: Instruction limit % 211.33/30.18 % (3361438)Termination phase: Saturation % 211.33/30.18 % (3361438)Time elapsed: 0.838 s % 211.33/30.18 % (3361438)Peak memory usage: 39 MB % 211.33/30.18 % (3361438)Instructions burned: 2947 (million) % 211.33/30.18 % (3361440)Cannot represent all propositional literals internally % 211.33/30.18 % (3361440)Refutation not found, incomplete strategy % 211.33/30.18 % (3361440)------------------------------ % 211.33/30.18 % (3361440)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 211.33/30.18 % (3361440)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 211.33/30.18 % (3361440)CaDiCaL version: 2.1.3 % 211.33/30.18 % (3361440)Termination reason: Refutation not found, incomplete strategy % 211.33/30.18 % (3361440)Time elapsed: 0.030 s % 211.33/30.18 % (3361440)Peak memory usage: 12 MB % 211.33/30.18 % (3361440)Instructions burned: 109 (million) % 211.33/30.18 % (3361442)fmb+10_1_fmbas=function:sil=32000:sas=cadical:si=on:fmbss=16:random_seed=369909010:fmbsr=2.30978:i=4348:rtra=on_2781 on theBenchmark for (2781ds/4348Mi) % 211.33/30.18 % (3361440)------------------------------ % 211.33/30.18 % (3361440)------------------------------ % 211.33/30.18 % (3361444)ott-2_1_sil=16000:si=on:newcnf=on:random_seed=2355182282:avsq=on:i=1738:avsqr=1,16:kws=inv_arity_squared:rtra=on_2781 on theBenchmark for (2781ds/1738Mi) % 211.33/30.18 % (3361442)Cannot represent all propositional literals internally % 211.33/30.18 % (3361442)Refutation not found, incomplete strategy % 211.33/30.18 % (3361442)------------------------------ % 249.95/35.66 % (3361442)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 249.95/35.66 % (3361442)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 249.95/35.66 % (3361442)CaDiCaL version: 2.1.3 % 249.95/35.66 % (3361442)Termination reason: Refutation not found, incomplete strategy % 249.95/35.66 % (3361442)Time elapsed: 0.146 s % 249.95/35.66 % (3361442)Peak memory usage: 16 MB % 249.95/35.66 % (3361442)Instructions burned: 558 (million) % 249.95/35.66 % (3361442)------------------------------ % 249.95/35.66 % (3361442)------------------------------ % 249.95/35.66 % (3361446)ott+10_1_sil=32000:tgt=ground:si=on:random_seed=3154607772:i=10228:av=off:rtra=on_2780 on theBenchmark for (2780ds/10228Mi) % 249.95/35.66 % (3361444)Instruction limit reached! % 249.95/35.66 % (3361444)------------------------------ % 249.95/35.66 % (3361444)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 249.95/35.66 % (3361444)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 249.95/35.66 % (3361444)CaDiCaL version: 2.1.3 % 249.95/35.66 % (3361444)Termination reason: Instruction limit % 249.95/35.66 % (3361444)Termination phase: Saturation % 249.95/35.66 % (3361444)Time elapsed: 0.366 s % 249.95/35.66 % (3361444)Peak memory usage: 14 MB % 249.95/35.66 % (3361444)Instructions burned: 1738 (million) % 249.95/35.66 % (3361448)fmb+10_1_sil=64000:sas=cadical:si=on:bce=on:rp=on:random_seed=1614262101:i=108564:rtra=on_2777 on theBenchmark for (2777ds/108564Mi) % 249.95/35.66 % TRYING [1] % 249.95/35.66 % TRYING [2] % 249.95/35.66 % (3361446)Instruction limit reached! % 249.95/35.66 % (3361446)------------------------------ % 249.95/35.66 % (3361446)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 249.95/35.66 % (3361446)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 249.95/35.66 % (3361446)CaDiCaL version: 2.1.3 % 249.95/35.66 % (3361446)Termination reason: Instruction limit % 249.95/35.66 % (3361446)Termination phase: Saturation % 249.95/35.66 % (3361446)Time elapsed: 3.490 s % 249.95/35.66 % (3361446)Peak memory usage: 76 MB % 249.95/35.66 % (3361446)Instructions burned: 10230 (million) % 249.95/35.66 % (3361450)dis-11_1_sil=16000:si=on:sp=reverse_frequency:alpa=true:random_seed=4273021236:i=7024:aac=none:rtra=on_2745 on theBenchmark for (2745ds/7024Mi) % 249.95/35.66 % (3361380)Instruction limit reached! % 249.95/35.66 % (3361380)------------------------------ % 249.95/35.66 % (3361380)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 249.95/35.66 % (3361380)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 249.95/35.66 % (3361380)CaDiCaL version: 2.1.3 % 249.95/35.66 % (3361380)Termination reason: Instruction limit % 249.95/35.66 % (3361380)Termination phase: Saturation % 249.95/35.66 % (3361380)Time elapsed: 14.738 s % 249.95/35.66 % (3361380)Peak memory usage: 162 MB % 249.95/35.66 % (3361380)Instructions burned: 53297 (million) % 249.95/35.66 % (3361452)dis+21_1_sil=32000:sas=cadical:si=on:random_seed=1739438420:i=7546:rtra=on:amm=off_2736 on theBenchmark for (2736ds/7546Mi) % 249.95/35.66 % (3361450)Instruction limit reached! % 249.95/35.66 % (3361450)------------------------------ % 249.95/35.66 % (3361450)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 249.95/35.66 % (3361450)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 249.95/35.66 % (3361450)CaDiCaL version: 2.1.3 % 249.95/35.66 % (3361450)Termination reason: Instruction limit % 249.95/35.66 % (3361450)Termination phase: Saturation % 249.95/35.66 % (3361450)Time elapsed: 1.972 s % 249.95/35.66 % (3361450)Peak memory usage: 31 MB % 249.95/35.66 % (3361450)Instructions burned: 7025 (million) % 249.95/35.66 % (3361448)Cannot represent all propositional literals internally % 249.95/35.66 % (3361454)ott+11_1_sil=16000:si=on:gs=on:random_seed=3285981504:s2a=on:i=4502:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:rtra=on:fsd=on_2725 on theBenchmark for (2725ds/4502Mi) % 249.95/35.66 % (3361448)Refutation not found, incomplete strategy % 249.95/35.66 % (3361448)------------------------------ % 249.95/35.66 % (3361448)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 249.95/35.66 % (3361448)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 249.95/35.66 % (3361448)CaDiCaL version: 2.1.3 % 249.95/35.66 % (3361448)Termination reason: Refutation not found, incomplete strategy % 249.95/35.66 % (3361448)Time elapsed: 5.831 s % 249.95/35.66 % (3361448)Peak memory usage: 661 MB % 249.95/35.66 % (3361448)Instructions burned: 12477 (million) % 249.95/35.66 % (3361448)------------------------------ % 249.95/35.66 % (3361448)------------------------------ % 249.95/35.66 % (3361456)fmb+10_1_fmbas=predicate:silTerminated % 300.33/42.83 % Vampire exiting %------------------------------------------------------------------------------