%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWW890+1 : TPTP v9.3.1. Released v7.3.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/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:45:08 PM UTC 2026 % Result : Timeout 291.29s 41.44s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : SWW890+1 : TPTP v9.3.1. Released v7.3.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.09/0.20 % Computer : n004.cluster.edu % 0.09/0.20 % Model : x86_64 x86_64 % 0.09/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.20 % Memory : 8046.5625MB % 0.09/0.20 % OS : Linux 6.8.0-71-generic % 0.09/0.20 % CPULimit : 300 % 0.09/0.20 % WCLimit : 300 % 0.09/0.20 % DateTime : Mon Sep 28 14:37:52 UTC 2026 % 0.09/0.21 % CPUTime : % 0.09/0.21 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.09/0.24 Running first-order model finding % 0.09/0.24 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 24.58/3.88 % (397944)Will run a generic schedule for satisfiability detection. % 24.58/3.88 % (397951)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=763040998:i=88024:add=on:rawr=on_2998 on theBenchmark for (2998ds/88024Mi) % 24.58/3.88 % (397950)% WARNING: option uhcvi not known. % 24.58/3.88 % (397949)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2666257497_2998 on theBenchmark for (2998ds/0Mi) % 24.58/3.88 % (397950)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2226629962:i=135531:add=off:rawr=on_2998 on theBenchmark for (2998ds/135531Mi) % 24.58/3.88 % (397952)dis+10_1_sil=32000:sp=arity:random_seed=3345698212:i=103:fgj=on_2998 on theBenchmark for (2998ds/103Mi) % 24.58/3.88 % (397953)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3044676250:i=116_2998 on theBenchmark for (2998ds/116Mi) % 24.58/3.88 % (397954)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=495026803:i=131_2998 on theBenchmark for (2998ds/131Mi) % 24.58/3.88 % (397955)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2196029528:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2998 on theBenchmark for (2998ds/159Mi) % 24.58/3.88 % (397952)Instruction limit reached! % 24.58/3.88 % (397952)------------------------------ % 24.58/3.88 % (397952)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 24.58/3.88 % (397952)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.58/3.88 % (397952)CaDiCaL version: 2.1.3 % 24.58/3.88 % (397952)Termination reason: Instruction limit % 24.58/3.88 % (397952)Termination phase: Property scanning % 24.58/3.88 % (397952)Time elapsed: 0.043 s % 24.58/3.88 % (397952)Peak memory usage: 12 MB % 24.58/3.88 % (397952)Instructions burned: 105 (million) % 24.58/3.88 % (397953)Instruction limit reached! % 24.58/3.88 % (397953)------------------------------ % 24.58/3.88 % (397953)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 24.58/3.88 % (397953)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.58/3.88 % (397953)CaDiCaL version: 2.1.3 % 24.58/3.88 % (397953)Termination reason: Instruction limit % 24.58/3.88 % (397953)Termination phase: Property scanning % 24.58/3.88 % (397953)Time elapsed: 0.052 s % 24.58/3.88 % (397953)Peak memory usage: 12 MB % 24.58/3.88 % (397953)Instructions burned: 116 (million) % 24.58/3.88 % (397954)Instruction limit reached! % 24.58/3.88 % (397954)------------------------------ % 24.58/3.88 % (397954)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 24.58/3.88 % (397954)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.58/3.88 % (397954)CaDiCaL version: 2.1.3 % 24.58/3.88 % (397954)Termination reason: Instruction limit % 24.58/3.88 % (397954)Termination phase: Property scanning % 24.58/3.88 % (397954)Time elapsed: 0.053 s % 24.58/3.88 % (397954)Peak memory usage: 12 MB % 24.58/3.88 % (397954)Instructions burned: 133 (million) % 24.58/3.88 % (397963)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2195051758:i=714:nm=2_2998 on theBenchmark for (2998ds/714Mi) % 24.58/3.88 % (397955)Instruction limit reached! % 24.58/3.88 % (397955)------------------------------ % 24.58/3.88 % (397955)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 24.58/3.88 % (397955)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.58/3.88 % (397955)CaDiCaL version: 2.1.3 % 24.58/3.88 % (397955)Termination reason: Instruction limit % 24.58/3.88 % (397955)Termination phase: Saturation % 24.58/3.88 % (397955)Time elapsed: 0.070 s % 24.58/3.88 % (397955)Peak memory usage: 14 MB % 24.58/3.88 % (397955)Instructions burned: 159 (million) % 24.58/3.88 % (397964)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=506997154:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi) % 24.58/3.88 % (397965)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=2949062450:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi) % 24.58/3.88 % (397967)ott-21_1_sil=16000:fs=off:random_seed=3546759629:i=180:av=off:fsr=off_2997 on theBenchmark for (2997ds/180Mi) % 24.58/3.88 % (397964)Instruction limit reached! % 24.58/3.88 % (397964)------------------------------ % 24.58/3.88 % (397964)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 24.58/3.88 % (397964)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.58/3.88 % (397964)CaDiCaL version: 2.1.3 % 24.58/3.88 % (397964)Termination reason: Instruction limit % 63.58/9.38 % (397964)Termination phase: Property scanning % 63.58/9.38 % (397964)Time elapsed: 0.052 s % 63.58/9.38 % (397964)Peak memory usage: 12 MB % 63.58/9.38 % (397964)Instructions burned: 133 (million) % 63.58/9.38 % (397971)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2110565534:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi) % 63.58/9.38 % (397967)Instruction limit reached! % 63.58/9.38 % (397967)------------------------------ % 63.58/9.38 % (397967)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 63.58/9.38 % (397967)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 63.58/9.38 % (397967)CaDiCaL version: 2.1.3 % 63.58/9.38 % (397967)Termination reason: Instruction limit % 63.58/9.38 % (397967)Termination phase: Saturation % 63.58/9.38 % (397967)Time elapsed: 0.072 s % 63.58/9.38 % (397967)Peak memory usage: 14 MB % 63.58/9.38 % (397967)Instructions burned: 182 (million) % 63.58/9.38 % (397973)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3562933520:fmbsr=1.3:i=865:ins=25_2996 on theBenchmark for (2996ds/865Mi) % 63.58/9.38 % (397965)Instruction limit reached! % 63.58/9.38 % (397965)------------------------------ % 63.58/9.38 % (397965)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 63.58/9.38 % (397965)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 63.58/9.38 % (397965)CaDiCaL version: 2.1.3 % 63.58/9.38 % (397965)Termination reason: Instruction limit % 63.58/9.38 % (397965)Termination phase: Saturation % 63.58/9.38 % (397965)Time elapsed: 0.245 s % 63.58/9.38 % (397965)Peak memory usage: 13 MB % 63.58/9.38 % (397965)Instructions burned: 686 (million) % 63.58/9.38 % (397963)Instruction limit reached! % 63.58/9.38 % (397963)------------------------------ % 63.58/9.38 % (397963)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 63.58/9.38 % (397963)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 63.58/9.38 % (397963)CaDiCaL version: 2.1.3 % 63.58/9.38 % (397963)Termination reason: Instruction limit % 63.58/9.38 % (397963)Termination phase: Finite model building preprocessing % 63.58/9.38 % (397963)Time elapsed: 0.267 s % 63.58/9.38 % (397963)Peak memory usage: 19 MB % 63.58/9.38 % (397963)Instructions burned: 714 (million) % 63.58/9.38 % (397975)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=4008973423:i=1179_2995 on theBenchmark for (2995ds/1179Mi) % 63.58/9.38 % (397976)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=254369168:i=889:ins=1_2995 on theBenchmark for (2995ds/889Mi) % 63.58/9.38 % (397971)Instruction limit reached! % 63.58/9.38 % (397971)------------------------------ % 63.58/9.38 % (397971)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 63.58/9.38 % (397971)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 63.58/9.38 % (397971)CaDiCaL version: 2.1.3 % 63.58/9.38 % (397971)Termination reason: Instruction limit % 63.58/9.38 % (397971)Termination phase: Saturation % 63.58/9.38 % (397971)Time elapsed: 0.251 s % 63.58/9.38 % (397971)Peak memory usage: 15 MB % 63.58/9.38 % (397971)Instructions burned: 478 (million) % 63.58/9.38 % (397979)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=2206247365: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) % 63.58/9.38 % (397973)Instruction limit reached! % 63.58/9.38 % (397973)------------------------------ % 63.58/9.38 % (397973)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 63.58/9.38 % (397973)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 63.58/9.38 % (397973)CaDiCaL version: 2.1.3 % 63.58/9.38 % (397973)Termination reason: Instruction limit % 63.58/9.38 % (397973)Termination phase: Finite model building preprocessing % 63.58/9.38 % (397973)Time elapsed: 0.297 s % 63.58/9.38 % (397973)Peak memory usage: 21 MB % 63.58/9.38 % (397973)Instructions burned: 866 (million) % 63.58/9.38 % (397981)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2691573716:i=879:kws=inv_precedence:fsr=off_2993 on theBenchmark for (2993ds/879Mi) % 63.58/9.38 % (397976)Instruction limit reached! % 63.58/9.38 % (397976)------------------------------ % 63.58/9.38 % (397976)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 63.58/9.38 % (397976)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 63.58/9.38 % (397976)CaDiCaL version: 2.1.3 % 63.58/9.38 % (397976)Termination reason: Instruction limit % 188.43/26.95 % (397976)Termination phase: Finite model building preprocessing % 188.43/26.95 % (397976)Time elapsed: 0.293 s % 188.43/26.95 % (397976)Peak memory usage: 21 MB % 188.43/26.95 % (397976)Instructions burned: 890 (million) % 188.43/26.95 % (397983)fmb+10_1_sil=64000:random_seed=2066293564:i=22061:nm=2:gsp=on_2992 on theBenchmark for (2992ds/22061Mi) % 188.43/26.95 % (397979)Instruction limit reached! % 188.43/26.95 % (397979)------------------------------ % 188.43/26.95 % (397979)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 188.43/26.95 % (397979)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 188.43/26.95 % (397979)CaDiCaL version: 2.1.3 % 188.43/26.95 % (397979)Termination reason: Instruction limit % 188.43/26.95 % (397979)Termination phase: Saturation % 188.43/26.95 % (397979)Time elapsed: 0.255 s % 188.43/26.95 % (397979)Peak memory usage: 15 MB % 188.43/26.95 % (397979)Instructions burned: 692 (million) % 188.43/26.95 % (397985)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3754292048:i=9515:nm=5_2991 on theBenchmark for (2991ds/9515Mi) % 188.43/26.95 % (397981)Instruction limit reached! % 188.43/26.95 % (397981)------------------------------ % 188.43/26.95 % (397981)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 188.43/26.95 % (397981)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 188.43/26.95 % (397981)CaDiCaL version: 2.1.3 % 188.43/26.95 % (397981)Termination reason: Instruction limit % 188.43/26.95 % (397981)Termination phase: Saturation % 188.43/26.95 % (397981)Time elapsed: 0.324 s % 188.43/26.95 % (397981)Peak memory usage: 13 MB % 188.43/26.95 % (397981)Instructions burned: 881 (million) % 188.43/26.95 % (397987)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3002321406:fmbsr=1.7:i=920_2990 on theBenchmark for (2990ds/920Mi) % 188.43/26.95 % (397975)Instruction limit reached! % 188.43/26.95 % (397975)------------------------------ % 188.43/26.95 % (397975)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 188.43/26.95 % (397975)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 188.43/26.95 % (397975)CaDiCaL version: 2.1.3 % 188.43/26.95 % (397975)Termination reason: Instruction limit % 188.43/26.95 % (397975)Termination phase: Saturation % 188.43/26.95 % (397975)Time elapsed: 0.568 s % 188.43/26.95 % (397975)Peak memory usage: 23 MB % 188.43/26.95 % (397975)Instructions burned: 1180 (million) % 188.43/26.95 % (397989)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=913030379:i=5131_2989 on theBenchmark for (2989ds/5131Mi) % 188.43/26.95 % (397987)Instruction limit reached! % 188.43/26.95 % (397987)------------------------------ % 188.43/26.95 % (397987)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 188.43/26.95 % (397987)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 188.43/26.95 % (397987)CaDiCaL version: 2.1.3 % 188.43/26.95 % (397987)Termination reason: Instruction limit % 188.43/26.95 % (397987)Termination phase: Finite model building preprocessing % 188.43/26.95 % (397987)Time elapsed: 0.324 s % 188.43/26.95 % (397987)Peak memory usage: 21 MB % 188.43/26.95 % (397987)Instructions burned: 922 (million) % 188.43/26.95 % (397991)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=4268294455:i=1472:ins=7:fdi=8:gsp=on_2986 on theBenchmark for (2986ds/1472Mi) % 188.43/26.95 % (397991)Instruction limit reached! % 188.43/26.95 % (397991)------------------------------ % 188.43/26.95 % (397991)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 188.43/26.95 % (397991)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 188.43/26.95 % (397991)CaDiCaL version: 2.1.3 % 188.43/26.95 % (397991)Termination reason: Instruction limit % 188.43/26.95 % (397991)Termination phase: Saturation % 188.43/26.95 % (397991)Time elapsed: 0.654 s % 188.43/26.95 % (397991)Peak memory usage: 26 MB % 188.43/26.95 % (397991)Instructions burned: 1474 (million) % 188.43/26.95 % (397993)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=1209758123:i=6324_2980 on theBenchmark for (2980ds/6324Mi) % 188.43/26.95 % (397989)Instruction limit reached! % 188.43/26.95 % (397989)------------------------------ % 188.43/26.95 % (397989)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 188.43/26.95 % (397989)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 188.43/26.95 % (397989)CaDiCaL version: 2.1.3 % 188.43/26.95 % (397989)Termination reason: Instruction limit % 188.43/26.95 % (397989)Termination phase: Saturation % 188.43/26.95 % (397989)Time elapsed: 2.545 s % 188.43/26.95 % (397989)Peak memory usage: 43 MB % 188.43/26.95 % (397989)Instructions burned: 5132 (million) % 188.43/26.95 % (397995)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=3247667147:fmbsr=2.30978:i=2174_2963 on theBenchmark for (2963ds/2174Mi) % 291.29/41.44 % (397995)Instruction limit reached! % 291.29/41.44 % (397995)------------------------------ % 291.29/41.44 % (397995)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 291.29/41.44 % (397995)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 291.29/41.44 % (397995)CaDiCaL version: 2.1.3 % 291.29/41.44 % (397995)Termination reason: Instruction limit % 291.29/41.44 % (397995)Termination phase: Finite model building preprocessing % 291.29/41.44 % (397995)Time elapsed: 0.986 s % 291.29/41.44 % (397995)Peak memory usage: 27 MB % 291.29/41.44 % (397995)Instructions burned: 2176 (million) % 291.29/41.44 % (397997)ott-2_1_sil=16000:newcnf=on:random_seed=4026992239:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2953 on theBenchmark for (2953ds/869Mi) % 291.29/41.44 % (397997)Instruction limit reached! % 291.29/41.44 % (397997)------------------------------ % 291.29/41.44 % (397997)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 291.29/41.44 % (397997)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 291.29/41.44 % (397997)CaDiCaL version: 2.1.3 % 291.29/41.44 % (397997)Termination reason: Instruction limit % 291.29/41.44 % (397997)Termination phase: Saturation % 291.29/41.44 % (397997)Time elapsed: 0.328 s % 291.29/41.44 % (397997)Peak memory usage: 17 MB % 291.29/41.44 % (397997)Instructions burned: 870 (million) % 291.29/41.44 % (397999)ott+10_1_sil=32000:tgt=ground:random_seed=465588273:i=5114:av=off_2950 on theBenchmark for (2950ds/5114Mi) % 291.29/41.44 % (397993)Instruction limit reached! % 291.29/41.44 % (397993)------------------------------ % 291.29/41.44 % (397993)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 291.29/41.44 % (397993)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 291.29/41.44 % (397993)CaDiCaL version: 2.1.3 % 291.29/41.44 % (397993)Termination reason: Instruction limit % 291.29/41.44 % (397993)Termination phase: Finite model building preprocessing % 291.29/41.44 % (397993)Time elapsed: 3.349 s % 291.29/41.44 % (397993)Peak memory usage: 34 MB % 291.29/41.44 % (397993)Instructions burned: 6325 (million) % 291.29/41.44 % (398001)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2282397576:i=54282_2946 on theBenchmark for (2946ds/54282Mi) % 291.29/41.44 % (397985)Instruction limit reached! % 291.29/41.44 % (397985)------------------------------ % 291.29/41.44 % (397985)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 291.29/41.44 % (397985)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 291.29/41.44 % (397985)CaDiCaL version: 2.1.3 % 291.29/41.44 % (397985)Termination reason: Instruction limit % 291.29/41.44 % (397985)Termination phase: Finite model building preprocessing % 291.29/41.44 % (397985)Time elapsed: 5.180 s % 291.29/41.44 % (397985)Peak memory usage: 35 MB % 291.29/41.44 % (397985)Instructions burned: 9516 (million) % 291.29/41.44 % (398003)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=2464908344:i=3512:aac=none_2939 on theBenchmark for (2939ds/3512Mi) % 291.29/41.44 % (397999)Instruction limit reached! % 291.29/41.44 % (397999)------------------------------ % 291.29/41.44 % (397999)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 291.29/41.44 % (397999)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 291.29/41.44 % (397999)CaDiCaL version: 2.1.3 % 291.29/41.44 % (397999)Termination reason: Instruction limit % 291.29/41.44 % (397999)Termination phase: Saturation % 291.29/41.44 % (397999)Time elapsed: 2.678 s % 291.29/41.44 % (397999)Peak memory usage: 56 MB % 291.29/41.44 % (397999)Instructions burned: 5116 (million) % 291.29/41.44 % (398005)dis+21_1_sil=32000:sas=cadical:random_seed=1664969153:i=3773:amm=off_2923 on theBenchmark for (2923ds/3773Mi) % 291.29/41.44 % (398003)Instruction limit reached! % 291.29/41.44 % (398003)------------------------------ % 291.29/41.44 % (398003)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 291.29/41.44 % (398003)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 291.29/41.44 % (398003)CaDiCaL version: 2.1.3 % 291.29/41.44 % (398003)Termination reason: Instruction limit % 291.29/41.44 % (398003)Termination phase: Saturation % 291.29/41.44 % (398003)Time elapsed: 1.855 s % 291.29/41.44 % (398003)Peak memory usage: 43 MB % 291.29/41.44 % (398003)Instructions burned: 3514 (million) % 291.29/41.44 % (398007)ott+11_1_sil=16000:gs=on:random_seed=1410718820:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2921 on theBenchmark for (2921ds/2251Mi) % 291.29/41.44 % (398007)Instruction limit reached! % 300.51/42.73 % (398007)------------------------------ % 300.51/42.73 % (398007)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.51/42.73 % (398007)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.51/42.73 % (398007)CaDiCaL version: 2.1.3 % 300.51/42.73 % (398007)Termination reason: Instruction limit % 300.51/42.73 % (398007)Termination phase: Saturation % 300.51/42.73 % (398007)Time elapsed: 1.218 s % 300.51/42.73 % (398007)Peak memory usage: 31 MB % 300.51/42.73 % (398007)Instructions burned: 2251 (million) % 300.51/42.73 % (398009)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=996721887:fmbsr=1.6:i=67534_2908 on theBenchmark for (2908ds/67534Mi) % 300.51/42.73 % (398005)Instruction limit reached! % 300.51/42.73 % (398005)------------------------------ % 300.51/42.73 % (398005)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.51/42.73 % (398005)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.51/42.73 % (398005)CaDiCaL version: 2.1.3 % 300.51/42.73 % (398005)Termination reason: Instruction limit % 300.51/42.73 % (398005)Termination phase: Saturation % 300.51/42.73 % (398005)Time elapsed: 1.984 s % 300.51/42.73 % (398005)Peak memory usage: 45 MB % 300.51/42.73 % (398005)Instructions burned: 3773 (million) % 300.51/42.73 % (398011)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=1758858941:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2903 on theBenchmark for (2903ds/4591Mi) % 300.51/42.73 % (398011)Instruction limit reached! % 300.51/42.73 % (398011)------------------------------ % 300.51/42.73 % (398011)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.51/42.73 % (398011)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.51/42.73 % (398011)CaDiCaL version: 2.1.3 % 300.51/42.73 % (398011)Termination reason: Instruction limit % 300.51/42.73 % (398011)Termination phase: Saturation % 300.51/42.73 % (398011)Time elapsed: 2.350 s % 300.51/42.73 % (398011)Peak memory usage: 77 MB % 300.51/42.73 % (398011)Instructions burned: 4592 (million) % 300.51/42.73 % (398013)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=197599827:i=29340_2879 on theBenchmark for (2879ds/29340Mi) % 300.51/42.73 % (397983)Instruction limit reached! % 300.51/42.73 % (397983)------------------------------ % 300.51/42.73 % (397983)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.51/42.73 % (397983)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.51/42.73 % (397983)CaDiCaL version: 2.1.3 % 300.51/42.73 % (397983)Termination reason: Instruction limit % 300.51/42.73 % (397983)Termination phase: Finite model building preprocessing % 300.51/42.73 % (397983)Time elapsed: 12.093 s % 300.51/42.73 % (397983)Peak memory usage: 81 MB % 300.51/42.73 % (397983)Instructions burned: 22061 (million) % 300.51/42.73 % (398015)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=4189564475:i=5211_2870 on theBenchmark for (2870ds/5211Mi) % 300.51/42.73 % (398015)Instruction limit reached! % 300.51/42.73 % (398015)------------------------------ % 300.51/42.73 % (398015)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.51/42.73 % (398015)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.51/42.73 % (398015)CaDiCaL version: 2.1.3 % 300.51/42.73 % (398015)Termination reason: Instruction limit % 300.51/42.73 % (398015)Termination phase: Saturation % 300.51/42.73 % (398015)Time elapsed: 2.536 s % 300.51/42.73 % (398015)Peak memory usage: 43 MB % 300.51/42.73 % (398015)Instructions burned: 5213 (million) % 300.51/42.73 % (398017)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=2618760119:i=5497:nm=2_2845 on theBenchmark for (2845ds/5497Mi) % 300.51/42.73 % (398017)Instruction limit reached! % 300.51/42.73 % (398017)------------------------------ % 300.51/42.73 % (398017)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.51/42.73 % (398017)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.51/42.73 % (398017)CaDiCaL version: 2.1.3 % 300.51/42.73 % (398017)Termination reason: Instruction limit % 300.51/42.73 % (398017)Termination phase: Finite model building preprocessing % 300.51/42.73 % (398017)Time elapsed: 2.980 s % 300.51/42.73 % (398017)Peak memory usage: 31 MB % 300.51/42.73 % (398017)Instructions burned: 5498 (million) % 300.51/42.73 % (398019)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=4274663503:fmbsr=2:i=46332_2815 on theBenchmark for (2815ds/46332Mi) % 300.51/42.73 % (398013)Instruction limit reached! % 300.51/42.73 % (398013)------------------------------ % 300.51/42.73 % (398013)Versio % 300.51/42.74 Terminated % 300.51/42.74 % Vampire exiting %------------------------------------------------------------------------------