%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : TOP040+4 : TPTP v9.3.1. Released v3.4.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % Computer : n002.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 02:34:27 PM UTC 2026 % Result : Timeout 300.01s 44.18s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : TOP040+4 : TPTP v9.3.1. Released v3.4.0. % 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.09/0.20 % Computer : n002.cluster.edu % 0.09/0.20 % Model : x86_64 x86_64 % 0.09/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.20 % Memory : 8046.5625MB % 0.09/0.20 % OS : Linux 6.8.0-71-generic % 0.09/0.20 % CPULimit : 300 % 0.09/0.20 % WCLimit : 300 % 0.09/0.20 % DateTime : Mon Sep 28 19:04:28 UTC 2026 % 0.09/0.20 % CPUTime : % 0.09/0.20 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.09/0.23 Running first-order model finding % 0.09/0.23 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 % 27.39/6.06 % (655308)Will run a generic schedule for satisfiability detection. % 27.39/6.06 % (655314)% WARNING: option uhcvi not known. % 27.39/6.06 % (655317)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1303516158:i=116_2981 on theBenchmark for (2981ds/116Mi) % 27.39/6.06 % (655313)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1914041679_2981 on theBenchmark for (2981ds/0Mi) % 27.39/6.06 % (655314)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=307665053:i=135531:add=off:rawr=on_2981 on theBenchmark for (2981ds/135531Mi) % 27.39/6.06 % (655315)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=419509294:i=88024:add=on:rawr=on_2981 on theBenchmark for (2981ds/88024Mi) % 27.39/6.06 % (655316)dis+10_1_sil=32000:sp=arity:random_seed=3565952441:i=103:fgj=on_2981 on theBenchmark for (2981ds/103Mi) % 27.39/6.06 % (655318)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1146393535:i=131_2981 on theBenchmark for (2981ds/131Mi) % 27.39/6.06 % (655319)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3191352835:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2981 on theBenchmark for (2981ds/159Mi) % 27.39/6.06 % (655317)Instruction limit reached! % 27.39/6.06 % (655317)------------------------------ % 27.39/6.06 % (655317)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 27.39/6.06 % (655317)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.39/6.06 % (655317)CaDiCaL version: 2.1.3 % 27.39/6.06 % (655317)Termination reason: Instruction limit % 27.39/6.06 % (655317)Termination phase: Preprocessing 1 % 27.39/6.06 % (655317)Time elapsed: 0.060 s % 27.39/6.06 % (655317)Peak memory usage: 80 MB % 27.39/6.06 % (655317)Instructions burned: 118 (million) % 27.39/6.06 % (655327)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1988131649:i=714:nm=2_2980 on theBenchmark for (2980ds/714Mi) % 27.39/6.06 % (655316)Instruction limit reached! % 27.39/6.06 % (655316)------------------------------ % 27.39/6.06 % (655316)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 27.39/6.06 % (655316)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.39/6.06 % (655316)CaDiCaL version: 2.1.3 % 27.39/6.06 % (655316)Termination reason: Instruction limit % 27.39/6.06 % (655316)Termination phase: Preprocessing 1 % 27.39/6.06 % (655316)Time elapsed: 0.074 s % 27.39/6.06 % (655316)Peak memory usage: 80 MB % 27.39/6.06 % (655316)Instructions burned: 103 (million) % 27.39/6.06 % (655318)Instruction limit reached! % 27.39/6.06 % (655318)------------------------------ % 27.39/6.06 % (655318)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 27.39/6.06 % (655318)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.39/6.06 % (655318)CaDiCaL version: 2.1.3 % 27.39/6.06 % (655318)Termination reason: Instruction limit % 27.39/6.06 % (655318)Termination phase: Preprocessing 1 % 27.39/6.06 % (655318)Time elapsed: 0.096 s % 27.39/6.06 % (655318)Peak memory usage: 80 MB % 27.39/6.06 % (655318)Instructions burned: 132 (million) % 27.39/6.06 % (655329)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=4091683882:i=131:bd=preordered:fsd=on_2980 on theBenchmark for (2980ds/131Mi) % 27.39/6.06 % (655319)Instruction limit reached! % 27.39/6.06 % (655319)------------------------------ % 27.39/6.06 % (655319)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 27.39/6.06 % (655319)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.39/6.06 % (655319)CaDiCaL version: 2.1.3 % 27.39/6.06 % (655319)Termination reason: Instruction limit % 27.39/6.06 % (655319)Termination phase: Preprocessing 1 % 27.39/6.06 % (655319)Time elapsed: 0.113 s % 27.39/6.06 % (655319)Peak memory usage: 80 MB % 27.39/6.06 % (655319)Instructions burned: 159 (million) % 27.39/6.06 % (655331)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=597988401:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2979 on theBenchmark for (2979ds/684Mi) % 27.39/6.06 % (655332)ott-21_1_sil=16000:fs=off:random_seed=4202162697:i=180:av=off:fsr=off_2979 on theBenchmark for (2979ds/180Mi) % 27.39/6.06 % (655329)Instruction limit reached! % 27.39/6.06 % (655329)------------------------------ % 27.39/6.06 % (655329)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 27.39/6.06 % (655329)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.39/6.06 % (655329)CaDiCaL version: 2.1.3 % 27.39/6.06 % (655329)Termination reason: Instruction limit % 58.10/10.13 % (655329)Termination phase: Preprocessing 1 % 58.10/10.13 % (655329)Time elapsed: 0.094 s % 58.10/10.13 % (655329)Peak memory usage: 80 MB % 58.10/10.13 % (655329)Instructions burned: 131 (million) % 58.10/10.13 % (655335)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2426832009:i=477:bd=all_2978 on theBenchmark for (2978ds/477Mi) % 58.10/10.13 % (655332)Instruction limit reached! % 58.10/10.13 % (655332)------------------------------ % 58.10/10.13 % (655332)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 58.10/10.13 % (655332)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 58.10/10.13 % (655332)CaDiCaL version: 2.1.3 % 58.10/10.13 % (655332)Termination reason: Instruction limit % 58.10/10.13 % (655332)Termination phase: Preprocessing 1 % 58.10/10.13 % (655332)Time elapsed: 0.128 s % 58.10/10.13 % (655332)Peak memory usage: 80 MB % 58.10/10.13 % (655332)Instructions burned: 180 (million) % 58.10/10.13 % (655337)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2880687175:fmbsr=1.3:i=865:ins=25_2978 on theBenchmark for (2978ds/865Mi) % 58.10/10.13 % (655327)Instruction limit reached! % 58.10/10.13 % (655327)------------------------------ % 58.10/10.13 % (655327)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 58.10/10.13 % (655327)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 58.10/10.13 % (655327)CaDiCaL version: 2.1.3 % 58.10/10.13 % (655327)Termination reason: Instruction limit % 58.10/10.13 % (655327)Termination phase: Naming % 58.10/10.13 % (655327)Time elapsed: 0.329 s % 58.10/10.13 % (655327)Peak memory usage: 125 MB % 58.10/10.13 % (655327)Instructions burned: 715 (million) % 58.10/10.13 % (655339)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3297646968:i=1179_2976 on theBenchmark for (2976ds/1179Mi) % 58.10/10.13 % (655335)Instruction limit reached! % 58.10/10.13 % (655335)------------------------------ % 58.10/10.13 % (655335)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 58.10/10.13 % (655335)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 58.10/10.13 % (655335)CaDiCaL version: 2.1.3 % 58.10/10.13 % (655335)Termination reason: Instruction limit % 58.10/10.13 % (655335)Termination phase: Preprocessing 2 % 58.10/10.13 % (655335)Time elapsed: 0.387 s % 58.10/10.13 % (655335)Peak memory usage: 100 MB % 58.10/10.13 % (655335)Instructions burned: 477 (million) % 58.10/10.13 % (655341)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3472150882:i=889:ins=1_2974 on theBenchmark for (2974ds/889Mi) % 58.10/10.13 % (655331)Instruction limit reached! % 58.10/10.13 % (655331)------------------------------ % 58.10/10.13 % (655331)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 58.10/10.13 % (655331)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 58.10/10.13 % (655331)CaDiCaL version: 2.1.3 % 58.10/10.13 % (655331)Termination reason: Instruction limit % 58.10/10.13 % (655331)Termination phase: Preprocessing 2 % 58.10/10.13 % (655331)Time elapsed: 0.532 s % 58.10/10.13 % (655331)Peak memory usage: 95 MB % 58.10/10.13 % (655331)Instructions burned: 684 (million) % 58.10/10.13 % (655343)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=3824031664:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2974 on theBenchmark for (2974ds/692Mi) % 58.10/10.13 % (655337)Instruction limit reached! % 58.10/10.13 % (655337)------------------------------ % 58.10/10.13 % (655337)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 58.10/10.13 % (655337)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 58.10/10.13 % (655337)CaDiCaL version: 2.1.3 % 58.10/10.13 % (655337)Termination reason: Instruction limit % 58.10/10.13 % (655337)Termination phase: Preprocessing 3 % 58.10/10.13 % (655337)Time elapsed: 0.580 s % 58.10/10.13 % (655337)Peak memory usage: 127 MB % 58.10/10.13 % (655337)Instructions burned: 866 (million) % 58.10/10.13 % (655339)Instruction limit reached! % 58.10/10.13 % (655339)------------------------------ % 58.10/10.13 % (655339)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 58.10/10.13 % (655339)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 58.10/10.13 % (655339)CaDiCaL version: 2.1.3 % 58.10/10.13 % (655339)Termination reason: Instruction limit % 58.10/10.13 % (655339)Termination phase: Preprocessing 3 % 58.10/10.13 % (655339)Time elapsed: 0.465 s % 58.10/10.13 % (655339)Peak memory usage: 136 MB % 58.10/10.13 % (655339)Instructions burned: 1179 (million) % 58.10/10.13 % (655346)fmb+10_1_sil=64000:random_seed=2354862105:i=22061:nm=2:gsp=on_2971 on theBenchmark for (2971ds/22061Mi) % 121.93/19.10 % (655345)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=4184143075:i=879:kws=inv_precedence:fsr=off_2971 on theBenchmark for (2971ds/879Mi) % 121.93/19.10 % (655343)Instruction limit reached! % 121.93/19.10 % (655343)------------------------------ % 121.93/19.10 % (655343)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 121.93/19.10 % (655343)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 121.93/19.10 % (655343)CaDiCaL version: 2.1.3 % 121.93/19.10 % (655343)Termination reason: Instruction limit % 121.93/19.10 % (655343)Termination phase: Preprocessing 2 % 121.93/19.10 % (655343)Time elapsed: 0.524 s % 121.93/19.10 % (655343)Peak memory usage: 96 MB % 121.93/19.10 % (655343)Instructions burned: 692 (million) % 121.93/19.10 % (655349)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=4241405320:i=9515:nm=5_2968 on theBenchmark for (2968ds/9515Mi) % 121.93/19.10 % (655341)Instruction limit reached! % 121.93/19.10 % (655341)------------------------------ % 121.93/19.10 % (655341)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 121.93/19.10 % (655341)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 121.93/19.10 % (655341)CaDiCaL version: 2.1.3 % 121.93/19.10 % (655341)Termination reason: Instruction limit % 121.93/19.10 % (655341)Termination phase: Preprocessing 3 % 121.93/19.10 % (655341)Time elapsed: 0.650 s % 121.93/19.10 % (655341)Peak memory usage: 126 MB % 121.93/19.10 % (655341)Instructions burned: 890 (million) % 121.93/19.10 % (655351)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=4167841971:fmbsr=1.7:i=920_2967 on theBenchmark for (2967ds/920Mi) % 121.93/19.10 % (655345)Instruction limit reached! % 121.93/19.10 % (655345)------------------------------ % 121.93/19.10 % (655345)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 121.93/19.10 % (655345)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 121.93/19.10 % (655345)CaDiCaL version: 2.1.3 % 121.93/19.10 % (655345)Termination reason: Instruction limit % 121.93/19.10 % (655345)Termination phase: NewCNF % 121.93/19.10 % (655345)Time elapsed: 0.617 s % 121.93/19.10 % (655345)Peak memory usage: 130 MB % 121.93/19.10 % (655345)Instructions burned: 881 (million) % 121.93/19.10 % (655353)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=4196746187:i=5131_2965 on theBenchmark for (2965ds/5131Mi) % 121.93/19.10 % (655351)Instruction limit reached! % 121.93/19.10 % (655351)------------------------------ % 121.93/19.10 % (655351)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 121.93/19.10 % (655351)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 121.93/19.10 % (655351)CaDiCaL version: 2.1.3 % 121.93/19.10 % (655351)Termination reason: Instruction limit % 121.93/19.10 % (655351)Termination phase: Preprocessing 3 % 121.93/19.10 % (655351)Time elapsed: 0.664 s % 121.93/19.10 % (655351)Peak memory usage: 128 MB % 121.93/19.10 % (655351)Instructions burned: 921 (million) % 121.93/19.10 % (655355)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1053976784:i=1472:ins=7:fdi=8:gsp=on_2960 on theBenchmark for (2960ds/1472Mi) % 121.93/19.10 % (655355)Instruction limit reached! % 121.93/19.10 % (655355)------------------------------ % 121.93/19.10 % (655355)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 121.93/19.10 % (655355)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 121.93/19.10 % (655355)CaDiCaL version: 2.1.3 % 121.93/19.10 % (655355)Termination reason: Instruction limit % 121.93/19.10 % (655355)Termination phase: Preprocessing 3 % 121.93/19.10 % (655355)Time elapsed: 0.965 s % 121.93/19.10 % (655355)Peak memory usage: 149 MB % 121.93/19.10 % (655355)Instructions burned: 1473 (million) % 121.93/19.10 % (655357)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=777442211:i=6324_2950 on theBenchmark for (2950ds/6324Mi) % 121.93/19.10 % (655353)Instruction limit reached! % 121.93/19.10 % (655353)------------------------------ % 121.93/19.10 % (655353)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 121.93/19.10 % (655353)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 121.93/19.10 % (655353)CaDiCaL version: 2.1.3 % 121.93/19.10 % (655353)Termination reason: Instruction limit % 121.93/19.10 % (655353)Termination phase: Property scanning % 121.93/19.10 % (655353)Time elapsed: 2.303 s % 121.93/19.10 % (655353)Peak memory usage: 186 MB % 121.93/19.10 % (655353)Instructions burned: 5133 (million) % 121.93/19.10 % (655359)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=3066275807:fmbsr=2.30978:i=2174_2941 on theBenchmark for (2941ds/2174Mi) % 201.88/30.36 % (655346)Instruction limit reached! % 201.88/30.36 % (655346)------------------------------ % 201.88/30.36 % (655346)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 201.88/30.36 % (655346)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 201.88/30.36 % (655346)CaDiCaL version: 2.1.3 % 201.88/30.36 % (655346)Termination reason: Instruction limit % 201.88/30.36 % (655346)Termination phase: Finite model building preprocessing % 201.88/30.36 % (655346)Time elapsed: 4.138 s % 201.88/30.36 % (655346)Peak memory usage: 256 MB % 201.88/30.36 % (655346)Instructions burned: 22067 (million) % 201.88/30.36 % (655361)ott-2_1_sil=16000:newcnf=on:random_seed=4181089040:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2930 on theBenchmark for (2930ds/869Mi) % 201.88/30.36 % (655359)Instruction limit reached! % 201.88/30.36 % (655359)------------------------------ % 201.88/30.36 % (655359)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 201.88/30.36 % (655359)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 201.88/30.36 % (655359)CaDiCaL version: 2.1.3 % 201.88/30.36 % (655359)Termination reason: Instruction limit % 201.88/30.36 % (655359)Termination phase: Property scanning % 201.88/30.36 % (655359)Time elapsed: 1.363 s % 201.88/30.36 % (655359)Peak memory usage: 174 MB % 201.88/30.36 % (655359)Instructions burned: 2176 (million) % 201.88/30.36 % (655363)ott+10_1_sil=32000:tgt=ground:random_seed=1093980416:i=5114:av=off_2927 on theBenchmark for (2927ds/5114Mi) % 201.88/30.36 % (655361)Instruction limit reached! % 201.88/30.36 % (655361)------------------------------ % 201.88/30.36 % (655361)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 201.88/30.36 % (655361)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 201.88/30.36 % (655361)CaDiCaL version: 2.1.3 % 201.88/30.36 % (655361)Termination reason: Instruction limit % 201.88/30.36 % (655361)Termination phase: NewCNF % 201.88/30.36 % (655361)Time elapsed: 0.365 s % 201.88/30.36 % (655361)Peak memory usage: 130 MB % 201.88/30.36 % (655361)Instructions burned: 870 (million) % 201.88/30.36 % (655365)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=3878782588:i=54282_2926 on theBenchmark for (2926ds/54282Mi) % 201.88/30.36 % (655349)Instruction limit reached! % 201.88/30.36 % (655349)------------------------------ % 201.88/30.36 % (655349)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 201.88/30.36 % (655349)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 201.88/30.36 % (655349)CaDiCaL version: 2.1.3 % 201.88/30.36 % (655349)Termination reason: Instruction limit % 201.88/30.36 % (655349)Termination phase: Finite model building preprocessing % 201.88/30.36 % (655349)Time elapsed: 4.239 s % 201.88/30.36 % (655349)Peak memory usage: 212 MB % 201.88/30.36 % (655349)Instructions burned: 9518 (million) % 201.88/30.36 % (655367)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=1968614390:i=3512:aac=none_2925 on theBenchmark for (2925ds/3512Mi) % 201.88/30.36 % (655357)Instruction limit reached! % 201.88/30.36 % (655357)------------------------------ % 201.88/30.36 % (655357)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 201.88/30.36 % (655357)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 201.88/30.36 % (655357)CaDiCaL version: 2.1.3 % 201.88/30.36 % (655357)Termination reason: Instruction limit % 201.88/30.36 % (655357)Termination phase: Blocked clause elimination % 201.88/30.36 % (655357)Time elapsed: 3.421 s % 201.88/30.36 % (655357)Peak memory usage: 225 MB % 201.88/30.36 % (655357)Instructions burned: 6324 (million) % 201.88/30.36 % (655369)dis+21_1_sil=32000:sas=cadical:random_seed=2652763222:i=3773:amm=off_2916 on theBenchmark for (2916ds/3773Mi) % 201.88/30.36 % (655367)Instruction limit reached! % 201.88/30.36 % (655367)------------------------------ % 201.88/30.36 % (655367)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 201.88/30.36 % (655367)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 201.88/30.36 % (655367)CaDiCaL version: 2.1.3 % 201.88/30.36 % (655367)Termination reason: Instruction limit % 201.88/30.36 % (655367)Termination phase: Function definition elimination % 201.88/30.36 % (655367)Time elapsed: 1.877 s % 201.88/30.36 % (655367)Peak memory usage: 177 MB % 201.88/30.36 % (655367)Instructions burned: 3513 (million) % 201.88/30.36 % (655371)ott+11_1_sil=16000:gs=on:random_seed=3989094472:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2906 on theBenchmark for (2906ds/2251Mi) % 201.88/30.36 % (655363)Instruction limit reached! Terminated %------------------------------------------------------------------------------