%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : NUM250-2 : TPTP v9.3.1. Bugfixed v2.1.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % Computer : n012.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 12:18:08 PM UTC 2026 % Result : Timeout 300.85s 43.05s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.01 % Problem : NUM250-2 : TPTP v9.3.1. Bugfixed v2.1.0. % 0.00/0.02 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.03/0.30 % Computer : n012.cluster.edu % 0.03/0.30 % Model : x86_64 x86_64 % 0.03/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.03/0.30 % Memory : 8046.5625MB % 0.03/0.30 % OS : Linux 6.8.0-71-generic % 0.03/0.30 % CPULimit : 300 % 0.03/0.30 % WCLimit : 300 % 0.03/0.30 % DateTime : Sun Sep 27 19:18:35 UTC 2026 % 0.03/0.30 % CPUTime : % 0.03/0.30 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.03/0.32 Running first-order model finding % 0.03/0.32 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 % 9.38/1.87 % (2680467)Will run a generic schedule for satisfiability detection. % 9.38/1.87 % (2680473)% WARNING: option uhcvi not known. % 9.38/1.87 % (2680472)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2527917837_2999 on theBenchmark for (2999ds/0Mi) % 9.38/1.87 % (2680478)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=755086302:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 9.38/1.87 % (2680473)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2540426085:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 9.38/1.87 % (2680474)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2645133429:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 9.38/1.87 % (2680475)dis+10_1_sil=32000:sp=arity:random_seed=1904692387:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 9.38/1.87 % (2680476)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3385806751:i=116_2999 on theBenchmark for (2999ds/116Mi) % 9.38/1.87 % (2680477)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3512485846:i=131_2999 on theBenchmark for (2999ds/131Mi) % 9.38/1.87 % (2680476)Instruction limit reached! % 9.38/1.87 % (2680476)------------------------------ % 9.38/1.87 % (2680476)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 9.38/1.87 % (2680476)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.38/1.87 % (2680476)CaDiCaL version: 2.1.3 % 9.38/1.87 % (2680476)Termination reason: Instruction limit % 9.38/1.87 % (2680476)Termination phase: Saturation % 9.38/1.87 % (2680476)Time elapsed: 0.038 s % 9.38/1.87 % (2680476)Peak memory usage: 13 MB % 9.38/1.87 % (2680476)Instructions burned: 118 (million) % 9.38/1.87 % (2680475)Instruction limit reached! % 9.38/1.87 % (2680475)------------------------------ % 9.38/1.87 % (2680475)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 9.38/1.87 % (2680475)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.38/1.87 % (2680475)CaDiCaL version: 2.1.3 % 9.38/1.87 % (2680475)Termination reason: Instruction limit % 9.38/1.87 % (2680475)Termination phase: Saturation % 9.38/1.87 % (2680475)Time elapsed: 0.039 s % 9.38/1.87 % (2680475)Peak memory usage: 13 MB % 9.38/1.87 % (2680475)Instructions burned: 104 (million) % 9.38/1.87 % (2680477)Instruction limit reached! % 9.38/1.87 % (2680477)------------------------------ % 9.38/1.87 % (2680477)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 9.38/1.87 % (2680477)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.38/1.87 % (2680477)CaDiCaL version: 2.1.3 % 9.38/1.87 % (2680477)Termination reason: Instruction limit % 9.38/1.87 % (2680477)Termination phase: Saturation % 9.38/1.87 % (2680477)Time elapsed: 0.046 s % 9.38/1.87 % (2680477)Peak memory usage: 13 MB % 9.38/1.87 % (2680477)Instructions burned: 133 (million) % 9.38/1.87 % (2680486)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=346479998:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 9.38/1.87 % (2680487)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2573479097:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 9.38/1.87 % (2680488)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=2528988369:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi) % 9.38/1.87 % (2680478)Instruction limit reached! % 9.38/1.87 % (2680478)------------------------------ % 9.38/1.87 % (2680478)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 9.38/1.87 % (2680478)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.38/1.87 % (2680478)CaDiCaL version: 2.1.3 % 9.38/1.87 % (2680478)Termination reason: Instruction limit % 9.38/1.87 % (2680478)Termination phase: Saturation % 9.38/1.87 % (2680478)Time elapsed: 0.066 s % 9.38/1.87 % (2680478)Peak memory usage: 14 MB % 9.38/1.87 % (2680478)Instructions burned: 159 (million) % 9.38/1.87 % (2680492)ott-21_1_sil=16000:fs=off:random_seed=4028862110:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi) % 9.38/1.87 % (2680487)Instruction limit reached! % 9.38/1.87 % (2680487)------------------------------ % 9.38/1.87 % (2680487)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 9.38/1.87 % (2680487)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.38/1.87 % (2680487)CaDiCaL version: 2.1.3 % 28.17/4.43 % (2680487)Termination reason: Instruction limit % 28.17/4.43 % (2680487)Termination phase: Saturation % 28.17/4.43 % (2680487)Time elapsed: 0.046 s % 28.17/4.43 % (2680487)Peak memory usage: 12 MB % 28.17/4.43 % (2680487)Instructions burned: 131 (million) % 28.17/4.43 % (2680494)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2193637487:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 28.17/4.43 % (2680492)Instruction limit reached! % 28.17/4.43 % (2680492)------------------------------ % 28.17/4.43 % (2680492)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 28.17/4.43 % (2680492)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.17/4.43 % (2680492)CaDiCaL version: 2.1.3 % 28.17/4.43 % (2680492)Termination reason: Instruction limit % 28.17/4.43 % (2680492)Termination phase: Saturation % 28.17/4.43 % (2680492)Time elapsed: 0.055 s % 28.17/4.43 % (2680492)Peak memory usage: 13 MB % 28.17/4.43 % (2680492)Instructions burned: 181 (million) % 28.17/4.43 % TRYING [1] % 28.17/4.43 % TRYING [2] % 28.17/4.43 % (2680496)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3762256602:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 28.17/4.43 % TRYING [3] % 28.17/4.43 % TRYING [1] % 28.17/4.43 % TRYING [2] % 28.17/4.43 % TRYING [3] % 28.17/4.43 % (2680486)Instruction limit reached! % 28.17/4.43 % (2680486)------------------------------ % 28.17/4.43 % (2680486)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 28.17/4.43 % (2680486)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.17/4.43 % (2680486)CaDiCaL version: 2.1.3 % 28.17/4.43 % (2680486)Termination reason: Instruction limit % 28.17/4.43 % (2680486)Termination phase: Finite model building constraint generation % 28.17/4.43 % (2680486)Time elapsed: 0.177 s % 28.17/4.43 % (2680486)Peak memory usage: 20 MB % 28.17/4.43 % (2680486)Instructions burned: 721 (million) % 28.17/4.43 % (2680498)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1770662527:i=1179_2997 on theBenchmark for (2997ds/1179Mi) % 28.17/4.43 % TRYING [1] % 28.17/4.43 % TRYING [4] % 28.17/4.43 % TRYING [2] % 28.17/4.43 % (2680494)Instruction limit reached! % 28.17/4.43 % (2680494)------------------------------ % 28.17/4.43 % (2680494)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 28.17/4.43 % (2680494)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.17/4.43 % (2680494)CaDiCaL version: 2.1.3 % 28.17/4.43 % (2680494)Termination reason: Instruction limit % 28.17/4.43 % (2680494)Termination phase: Saturation % 28.17/4.43 % (2680494)Time elapsed: 0.188 s % 28.17/4.43 % (2680494)Peak memory usage: 14 MB % 28.17/4.43 % (2680494)Instructions burned: 478 (million) % 28.17/4.43 % (2680488)Instruction limit reached! % 28.17/4.43 % (2680488)------------------------------ % 28.17/4.43 % (2680488)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 28.17/4.43 % (2680488)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.17/4.43 % (2680488)CaDiCaL version: 2.1.3 % 28.17/4.43 % (2680488)Termination reason: Instruction limit % 28.17/4.43 % (2680488)Termination phase: Saturation % 28.17/4.43 % (2680488)Time elapsed: 0.247 s % 28.17/4.43 % (2680488)Peak memory usage: 17 MB % 28.17/4.43 % (2680488)Instructions burned: 686 (million) % 28.17/4.43 % (2680500)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=4170786883:i=889:ins=1_2996 on theBenchmark for (2996ds/889Mi) % 28.17/4.43 % (2680501)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=686582217:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2996 on theBenchmark for (2996ds/692Mi) % 28.17/4.43 % (2680496)Instruction limit reached! % 28.17/4.43 % (2680496)------------------------------ % 28.17/4.43 % (2680496)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 28.17/4.43 % (2680496)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.17/4.43 % (2680496)CaDiCaL version: 2.1.3 % 28.17/4.43 % (2680496)Termination reason: Instruction limit % 28.17/4.43 % (2680496)Termination phase: Finite model building SAT solving % 28.17/4.43 % (2680496)Time elapsed: 0.230 s % 28.17/4.43 % (2680496)Peak memory usage: 21 MB % 28.17/4.43 % (2680496)Instructions burned: 870 (million) % 28.17/4.43 % (2680504)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1058002234:i=879:kws=inv_precedence:fsr=off_2995 on theBenchmark for (2995ds/879Mi) % 28.17/4.43 % (2680501)Instruction limit reached! % 28.17/4.43 % (2680501)------------------------------ % 28.17/4.43 % (2680501)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 61.84/9.15 % (2680501)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 61.84/9.15 % (2680501)CaDiCaL version: 2.1.3 % 61.84/9.15 % (2680501)Termination reason: Instruction limit % 61.84/9.15 % (2680501)Termination phase: Saturation % 61.84/9.15 % (2680501)Time elapsed: 0.234 s % 61.84/9.15 % (2680501)Peak memory usage: 20 MB % 61.84/9.15 % (2680501)Instructions burned: 693 (million) % 61.84/9.15 % (2680500)Instruction limit reached! % 61.84/9.15 % (2680500)------------------------------ % 61.84/9.15 % (2680500)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 61.84/9.15 % (2680500)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 61.84/9.15 % (2680500)CaDiCaL version: 2.1.3 % 61.84/9.15 % (2680500)Termination reason: Instruction limit % 61.84/9.15 % (2680500)Termination phase: Finite model building constraint generation % 61.84/9.15 % (2680500)Time elapsed: 0.245 s % 61.84/9.15 % (2680500)Peak memory usage: 62 MB % 61.84/9.15 % (2680500)Instructions burned: 892 (million) % 61.84/9.15 % (2680506)fmb+10_1_sil=64000:random_seed=2004413314:i=22061:nm=2:gsp=on_2994 on theBenchmark for (2994ds/22061Mi) % 61.84/9.15 % (2680507)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2535640293:i=9515:nm=5_2994 on theBenchmark for (2994ds/9515Mi) % 61.84/9.15 % (2680498)Instruction limit reached! % 61.84/9.15 % (2680498)------------------------------ % 61.84/9.15 % (2680498)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 61.84/9.15 % (2680498)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 61.84/9.15 % (2680498)CaDiCaL version: 2.1.3 % 61.84/9.15 % (2680498)Termination reason: Instruction limit % 61.84/9.15 % (2680498)Termination phase: Saturation % 61.84/9.15 % (2680498)Time elapsed: 0.395 s % 61.84/9.15 % (2680498)Peak memory usage: 26 MB % 61.84/9.15 % (2680498)Instructions burned: 1180 (million) % 61.84/9.15 % (2680510)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2692747769:fmbsr=1.7:i=920_2993 on theBenchmark for (2993ds/920Mi) % 61.84/9.15 % (2680504)Instruction limit reached! % 61.84/9.15 % (2680504)------------------------------ % 61.84/9.15 % (2680504)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 61.84/9.15 % (2680504)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 61.84/9.15 % (2680504)CaDiCaL version: 2.1.3 % 61.84/9.15 % (2680504)Termination reason: Instruction limit % 61.84/9.15 % (2680504)Termination phase: Saturation % 61.84/9.15 % (2680504)Time elapsed: 0.268 s % 61.84/9.15 % (2680504)Peak memory usage: 19 MB % 61.84/9.15 % (2680504)Instructions burned: 879 (million) % 61.84/9.15 % (2680512)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=443261364:i=5131_2993 on theBenchmark for (2993ds/5131Mi) % 61.84/9.15 % TRYING [1] % 61.84/9.15 % TRYING [20] % 61.84/9.15 % TRYING [2] % 61.84/9.15 % TRYING [8] % 61.84/9.15 % TRYING [5] % 61.84/9.15 % TRYING [3] % 61.84/9.15 % (2680510)Instruction limit reached! % 61.84/9.15 % (2680510)------------------------------ % 61.84/9.15 % (2680510)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 61.84/9.15 % (2680510)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 61.84/9.15 % (2680510)CaDiCaL version: 2.1.3 % 61.84/9.15 % (2680510)Termination reason: Instruction limit % 61.84/9.15 % (2680510)Termination phase: Finite model building constraint generation % 61.84/9.15 % (2680510)Time elapsed: 0.215 s % 61.84/9.15 % (2680510)Peak memory usage: 42 MB % 61.84/9.15 % (2680510)Instructions burned: 921 (million) % 61.84/9.15 % (2680514)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=362245802:i=1472:ins=7:fdi=8:gsp=on_2991 on theBenchmark for (2991ds/1472Mi) % 61.84/9.15 % TRYING [4] % 61.84/9.15 % (2680514)Instruction limit reached! % 61.84/9.15 % (2680514)------------------------------ % 61.84/9.15 % (2680514)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 61.84/9.15 % (2680514)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 61.84/9.15 % (2680514)CaDiCaL version: 2.1.3 % 61.84/9.15 % (2680514)Termination reason: Instruction limit % 61.84/9.15 % (2680514)Termination phase: Saturation % 61.84/9.15 % (2680514)Time elapsed: 0.480 s % 61.84/9.15 % (2680514)Peak memory usage: 33 MB % 61.84/9.15 % (2680514)Instructions burned: 1472 (million) % 61.84/9.15 % (2680516)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=1912259162:i=6324_2986 on theBenchmark for (2986ds/6324Mi) % 61.84/9.15 % (2680516)Cannot represent all propositional literals internally % 61.84/9.15 % (2680516)Refutation not found, incomplete strategy % 61.84/9.15 % (2680516)------------------------------ % 135.02/19.54 % (2680516)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 135.02/19.54 % (2680516)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 135.02/19.54 % (2680516)CaDiCaL version: 2.1.3 % 135.02/19.54 % (2680516)Termination reason: Refutation not found, incomplete strategy % 135.02/19.54 % (2680516)Time elapsed: 0.138 s % 135.02/19.54 % (2680516)Peak memory usage: 14 MB % 135.02/19.54 % (2680516)Instructions burned: 511 (million) % 135.02/19.54 % (2680516)------------------------------ % 135.02/19.54 % (2680516)------------------------------ % 135.02/19.54 % (2680519)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1199017741:fmbsr=2.30978:i=2174_2984 on theBenchmark for (2984ds/2174Mi) % 135.02/19.54 % (2680519)Instruction limit reached! % 135.02/19.54 % (2680519)------------------------------ % 135.02/19.54 % (2680519)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 135.02/19.54 % (2680519)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 135.02/19.54 % (2680519)CaDiCaL version: 2.1.3 % 135.02/19.54 % (2680519)Termination reason: Instruction limit % 135.02/19.54 % (2680519)Termination phase: Finite model building preprocessing % 135.02/19.54 % (2680519)Time elapsed: 0.623 s % 135.02/19.54 % (2680519)Peak memory usage: 18 MB % 135.02/19.54 % (2680519)Instructions burned: 2175 (million) % 135.02/19.54 % (2680521)ott-2_1_sil=16000:newcnf=on:random_seed=1179149984:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2978 on theBenchmark for (2978ds/869Mi) % 135.02/19.54 % (2680512)Instruction limit reached! % 135.02/19.54 % (2680512)------------------------------ % 135.02/19.54 % (2680512)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 135.02/19.54 % (2680512)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 135.02/19.54 % (2680512)CaDiCaL version: 2.1.3 % 135.02/19.54 % (2680512)Termination reason: Instruction limit % 135.02/19.54 % (2680512)Termination phase: Saturation % 135.02/19.54 % (2680512)Time elapsed: 1.561 s % 135.02/19.54 % (2680512)Peak memory usage: 34 MB % 135.02/19.54 % (2680512)Instructions burned: 5134 (million) % 135.02/19.54 % (2680523)ott+10_1_sil=32000:tgt=ground:random_seed=3515404616:i=5114:av=off_2977 on theBenchmark for (2977ds/5114Mi) % 135.02/19.54 % (2680521)Instruction limit reached! % 135.02/19.54 % (2680521)------------------------------ % 135.02/19.54 % (2680521)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 135.02/19.54 % (2680521)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 135.02/19.54 % (2680521)CaDiCaL version: 2.1.3 % 135.02/19.54 % (2680521)Termination reason: Instruction limit % 135.02/19.54 % (2680521)Termination phase: Saturation % 135.02/19.54 % (2680521)Time elapsed: 0.305 s % 135.02/19.54 % (2680521)Peak memory usage: 20 MB % 135.02/19.54 % (2680521)Instructions burned: 870 (million) % 135.02/19.54 % (2680525)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2458481299:i=54282_2975 on theBenchmark for (2975ds/54282Mi) % 135.02/19.54 % (2680507)Instruction limit reached! % 135.02/19.54 % (2680507)------------------------------ % 135.02/19.54 % (2680507)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 135.02/19.54 % (2680507)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 135.02/19.54 % (2680507)CaDiCaL version: 2.1.3 % 135.02/19.54 % (2680507)Termination reason: Instruction limit % 135.02/19.54 % (2680507)Termination phase: Finite model building constraint generation % 135.02/19.54 % (2680507)Time elapsed: 1.924 s % 135.02/19.54 % (2680507)Peak memory usage: 656 MB % 135.02/19.54 % (2680507)Instructions burned: 9521 (million) % 135.02/19.54 % (2680527)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3537585142:i=3512:aac=none_2974 on theBenchmark for (2974ds/3512Mi) % 135.02/19.54 % TRYING [1] % 135.02/19.54 % TRYING [2] % 135.02/19.54 % TRYING [3] % 135.02/19.54 % TRYING [4] % 135.02/19.54 % TRYING [6] % 135.02/19.54 % TRYING [5] % 135.02/19.54 % TRYING [5] % 135.02/19.54 % (2680527)Instruction limit reached! % 135.02/19.54 % (2680527)------------------------------ % 135.02/19.54 % (2680527)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 135.02/19.54 % (2680527)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 135.02/19.54 % (2680527)CaDiCaL version: 2.1.3 % 135.02/19.54 % (2680527)Termination reason: Instruction limit % 135.02/19.54 % (2680527)Termination phase: Saturation % 135.02/19.54 % (2680527)Time elapsed: 1.099 s % 135.02/19.54 % (2680527)Peak memory usage: 32 MB % 135.02/19.54 % (2680527)Instructions burned: 3515 (million) % 135.02/19.54 % (2680529)dis+21_1_sil=32000:sas=cadical:random_seed=3983136830:i=3773:amm=off_2963 on theBenchmark for (2963ds/3773Mi) % 135.02/19.54 % (2680523)Instruction limit reached! % 200.58/28.83 % (2680523)------------------------------ % 200.58/28.83 % (2680523)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 200.58/28.83 % (2680523)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 200.58/28.83 % (2680523)CaDiCaL version: 2.1.3 % 200.58/28.83 % (2680523)Termination reason: Instruction limit % 200.58/28.83 % (2680523)Termination phase: Saturation % 200.58/28.83 % (2680523)Time elapsed: 1.827 s % 200.58/28.83 % (2680523)Peak memory usage: 51 MB % 200.58/28.83 % (2680523)Instructions burned: 5116 (million) % 200.58/28.83 % (2680531)ott+11_1_sil=16000:gs=on:random_seed=3347860236:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2958 on theBenchmark for (2958ds/2251Mi) % 200.58/28.83 % (2680531)Instruction limit reached! % 200.58/28.83 % (2680531)------------------------------ % 200.58/28.83 % (2680531)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 200.58/28.83 % (2680531)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 200.58/28.83 % (2680531)CaDiCaL version: 2.1.3 % 200.58/28.83 % (2680531)Termination reason: Instruction limit % 200.58/28.83 % (2680531)Termination phase: Saturation % 200.58/28.83 % (2680531)Time elapsed: 0.573 s % 200.58/28.83 % (2680531)Peak memory usage: 21 MB % 200.58/28.83 % (2680531)Instructions burned: 2251 (million) % 200.58/28.83 % (2680533)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=882048748:fmbsr=1.6:i=67534_2953 on theBenchmark for (2953ds/67534Mi) % 200.58/28.83 % (2680529)Instruction limit reached! % 200.58/28.83 % (2680529)------------------------------ % 200.58/28.83 % (2680529)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 200.58/28.83 % (2680529)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 200.58/28.83 % (2680529)CaDiCaL version: 2.1.3 % 200.58/28.83 % (2680529)Termination reason: Instruction limit % 200.58/28.83 % (2680529)Termination phase: Saturation % 200.58/28.83 % (2680529)Time elapsed: 1.191 s % 200.58/28.83 % (2680529)Peak memory usage: 35 MB % 200.58/28.83 % (2680529)Instructions burned: 3776 (million) % 200.58/28.83 % (2680535)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=588784593:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2951 on theBenchmark for (2951ds/4591Mi) % 200.58/28.83 % TRYING [7] % 200.58/28.83 % TRYING [6] % 200.58/28.83 % (2680506)Instruction limit reached! % 200.58/28.83 % (2680506)------------------------------ % 200.58/28.83 % (2680506)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 200.58/28.83 % (2680506)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 200.58/28.83 % (2680506)CaDiCaL version: 2.1.3 % 200.58/28.83 % (2680506)Termination reason: Instruction limit % 200.58/28.83 % (2680506)Termination phase: Finite model building SAT solving % 200.58/28.83 % (2680506)Time elapsed: 5.165 s % 200.58/28.83 % (2680506)Peak memory usage: 458 MB % 200.58/28.83 % (2680506)Instructions burned: 22064 (million) % 200.58/28.83 % (2680537)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=1164198271:i=29340_2942 on theBenchmark for (2942ds/29340Mi) % 200.58/28.83 % (2680535)Instruction limit reached! % 200.58/28.83 % (2680535)------------------------------ % 200.58/28.83 % (2680535)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 200.58/28.83 % (2680535)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 200.58/28.83 % (2680535)CaDiCaL version: 2.1.3 % 200.58/28.83 % (2680535)Termination reason: Instruction limit % 200.58/28.83 % (2680535)Termination phase: Saturation % 200.58/28.83 % (2680535)Time elapsed: 1.397 s % 200.58/28.83 % (2680535)Peak memory usage: 54 MB % 200.58/28.83 % (2680535)Instructions burned: 4592 (million) % 200.58/28.83 % (2680539)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=2009578606:i=5211_2936 on theBenchmark for (2936ds/5211Mi) % 200.58/28.83 % (2680539)Instruction limit reached! % 200.58/28.83 % (2680539)------------------------------ % 200.58/28.83 % (2680539)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 200.58/28.83 % (2680539)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 200.58/28.83 % (2680539)CaDiCaL version: 2.1.3 % 200.58/28.83 % (2680539)Termination reason: Instruction limit % 200.58/28.83 % (2680539)Termination phase: Saturation % 200.58/28.83 % (2680539)Time elapsed: 1.376 s % 200.58/28.83 % (2680539)Peak memory usage: 43 MB % 200.58/28.83 % (2680539)Instructions burned: 5212 (million) % 200.58/28.83 % (2680541)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=1531189734:i=5497:nm=2_2923 on theBenchmark for (2923ds/5497Mi) % 200.58/28.83 % TRYING [17] % 200.58/28.83 % (26Terminated % 300.85/43.05 % Vampire exiting %------------------------------------------------------------------------------