%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : TOP040+2 : TPTP v9.3.1. Released v3.4.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % Computer : n006.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.49s 42.74s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : TOP040+2 : TPTP v9.3.1. Released v3.4.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.09/0.17 % Computer : n006.cluster.edu % 0.09/0.17 % Model : x86_64 x86_64 % 0.09/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.17 % Memory : 8046.5625MB % 0.09/0.17 % OS : Linux 6.8.0-71-generic % 0.09/0.17 % CPULimit : 300 % 0.09/0.17 % WCLimit : 300 % 0.09/0.17 % DateTime : Mon Sep 28 19:01:10 UTC 2026 % 0.09/0.17 % CPUTime : % 0.09/0.18 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.09/0.20 Running first-order model finding % 0.09/0.20 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 % 16.72/2.73 % (61070)Will run a generic schedule for satisfiability detection. % 16.72/2.73 % (61076)% WARNING: option uhcvi not known. % 16.72/2.73 % (61076)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2013418820:i=135531:add=off:rawr=on_2998 on theBenchmark for (2998ds/135531Mi) % 16.72/2.73 % (61075)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2399171223_2998 on theBenchmark for (2998ds/0Mi) % 16.72/2.73 % (61077)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3032281990:i=88024:add=on:rawr=on_2998 on theBenchmark for (2998ds/88024Mi) % 16.72/2.73 % (61078)dis+10_1_sil=32000:sp=arity:random_seed=4102828146:i=103:fgj=on_2998 on theBenchmark for (2998ds/103Mi) % 16.72/2.73 % (61079)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3315096273:i=116_2998 on theBenchmark for (2998ds/116Mi) % 16.72/2.73 % (61080)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2764811651:i=131_2998 on theBenchmark for (2998ds/131Mi) % 16.72/2.73 % (61081)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2414877176:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2998 on theBenchmark for (2998ds/159Mi) % 16.72/2.73 % (61078)Instruction limit reached! % 16.72/2.73 % (61078)------------------------------ % 16.72/2.73 % (61078)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 16.72/2.73 % (61078)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.72/2.73 % (61078)CaDiCaL version: 2.1.3 % 16.72/2.73 % (61078)Termination reason: Instruction limit % 16.72/2.73 % (61078)Termination phase: Preprocessing 3 % 16.72/2.73 % (61078)Time elapsed: 0.069 s % 16.72/2.73 % (61078)Peak memory usage: 21 MB % 16.72/2.73 % (61078)Instructions burned: 105 (million) % 16.72/2.73 % (61079)Instruction limit reached! % 16.72/2.73 % (61079)------------------------------ % 16.72/2.73 % (61079)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 16.72/2.73 % (61079)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.72/2.73 % (61079)CaDiCaL version: 2.1.3 % 16.72/2.73 % (61079)Termination reason: Instruction limit % 16.72/2.73 % (61079)Termination phase: NewCNF % 16.72/2.73 % (61079)Time elapsed: 0.076 s % 16.72/2.73 % (61079)Peak memory usage: 22 MB % 16.72/2.73 % (61079)Instructions burned: 118 (million) % 16.72/2.73 % (61080)Instruction limit reached! % 16.72/2.73 % (61080)------------------------------ % 16.72/2.73 % (61080)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 16.72/2.73 % (61080)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.72/2.73 % (61080)CaDiCaL version: 2.1.3 % 16.72/2.73 % (61080)Termination reason: Instruction limit % 16.72/2.73 % (61080)Termination phase: Preprocessing 3 % 16.72/2.73 % (61080)Time elapsed: 0.084 s % 16.72/2.73 % (61080)Peak memory usage: 22 MB % 16.72/2.73 % (61080)Instructions burned: 131 (million) % 16.72/2.73 % (61089)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3944401579:i=714:nm=2_2997 on theBenchmark for (2997ds/714Mi) % 16.72/2.73 % (61090)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2374077012:i=131:bd=preordered:fsd=on_2997 on theBenchmark for (2997ds/131Mi) % 16.72/2.73 % (61091)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=655999247:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2997 on theBenchmark for (2997ds/684Mi) % 16.72/2.73 % (61081)Instruction limit reached! % 16.72/2.73 % (61081)------------------------------ % 16.72/2.73 % (61081)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 16.72/2.73 % (61081)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.72/2.73 % (61081)CaDiCaL version: 2.1.3 % 16.72/2.73 % (61081)Termination reason: Instruction limit % 16.72/2.73 % (61081)Termination phase: Property scanning % 16.72/2.73 % (61081)Time elapsed: 0.108 s % 16.72/2.73 % (61081)Peak memory usage: 24 MB % 16.72/2.73 % (61081)Instructions burned: 159 (million) % 16.72/2.73 % (61095)ott-21_1_sil=16000:fs=off:random_seed=2654493539:i=180:av=off:fsr=off_2997 on theBenchmark for (2997ds/180Mi) % 16.72/2.73 % (61090)Instruction limit reached! % 16.72/2.73 % (61090)------------------------------ % 16.72/2.73 % (61090)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 16.72/2.73 % (61090)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.72/2.73 % (61090)CaDiCaL version: 2.1.3 % 16.72/2.73 % (61090)Termination reason: Instruction limit % 16.72/2.73 % (61090)Termination phase: Preprocessing 3 % 48.73/7.25 % (61090)Time elapsed: 0.089 s % 48.73/7.25 % (61090)Peak memory usage: 22 MB % 48.73/7.25 % (61090)Instructions burned: 133 (million) % 48.73/7.25 % (61097)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1931171254:i=477:bd=all_2996 on theBenchmark for (2996ds/477Mi) % 48.73/7.25 % (61095)Instruction limit reached! % 48.73/7.25 % (61095)------------------------------ % 48.73/7.25 % (61095)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 48.73/7.25 % (61095)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 48.73/7.25 % (61095)CaDiCaL version: 2.1.3 % 48.73/7.25 % (61095)Termination reason: Instruction limit % 48.73/7.25 % (61095)Termination phase: Property scanning % 48.73/7.25 % (61095)Time elapsed: 0.108 s % 48.73/7.25 % (61095)Peak memory usage: 24 MB % 48.73/7.25 % (61095)Instructions burned: 181 (million) % 48.73/7.25 % (61099)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2128811711:fmbsr=1.3:i=865:ins=25_2995 on theBenchmark for (2995ds/865Mi) % 48.73/7.25 % (61091)Instruction limit reached! % 48.73/7.25 % (61091)------------------------------ % 48.73/7.25 % (61091)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 48.73/7.25 % (61091)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 48.73/7.25 % (61091)CaDiCaL version: 2.1.3 % 48.73/7.25 % (61091)Termination reason: Instruction limit % 48.73/7.25 % (61091)Termination phase: Saturation % 48.73/7.25 % (61091)Time elapsed: 0.349 s % 48.73/7.25 % (61091)Peak memory usage: 30 MB % 48.73/7.25 % (61091)Instructions burned: 684 (million) % 48.73/7.25 % (61089)Instruction limit reached! % 48.73/7.25 % (61089)------------------------------ % 48.73/7.25 % (61089)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 48.73/7.25 % (61089)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 48.73/7.25 % (61089)CaDiCaL version: 2.1.3 % 48.73/7.25 % (61089)Termination reason: Instruction limit % 48.73/7.25 % (61089)Termination phase: Finite model building preprocessing % 48.73/7.25 % (61089)Time elapsed: 0.365 s % 48.73/7.25 % (61089)Peak memory usage: 35 MB % 48.73/7.25 % (61089)Instructions burned: 714 (million) % 48.73/7.25 % (61097)Instruction limit reached! % 48.73/7.25 % (61097)------------------------------ % 48.73/7.25 % (61097)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 48.73/7.25 % (61097)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 48.73/7.25 % (61097)CaDiCaL version: 2.1.3 % 48.73/7.25 % (61097)Termination reason: Instruction limit % 48.73/7.25 % (61097)Termination phase: Saturation % 48.73/7.25 % (61097)Time elapsed: 0.253 s % 48.73/7.25 % (61097)Peak memory usage: 28 MB % 48.73/7.25 % (61097)Instructions burned: 478 (million) % 48.73/7.25 % (61101)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=287131714:i=1179_2993 on theBenchmark for (2993ds/1179Mi) % 48.73/7.25 % (61102)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1412344416:i=889:ins=1_2993 on theBenchmark for (2993ds/889Mi) % 48.73/7.25 % (61103)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=1817665338:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2993 on theBenchmark for (2993ds/692Mi) % 48.73/7.25 % (61099)Instruction limit reached! % 48.73/7.25 % (61099)------------------------------ % 48.73/7.25 % (61099)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 48.73/7.25 % (61099)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 48.73/7.25 % (61099)CaDiCaL version: 2.1.3 % 48.73/7.25 % (61099)Termination reason: Instruction limit % 48.73/7.25 % (61099)Termination phase: Finite model building preprocessing % 48.73/7.25 % (61099)Time elapsed: 0.424 s % 48.73/7.25 % (61099)Peak memory usage: 34 MB % 48.73/7.25 % (61099)Instructions burned: 866 (million) % 48.73/7.25 % (61107)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2705039297:i=879:kws=inv_precedence:fsr=off_2991 on theBenchmark for (2991ds/879Mi) % 48.73/7.25 % (61103)Instruction limit reached! % 48.73/7.25 % (61103)------------------------------ % 48.73/7.25 % (61103)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 48.73/7.25 % (61103)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 48.73/7.25 % (61103)CaDiCaL version: 2.1.3 % 48.73/7.25 % (61103)Termination reason: Instruction limit % 48.73/7.25 % (61103)Termination phase: Saturation % 48.73/7.25 % (61103)Time elapsed: 0.363 s % 48.73/7.25 % (61103)Peak memory usage: 32 MB % 48.73/7.25 % (61103)Instructions burned: 693 (million) % 101.91/14.74 % (61109)fmb+10_1_sil=64000:random_seed=2173026918:i=22061:nm=2:gsp=on_2989 on theBenchmark for (2989ds/22061Mi) % 101.91/14.74 % (61102)Instruction limit reached! % 101.91/14.74 % (61102)------------------------------ % 101.91/14.74 % (61102)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 101.91/14.74 % (61102)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 101.91/14.74 % (61102)CaDiCaL version: 2.1.3 % 101.91/14.74 % (61102)Termination reason: Instruction limit % 101.91/14.74 % (61102)Termination phase: Finite model building preprocessing % 101.91/14.74 % (61102)Time elapsed: 0.440 s % 101.91/14.74 % (61102)Peak memory usage: 34 MB % 101.91/14.74 % (61102)Instructions burned: 891 (million) % 101.91/14.74 % (61111)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2475047666:i=9515:nm=5_2989 on theBenchmark for (2989ds/9515Mi) % 101.91/14.74 % (61101)Instruction limit reached! % 101.91/14.74 % (61101)------------------------------ % 101.91/14.74 % (61101)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 101.91/14.74 % (61101)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 101.91/14.74 % (61101)CaDiCaL version: 2.1.3 % 101.91/14.74 % (61101)Termination reason: Instruction limit % 101.91/14.74 % (61101)Termination phase: Saturation % 101.91/14.74 % (61101)Time elapsed: 0.637 s % 101.91/14.74 % (61101)Peak memory usage: 41 MB % 101.91/14.74 % (61101)Instructions burned: 1179 (million) % 101.91/14.74 % (61107)Instruction limit reached! % 101.91/14.74 % (61107)------------------------------ % 101.91/14.74 % (61107)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 101.91/14.74 % (61107)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 101.91/14.74 % (61107)CaDiCaL version: 2.1.3 % 101.91/14.74 % (61107)Termination reason: Instruction limit % 101.91/14.74 % (61107)Termination phase: Saturation % 101.91/14.74 % (61107)Time elapsed: 0.428 s % 101.91/14.74 % (61107)Peak memory usage: 37 MB % 101.91/14.74 % (61107)Instructions burned: 881 (million) % 101.91/14.74 % (61113)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=695384686:fmbsr=1.7:i=920_2987 on theBenchmark for (2987ds/920Mi) % 101.91/14.74 % (61115)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2334551264:i=5131_2986 on theBenchmark for (2986ds/5131Mi) % 101.91/14.74 % Detected minimum model sizes of [5] % 101.91/14.74 % Detected maximum model sizes of [max] % 101.91/14.74 % TRYING [5] % 101.91/14.74 % (61113)Instruction limit reached! % 101.91/14.74 % (61113)------------------------------ % 101.91/14.74 % (61113)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 101.91/14.74 % (61113)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 101.91/14.74 % (61113)CaDiCaL version: 2.1.3 % 101.91/14.74 % (61113)Termination reason: Instruction limit % 101.91/14.74 % (61113)Termination phase: Finite model building preprocessing % 101.91/14.74 % (61113)Time elapsed: 0.453 s % 101.91/14.74 % (61113)Peak memory usage: 34 MB % 101.91/14.74 % (61113)Instructions burned: 922 (million) % 101.91/14.74 % (61117)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1456919540:i=1472:ins=7:fdi=8:gsp=on_2982 on theBenchmark for (2982ds/1472Mi) % 101.91/14.74 % Detected minimum model sizes of [5] % 101.91/14.74 % Detected maximum model sizes of [max] % 101.91/14.74 % Detected minimum model sizes of [5] % 101.91/14.74 % Detected maximum model sizes of [max] % 101.91/14.74 % (61111)Cannot represent all propositional literals internally % 101.91/14.74 % (61111)Refutation not found, incomplete strategy % 101.91/14.74 % (61111)------------------------------ % 101.91/14.74 % (61111)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 101.91/14.74 % (61111)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 101.91/14.74 % (61111)CaDiCaL version: 2.1.3 % 101.91/14.74 % (61111)Termination reason: Refutation not found, incomplete strategy % 101.91/14.74 % (61111)Time elapsed: 1.259 s % 101.91/14.74 % (61111)Peak memory usage: 60 MB % 101.91/14.74 % (61111)Instructions burned: 2556 (million) % 101.91/14.74 % (61111)------------------------------ % 101.91/14.74 % (61111)------------------------------ % 101.91/14.74 % (61119)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3803701251:i=6324_2976 on theBenchmark for (2976ds/6324Mi) % 101.91/14.74 % (61117)Instruction limit reached! % 101.91/14.74 % (61117)------------------------------ % 101.91/14.74 % (61117)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 101.91/14.74 % (61117)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 101.91/14.74 % (61117)CaDiCaL version: 2.1.3 % 101.91/14.74 % (61117)Termination reason: Instruction limit % 190.63/27.94 % (61117)Termination phase: Saturation % 190.63/27.94 % (61117)Time elapsed: 0.736 s % 190.63/27.94 % (61117)Peak memory usage: 35 MB % 190.63/27.94 % (61117)Instructions burned: 1472 (million) % 190.63/27.94 % (61121)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1255533364:fmbsr=2.30978:i=2174_2974 on theBenchmark for (2974ds/2174Mi) % 190.63/27.94 % (61121)Instruction limit reached! % 190.63/27.94 % (61121)------------------------------ % 190.63/27.94 % (61121)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 190.63/27.94 % (61121)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 190.63/27.94 % (61121)CaDiCaL version: 2.1.3 % 190.63/27.94 % (61121)Termination reason: Instruction limit % 190.63/27.94 % (61121)Termination phase: Finite model building preprocessing % 190.63/27.94 % (61121)Time elapsed: 1.032 s % 190.63/27.94 % (61121)Peak memory usage: 49 MB % 190.63/27.94 % (61121)Instructions burned: 2176 (million) % 190.63/27.94 % (61123)ott-2_1_sil=16000:newcnf=on:random_seed=3763922266:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2964 on theBenchmark for (2964ds/869Mi) % 190.63/27.94 % Detected minimum model sizes of [5] % 190.63/27.94 % Detected maximum model sizes of [max] % 190.63/27.94 % (61119)Cannot represent all propositional literals internally % 190.63/27.94 % (61119)Refutation not found, incomplete strategy % 190.63/27.94 % (61119)------------------------------ % 190.63/27.94 % (61119)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 190.63/27.94 % (61119)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 190.63/27.94 % (61119)CaDiCaL version: 2.1.3 % 190.63/27.94 % (61119)Termination reason: Refutation not found, incomplete strategy % 190.63/27.94 % (61119)Time elapsed: 1.505 s % 190.63/27.94 % (61119)Peak memory usage: 64 MB % 190.63/27.94 % (61119)Instructions burned: 3017 (million) % 190.63/27.94 % (61119)------------------------------ % 190.63/27.94 % (61119)------------------------------ % 190.63/27.94 % (61125)ott+10_1_sil=32000:tgt=ground:random_seed=881057628:i=5114:av=off_2960 on theBenchmark for (2960ds/5114Mi) % 190.63/27.94 % (61123)Instruction limit reached! % 190.63/27.94 % (61123)------------------------------ % 190.63/27.94 % (61123)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 190.63/27.94 % (61123)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 190.63/27.94 % (61123)CaDiCaL version: 2.1.3 % 190.63/27.94 % (61123)Termination reason: Instruction limit % 190.63/27.94 % (61123)Termination phase: Saturation % 190.63/27.94 % (61123)Time elapsed: 0.436 s % 190.63/27.94 % (61123)Peak memory usage: 33 MB % 190.63/27.94 % (61123)Instructions burned: 869 (million) % 190.63/27.94 % (61127)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=1570186984:i=54282_2959 on theBenchmark for (2959ds/54282Mi) % 190.63/27.94 % (61115)Instruction limit reached! % 190.63/27.94 % (61115)------------------------------ % 190.63/27.94 % (61115)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 190.63/27.94 % (61115)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 190.63/27.94 % (61115)CaDiCaL version: 2.1.3 % 190.63/27.94 % (61115)Termination reason: Instruction limit % 190.63/27.94 % (61115)Termination phase: Saturation % 190.63/27.94 % (61115)Time elapsed: 2.975 s % 190.63/27.94 % (61115)Peak memory usage: 67 MB % 190.63/27.94 % (61115)Instructions burned: 5132 (million) % 190.63/27.94 % (61129)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3480816892:i=3512:aac=none_2956 on theBenchmark for (2956ds/3512Mi) % 190.63/27.94 % Detected minimum model sizes of [5] % 190.63/27.94 % Detected maximum model sizes of [max] % 190.63/27.94 % TRYING [5] % 190.63/27.94 % (61129)Instruction limit reached! % 190.63/27.94 % (61129)------------------------------ % 190.63/27.94 % (61129)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 190.63/27.94 % (61129)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 190.63/27.94 % (61129)CaDiCaL version: 2.1.3 % 190.63/27.94 % (61129)Termination reason: Instruction limit % 190.63/27.94 % (61129)Termination phase: Saturation % 190.63/27.94 % (61129)Time elapsed: 1.940 s % 190.63/27.94 % (61129)Peak memory usage: 54 MB % 190.63/27.94 % (61129)Instructions burned: 3512 (million) % 190.63/27.94 % (61131)dis+21_1_sil=32000:sas=cadical:random_seed=3136352473:i=3773:amm=off_2937 on theBenchmark for (2937ds/3773Mi) % 190.63/27.94 % (61125)Instruction limit reached! % 190.63/27.94 % (61125)------------------------------ % 190.63/27.94 % (61125)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 190.63/27.94 % (61125)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 190.63/27.94 % (61125)CaTerminated % 300.49/42.74 % Vampire exiting % 300.49/42.74 Terminated %------------------------------------------------------------------------------