%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWV515-1.030 : TPTP v9.3.1. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % Computer : n013.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:24:49 PM UTC 2026 % Result : Timeout 300.30s 42.64s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWV515-1.030 : TPTP v9.3.1. Released v4.0.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.09/0.21 % Computer : n013.cluster.edu % 0.09/0.21 % Model : x86_64 x86_64 % 0.09/0.21 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.21 % Memory : 8046.5625MB % 0.09/0.21 % OS : Linux 6.8.0-71-generic % 0.09/0.21 % CPULimit : 300 % 0.09/0.21 % WCLimit : 300 % 0.09/0.21 % DateTime : Mon Sep 28 11:24:52 UTC 2026 % 0.09/0.21 % CPUTime : % 0.09/0.21 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.09/0.24 Running first-order model finding % 0.09/0.24 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 % 13.34/2.15 % (1113930)Will run a generic schedule for satisfiability detection. % 13.34/2.15 % (1113939)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3735675072:i=116_2999 on theBenchmark for (2999ds/116Mi) % 13.34/2.15 % (1113936)% WARNING: option uhcvi not known. % 13.34/2.15 % (1113935)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=452296451_2999 on theBenchmark for (2999ds/0Mi) % 13.34/2.15 % (1113937)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2551498871:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 13.34/2.15 % (1113936)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1892486809:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 13.34/2.15 % (1113938)dis+10_1_sil=32000:sp=arity:random_seed=2548359620:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 13.34/2.15 % (1113940)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=902120187:i=131_2999 on theBenchmark for (2999ds/131Mi) % 13.34/2.15 % (1113941)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2703777333:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 13.34/2.15 % Detected minimum model sizes of [30] % 13.34/2.15 % Detected maximum model sizes of [max] % 13.34/2.15 % TRYING [30] % 13.34/2.15 % (1113939)Instruction limit reached! % 13.34/2.15 % (1113939)------------------------------ % 13.34/2.15 % (1113939)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 13.34/2.15 % (1113939)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.34/2.15 % (1113939)CaDiCaL version: 2.1.3 % 13.34/2.15 % (1113939)Termination reason: Instruction limit % 13.34/2.15 % (1113939)Termination phase: Saturation % 13.34/2.15 % (1113939)Time elapsed: 0.035 s % 13.34/2.15 % (1113939)Peak memory usage: 13 MB % 13.34/2.15 % (1113939)Instructions burned: 118 (million) % 13.34/2.15 % (1113949)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=239254250:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 13.34/2.15 % Detected minimum model sizes of [30] % 13.34/2.15 % Detected maximum model sizes of [max] % 13.34/2.15 % TRYING [30] % 13.34/2.15 % (1113938)Instruction limit reached! % 13.34/2.15 % (1113938)------------------------------ % 13.34/2.15 % (1113938)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 13.34/2.15 % (1113938)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.34/2.15 % (1113938)CaDiCaL version: 2.1.3 % 13.34/2.15 % (1113938)Termination reason: Instruction limit % 13.34/2.15 % (1113938)Termination phase: Saturation % 13.34/2.15 % (1113938)Time elapsed: 0.056 s % 13.34/2.15 % (1113938)Peak memory usage: 12 MB % 13.34/2.15 % (1113938)Instructions burned: 103 (million) % 13.34/2.15 % (1113940)Instruction limit reached! % 13.34/2.15 % (1113940)------------------------------ % 13.34/2.15 % (1113940)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 13.34/2.15 % (1113940)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.34/2.15 % (1113940)CaDiCaL version: 2.1.3 % 13.34/2.15 % (1113940)Termination reason: Instruction limit % 13.34/2.15 % (1113940)Termination phase: Saturation % 13.34/2.15 % (1113940)Time elapsed: 0.073 s % 13.34/2.15 % (1113940)Peak memory usage: 13 MB % 13.34/2.15 % (1113940)Instructions burned: 131 (million) % 13.34/2.15 % (1113951)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=4113161696:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 13.34/2.15 % (1113952)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=2289114003:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi) % 13.34/2.15 % (1113941)Instruction limit reached! % 13.34/2.15 % (1113941)------------------------------ % 13.34/2.15 % (1113941)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 13.34/2.15 % (1113941)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.34/2.15 % (1113941)CaDiCaL version: 2.1.3 % 13.34/2.15 % (1113941)Termination reason: Instruction limit % 13.34/2.15 % (1113941)Termination phase: Saturation % 13.34/2.15 % (1113941)Time elapsed: 0.094 s % 13.34/2.15 % (1113941)Peak memory usage: 13 MB % 13.34/2.15 % (1113941)Instructions burned: 160 (million) % 13.34/2.15 % (1113955)ott-21_1_sil=16000:fs=off:random_seed=3137082165:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 13.34/2.15 % (1113951)Instruction limit reached! % 13.34/2.15 % (1113951)------------------------------ % 13.34/2.15 % (1113951)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 38.61/5.72 % (1113951)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 38.61/5.72 % (1113951)CaDiCaL version: 2.1.3 % 38.61/5.72 % (1113951)Termination reason: Instruction limit % 38.61/5.72 % (1113951)Termination phase: Saturation % 38.61/5.72 % (1113951)Time elapsed: 0.061 s % 38.61/5.72 % (1113951)Peak memory usage: 12 MB % 38.61/5.72 % (1113951)Instructions burned: 132 (million) % 38.61/5.72 % (1113957)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2623321589:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 38.61/5.72 % (1113949)Instruction limit reached! % 38.61/5.72 % (1113949)------------------------------ % 38.61/5.72 % (1113949)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 38.61/5.72 % (1113949)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 38.61/5.72 % (1113949)CaDiCaL version: 2.1.3 % 38.61/5.72 % (1113949)Termination reason: Instruction limit % 38.61/5.72 % (1113949)Termination phase: Finite model building constraint generation % 38.61/5.72 % (1113949)Time elapsed: 0.144 s % 38.61/5.72 % (1113949)Peak memory usage: 59 MB % 38.61/5.72 % (1113949)Instructions burned: 717 (million) % 38.61/5.72 % (1113955)Instruction limit reached! % 38.61/5.72 % (1113955)------------------------------ % 38.61/5.72 % (1113955)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 38.61/5.72 % (1113955)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 38.61/5.72 % (1113955)CaDiCaL version: 2.1.3 % 38.61/5.72 % (1113955)Termination reason: Instruction limit % 38.61/5.72 % (1113955)Termination phase: Saturation % 38.61/5.72 % (1113955)Time elapsed: 0.085 s % 38.61/5.72 % (1113955)Peak memory usage: 11 MB % 38.61/5.72 % (1113955)Instructions burned: 182 (million) % 38.61/5.72 % (1113959)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2058179292:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi) % 38.61/5.72 % (1113960)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2140688597:i=1179_2997 on theBenchmark for (2997ds/1179Mi) % 38.61/5.72 % Detected minimum model sizes of [30] % 38.61/5.72 % Detected maximum model sizes of [max] % 38.61/5.72 % (1113957)Instruction limit reached! % 38.61/5.72 % (1113957)------------------------------ % 38.61/5.72 % (1113957)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 38.61/5.72 % (1113957)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 38.61/5.72 % (1113957)CaDiCaL version: 2.1.3 % 38.61/5.72 % (1113957)Termination reason: Instruction limit % 38.61/5.72 % (1113957)Termination phase: Saturation % 38.61/5.72 % (1113957)Time elapsed: 0.243 s % 38.61/5.72 % (1113957)Peak memory usage: 14 MB % 38.61/5.72 % (1113957)Instructions burned: 479 (million) % 38.61/5.72 % (1113963)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=4144814278:i=889:ins=1_2995 on theBenchmark for (2995ds/889Mi) % 38.61/5.72 % (1113952)Instruction limit reached! % 38.61/5.72 % (1113952)------------------------------ % 38.61/5.72 % (1113952)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 38.61/5.72 % (1113952)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 38.61/5.72 % (1113952)CaDiCaL version: 2.1.3 % 38.61/5.72 % (1113952)Termination reason: Instruction limit % 38.61/5.72 % (1113952)Termination phase: Saturation % 38.61/5.72 % (1113952)Time elapsed: 0.370 s % 38.61/5.72 % (1113952)Peak memory usage: 16 MB % 38.61/5.72 % (1113952)Instructions burned: 685 (million) % 38.61/5.72 % (1113965)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=4156323976: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) % 38.61/5.72 % (1113960)Instruction limit reached! % 38.61/5.72 % (1113960)------------------------------ % 38.61/5.72 % (1113960)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 38.61/5.72 % (1113960)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 38.61/5.72 % (1113960)CaDiCaL version: 2.1.3 % 38.61/5.72 % (1113960)Termination reason: Instruction limit % 38.61/5.72 % (1113960)Termination phase: Saturation % 38.61/5.72 % (1113960)Time elapsed: 0.324 s % 38.61/5.72 % (1113960)Peak memory usage: 23 MB % 38.61/5.72 % (1113960)Instructions burned: 1179 (million) % 38.61/5.72 % (1113967)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2504768241:i=879:kws=inv_precedence:fsr=off_2994 on theBenchmark for (2994ds/879Mi) % 38.61/5.72 % (1113959)Instruction limit reached! % 93.94/13.54 % (1113959)------------------------------ % 93.94/13.54 % (1113959)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 93.94/13.54 % (1113959)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 93.94/13.54 % (1113959)CaDiCaL version: 2.1.3 % 93.94/13.54 % (1113959)Termination reason: Instruction limit % 93.94/13.54 % (1113959)Termination phase: Finite model building constraint generation % 93.94/13.54 % (1113959)Time elapsed: 0.408 s % 93.94/13.54 % (1113959)Peak memory usage: 107 MB % 93.94/13.54 % (1113959)Instructions burned: 865 (million) % 93.94/13.54 % (1113969)fmb+10_1_sil=64000:random_seed=94108807:i=22061:nm=2:gsp=on_2993 on theBenchmark for (2993ds/22061Mi) % 93.94/13.54 % Detected minimum model sizes of [30] % 93.94/13.54 % Detected maximum model sizes of [max] % 93.94/13.54 % (1113967)Instruction limit reached! % 93.94/13.54 % (1113967)------------------------------ % 93.94/13.54 % (1113967)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 93.94/13.54 % (1113967)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 93.94/13.54 % (1113967)CaDiCaL version: 2.1.3 % 93.94/13.54 % (1113967)Termination reason: Instruction limit % 93.94/13.54 % (1113967)Termination phase: Saturation % 93.94/13.54 % (1113967)Time elapsed: 0.195 s % 93.94/13.54 % (1113967)Peak memory usage: 14 MB % 93.94/13.54 % (1113967)Instructions burned: 884 (million) % 93.94/13.54 % (1113971)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=4073957373:i=9515:nm=5_2992 on theBenchmark for (2992ds/9515Mi) % 93.94/13.54 % Detected minimum model sizes of [30] % 93.94/13.54 % Detected maximum model sizes of [max] % 93.94/13.54 % TRYING [30] % 93.94/13.54 % TRYING [14] % 93.94/13.54 % (1113963)Instruction limit reached! % 93.94/13.54 % (1113963)------------------------------ % 93.94/13.54 % (1113963)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 93.94/13.54 % (1113963)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 93.94/13.54 % (1113963)CaDiCaL version: 2.1.3 % 93.94/13.54 % (1113963)Termination reason: Instruction limit % 93.94/13.54 % (1113963)Termination phase: Finite model building constraint generation % 93.94/13.54 % (1113963)Time elapsed: 0.397 s % 93.94/13.54 % (1113963)Peak memory usage: 98 MB % 93.94/13.54 % (1113963)Instructions burned: 891 (million) % 93.94/13.54 % (1113973)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=785537358:fmbsr=1.7:i=920_2991 on theBenchmark for (2991ds/920Mi) % 93.94/13.54 % Detected minimum model sizes of [30] % 93.94/13.54 % Detected maximum model sizes of [max] % 93.94/13.54 % TRYING [30] % 93.94/13.54 % (1113965)Instruction limit reached! % 93.94/13.54 % (1113965)------------------------------ % 93.94/13.54 % (1113965)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 93.94/13.54 % (1113965)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 93.94/13.54 % (1113965)CaDiCaL version: 2.1.3 % 93.94/13.54 % (1113965)Termination reason: Instruction limit % 93.94/13.54 % (1113965)Termination phase: Saturation % 93.94/13.54 % (1113965)Time elapsed: 0.401 s % 93.94/13.54 % (1113965)Peak memory usage: 20 MB % 93.94/13.54 % (1113965)Instructions burned: 692 (million) % 93.94/13.54 % (1113975)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=136393323:i=5131_2990 on theBenchmark for (2990ds/5131Mi) % 93.94/13.54 % (1113973)Instruction limit reached! % 93.94/13.54 % (1113973)------------------------------ % 93.94/13.54 % (1113973)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 93.94/13.54 % (1113973)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 93.94/13.54 % (1113973)CaDiCaL version: 2.1.3 % 93.94/13.54 % (1113973)Termination reason: Instruction limit % 93.94/13.54 % (1113973)Termination phase: Finite model building constraint generation % 93.94/13.54 % (1113973)Time elapsed: 0.305 s % 93.94/13.54 % (1113973)Peak memory usage: 65 MB % 93.94/13.54 % (1113973)Instructions burned: 921 (million) % 93.94/13.54 % (1113977)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3416495654:i=1472:ins=7:fdi=8:gsp=on_2987 on theBenchmark for (2987ds/1472Mi) % 93.94/13.54 % (1113977)Instruction limit reached! % 93.94/13.54 % (1113977)------------------------------ % 93.94/13.54 % (1113977)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 93.94/13.54 % (1113977)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 93.94/13.54 % (1113977)CaDiCaL version: 2.1.3 % 93.94/13.54 % (1113977)Termination reason: Instruction limit % 93.94/13.54 % (1113977)Termination phase: Saturation % 93.94/13.54 % (1113977)Time elapsed: 0.672 s % 155.12/23.54 % (1113977)Peak memory usage: 22 MB % 155.12/23.54 % (1113977)Instructions burned: 1474 (million) % 155.12/23.54 % (1113979)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=454094530:i=6324_2981 on theBenchmark for (2981ds/6324Mi) % 155.12/23.54 % Detected minimum model sizes of [30] % 155.12/23.54 % Detected maximum model sizes of [max] % 155.12/23.54 % (1113979)Cannot represent all propositional literals internally % 155.12/23.54 % (1113979)Refutation not found, incomplete strategy % 155.12/23.54 % (1113979)------------------------------ % 155.12/23.54 % (1113979)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 155.12/23.54 % (1113979)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 155.12/23.54 % (1113979)CaDiCaL version: 2.1.3 % 155.12/23.54 % (1113979)Termination reason: Refutation not found, incomplete strategy % 155.12/23.54 % (1113979)Time elapsed: 0.007 s % 155.12/23.54 % (1113979)Peak memory usage: 10 MB % 155.12/23.54 % (1113979)Instructions burned: 15 (million) % 155.12/23.54 % (1113979)------------------------------ % 155.12/23.54 % (1113979)------------------------------ % 155.12/23.54 % (1113981)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=3446485630:fmbsr=2.30978:i=2174_2980 on theBenchmark for (2980ds/2174Mi) % 155.12/23.54 % Detected minimum model sizes of [30] % 155.12/23.54 % Detected maximum model sizes of [max] % 155.12/23.54 % TRYING [30] % 155.12/23.54 % (1113971)Instruction limit reached! % 155.12/23.54 % (1113971)------------------------------ % 155.12/23.54 % (1113971)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 155.12/23.54 % (1113971)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 155.12/23.54 % (1113971)CaDiCaL version: 2.1.3 % 155.12/23.54 % (1113971)Termination reason: Instruction limit % 155.12/23.54 % (1113971)Termination phase: Finite model building constraint generation % 155.12/23.54 % (1113971)Time elapsed: 1.815 s % 155.12/23.54 % (1113971)Peak memory usage: 577 MB % 155.12/23.54 % (1113971)Instructions burned: 9518 (million) % 155.12/23.54 % (1113983)ott-2_1_sil=16000:newcnf=on:random_seed=1525484845:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2973 on theBenchmark for (2973ds/869Mi) % 155.12/23.54 % (1113981)Instruction limit reached! % 155.12/23.54 % (1113981)------------------------------ % 155.12/23.54 % (1113981)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 155.12/23.54 % (1113981)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 155.12/23.54 % (1113981)CaDiCaL version: 2.1.3 % 155.12/23.54 % (1113981)Termination reason: Instruction limit % 155.12/23.54 % (1113981)Termination phase: Finite model building constraint generation % 155.12/23.54 % (1113981)Time elapsed: 0.767 s % 155.12/23.54 % (1113981)Peak memory usage: 152 MB % 155.12/23.54 % (1113981)Instructions burned: 2175 (million) % 155.12/23.54 % (1113985)ott+10_1_sil=32000:tgt=ground:random_seed=565727734:i=5114:av=off_2972 on theBenchmark for (2972ds/5114Mi) % 155.12/23.54 % (1113983)Instruction limit reached! % 155.12/23.54 % (1113983)------------------------------ % 155.12/23.54 % (1113983)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 155.12/23.54 % (1113983)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 155.12/23.54 % (1113983)CaDiCaL version: 2.1.3 % 155.12/23.54 % (1113983)Termination reason: Instruction limit % 155.12/23.54 % (1113983)Termination phase: Saturation % 155.12/23.54 % (1113983)Time elapsed: 0.253 s % 155.12/23.54 % (1113983)Peak memory usage: 21 MB % 155.12/23.54 % (1113983)Instructions burned: 870 (million) % 155.12/23.54 % (1113987)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=840353227:i=54282_2970 on theBenchmark for (2970ds/54282Mi) % 155.12/23.54 % Detected minimum model sizes of [30] % 155.12/23.54 % Detected maximum model sizes of [max] % 155.12/23.54 % TRYING [30] % 155.12/23.54 % (1113975)Instruction limit reached! % 155.12/23.54 % (1113975)------------------------------ % 155.12/23.54 % (1113975)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 155.12/23.54 % (1113975)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 155.12/23.54 % (1113975)CaDiCaL version: 2.1.3 % 155.12/23.54 % (1113975)Termination reason: Instruction limit % 155.12/23.54 % (1113975)Termination phase: Saturation % 155.12/23.54 % (1113975)Time elapsed: 2.690 s % 155.12/23.54 % (1113975)Peak memory usage: 39 MB % 155.12/23.54 % (1113975)Instructions burned: 5131 (million) % 155.12/23.54 % (1113989)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=4222277418:i=3512:aac=none_2963 on theBenchmark for (2963ds/3512Mi) % 155.12/23.54 % (1113989)Instruction limit reached! % 155.12/23.54 % (1113989)------------------------------ % 155.12/23.54 % (1113989)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 264.78/37.69 % (1113989)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 264.78/37.69 % (1113989)CaDiCaL version: 2.1.3 % 264.78/37.69 % (1113989)Termination reason: Instruction limit % 264.78/37.69 % (1113989)Termination phase: Saturation % 264.78/37.69 % (1113989)Time elapsed: 1.811 s % 264.78/37.69 % (1113989)Peak memory usage: 28 MB % 264.78/37.69 % (1113989)Instructions burned: 3514 (million) % 264.78/37.69 % (1113985)Instruction limit reached! % 264.78/37.69 % (1113985)------------------------------ % 264.78/37.69 % (1113985)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 264.78/37.69 % (1113985)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 264.78/37.69 % (1113985)CaDiCaL version: 2.1.3 % 264.78/37.69 % (1113985)Termination reason: Instruction limit % 264.78/37.69 % (1113985)Termination phase: Saturation % 264.78/37.69 % (1113985)Time elapsed: 2.740 s % 264.78/37.69 % (1113985)Peak memory usage: 89 MB % 264.78/37.69 % (1113985)Instructions burned: 5115 (million) % 264.78/37.69 % (1113991)dis+21_1_sil=32000:sas=cadical:random_seed=169559053:i=3773:amm=off_2945 on theBenchmark for (2945ds/3773Mi) % 264.78/37.69 % (1113993)ott+11_1_sil=16000:gs=on:random_seed=2277731453:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2945 on theBenchmark for (2945ds/2251Mi) % 264.78/37.69 % (1113993)Instruction limit reached! % 264.78/37.69 % (1113993)------------------------------ % 264.78/37.69 % (1113993)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 264.78/37.69 % (1113993)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 264.78/37.69 % (1113993)CaDiCaL version: 2.1.3 % 264.78/37.69 % (1113993)Termination reason: Instruction limit % 264.78/37.69 % (1113993)Termination phase: Saturation % 264.78/37.69 % (1113993)Time elapsed: 0.852 s % 264.78/37.69 % (1113993)Peak memory usage: 12 MB % 264.78/37.69 % (1113993)Instructions burned: 2253 (million) % 264.78/37.69 % (1113995)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=3065126229:fmbsr=1.6:i=67534_2936 on theBenchmark for (2936ds/67534Mi) % 264.78/37.69 % Detected minimum model sizes of [30] % 264.78/37.69 % Detected maximum model sizes of [max] % 264.78/37.69 % (1113991)Instruction limit reached! % 264.78/37.69 % (1113991)------------------------------ % 264.78/37.69 % (1113991)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 264.78/37.69 % (1113991)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 264.78/37.69 % (1113991)CaDiCaL version: 2.1.3 % 264.78/37.69 % (1113991)Termination reason: Instruction limit % 264.78/37.69 % (1113991)Termination phase: Saturation % 264.78/37.69 % (1113991)Time elapsed: 1.956 s % 264.78/37.69 % (1113991)Peak memory usage: 33 MB % 264.78/37.69 % (1113991)Instructions burned: 3775 (million) % 264.78/37.69 % (1113997)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=2949848155:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2925 on theBenchmark for (2925ds/4591Mi) % 264.78/37.69 % (1113997)Instruction limit reached! % 264.78/37.69 % (1113997)------------------------------ % 264.78/37.69 % (1113997)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 264.78/37.69 % (1113997)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 264.78/37.69 % (1113997)CaDiCaL version: 2.1.3 % 264.78/37.69 % (1113997)Termination reason: Instruction limit % 264.78/37.69 % (1113997)Termination phase: Saturation % 264.78/37.69 % (1113997)Time elapsed: 2.354 s % 264.78/37.69 % (1113997)Peak memory usage: 61 MB % 264.78/37.69 % (1113997)Instructions burned: 4591 (million) % 264.78/37.69 % (1113999)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=4112815689:i=29340_2901 on theBenchmark for (2901ds/29340Mi) % 264.78/37.69 % (1113969)Instruction limit reached! % 264.78/37.69 % (1113969)------------------------------ % 264.78/37.69 % (1113969)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 264.78/37.69 % (1113969)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 264.78/37.69 % (1113969)CaDiCaL version: 2.1.3 % 264.78/37.69 % (1113969)Termination reason: Instruction limit % 264.78/37.69 % (1113969)Termination phase: Finite model building constraint generation % 264.78/37.69 % (1113969)Time elapsed: 9.735 s % 264.78/37.69 % (1113969)Peak memory usage: 2134 MB % 264.78/37.69 % (1113969)Instructions burned: 22062 (million) % 264.78/37.69 % (1114001)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=4190119066:i=5211_2892 on theBenchmark for (2892ds/5211Mi) % 264.78/37.69 % (1113987)Instruction limit reached! % 264.78/37.69 % (1113987)------------------------------ % 264.78/37.69 % (Terminated % 300.30/42.64 % Vampire exiting %------------------------------------------------------------------------------