%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWW443-1 : TPTP v9.3.1. Released v5.2.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % Computer : n009.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:40:02 PM UTC 2026 % Result : Timeout 300.20s 42.63s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : SWW443-1 : TPTP v9.3.1. Released v5.2.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.08/0.17 % Computer : n009.cluster.edu % 0.08/0.17 % Model : x86_64 x86_64 % 0.08/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.08/0.17 % Memory : 8046.5625MB % 0.08/0.17 % OS : Linux 6.8.0-71-generic % 0.08/0.17 % CPULimit : 300 % 0.08/0.17 % WCLimit : 300 % 0.08/0.17 % DateTime : Mon Sep 28 13:55:45 UTC 2026 % 0.08/0.18 % CPUTime : % 0.08/0.18 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.08/0.21 Running first-order model finding % 0.08/0.21 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 % 8.33/1.57 % (3036017)Will run a generic schedule for satisfiability detection. % 8.33/1.57 % (3036027)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2850365916:i=131_2999 on theBenchmark for (2999ds/131Mi) % 8.33/1.57 % (3036023)% WARNING: option uhcvi not known. % 8.33/1.57 % (3036022)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3851717765_2999 on theBenchmark for (2999ds/0Mi) % 8.33/1.57 % (3036026)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3186073577:i=116_2999 on theBenchmark for (2999ds/116Mi) % 8.33/1.57 % (3036023)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2838622879:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 8.33/1.57 % (3036024)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=415277355:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 8.33/1.57 % (3036025)dis+10_1_sil=32000:sp=arity:random_seed=307372914:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 8.33/1.57 % (3036028)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3476118461:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 8.33/1.57 % Detected minimum model sizes of [3] % 8.33/1.57 % Detected maximum model sizes of [max] % 8.33/1.57 % TRYING [3] % 8.33/1.57 % (3036027)Instruction limit reached! % 8.33/1.57 % (3036027)------------------------------ % 8.33/1.57 % (3036027)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.33/1.57 % (3036027)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.33/1.57 % (3036027)CaDiCaL version: 2.1.3 % 8.33/1.57 % (3036027)Termination reason: Instruction limit % 8.33/1.57 % (3036027)Termination phase: Saturation % 8.33/1.57 % (3036027)Time elapsed: 0.031 s % 8.33/1.57 % (3036027)Peak memory usage: 11 MB % 8.33/1.57 % (3036027)Instructions burned: 132 (million) % 8.33/1.57 % TRYING [4] % 8.33/1.57 % (3036036)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3055681206:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 8.33/1.57 % Detected minimum model sizes of [3] % 8.33/1.57 % Detected maximum model sizes of [max] % 8.33/1.57 % TRYING [3] % 8.33/1.57 % (3036026)Instruction limit reached! % 8.33/1.57 % (3036026)------------------------------ % 8.33/1.57 % (3036026)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.33/1.57 % (3036026)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.33/1.57 % (3036026)CaDiCaL version: 2.1.3 % 8.33/1.57 % (3036026)Termination reason: Instruction limit % 8.33/1.57 % (3036026)Termination phase: Saturation % 8.33/1.57 % (3036026)Time elapsed: 0.056 s % 8.33/1.57 % (3036026)Peak memory usage: 12 MB % 8.33/1.57 % (3036026)Instructions burned: 117 (million) % 8.33/1.57 % (3036025)Instruction limit reached! % 8.33/1.57 % (3036025)------------------------------ % 8.33/1.57 % (3036025)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.33/1.57 % (3036025)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.33/1.57 % (3036025)CaDiCaL version: 2.1.3 % 8.33/1.57 % (3036025)Termination reason: Instruction limit % 8.33/1.57 % (3036025)Termination phase: Saturation % 8.33/1.57 % (3036025)Time elapsed: 0.061 s % 8.33/1.57 % (3036025)Peak memory usage: 12 MB % 8.33/1.57 % (3036025)Instructions burned: 103 (million) % 8.33/1.57 % TRYING [4] % 8.33/1.57 % (3036038)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2706448977:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 8.33/1.58 % (3036039)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=2075933353:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi) % 8.33/1.58 % (3036028)Instruction limit reached! % 8.33/1.58 % (3036028)------------------------------ % 8.33/1.58 % (3036028)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.33/1.58 % (3036028)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.33/1.58 % (3036028)CaDiCaL version: 2.1.3 % 8.33/1.58 % (3036028)Termination reason: Instruction limit % 8.33/1.58 % (3036028)Termination phase: Saturation % 8.33/1.58 % (3036028)Time elapsed: 0.090 s % 8.33/1.58 % (3036028)Peak memory usage: 12 MB % 8.33/1.58 % (3036028)Instructions burned: 160 (million) % 8.33/1.58 % (3036042)ott-21_1_sil=16000:fs=off:random_seed=1617400812:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 8.33/1.58 % (3036038)Instruction limit reached! % 8.33/1.58 % (3036038)------------------------------ % 38.83/5.71 % (3036038)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 38.83/5.71 % (3036038)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 38.83/5.71 % (3036038)CaDiCaL version: 2.1.3 % 38.83/5.71 % (3036038)Termination reason: Instruction limit % 38.83/5.71 % (3036038)Termination phase: Saturation % 38.83/5.71 % (3036038)Time elapsed: 0.065 s % 38.83/5.71 % (3036038)Peak memory usage: 12 MB % 38.83/5.71 % (3036038)Instructions burned: 131 (million) % 38.83/5.71 % (3036044)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2514176540:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 38.83/5.71 % (3036042)Instruction limit reached! % 38.83/5.71 % (3036042)------------------------------ % 38.83/5.71 % (3036042)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 38.83/5.71 % (3036042)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 38.83/5.71 % (3036042)CaDiCaL version: 2.1.3 % 38.83/5.71 % (3036042)Termination reason: Instruction limit % 38.83/5.71 % (3036042)Termination phase: Saturation % 38.83/5.71 % (3036042)Time elapsed: 0.070 s % 38.83/5.71 % (3036042)Peak memory usage: 11 MB % 38.83/5.71 % (3036042)Instructions burned: 184 (million) % 38.83/5.71 % (3036046)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=572707935:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi) % 38.83/5.71 % Detected minimum model sizes of [3] % 38.83/5.71 % Detected maximum model sizes of [max] % 38.83/5.71 % TRYING [3] % 38.83/5.71 % (3036036)Instruction limit reached! % 38.83/5.71 % (3036036)------------------------------ % 38.83/5.71 % (3036036)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 38.83/5.71 % (3036036)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 38.83/5.71 % (3036036)CaDiCaL version: 2.1.3 % 38.83/5.71 % (3036036)Termination reason: Instruction limit % 38.83/5.71 % (3036036)Termination phase: Finite model building SAT solving % 38.83/5.71 % (3036036)Time elapsed: 0.213 s % 38.83/5.71 % (3036036)Peak memory usage: 19 MB % 38.83/5.71 % (3036036)Instructions burned: 716 (million) % 38.83/5.71 % TRYING [4] % 38.83/5.71 % (3036048)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=143481029:i=1179_2997 on theBenchmark for (2997ds/1179Mi) % 38.83/5.71 % (3036044)Instruction limit reached! % 38.83/5.71 % (3036044)------------------------------ % 38.83/5.71 % (3036044)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 38.83/5.71 % (3036044)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 38.83/5.71 % (3036044)CaDiCaL version: 2.1.3 % 38.83/5.71 % (3036044)Termination reason: Instruction limit % 38.83/5.71 % (3036044)Termination phase: Saturation % 38.83/5.71 % (3036044)Time elapsed: 0.233 s % 38.83/5.71 % (3036044)Peak memory usage: 13 MB % 38.83/5.71 % (3036044)Instructions burned: 478 (million) % 38.83/5.71 % (3036039)Instruction limit reached! % 38.83/5.71 % (3036039)------------------------------ % 38.83/5.71 % (3036039)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 38.83/5.71 % (3036039)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 38.83/5.71 % (3036039)CaDiCaL version: 2.1.3 % 38.83/5.71 % (3036039)Termination reason: Instruction limit % 38.83/5.71 % (3036039)Termination phase: Saturation % 38.83/5.71 % (3036039)Time elapsed: 0.322 s % 38.83/5.71 % (3036039)Peak memory usage: 15 MB % 38.83/5.71 % (3036039)Instructions burned: 686 (million) % 38.83/5.71 % (3036050)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=215408442:i=889:ins=1_2995 on theBenchmark for (2995ds/889Mi) % 38.83/5.71 % (3036051)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=2585132047: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) % 38.83/5.71 % (3036048)Instruction limit reached! % 38.83/5.71 % (3036048)------------------------------ % 38.83/5.71 % (3036048)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 38.83/5.71 % (3036048)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 38.83/5.71 % (3036048)CaDiCaL version: 2.1.3 % 38.83/5.71 % (3036048)Termination reason: Instruction limit % 38.83/5.71 % (3036048)Termination phase: Saturation % 38.83/5.71 % (3036048)Time elapsed: 0.267 s % 38.83/5.71 % (3036048)Peak memory usage: 14 MB % 38.83/5.71 % (3036048)Instructions burned: 1180 (million) % 38.83/5.71 % (3036054)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3161493686:i=879:kws=inv_precedence:fsr=off_2994 on theBenchmark for (2994ds/879Mi) % 111.18/15.91 % TRYING [14] % 111.18/15.91 % (3036046)Instruction limit reached! % 111.18/15.91 % (3036046)------------------------------ % 111.18/15.91 % (3036046)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 111.18/15.91 % (3036046)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 111.18/15.91 % (3036046)CaDiCaL version: 2.1.3 % 111.18/15.91 % (3036046)Termination reason: Instruction limit % 111.18/15.91 % (3036046)Termination phase: Finite model building SAT solving % 111.18/15.91 % (3036046)Time elapsed: 0.470 s % 111.18/15.91 % (3036046)Peak memory usage: 15 MB % 111.18/15.91 % (3036046)Instructions burned: 865 (million) % 111.18/15.91 % (3036056)fmb+10_1_sil=64000:random_seed=3894052772:i=22061:nm=2:gsp=on_2992 on theBenchmark for (2992ds/22061Mi) % 111.18/15.91 % Detected minimum model sizes of [3] % 111.18/15.91 % Detected maximum model sizes of [max] % 111.18/15.91 % TRYING [3] % 111.18/15.91 % (3036051)Instruction limit reached! % 111.18/15.91 % (3036051)------------------------------ % 111.18/15.91 % (3036051)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 111.18/15.91 % (3036051)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 111.18/15.91 % (3036051)CaDiCaL version: 2.1.3 % 111.18/15.91 % (3036051)Termination reason: Instruction limit % 111.18/15.91 % (3036051)Termination phase: Saturation % 111.18/15.91 % (3036051)Time elapsed: 0.284 s % 111.18/15.91 % (3036051)Peak memory usage: 13 MB % 111.18/15.91 % (3036051)Instructions burned: 693 (million) % 111.18/15.91 % (3036058)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3829323492:i=9515:nm=5_2992 on theBenchmark for (2992ds/9515Mi) % 111.18/15.91 % Detected minimum model sizes of [3] % 111.18/15.91 % Detected maximum model sizes of [max] % 111.18/15.91 % TRYING [20] % 111.18/15.91 % TRYING [4] % 111.18/15.91 % (3036054)Instruction limit reached! % 111.18/15.91 % (3036054)------------------------------ % 111.18/15.91 % (3036054)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 111.18/15.91 % (3036054)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 111.18/15.91 % (3036054)CaDiCaL version: 2.1.3 % 111.18/15.91 % (3036054)Termination reason: Instruction limit % 111.18/15.91 % (3036054)Termination phase: Saturation % 111.18/15.91 % (3036054)Time elapsed: 0.228 s % 111.18/15.91 % (3036054)Peak memory usage: 16 MB % 111.18/15.91 % (3036054)Instructions burned: 881 (million) % 111.18/15.91 % (3036050)Instruction limit reached! % 111.18/15.91 % (3036050)------------------------------ % 111.18/15.91 % (3036050)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 111.18/15.91 % (3036050)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 111.18/15.91 % (3036050)CaDiCaL version: 2.1.3 % 111.18/15.91 % (3036050)Termination reason: Instruction limit % 111.18/15.91 % (3036050)Termination phase: Finite model building constraint generation % 111.18/15.91 % (3036050)Time elapsed: 0.362 s % 111.18/15.91 % (3036050)Peak memory usage: 91 MB % 111.18/15.91 % (3036050)Instructions burned: 890 (million) % 111.18/15.91 % (3036060)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1668423175:fmbsr=1.7:i=920_2991 on theBenchmark for (2991ds/920Mi) % 111.18/15.91 % Detected minimum model sizes of [3] % 111.18/15.91 % Detected maximum model sizes of [max] % 111.18/15.91 % TRYING [8] % 111.18/15.91 % (3036062)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1215822940:i=5131_2991 on theBenchmark for (2991ds/5131Mi) % 111.18/15.91 % TRYING [5] % 111.18/15.91 % (3036060)Instruction limit reached! % 111.18/15.91 % (3036060)------------------------------ % 111.18/15.91 % (3036060)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 111.18/15.91 % (3036060)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 111.18/15.91 % (3036060)CaDiCaL version: 2.1.3 % 111.18/15.91 % (3036060)Termination reason: Instruction limit % 111.18/15.91 % (3036060)Termination phase: Finite model building constraint generation % 111.18/15.91 % (3036060)Time elapsed: 0.194 s % 111.18/15.91 % (3036060)Peak memory usage: 73 MB % 111.18/15.91 % (3036060)Instructions burned: 923 (million) % 111.18/15.91 % (3036064)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=558409683:i=1472:ins=7:fdi=8:gsp=on_2989 on theBenchmark for (2989ds/1472Mi) % 111.18/15.91 % (3036064)Instruction limit reached! % 111.18/15.91 % (3036064)------------------------------ % 111.18/15.91 % (3036064)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 111.18/15.91 % (3036064)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 111.18/15.91 % (3036064)CaDiCaL version: 2.1.3 % 111.18/15.91 % (3036064)Termination reason: Instruction limit % 111.18/15.91 % (3036064)Termination phase: Saturation % 190.15/27.04 % (3036064)Time elapsed: 0.330 s % 190.15/27.04 % (3036064)Peak memory usage: 21 MB % 190.15/27.04 % (3036064)Instructions burned: 1476 (million) % 190.15/27.04 % (3036066)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=2877570243:i=6324_2986 on theBenchmark for (2986ds/6324Mi) % 190.15/27.04 % Detected minimum model sizes of [3] % 190.15/27.04 % Detected maximum model sizes of [max] % 190.15/27.04 % TRYING [77] % 190.15/27.04 % TRYING [5] % 190.15/27.04 % (3036066)Instruction limit reached! % 190.15/27.04 % (3036066)------------------------------ % 190.15/27.04 % (3036066)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 190.15/27.04 % (3036066)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 190.15/27.04 % (3036066)CaDiCaL version: 2.1.3 % 190.15/27.04 % (3036066)Termination reason: Instruction limit % 190.15/27.04 % (3036066)Termination phase: Finite model building constraint generation % 190.15/27.04 % (3036066)Time elapsed: 1.304 s % 190.15/27.04 % (3036066)Peak memory usage: 514 MB % 190.15/27.04 % (3036066)Instructions burned: 6324 (million) % 190.15/27.04 % (3036068)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=3803646636:fmbsr=2.30978:i=2174_2972 on theBenchmark for (2972ds/2174Mi) % 190.15/27.04 % Detected minimum model sizes of [3] % 190.15/27.04 % Detected maximum model sizes of [max] % 190.15/27.04 % TRYING [16] % 190.15/27.04 % (3036068)Instruction limit reached! % 190.15/27.04 % (3036068)------------------------------ % 190.15/27.04 % (3036068)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 190.15/27.04 % (3036068)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 190.15/27.04 % (3036068)CaDiCaL version: 2.1.3 % 190.15/27.04 % (3036068)Termination reason: Instruction limit % 190.15/27.04 % (3036068)Termination phase: Finite model building constraint generation % 190.15/27.04 % (3036068)Time elapsed: 0.414 s % 190.15/27.04 % (3036068)Peak memory usage: 135 MB % 190.15/27.04 % (3036068)Instructions burned: 2175 (million) % 190.15/27.04 % (3036070)ott-2_1_sil=16000:newcnf=on:random_seed=334459788:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2968 on theBenchmark for (2968ds/869Mi) % 190.15/27.04 % (3036062)Instruction limit reached! % 190.15/27.04 % (3036062)------------------------------ % 190.15/27.04 % (3036062)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 190.15/27.04 % (3036062)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 190.15/27.04 % (3036062)CaDiCaL version: 2.1.3 % 190.15/27.04 % (3036062)Termination reason: Instruction limit % 190.15/27.04 % (3036062)Termination phase: Saturation % 190.15/27.04 % (3036062)Time elapsed: 2.489 s % 190.15/27.04 % (3036062)Peak memory usage: 31 MB % 190.15/27.04 % (3036062)Instructions burned: 5131 (million) % 190.15/27.04 % (3036072)ott+10_1_sil=32000:tgt=ground:random_seed=3201605009:i=5114:av=off_2966 on theBenchmark for (2966ds/5114Mi) % 190.15/27.04 % (3036070)Instruction limit reached! % 190.15/27.04 % (3036070)------------------------------ % 190.15/27.04 % (3036070)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 190.15/27.04 % (3036070)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 190.15/27.04 % (3036070)CaDiCaL version: 2.1.3 % 190.15/27.04 % (3036070)Termination reason: Instruction limit % 190.15/27.04 % (3036070)Termination phase: Saturation % 190.15/27.04 % (3036070)Time elapsed: 0.197 s % 190.15/27.04 % (3036070)Peak memory usage: 13 MB % 190.15/27.04 % (3036070)Instructions burned: 872 (million) % 190.15/27.04 % (3036074)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=1130212485:i=54282_2966 on theBenchmark for (2966ds/54282Mi) % 190.15/27.04 % Detected minimum model sizes of [3] % 190.15/27.04 % Detected maximum model sizes of [max] % 190.15/27.04 % TRYING [3] % 190.15/27.04 % TRYING [4] % 190.15/27.04 % TRYING [5] % 190.15/27.04 % (3036058)Instruction limit reached! % 190.15/27.04 % (3036058)------------------------------ % 190.15/27.04 % (3036058)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 190.15/27.04 % (3036058)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 190.15/27.04 % (3036058)CaDiCaL version: 2.1.3 % 190.15/27.04 % (3036058)Termination reason: Instruction limit % 190.15/27.04 % (3036058)Termination phase: Finite model building constraint generation % 190.15/27.04 % (3036058)Time elapsed: 3.421 s % 190.15/27.04 % (3036058)Peak memory usage: 665 MB % 190.15/27.04 % (3036058)Instructions burned: 9518 (million) % 190.15/27.04 % (3036076)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=472922240:i=3512:aac=none_2957 on theBenchmark for (2957ds/3512Mi) % 190.15/27.04 % (3036072)Instruction limit reached! % 190.15/27.04 % (3036072)------------------------------ % 190.15/27.04 % (3036072)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.20/42.63 % (3036072)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.20/42.63 % (3036072)CaDiCaL version: 2.1.3 % 300.20/42.63 % (3036072)Termination reason: Instruction limit % 300.20/42.63 % (3036072)Termination phase: Saturation % 300.20/42.63 % (3036072)Time elapsed: 2.138 s % 300.20/42.63 % (3036072)Peak memory usage: 18 MB % 300.20/42.63 % (3036072)Instructions burned: 5115 (million) % 300.20/42.63 % (3036078)dis+21_1_sil=32000:sas=cadical:random_seed=1681181181:i=3773:amm=off_2945 on theBenchmark for (2945ds/3773Mi) % 300.20/42.63 % (3036076)Instruction limit reached! % 300.20/42.63 % (3036076)------------------------------ % 300.20/42.63 % (3036076)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.20/42.63 % (3036076)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.20/42.63 % (3036076)CaDiCaL version: 2.1.3 % 300.20/42.63 % (3036076)Termination reason: Instruction limit % 300.20/42.63 % (3036076)Termination phase: Saturation % 300.20/42.63 % (3036076)Time elapsed: 1.721 s % 300.20/42.63 % (3036076)Peak memory usage: 26 MB % 300.20/42.63 % (3036076)Instructions burned: 3514 (million) % 300.20/42.63 % (3036080)ott+11_1_sil=16000:gs=on:random_seed=3117634877:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2939 on theBenchmark for (2939ds/2251Mi) % 300.20/42.63 % (3036080)Instruction limit reached! % 300.20/42.63 % (3036080)------------------------------ % 300.20/42.63 % (3036080)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.20/42.63 % (3036080)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.20/42.63 % (3036080)CaDiCaL version: 2.1.3 % 300.20/42.63 % (3036080)Termination reason: Instruction limit % 300.20/42.63 % (3036080)Termination phase: Saturation % 300.20/42.63 % (3036080)Time elapsed: 0.948 s % 300.20/42.63 % (3036080)Peak memory usage: 17 MB % 300.20/42.63 % (3036080)Instructions burned: 2252 (million) % 300.20/42.63 % (3036082)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=158746633:fmbsr=1.6:i=67534_2930 on theBenchmark for (2930ds/67534Mi) % 300.20/42.63 % Detected minimum model sizes of [3] % 300.20/42.63 % Detected maximum model sizes of [max] % 300.20/42.63 % TRYING [7] % 300.20/42.63 % (3036078)Instruction limit reached! % 300.20/42.63 % (3036078)------------------------------ % 300.20/42.63 % (3036078)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.20/42.63 % (3036078)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.20/42.63 % (3036078)CaDiCaL version: 2.1.3 % 300.20/42.63 % (3036078)Termination reason: Instruction limit % 300.20/42.63 % (3036078)Termination phase: Saturation % 300.20/42.63 % (3036078)Time elapsed: 1.723 s % 300.20/42.63 % (3036078)Peak memory usage: 27 MB % 300.20/42.63 % (3036078)Instructions burned: 3773 (million) % 300.20/42.63 % (3036084)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=1923279817:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2927 on theBenchmark for (2927ds/4591Mi) % 300.20/42.63 % (3036084)Instruction limit reached! % 300.20/42.63 % (3036084)------------------------------ % 300.20/42.63 % (3036084)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.20/42.63 % (3036084)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.20/42.63 % (3036084)CaDiCaL version: 2.1.3 % 300.20/42.63 % (3036084)Termination reason: Instruction limit % 300.20/42.63 % (3036084)Termination phase: Saturation % 300.20/42.63 % (3036084)Time elapsed: 1.866 s % 300.20/42.63 % (3036084)Peak memory usage: 32 MB % 300.20/42.63 % (3036084)Instructions burned: 4593 (million) % 300.20/42.63 % (3036086)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=2677001160:i=29340_2908 on theBenchmark for (2908ds/29340Mi) % 300.20/42.63 % (3036056)Instruction limit reached! % 300.20/42.63 % (3036056)------------------------------ % 300.20/42.63 % (3036056)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.20/42.63 % (3036056)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.20/42.63 % (3036056)CaDiCaL version: 2.1.3 % 300.20/42.63 % (3036056)Termination reason: Instruction limit % 300.20/42.63 % (3036056)Termination phase: Finite model building SAT solving % 300.20/42.63 % (3036056)Time elapsed: 12.348 s % 300.20/42.63 % (3036056)Peak memory usage: 29 MB % 300.20/42.63 % (3036056)Instructions burned: 22061 (million) % 300.20/42.63 % (3036088)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=3466481866:i=5211_2869 on theBenchmark for (2869ds/5211Mi) % 300.20/42.63 % (3036088)Instruction limit reached! % 300.20/42.63 % (3036088)------------------------------ % 300.20/42.63 % % 300.20/42.63 Terminated % 300.20/42.63 % Vampire exiting % 300.20/42.63 Terminated %------------------------------------------------------------------------------