%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWW320+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 : n010.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:39:49 PM UTC 2026 % Result : Timeout 286.01s 41.39s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.05 % Problem : SWW320+1 : TPTP v9.3.1. Released v5.2.0. % 0.00/0.09 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.29/0.32 % Computer : n010.cluster.edu % 0.29/0.32 % Model : x86_64 x86_64 % 0.29/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.29/0.32 % Memory : 8046.5625MB % 0.29/0.32 % OS : Linux 6.8.0-71-generic % 0.29/0.32 % CPULimit : 300 % 0.29/0.32 % WCLimit : 300 % 0.29/0.32 % DateTime : Mon Sep 28 13:35:02 UTC 2026 % 0.29/0.33 % CPUTime : % 0.29/0.33 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.29/0.39 Running first-order model finding % 0.29/0.39 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 % 34.94/6.03 % (1925139)Will run a generic schedule for satisfiability detection. % 34.94/6.03 % (1925147)dis+10_1_sil=32000:sp=arity:random_seed=2826488212:i=103:fgj=on_2993 on theBenchmark for (2993ds/103Mi) % 34.94/6.03 % (1925145)% WARNING: option uhcvi not known. % 34.94/6.03 % (1925145)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1601145412:i=135531:add=off:rawr=on_2993 on theBenchmark for (2993ds/135531Mi) % 34.94/6.03 % (1925144)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=4052624356_2993 on theBenchmark for (2993ds/0Mi) % 34.94/6.03 % (1925148)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1972945682:i=116_2993 on theBenchmark for (2993ds/116Mi) % 34.94/6.03 % (1925146)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1997103762:i=88024:add=on:rawr=on_2993 on theBenchmark for (2993ds/88024Mi) % 34.94/6.03 % (1925150)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=175503841:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2993 on theBenchmark for (2993ds/159Mi) % 34.94/6.03 % (1925149)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1331835656:i=131_2993 on theBenchmark for (2993ds/131Mi) % 34.94/6.03 % (1925147)Instruction limit reached! % 34.94/6.03 % (1925147)------------------------------ % 34.94/6.03 % (1925147)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 34.94/6.03 % (1925147)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.94/6.03 % (1925147)CaDiCaL version: 2.1.3 % 34.94/6.03 % (1925147)Termination reason: Instruction limit % 34.94/6.03 % (1925147)Termination phase: Preprocessing 3 % 34.94/6.03 % (1925147)Time elapsed: 0.062 s % 34.94/6.03 % (1925147)Peak memory usage: 20 MB % 34.94/6.03 % (1925147)Instructions burned: 105 (million) % 34.94/6.03 % (1925158)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3198118395:i=714:nm=2_2992 on theBenchmark for (2992ds/714Mi) % 34.94/6.03 % (1925148)Instruction limit reached! % 34.94/6.03 % (1925148)------------------------------ % 34.94/6.03 % (1925148)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 34.94/6.03 % (1925148)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.94/6.03 % (1925148)CaDiCaL version: 2.1.3 % 34.94/6.03 % (1925148)Termination reason: Instruction limit % 34.94/6.03 % (1925148)Termination phase: NewCNF % 34.94/6.03 % (1925148)Time elapsed: 0.120 s % 34.94/6.03 % (1925148)Peak memory usage: 21 MB % 34.94/6.03 % (1925148)Instructions burned: 116 (million) % 34.94/6.03 % (1925149)Instruction limit reached! % 34.94/6.03 % (1925149)------------------------------ % 34.94/6.03 % (1925149)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 34.94/6.03 % (1925149)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.94/6.03 % (1925149)CaDiCaL version: 2.1.3 % 34.94/6.03 % (1925149)Termination reason: Instruction limit % 34.94/6.03 % (1925149)Termination phase: Preprocessing 3 % 34.94/6.03 % (1925149)Time elapsed: 0.135 s % 34.94/6.03 % (1925149)Peak memory usage: 20 MB % 34.94/6.03 % (1925149)Instructions burned: 131 (million) % 34.94/6.03 % (1925150)Instruction limit reached! % 34.94/6.03 % (1925150)------------------------------ % 34.94/6.03 % (1925150)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 34.94/6.03 % (1925150)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.94/6.03 % (1925150)CaDiCaL version: 2.1.3 % 34.94/6.03 % (1925150)Termination reason: Instruction limit % 34.94/6.03 % (1925150)Termination phase: Clausification % 34.94/6.03 % (1925150)Time elapsed: 0.157 s % 34.94/6.03 % (1925150)Peak memory usage: 21 MB % 34.94/6.03 % (1925150)Instructions burned: 159 (million) % 34.94/6.03 % (1925160)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3299993194:i=131:bd=preordered:fsd=on_2991 on theBenchmark for (2991ds/131Mi) % 34.94/6.03 % (1925161)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=680792231:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2991 on theBenchmark for (2991ds/684Mi) % 34.94/6.03 % (1925162)ott-21_1_sil=16000:fs=off:random_seed=913309981:i=180:av=off:fsr=off_2991 on theBenchmark for (2991ds/180Mi) % 34.94/6.03 % (1925160)Instruction limit reached! % 34.94/6.03 % (1925160)------------------------------ % 34.94/6.03 % (1925160)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 34.94/6.03 % (1925160)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 63.27/9.92 % (1925160)CaDiCaL version: 2.1.3 % 63.27/9.92 % (1925160)Termination reason: Instruction limit % 63.27/9.92 % (1925160)Termination phase: Preprocessing 3 % 63.27/9.92 % (1925160)Time elapsed: 0.132 s % 63.27/9.92 % (1925160)Peak memory usage: 20 MB % 63.27/9.92 % (1925160)Instructions burned: 131 (million) % 63.27/9.92 % (1925166)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2552883050:i=477:bd=all_2989 on theBenchmark for (2989ds/477Mi) % 63.27/9.92 % (1925162)Instruction limit reached! % 63.27/9.92 % (1925162)------------------------------ % 63.27/9.92 % (1925162)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 63.27/9.92 % (1925162)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 63.27/9.92 % (1925162)CaDiCaL version: 2.1.3 % 63.27/9.92 % (1925162)Termination reason: Instruction limit % 63.27/9.92 % (1925162)Termination phase: Property scanning % 63.27/9.92 % (1925162)Time elapsed: 0.179 s % 63.27/9.92 % (1925162)Peak memory usage: 22 MB % 63.27/9.92 % (1925162)Instructions burned: 180 (million) % 63.27/9.92 % (1925168)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2174201424:fmbsr=1.3:i=865:ins=25_2988 on theBenchmark for (2988ds/865Mi) % 63.27/9.92 % (1925158)Instruction limit reached! % 63.27/9.92 % (1925158)------------------------------ % 63.27/9.92 % (1925158)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 63.27/9.92 % (1925158)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 63.27/9.92 % (1925158)CaDiCaL version: 2.1.3 % 63.27/9.92 % (1925158)Termination reason: Instruction limit % 63.27/9.92 % (1925158)Termination phase: Finite model building preprocessing % 63.27/9.92 % (1925158)Time elapsed: 0.399 s % 63.27/9.92 % (1925158)Peak memory usage: 25 MB % 63.27/9.92 % (1925158)Instructions burned: 717 (million) % 63.27/9.92 % (1925170)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3459563895:i=1179_2987 on theBenchmark for (2987ds/1179Mi) % 63.27/9.92 % (1925166)Instruction limit reached! % 63.27/9.92 % (1925166)------------------------------ % 63.27/9.92 % (1925166)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 63.27/9.92 % (1925166)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 63.27/9.92 % (1925166)CaDiCaL version: 2.1.3 % 63.27/9.92 % (1925166)Termination reason: Instruction limit % 63.27/9.92 % (1925166)Termination phase: Property scanning % 63.27/9.92 % (1925166)Time elapsed: 0.424 s % 63.27/9.92 % (1925166)Peak memory usage: 23 MB % 63.27/9.92 % (1925166)Instructions burned: 477 (million) % 63.27/9.92 % (1925161)Instruction limit reached! % 63.27/9.92 % (1925161)------------------------------ % 63.27/9.92 % (1925161)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 63.27/9.92 % (1925161)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 63.27/9.92 % (1925161)CaDiCaL version: 2.1.3 % 63.27/9.92 % (1925161)Termination reason: Instruction limit % 63.27/9.92 % (1925161)Termination phase: Saturation % 63.27/9.92 % (1925161)Time elapsed: 0.601 s % 63.27/9.92 % (1925161)Peak memory usage: 24 MB % 63.27/9.92 % (1925161)Instructions burned: 685 (million) % 63.27/9.92 % (1925174)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=1608351774:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2984 on theBenchmark for (2984ds/692Mi) % 63.27/9.92 % (1925173)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=452449850:i=889:ins=1_2984 on theBenchmark for (2984ds/889Mi) % 63.27/9.92 % (1925170)Instruction limit reached! % 63.27/9.92 % (1925170)------------------------------ % 63.27/9.92 % (1925170)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 63.27/9.92 % (1925170)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 63.27/9.92 % (1925170)CaDiCaL version: 2.1.3 % 63.27/9.92 % (1925170)Termination reason: Instruction limit % 63.27/9.92 % (1925170)Termination phase: Saturation % 63.27/9.92 % (1925170)Time elapsed: 0.586 s % 63.27/9.92 % (1925170)Peak memory usage: 30 MB % 63.27/9.92 % (1925170)Instructions burned: 1181 (million) % 63.27/9.92 % (1925168)Instruction limit reached! % 63.27/9.92 % (1925168)------------------------------ % 63.27/9.92 % (1925168)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 63.27/9.92 % (1925168)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 63.27/9.92 % (1925168)CaDiCaL version: 2.1.3 % 63.27/9.92 % (1925168)Termination reason: Instruction limit % 63.27/9.92 % (1925168)Termination phase: Finite model building preprocessing % 93.79/14.24 % (1925168)Time elapsed: 0.746 s % 93.79/14.24 % (1925168)Peak memory usage: 30 MB % 93.79/14.24 % (1925168)Instructions burned: 865 (million) % 93.79/14.24 % (1925177)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1493466870:i=879:kws=inv_precedence:fsr=off_2981 on theBenchmark for (2981ds/879Mi) % 93.79/14.24 % (1925178)fmb+10_1_sil=64000:random_seed=76515842:i=22061:nm=2:gsp=on_2980 on theBenchmark for (2980ds/22061Mi) % 93.79/14.24 % (1925174)Instruction limit reached! % 93.79/14.24 % (1925174)------------------------------ % 93.79/14.24 % (1925174)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 93.79/14.24 % (1925174)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 93.79/14.24 % (1925174)CaDiCaL version: 2.1.3 % 93.79/14.24 % (1925174)Termination reason: Instruction limit % 93.79/14.24 % (1925174)Termination phase: Saturation % 93.79/14.24 % (1925174)Time elapsed: 0.616 s % 93.79/14.24 % (1925174)Peak memory usage: 28 MB % 93.79/14.24 % (1925174)Instructions burned: 692 (million) % 93.79/14.24 % (1925181)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=211663704:i=9515:nm=5_2978 on theBenchmark for (2978ds/9515Mi) % 93.79/14.24 % (1925173)Instruction limit reached! % 93.79/14.24 % (1925173)------------------------------ % 93.79/14.24 % (1925173)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 93.79/14.24 % (1925173)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 93.79/14.24 % (1925173)CaDiCaL version: 2.1.3 % 93.79/14.24 % (1925173)Termination reason: Instruction limit % 93.79/14.24 % (1925173)Termination phase: Finite model building preprocessing % 93.79/14.24 % (1925173)Time elapsed: 0.773 s % 93.79/14.24 % (1925173)Peak memory usage: 31 MB % 93.79/14.24 % (1925173)Instructions burned: 889 (million) % 93.79/14.24 % (1925183)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2505631671:fmbsr=1.7:i=920_2976 on theBenchmark for (2976ds/920Mi) % 93.79/14.24 % (1925177)Instruction limit reached! % 93.79/14.24 % (1925177)------------------------------ % 93.79/14.24 % (1925177)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 93.79/14.24 % (1925177)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 93.79/14.24 % (1925177)CaDiCaL version: 2.1.3 % 93.79/14.24 % (1925177)Termination reason: Instruction limit % 93.79/14.24 % (1925177)Termination phase: Saturation % 93.79/14.24 % (1925177)Time elapsed: 0.770 s % 93.79/14.24 % (1925177)Peak memory usage: 30 MB % 93.79/14.24 % (1925177)Instructions burned: 879 (million) % 93.79/14.24 % (1925185)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=79991855:i=5131_2973 on theBenchmark for (2973ds/5131Mi) % 93.79/14.24 % (1925183)Instruction limit reached! % 93.79/14.24 % (1925183)------------------------------ % 93.79/14.24 % (1925183)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 93.79/14.24 % (1925183)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 93.79/14.24 % (1925183)CaDiCaL version: 2.1.3 % 93.79/14.24 % (1925183)Termination reason: Instruction limit % 93.79/14.24 % (1925183)Termination phase: Finite model building preprocessing % 93.79/14.24 % (1925183)Time elapsed: 0.811 s % 93.79/14.24 % (1925183)Peak memory usage: 32 MB % 93.79/14.24 % (1925183)Instructions burned: 920 (million) % 93.79/14.24 % (1925187)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2026022800:i=1472:ins=7:fdi=8:gsp=on_2968 on theBenchmark for (2968ds/1472Mi) % 93.79/14.24 % (1925187)Instruction limit reached! % 93.79/14.24 % (1925187)------------------------------ % 93.79/14.24 % (1925187)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 93.79/14.24 % (1925187)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 93.79/14.24 % (1925187)CaDiCaL version: 2.1.3 % 93.79/14.24 % (1925187)Termination reason: Instruction limit % 93.79/14.24 % (1925187)Termination phase: Saturation % 93.79/14.24 % (1925187)Time elapsed: 0.672 s % 93.79/14.24 % (1925187)Peak memory usage: 28 MB % 93.79/14.24 % (1925187)Instructions burned: 1473 (million) % 93.79/14.24 % (1925189)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3610622475:i=6324_2960 on theBenchmark for (2960ds/6324Mi) % 93.79/14.24 % (1925185)Instruction limit reached! % 93.79/14.24 % (1925185)------------------------------ % 93.79/14.24 % (1925185)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 93.79/14.24 % (1925185)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 93.79/14.24 % (1925185)CaDiCaL version: 2.1.3 % 93.79/14.24 % (1925185)Termination reason: Instruction limit % 200.18/29.20 % (1925185)Termination phase: Saturation % 200.18/29.20 % (1925185)Time elapsed: 2.917 s % 200.18/29.20 % (1925185)Peak memory usage: 51 MB % 200.18/29.20 % (1925185)Instructions burned: 5132 (million) % 200.18/29.20 % (1925191)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=2364053507:fmbsr=2.30978:i=2174_2943 on theBenchmark for (2943ds/2174Mi) % 200.18/29.20 % (1925191)Instruction limit reached! % 200.18/29.20 % (1925191)------------------------------ % 200.18/29.20 % (1925191)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 200.18/29.20 % (1925191)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 200.18/29.20 % (1925191)CaDiCaL version: 2.1.3 % 200.18/29.20 % (1925191)Termination reason: Instruction limit % 200.18/29.20 % (1925191)Termination phase: Finite model building preprocessing % 200.18/29.20 % (1925191)Time elapsed: 1.001 s % 200.18/29.20 % (1925191)Peak memory usage: 47 MB % 200.18/29.20 % (1925191)Instructions burned: 2175 (million) % 200.18/29.20 % (1925193)ott-2_1_sil=16000:newcnf=on:random_seed=3842119358:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2933 on theBenchmark for (2933ds/869Mi) % 200.18/29.20 % (1925189)Instruction limit reached! % 200.18/29.20 % (1925189)------------------------------ % 200.18/29.20 % (1925189)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 200.18/29.20 % (1925189)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 200.18/29.20 % (1925189)CaDiCaL version: 2.1.3 % 200.18/29.20 % (1925189)Termination reason: Instruction limit % 200.18/29.20 % (1925189)Termination phase: Finite model building preprocessing % 200.18/29.20 % (1925189)Time elapsed: 3.189 s % 200.18/29.20 % (1925189)Peak memory usage: 66 MB % 200.18/29.20 % (1925189)Instructions burned: 6324 (million) % 200.18/29.20 % (1925193)Instruction limit reached! % 200.18/29.20 % (1925193)------------------------------ % 200.18/29.20 % (1925193)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 200.18/29.20 % (1925193)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 200.18/29.20 % (1925193)CaDiCaL version: 2.1.3 % 200.18/29.20 % (1925193)Termination reason: Instruction limit % 200.18/29.20 % (1925193)Termination phase: Saturation % 200.18/29.20 % (1925193)Time elapsed: 0.436 s % 200.18/29.20 % (1925193)Peak memory usage: 28 MB % 200.18/29.20 % (1925193)Instructions burned: 869 (million) % 200.18/29.20 % (1925196)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=837994221:i=54282_2928 on theBenchmark for (2928ds/54282Mi) % 200.18/29.20 % (1925195)ott+10_1_sil=32000:tgt=ground:random_seed=1337634485:i=5114:av=off_2928 on theBenchmark for (2928ds/5114Mi) % 200.18/29.20 % (1925181)Instruction limit reached! % 200.18/29.20 % (1925181)------------------------------ % 200.18/29.20 % (1925181)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 200.18/29.20 % (1925181)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 200.18/29.20 % (1925181)CaDiCaL version: 2.1.3 % 200.18/29.20 % (1925181)Termination reason: Instruction limit % 200.18/29.20 % (1925181)Termination phase: Finite model building preprocessing % 200.18/29.20 % (1925181)Time elapsed: 5.419 s % 200.18/29.20 % (1925181)Peak memory usage: 78 MB % 200.18/29.20 % (1925181)Instructions burned: 9516 (million) % 200.18/29.20 % (1925199)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=1009281754:i=3512:aac=none_2923 on theBenchmark for (2923ds/3512Mi) % 200.18/29.20 % (1925178)Instruction limit reached! % 200.18/29.20 % (1925178)------------------------------ % 200.18/29.20 % (1925178)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 200.18/29.20 % (1925178)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 200.18/29.20 % (1925178)CaDiCaL version: 2.1.3 % 200.18/29.20 % (1925178)Termination reason: Instruction limit % 200.18/29.20 % (1925178)Termination phase: Finite model building preprocessing % 200.18/29.20 % (1925178)Time elapsed: 6.407 s % 200.18/29.20 % (1925178)Peak memory usage: 216 MB % 200.18/29.20 % (1925178)Instructions burned: 22062 (million) % 200.18/29.20 % (1925201)dis+21_1_sil=32000:sas=cadical:random_seed=871877989:i=3773:amm=off_2916 on theBenchmark for (2916ds/3773Mi) % 200.18/29.20 % (1925201)Instruction limit reached! % 200.18/29.20 % (1925201)------------------------------ % 200.18/29.20 % (1925201)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 200.18/29.20 % (1925201)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 200.18/29.20 % (1925201)CaDiCaL version: 2.1.3 % 200.18/29.20 % (1925201)Termination reason: Instruction limit % 200.18/29.20 % (1925201)Termination phase: Saturation % 200.18/29.20 % (1925201)Time elapsed: 1.142 s % 286.01/41.39 % (1925201)Peak memory usage: 56 MB % 286.01/41.39 % (1925201)Instructions burned: 3776 (million) % 286.01/41.39 % (1925203)ott+11_1_sil=16000:gs=on:random_seed=3518749838:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2904 on theBenchmark for (2904ds/2251Mi) % 286.01/41.39 % (1925199)Instruction limit reached! % 286.01/41.39 % (1925199)------------------------------ % 286.01/41.39 % (1925199)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 286.01/41.39 % (1925199)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 286.01/41.39 % (1925199)CaDiCaL version: 2.1.3 % 286.01/41.39 % (1925199)Termination reason: Instruction limit % 286.01/41.39 % (1925199)Termination phase: Saturation % 286.01/41.39 % (1925199)Time elapsed: 1.948 s % 286.01/41.39 % (1925199)Peak memory usage: 51 MB % 286.01/41.39 % (1925199)Instructions burned: 3513 (million) % 286.01/41.39 % (1925205)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=3954443338:fmbsr=1.6:i=67534_2903 on theBenchmark for (2903ds/67534Mi) % 286.01/41.39 % (1925203)Instruction limit reached! % 286.01/41.39 % (1925203)------------------------------ % 286.01/41.39 % (1925203)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 286.01/41.39 % (1925203)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 286.01/41.39 % (1925203)CaDiCaL version: 2.1.3 % 286.01/41.39 % (1925203)Termination reason: Instruction limit % 286.01/41.39 % (1925203)Termination phase: Saturation % 286.01/41.39 % (1925203)Time elapsed: 0.645 s % 286.01/41.39 % (1925203)Peak memory usage: 34 MB % 286.01/41.39 % (1925203)Instructions burned: 2254 (million) % 286.01/41.39 % (1925207)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=3273036401:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2898 on theBenchmark for (2898ds/4591Mi) % 286.01/41.39 % (1925195)Instruction limit reached! % 286.01/41.39 % (1925195)------------------------------ % 286.01/41.39 % (1925195)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 286.01/41.39 % (1925195)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 286.01/41.39 % (1925195)CaDiCaL version: 2.1.3 % 286.01/41.39 % (1925195)Termination reason: Instruction limit % 286.01/41.39 % (1925195)Termination phase: Saturation % 286.01/41.39 % (1925195)Time elapsed: 3.120 s % 286.01/41.39 % (1925195)Peak memory usage: 66 MB % 286.01/41.39 % (1925195)Instructions burned: 5114 (million) % 286.01/41.39 % (1925209)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=2920991825:i=29340_2897 on theBenchmark for (2897ds/29340Mi) % 286.01/41.39 % (1925207)Instruction limit reached! % 286.01/41.39 % (1925207)------------------------------ % 286.01/41.39 % (1925207)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 286.01/41.39 % (1925207)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 286.01/41.39 % (1925207)CaDiCaL version: 2.1.3 % 286.01/41.39 % (1925207)Termination reason: Instruction limit % 286.01/41.39 % (1925207)Termination phase: Saturation % 286.01/41.39 % (1925207)Time elapsed: 0.974 s % 286.01/41.39 % (1925207)Peak memory usage: 31 MB % 286.01/41.39 % (1925207)Instructions burned: 4593 (million) % 286.01/41.39 % (1925211)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=262064842:i=5211_2888 on theBenchmark for (2888ds/5211Mi) % 286.01/41.39 % (1925211)Instruction limit reached! % 286.01/41.39 % (1925211)------------------------------ % 286.01/41.39 % (1925211)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 286.01/41.39 % (1925211)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 286.01/41.39 % (1925211)CaDiCaL version: 2.1.3 % 286.01/41.39 % (1925211)Termination reason: Instruction limit % 286.01/41.39 % (1925211)Termination phase: Saturation % 286.01/41.39 % (1925211)Time elapsed: 1.131 s % 286.01/41.39 % (1925211)Peak memory usage: 46 MB % 286.01/41.39 % (1925211)Instructions burned: 5214 (million) % 286.01/41.39 % (1925213)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=1417889969:i=5497:nm=2_2876 on theBenchmark for (2876ds/5497Mi) % 286.01/41.39 % (1925213)Instruction limit reached! % 286.01/41.39 % (1925213)------------------------------ % 286.01/41.39 % (1925213)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 286.01/41.39 % (1925213)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 286.01/41.39 % (1925213)CaDiCaL version: 2.1.3 % 286.01/41.39 % (1925213)Termination reason: Instruction limit % 286.01/41.39 % (1925213)Termination phase: Finite model building preprocessing % 286.01/41.39 % (1925213)Time elapsed: 1.494 s % 286.01/41.39 % (1925213Terminated % 300.19/43.34 % Vampire exiting %------------------------------------------------------------------------------