%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWX189+1 : TPTP v9.3.1. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % Computer : n008.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 29 01:46:40 PM UTC 2026 % Result : Timeout 300.66s 42.64s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWX189+1 : TPTP v9.3.1. Released v9.3.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.09/0.21 % Computer : n008.cluster.edu % 0.09/0.21 % Model : x86_64 x86_64 % 0.09/0.21 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.21 % Memory : 8046.5625MB % 0.09/0.21 % OS : Linux 6.8.0-71-generic % 0.09/0.21 % CPULimit : 300 % 0.09/0.21 % WCLimit : 300 % 0.09/0.21 % DateTime : Mon Sep 28 15:07:24 UTC 2026 % 0.09/0.22 % CPUTime : % 0.09/0.22 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.09/0.27 Running first-order model finding % 0.09/0.27 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 % 26.79/4.12 % (2320392)Will run a generic schedule for satisfiability detection. % 26.79/4.12 % (2320401)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=649939845:i=116_2999 on theBenchmark for (2999ds/116Mi) % 26.79/4.12 % (2320398)% WARNING: option uhcvi not known. % 26.79/4.12 % (2320402)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3656820063:i=131_2999 on theBenchmark for (2999ds/131Mi) % 26.79/4.12 % (2320399)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2629843434:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 26.79/4.12 % (2320398)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2030480760:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 26.79/4.12 % (2320400)dis+10_1_sil=32000:sp=arity:random_seed=3355563027:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 26.79/4.12 % (2320397)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3365720640_2999 on theBenchmark for (2999ds/0Mi) % 26.79/4.12 % (2320403)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3351677131:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 26.79/4.12 % TRYING [1] % 26.79/4.12 % TRYING [2] % 26.79/4.12 % TRYING [3] % 26.79/4.12 % TRYING [4] % 26.79/4.12 % (2320401)Instruction limit reached! % 26.79/4.12 % (2320401)------------------------------ % 26.79/4.12 % (2320401)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 26.79/4.12 % (2320401)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.79/4.12 % (2320401)CaDiCaL version: 2.1.3 % 26.79/4.12 % (2320401)Termination reason: Instruction limit % 26.79/4.12 % (2320401)Termination phase: Saturation % 26.79/4.12 % (2320401)Time elapsed: 0.062 s % 26.79/4.12 % (2320401)Peak memory usage: 13 MB % 26.79/4.12 % (2320401)Instructions burned: 116 (million) % 26.79/4.12 % (2320411)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1364852960:i=714:nm=2_2998 on theBenchmark for (2998ds/714Mi) % 26.79/4.12 % TRYING [1] % 26.79/4.12 % TRYING [2] % 26.79/4.12 % TRYING [3] % 26.79/4.12 % TRYING [5] % 26.79/4.12 % TRYING [4] % 26.79/4.12 % (2320400)Instruction limit reached! % 26.79/4.12 % (2320400)------------------------------ % 26.79/4.12 % (2320400)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 26.79/4.12 % (2320400)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.79/4.12 % (2320400)CaDiCaL version: 2.1.3 % 26.79/4.12 % (2320400)Termination reason: Instruction limit % 26.79/4.12 % (2320400)Termination phase: Saturation % 26.79/4.12 % (2320400)Time elapsed: 0.106 s % 26.79/4.12 % (2320400)Peak memory usage: 12 MB % 26.79/4.12 % (2320400)Instructions burned: 103 (million) % 26.79/4.12 % (2320402)Instruction limit reached! % 26.79/4.12 % (2320402)------------------------------ % 26.79/4.12 % (2320402)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 26.79/4.12 % (2320402)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.79/4.12 % (2320402)CaDiCaL version: 2.1.3 % 26.79/4.12 % (2320402)Termination reason: Instruction limit % 26.79/4.12 % (2320402)Termination phase: Saturation % 26.79/4.12 % (2320402)Time elapsed: 0.127 s % 26.79/4.12 % (2320402)Peak memory usage: 13 MB % 26.79/4.12 % (2320402)Instructions burned: 132 (million) % 26.79/4.12 % TRYING [5] % 26.79/4.12 % (2320403)Instruction limit reached! % 26.79/4.12 % (2320403)------------------------------ % 26.79/4.12 % (2320403)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 26.79/4.12 % (2320403)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.79/4.12 % (2320403)CaDiCaL version: 2.1.3 % 26.79/4.12 % (2320403)Termination reason: Instruction limit % 26.79/4.12 % (2320403)Termination phase: Saturation % 26.79/4.12 % (2320403)Time elapsed: 0.152 s % 26.79/4.12 % (2320403)Peak memory usage: 13 MB % 26.79/4.12 % (2320403)Instructions burned: 160 (million) % 26.79/4.12 % (2320413)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=952621103:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi) % 26.79/4.12 % (2320414)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=4173428145:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi) % 26.79/4.12 % (2320415)ott-21_1_sil=16000:fs=off:random_seed=1864861163:i=180:av=off:fsr=off_2997 on theBenchmark for (2997ds/180Mi) % 26.79/4.12 % TRYING [6] % 26.79/4.12 % TRYING [6] % 26.79/4.12 % (2320413)Instruction limit reached! % 26.79/4.12 % (2320413)------------------------------ % 26.79/4.12 % (2320413)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 60.14/8.91 % (2320413)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 60.14/8.91 % (2320413)CaDiCaL version: 2.1.3 % 60.14/8.91 % (2320413)Termination reason: Instruction limit % 60.14/8.91 % (2320413)Termination phase: Saturation % 60.14/8.91 % (2320413)Time elapsed: 0.136 s % 60.14/8.91 % (2320413)Peak memory usage: 12 MB % 60.14/8.91 % (2320413)Instructions burned: 131 (million) % 60.14/8.91 % (2320419)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2057377596:i=477:bd=all_2996 on theBenchmark for (2996ds/477Mi) % 60.14/8.91 % TRYING [7] % 60.14/8.91 % (2320411)Instruction limit reached! % 60.14/8.91 % (2320411)------------------------------ % 60.14/8.91 % (2320411)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 60.14/8.91 % (2320411)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 60.14/8.91 % (2320411)CaDiCaL version: 2.1.3 % 60.14/8.91 % (2320411)Termination reason: Instruction limit % 60.14/8.91 % (2320411)Termination phase: Finite model building constraint generation % 60.14/8.91 % (2320411)Time elapsed: 0.288 s % 60.14/8.91 % (2320411)Peak memory usage: 34 MB % 60.14/8.91 % (2320411)Instructions burned: 717 (million) % 60.14/8.91 % (2320415)Instruction limit reached! % 60.14/8.91 % (2320415)------------------------------ % 60.14/8.91 % (2320415)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 60.14/8.91 % (2320415)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 60.14/8.91 % (2320415)CaDiCaL version: 2.1.3 % 60.14/8.91 % (2320415)Termination reason: Instruction limit % 60.14/8.91 % (2320415)Termination phase: Saturation % 60.14/8.91 % (2320415)Time elapsed: 0.177 s % 60.14/8.91 % (2320415)Peak memory usage: 12 MB % 60.14/8.91 % (2320415)Instructions burned: 180 (million) % 60.14/8.91 % (2320421)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1446633124:fmbsr=1.3:i=865:ins=25_2995 on theBenchmark for (2995ds/865Mi) % 60.14/8.91 % (2320422)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2325007275:i=1179_2995 on theBenchmark for (2995ds/1179Mi) % 60.14/8.91 % TRYING [1] % 60.14/8.91 % TRYING [2] % 60.14/8.91 % TRYING [3] % 60.14/8.91 % TRYING [4] % 60.14/8.91 % TRYING [7] % 60.14/8.91 % TRYING [5] % 60.14/8.91 % TRYING [6] % 60.14/8.91 % (2320421)Instruction limit reached! % 60.14/8.91 % (2320421)------------------------------ % 60.14/8.91 % (2320421)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 60.14/8.91 % (2320421)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 60.14/8.91 % (2320421)CaDiCaL version: 2.1.3 % 60.14/8.91 % (2320421)Termination reason: Instruction limit % 60.14/8.91 % (2320421)Termination phase: Finite model building constraint generation % 60.14/8.91 % (2320421)Time elapsed: 0.343 s % 60.14/8.91 % (2320421)Peak memory usage: 22 MB % 60.14/8.91 % (2320421)Instructions burned: 866 (million) % 60.14/8.91 % (2320414)Instruction limit reached! % 60.14/8.91 % (2320414)------------------------------ % 60.14/8.91 % (2320414)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 60.14/8.91 % (2320414)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 60.14/8.91 % (2320414)CaDiCaL version: 2.1.3 % 60.14/8.91 % (2320414)Termination reason: Instruction limit % 60.14/8.91 % (2320414)Termination phase: Saturation % 60.14/8.91 % (2320414)Time elapsed: 0.628 s % 60.14/8.91 % (2320414)Peak memory usage: 18 MB % 60.14/8.91 % (2320414)Instructions burned: 684 (million) % 60.14/8.91 % (2320425)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1624379657:i=889:ins=1_2991 on theBenchmark for (2991ds/889Mi) % 60.14/8.91 % (2320419)Instruction limit reached! % 60.14/8.91 % (2320419)------------------------------ % 60.14/8.91 % (2320419)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 60.14/8.91 % (2320419)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 60.14/8.91 % (2320419)CaDiCaL version: 2.1.3 % 60.14/8.91 % (2320419)Termination reason: Instruction limit % 60.14/8.91 % (2320419)Termination phase: Saturation % 60.14/8.91 % (2320419)Time elapsed: 0.467 s % 60.14/8.91 % (2320419)Peak memory usage: 14 MB % 60.14/8.91 % (2320419)Instructions burned: 477 (million) % 60.14/8.91 % (2320427)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=3480115819: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) % 60.14/8.91 % (2320428)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1382182660:i=879:kws=inv_precedence:fsr=off_2991 on theBenchmark for (2991ds/879Mi) % 89.55/13.01 % TRYING [14] % 89.55/13.01 % TRYING [8] % 89.55/13.01 % (2320425)Instruction limit reached! % 89.55/13.01 % (2320425)------------------------------ % 89.55/13.01 % (2320425)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 89.55/13.01 % (2320425)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 89.55/13.01 % (2320425)CaDiCaL version: 2.1.3 % 89.55/13.01 % (2320425)Termination reason: Instruction limit % 89.55/13.01 % (2320425)Termination phase: Finite model building constraint generation % 89.55/13.01 % (2320425)Time elapsed: 0.364 s % 89.55/13.01 % (2320425)Peak memory usage: 79 MB % 89.55/13.01 % (2320425)Instructions burned: 892 (million) % 89.55/13.01 % (2320431)fmb+10_1_sil=64000:random_seed=1461677037:i=22061:nm=2:gsp=on_2987 on theBenchmark for (2987ds/22061Mi) % 89.55/13.01 % TRYING [1] % 89.55/13.01 % TRYING [2] % 89.55/13.01 % TRYING [3] % 89.55/13.01 % TRYING [4] % 89.55/13.01 % TRYING [5] % 89.55/13.01 % TRYING [6] % 89.55/13.01 % (2320427)Instruction limit reached! % 89.55/13.01 % (2320427)------------------------------ % 89.55/13.01 % (2320427)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 89.55/13.01 % (2320427)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 89.55/13.01 % (2320427)CaDiCaL version: 2.1.3 % 89.55/13.01 % (2320427)Termination reason: Instruction limit % 89.55/13.01 % (2320427)Termination phase: Saturation % 89.55/13.01 % (2320427)Time elapsed: 0.678 s % 89.55/13.01 % (2320427)Peak memory usage: 20 MB % 89.55/13.01 % (2320427)Instructions burned: 692 (million) % 89.55/13.01 % (2320428)Instruction limit reached! % 89.55/13.01 % (2320428)------------------------------ % 89.55/13.01 % (2320428)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 89.55/13.01 % (2320428)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 89.55/13.01 % (2320428)CaDiCaL version: 2.1.3 % 89.55/13.01 % (2320428)Termination reason: Instruction limit % 89.55/13.01 % (2320428)Termination phase: Saturation % 89.55/13.01 % (2320428)Time elapsed: 0.675 s % 89.55/13.01 % (2320428)Peak memory usage: 14 MB % 89.55/13.01 % (2320428)Instructions burned: 880 (million) % 89.55/13.01 % (2320422)Instruction limit reached! % 89.55/13.01 % (2320422)------------------------------ % 89.55/13.01 % (2320422)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 89.55/13.01 % (2320422)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 89.55/13.01 % (2320422)CaDiCaL version: 2.1.3 % 89.55/13.01 % (2320422)Termination reason: Instruction limit % 89.55/13.01 % (2320422)Termination phase: Saturation % 89.55/13.01 % (2320422)Time elapsed: 1.125 s % 89.55/13.01 % (2320422)Peak memory usage: 21 MB % 89.55/13.01 % (2320422)Instructions burned: 1179 (million) % 89.55/13.01 % (2320433)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2489441475:i=9515:nm=5_2984 on theBenchmark for (2984ds/9515Mi) % 89.55/13.01 % TRYING [20] % 89.55/13.01 % (2320434)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3330130848:fmbsr=1.7:i=920_2984 on theBenchmark for (2984ds/920Mi) % 89.55/13.01 % (2320435)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=4213204368:i=5131_2984 on theBenchmark for (2984ds/5131Mi) % 89.55/13.01 % TRYING [8] % 89.55/13.01 % TRYING [7] % 89.55/13.01 % TRYING [9] % 89.55/13.01 % (2320434)Instruction limit reached! % 89.55/13.01 % (2320434)------------------------------ % 89.55/13.01 % (2320434)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 89.55/13.01 % (2320434)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 89.55/13.01 % (2320434)CaDiCaL version: 2.1.3 % 89.55/13.01 % (2320434)Termination reason: Instruction limit % 89.55/13.01 % (2320434)Termination phase: Finite model building constraint generation % 89.55/13.01 % (2320434)Time elapsed: 0.727 s % 89.55/13.01 % (2320434)Peak memory usage: 69 MB % 89.55/13.01 % (2320434)Instructions burned: 921 (million) % 89.55/13.01 % (2320439)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3332173158:i=1472:ins=7:fdi=8:gsp=on_2976 on theBenchmark for (2976ds/1472Mi) % 89.55/13.01 % TRYING [8] % 89.55/13.01 % TRYING [10] % 89.55/13.01 % TRYING [9] % 89.55/13.01 % (2320439)Instruction limit reached! % 89.55/13.01 % (2320439)------------------------------ % 89.55/13.01 % (2320439)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 89.55/13.01 % (2320439)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 89.55/13.01 % (2320439)CaDiCaL version: 2.1.3 % 89.55/13.01 % (2320439)Termination reason: Instruction limit % 89.55/13.01 % (2320439)Termination phase: Saturation % 89.55/13.01 % (2320439)Time elapsed: 1.412 s % 89.55/13.01 % (2320439)Peak memory usage: 29 MB % 89.55/13.01 % (2320439)Instructions burned: 1472 (million) % 300.66/42.64 % (2320441)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3265817905:i=6324_2961 on theBenchmark for (2961ds/6324Mi) % 300.66/42.64 % TRYING [77] % 300.66/42.64 % TRYING [11] % 300.66/42.64 % (2320435)Instruction limit reached! % 300.66/42.64 % (2320435)------------------------------ % 300.66/42.64 % (2320435)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.66/42.64 % (2320435)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.66/42.64 % (2320435)CaDiCaL version: 2.1.3 % 300.66/42.64 % (2320435)Termination reason: Instruction limit % 300.66/42.64 % (2320435)Termination phase: Saturation % 300.66/42.64 % (2320435)Time elapsed: 4.463 s % 300.66/42.64 % (2320435)Peak memory usage: 37 MB % 300.66/42.64 % (2320435)Instructions burned: 5132 (million) % 300.66/42.64 % (2320443)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=2846635172:fmbsr=2.30978:i=2174_2938 on theBenchmark for (2938ds/2174Mi) % 300.66/42.64 % TRYING [16] % 300.66/42.64 % TRYING [10] % 300.66/42.64 % (2320443)Instruction limit reached! % 300.66/42.64 % (2320443)------------------------------ % 300.66/42.64 % (2320443)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.66/42.64 % (2320443)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.66/42.64 % (2320443)CaDiCaL version: 2.1.3 % 300.66/42.64 % (2320443)Termination reason: Instruction limit % 300.66/42.64 % (2320443)Termination phase: Finite model building constraint generation % 300.66/42.64 % (2320443)Time elapsed: 1.484 s % 300.66/42.64 % (2320443)Peak memory usage: 134 MB % 300.66/42.64 % (2320443)Instructions burned: 2175 (million) % 300.66/42.64 % (2320445)ott-2_1_sil=16000:newcnf=on:random_seed=851495628:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2923 on theBenchmark for (2923ds/869Mi) % 300.66/42.64 % (2320433)Instruction limit reached! % 300.66/42.64 % (2320433)------------------------------ % 300.66/42.64 % (2320433)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.66/42.64 % (2320433)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.66/42.64 % (2320433)CaDiCaL version: 2.1.3 % 300.66/42.64 % (2320433)Termination reason: Instruction limit % 300.66/42.64 % (2320433)Termination phase: Finite model building constraint generation % 300.66/42.64 % (2320433)Time elapsed: 6.488 s % 300.66/42.64 % (2320433)Peak memory usage: 646 MB % 300.66/42.64 % (2320433)Instructions burned: 9517 (million) % 300.66/42.64 % (2320486)ott+10_1_sil=32000:tgt=ground:random_seed=2013326237:i=5114:av=off_2918 on theBenchmark for (2918ds/5114Mi) % 300.66/42.64 % (2320441)Instruction limit reached! % 300.66/42.64 % (2320441)------------------------------ % 300.66/42.64 % (2320441)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.66/42.64 % (2320441)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.66/42.64 % (2320441)CaDiCaL version: 2.1.3 % 300.66/42.64 % (2320441)Termination reason: Instruction limit % 300.66/42.64 % (2320441)Termination phase: Finite model building constraint generation % 300.66/42.64 % (2320441)Time elapsed: 4.344 s % 300.66/42.64 % (2320441)Peak memory usage: 516 MB % 300.66/42.64 % (2320441)Instructions burned: 6327 (million) % 300.66/42.64 % (2320519)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=1752582746:i=54282_2917 on theBenchmark for (2917ds/54282Mi) % 300.66/42.64 % TRYING [1] % 300.66/42.64 % TRYING [2] % 300.66/42.64 % (2320445)Instruction limit reached! % 300.66/42.64 % (2320445)------------------------------ % 300.66/42.64 % (2320445)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.66/42.64 % (2320445)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.66/42.64 % (2320445)CaDiCaL version: 2.1.3 % 300.66/42.64 % (2320445)Termination reason: Instruction limit % 300.66/42.64 % (2320445)Termination phase: Saturation % 300.66/42.64 % (2320445)Time elapsed: 0.602 s % 300.66/42.64 % (2320445)Peak memory usage: 17 MB % 300.66/42.64 % (2320445)Instructions burned: 870 (million) % 300.66/42.64 % TRYING [3] % 300.66/42.64 % TRYING [4] % 300.66/42.64 % (2320527)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=569051031:i=3512:aac=none_2916 on theBenchmark for (2916ds/3512Mi) % 300.66/42.64 % TRYING [5] % 300.66/42.64 % TRYING [6] % 300.66/42.64 % TRYING [7] % 300.66/42.64 % (2320431)Instruction limit reached! % 300.66/42.64 % (2320431)------------------------------ % 300.66/42.64 % (2320431)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.66/42.64 % (2320431)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.66/42.64 % (2320431)CaDiCaL version: 2.1.3 % 300.66/42.64 % (2320431)Termination reason: Instruction limit % 300.66/42.64 % (2320431)Termination phase: Finite model building SAT solving % 300.66/42.64 % (2320431)Time elapsed: 7.355 s % 300.66/42.64 % (2320431)Peak memory usage: 172 MB % 300.66/42.64 % (2320431)Instructions burned: 22062 (million) % 300.66/42.64 % (2320605)dis+21_1_sil=32000:sas=cadical:random_seed=3470134682:i=3773:amm=off_2913 on theBenchmark for (2913ds/3773Mi) % 300.66/42.64 % TRYING [8] % 300.66/42.64 % TRYING [12] % 300.66/42.64 % TRYING [9] % 300.66/42.64 % (2320605)Instruction limit reached! % 300.66/42.64 % (2320605)------------------------------ % 300.66/42.64 % (2320605)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.66/42.64 % (2320605)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.66/42.64 % (2320605)CaDiCaL version: 2.1.3 % 300.66/42.64 % (2320605)Termination reason: Instruction limit % 300.66/42.64 % (2320605)Termination phase: Saturation % 300.66/42.64 % (2320605)Time elapsed: 1.055 s % 300.66/42.64 % (2320605)Peak memory usage: 30 MB % 300.66/42.64 % (2320605)Instructions burned: 3776 (million) % 300.66/42.64 % (2320607)ott+11_1_sil=16000:gs=on:random_seed=2293502662:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2902 on theBenchmark for (2902ds/2251Mi) % 300.66/42.64 % TRYING [10] % 300.66/42.64 % (2320527)Instruction limit reached! % 300.66/42.64 % (2320527)------------------------------ % 300.66/42.64 % (2320527)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.66/42.64 % (2320527)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.66/42.64 % (2320527)CaDiCaL version: 2.1.3 % 300.66/42.64 % (2320527)Termination reason: Instruction limit % 300.66/42.64 % (2320527)Termination phase: Saturation % 300.66/42.64 % (2320527)Time elapsed: 1.786 s % 300.66/42.64 % (2320527)Peak memory usage: 28 MB % 300.66/42.64 % (2320527)Instructions burned: 3513 (million) % 300.66/42.64 % (2320609)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=1235225445:fmbsr=1.6:i=67534_2898 on theBenchmark for (2898ds/67534Mi) % 300.66/42.64 % TRYING [7] % 300.66/42.64 % (2320607)Instruction limit reached! % 300.66/42.64 % (2320607)------------------------------ % 300.66/42.64 % (2320607)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.66/42.64 % (2320607)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.66/42.64 % (2320607)CaDiCaL version: 2.1.3 % 300.66/42.64 % (2320607)Termination reason: Instruction limit % 300.66/42.64 % (2320607)Termination phase: Saturation % 300.66/42.64 % (2320607)Time elapsed: 0.559 s % 300.66/42.64 % (2320607)Peak memory usage: 16 MB % 300.66/42.64 % (2320607)Instructions burned: 2256 (million) % 300.66/42.64 % (2320611)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=2539052766:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2897 on theBenchmark for (2897ds/4591Mi) % 300.66/42.64 % TRYING [8] % 300.66/42.64 % (2320486)Instruction limit reached! % 300.66/42.64 % (2320486)------------------------------ % 300.66/42.64 % (2320486)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.66/42.64 % (2320486)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.66/42.64 % (2320486)CaDiCaL version: 2.1.3 % 300.66/42.64 % (2320486)Termination reason: Instruction limit % 300.66/42.64 % (2320486)Termination phase: Saturation % 300.66/42.64 % (2320486)Time elapsed: 2.903 s % 300.66/42.64 % (2320486)Peak memory usage: 45 MB % 300.66/42.64 % (2320486)Instructions burned: 5114 (million) % 300.66/42.64 % TRYING [11] % 300.66/42.64 % (2320613)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=1370426256:i=29340_2888 on theBenchmark for (2888ds/29340Mi) % 300.66/42.64 % (2320611)Instruction limit reached! % 300.66/42.64 % (2320611)------------------------------ % 300.66/42.64 % (2320611)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.66/42.64 % (2320611)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.66/42.64 % (2320611)CaDiCaL version: 2.1.3 % 300.66/42.64 % (2320611)Termination reason: Instruction limit % 300.66/42.64 % (2320611)Termination phase: Saturation % 300.66/42.64 % (2320611)Time elapsed: 1.019 s % 300.66/42.64 % (2320611)Peak memory usage: 34 MB % 300.66/42.64 % (2320611)Instructions burned: 4595 (million) % 300.66/42.64 % (2320615)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=4027288282:i=5211_2886 on theBenchmark for (2886ds/5211Mi) % 300.66/42.64 % TRYING [13] % 300.66/42.64 % TRYING [9] % 300.66/42.64 % (2320615)Instruction limit reached! % 300.66/42.64 % (2320615)------------------------------ % 300.66/42.64 % (2320615)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.66/42.64 % (2320615)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.66/42.64 % (2320615)CaDiCaL version: 2.1.3 % 300.66/42.64 % (2320615)Termination reason: Instruction limit % 300.66/42.64 Terminated % 300.66/42.64 % Vampire exiting % 300.66/42.64 Terminated %------------------------------------------------------------------------------