%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWV581-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 : n008.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:04 PM UTC 2026 % Result : Timeout 300.62s 42.84s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.04 % Problem : SWV581-1 : TPTP v9.3.1. Released v4.1.0. % 0.00/0.07 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.10/0.26 % Computer : n008.cluster.edu % 0.10/0.26 % Model : x86_64 x86_64 % 0.10/0.26 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.26 % Memory : 8046.5625MB % 0.10/0.26 % OS : Linux 6.8.0-71-generic % 0.10/0.26 % CPULimit : 300 % 0.10/0.26 % WCLimit : 300 % 0.10/0.26 % DateTime : Mon Sep 28 11:56:25 UTC 2026 % 0.10/0.27 % CPUTime : % 0.10/0.27 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.26/0.32 Running first-order model finding % 0.26/0.32 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 % 18.95/3.07 % (2199133)Will run a generic schedule for satisfiability detection. % 18.95/3.07 % (2199140)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2659663776:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 18.95/3.07 % (2199138)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1720212637_2999 on theBenchmark for (2999ds/0Mi) % 18.95/3.07 % (2199139)% WARNING: option uhcvi not known. % 18.95/3.07 % (2199141)dis+10_1_sil=32000:sp=arity:random_seed=1886523145:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 18.95/3.07 % (2199142)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=372710984:i=116_2999 on theBenchmark for (2999ds/116Mi) % 18.95/3.07 % (2199143)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1470785842:i=131_2999 on theBenchmark for (2999ds/131Mi) % 18.95/3.07 % (2199144)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=230728752:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 18.95/3.07 % (2199139)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3651937598:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 18.95/3.07 % (2199141)Instruction limit reached! % 18.95/3.07 % (2199141)------------------------------ % 18.95/3.07 % (2199141)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 18.95/3.07 % (2199141)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.95/3.07 % (2199141)CaDiCaL version: 2.1.3 % 18.95/3.07 % (2199141)Termination reason: Instruction limit % 18.95/3.07 % (2199141)Termination phase: Saturation % 18.95/3.07 % (2199141)Time elapsed: 0.104 s % 18.95/3.07 % (2199141)Peak memory usage: 13 MB % 18.95/3.07 % (2199141)Instructions burned: 103 (million) % 18.95/3.07 % (2199142)Instruction limit reached! % 18.95/3.07 % (2199142)------------------------------ % 18.95/3.07 % (2199142)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 18.95/3.07 % (2199142)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.95/3.07 % (2199142)CaDiCaL version: 2.1.3 % 18.95/3.07 % (2199142)Termination reason: Instruction limit % 18.95/3.07 % (2199142)Termination phase: Saturation % 18.95/3.07 % (2199142)Time elapsed: 0.112 s % 18.95/3.07 % (2199142)Peak memory usage: 14 MB % 18.95/3.07 % (2199142)Instructions burned: 117 (million) % 18.95/3.07 % (2199143)Instruction limit reached! % 18.95/3.07 % (2199143)------------------------------ % 18.95/3.07 % (2199143)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 18.95/3.07 % (2199143)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.95/3.07 % (2199143)CaDiCaL version: 2.1.3 % 18.95/3.07 % (2199143)Termination reason: Instruction limit % 18.95/3.07 % (2199143)Termination phase: Saturation % 18.95/3.07 % (2199143)Time elapsed: 0.120 s % 18.95/3.07 % (2199143)Peak memory usage: 14 MB % 18.95/3.07 % (2199143)Instructions burned: 131 (million) % 18.95/3.07 % (2199154)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1262523391:i=714:nm=2_2997 on theBenchmark for (2997ds/714Mi) % 18.95/3.07 % (2199155)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3692457727:i=131:bd=preordered:fsd=on_2997 on theBenchmark for (2997ds/131Mi) % 18.95/3.07 % (2199156)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=4281395928:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2997 on theBenchmark for (2997ds/684Mi) % 18.95/3.07 % (2199144)Instruction limit reached! % 18.95/3.07 % (2199144)------------------------------ % 18.95/3.07 % (2199144)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 18.95/3.07 % (2199144)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.95/3.07 % (2199144)CaDiCaL version: 2.1.3 % 18.95/3.07 % (2199144)Termination reason: Instruction limit % 18.95/3.07 % (2199144)Termination phase: Saturation % 18.95/3.07 % (2199144)Time elapsed: 0.170 s % 18.95/3.07 % (2199144)Peak memory usage: 15 MB % 18.95/3.07 % (2199144)Instructions burned: 159 (million) % 18.95/3.07 % (2199160)ott-21_1_sil=16000:fs=off:random_seed=409831017:i=180:av=off:fsr=off_2997 on theBenchmark for (2997ds/180Mi) % 18.95/3.07 % (2199155)Instruction limit reached! % 18.95/3.07 % (2199155)------------------------------ % 18.95/3.07 % (2199155)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 18.95/3.07 % (2199155)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.95/3.07 % (2199155)CaDiCaL version: 2.1.3 % 64.07/9.44 % (2199155)Termination reason: Instruction limit % 64.07/9.44 % (2199155)Termination phase: Saturation % 64.07/9.44 % (2199155)Time elapsed: 0.126 s % 64.07/9.44 % (2199155)Peak memory usage: 14 MB % 64.07/9.44 % (2199155)Instructions burned: 132 (million) % 64.07/9.44 % (2199162)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3841377061:i=477:bd=all_2996 on theBenchmark for (2996ds/477Mi) % 64.07/9.44 % (2199160)Instruction limit reached! % 64.07/9.44 % (2199160)------------------------------ % 64.07/9.44 % (2199160)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 64.07/9.44 % (2199160)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 64.07/9.44 % (2199160)CaDiCaL version: 2.1.3 % 64.07/9.44 % (2199160)Termination reason: Instruction limit % 64.07/9.44 % (2199160)Termination phase: Saturation % 64.07/9.44 % (2199160)Time elapsed: 0.142 s % 64.07/9.44 % (2199160)Peak memory usage: 13 MB % 64.07/9.44 % (2199160)Instructions burned: 180 (million) % 64.07/9.44 % (2199164)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=97195228:fmbsr=1.3:i=865:ins=25_2995 on theBenchmark for (2995ds/865Mi) % 64.07/9.44 % TRYING [1] % 64.07/9.44 % TRYING [2] % 64.07/9.44 % TRYING [1] % 64.07/9.44 % TRYING [2] % 64.07/9.44 % TRYING [3] % 64.07/9.44 % (2199154)Instruction limit reached! % 64.07/9.44 % (2199154)------------------------------ % 64.07/9.44 % (2199154)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 64.07/9.44 % (2199154)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 64.07/9.44 % (2199154)CaDiCaL version: 2.1.3 % 64.07/9.44 % (2199154)Termination reason: Instruction limit % 64.07/9.44 % (2199154)Termination phase: Finite model building constraint generation % 64.07/9.44 % (2199154)Time elapsed: 0.610 s % 64.07/9.44 % (2199154)Peak memory usage: 36 MB % 64.07/9.44 % (2199154)Instructions burned: 715 (million) % 64.07/9.44 % (2199166)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2122851266:i=1179_2991 on theBenchmark for (2991ds/1179Mi) % 64.07/9.44 % (2199162)Instruction limit reached! % 64.07/9.44 % (2199162)------------------------------ % 64.07/9.44 % (2199162)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 64.07/9.44 % (2199162)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 64.07/9.44 % (2199162)CaDiCaL version: 2.1.3 % 64.07/9.44 % (2199162)Termination reason: Instruction limit % 64.07/9.44 % (2199162)Termination phase: Saturation % 64.07/9.44 % (2199162)Time elapsed: 0.487 s % 64.07/9.44 % (2199162)Peak memory usage: 15 MB % 64.07/9.44 % (2199162)Instructions burned: 478 (million) % 64.07/9.44 % (2199156)Instruction limit reached! % 64.07/9.44 % (2199156)------------------------------ % 64.07/9.44 % (2199156)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 64.07/9.44 % (2199156)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 64.07/9.44 % (2199156)CaDiCaL version: 2.1.3 % 64.07/9.44 % (2199156)Termination reason: Instruction limit % 64.07/9.44 % (2199156)Termination phase: Saturation % 64.07/9.44 % (2199156)Time elapsed: 0.659 s % 64.07/9.44 % (2199156)Peak memory usage: 18 MB % 64.07/9.44 % (2199156)Instructions burned: 684 (million) % 64.07/9.44 % (2199168)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3350936606:i=889:ins=1_2990 on theBenchmark for (2990ds/889Mi) % 64.07/9.44 % (2199169)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=1376154556:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2990 on theBenchmark for (2990ds/692Mi) % 64.07/9.44 % TRYING [1] % 64.07/9.44 % (2199164)Instruction limit reached! % 64.07/9.44 % (2199164)------------------------------ % 64.07/9.44 % (2199164)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 64.07/9.44 % (2199164)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 64.07/9.44 % (2199164)CaDiCaL version: 2.1.3 % 64.07/9.44 % (2199164)Termination reason: Instruction limit % 64.07/9.44 % (2199164)Termination phase: Finite model building constraint generation % 64.07/9.44 % (2199164)Time elapsed: 0.736 s % 64.07/9.44 % (2199164)Peak memory usage: 29 MB % 64.07/9.44 % (2199164)Instructions burned: 866 (million) % 64.07/9.44 % (2199172)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1396298893:i=879:kws=inv_precedence:fsr=off_2987 on theBenchmark for (2987ds/879Mi) % 64.07/9.44 % (2199168)Cannot represent all propositional literals internally % 64.07/9.44 % (2199168)Refutation not found, incomplete strategy % 64.07/9.44 % (2199168)------------------------------ % 130.78/18.83 % (2199168)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 130.78/18.83 % (2199168)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 130.78/18.83 % (2199168)CaDiCaL version: 2.1.3 % 130.78/18.83 % (2199168)Termination reason: Refutation not found, incomplete strategy % 130.78/18.83 % (2199168)Time elapsed: 0.419 s % 130.78/18.83 % (2199168)Peak memory usage: 19 MB % 130.78/18.83 % (2199168)Instructions burned: 475 (million) % 130.78/18.83 % (2199168)------------------------------ % 130.78/18.83 % (2199168)------------------------------ % 130.78/18.83 % (2199174)fmb+10_1_sil=64000:random_seed=2363674326:i=22061:nm=2:gsp=on_2986 on theBenchmark for (2986ds/22061Mi) % 130.78/18.83 % (2199169)Instruction limit reached! % 130.78/18.83 % (2199169)------------------------------ % 130.78/18.83 % (2199169)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 130.78/18.83 % (2199169)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 130.78/18.83 % (2199169)CaDiCaL version: 2.1.3 % 130.78/18.83 % (2199169)Termination reason: Instruction limit % 130.78/18.83 % (2199169)Termination phase: Saturation % 130.78/18.83 % (2199169)Time elapsed: 0.573 s % 130.78/18.83 % (2199169)Peak memory usage: 16 MB % 130.78/18.83 % (2199169)Instructions burned: 692 (million) % 130.78/18.83 % (2199176)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=633748524:i=9515:nm=5_2984 on theBenchmark for (2984ds/9515Mi) % 130.78/18.83 % TRYING [1] % 130.78/18.83 % TRYING [2] % 130.78/18.83 % (2199176)Cannot represent all propositional literals internally % 130.78/18.83 % (2199176)Refutation not found, incomplete strategy % 130.78/18.83 % (2199176)------------------------------ % 130.78/18.83 % (2199176)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 130.78/18.83 % (2199176)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 130.78/18.83 % (2199176)CaDiCaL version: 2.1.3 % 130.78/18.83 % (2199176)Termination reason: Refutation not found, incomplete strategy % 130.78/18.83 % (2199176)Time elapsed: 0.410 s % 130.78/18.83 % (2199176)Peak memory usage: 19 MB % 130.78/18.83 % (2199176)Instructions burned: 463 (million) % 130.78/18.83 % (2199176)------------------------------ % 130.78/18.83 % (2199176)------------------------------ % 130.78/18.83 % (2199166)Instruction limit reached! % 130.78/18.83 % (2199166)------------------------------ % 130.78/18.83 % (2199166)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 130.78/18.83 % (2199166)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 130.78/18.83 % (2199166)CaDiCaL version: 2.1.3 % 130.78/18.83 % (2199166)Termination reason: Instruction limit % 130.78/18.83 % (2199166)Termination phase: Saturation % 130.78/18.83 % (2199166)Time elapsed: 1.108 s % 130.78/18.83 % (2199166)Peak memory usage: 22 MB % 130.78/18.83 % (2199166)Instructions burned: 1179 (million) % 130.78/18.83 % (2199178)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2848589889:fmbsr=1.7:i=920_2980 on theBenchmark for (2980ds/920Mi) % 130.78/18.83 % (2199179)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=3898549393:i=5131_2979 on theBenchmark for (2979ds/5131Mi) % 130.78/18.83 % (2199172)Instruction limit reached! % 130.78/18.83 % (2199172)------------------------------ % 130.78/18.83 % (2199172)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 130.78/18.83 % (2199172)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 130.78/18.83 % (2199172)CaDiCaL version: 2.1.3 % 130.78/18.83 % (2199172)Termination reason: Instruction limit % 130.78/18.83 % (2199172)Termination phase: Saturation % 130.78/18.83 % (2199172)Time elapsed: 0.847 s % 130.78/18.83 % (2199172)Peak memory usage: 20 MB % 130.78/18.83 % (2199172)Instructions burned: 879 (million) % 130.78/18.83 % (2199182)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2226373413:i=1472:ins=7:fdi=8:gsp=on_2978 on theBenchmark for (2978ds/1472Mi) % 130.78/18.83 % TRYING [8] % 130.78/18.83 % (2199178)Instruction limit reached! % 130.78/18.83 % (2199178)------------------------------ % 130.78/18.83 % (2199178)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 130.78/18.83 % (2199178)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 130.78/18.83 % (2199178)CaDiCaL version: 2.1.3 % 130.78/18.83 % (2199178)Termination reason: Instruction limit % 130.78/18.83 % (2199178)Termination phase: Finite model building constraint generation % 130.78/18.83 % (2199178)Time elapsed: 0.676 s % 130.78/18.83 % (2199178)Peak memory usage: 47 MB % 130.78/18.83 % (2199178)Instructions burned: 920 (million) % 130.78/18.83 % (2199184)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=920657460:i=6324_2973 on theBenchmark for (2973ds/6324Mi) % 261.41/37.22 % (2199184)Cannot represent all propositional literals internally % 261.41/37.22 % (2199184)Refutation not found, incomplete strategy % 261.41/37.22 % (2199184)------------------------------ % 261.41/37.22 % (2199184)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 261.41/37.22 % (2199184)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 261.41/37.22 % (2199184)CaDiCaL version: 2.1.3 % 261.41/37.22 % (2199184)Termination reason: Refutation not found, incomplete strategy % 261.41/37.22 % (2199184)Time elapsed: 0.435 s % 261.41/37.22 % (2199184)Peak memory usage: 19 MB % 261.41/37.22 % (2199184)Instructions burned: 490 (million) % 261.41/37.22 % (2199184)------------------------------ % 261.41/37.22 % (2199184)------------------------------ % 261.41/37.22 % (2199188)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=12825259:fmbsr=2.30978:i=2174_2968 on theBenchmark for (2968ds/2174Mi) % 261.41/37.22 % (2199182)Instruction limit reached! % 261.41/37.22 % (2199182)------------------------------ % 261.41/37.22 % (2199182)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 261.41/37.22 % (2199182)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 261.41/37.22 % (2199182)CaDiCaL version: 2.1.3 % 261.41/37.22 % (2199182)Termination reason: Instruction limit % 261.41/37.22 % (2199182)Termination phase: Saturation % 261.41/37.22 % (2199182)Time elapsed: 1.201 s % 261.41/37.22 % (2199182)Peak memory usage: 26 MB % 261.41/37.22 % (2199182)Instructions burned: 1472 (million) % 261.41/37.22 % (2199190)ott-2_1_sil=16000:newcnf=on:random_seed=3560876312:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2966 on theBenchmark for (2966ds/869Mi) % 261.41/37.22 % TRYING [4] % 261.41/37.22 % TRYING [3] % 261.41/37.22 % (2199190)Instruction limit reached! % 261.41/37.22 % (2199190)------------------------------ % 261.41/37.22 % (2199190)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 261.41/37.22 % (2199190)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 261.41/37.22 % (2199190)CaDiCaL version: 2.1.3 % 261.41/37.22 % (2199190)Termination reason: Instruction limit % 261.41/37.22 % (2199190)Termination phase: Saturation % 261.41/37.22 % (2199190)Time elapsed: 0.792 s % 261.41/37.22 % (2199190)Peak memory usage: 19 MB % 261.41/37.22 % (2199190)Instructions burned: 869 (million) % 261.41/37.22 % (2199192)ott+10_1_sil=32000:tgt=ground:random_seed=2927079049:i=5114:av=off_2958 on theBenchmark for (2958ds/5114Mi) % 261.41/37.22 % (2199188)Instruction limit reached! % 261.41/37.22 % (2199188)------------------------------ % 261.41/37.22 % (2199188)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 261.41/37.22 % (2199188)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 261.41/37.22 % (2199188)CaDiCaL version: 2.1.3 % 261.41/37.22 % (2199188)Termination reason: Instruction limit % 261.41/37.22 % (2199188)Termination phase: Finite model building preprocessing % 261.41/37.22 % (2199188)Time elapsed: 1.860 s % 261.41/37.22 % (2199188)Peak memory usage: 34 MB % 261.41/37.22 % (2199188)Instructions burned: 2174 (million) % 261.41/37.22 % (2199194)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=1326791584:i=54282_2949 on theBenchmark for (2949ds/54282Mi) % 261.41/37.22 % TRYING [1] % 261.41/37.22 % TRYING [2] % 261.41/37.22 % TRYING [3] % 261.41/37.22 % (2199179)Instruction limit reached! % 261.41/37.22 % (2199179)------------------------------ % 261.41/37.22 % (2199179)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 261.41/37.22 % (2199179)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 261.41/37.22 % (2199179)CaDiCaL version: 2.1.3 % 261.41/37.22 % (2199179)Termination reason: Instruction limit % 261.41/37.22 % (2199179)Termination phase: Saturation % 261.41/37.22 % (2199179)Time elapsed: 4.951 s % 261.41/37.22 % (2199179)Peak memory usage: 37 MB % 261.41/37.22 % (2199179)Instructions burned: 5132 (million) % 261.41/37.22 % (2199199)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=627230127:i=3512:aac=none_2929 on theBenchmark for (2929ds/3512Mi) % 261.41/37.22 % TRYING [4] % 261.41/37.22 % (2199192)Instruction limit reached! % 261.41/37.22 % (2199192)------------------------------ % 261.41/37.22 % (2199192)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 261.41/37.22 % (2199192)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 261.41/37.22 % (2199192)CaDiCaL version: 2.1.3 % 261.41/37.22 % (2199192)Termination reason: Instruction limit % 261.41/37.22 % (2199192)Termination phase: Saturation % 261.41/37.22 % (2199192)Time elapsed: 4.865 s % 261.41/37.22 % (2199192)Peak memory usage: 44 MB % 261.41/37.22 % (2199192)Instructions burned: 5114 (million) % 261.41/37.22 % (2199202)dis+21_1_sil=32000:sas=cadical:random_seed=3373737685:i=3773:amm=off_2909 on theBenchmark for (2909ds/3773Mi) % 300.62/42.84 % (2199199)Instruction limit reached! % 300.62/42.84 % (2199199)------------------------------ % 300.62/42.84 % (2199199)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.62/42.84 % (2199199)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.62/42.84 % (2199199)CaDiCaL version: 2.1.3 % 300.62/42.84 % (2199199)Termination reason: Instruction limit % 300.62/42.84 % (2199199)Termination phase: Saturation % 300.62/42.84 % (2199199)Time elapsed: 3.314 s % 300.62/42.84 % (2199199)Peak memory usage: 33 MB % 300.62/42.84 % (2199199)Instructions burned: 3512 (million) % 300.62/42.84 % (2199204)ott+11_1_sil=16000:gs=on:random_seed=3961183365:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2896 on theBenchmark for (2896ds/2251Mi) % 300.62/42.84 % (2199204)Instruction limit reached! % 300.62/42.84 % (2199204)------------------------------ % 300.62/42.84 % (2199204)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.62/42.84 % (2199204)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.62/42.84 % (2199204)CaDiCaL version: 2.1.3 % 300.62/42.84 % (2199204)Termination reason: Instruction limit % 300.62/42.84 % (2199204)Termination phase: Saturation % 300.62/42.84 % (2199204)Time elapsed: 2.072 s % 300.62/42.84 % (2199204)Peak memory usage: 26 MB % 300.62/42.84 % (2199204)Instructions burned: 2251 (million) % 300.62/42.84 % (2199206)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=2091807162:fmbsr=1.6:i=67534_2875 on theBenchmark for (2875ds/67534Mi) % 300.62/42.84 % (2199202)Instruction limit reached! % 300.62/42.84 % (2199202)------------------------------ % 300.62/42.84 % (2199202)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.62/42.84 % (2199202)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.62/42.84 % (2199202)CaDiCaL version: 2.1.3 % 300.62/42.84 % (2199202)Termination reason: Instruction limit % 300.62/42.84 % (2199202)Termination phase: Saturation % 300.62/42.84 % (2199202)Time elapsed: 3.422 s % 300.62/42.84 % (2199202)Peak memory usage: 37 MB % 300.62/42.84 % (2199202)Instructions burned: 3773 (million) % 300.62/42.84 % TRYING [4] % 300.62/42.84 % (2199208)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=480969264:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2874 on theBenchmark for (2874ds/4591Mi) % 300.62/42.84 % (2199208)Instruction limit reached! % 300.62/42.84 % (2199208)------------------------------ % 300.62/42.84 % (2199208)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.62/42.84 % (2199208)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.62/42.84 % (2199208)CaDiCaL version: 2.1.3 % 300.62/42.84 % (2199208)Termination reason: Instruction limit % 300.62/42.84 % (2199208)Termination phase: Saturation % 300.62/42.84 % (2199208)Time elapsed: 2.405 s % 300.62/42.84 % (2199208)Peak memory usage: 50 MB % 300.62/42.84 % (2199208)Instructions burned: 4591 (million) % 300.62/42.84 % (2199250)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=3463638723:i=29340_2850 on theBenchmark for (2850ds/29340Mi) % 300.62/42.84 % (2199174)Instruction limit reached! % 300.62/42.84 % (2199174)------------------------------ % 300.62/42.84 % (2199174)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.62/42.84 % (2199174)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.62/42.84 % (2199174)CaDiCaL version: 2.1.3 % 300.62/42.84 % (2199174)Termination reason: Instruction limit % 300.62/42.84 % (2199174)Termination phase: Finite model building constraint generation % 300.62/42.84 % (2199174)Time elapsed: 14.159 s % 300.62/42.84 % (2199174)Peak memory usage: 537 MB % 300.62/42.84 % (2199174)Instructions burned: 22061 (million) % 300.62/42.84 % (2199252)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=4268384098:i=5211_2843 on theBenchmark for (2843ds/5211Mi) % 300.62/42.84 % (2199252)Instruction limit reached! % 300.62/42.84 % (2199252)------------------------------ % 300.62/42.84 % (2199252)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.62/42.84 % (2199252)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.62/42.84 % (2199252)CaDiCaL version: 2.1.3 % 300.62/42.84 % (2199252)Termination reason: Instruction limit % 300.62/42.84 % (2199252)Termination phase: Saturation % 300.62/42.84 % (2199252)Time elapsed: 2.822 s % 300.62/42.84 % (2199252)Peak memory usage: 48 MB % 300.62/42.84 % (2199252)Instructions burned: 5213 (million) % 300.62/42.84 % (2199254)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=3643377936:i=5497:nm=2_2815 on theBenchmark for (2815ds/5497Mi) % 300.62/42.84 % (2199254)Cannot represent all propositional literals internally % 300.62/42.84 % (2199254)Refutation not found, incomplete strategy % 300.62/42.84 % (2199254)------------------------------ % 300.62/42.84 % (2199254)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.62/42.84 % (2199254)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.62/42.84 % (2199254)CaDiCaL version: 2.1.3 % 300.62/42.84 % (2199254)Termination reason: Refutation not found, incomplete strategy % 300.62/42.84 % (2199254)Time elapsed: 0.245 s % 300.62/42.84 % (2199254)Peak memory usage: 19 MB % 300.62/42.84 % (2199254)Instructions burned: 490 (million) % 300.62/42.84 % (2199254)------------------------------ % 300.62/42.84 % (2199254)------------------------------ % 300.62/42.84 % (2199256)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=2708835647:fmbsr=2:i=46332_2812 on theBenchmark for (2812ds/46332Mi) % 300.62/42.84 % (2199256)Cannot represent all propositional literals internally % 300.62/42.84 % (2199256)Refutation not found, incomplete strategy % 300.62/42.84 % (2199256)------------------------------ % 300.62/42.84 % (2199256)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.62/42.84 % (2199256)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.62/42.84 % (2199256)CaDiCaL version: 2.1.3 % 300.62/42.84 % (2199256)Termination reason: Refutation not found, incomplete strategy % 300.62/42.84 % (2199256)Time elapsed: 0.241 s % 300.62/42.84 % (2199256)Peak memory usage: 18 MB % 300.62/42.84 % (2199256)Instructions burned: 496 (million) % 300.62/42.84 % (2199256)------------------------------ % 300.62/42.84 % (2199256)------------------------------ % 300.62/42.84 % (2199258)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=2707028836:i=14071_2809 on theBenchmark for (2809ds/14071Mi) % 300.62/42.84 % (2199258)Cannot represent all propositional literals internally % 300.62/42.84 % (2199258)Refutation not found, incomplete strategy % 300.62/42.84 % (2199258)------------------------------ % 300.62/42.84 % (2199258)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.62/42.84 % (2199258)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.62/42.84 % (2199258)CaDiCaL version: 2.1.3 % 300.62/42.84 % (2199258)Termination reason: Refutation not found, incomplete strategy % 300.62/42.84 % (2199258)Time elapsed: 0.242 s % 300.62/42.84 % (2199258)Peak memory usage: 19 MB % 300.62/42.84 % (2199258)Instructions burned: 487 (million) % 300.62/42.84 % (2199258)------------------------------ % 300.62/42.84 % (2199258)------------------------------ % 300.62/42.84 % (2199260)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=4278431719:i=22565:add=on:rawr=on_2807 on theBenchmark for (2807ds/22565Mi) % 300.62/42.84 % TRYING [7] % 300.62/42.84 % TRYING [5] % 300.62/42.84 % TRYING [5] % 300.62/42.84 % (2199250)Instruction limit reached! % 300.62/42.84 % (2199250)------------------------------ % 300.62/42.84 % (2199250)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.62/42.84 % (2199250)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.62/42.84 % (2199250)CaDiCaL version: 2.1.3 % 300.62/42.84 % (2199250)Termination reason: Instruction limit % 300.62/42.84 % (2199250)Termination phase: Saturation % 300.62/42.84 % (2199250)Time elapsed: 13.893 s % 300.62/42.84 % (2199250)Peak memory usage: 142 MB % 300.62/42.84 % (2199250)Instructions burned: 29342 (million) % 300.62/42.84 % (2199508)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=4104916462:i=8173:av=off_2710 on theBenchmark for (2710ds/8173Mi) % 300.62/42.84 % (2199260)Instruction limit reached! % 300.62/42.84 % (2199260)------------------------------ % 300.62/42.84 % (2199260)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.62/42.84 % (2199260)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.62/42.84 % (2199260)CaDiCaL version: 2.1.3 % 300.62/42.84 % (2199260)Termination reason: Instruction limit % 300.62/42.84 % (2199260)Termination phase: Saturation % 300.62/42.84 % (2199260)Time elapsed: 15.462 s % 300.62/42.84 % (2199260)Peak memory usage: 172 MB % 300.62/42.84 % (2199260)Instructions burned: 22565 (million) % 300.62/42.84 % (2199692)dis+10_16:1_sil=16000:random_seed=2379450896:i=9155:fsr=off_2651 on theBenchmark for (2651ds/9155Mi) % 300.62/42.84 % (2199508)Instruction limit reached! % 300.62/42.84 % (2199508)------------------------------ % 300.62/42.84 % (2199508)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.62/42.84 % (2199508)Linked wi % 300.62/42.84 Terminated %------------------------------------------------------------------------------