%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWV361-1 : TPTP v9.3.1. Released v3.2.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % Computer : n015.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:21:04 PM UTC 2026 % Result : Timeout 290.28s 41.44s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.05 % Problem : SWV361-1 : TPTP v9.3.1. Released v3.2.0. % 0.00/0.08 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.21/0.32 % Computer : n015.cluster.edu % 0.21/0.32 % Model : x86_64 x86_64 % 0.21/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.21/0.32 % Memory : 8046.5625MB % 0.21/0.32 % OS : Linux 6.8.0-71-generic % 0.21/0.32 % CPULimit : 300 % 0.21/0.32 % WCLimit : 300 % 0.21/0.32 % DateTime : Mon Sep 28 10:47:02 UTC 2026 % 0.21/0.32 % CPUTime : % 0.21/0.32 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.21/0.35 Running first-order model finding % 0.21/0.35 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 7.51/1.66 % (2537484)Will run a generic schedule for satisfiability detection. % 7.51/1.66 % (2537490)% WARNING: option uhcvi not known. % 7.51/1.66 % (2537492)dis+10_1_sil=32000:sp=arity:random_seed=2146560570:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 7.51/1.66 % (2537489)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=826883070_2999 on theBenchmark for (2999ds/0Mi) % 7.51/1.66 % (2537490)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3931028445:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 7.51/1.66 % (2537491)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1193116977:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 7.51/1.66 % (2537494)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=212807461:i=131_2999 on theBenchmark for (2999ds/131Mi) % 7.51/1.66 % (2537493)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3481710612:i=116_2999 on theBenchmark for (2999ds/116Mi) % 7.51/1.66 % (2537495)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1728287765:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 7.51/1.66 % (2537494)Instruction limit reached! % 7.51/1.66 % (2537494)------------------------------ % 7.51/1.66 % (2537494)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.51/1.66 % (2537494)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.51/1.66 % (2537494)CaDiCaL version: 2.1.3 % 7.51/1.66 % (2537494)Termination reason: Instruction limit % 7.51/1.66 % (2537494)Termination phase: Saturation % 7.51/1.66 % (2537494)Time elapsed: 0.039 s % 7.51/1.66 % (2537494)Peak memory usage: 17 MB % 7.51/1.66 % (2537494)Instructions burned: 131 (million) % 7.51/1.66 % (2537503)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2732548019:i=714:nm=2_2998 on theBenchmark for (2998ds/714Mi) % 7.51/1.66 % (2537492)Instruction limit reached! % 7.51/1.66 % (2537492)------------------------------ % 7.51/1.66 % (2537492)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.51/1.66 % (2537492)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.51/1.66 % (2537492)CaDiCaL version: 2.1.3 % 7.51/1.66 % (2537492)Termination reason: Instruction limit % 7.51/1.66 % (2537492)Termination phase: Saturation % 7.51/1.66 % (2537492)Time elapsed: 0.060 s % 7.51/1.66 % (2537492)Peak memory usage: 15 MB % 7.51/1.66 % (2537492)Instructions burned: 103 (million) % 7.51/1.66 % (2537505)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=386822257:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi) % 7.51/1.66 % (2537495)Instruction limit reached! % 7.51/1.66 % (2537495)------------------------------ % 7.51/1.66 % (2537495)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.51/1.66 % (2537495)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.51/1.66 % (2537495)CaDiCaL version: 2.1.3 % 7.51/1.66 % (2537495)Termination reason: Instruction limit % 7.51/1.66 % (2537495)Termination phase: Saturation % 7.51/1.66 % (2537495)Time elapsed: 0.096 s % 7.51/1.66 % (2537495)Peak memory usage: 17 MB % 7.51/1.66 % (2537495)Instructions burned: 159 (million) % 7.51/1.66 % (2537493)Instruction limit reached! % 7.51/1.66 % (2537493)------------------------------ % 7.51/1.66 % (2537493)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.51/1.66 % (2537493)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.51/1.66 % (2537493)CaDiCaL version: 2.1.3 % 7.51/1.66 % (2537493)Termination reason: Instruction limit % 7.51/1.66 % (2537493)Termination phase: Saturation % 7.51/1.66 % (2537493)Time elapsed: 0.103 s % 7.51/1.66 % (2537493)Peak memory usage: 16 MB % 7.51/1.66 % (2537493)Instructions burned: 117 (million) % 7.51/1.66 % (2537507)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=3052115610:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi) % 7.51/1.66 % (2537508)ott-21_1_sil=16000:fs=off:random_seed=1428209927:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 7.51/1.66 % (2537505)Instruction limit reached! % 7.51/1.66 % (2537505)------------------------------ % 7.51/1.66 % (2537505)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.51/1.66 % (2537505)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.51/1.66 % (2537505)CaDiCaL version: 2.1.3 % 28.92/4.53 % (2537505)Termination reason: Instruction limit % 28.92/4.53 % (2537505)Termination phase: Saturation % 28.92/4.53 % (2537505)Time elapsed: 0.075 s % 28.92/4.53 % (2537505)Peak memory usage: 16 MB % 28.92/4.53 % (2537505)Instructions burned: 132 (million) % 28.92/4.53 % (2537511)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1377445307:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi) % 28.92/4.53 % (2537508)Instruction limit reached! % 28.92/4.53 % (2537508)------------------------------ % 28.92/4.53 % (2537508)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 28.92/4.53 % (2537508)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.92/4.53 % (2537508)CaDiCaL version: 2.1.3 % 28.92/4.53 % (2537508)Termination reason: Instruction limit % 28.92/4.53 % (2537508)Termination phase: Saturation % 28.92/4.53 % (2537508)Time elapsed: 0.093 s % 28.92/4.53 % (2537508)Peak memory usage: 16 MB % 28.92/4.53 % (2537508)Instructions burned: 182 (million) % 28.92/4.53 % (2537503)Instruction limit reached! % 28.92/4.53 % (2537503)------------------------------ % 28.92/4.53 % (2537503)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 28.92/4.53 % (2537503)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.92/4.53 % (2537503)CaDiCaL version: 2.1.3 % 28.92/4.53 % (2537503)Termination reason: Instruction limit % 28.92/4.53 % (2537503)Termination phase: Finite model building preprocessing % 28.92/4.53 % (2537503)Time elapsed: 0.183 s % 28.92/4.53 % (2537503)Peak memory usage: 24 MB % 28.92/4.53 % (2537503)Instructions burned: 717 (million) % 28.92/4.53 % (2537513)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2299241739:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi) % 28.92/4.53 % (2537514)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3708167359:i=1179_2996 on theBenchmark for (2996ds/1179Mi) % 28.92/4.53 % TRYING [1] % 28.92/4.53 % TRYING [2] % 28.92/4.53 % (2537511)Instruction limit reached! % 28.92/4.53 % (2537511)------------------------------ % 28.92/4.53 % (2537511)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 28.92/4.53 % (2537511)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.92/4.53 % (2537511)CaDiCaL version: 2.1.3 % 28.92/4.53 % (2537511)Termination reason: Instruction limit % 28.92/4.53 % (2537511)Termination phase: Saturation % 28.92/4.53 % (2537511)Time elapsed: 0.288 s % 28.92/4.53 % (2537511)Peak memory usage: 17 MB % 28.92/4.53 % (2537511)Instructions burned: 478 (million) % 28.92/4.53 % (2537507)Instruction limit reached! % 28.92/4.53 % (2537507)------------------------------ % 28.92/4.53 % (2537507)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 28.92/4.53 % (2537507)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.92/4.53 % (2537507)CaDiCaL version: 2.1.3 % 28.92/4.53 % (2537507)Termination reason: Instruction limit % 28.92/4.53 % (2537507)Termination phase: Saturation % 28.92/4.53 % (2537507)Time elapsed: 0.346 s % 28.92/4.53 % (2537507)Peak memory usage: 19 MB % 28.92/4.53 % (2537507)Instructions burned: 685 (million) % 28.92/4.53 % (2537517)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=4237233483:i=889:ins=1_2994 on theBenchmark for (2994ds/889Mi) % 28.92/4.53 % (2537518)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=2357868912:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2994 on theBenchmark for (2994ds/692Mi) % 28.92/4.53 % TRYING [1] % 28.92/4.53 % (2537514)Instruction limit reached! % 28.92/4.53 % (2537514)------------------------------ % 28.92/4.53 % (2537514)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 28.92/4.53 % (2537514)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.92/4.53 % (2537514)CaDiCaL version: 2.1.3 % 28.92/4.53 % (2537514)Termination reason: Instruction limit % 28.92/4.53 % (2537514)Termination phase: Saturation % 28.92/4.53 % (2537514)Time elapsed: 0.391 s % 28.92/4.53 % (2537514)Peak memory usage: 29 MB % 28.92/4.53 % (2537514)Instructions burned: 1180 (million) % 28.92/4.53 % (2537521)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=836399787:i=879:kws=inv_precedence:fsr=off_2992 on theBenchmark for (2992ds/879Mi) % 28.92/4.53 % (2537513)Instruction limit reached! % 28.92/4.53 % (2537513)------------------------------ % 28.92/4.53 % (2537513)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 28.92/4.53 % (2537513)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 60.44/8.93 % (2537513)CaDiCaL version: 2.1.3 % 60.44/8.93 % (2537513)Termination reason: Instruction limit % 60.44/8.93 % (2537513)Termination phase: Finite model building constraint generation % 60.44/8.93 % (2537513)Time elapsed: 0.423 s % 60.44/8.93 % (2537513)Peak memory usage: 30 MB % 60.44/8.93 % (2537513)Instructions burned: 866 (million) % 60.44/8.93 % (2537523)fmb+10_1_sil=64000:random_seed=2555917165:i=22061:nm=2:gsp=on_2992 on theBenchmark for (2992ds/22061Mi) % 60.44/8.93 % (2537517)Cannot represent all propositional literals internally % 60.44/8.93 % (2537517)Refutation not found, incomplete strategy % 60.44/8.93 % (2537517)------------------------------ % 60.44/8.93 % (2537517)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 60.44/8.93 % (2537517)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 60.44/8.93 % (2537517)CaDiCaL version: 2.1.3 % 60.44/8.93 % (2537517)Termination reason: Refutation not found, incomplete strategy % 60.44/8.93 % (2537517)Time elapsed: 0.345 s % 60.44/8.93 % (2537517)Peak memory usage: 25 MB % 60.44/8.93 % (2537517)Instructions burned: 697 (million) % 60.44/8.93 % (2537517)------------------------------ % 60.44/8.93 % (2537517)------------------------------ % 60.44/8.93 % (2537525)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3448969946:i=9515:nm=5_2990 on theBenchmark for (2990ds/9515Mi) % 60.44/8.93 % (2537521)Instruction limit reached! % 60.44/8.93 % (2537521)------------------------------ % 60.44/8.93 % (2537521)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 60.44/8.93 % (2537521)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 60.44/8.93 % (2537521)CaDiCaL version: 2.1.3 % 60.44/8.93 % (2537521)Termination reason: Instruction limit % 60.44/8.93 % (2537521)Termination phase: Saturation % 60.44/8.93 % (2537521)Time elapsed: 0.228 s % 60.44/8.93 % (2537521)Peak memory usage: 21 MB % 60.44/8.93 % (2537521)Instructions burned: 883 (million) % 60.44/8.93 % (2537518)Instruction limit reached! % 60.44/8.93 % (2537518)------------------------------ % 60.44/8.93 % (2537518)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 60.44/8.93 % (2537518)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 60.44/8.93 % (2537518)CaDiCaL version: 2.1.3 % 60.44/8.93 % (2537518)Termination reason: Instruction limit % 60.44/8.93 % (2537518)Termination phase: Saturation % 60.44/8.93 % (2537527)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1663726424:fmbsr=1.7:i=920_2990 on theBenchmark for (2990ds/920Mi) % 60.44/8.93 % (2537518)Time elapsed: 0.402 s % 60.44/8.93 % (2537518)Peak memory usage: 24 MB % 60.44/8.93 % (2537518)Instructions burned: 693 (million) % 60.44/8.93 % (2537529)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=3873670162:i=5131_2990 on theBenchmark for (2990ds/5131Mi) % 60.44/8.93 % TRYING [1] % 60.44/8.93 % (2537527)Cannot represent all propositional literals internally % 60.44/8.93 % (2537527)Refutation not found, incomplete strategy % 60.44/8.93 % (2537527)------------------------------ % 60.44/8.93 % (2537527)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 60.44/8.93 % (2537527)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 60.44/8.93 % (2537527)CaDiCaL version: 2.1.3 % 60.44/8.93 % (2537527)Termination reason: Refutation not found, incomplete strategy % 60.44/8.93 % (2537527)Time elapsed: 0.182 s % 60.44/8.93 % (2537527)Peak memory usage: 25 MB % 60.44/8.93 % (2537527)Instructions burned: 693 (million) % 60.44/8.93 % (2537527)------------------------------ % 60.44/8.93 % (2537527)------------------------------ % 60.44/8.93 % (2537531)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1633069201:i=1472:ins=7:fdi=8:gsp=on_2988 on theBenchmark for (2988ds/1472Mi) % 60.44/8.93 % (2537525)Cannot represent all propositional literals internally % 60.44/8.93 % (2537525)Refutation not found, incomplete strategy % 60.44/8.93 % (2537525)------------------------------ % 60.44/8.93 % (2537525)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 60.44/8.93 % (2537525)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 60.44/8.93 % (2537525)CaDiCaL version: 2.1.3 % 60.44/8.93 % (2537525)Termination reason: Refutation not found, incomplete strategy % 60.44/8.93 % (2537525)Time elapsed: 0.341 s % 60.44/8.93 % (2537525)Peak memory usage: 25 MB % 60.44/8.93 % (2537525)Instructions burned: 693 (million) % 60.44/8.93 % (2537525)------------------------------ % 60.44/8.93 % (2537525)------------------------------ % 60.44/8.93 % (2537533)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=1440543603:i=6324_2987 on theBenchmark for (2987ds/6324Mi) % 82.75/12.11 % TRYING [2] % 82.75/12.11 % (2537533)Cannot represent all propositional literals internally % 82.75/12.11 % (2537533)Refutation not found, incomplete strategy % 82.75/12.11 % (2537533)------------------------------ % 82.75/12.11 % (2537533)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 82.75/12.11 % (2537533)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 82.75/12.11 % (2537533)CaDiCaL version: 2.1.3 % 82.75/12.11 % (2537533)Termination reason: Refutation not found, incomplete strategy % 82.75/12.11 % (2537533)Time elapsed: 0.353 s % 82.75/12.11 % (2537533)Peak memory usage: 26 MB % 82.75/12.11 % (2537533)Instructions burned: 715 (million) % 82.75/12.11 % (2537533)------------------------------ % 82.75/12.11 % (2537533)------------------------------ % 82.75/12.11 % (2537535)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1331545570:fmbsr=2.30978:i=2174_2983 on theBenchmark for (2983ds/2174Mi) % 82.75/12.11 % (2537531)Instruction limit reached! % 82.75/12.11 % (2537531)------------------------------ % 82.75/12.11 % (2537531)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 82.75/12.11 % (2537531)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 82.75/12.11 % (2537531)CaDiCaL version: 2.1.3 % 82.75/12.11 % (2537531)Termination reason: Instruction limit % 82.75/12.11 % (2537531)Termination phase: Saturation % 82.75/12.11 % (2537531)Time elapsed: 0.599 s % 82.75/12.11 % (2537531)Peak memory usage: 35 MB % 82.75/12.11 % (2537531)Instructions burned: 1475 (million) % 82.75/12.11 % (2537537)ott-2_1_sil=16000:newcnf=on:random_seed=3787046738:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2982 on theBenchmark for (2982ds/869Mi) % 82.75/12.11 % (2537537)Instruction limit reached! % 82.75/12.11 % (2537537)------------------------------ % 82.75/12.11 % (2537537)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 82.75/12.11 % (2537537)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 82.75/12.11 % (2537537)CaDiCaL version: 2.1.3 % 82.75/12.11 % (2537537)Termination reason: Instruction limit % 82.75/12.11 % (2537537)Termination phase: Saturation % 82.75/12.11 % (2537537)Time elapsed: 0.236 s % 82.75/12.11 % (2537537)Peak memory usage: 18 MB % 82.75/12.11 % (2537537)Instructions burned: 870 (million) % 82.75/12.11 % (2537539)ott+10_1_sil=32000:tgt=ground:random_seed=1434067391:i=5114:av=off_2979 on theBenchmark for (2979ds/5114Mi) % 82.75/12.11 % (2537535)Instruction limit reached! % 82.75/12.11 % (2537535)------------------------------ % 82.75/12.11 % (2537535)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 82.75/12.11 % (2537535)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 82.75/12.11 % (2537535)CaDiCaL version: 2.1.3 % 82.75/12.11 % (2537535)Termination reason: Instruction limit % 82.75/12.11 % (2537535)Termination phase: Finite model building preprocessing % 82.75/12.11 % (2537535)Time elapsed: 1.082 s % 82.75/12.11 % (2537535)Peak memory usage: 42 MB % 82.75/12.11 % (2537535)Instructions burned: 2175 (million) % 82.75/12.11 % (2537541)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=979375685:i=54282_2972 on theBenchmark for (2972ds/54282Mi) % 82.75/12.11 % TRYING [1] % 82.75/12.11 % TRYING [2] % 82.75/12.11 % (2537539)Instruction limit reached! % 82.75/12.11 % (2537539)------------------------------ % 82.75/12.11 % (2537539)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 82.75/12.11 % (2537539)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 82.75/12.11 % (2537539)CaDiCaL version: 2.1.3 % 82.75/12.11 % (2537539)Termination reason: Instruction limit % 82.75/12.11 % (2537539)Termination phase: Saturation % 82.75/12.11 % (2537539)Time elapsed: 1.800 s % 82.75/12.11 % (2537539)Peak memory usage: 69 MB % 82.75/12.11 % (2537539)Instructions burned: 5117 (million) % 82.75/12.11 % (2537543)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3314656297:i=3512:aac=none_2961 on theBenchmark for (2961ds/3512Mi) % 82.75/12.11 % (2537529)Instruction limit reached! % 82.75/12.11 % (2537529)------------------------------ % 82.75/12.11 % (2537529)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 82.75/12.11 % (2537529)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 82.75/12.11 % (2537529)CaDiCaL version: 2.1.3 % 82.75/12.11 % (2537529)Termination reason: Instruction limit % 82.75/12.11 % (2537529)Termination phase: Saturation % 82.75/12.11 % (2537529)Time elapsed: 3.181 s % 82.75/12.11 % (2537529)Peak memory usage: 52 MB % 82.75/12.11 % (2537529)Instructions burned: 5131 (million) % 127.74/20.33 % (2537545)dis+21_1_sil=32000:sas=cadical:random_seed=1187084306:i=3773:amm=off_2958 on theBenchmark for (2958ds/3773Mi) % 127.74/20.33 % (2537543)Instruction limit reached! % 127.74/20.33 % (2537543)------------------------------ % 127.74/20.33 % (2537543)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 127.74/20.33 % (2537543)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 127.74/20.33 % (2537543)CaDiCaL version: 2.1.3 % 127.74/20.33 % (2537543)Termination reason: Instruction limit % 127.74/20.33 % (2537543)Termination phase: Saturation % 127.74/20.33 % (2537543)Time elapsed: 1.155 s % 127.74/20.33 % (2537543)Peak memory usage: 47 MB % 127.74/20.33 % (2537543)Instructions burned: 3515 (million) % 127.74/20.33 % (2537547)ott+11_1_sil=16000:gs=on:random_seed=196976086:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2949 on theBenchmark for (2949ds/2251Mi) % 127.74/20.33 % (2537547)Instruction limit reached! % 127.74/20.33 % (2537547)------------------------------ % 127.74/20.33 % (2537547)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 127.74/20.33 % (2537547)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 127.74/20.33 % (2537547)CaDiCaL version: 2.1.3 % 127.74/20.33 % (2537547)Termination reason: Instruction limit % 127.74/20.33 % (2537547)Termination phase: Saturation % 127.74/20.33 % (2537547)Time elapsed: 0.811 s % 127.74/20.33 % (2537547)Peak memory usage: 82 MB % 127.74/20.33 % (2537547)Instructions burned: 2252 (million) % 127.74/20.33 % (2537549)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=3702663246:fmbsr=1.6:i=67534_2941 on theBenchmark for (2941ds/67534Mi) % 127.74/20.33 % (2537549)Cannot represent all propositional literals internally % 127.74/20.33 % (2537549)Refutation not found, incomplete strategy % 127.74/20.33 % (2537549)------------------------------ % 127.74/20.33 % (2537549)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 127.74/20.33 % (2537549)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 127.74/20.33 % (2537549)CaDiCaL version: 2.1.3 % 127.74/20.33 % (2537549)Termination reason: Refutation not found, incomplete strategy % 127.74/20.33 % (2537549)Time elapsed: 0.189 s % 127.74/20.33 % (2537549)Peak memory usage: 24 MB % 127.74/20.33 % (2537549)Instructions burned: 724 (million) % 127.74/20.33 % (2537549)------------------------------ % 127.74/20.33 % (2537549)------------------------------ % 127.74/20.33 % (2537551)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=4182951666:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2939 on theBenchmark for (2939ds/4591Mi) % 127.74/20.33 % (2537545)Instruction limit reached! % 127.74/20.33 % (2537545)------------------------------ % 127.74/20.33 % (2537545)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 127.74/20.33 % (2537545)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 127.74/20.33 % (2537545)CaDiCaL version: 2.1.3 % 127.74/20.33 % (2537545)Termination reason: Instruction limit % 127.74/20.33 % (2537545)Termination phase: Saturation % 127.74/20.33 % (2537545)Time elapsed: 2.255 s % 127.74/20.33 % (2537545)Peak memory usage: 40 MB % 127.74/20.33 % (2537545)Instructions burned: 3774 (million) % 127.74/20.33 % (2537553)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=3719158724:i=29340_2935 on theBenchmark for (2935ds/29340Mi) % 127.74/20.33 % (2537551)Instruction limit reached! % 127.74/20.33 % (2537551)------------------------------ % 127.74/20.33 % (2537551)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 127.74/20.33 % (2537551)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 127.74/20.33 % (2537551)CaDiCaL version: 2.1.3 % 127.74/20.33 % (2537551)Termination reason: Instruction limit % 127.74/20.33 % (2537551)Termination phase: Saturation % 127.74/20.33 % (2537551)Time elapsed: 1.115 s % 127.74/20.33 % (2537551)Peak memory usage: 43 MB % 127.74/20.33 % (2537551)Instructions burned: 4594 (million) % 127.74/20.33 % (2537555)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=4063644453:i=5211_2928 on theBenchmark for (2928ds/5211Mi) % 127.74/20.33 % (2537489)Cannot represent all propositional literals internally % 127.74/20.33 % (2537555)Instruction limit reached! % 127.74/20.33 % (2537555)------------------------------ % 127.74/20.33 % (2537555)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 127.74/20.33 % (2537555)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 127.74/20.33 % (2537555)CaDiCaL version: 2.1.3 % 127.74/20.33 % (2537555)Termination reason: Instruction limit % 127.74/20.33 % (2537555)Termination phase: Saturation % 168.63/24.17 % (2537555)Time elapsed: 1.378 s % 168.63/24.17 % (2537555)Peak memory usage: 43 MB % 168.63/24.17 % (2537555)Instructions burned: 5215 (million) % 168.63/24.17 % (2537557)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=23376362:i=5497:nm=2_2914 on theBenchmark for (2914ds/5497Mi) % 168.63/24.17 % (2537557)Cannot represent all propositional literals internally % 168.63/24.17 % (2537557)Refutation not found, incomplete strategy % 168.63/24.17 % (2537557)------------------------------ % 168.63/24.17 % (2537557)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 168.63/24.17 % (2537557)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 168.63/24.17 % (2537557)CaDiCaL version: 2.1.3 % 168.63/24.17 % (2537557)Termination reason: Refutation not found, incomplete strategy % 168.63/24.17 % (2537557)Time elapsed: 0.196 s % 168.63/24.17 % (2537557)Peak memory usage: 26 MB % 168.63/24.17 % (2537557)Instructions burned: 715 (million) % 168.63/24.17 % (2537557)------------------------------ % 168.63/24.17 % (2537557)------------------------------ % 168.63/24.17 % (2537559)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=1300923698:fmbsr=2:i=46332_2912 on theBenchmark for (2912ds/46332Mi) % 168.63/24.17 % (2537489)Refutation not found, incomplete strategy % 168.63/24.17 % (2537489)------------------------------ % 168.63/24.17 % (2537489)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 168.63/24.17 % (2537489)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 168.63/24.17 % (2537489)CaDiCaL version: 2.1.3 % 168.63/24.17 % (2537489)Termination reason: Refutation not found, incomplete strategy % 168.63/24.17 % (2537489)Time elapsed: 8.867 s % 168.63/24.17 % (2537489)Peak memory usage: 983 MB % 168.63/24.17 % (2537489)Instructions burned: 14876 (million) % 168.63/24.17 % (2537489)------------------------------ % 168.63/24.17 % (2537489)------------------------------ % 168.63/24.17 % (2537559)Cannot represent all propositional literals internally % 168.63/24.17 % (2537559)Refutation not found, incomplete strategy % 168.63/24.17 % (2537559)------------------------------ % 168.63/24.17 % (2537559)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 168.63/24.17 % (2537559)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 168.63/24.17 % (2537559)CaDiCaL version: 2.1.3 % 168.63/24.17 % (2537559)Termination reason: Refutation not found, incomplete strategy % 168.63/24.17 % (2537559)Time elapsed: 0.190 s % 168.63/24.17 % (2537559)Peak memory usage: 24 MB % 168.63/24.17 % (2537559)Instructions burned: 724 (million) % 168.63/24.17 % (2537559)------------------------------ % 168.63/24.17 % (2537559)------------------------------ % 168.63/24.17 % (2537561)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=578275758:i=14071_2910 on theBenchmark for (2910ds/14071Mi) % 168.63/24.17 % (2537563)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1150196166:i=22565:add=on:rawr=on_2909 on theBenchmark for (2909ds/22565Mi) % 168.63/24.17 % (2537561)Cannot represent all propositional literals internally % 168.63/24.17 % (2537561)Refutation not found, incomplete strategy % 168.63/24.17 % (2537561)------------------------------ % 168.63/24.17 % (2537561)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 168.63/24.17 % (2537561)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 168.63/24.17 % (2537561)CaDiCaL version: 2.1.3 % 168.63/24.17 % (2537561)Termination reason: Refutation not found, incomplete strategy % 168.63/24.17 % (2537561)Time elapsed: 0.190 s % 168.63/24.17 % (2537561)Peak memory usage: 25 MB % 168.63/24.17 % (2537561)Instructions burned: 694 (million) % 168.63/24.17 % (2537561)------------------------------ % 168.63/24.17 % (2537561)------------------------------ % 168.63/24.17 % (2537565)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=866049727:i=8173:av=off_2908 on theBenchmark for (2908ds/8173Mi) % 168.63/24.17 % (2537541)Cannot represent all propositional literals internally % 168.63/24.17 % (2537541)Refutation not found, incomplete strategy % 168.63/24.17 % (2537541)------------------------------ % 168.63/24.17 % (2537541)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 168.63/24.17 % (2537541)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 168.63/24.17 % (2537541)CaDiCaL version: 2.1.3 % 168.63/24.17 % (2537541)Termination reason: Refutation not found, incomplete strategy % 168.63/24.17 % (2537541)Time elapsed: 8.956 s % 168.63/24.17 % (2537541)Peak memory usage: 983 MB % 168.63/24.17 % (2537541)Instructions burned: 14875 (million) % 168.63/24.17 % (2537541)------------------------------ % 206.00/29.41 % (2537541)------------------------------ % 206.00/29.41 % (2537567)dis+10_16:1_sil=16000:random_seed=646716812:i=9155:fsr=off_2881 on theBenchmark for (2881ds/9155Mi) % 206.00/29.41 % (2537565)Instruction limit reached! % 206.00/29.41 % (2537565)------------------------------ % 206.00/29.41 % (2537565)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 206.00/29.41 % (2537565)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 206.00/29.41 % (2537565)CaDiCaL version: 2.1.3 % 206.00/29.41 % (2537565)Termination reason: Instruction limit % 206.00/29.41 % (2537565)Termination phase: Saturation % 206.00/29.41 % (2537565)Time elapsed: 2.865 s % 206.00/29.41 % (2537565)Peak memory usage: 86 MB % 206.00/29.41 % (2537565)Instructions burned: 8173 (million) % 206.00/29.41 % (2537569)ott-3_8_sil=64000:random_seed=2415848486:i=20139:bs=on_2879 on theBenchmark for (2879ds/20139Mi) % 206.00/29.41 % (2537523)Instruction limit reached! % 206.00/29.41 % (2537523)------------------------------ % 206.00/29.41 % (2537523)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 206.00/29.41 % (2537523)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 206.00/29.41 % (2537523)CaDiCaL version: 2.1.3 % 206.00/29.41 % (2537523)Termination reason: Instruction limit % 206.00/29.41 % (2537523)Termination phase: Finite model building SAT solving % 206.00/29.41 % (2537523)Time elapsed: 13.691 s % 206.00/29.41 % (2537523)Peak memory usage: 744 MB % 206.00/29.41 % (2537523)Instructions burned: 22064 (million) % 206.00/29.41 % (2537571)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=3533107652:fmbsr=2:i=32576_2854 on theBenchmark for (2854ds/32576Mi) % 206.00/29.41 % (2537571)Cannot represent all propositional literals internally % 206.00/29.41 % (2537571)Refutation not found, incomplete strategy % 206.00/29.41 % (2537571)------------------------------ % 206.00/29.41 % (2537571)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 206.00/29.41 % (2537571)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 206.00/29.41 % (2537571)CaDiCaL version: 2.1.3 % 206.00/29.41 % (2537571)Termination reason: Refutation not found, incomplete strategy % 206.00/29.41 % (2537571)Time elapsed: 0.359 s % 206.00/29.41 % (2537571)Peak memory usage: 26 MB % 206.00/29.41 % (2537571)Instructions burned: 716 (million) % 206.00/29.41 % (2537571)------------------------------ % 206.00/29.41 % (2537571)------------------------------ % 206.00/29.41 % (2537573)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=1901913048:i=11404_2850 on theBenchmark for (2850ds/11404Mi) % 206.00/29.41 % (2537567)Instruction limit reached! % 206.00/29.41 % (2537567)------------------------------ % 206.00/29.41 % (2537567)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 206.00/29.41 % (2537567)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 206.00/29.41 % (2537567)CaDiCaL version: 2.1.3 % 206.00/29.41 % (2537567)Termination reason: Instruction limit % 206.00/29.41 % (2537567)Termination phase: Saturation % 206.00/29.41 % (2537567)Time elapsed: 5.216 s % 206.00/29.41 % (2537567)Peak memory usage: 89 MB % 206.00/29.41 % (2537567)Instructions burned: 9156 (million) % 206.00/29.41 % (2537575)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=39786230:i=14134_2828 on theBenchmark for (2828ds/14134Mi) % 206.00/29.41 % (2537569)Instruction limit reached! % 206.00/29.41 % (2537569)------------------------------ % 206.00/29.41 % (2537569)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 206.00/29.41 % (2537569)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 206.00/29.41 % (2537569)CaDiCaL version: 2.1.3 % 206.00/29.41 % (2537569)Termination reason: Instruction limit % 206.00/29.41 % (2537569)Termination phase: Saturation % 206.00/29.41 % (2537569)Time elapsed: 6.879 s % 206.00/29.41 % (2537569)Peak memory usage: 106 MB % 206.00/29.41 % (2537569)Instructions burned: 20140 (million) % 206.00/29.41 % (2537577)dis+33_16_sil=32000:sac=on:random_seed=2136739322:i=15851:nm=0_2810 on theBenchmark for (2810ds/15851Mi) % 206.00/29.41 % (2537553)Instruction limit reached! % 206.00/29.41 % (2537553)------------------------------ % 206.00/29.41 % (2537553)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 206.00/29.41 % (2537553)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 206.00/29.41 % (2537553)CaDiCaL version: 2.1.3 % 206.00/29.41 % (2537553)Termination reason: Instruction limit % 206.00/29.41 % (2537553)Termination phase: Saturation % 206.00/29.41 % (2537553)Time elapsed: 13.415 s % 206.00/29.41 % (2537553)Peak memory usage: 446 MB % 206.00/29.41 % (2537553)Instructions burned: 29341 (million) % 206.00/29.41 % (2537579)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=1816899041:avsq=on:i=17627:add=on:amm=off_2800 on theBenchmark for (2800ds/17627Mi) % 230.08/33.03 % (2537573)Instruction limit reached! % 230.08/33.03 % (2537573)------------------------------ % 230.08/33.03 % (2537573)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 230.08/33.03 % (2537573)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 230.08/33.03 % (2537573)CaDiCaL version: 2.1.3 % 230.08/33.03 % (2537573)Termination reason: Instruction limit % 230.08/33.03 % (2537573)Termination phase: Saturation % 230.08/33.03 % (2537573)Time elapsed: 7.448 s % 230.08/33.03 % (2537573)Peak memory usage: 131 MB % 230.08/33.03 % (2537573)Instructions burned: 11405 (million) % 230.08/33.03 % (2537581)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=2249884816:s2a=on:i=53295_2775 on theBenchmark for (2775ds/53295Mi) % 230.08/33.03 % (2537577)Instruction limit reached! % 230.08/33.03 % (2537577)------------------------------ % 230.08/33.03 % (2537577)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 230.08/33.03 % (2537577)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 230.08/33.03 % (2537577)CaDiCaL version: 2.1.3 % 230.08/33.03 % (2537577)Termination reason: Instruction limit % 230.08/33.03 % (2537577)Termination phase: Saturation % 230.08/33.03 % (2537577)Time elapsed: 4.171 s % 230.08/33.03 % (2537577)Peak memory usage: 226 MB % 230.08/33.03 % (2537577)Instructions burned: 15854 (million) % 230.08/33.03 % (2537583)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=394819280:i=26857:ins=20_2768 on theBenchmark for (2768ds/26857Mi) % 230.08/33.03 % (2537563)Instruction limit reached! % 230.08/33.03 % (2537563)------------------------------ % 230.08/33.03 % (2537563)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 230.08/33.03 % (2537563)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 230.08/33.03 % (2537563)CaDiCaL version: 2.1.3 % 230.08/33.03 % (2537563)Termination reason: Instruction limit % 230.08/33.03 % (2537563)Termination phase: Saturation % 230.08/33.03 % (2537563)Time elapsed: 14.239 s % 230.08/33.03 % (2537563)Peak memory usage: 459 MB % 230.08/33.03 % (2537563)Instructions burned: 22566 (million) % 230.08/33.03 % (2537583)Cannot represent all propositional literals internally % 230.08/33.03 % (2537583)Refutation not found, incomplete strategy % 230.08/33.03 % (2537583)------------------------------ % 230.08/33.03 % (2537583)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 230.08/33.03 % (2537583)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 230.08/33.03 % (2537583)CaDiCaL version: 2.1.3 % 230.08/33.03 % (2537583)Termination reason: Refutation not found, incomplete strategy % 230.08/33.03 % (2537583)Time elapsed: 0.184 s % 230.08/33.03 % (2537583)Peak memory usage: 25 MB % 230.08/33.03 % (2537583)Instructions burned: 693 (million) % 230.08/33.03 % (2537583)------------------------------ % 230.08/33.03 % (2537583)------------------------------ % 230.08/33.03 % (2537585)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=4249375831:i=28120:bs=on:fsr=off_2766 on theBenchmark for (2766ds/28120Mi) % 230.08/33.03 % (2537586)fmb+10_1_sil=256000:fmbss=7:random_seed=4094853132:fmbsr=1.6:i=182295_2766 on theBenchmark for (2766ds/182295Mi) % 230.08/33.03 % (2537586)Cannot represent all propositional literals internally % 230.08/33.03 % (2537586)Refutation not found, incomplete strategy % 230.08/33.03 % (2537586)------------------------------ % 230.08/33.03 % (2537586)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 230.08/33.03 % (2537586)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 230.08/33.03 % (2537586)CaDiCaL version: 2.1.3 % 230.08/33.03 % (2537586)Termination reason: Refutation not found, incomplete strategy % 230.08/33.03 % (2537586)Time elapsed: 0.200 s % 230.08/33.03 % (2537586)Peak memory usage: 26 MB % 230.08/33.03 % (2537586)Instructions burned: 693 (million) % 230.08/33.03 % (2537586)------------------------------ % 230.08/33.03 % (2537586)------------------------------ % 230.08/33.03 % (2537589)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=3427484495:i=44625:gsp=on_2763 on theBenchmark for (2763ds/44625Mi) % 230.08/33.03 % (2537589)Cannot represent all propositional literals internally % 230.08/33.03 % (2537589)Refutation not found, incomplete strategy % 230.08/33.03 % (2537589)------------------------------ % 230.08/33.03 % (2537589)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 230.08/33.03 % (2537589)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 230.08/33.03 % (2537589)CaDiCaL version: 2.1.3 % 247.35/35.32 % (2537589)Termination reason: Refutation not found, incomplete strategy % 247.35/35.32 % (2537589)Time elapsed: 0.181 s % 247.35/35.32 % (2537589)Peak memory usage: 25 MB % 247.35/35.32 % (2537589)Instructions burned: 691 (million) % 247.35/35.32 % (2537589)------------------------------ % 247.35/35.32 % (2537589)------------------------------ % 247.35/35.32 % (2537591)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=109353299:i=160505_2761 on theBenchmark for (2761ds/160505Mi) % 247.35/35.32 % (2537591)Cannot represent all propositional literals internally % 247.35/35.32 % (2537591)Refutation not found, incomplete strategy % 247.35/35.32 % (2537591)------------------------------ % 247.35/35.32 % (2537591)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 247.35/35.32 % (2537591)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 247.35/35.32 % (2537591)CaDiCaL version: 2.1.3 % 247.35/35.32 % (2537591)Termination reason: Refutation not found, incomplete strategy % 247.35/35.32 % (2537591)Time elapsed: 0.183 s % 247.35/35.32 % (2537591)Peak memory usage: 25 MB % 247.35/35.32 % (2537591)Instructions burned: 693 (million) % 247.35/35.32 % (2537591)------------------------------ % 247.35/35.32 % (2537591)------------------------------ % 247.35/35.32 % (2537593)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=1329353040:fmbsr=1.3:i=225729_2759 on theBenchmark for (2759ds/225729Mi) % 247.35/35.32 % (2537593)Cannot represent all propositional literals internally % 247.35/35.32 % (2537593)Refutation not found, incomplete strategy % 247.35/35.32 % (2537593)------------------------------ % 247.35/35.32 % (2537593)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 247.35/35.32 % (2537593)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 247.35/35.32 % (2537593)CaDiCaL version: 2.1.3 % 247.35/35.32 % (2537593)Termination reason: Refutation not found, incomplete strategy % 247.35/35.32 % (2537593)Time elapsed: 0.182 s % 247.35/35.32 % (2537593)Peak memory usage: 25 MB % 247.35/35.32 % (2537593)Instructions burned: 694 (million) % 247.35/35.32 % (2537593)------------------------------ % 247.35/35.32 % (2537593)------------------------------ % 247.35/35.32 % (2537595)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=650893710:fmbsr=2:i=185024:ins=7_2757 on theBenchmark for (2757ds/185024Mi) % 247.35/35.32 % (2537595)Cannot represent all propositional literals internally % 247.35/35.32 % (2537595)Refutation not found, incomplete strategy % 247.35/35.32 % (2537595)------------------------------ % 247.35/35.32 % (2537595)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 247.35/35.32 % (2537595)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 247.35/35.32 % (2537595)CaDiCaL version: 2.1.3 % 247.35/35.32 % (2537595)Termination reason: Refutation not found, incomplete strategy % 247.35/35.32 % (2537595)Time elapsed: 0.183 s % 247.35/35.32 % (2537595)Peak memory usage: 25 MB % 247.35/35.32 % (2537595)Instructions burned: 694 (million) % 247.35/35.32 % (2537595)------------------------------ % 247.35/35.32 % (2537595)------------------------------ % 247.35/35.32 % (2537597)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=221725010:rtra=on_2755 on theBenchmark for (2755ds/0Mi) % 247.35/35.32 % TRYING [1] % 247.35/35.32 % TRYING [2] % 247.35/35.32 % (2537575)Instruction limit reached! % 247.35/35.32 % (2537575)------------------------------ % 247.35/35.32 % (2537575)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 247.35/35.32 % (2537575)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 247.35/35.32 % (2537575)CaDiCaL version: 2.1.3 % 247.35/35.32 % (2537575)Termination reason: Instruction limit % 247.35/35.32 % (2537575)Termination phase: Saturation % 247.35/35.32 % (2537575)Time elapsed: 9.286 s % 247.35/35.32 % (2537575)Peak memory usage: 132 MB % 247.35/35.32 % (2537575)Instructions burned: 14135 (million) % 247.35/35.32 % (2537599)% WARNING: option uhcvi not known. % 247.35/35.32 % (2537599)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1463694572:i=271062:add=off:rtra=on:rawr=on_2735 on theBenchmark for (2735ds/271062Mi) % 247.35/35.32 % (2537579)Instruction limit reached! % 247.35/35.32 % (2537579)------------------------------ % 247.35/35.32 % (2537579)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 247.35/35.32 % (2537579)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 247.35/35.32 % (2537579)CaDiCaL version: 2.1.3 % 247.35/35.32 % (2537579)Termination reason: Instruction limit % 247.35/35.32 % (2537579)Termination phase: Saturation % 247.35/35.32 % (2537579)Time elapsed: 9.076 s % 247.35/35.32 % (2537579)Peak memory usage: 121 MB % 247.35/35.32 % (2537579)Instructions burned: 17629 (million) % 290.28/41.44 % (2537601)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1996512441:i=176048:add=on:rtra=on:rawr=on_2709 on theBenchmark for (2709ds/176048Mi) % 290.28/41.44 % (2537597)Cannot represent all propositional literals internally % 290.28/41.44 % (2537597)Refutation not found, incomplete strategy % 290.28/41.44 % (2537597)------------------------------ % 290.28/41.44 % (2537597)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 290.28/41.44 % (2537597)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 290.28/41.44 % (2537597)CaDiCaL version: 2.1.3 % 290.28/41.44 % (2537597)Termination reason: Refutation not found, incomplete strategy % 290.28/41.44 % (2537597)Time elapsed: 7.416 s % 290.28/41.44 % (2537597)Peak memory usage: 937 MB % 290.28/41.44 % (2537597)Instructions burned: 15276 (million) % 290.28/41.44 % (2537597)------------------------------ % 290.28/41.44 % (2537597)------------------------------ % 290.28/41.44 % (2537603)dis+10_1_sil=32000:si=on:sp=arity:random_seed=2750485262:i=206:fgj=on:rtra=on_2680 on theBenchmark for (2680ds/206Mi) % 290.28/41.44 % (2537603)Instruction limit reached! % 290.28/41.44 % (2537603)------------------------------ % 290.28/41.44 % (2537603)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 290.28/41.44 % (2537603)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 290.28/41.44 % (2537603)CaDiCaL version: 2.1.3 % 290.28/41.44 % (2537603)Termination reason: Instruction limit % 290.28/41.44 % (2537603)Termination phase: Saturation % 290.28/41.44 % (2537603)Time elapsed: 0.073 s % 290.28/41.44 % (2537603)Peak memory usage: 17 MB % 290.28/41.44 % (2537603)Instructions burned: 208 (million) % 290.28/41.44 % (2537605)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=1797481615:i=232:rtra=on_2680 on theBenchmark for (2680ds/232Mi) % 290.28/41.44 % (2537605)Instruction limit reached! % 290.28/41.44 % (2537605)------------------------------ % 290.28/41.44 % (2537605)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 290.28/41.44 % (2537605)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 290.28/41.44 % (2537605)CaDiCaL version: 2.1.3 % 290.28/41.44 % (2537605)Termination reason: Instruction limit % 290.28/41.44 % (2537605)Termination phase: Saturation % 290.28/41.44 % (2537605)Time elapsed: 0.076 s % 290.28/41.44 % (2537605)Peak memory usage: 18 MB % 290.28/41.44 % (2537605)Instructions burned: 235 (million) % 290.28/41.44 % (2537607)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=1884379935:i=262:rtra=on_2679 on theBenchmark for (2679ds/262Mi) % 290.28/41.44 % (2537607)Instruction limit reached! % 290.28/41.44 % (2537607)------------------------------ % 290.28/41.44 % (2537607)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 290.28/41.44 % (2537607)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 290.28/41.44 % (2537607)CaDiCaL version: 2.1.3 % 290.28/41.44 % (2537607)Termination reason: Instruction limit % 290.28/41.44 % (2537607)Termination phase: Saturation % 290.28/41.44 % (2537607)Time elapsed: 0.090 s % 290.28/41.44 % (2537607)Peak memory usage: 19 MB % 290.28/41.44 % (2537607)Instructions burned: 264 (million) % 290.28/41.44 % (2537609)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=1831210123:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2678 on theBenchmark for (2678ds/318Mi) % 290.28/41.44 % (2537609)Instruction limit reached! % 290.28/41.44 % (2537609)------------------------------ % 290.28/41.44 % (2537609)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 290.28/41.44 % (2537609)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 290.28/41.44 % (2537609)CaDiCaL version: 2.1.3 % 290.28/41.44 % (2537609)Termination reason: Instruction limit % 290.28/41.44 % (2537609)Termination phase: Saturation % 290.28/41.44 % (2537609)Time elapsed: 0.116 s % 290.28/41.44 % (2537609)Peak memory usage: 19 MB % 290.28/41.44 % (2537609)Instructions burned: 318 (million) % 290.28/41.44 % (2537611)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=214830228:i=1428:nm=2:rtra=on_2676 on theBenchmark for (2676ds/1428Mi) % 290.28/41.44 % TRYING [1] % 290.28/41.44 % TRYING [2] % 290.28/41.44 % (2537611)Instruction limit reached! % 290.28/41.44 % (2537611)------------------------------ % 290.28/41.44 % (2537611)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 290.28/41.44 % (2537611)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 290.28/41.44 % (2537611)CaDiCaL version: 2.1.3 % 290.28/41.44 % (2537611)Termination reason: Instruction limit % 290.28/41.44 % (2537611)TerminTerminated % 300.60/42.84 % Vampire exiting % 300.60/42.85 Terminated %------------------------------------------------------------------------------