%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : NUM697+4 : TPTP v9.3.1. Released v7.3.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % Computer : n005.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:25:25 PM UTC 2026 % Result : Timeout 300.64s 42.84s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : NUM697+4 : TPTP v9.3.1. Released v7.3.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.12/0.37 % Computer : n005.cluster.edu % 0.12/0.37 % Model : x86_64 x86_64 % 0.12/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.37 % Memory : 8046.5625MB % 0.12/0.37 % OS : Linux 6.8.0-71-generic % 0.12/0.37 % CPULimit : 300 % 0.12/0.37 % WCLimit : 300 % 0.12/0.37 % DateTime : Sun Sep 27 21:07:32 UTC 2026 % 0.12/0.37 % CPUTime : % 0.12/0.37 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.12/0.40 Running first-order model finding % 0.12/0.40 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 % 11.33/2.10 % (163472)Will run a generic schedule for satisfiability detection. % 11.33/2.10 % (163480)dis+10_1_sil=32000:sp=arity:random_seed=1642422124:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 11.33/2.10 % (163478)% WARNING: option uhcvi not known. % 11.33/2.10 % (163477)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3459313477_2999 on theBenchmark for (2999ds/0Mi) % 11.33/2.10 % (163478)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1233083282:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 11.33/2.10 % (163479)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3447098951:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 11.33/2.10 % (163481)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1585963029:i=116_2999 on theBenchmark for (2999ds/116Mi) % 11.33/2.10 % (163482)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2103344836:i=131_2999 on theBenchmark for (2999ds/131Mi) % 11.33/2.10 % (163483)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2796763928:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 11.33/2.10 % (163480)Instruction limit reached! % 11.33/2.10 % (163480)------------------------------ % 11.33/2.10 % (163480)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 11.33/2.10 % (163480)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.33/2.10 % (163480)CaDiCaL version: 2.1.3 % 11.33/2.10 % (163480)Termination reason: Instruction limit % 11.33/2.10 % (163480)Termination phase: Saturation % 11.33/2.10 % (163480)Time elapsed: 0.030 s % 11.33/2.10 % (163480)Peak memory usage: 13 MB % 11.33/2.10 % (163480)Instructions burned: 104 (million) % 11.33/2.10 % (163491)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1482031475:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 11.33/2.10 % (163481)Instruction limit reached! % 11.33/2.10 % (163481)------------------------------ % 11.33/2.10 % (163481)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 11.33/2.10 % (163481)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.33/2.10 % (163481)CaDiCaL version: 2.1.3 % 11.33/2.10 % (163481)Termination reason: Instruction limit % 11.33/2.10 % (163481)Termination phase: Saturation % 11.33/2.10 % (163481)Time elapsed: 0.054 s % 11.33/2.10 % (163481)Peak memory usage: 13 MB % 11.33/2.10 % (163481)Instructions burned: 116 (million) % 11.33/2.10 % (163482)Instruction limit reached! % 11.33/2.10 % (163482)------------------------------ % 11.33/2.10 % (163482)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 11.33/2.10 % (163482)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.33/2.10 % (163482)CaDiCaL version: 2.1.3 % 11.33/2.10 % (163482)Termination reason: Instruction limit % 11.33/2.10 % (163482)Termination phase: Saturation % 11.33/2.10 % (163482)Time elapsed: 0.068 s % 11.33/2.10 % (163482)Peak memory usage: 14 MB % 11.33/2.10 % (163482)Instructions burned: 132 (million) % 11.33/2.10 % (163493)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=683324595:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi) % 11.33/2.10 % (163494)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=3271666507:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi) % 11.33/2.10 % (163483)Instruction limit reached! % 11.33/2.10 % (163483)------------------------------ % 11.33/2.10 % (163483)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 11.33/2.10 % (163483)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.33/2.10 % (163483)CaDiCaL version: 2.1.3 % 11.33/2.10 % (163483)Termination reason: Instruction limit % 11.33/2.10 % (163483)Termination phase: Saturation % 11.33/2.10 % (163483)Time elapsed: 0.094 s % 11.33/2.10 % (163483)Peak memory usage: 15 MB % 11.33/2.10 % (163483)Instructions burned: 160 (million) % 11.33/2.10 % (163497)ott-21_1_sil=16000:fs=off:random_seed=2638881189:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 11.33/2.10 % (163493)Instruction limit reached! % 11.33/2.10 % (163493)------------------------------ % 11.33/2.10 % (163493)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 11.33/2.10 % (163493)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.33/2.10 % (163493)CaDiCaL version: 2.1.3 % 11.33/2.10 % (163493)Termination reason: Instruction limit % 35.95/5.59 % (163493)Termination phase: Saturation % 35.95/5.59 % (163493)Time elapsed: 0.064 s % 35.95/5.59 % (163493)Peak memory usage: 14 MB % 35.95/5.59 % (163493)Instructions burned: 132 (million) % 35.95/5.59 % (163499)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=818047106:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 35.95/5.59 % TRYING [1] % 35.95/5.59 % TRYING [2] % 35.95/5.59 % (163497)Instruction limit reached! % 35.95/5.59 % (163497)------------------------------ % 35.95/5.59 % (163497)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 35.95/5.59 % (163497)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 35.95/5.59 % (163497)CaDiCaL version: 2.1.3 % 35.95/5.59 % (163497)Termination reason: Instruction limit % 35.95/5.59 % (163497)Termination phase: Saturation % 35.95/5.59 % (163497)Time elapsed: 0.082 s % 35.95/5.59 % (163497)Peak memory usage: 13 MB % 35.95/5.59 % (163497)Instructions burned: 181 (million) % 35.95/5.59 % (163491)Instruction limit reached! % 35.95/5.59 % (163491)------------------------------ % 35.95/5.59 % (163491)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 35.95/5.59 % (163491)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 35.95/5.59 % (163491)CaDiCaL version: 2.1.3 % 35.95/5.59 % (163491)Termination reason: Instruction limit % 35.95/5.59 % (163491)Termination phase: Finite model building constraint generation % 35.95/5.59 % (163491)Time elapsed: 0.182 s % 35.95/5.59 % (163491)Peak memory usage: 35 MB % 35.95/5.59 % (163491)Instructions burned: 717 (million) % 35.95/5.59 % (163501)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=936310767:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi) % 35.95/5.59 % (163503)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2461941641:i=1179_2997 on theBenchmark for (2997ds/1179Mi) % 35.95/5.59 % TRYING [1] % 35.95/5.59 % TRYING [2] % 35.95/5.59 % (163494)Instruction limit reached! % 35.95/5.59 % (163494)------------------------------ % 35.95/5.59 % (163494)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 35.95/5.59 % (163494)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 35.95/5.59 % (163494)CaDiCaL version: 2.1.3 % 35.95/5.59 % (163494)Termination reason: Instruction limit % 35.95/5.59 % (163494)Termination phase: Saturation % 35.95/5.59 % (163494)Time elapsed: 0.338 s % 35.95/5.59 % (163494)Peak memory usage: 18 MB % 35.95/5.59 % (163494)Instructions burned: 684 (million) % 35.95/5.59 % TRYING [3] % 35.95/5.59 % (163499)Instruction limit reached! % 35.95/5.59 % (163499)------------------------------ % 35.95/5.59 % (163499)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 35.95/5.59 % (163499)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 35.95/5.59 % (163499)CaDiCaL version: 2.1.3 % 35.95/5.59 % (163499)Termination reason: Instruction limit % 35.95/5.59 % (163499)Termination phase: Saturation % 35.95/5.59 % (163499)Time elapsed: 0.284 s % 35.95/5.59 % (163499)Peak memory usage: 17 MB % 35.95/5.59 % (163499)Instructions burned: 478 (million) % 35.95/5.59 % (163505)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=531680576:i=889:ins=1_2995 on theBenchmark for (2995ds/889Mi) % 35.95/5.59 % (163506)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=633330532:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2995 on theBenchmark for (2995ds/692Mi) % 35.95/5.59 % TRYING [1] % 35.95/5.59 % TRYING [2] % 35.95/5.59 % (163503)Instruction limit reached! % 35.95/5.59 % (163503)------------------------------ % 35.95/5.59 % (163503)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 35.95/5.59 % (163503)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 35.95/5.59 % (163503)CaDiCaL version: 2.1.3 % 35.95/5.59 % (163503)Termination reason: Instruction limit % 35.95/5.59 % (163503)Termination phase: Saturation % 35.95/5.59 % (163503)Time elapsed: 0.388 s % 35.95/5.59 % (163503)Peak memory usage: 25 MB % 35.95/5.59 % (163503)Instructions burned: 1180 (million) % 35.95/5.59 % (163501)Instruction limit reached! % 35.95/5.59 % (163501)------------------------------ % 35.95/5.59 % (163501)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 35.95/5.59 % (163501)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 35.95/5.59 % (163501)CaDiCaL version: 2.1.3 % 35.95/5.59 % (163501)Termination reason: Instruction limit % 35.95/5.59 % (163501)Termination phase: Finite model building constraint generation % 35.95/5.59 % (163501)Time elapsed: 0.401 s % 102.61/14.93 % (163501)Peak memory usage: 35 MB % 102.61/14.93 % (163501)Instructions burned: 865 (million) % 102.61/14.93 % (163509)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1862882104:i=879:kws=inv_precedence:fsr=off_2993 on theBenchmark for (2993ds/879Mi) % 102.61/14.93 % (163510)fmb+10_1_sil=64000:random_seed=69781965:i=22061:nm=2:gsp=on_2993 on theBenchmark for (2993ds/22061Mi) % 102.61/14.93 % (163506)Instruction limit reached! % 102.61/14.93 % (163506)------------------------------ % 102.61/14.93 % (163506)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 102.61/14.93 % (163506)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 102.61/14.93 % (163506)CaDiCaL version: 2.1.3 % 102.61/14.93 % (163506)Termination reason: Instruction limit % 102.61/14.93 % (163506)Termination phase: Saturation % 102.61/14.93 % (163506)Time elapsed: 0.374 s % 102.61/14.93 % (163506)Peak memory usage: 19 MB % 102.61/14.93 % (163506)Instructions burned: 693 (million) % 102.61/14.93 % (163509)Instruction limit reached! % 102.61/14.93 % (163509)------------------------------ % 102.61/14.93 % (163509)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 102.61/14.93 % (163509)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 102.61/14.93 % (163509)CaDiCaL version: 2.1.3 % 102.61/14.93 % (163509)Termination reason: Instruction limit % 102.61/14.93 % (163509)Termination phase: Saturation % 102.61/14.93 % (163509)Time elapsed: 0.210 s % 102.61/14.93 % (163509)Peak memory usage: 19 MB % 102.61/14.93 % (163509)Instructions burned: 879 (million) % 102.61/14.93 % (163514)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2706694855:fmbsr=1.7:i=920_2991 on theBenchmark for (2991ds/920Mi) % 102.61/14.93 % (163513)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3019291491:i=9515:nm=5_2991 on theBenchmark for (2991ds/9515Mi) % 102.61/14.93 % (163505)Instruction limit reached! % 102.61/14.93 % (163505)------------------------------ % 102.61/14.93 % (163505)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 102.61/14.93 % (163505)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 102.61/14.93 % (163505)CaDiCaL version: 2.1.3 % 102.61/14.93 % (163505)Termination reason: Instruction limit % 102.61/14.93 % (163505)Termination phase: Finite model building constraint generation % 102.61/14.93 % (163505)Time elapsed: 0.436 s % 102.61/14.93 % (163505)Peak memory usage: 62 MB % 102.61/14.93 % (163505)Instructions burned: 892 (million) % 102.61/14.93 % (163517)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=4103763220:i=5131_2990 on theBenchmark for (2990ds/5131Mi) % 102.61/14.93 % TRYING [1] % 102.61/14.93 % TRYING [4] % 102.61/14.93 % TRYING [2] % 102.61/14.93 % TRYING [8] % 102.61/14.93 % (163514)Instruction limit reached! % 102.61/14.93 % (163514)------------------------------ % 102.61/14.93 % (163514)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 102.61/14.93 % (163514)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 102.61/14.93 % (163514)CaDiCaL version: 2.1.3 % 102.61/14.93 % (163514)Termination reason: Instruction limit % 102.61/14.93 % (163514)Termination phase: Finite model building constraint generation % 102.61/14.93 % (163514)Time elapsed: 0.215 s % 102.61/14.93 % (163514)Peak memory usage: 45 MB % 102.61/14.93 % (163514)Instructions burned: 923 (million) % 102.61/14.93 % (163519)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1715502572:i=1472:ins=7:fdi=8:gsp=on_2988 on theBenchmark for (2988ds/1472Mi) % 102.61/14.93 % TRYING [20] % 102.61/14.93 % (163519)Instruction limit reached! % 102.61/14.93 % (163519)------------------------------ % 102.61/14.93 % (163519)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 102.61/14.93 % (163519)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 102.61/14.93 % (163519)CaDiCaL version: 2.1.3 % 102.61/14.93 % (163519)Termination reason: Instruction limit % 102.61/14.93 % (163519)Termination phase: Saturation % 102.61/14.93 % (163519)Time elapsed: 0.382 s % 102.61/14.93 % (163519)Peak memory usage: 27 MB % 102.61/14.93 % (163519)Instructions burned: 1473 (million) % 102.61/14.93 % (163521)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3872561080:i=6324_2984 on theBenchmark for (2984ds/6324Mi) % 102.61/14.93 % TRYING [3] % 102.61/14.93 % (163521)Cannot represent all propositional literals internally % 102.61/14.93 % (163521)Refutation not found, incomplete strategy % 102.61/14.93 % (163521)------------------------------ % 102.61/14.93 % (163521)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 102.61/14.93 % (163521)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 217.20/31.10 % (163521)CaDiCaL version: 2.1.3 % 217.20/31.10 % (163521)Termination reason: Refutation not found, incomplete strategy % 217.20/31.10 % (163521)Time elapsed: 0.157 s % 217.20/31.10 % (163521)Peak memory usage: 23 MB % 217.20/31.10 % (163521)Instructions burned: 614 (million) % 217.20/31.10 % (163521)------------------------------ % 217.20/31.10 % (163521)------------------------------ % 217.20/31.10 % (163523)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=688068410:fmbsr=2.30978:i=2174_2983 on theBenchmark for (2983ds/2174Mi) % 217.20/31.10 % TRYING [16] % 217.20/31.10 % (163523)Instruction limit reached! % 217.20/31.10 % (163523)------------------------------ % 217.20/31.10 % (163523)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 217.20/31.10 % (163523)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 217.20/31.10 % (163523)CaDiCaL version: 2.1.3 % 217.20/31.10 % (163523)Termination reason: Instruction limit % 217.20/31.10 % (163523)Termination phase: Finite model building constraint generation % 217.20/31.10 % (163523)Time elapsed: 0.430 s % 217.20/31.10 % (163523)Peak memory usage: 115 MB % 217.20/31.10 % (163523)Instructions burned: 2178 (million) % 217.20/31.10 % (163525)ott-2_1_sil=16000:newcnf=on:random_seed=3546171300:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2978 on theBenchmark for (2978ds/869Mi) % 217.20/31.10 % (163525)Instruction limit reached! % 217.20/31.10 % (163525)------------------------------ % 217.20/31.10 % (163525)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 217.20/31.10 % (163525)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 217.20/31.10 % (163525)CaDiCaL version: 2.1.3 % 217.20/31.10 % (163525)Termination reason: Instruction limit % 217.20/31.10 % (163525)Termination phase: Saturation % 217.20/31.10 % (163525)Time elapsed: 0.251 s % 217.20/31.10 % (163525)Peak memory usage: 16 MB % 217.20/31.10 % (163525)Instructions burned: 871 (million) % 217.20/31.10 % (163527)ott+10_1_sil=32000:tgt=ground:random_seed=2106099136:i=5114:av=off_2975 on theBenchmark for (2975ds/5114Mi) % 217.20/31.10 % TRYING [5] % 217.20/31.10 % TRYING [4] % 217.20/31.10 % (163517)Instruction limit reached! % 217.20/31.10 % (163517)------------------------------ % 217.20/31.10 % (163517)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 217.20/31.10 % (163517)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 217.20/31.10 % (163517)CaDiCaL version: 2.1.3 % 217.20/31.10 % (163517)Termination reason: Instruction limit % 217.20/31.10 % (163517)Termination phase: Saturation % 217.20/31.10 % (163517)Time elapsed: 2.805 s % 217.20/31.10 % (163517)Peak memory usage: 55 MB % 217.20/31.10 % (163517)Instructions burned: 5132 (million) % 217.20/31.10 % (163529)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2535105525:i=54282_2962 on theBenchmark for (2962ds/54282Mi) % 217.20/31.10 % TRYING [1] % 217.20/31.10 % (163527)Instruction limit reached! % 217.20/31.10 % (163527)------------------------------ % 217.20/31.10 % (163527)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 217.20/31.10 % (163527)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 217.20/31.10 % (163527)CaDiCaL version: 2.1.3 % 217.20/31.10 % (163527)Termination reason: Instruction limit % 217.20/31.10 % (163527)Termination phase: Saturation % 217.20/31.10 % (163527)Time elapsed: 1.670 s % 217.20/31.10 % (163527)Peak memory usage: 62 MB % 217.20/31.10 % (163527)Instructions burned: 5114 (million) % 217.20/31.10 % TRYING [2] % 217.20/31.10 % (163531)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=804376736:i=3512:aac=none_2958 on theBenchmark for (2958ds/3512Mi) % 217.20/31.10 % TRYING [3] % 217.20/31.10 % (163513)Instruction limit reached! % 217.20/31.10 % (163513)------------------------------ % 217.20/31.10 % (163513)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 217.20/31.10 % (163513)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 217.20/31.10 % (163513)CaDiCaL version: 2.1.3 % 217.20/31.10 % (163513)Termination reason: Instruction limit % 217.20/31.10 % (163513)Termination phase: Finite model building constraint generation % 217.20/31.10 % (163513)Time elapsed: 3.517 s % 217.20/31.10 % (163513)Peak memory usage: 642 MB % 217.20/31.10 % (163513)Instructions burned: 9515 (million) % 217.20/31.10 % (163533)dis+21_1_sil=32000:sas=cadical:random_seed=1598568634:i=3773:amm=off_2954 on theBenchmark for (2954ds/3773Mi) % 217.20/31.10 % TRYING [4] % 217.20/31.10 % (163531)Instruction limit reached! % 217.20/31.10 % (163531)------------------------------ % 217.20/31.10 % (163531)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 217.20/31.10 % (163531)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 217.20/31.10 % (1635Terminated % 300.64/42.84 % Vampire exiting % 300.64/42.84 Terminated %------------------------------------------------------------------------------