%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWV761-1 : TPTP v9.3.1. Released v4.1.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % Computer : n010.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 29 01:26:22 PM UTC 2026 % Result : Timeout 300.33s 42.64s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWV761-1 : TPTP v9.3.1. Released v4.1.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.09/0.19 % Computer : n010.cluster.edu % 0.09/0.19 % Model : x86_64 x86_64 % 0.09/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.19 % Memory : 8046.5625MB % 0.09/0.19 % OS : Linux 6.8.0-71-generic % 0.09/0.19 % CPULimit : 300 % 0.09/0.19 % WCLimit : 300 % 0.09/0.19 % DateTime : Mon Sep 28 12:29:32 UTC 2026 % 0.09/0.19 % CPUTime : % 0.09/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.09/0.22 Running first-order model finding % 0.09/0.22 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 18.63/2.93 % (1893363)Will run a generic schedule for satisfiability detection. % 18.63/2.93 % (1893370)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2447187096:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 18.63/2.93 % (1893369)% WARNING: option uhcvi not known. % 18.63/2.93 % (1893369)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=842140662:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 18.63/2.93 % (1893368)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1951726721_2999 on theBenchmark for (2999ds/0Mi) % 18.63/2.93 % (1893371)dis+10_1_sil=32000:sp=arity:random_seed=2781584682:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 18.63/2.93 % (1893372)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=950203481:i=116_2999 on theBenchmark for (2999ds/116Mi) % 18.63/2.93 % (1893373)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2215553777:i=131_2999 on theBenchmark for (2999ds/131Mi) % 18.63/2.93 % (1893374)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=4251316617:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 18.63/2.93 % (1893371)Instruction limit reached! % 18.63/2.93 % (1893371)------------------------------ % 18.63/2.93 % (1893371)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 18.63/2.93 % (1893371)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.63/2.93 % (1893371)CaDiCaL version: 2.1.3 % 18.63/2.93 % (1893371)Termination reason: Instruction limit % 18.63/2.93 % (1893371)Termination phase: Saturation % 18.63/2.93 % (1893371)Time elapsed: 0.064 s % 18.63/2.93 % (1893371)Peak memory usage: 13 MB % 18.63/2.93 % (1893371)Instructions burned: 105 (million) % 18.63/2.93 % (1893372)Instruction limit reached! % 18.63/2.93 % (1893372)------------------------------ % 18.63/2.93 % (1893372)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 18.63/2.93 % (1893372)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.63/2.93 % (1893372)CaDiCaL version: 2.1.3 % 18.63/2.93 % (1893372)Termination reason: Instruction limit % 18.63/2.93 % (1893372)Termination phase: Saturation % 18.63/2.93 % (1893372)Time elapsed: 0.072 s % 18.63/2.93 % (1893372)Peak memory usage: 13 MB % 18.63/2.93 % (1893372)Instructions burned: 116 (million) % 18.63/2.93 % (1893373)Instruction limit reached! % 18.63/2.93 % (1893373)------------------------------ % 18.63/2.93 % (1893373)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 18.63/2.93 % (1893373)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.63/2.93 % (1893373)CaDiCaL version: 2.1.3 % 18.63/2.93 % (1893373)Termination reason: Instruction limit % 18.63/2.93 % (1893373)Termination phase: Saturation % 18.63/2.93 % (1893373)Time elapsed: 0.081 s % 18.63/2.93 % (1893373)Peak memory usage: 13 MB % 18.63/2.93 % (1893373)Instructions burned: 131 (million) % 18.63/2.93 % (1893382)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=18134724:i=714:nm=2_2998 on theBenchmark for (2998ds/714Mi) % 18.63/2.93 % (1893383)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2780464928:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi) % 18.63/2.93 % (1893384)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=2542384447:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi) % 18.63/2.93 % (1893374)Instruction limit reached! % 18.63/2.93 % (1893374)------------------------------ % 18.63/2.93 % (1893374)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 18.63/2.93 % (1893374)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.63/2.93 % (1893374)CaDiCaL version: 2.1.3 % 18.63/2.93 % (1893374)Termination reason: Instruction limit % 18.63/2.93 % (1893374)Termination phase: Saturation % 18.63/2.93 % (1893374)Time elapsed: 0.102 s % 18.63/2.93 % (1893374)Peak memory usage: 14 MB % 18.63/2.93 % (1893374)Instructions burned: 159 (million) % 18.63/2.93 % (1893388)ott-21_1_sil=16000:fs=off:random_seed=1418468711:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 18.63/2.93 % (1893383)Instruction limit reached! % 18.63/2.93 % (1893383)------------------------------ % 18.63/2.93 % (1893383)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 18.63/2.93 % (1893383)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.63/2.93 % (1893383)CaDiCaL version: 2.1.3 % 47.18/7.02 % (1893383)Termination reason: Instruction limit % 47.18/7.02 % (1893383)Termination phase: Saturation % 47.18/7.02 % (1893383)Time elapsed: 0.081 s % 47.18/7.02 % (1893383)Peak memory usage: 14 MB % 47.18/7.02 % (1893383)Instructions burned: 131 (million) % 47.18/7.02 % TRYING [1] % 47.18/7.02 % (1893388)Instruction limit reached! % 47.18/7.02 % (1893388)------------------------------ % 47.18/7.02 % (1893388)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 47.18/7.02 % (1893388)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 47.18/7.02 % (1893388)CaDiCaL version: 2.1.3 % 47.18/7.02 % (1893388)Termination reason: Instruction limit % 47.18/7.02 % (1893388)Termination phase: Saturation % 47.18/7.02 % (1893388)Time elapsed: 0.069 s % 47.18/7.02 % (1893388)Peak memory usage: 12 MB % 47.18/7.02 % (1893388)Instructions burned: 182 (million) % 47.18/7.02 % (1893390)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3228291145:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi) % 47.18/7.02 % TRYING [2] % 47.18/7.02 % (1893391)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1238383172:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi) % 47.18/7.02 % TRYING [1] % 47.18/7.02 % TRYING [3] % 47.18/7.02 % TRYING [2] % 47.18/7.02 % TRYING [3] % 47.18/7.02 % (1893382)Instruction limit reached! % 47.18/7.02 % (1893382)------------------------------ % 47.18/7.02 % (1893382)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 47.18/7.02 % (1893382)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 47.18/7.02 % (1893382)CaDiCaL version: 2.1.3 % 47.18/7.02 % (1893382)Termination reason: Instruction limit % 47.18/7.02 % (1893382)Termination phase: Finite model building constraint generation % 47.18/7.02 % (1893382)Time elapsed: 0.312 s % 47.18/7.02 % (1893382)Peak memory usage: 30 MB % 47.18/7.02 % (1893382)Instructions burned: 714 (million) % 47.18/7.02 % TRYING [1] % 47.18/7.02 % (1893394)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3713307443:i=1179_2995 on theBenchmark for (2995ds/1179Mi) % 47.18/7.02 % TRYING [2] % 47.18/7.02 % (1893390)Instruction limit reached! % 47.18/7.02 % (1893390)------------------------------ % 47.18/7.02 % (1893390)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 47.18/7.02 % (1893390)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 47.18/7.02 % (1893390)CaDiCaL version: 2.1.3 % 47.18/7.02 % (1893390)Termination reason: Instruction limit % 47.18/7.02 % (1893390)Termination phase: Saturation % 47.18/7.02 % (1893390)Time elapsed: 0.294 s % 47.18/7.02 % (1893390)Peak memory usage: 15 MB % 47.18/7.02 % (1893390)Instructions burned: 478 (million) % 47.18/7.02 % (1893384)Instruction limit reached! % 47.18/7.02 % (1893384)------------------------------ % 47.18/7.02 % (1893384)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 47.18/7.02 % (1893384)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 47.18/7.02 % (1893384)CaDiCaL version: 2.1.3 % 47.18/7.02 % (1893384)Termination reason: Instruction limit % 47.18/7.02 % (1893384)Termination phase: Saturation % 47.18/7.02 % (1893384)Time elapsed: 0.393 s % 47.18/7.02 % (1893384)Peak memory usage: 17 MB % 47.18/7.02 % (1893384)Instructions burned: 685 (million) % 47.18/7.02 % (1893396)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1850408367:i=889:ins=1_2994 on theBenchmark for (2994ds/889Mi) % 47.18/7.02 % (1893397)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=896026950: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) % 47.18/7.02 % (1893391)Instruction limit reached! % 47.18/7.02 % (1893391)------------------------------ % 47.18/7.02 % (1893391)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 47.18/7.02 % (1893391)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 47.18/7.02 % (1893391)CaDiCaL version: 2.1.3 % 47.18/7.02 % (1893391)Termination reason: Instruction limit % 47.18/7.02 % (1893391)Termination phase: Finite model building SAT solving % 47.18/7.02 % (1893391)Time elapsed: 0.416 s % 47.18/7.02 % (1893391)Peak memory usage: 31 MB % 47.18/7.02 % (1893391)Instructions burned: 866 (million) % 47.18/7.02 % (1893400)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2527866420:i=879:kws=inv_precedence:fsr=off_2993 on theBenchmark for (2993ds/879Mi) % 47.18/7.02 % TRYING [4] % 47.18/7.02 % (1893397)Instruction limit reached! % 47.18/7.02 % (1893397)------------------------------ % 47.18/7.02 % (1893397)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 102.48/14.80 % (1893397)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 102.48/14.80 % (1893397)CaDiCaL version: 2.1.3 % 102.48/14.80 % (1893397)Termination reason: Instruction limit % 102.48/14.80 % (1893397)Termination phase: Saturation % 102.48/14.80 % (1893397)Time elapsed: 0.425 s % 102.48/14.80 % (1893397)Peak memory usage: 19 MB % 102.48/14.80 % (1893397)Instructions burned: 693 (million) % 102.48/14.80 % (1893396)Instruction limit reached! % 102.48/14.80 % (1893396)------------------------------ % 102.48/14.80 % (1893396)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 102.48/14.80 % (1893396)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 102.48/14.80 % (1893396)CaDiCaL version: 2.1.3 % 102.48/14.80 % (1893396)Termination reason: Instruction limit % 102.48/14.80 % (1893396)Termination phase: Finite model building constraint generation % 102.48/14.80 % (1893396)Time elapsed: 0.435 s % 102.48/14.80 % (1893396)Peak memory usage: 81 MB % 102.48/14.80 % (1893396)Instructions burned: 891 (million) % 102.48/14.80 % (1893402)fmb+10_1_sil=64000:random_seed=471455389:i=22061:nm=2:gsp=on_2990 on theBenchmark for (2990ds/22061Mi) % 102.48/14.80 % (1893403)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=661276220:i=9515:nm=5_2989 on theBenchmark for (2989ds/9515Mi) % 102.48/14.80 % (1893400)Instruction limit reached! % 102.48/14.80 % (1893400)------------------------------ % 102.48/14.80 % (1893400)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 102.48/14.80 % (1893400)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 102.48/14.80 % (1893400)CaDiCaL version: 2.1.3 % 102.48/14.80 % (1893400)Termination reason: Instruction limit % 102.48/14.80 % (1893400)Termination phase: Saturation % 102.48/14.80 % (1893400)Time elapsed: 0.474 s % 102.48/14.80 % (1893400)Peak memory usage: 19 MB % 102.48/14.80 % (1893400)Instructions burned: 880 (million) % 102.48/14.80 % TRYING [1] % 102.48/14.80 % (1893406)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3548978438:fmbsr=1.7:i=920_2988 on theBenchmark for (2988ds/920Mi) % 102.48/14.80 % (1893394)Instruction limit reached! % 102.48/14.80 % (1893394)------------------------------ % 102.48/14.80 % (1893394)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 102.48/14.80 % (1893394)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 102.48/14.80 % (1893394)CaDiCaL version: 2.1.3 % 102.48/14.80 % (1893394)Termination reason: Instruction limit % 102.48/14.80 % (1893394)Termination phase: Saturation % 102.48/14.80 % (1893394)Time elapsed: 0.734 s % 102.48/14.80 % (1893394)Peak memory usage: 24 MB % 102.48/14.80 % (1893394)Instructions burned: 1179 (million) % 102.48/14.80 % TRYING [20] % 102.48/14.80 % TRYING [2] % 102.48/14.80 % (1893408)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=739212735:i=5131_2987 on theBenchmark for (2987ds/5131Mi) % 102.48/14.80 % TRYING [8] % 102.48/14.80 % TRYING [3] % 102.48/14.80 % (1893406)Instruction limit reached! % 102.48/14.80 % (1893406)------------------------------ % 102.48/14.80 % (1893406)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 102.48/14.80 % (1893406)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 102.48/14.80 % (1893406)CaDiCaL version: 2.1.3 % 102.48/14.80 % (1893406)Termination reason: Instruction limit % 102.48/14.80 % (1893406)Termination phase: Finite model building constraint generation % 102.48/14.80 % (1893406)Time elapsed: 0.370 s % 102.48/14.80 % (1893406)Peak memory usage: 51 MB % 102.48/14.80 % (1893406)Instructions burned: 924 (million) % 102.48/14.80 % (1893410)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=996120925:i=1472:ins=7:fdi=8:gsp=on_2984 on theBenchmark for (2984ds/1472Mi) % 102.48/14.80 % (1893410)Instruction limit reached! % 102.48/14.80 % (1893410)------------------------------ % 102.48/14.80 % (1893410)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 102.48/14.80 % (1893410)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 102.48/14.80 % (1893410)CaDiCaL version: 2.1.3 % 102.48/14.80 % (1893410)Termination reason: Instruction limit % 102.48/14.80 % (1893410)Termination phase: Saturation % 102.48/14.80 % (1893410)Time elapsed: 0.894 s % 102.48/14.80 % (1893410)Peak memory usage: 31 MB % 102.48/14.80 % (1893410)Instructions burned: 1473 (million) % 102.48/14.80 % (1893412)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=4174033968:i=6324_2975 on theBenchmark for (2975ds/6324Mi) % 102.48/14.80 % TRYING [5] % 102.48/14.80 % (1893412)Cannot represent all propositional literals internally % 102.48/14.80 % (1893412)Refutation not found, incomplete strategy % 102.48/14.80 % (1893412)------------------------------ % 211.26/30.81 % (1893412)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 211.26/30.81 % (1893412)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 211.26/30.81 % (1893412)CaDiCaL version: 2.1.3 % 211.26/30.81 % (1893412)Termination reason: Refutation not found, incomplete strategy % 211.26/30.81 % (1893412)Time elapsed: 0.190 s % 211.26/30.81 % (1893412)Peak memory usage: 17 MB % 211.26/30.81 % (1893412)Instructions burned: 382 (million) % 211.26/30.81 % (1893412)------------------------------ % 211.26/30.81 % (1893412)------------------------------ % 211.26/30.81 % (1893414)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=2719176603:fmbsr=2.30978:i=2174_2972 on theBenchmark for (2972ds/2174Mi) % 211.26/30.81 % TRYING [4] % 211.26/30.81 % (1893414)Cannot represent all propositional literals internally % 211.26/30.81 % (1893414)Refutation not found, incomplete strategy % 211.26/30.81 % (1893414)------------------------------ % 211.26/30.81 % (1893414)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 211.26/30.81 % (1893414)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 211.26/30.81 % (1893414)CaDiCaL version: 2.1.3 % 211.26/30.81 % (1893414)Termination reason: Refutation not found, incomplete strategy % 211.26/30.81 % (1893414)Time elapsed: 0.703 s % 211.26/30.81 % (1893414)Peak memory usage: 26 MB % 211.26/30.81 % (1893414)Instructions burned: 1457 (million) % 211.26/30.81 % (1893414)------------------------------ % 211.26/30.81 % (1893414)------------------------------ % 211.26/30.81 % (1893416)ott-2_1_sil=16000:newcnf=on:random_seed=4242558519:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2965 on theBenchmark for (2965ds/869Mi) % 211.26/30.81 % (1893416)Instruction limit reached! % 211.26/30.81 % (1893416)------------------------------ % 211.26/30.81 % (1893416)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 211.26/30.81 % (1893416)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 211.26/30.81 % (1893416)CaDiCaL version: 2.1.3 % 211.26/30.81 % (1893416)Termination reason: Instruction limit % 211.26/30.81 % (1893416)Termination phase: Saturation % 211.26/30.81 % (1893416)Time elapsed: 0.468 s % 211.26/30.81 % (1893416)Peak memory usage: 17 MB % 211.26/30.81 % (1893416)Instructions burned: 869 (million) % 211.26/30.81 % (1893418)ott+10_1_sil=32000:tgt=ground:random_seed=2548993533:i=5114:av=off_2960 on theBenchmark for (2960ds/5114Mi) % 211.26/30.81 % (1893408)Instruction limit reached! % 211.26/30.81 % (1893408)------------------------------ % 211.26/30.81 % (1893408)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 211.26/30.81 % (1893408)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 211.26/30.81 % (1893408)CaDiCaL version: 2.1.3 % 211.26/30.81 % (1893408)Termination reason: Instruction limit % 211.26/30.81 % (1893408)Termination phase: Saturation % 211.26/30.81 % (1893408)Time elapsed: 3.013 s % 211.26/30.81 % (1893408)Peak memory usage: 47 MB % 211.26/30.81 % (1893408)Instructions burned: 5131 (million) % 211.26/30.81 % (1893420)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=1957084120:i=54282_2957 on theBenchmark for (2957ds/54282Mi) % 211.26/30.81 % TRYING [1] % 211.26/30.81 % TRYING [2] % 211.26/30.81 % (1893403)Instruction limit reached! % 211.26/30.81 % (1893403)------------------------------ % 211.26/30.81 % (1893403)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 211.26/30.81 % (1893403)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 211.26/30.81 % (1893403)CaDiCaL version: 2.1.3 % 211.26/30.81 % (1893403)Termination reason: Instruction limit % 211.26/30.81 % (1893403)Termination phase: Finite model building constraint generation % 211.26/30.81 % (1893403)Time elapsed: 3.523 s % 211.26/30.81 % (1893403)Peak memory usage: 636 MB % 211.26/30.81 % (1893403)Instructions burned: 9518 (million) % 211.26/30.81 % TRYING [3] % 211.26/30.81 % (1893422)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=1440486200:i=3512:aac=none_2953 on theBenchmark for (2953ds/3512Mi) % 211.26/30.81 % TRYING [4] % 211.26/30.81 % (1893422)Instruction limit reached! % 211.26/30.81 % (1893422)------------------------------ % 211.26/30.81 % (1893422)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 211.26/30.81 % (1893422)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 211.26/30.81 % (1893422)CaDiCaL version: 2.1.3 % 211.26/30.81 % (1893422)Termination reason: Instruction limit % 211.26/30.81 % (1893422)Termination phase: Saturation % 211.26/30.81 % (1893422)Time elapsed: 2.118 s % 211.26/30.81 % (1893422)Peak memory usage: 40 MB % 211.26/30.81 % (1893422)Instructions burned: 3513 (million) % 211.26/30.81 % (1893424)dis+21_1_sil=32000:sas=cadical:random_seed=4041327181:i=3773:amm=off_2932 on theBenchmark for (2932ds/3773Mi) % 270.20/38.45 % TRYING [5] % 270.20/38.45 % (1893418)Instruction limit reached! % 270.20/38.45 % (1893418)------------------------------ % 270.20/38.45 % (1893418)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 270.20/38.45 % (1893418)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 270.20/38.45 % (1893418)CaDiCaL version: 2.1.3 % 270.20/38.45 % (1893418)Termination reason: Instruction limit % 270.20/38.45 % (1893418)Termination phase: Saturation % 270.20/38.45 % (1893418)Time elapsed: 3.238 s % 270.20/38.45 % (1893418)Peak memory usage: 53 MB % 270.20/38.45 % (1893418)Instructions burned: 5114 (million) % 270.20/38.45 % (1893426)ott+11_1_sil=16000:gs=on:random_seed=621096099:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2928 on theBenchmark for (2928ds/2251Mi) % 270.20/38.45 % (1893426)Instruction limit reached! % 270.20/38.45 % (1893426)------------------------------ % 270.20/38.45 % (1893426)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 270.20/38.45 % (1893426)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 270.20/38.45 % (1893426)CaDiCaL version: 2.1.3 % 270.20/38.45 % (1893426)Termination reason: Instruction limit % 270.20/38.45 % (1893426)Termination phase: Saturation % 270.20/38.45 % (1893426)Time elapsed: 1.301 s % 270.20/38.45 % (1893426)Peak memory usage: 27 MB % 270.20/38.45 % (1893426)Instructions burned: 2253 (million) % 270.20/38.45 % (1893428)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=1226575452:fmbsr=1.6:i=67534_2914 on theBenchmark for (2914ds/67534Mi) % 270.20/38.45 % (1893424)Instruction limit reached! % 270.20/38.45 % (1893424)------------------------------ % 270.20/38.45 % (1893424)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 270.20/38.45 % (1893424)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 270.20/38.45 % (1893424)CaDiCaL version: 2.1.3 % 270.20/38.45 % (1893424)Termination reason: Instruction limit % 270.20/38.45 % (1893424)Termination phase: Saturation % 270.20/38.45 % (1893424)Time elapsed: 2.244 s % 270.20/38.45 % (1893424)Peak memory usage: 40 MB % 270.20/38.45 % (1893424)Instructions burned: 3773 (million) % 270.20/38.45 % (1893430)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=917363291:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2909 on theBenchmark for (2909ds/4591Mi) % 270.20/38.45 % TRYING [6] % 270.20/38.45 % (1893402)Instruction limit reached! % 270.20/38.45 % (1893402)------------------------------ % 270.20/38.45 % (1893402)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 270.20/38.45 % (1893402)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 270.20/38.45 % (1893402)CaDiCaL version: 2.1.3 % 270.20/38.45 % (1893402)Termination reason: Instruction limit % 270.20/38.45 % (1893402)Termination phase: Finite model building constraint generation % 270.20/38.45 % (1893402)Time elapsed: 8.901 s % 270.20/38.45 % (1893402)Peak memory usage: 301 MB % 270.20/38.45 % (1893402)Instructions burned: 22062 (million) % 270.20/38.45 % TRYING [7] % 270.20/38.45 % (1893432)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=2170219092:i=29340_2900 on theBenchmark for (2900ds/29340Mi) % 270.20/38.45 % (1893430)Instruction limit reached! % 270.20/38.45 % (1893430)------------------------------ % 270.20/38.45 % (1893430)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 270.20/38.45 % (1893430)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 270.20/38.45 % (1893430)CaDiCaL version: 2.1.3 % 270.20/38.45 % (1893430)Termination reason: Instruction limit % 270.20/38.45 % (1893430)Termination phase: Saturation % 270.20/38.45 % (1893430)Time elapsed: 2.589 s % 270.20/38.45 % (1893430)Peak memory usage: 56 MB % 270.20/38.45 % (1893430)Instructions burned: 4592 (million) % 270.20/38.45 % (1893434)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=202399074:i=5211_2883 on theBenchmark for (2883ds/5211Mi) % 270.20/38.45 % TRYING [6] % 270.20/38.45 % (1893434)Instruction limit reached! % 270.20/38.45 % (1893434)------------------------------ % 270.20/38.45 % (1893434)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 270.20/38.45 % (1893434)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 270.20/38.45 % (1893434)CaDiCaL version: 2.1.3 % 270.20/38.45 % (1893434)Termination reason: Instruction limit % 270.20/38.45 % (1893434)Termination phase: Saturation % 270.20/38.45 % (1893434)Time elapsed: 2.863 s % 270.20/38.45 % (1893434)Peak memory usage: 50 MB % 270.20/38.45 % (1893434)Instructions burned: 5213 (million) % 270.20/38.45 % (1893436)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=253615452:i=5497:nm=2_2854 on theBenchmark for (2854ds/5497Mi) % 300.33/42.64 % TRYING [17] % 300.33/42.64 % (1893436)Instruction limit reached! % 300.33/42.64 % (1893436)------------------------------ % 300.33/42.64 % (1893436)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.33/42.64 % (1893436)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.33/42.64 % (1893436)CaDiCaL version: 2.1.3 % 300.33/42.64 % (1893436)Termination reason: Instruction limit % 300.33/42.64 % (1893436)Termination phase: Finite model building constraint generation % 300.33/42.64 % (1893436)Time elapsed: 2.028 s % 300.33/42.64 % (1893436)Peak memory usage: 365 MB % 300.33/42.64 % (1893436)Instructions burned: 5498 (million) % 300.33/42.64 % (1893438)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=1749537261:fmbsr=2:i=46332_2833 on theBenchmark for (2833ds/46332Mi) % 300.33/42.64 % TRYING [15] % 300.33/42.64 % (1893370)Instruction limit reached! % 300.33/42.64 % (1893370)------------------------------ % 300.33/42.64 % (1893370)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.33/42.64 % (1893370)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.33/42.64 % (1893370)CaDiCaL version: 2.1.3 % 300.33/42.64 % (1893370)Termination reason: Instruction limit % 300.33/42.64 % (1893370)Termination phase: Saturation % 300.33/42.64 % (1893370)Time elapsed: 22.268 s % 300.33/42.64 % (1893370)Peak memory usage: 95 MB % 300.33/42.64 % (1893370)Instructions burned: 88028 (million) % 300.33/42.64 % (1893440)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=767710242:i=14071_2776 on theBenchmark for (2776ds/14071Mi) % 300.33/42.64 % TRYING [12] % 300.33/42.64 % (1893420)Instruction limit reached! % 300.33/42.64 % (1893420)------------------------------ % 300.33/42.64 % (1893420)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.33/42.64 % (1893420)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.33/42.64 % (1893420)CaDiCaL version: 2.1.3 % 300.33/42.64 % (1893420)Termination reason: Instruction limit % 300.33/42.64 % (1893420)Termination phase: Finite model building constraint generation % 300.33/42.64 % (1893420)Time elapsed: 20.877 s % 300.33/42.64 % (1893420)Peak memory usage: 2118 MB % 300.33/42.64 % (1893420)Instructions burned: 54285 (million) % 300.33/42.64 % (1893440)Instruction limit reached! % 300.33/42.64 % (1893440)------------------------------ % 300.33/42.64 % (1893440)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.33/42.64 % (1893440)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.33/42.64 % (1893440)CaDiCaL version: 2.1.3 % 300.33/42.64 % (1893440)Termination reason: Instruction limit % 300.33/42.64 % (1893440)Termination phase: Finite model building constraint generation % 300.33/42.64 % (1893440)Time elapsed: 2.829 s % 300.33/42.64 % (1893440)Peak memory usage: 1027 MB % 300.33/42.64 % (1893440)Instructions burned: 14076 (million) % 300.33/42.64 % (1893442)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1735719930:i=22565:add=on:rawr=on_2747 on theBenchmark for (2747ds/22565Mi) % 300.33/42.64 % (1893432)Instruction limit reached! % 300.33/42.64 % (1893432)------------------------------ % 300.33/42.64 % (1893432)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.33/42.64 % (1893432)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.33/42.64 % (1893432)CaDiCaL version: 2.1.3 % 300.33/42.64 % (1893432)Termination reason: Instruction limit % 300.33/42.64 % (1893432)Termination phase: Saturation % 300.33/42.64 % (1893432)Time elapsed: 15.418 s % 300.33/42.64 % (1893432)Peak memory usage: 212 MB % 300.33/42.64 % (1893432)Instructions burned: 29341 (million) % 300.33/42.64 % (1893444)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=502455228:i=8173:av=off_2745 on theBenchmark for (2745ds/8173Mi) % 300.33/42.64 % (1893445)dis+10_16:1_sil=16000:random_seed=1405167241:i=9155:fsr=off_2745 on theBenchmark for (2745ds/9155Mi) % 300.33/42.64 % (1893442)Instruction limit reached! % 300.33/42.64 % (1893442)------------------------------ % 300.33/42.64 % (1893442)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.33/42.64 % (1893442)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.33/42.64 % (1893442)CaDiCaL version: 2.1.3 % 300.33/42.64 % (1893442)Termination reason: Instruction limit % 300.33/42.64 % (1893442)Termination phase: Saturation % 300.33/42.64 % (1893442)Time elapsed: 5.321 s % 300.33/42.64 % (1893442)Peak memory usage: 54 MB % 300.33/42.64 % (1893442)Instructions burned: 22567 (million) % 300.33/42.64 % (1893448)ott-3_8_si % 300.33/42.64 Terminated % 300.33/42.64 % Vampire exiting % 300.33/42.64 Terminated %------------------------------------------------------------------------------