%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWW363+1 : TPTP v9.3.1. Released v5.2.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % Computer : n004.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:39:53 PM UTC 2026 % Result : Timeout 300.44s 42.94s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWW363+1 : TPTP v9.3.1. Released v5.2.0. % 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.08/0.20 % Computer : n004.cluster.edu % 0.08/0.20 % Model : x86_64 x86_64 % 0.08/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.08/0.20 % Memory : 8046.5625MB % 0.08/0.20 % OS : Linux 6.8.0-71-generic % 0.08/0.20 % CPULimit : 300 % 0.08/0.20 % WCLimit : 300 % 0.08/0.20 % DateTime : Mon Sep 28 13:42:07 UTC 2026 % 0.08/0.20 % CPUTime : % 0.08/0.20 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.08/0.24 Running first-order model finding % 0.08/0.24 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 % 22.35/3.79 % (362296)Will run a generic schedule for satisfiability detection. % 22.35/3.79 % (362304)dis+10_1_sil=32000:sp=arity:random_seed=2487859340:i=103:fgj=on_2996 on theBenchmark for (2996ds/103Mi) % 22.35/3.79 % (362302)% WARNING: option uhcvi not known. % 22.35/3.79 % (362301)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1341573996_2996 on theBenchmark for (2996ds/0Mi) % 22.35/3.79 % (362302)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=477328596:i=135531:add=off:rawr=on_2996 on theBenchmark for (2996ds/135531Mi) % 22.35/3.79 % (362303)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3681876600:i=88024:add=on:rawr=on_2996 on theBenchmark for (2996ds/88024Mi) % 22.35/3.79 % (362305)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1366071011:i=116_2996 on theBenchmark for (2996ds/116Mi) % 22.35/3.79 % (362306)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=918339091:i=131_2996 on theBenchmark for (2996ds/131Mi) % 22.35/3.79 % (362307)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3285705856:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2996 on theBenchmark for (2996ds/159Mi) % 22.35/3.79 % (362304)Instruction limit reached! % 22.35/3.79 % (362304)------------------------------ % 22.35/3.79 % (362304)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.35/3.79 % (362304)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.35/3.79 % (362304)CaDiCaL version: 2.1.3 % 22.35/3.79 % (362304)Termination reason: Instruction limit % 22.35/3.79 % (362304)Termination phase: Preprocessing 3 % 22.35/3.79 % (362304)Time elapsed: 0.039 s % 22.35/3.79 % (362304)Peak memory usage: 20 MB % 22.35/3.79 % (362304)Instructions burned: 104 (million) % 22.35/3.79 % (362315)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=787328952:i=714:nm=2_2995 on theBenchmark for (2995ds/714Mi) % 22.35/3.79 % (362305)Instruction limit reached! % 22.35/3.79 % (362305)------------------------------ % 22.35/3.79 % (362305)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.35/3.79 % (362305)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.35/3.79 % (362305)CaDiCaL version: 2.1.3 % 22.35/3.79 % (362305)Termination reason: Instruction limit % 22.35/3.79 % (362305)Termination phase: NewCNF % 22.35/3.79 % (362305)Time elapsed: 0.076 s % 22.35/3.79 % (362305)Peak memory usage: 21 MB % 22.35/3.79 % (362305)Instructions burned: 117 (million) % 22.35/3.79 % (362306)Instruction limit reached! % 22.35/3.79 % (362306)------------------------------ % 22.35/3.79 % (362306)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.35/3.79 % (362306)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.35/3.79 % (362306)CaDiCaL version: 2.1.3 % 22.35/3.79 % (362306)Termination reason: Instruction limit % 22.35/3.79 % (362306)Termination phase: Preprocessing 3 % 22.35/3.79 % (362306)Time elapsed: 0.079 s % 22.35/3.79 % (362306)Peak memory usage: 20 MB % 22.35/3.79 % (362306)Instructions burned: 131 (million) % 22.35/3.79 % (362307)Instruction limit reached! % 22.35/3.79 % (362307)------------------------------ % 22.35/3.79 % (362307)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.35/3.79 % (362307)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.35/3.79 % (362307)CaDiCaL version: 2.1.3 % 22.35/3.79 % (362307)Termination reason: Instruction limit % 22.35/3.79 % (362307)Termination phase: Clausification % 22.35/3.79 % (362307)Time elapsed: 0.097 s % 22.35/3.79 % (362307)Peak memory usage: 21 MB % 22.35/3.79 % (362307)Instructions burned: 159 (million) % 22.35/3.79 % (362317)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1597026037:i=131:bd=preordered:fsd=on_2995 on theBenchmark for (2995ds/131Mi) % 22.35/3.79 % (362318)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=2281871388:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2995 on theBenchmark for (2995ds/684Mi) % 22.35/3.79 % (362321)ott-21_1_sil=16000:fs=off:random_seed=944099805:i=180:av=off:fsr=off_2995 on theBenchmark for (2995ds/180Mi) % 22.35/3.79 % (362317)Instruction limit reached! % 22.35/3.79 % (362317)------------------------------ % 22.35/3.79 % (362317)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.35/3.79 % (362317)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.35/3.79 % (362317)CaDiCaL version: 2.1.3 % 22.35/3.79 % (362317)Termination reason: Instruction limit % 63.51/9.50 % (362317)Termination phase: Preprocessing 3 % 63.51/9.50 % (362317)Time elapsed: 0.078 s % 63.51/9.50 % (362317)Peak memory usage: 20 MB % 63.51/9.50 % (362317)Instructions burned: 132 (million) % 63.51/9.50 % (362323)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2226222761:i=477:bd=all_2994 on theBenchmark for (2994ds/477Mi) % 63.51/9.50 % (362321)Instruction limit reached! % 63.51/9.50 % (362321)------------------------------ % 63.51/9.50 % (362321)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 63.51/9.50 % (362321)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 63.51/9.50 % (362321)CaDiCaL version: 2.1.3 % 63.51/9.50 % (362321)Termination reason: Instruction limit % 63.51/9.50 % (362321)Termination phase: Property scanning % 63.51/9.50 % (362321)Time elapsed: 0.104 s % 63.51/9.50 % (362321)Peak memory usage: 21 MB % 63.51/9.50 % (362321)Instructions burned: 180 (million) % 63.51/9.50 % (362315)Instruction limit reached! % 63.51/9.50 % (362315)------------------------------ % 63.51/9.50 % (362315)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 63.51/9.50 % (362315)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 63.51/9.50 % (362315)CaDiCaL version: 2.1.3 % 63.51/9.50 % (362315)Termination reason: Instruction limit % 63.51/9.50 % (362315)Termination phase: Finite model building preprocessing % 63.51/9.50 % (362315)Time elapsed: 0.181 s % 63.51/9.50 % (362315)Peak memory usage: 25 MB % 63.51/9.50 % (362315)Instructions burned: 715 (million) % 63.51/9.50 % (362326)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2653490260:i=1179_2993 on theBenchmark for (2993ds/1179Mi) % 63.51/9.50 % (362325)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3939295022:fmbsr=1.3:i=865:ins=25_2993 on theBenchmark for (2993ds/865Mi) % 63.51/9.50 % (362318)Instruction limit reached! % 63.51/9.50 % (362318)------------------------------ % 63.51/9.50 % (362318)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 63.51/9.50 % (362318)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 63.51/9.50 % (362318)CaDiCaL version: 2.1.3 % 63.51/9.50 % (362318)Termination reason: Instruction limit % 63.51/9.50 % (362318)Termination phase: Saturation % 63.51/9.50 % (362318)Time elapsed: 0.318 s % 63.51/9.50 % (362318)Peak memory usage: 24 MB % 63.51/9.50 % (362318)Instructions burned: 685 (million) % 63.51/9.50 % (362323)Instruction limit reached! % 63.51/9.50 % (362323)------------------------------ % 63.51/9.50 % (362323)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 63.51/9.50 % (362323)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 63.51/9.50 % (362323)CaDiCaL version: 2.1.3 % 63.51/9.50 % (362323)Termination reason: Instruction limit % 63.51/9.50 % (362323)Termination phase: Property scanning % 63.51/9.50 % (362323)Time elapsed: 0.224 s % 63.51/9.50 % (362323)Peak memory usage: 22 MB % 63.51/9.50 % (362323)Instructions burned: 479 (million) % 63.51/9.50 % (362329)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2543655197:i=889:ins=1_2991 on theBenchmark for (2991ds/889Mi) % 63.51/9.50 % (362330)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=1625437560:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2991 on theBenchmark for (2991ds/692Mi) % 63.51/9.50 % (362326)Instruction limit reached! % 63.51/9.50 % (362326)------------------------------ % 63.51/9.50 % (362326)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 63.51/9.50 % (362326)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 63.51/9.50 % (362326)CaDiCaL version: 2.1.3 % 63.51/9.50 % (362326)Termination reason: Instruction limit % 63.51/9.50 % (362326)Termination phase: Saturation % 63.51/9.50 % (362326)Time elapsed: 0.341 s % 63.51/9.50 % (362326)Peak memory usage: 30 MB % 63.51/9.50 % (362326)Instructions burned: 1180 (million) % 63.51/9.50 % (362333)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1523732385:i=879:kws=inv_precedence:fsr=off_2990 on theBenchmark for (2990ds/879Mi) % 63.51/9.50 % (362325)Instruction limit reached! % 63.51/9.50 % (362325)------------------------------ % 63.51/9.50 % (362325)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 63.51/9.50 % (362325)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 63.51/9.50 % (362325)CaDiCaL version: 2.1.3 % 63.51/9.50 % (362325)Termination reason: Instruction limit % 63.51/9.50 % (362325)Termination phase: Finite model building preprocessing % 127.31/18.55 % (362325)Time elapsed: 0.402 s % 127.31/18.55 % (362325)Peak memory usage: 30 MB % 127.31/18.55 % (362325)Instructions burned: 866 (million) % 127.31/18.55 % (362335)fmb+10_1_sil=64000:random_seed=3607869676:i=22061:nm=2:gsp=on_2989 on theBenchmark for (2989ds/22061Mi) % 127.31/18.55 % (362330)Instruction limit reached! % 127.31/18.55 % (362330)------------------------------ % 127.31/18.55 % (362330)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 127.31/18.55 % (362330)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 127.31/18.55 % (362330)CaDiCaL version: 2.1.3 % 127.31/18.55 % (362330)Termination reason: Instruction limit % 127.31/18.55 % (362330)Termination phase: Saturation % 127.31/18.55 % (362330)Time elapsed: 0.340 s % 127.31/18.55 % (362330)Peak memory usage: 27 MB % 127.31/18.55 % (362330)Instructions burned: 692 (million) % 127.31/18.55 % (362337)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3777133530:i=9515:nm=5_2988 on theBenchmark for (2988ds/9515Mi) % 127.31/18.55 % (362333)Instruction limit reached! % 127.31/18.55 % (362333)------------------------------ % 127.31/18.55 % (362333)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 127.31/18.55 % (362333)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 127.31/18.55 % (362333)CaDiCaL version: 2.1.3 % 127.31/18.55 % (362333)Termination reason: Instruction limit % 127.31/18.55 % (362333)Termination phase: Saturation % 127.31/18.55 % (362333)Time elapsed: 0.227 s % 127.31/18.55 % (362333)Peak memory usage: 30 MB % 127.31/18.55 % (362333)Instructions burned: 884 (million) % 127.31/18.55 % (362339)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2891698243:fmbsr=1.7:i=920_2987 on theBenchmark for (2987ds/920Mi) % 127.31/18.55 % (362329)Instruction limit reached! % 127.31/18.55 % (362329)------------------------------ % 127.31/18.55 % (362329)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 127.31/18.55 % (362329)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 127.31/18.55 % (362329)CaDiCaL version: 2.1.3 % 127.31/18.55 % (362329)Termination reason: Instruction limit % 127.31/18.55 % (362329)Termination phase: Finite model building preprocessing % 127.31/18.55 % (362329)Time elapsed: 0.419 s % 127.31/18.55 % (362329)Peak memory usage: 31 MB % 127.31/18.55 % (362329)Instructions burned: 889 (million) % 127.31/18.55 % (362341)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1241574619:i=5131_2987 on theBenchmark for (2987ds/5131Mi) % 127.31/18.55 % (362339)Instruction limit reached! % 127.31/18.55 % (362339)------------------------------ % 127.31/18.55 % (362339)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 127.31/18.55 % (362339)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 127.31/18.55 % (362339)CaDiCaL version: 2.1.3 % 127.31/18.55 % (362339)Termination reason: Instruction limit % 127.31/18.55 % (362339)Termination phase: Finite model building preprocessing % 127.31/18.55 % (362339)Time elapsed: 0.235 s % 127.31/18.55 % (362339)Peak memory usage: 31 MB % 127.31/18.55 % (362339)Instructions burned: 923 (million) % 127.31/18.55 % (362343)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1667301852:i=1472:ins=7:fdi=8:gsp=on_2985 on theBenchmark for (2985ds/1472Mi) % 127.31/18.55 % (362343)Instruction limit reached! % 127.31/18.55 % (362343)------------------------------ % 127.31/18.55 % (362343)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 127.31/18.55 % (362343)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 127.31/18.55 % (362343)CaDiCaL version: 2.1.3 % 127.31/18.55 % (362343)Termination reason: Instruction limit % 127.31/18.55 % (362343)Termination phase: Saturation % 127.31/18.55 % (362343)Time elapsed: 0.337 s % 127.31/18.55 % (362343)Peak memory usage: 28 MB % 127.31/18.55 % (362343)Instructions burned: 1473 (million) % 127.31/18.55 % (362345)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=2362660104:i=6324_2981 on theBenchmark for (2981ds/6324Mi) % 127.31/18.55 % (362345)Instruction limit reached! % 127.31/18.55 % (362345)------------------------------ % 127.31/18.55 % (362345)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 127.31/18.55 % (362345)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 127.31/18.55 % (362345)CaDiCaL version: 2.1.3 % 127.31/18.55 % (362345)Termination reason: Instruction limit % 127.31/18.55 % (362345)Termination phase: Finite model building preprocessing % 127.31/18.55 % (362345)Time elapsed: 1.715 s % 127.31/18.55 % (362345)Peak memory usage: 67 MB % 127.31/18.55 % (362345)Instructions burned: 6327 (million) % 210.30/30.26 % (362347)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=147110239:fmbsr=2.30978:i=2174_2964 on theBenchmark for (2964ds/2174Mi) % 210.30/30.26 % (362347)Instruction limit reached! % 210.30/30.26 % (362347)------------------------------ % 210.30/30.26 % (362347)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 210.30/30.26 % (362347)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 210.30/30.26 % (362347)CaDiCaL version: 2.1.3 % 210.30/30.26 % (362347)Termination reason: Instruction limit % 210.30/30.26 % (362347)Termination phase: Finite model building preprocessing % 210.30/30.26 % (362347)Time elapsed: 0.539 s % 210.30/30.26 % (362347)Peak memory usage: 48 MB % 210.30/30.26 % (362347)Instructions burned: 2178 (million) % 210.30/30.26 % (362349)ott-2_1_sil=16000:newcnf=on:random_seed=2903314609:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2958 on theBenchmark for (2958ds/869Mi) % 210.30/30.26 % (362341)Instruction limit reached! % 210.30/30.26 % (362341)------------------------------ % 210.30/30.26 % (362341)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 210.30/30.26 % (362341)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 210.30/30.26 % (362341)CaDiCaL version: 2.1.3 % 210.30/30.26 % (362341)Termination reason: Instruction limit % 210.30/30.26 % (362341)Termination phase: Saturation % 210.30/30.26 % (362341)Time elapsed: 2.916 s % 210.30/30.26 % (362341)Peak memory usage: 59 MB % 210.30/30.26 % (362341)Instructions burned: 5133 (million) % 210.30/30.26 % (362351)ott+10_1_sil=32000:tgt=ground:random_seed=3248887872:i=5114:av=off_2958 on theBenchmark for (2958ds/5114Mi) % 210.30/30.26 % (362349)Instruction limit reached! % 210.30/30.26 % (362349)------------------------------ % 210.30/30.26 % (362349)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 210.30/30.26 % (362349)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 210.30/30.26 % (362349)CaDiCaL version: 2.1.3 % 210.30/30.26 % (362349)Termination reason: Instruction limit % 210.30/30.26 % (362349)Termination phase: Saturation % 210.30/30.26 % (362349)Time elapsed: 0.236 s % 210.30/30.26 % (362349)Peak memory usage: 28 MB % 210.30/30.26 % (362349)Instructions burned: 872 (million) % 210.30/30.26 % (362353)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=3051423698:i=54282_2956 on theBenchmark for (2956ds/54282Mi) % 210.30/30.26 % (362337)Instruction limit reached! % 210.30/30.26 % (362337)------------------------------ % 210.30/30.26 % (362337)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 210.30/30.26 % (362337)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 210.30/30.26 % (362337)CaDiCaL version: 2.1.3 % 210.30/30.26 % (362337)Termination reason: Instruction limit % 210.30/30.26 % (362337)Termination phase: Finite model building preprocessing % 210.30/30.26 % (362337)Time elapsed: 4.876 s % 210.30/30.26 % (362337)Peak memory usage: 95 MB % 210.30/30.26 % (362337)Instructions burned: 9516 (million) % 210.30/30.26 % (362355)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=2828089850:i=3512:aac=none_2939 on theBenchmark for (2939ds/3512Mi) % 210.30/30.26 % (362351)Instruction limit reached! % 210.30/30.26 % (362351)------------------------------ % 210.30/30.26 % (362351)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 210.30/30.26 % (362351)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 210.30/30.26 % (362351)CaDiCaL version: 2.1.3 % 210.30/30.26 % (362351)Termination reason: Instruction limit % 210.30/30.26 % (362351)Termination phase: Saturation % 210.30/30.26 % (362351)Time elapsed: 3.111 s % 210.30/30.26 % (362351)Peak memory usage: 65 MB % 210.30/30.26 % (362351)Instructions burned: 5114 (million) % 210.30/30.26 % (362357)dis+21_1_sil=32000:sas=cadical:random_seed=1043255087:i=3773:amm=off_2926 on theBenchmark for (2926ds/3773Mi) % 210.30/30.26 % (362355)Instruction limit reached! % 210.30/30.26 % (362355)------------------------------ % 210.30/30.26 % (362355)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 210.30/30.26 % (362355)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 210.30/30.26 % (362355)CaDiCaL version: 2.1.3 % 210.30/30.26 % (362355)Termination reason: Instruction limit % 210.30/30.26 % (362355)Termination phase: Saturation % 210.30/30.26 % (362355)Time elapsed: 1.953 s % 210.30/30.26 % (362355)Peak memory usage: 52 MB % 210.30/30.26 % (362355)Instructions burned: 3512 (million) % 210.30/30.26 % (362359)ott+11_1_sil=16000:gs=on:random_seed=1300006606:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2919 on theBenchmark for (2919ds/2251Mi) % 210.30/30.26 % (362359)Instruction limit reached! % 281.98/40.34 % (362359)------------------------------ % 281.98/40.34 % (362359)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 281.98/40.34 % (362359)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 281.98/40.34 % (362359)CaDiCaL version: 2.1.3 % 281.98/40.34 % (362359)Termination reason: Instruction limit % 281.98/40.34 % (362359)Termination phase: Saturation % 281.98/40.34 % (362359)Time elapsed: 1.171 s % 281.98/40.34 % (362359)Peak memory usage: 34 MB % 281.98/40.34 % (362359)Instructions burned: 2253 (million) % 281.98/40.34 % (362361)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=1811421750:fmbsr=1.6:i=67534_2907 on theBenchmark for (2907ds/67534Mi) % 281.98/40.34 % (362357)Instruction limit reached! % 281.98/40.34 % (362357)------------------------------ % 281.98/40.34 % (362357)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 281.98/40.34 % (362357)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 281.98/40.34 % (362357)CaDiCaL version: 2.1.3 % 281.98/40.34 % (362357)Termination reason: Instruction limit % 281.98/40.34 % (362357)Termination phase: Saturation % 281.98/40.34 % (362357)Time elapsed: 2.087 s % 281.98/40.34 % (362357)Peak memory usage: 56 MB % 281.98/40.34 % (362357)Instructions burned: 3774 (million) % 281.98/40.34 % (362363)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=428206294:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2905 on theBenchmark for (2905ds/4591Mi) % 281.98/40.34 % TRYING [1] % 281.98/40.34 % (362363)Instruction limit reached! % 281.98/40.34 % (362363)------------------------------ % 281.98/40.34 % (362363)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 281.98/40.34 % (362363)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 281.98/40.34 % (362363)CaDiCaL version: 2.1.3 % 281.98/40.34 % (362363)Termination reason: Instruction limit % 281.98/40.34 % (362363)Termination phase: Saturation % 281.98/40.34 % (362363)Time elapsed: 1.710 s % 281.98/40.34 % (362363)Peak memory usage: 31 MB % 281.98/40.34 % (362363)Instructions burned: 4592 (million) % 281.98/40.34 % (362365)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=1609833568:i=29340_2888 on theBenchmark for (2888ds/29340Mi) % 281.98/40.34 % TRYING [2] % 281.98/40.34 % (362335)Instruction limit reached! % 281.98/40.34 % (362335)------------------------------ % 281.98/40.34 % (362335)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 281.98/40.34 % (362335)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 281.98/40.34 % (362335)CaDiCaL version: 2.1.3 % 281.98/40.34 % (362335)Termination reason: Instruction limit % 281.98/40.34 % (362335)Termination phase: Finite model building preprocessing % 281.98/40.34 % (362335)Time elapsed: 11.541 s % 281.98/40.34 % (362335)Peak memory usage: 216 MB % 281.98/40.34 % (362335)Instructions burned: 22062 (million) % 281.98/40.34 % (362367)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=3278067592:i=5211_2873 on theBenchmark for (2873ds/5211Mi) % 281.98/40.34 % TRYING [1] % 281.98/40.34 % TRYING [3] % 281.98/40.34 % TRYING [2] % 281.98/40.34 % (362367)Instruction limit reached! % 281.98/40.34 % (362367)------------------------------ % 281.98/40.34 % (362367)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 281.98/40.34 % (362367)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 281.98/40.34 % (362367)CaDiCaL version: 2.1.3 % 281.98/40.34 % (362367)Termination reason: Instruction limit % 281.98/40.34 % (362367)Termination phase: Saturation % 281.98/40.34 % (362367)Time elapsed: 2.088 s % 281.98/40.34 % (362367)Peak memory usage: 45 MB % 281.98/40.34 % (362367)Instructions burned: 5211 (million) % 281.98/40.34 % (362369)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=2874256853:i=5497:nm=2_2852 on theBenchmark for (2852ds/5497Mi) % 281.98/40.34 % TRYING [3] % 281.98/40.34 % (362369)Instruction limit reached! % 281.98/40.34 % (362369)------------------------------ % 281.98/40.34 % (362369)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 281.98/40.34 % (362369)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 281.98/40.34 % (362369)CaDiCaL version: 2.1.3 % 281.98/40.34 % (362369)Termination reason: Instruction limit % 281.98/40.34 % (362369)Termination phase: Finite model building preprocessing % 281.98/40.34 % (362369)Time elapsed: 2.811 s % 281.98/40.34 % (362369)Peak memory usage: 64 MB % 281.98/40.34 % (362369)Instructions burned: 5498 (million) % 281.98/40.34 % (362371)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=3780963852:fmbsr=2:i=46332_2824 on theBenchmark for (2824ds/46332Mi) % 281.98/40.34 % (362353)InsTerminated % 300.44/42.94 % Vampire exiting % 300.44/42.94 Terminated %------------------------------------------------------------------------------