%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : NUM093-1 : TPTP v9.3.1. Bugfixed v2.1.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % Computer : n018.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 12:17:56 PM UTC 2026 % Result : Timeout 300.53s 42.83s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : NUM093-1 : TPTP v9.3.1. Bugfixed v2.1.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.09/0.37 % Computer : n018.cluster.edu % 0.09/0.37 % Model : x86_64 x86_64 % 0.09/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.37 % Memory : 8046.5625MB % 0.09/0.37 % OS : Linux 6.8.0-71-generic % 0.05/0.37 % CPULimit : 300 % 0.05/0.37 % WCLimit : 300 % 0.05/0.37 % DateTime : Sun Sep 27 18:53:54 UTC 2026 % 0.05/0.37 % CPUTime : % 0.05/0.38 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.05/0.41 Running first-order model finding % 0.05/0.41 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 % 15.92/2.76 % (2668245)Will run a generic schedule for satisfiability detection. % 15.92/2.76 % (2668253)dis+10_1_sil=32000:sp=arity:random_seed=838042998:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 15.92/2.76 % (2668251)% WARNING: option uhcvi not known. % 15.92/2.76 % (2668250)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3691259664_2999 on theBenchmark for (2999ds/0Mi) % 15.92/2.76 % (2668251)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=399491268:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 15.92/2.76 % (2668252)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2055172287:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 15.92/2.76 % (2668254)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=467452232:i=116_2999 on theBenchmark for (2999ds/116Mi) % 15.92/2.76 % (2668256)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3979427748:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 15.92/2.76 % (2668255)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2762774545:i=131_2999 on theBenchmark for (2999ds/131Mi) % 15.92/2.76 % (2668253)Instruction limit reached! % 15.92/2.76 % (2668253)------------------------------ % 15.92/2.76 % (2668253)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 15.92/2.76 % (2668253)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.92/2.76 % (2668253)CaDiCaL version: 2.1.3 % 15.92/2.76 % (2668253)Termination reason: Instruction limit % 15.92/2.76 % (2668253)Termination phase: Saturation % 15.92/2.76 % (2668253)Time elapsed: 0.042 s % 15.92/2.76 % (2668253)Peak memory usage: 13 MB % 15.92/2.76 % (2668253)Instructions burned: 105 (million) % 15.92/2.76 % (2668264)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3849663478:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 15.92/2.76 % (2668254)Instruction limit reached! % 15.92/2.76 % (2668254)------------------------------ % 15.92/2.76 % (2668254)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 15.92/2.76 % (2668254)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.92/2.76 % (2668254)CaDiCaL version: 2.1.3 % 15.92/2.76 % (2668254)Termination reason: Instruction limit % 15.92/2.76 % (2668254)Termination phase: Saturation % 15.92/2.76 % (2668254)Time elapsed: 0.071 s % 15.92/2.76 % (2668254)Peak memory usage: 13 MB % 15.92/2.76 % (2668254)Instructions burned: 116 (million) % 15.92/2.76 % (2668255)Instruction limit reached! % 15.92/2.76 % (2668255)------------------------------ % 15.92/2.76 % (2668255)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 15.92/2.76 % (2668255)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.92/2.76 % (2668255)CaDiCaL version: 2.1.3 % 15.92/2.76 % (2668255)Termination reason: Instruction limit % 15.92/2.76 % (2668255)Termination phase: Saturation % 15.92/2.76 % (2668255)Time elapsed: 0.083 s % 15.92/2.76 % (2668255)Peak memory usage: 13 MB % 15.92/2.76 % (2668255)Instructions burned: 131 (million) % 15.92/2.76 % (2668266)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3958047686:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi) % 15.92/2.76 % (2668267)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=2533488791:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi) % 15.92/2.76 % (2668256)Instruction limit reached! % 15.92/2.76 % (2668256)------------------------------ % 15.92/2.76 % (2668256)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 15.92/2.76 % (2668256)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.92/2.76 % (2668256)CaDiCaL version: 2.1.3 % 15.92/2.76 % (2668256)Termination reason: Instruction limit % 15.92/2.76 % (2668256)Termination phase: Saturation % 15.92/2.76 % (2668256)Time elapsed: 0.117 s % 15.92/2.76 % (2668256)Peak memory usage: 14 MB % 15.92/2.76 % (2668256)Instructions burned: 160 (million) % 15.92/2.76 % (2668270)ott-21_1_sil=16000:fs=off:random_seed=67659669:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 15.92/2.76 % TRYING [1] % 15.92/2.76 % TRYING [2] % 15.92/2.76 % TRYING [3] % 15.92/2.76 % (2668266)Instruction limit reached! % 15.92/2.76 % (2668266)------------------------------ % 15.92/2.76 % (2668266)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 15.92/2.76 % (2668266)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 40.47/6.17 % (2668266)CaDiCaL version: 2.1.3 % 40.47/6.17 % (2668266)Termination reason: Instruction limit % 40.47/6.17 % (2668266)Termination phase: Saturation % 40.47/6.17 % (2668266)Time elapsed: 0.089 s % 40.47/6.17 % (2668266)Peak memory usage: 13 MB % 40.47/6.17 % (2668266)Instructions burned: 131 (million) % 40.47/6.17 % (2668272)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2965079284:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi) % 40.47/6.17 % TRYING [1] % 40.47/6.17 % TRYING [2] % 40.47/6.17 % (2668264)Instruction limit reached! % 40.47/6.17 % (2668264)------------------------------ % 40.47/6.17 % (2668264)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 40.47/6.17 % (2668264)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 40.47/6.17 % (2668264)CaDiCaL version: 2.1.3 % 40.47/6.17 % (2668264)Termination reason: Instruction limit % 40.47/6.17 % (2668264)Termination phase: Finite model building constraint generation % 40.47/6.17 % (2668264)Time elapsed: 0.180 s % 40.47/6.17 % (2668264)Peak memory usage: 35 MB % 40.47/6.17 % (2668264)Instructions burned: 717 (million) % 40.47/6.17 % (2668270)Instruction limit reached! % 40.47/6.17 % (2668270)------------------------------ % 40.47/6.17 % (2668270)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 40.47/6.17 % (2668270)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 40.47/6.17 % (2668270)CaDiCaL version: 2.1.3 % 40.47/6.17 % (2668270)Termination reason: Instruction limit % 40.47/6.17 % (2668270)Termination phase: Saturation % 40.47/6.17 % (2668270)Time elapsed: 0.100 s % 40.47/6.17 % (2668270)Peak memory usage: 12 MB % 40.47/6.17 % (2668270)Instructions burned: 180 (million) % 40.47/6.17 % (2668274)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2682935424:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi) % 40.47/6.17 % TRYING [3] % 40.47/6.17 % (2668276)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=80780846:i=1179_2997 on theBenchmark for (2997ds/1179Mi) % 40.47/6.17 % TRYING [1] % 40.47/6.17 % TRYING [2] % 40.47/6.17 % TRYING [4] % 40.47/6.17 % TRYING [3] % 40.47/6.17 % (2668274)Instruction limit reached! % 40.47/6.17 % (2668274)------------------------------ % 40.47/6.17 % (2668274)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 40.47/6.17 % (2668274)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 40.47/6.17 % (2668274)CaDiCaL version: 2.1.3 % 40.47/6.17 % (2668274)Termination reason: Instruction limit % 40.47/6.17 % (2668274)Termination phase: Finite model building constraint generation % 40.47/6.17 % (2668274)Time elapsed: 0.217 s % 40.47/6.17 % (2668274)Peak memory usage: 26 MB % 40.47/6.17 % (2668274)Instructions burned: 867 (million) % 40.47/6.17 % (2668278)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3337847462:i=889:ins=1_2995 on theBenchmark for (2995ds/889Mi) % 40.47/6.17 % (2668267)Instruction limit reached! % 40.47/6.17 % (2668267)------------------------------ % 40.47/6.17 % (2668267)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 40.47/6.17 % (2668267)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 40.47/6.17 % (2668267)CaDiCaL version: 2.1.3 % 40.47/6.17 % (2668267)Termination reason: Instruction limit % 40.47/6.17 % (2668267)Termination phase: Saturation % 40.47/6.17 % (2668267)Time elapsed: 0.445 s % 40.47/6.17 % (2668267)Peak memory usage: 19 MB % 40.47/6.17 % (2668267)Instructions burned: 684 (million) % 40.47/6.17 % (2668272)Instruction limit reached! % 40.47/6.17 % (2668272)------------------------------ % 40.47/6.17 % (2668272)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 40.47/6.17 % (2668272)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 40.47/6.17 % (2668272)CaDiCaL version: 2.1.3 % 40.47/6.17 % (2668272)Termination reason: Instruction limit % 40.47/6.17 % (2668272)Termination phase: Saturation % 40.47/6.17 % (2668272)Time elapsed: 0.348 s % 40.47/6.17 % (2668272)Peak memory usage: 14 MB % 40.47/6.17 % (2668272)Instructions burned: 477 (million) % 40.47/6.17 % (2668280)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=3913865653: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) % 40.47/6.17 % (2668281)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2416249355:i=879:kws=inv_precedence:fsr=off_2994 on theBenchmark for (2994ds/879Mi) % 40.47/6.17 % (2668278)Instruction limit reached! % 40.47/6.17 % (2668278)------------------------------ % 40.47/6.17 % (2668278)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 88.45/13.00 % (2668278)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 88.45/13.00 % (2668278)CaDiCaL version: 2.1.3 % 88.45/13.00 % (2668278)Termination reason: Instruction limit % 88.45/13.00 % (2668278)Termination phase: Finite model building constraint generation % 88.45/13.00 % (2668278)Time elapsed: 0.250 s % 88.45/13.00 % (2668278)Peak memory usage: 76 MB % 88.45/13.00 % (2668278)Instructions burned: 894 (million) % 88.45/13.00 % (2668284)fmb+10_1_sil=64000:random_seed=3132327037:i=22061:nm=2:gsp=on_2992 on theBenchmark for (2992ds/22061Mi) % 88.45/13.00 % TRYING [1] % 88.45/13.00 % TRYING [2] % 88.45/13.00 % TRYING [3] % 88.45/13.00 % (2668276)Instruction limit reached! % 88.45/13.00 % (2668276)------------------------------ % 88.45/13.00 % (2668276)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 88.45/13.00 % (2668276)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 88.45/13.00 % (2668276)CaDiCaL version: 2.1.3 % 88.45/13.00 % (2668276)Termination reason: Instruction limit % 88.45/13.00 % (2668276)Termination phase: Saturation % 88.45/13.00 % (2668276)Time elapsed: 0.733 s % 88.45/13.00 % (2668276)Peak memory usage: 23 MB % 88.45/13.00 % (2668276)Instructions burned: 1180 (million) % 88.45/13.00 % (2668280)Instruction limit reached! % 88.45/13.00 % (2668280)------------------------------ % 88.45/13.00 % (2668280)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 88.45/13.00 % (2668280)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 88.45/13.00 % (2668280)CaDiCaL version: 2.1.3 % 88.45/13.00 % (2668280)Termination reason: Instruction limit % 88.45/13.00 % (2668280)Termination phase: Saturation % 88.45/13.00 % (2668280)Time elapsed: 0.445 s % 88.45/13.00 % (2668280)Peak memory usage: 19 MB % 88.45/13.00 % (2668280)Instructions burned: 693 (million) % 88.45/13.00 % (2668286)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2015404983:i=9515:nm=5_2989 on theBenchmark for (2989ds/9515Mi) % 88.45/13.00 % (2668288)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2618220922:fmbsr=1.7:i=920_2989 on theBenchmark for (2989ds/920Mi) % 88.45/13.00 % (2668281)Instruction limit reached! % 88.45/13.00 % (2668281)------------------------------ % 88.45/13.00 % (2668281)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 88.45/13.00 % (2668281)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 88.45/13.00 % (2668281)CaDiCaL version: 2.1.3 % 88.45/13.00 % (2668281)Termination reason: Instruction limit % 88.45/13.00 % (2668281)Termination phase: Saturation % 88.45/13.00 % (2668281)Time elapsed: 0.496 s % 88.45/13.00 % (2668281)Peak memory usage: 19 MB % 88.45/13.00 % (2668281)Instructions burned: 880 (million) % 88.45/13.00 % (2668290)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1115796492:i=5131_2988 on theBenchmark for (2988ds/5131Mi) % 88.45/13.00 % TRYING [20] % 88.45/13.00 % TRYING [8] % 88.45/13.00 % TRYING [5] % 88.45/13.00 % TRYING [4] % 88.45/13.00 % (2668288)Instruction limit reached! % 88.45/13.00 % (2668288)------------------------------ % 88.45/13.00 % (2668288)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 88.45/13.00 % (2668288)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 88.45/13.00 % (2668288)CaDiCaL version: 2.1.3 % 88.45/13.00 % (2668288)Termination reason: Instruction limit % 88.45/13.00 % (2668288)Termination phase: Finite model building constraint generation % 88.45/13.00 % (2668288)Time elapsed: 0.384 s % 88.45/13.00 % (2668288)Peak memory usage: 46 MB % 88.45/13.00 % (2668288)Instructions burned: 924 (million) % 88.45/13.00 % (2668292)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=431616926:i=1472:ins=7:fdi=8:gsp=on_2985 on theBenchmark for (2985ds/1472Mi) % 88.45/13.00 % (2668292)Instruction limit reached! % 88.45/13.00 % (2668292)------------------------------ % 88.45/13.00 % (2668292)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 88.45/13.00 % (2668292)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 88.45/13.00 % (2668292)CaDiCaL version: 2.1.3 % 88.45/13.00 % (2668292)Termination reason: Instruction limit % 88.45/13.00 % (2668292)Termination phase: Saturation % 88.45/13.00 % (2668292)Time elapsed: 0.625 s % 88.45/13.00 % (2668292)Peak memory usage: 19 MB % 88.45/13.00 % (2668292)Instructions burned: 1475 (million) % 88.45/13.00 % (2668294)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=791192779:i=6324_2978 on theBenchmark for (2978ds/6324Mi) % 88.45/13.00 % (2668294)Cannot represent all propositional literals internally % 88.45/13.00 % (2668294)Refutation not found, incomplete strategy % 204.77/29.34 % (2668294)------------------------------ % 204.77/29.34 % (2668294)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 204.77/29.34 % (2668294)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 204.77/29.34 % (2668294)CaDiCaL version: 2.1.3 % 204.77/29.34 % (2668294)Termination reason: Refutation not found, incomplete strategy % 204.77/29.34 % (2668294)Time elapsed: 0.214 s % 204.77/29.34 % (2668294)Peak memory usage: 13 MB % 204.77/29.34 % (2668294)Instructions burned: 406 (million) % 204.77/29.34 % (2668294)------------------------------ % 204.77/29.34 % (2668294)------------------------------ % 204.77/29.34 % (2668296)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1534732881:fmbsr=2.30978:i=2174_2976 on theBenchmark for (2976ds/2174Mi) % 204.77/29.34 % TRYING [5] % 204.77/29.34 % (2668296)Cannot represent all propositional literals internally % 204.77/29.34 % (2668296)Refutation not found, incomplete strategy % 204.77/29.34 % (2668296)------------------------------ % 204.77/29.34 % (2668296)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 204.77/29.34 % (2668296)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 204.77/29.34 % (2668296)CaDiCaL version: 2.1.3 % 204.77/29.34 % (2668296)Termination reason: Refutation not found, incomplete strategy % 204.77/29.34 % (2668296)Time elapsed: 1.112 s % 204.77/29.34 % (2668296)Peak memory usage: 18 MB % 204.77/29.34 % (2668296)Instructions burned: 2059 (million) % 204.77/29.34 % (2668296)------------------------------ % 204.77/29.34 % (2668296)------------------------------ % 204.77/29.34 % (2668298)ott-2_1_sil=16000:newcnf=on:random_seed=1566342064:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2965 on theBenchmark for (2965ds/869Mi) % 204.77/29.34 % (2668298)Instruction limit reached! % 204.77/29.34 % (2668298)------------------------------ % 204.77/29.34 % (2668298)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 204.77/29.34 % (2668298)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 204.77/29.34 % (2668298)CaDiCaL version: 2.1.3 % 204.77/29.34 % (2668298)Termination reason: Instruction limit % 204.77/29.34 % (2668298)Termination phase: Saturation % 204.77/29.34 % (2668298)Time elapsed: 0.570 s % 204.77/29.34 % (2668298)Peak memory usage: 20 MB % 204.77/29.34 % (2668298)Instructions burned: 870 (million) % 204.77/29.34 % (2668290)Instruction limit reached! % 204.77/29.34 % (2668290)------------------------------ % 204.77/29.34 % (2668290)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 204.77/29.34 % (2668290)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 204.77/29.34 % (2668290)CaDiCaL version: 2.1.3 % 204.77/29.34 % (2668290)Termination reason: Instruction limit % 204.77/29.34 % (2668290)Termination phase: Saturation % 204.77/29.34 % (2668290)Time elapsed: 2.951 s % 204.77/29.34 % (2668290)Peak memory usage: 36 MB % 204.77/29.34 % (2668290)Instructions burned: 5133 (million) % 204.77/29.34 % (2668300)ott+10_1_sil=32000:tgt=ground:random_seed=3819631373:i=5114:av=off_2959 on theBenchmark for (2959ds/5114Mi) % 204.77/29.34 % (2668301)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=1172045388:i=54282_2959 on theBenchmark for (2959ds/54282Mi) % 204.77/29.34 % TRYING [1] % 204.77/29.34 % TRYING [2] % 204.77/29.34 % TRYING [3] % 204.77/29.34 % (2668286)Instruction limit reached! % 204.77/29.34 % (2668286)------------------------------ % 204.77/29.34 % (2668286)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 204.77/29.34 % (2668286)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 204.77/29.34 % (2668286)CaDiCaL version: 2.1.3 % 204.77/29.34 % (2668286)Termination reason: Instruction limit % 204.77/29.34 % (2668286)Termination phase: Finite model building constraint generation % 204.77/29.34 % (2668286)Time elapsed: 3.335 s % 204.77/29.34 % (2668286)Peak memory usage: 537 MB % 204.77/29.34 % (2668286)Instructions burned: 9517 (million) % 204.77/29.34 % (2668304)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=632786311:i=3512:aac=none_2955 on theBenchmark for (2955ds/3512Mi) % 204.77/29.34 % TRYING [4] % 204.77/29.34 % TRYING [6] % 204.77/29.34 % TRYING [5] % 204.77/29.34 % (2668284)Instruction limit reached! % 204.77/29.34 % (2668284)------------------------------ % 204.77/29.34 % (2668284)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 204.77/29.34 % (2668284)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 204.77/29.34 % (2668284)CaDiCaL version: 2.1.3 % 204.77/29.34 % (2668284)Termination reason: Instruction limit % 204.77/29.34 % (2668284)Termination phase: Finite model building SAT solving % 204.77/29.34 % (2668284)Time elapsed: 4.979 s % 204.77/29.34 % (2668284)Peak memory usage: 436 MB % 204.77/29.34 % (2668284)Instructions burned: 22064 (million) % 285.64/40.78 % (2668306)dis+21_1_sil=32000:sas=cadical:random_seed=2506029526:i=3773:amm=off_2942 on theBenchmark for (2942ds/3773Mi) % 285.64/40.78 % (2668304)Instruction limit reached! % 285.64/40.78 % (2668304)------------------------------ % 285.64/40.78 % (2668304)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 285.64/40.78 % (2668304)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 285.64/40.78 % (2668304)CaDiCaL version: 2.1.3 % 285.64/40.78 % (2668304)Termination reason: Instruction limit % 285.64/40.78 % (2668304)Termination phase: Saturation % 285.64/40.78 % (2668304)Time elapsed: 1.898 s % 285.64/40.78 % (2668304)Peak memory usage: 34 MB % 285.64/40.78 % (2668304)Instructions burned: 3514 (million) % 285.64/40.78 % (2668308)ott+11_1_sil=16000:gs=on:random_seed=3254265002:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2936 on theBenchmark for (2936ds/2251Mi) % 285.64/40.78 % (2668306)Instruction limit reached! % 285.64/40.78 % (2668306)------------------------------ % 285.64/40.78 % (2668306)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 285.64/40.78 % (2668306)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 285.64/40.78 % (2668306)CaDiCaL version: 2.1.3 % 285.64/40.78 % (2668306)Termination reason: Instruction limit % 285.64/40.78 % (2668306)Termination phase: Saturation % 285.64/40.78 % (2668306)Time elapsed: 1.210 s % 285.64/40.78 % (2668306)Peak memory usage: 38 MB % 285.64/40.78 % (2668306)Instructions burned: 3774 (million) % 285.64/40.78 % (2668310)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=1928407595:fmbsr=1.6:i=67534_2929 on theBenchmark for (2929ds/67534Mi) % 285.64/40.78 % (2668300)Instruction limit reached! % 285.64/40.78 % (2668300)------------------------------ % 285.64/40.78 % (2668300)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 285.64/40.78 % (2668300)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 285.64/40.78 % (2668300)CaDiCaL version: 2.1.3 % 285.64/40.78 % (2668300)Termination reason: Instruction limit % 285.64/40.78 % (2668300)Termination phase: Saturation % 285.64/40.78 % (2668300)Time elapsed: 3.167 s % 285.64/40.78 % (2668300)Peak memory usage: 49 MB % 285.64/40.78 % (2668300)Instructions burned: 5115 (million) % 285.64/40.78 % (2668312)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=1306229551:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2927 on theBenchmark for (2927ds/4591Mi) % 285.64/40.78 % (2668308)Instruction limit reached! % 285.64/40.78 % (2668308)------------------------------ % 285.64/40.78 % (2668308)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 285.64/40.78 % (2668308)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 285.64/40.78 % (2668308)CaDiCaL version: 2.1.3 % 285.64/40.78 % (2668308)Termination reason: Instruction limit % 285.64/40.78 % (2668308)Termination phase: Saturation % 285.64/40.78 % (2668308)Time elapsed: 1.056 s % 285.64/40.78 % (2668308)Peak memory usage: 21 MB % 285.64/40.78 % (2668308)Instructions burned: 2251 (million) % 285.64/40.78 % (2668314)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=1751693399:i=29340_2925 on theBenchmark for (2925ds/29340Mi) % 285.64/40.78 % TRYING [7] % 285.64/40.78 % TRYING [6] % 285.64/40.78 % (2668312)Instruction limit reached! % 285.64/40.78 % (2668312)------------------------------ % 285.64/40.78 % (2668312)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 285.64/40.78 % (2668312)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 285.64/40.78 % (2668312)CaDiCaL version: 2.1.3 % 285.64/40.78 % (2668312)Termination reason: Instruction limit % 285.64/40.78 % (2668312)Termination phase: Saturation % 285.64/40.78 % (2668312)Time elapsed: 2.652 s % 285.64/40.78 % (2668312)Peak memory usage: 48 MB % 285.64/40.78 % (2668312)Instructions burned: 4593 (million) % 285.64/40.78 % (2668316)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=2508379944:i=5211_2900 on theBenchmark for (2900ds/5211Mi) % 285.64/40.78 % (2668316)Instruction limit reached! % 285.64/40.78 % (2668316)------------------------------ % 285.64/40.78 % (2668316)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 285.64/40.78 % (2668316)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 285.64/40.78 % (2668316)CaDiCaL version: 2.1.3 % 285.64/40.78 % (2668316)Termination reason: Instruction limit % 285.64/40.78 % (2668316)Termination phase: Saturation % 285.64/40.78 % (2668316)Time elapsed: 2.589 s % 285.64/40.78 % (2668316)Peak memory usage: 49 MB % 285.64/40.78 % (2668316)Instructions burned: 5211 (million) % 285.64/40.78 % (2668318)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=958556733:i=5497:nm=2_2874 on theBenchmark for (2874ds/5497Mi) % 300.53/42.83 % TRYING [17] % 300.53/42.83 % (2668318)Instruction limit reached! % 300.53/42.83 % (2668318)------------------------------ % 300.53/42.83 % (2668318)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.53/42.83 % (2668318)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.53/42.83 % (2668318)CaDiCaL version: 2.1.3 % 300.53/42.83 % (2668318)Termination reason: Instruction limit % 300.53/42.83 % (2668318)Termination phase: Finite model building constraint generation % 300.53/42.83 % (2668318)Time elapsed: 1.937 s % 300.53/42.83 % (2668318)Peak memory usage: 303 MB % 300.53/42.83 % (2668318)Instructions burned: 5497 (million) % 300.53/42.83 % (2668320)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=833887252:fmbsr=2:i=46332_2854 on theBenchmark for (2854ds/46332Mi) % 300.53/42.83 % TRYING [15] % 300.53/42.83 % TRYING [7] % 300.53/42.83 % (2668314)Instruction limit reached! % 300.53/42.83 % (2668314)------------------------------ % 300.53/42.83 % (2668314)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.53/42.83 % (2668314)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.53/42.83 % (2668314)CaDiCaL version: 2.1.3 % 300.53/42.83 % (2668314)Termination reason: Instruction limit % 300.53/42.83 % (2668314)Termination phase: Saturation % 300.53/42.83 % (2668314)Time elapsed: 13.629 s % 300.53/42.83 % (2668314)Peak memory usage: 170 MB % 300.53/42.83 % (2668314)Instructions burned: 29341 (million) % 300.53/42.83 % (2668322)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=202088141:i=14071_2788 on theBenchmark for (2788ds/14071Mi) % 300.53/42.83 % TRYING [12] % 300.53/42.83 % TRYING [7] % 300.53/42.83 % (2668310)Instruction limit reached! % 300.53/42.83 % (2668310)------------------------------ % 300.53/42.83 % (2668310)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.53/42.83 % (2668310)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.53/42.83 % (2668310)CaDiCaL version: 2.1.3 % 300.53/42.83 % (2668310)Termination reason: Instruction limit % 300.53/42.83 % (2668310)Termination phase: Finite model building constraint generation % 300.53/42.83 % (2668310)Time elapsed: 16.855 s % 300.53/42.83 % (2668310)Peak memory usage: 3185 MB % 300.53/42.83 % (2668310)Instructions burned: 67537 (million) % 300.53/42.83 % (2668324)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2165267996:i=22565:add=on:rawr=on_2758 on theBenchmark for (2758ds/22565Mi) % 300.53/42.83 % (2668301)Instruction limit reached! % 300.53/42.83 % (2668301)------------------------------ % 300.53/42.83 % (2668301)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.53/42.83 % (2668301)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.53/42.83 % (2668301)CaDiCaL version: 2.1.3 % 300.53/42.83 % (2668301)Termination reason: Instruction limit % 300.53/42.83 % (2668301)Termination phase: Finite model building constraint generation % 300.53/42.83 % (2668301)Time elapsed: 20.160 s % 300.53/42.83 % (2668301)Peak memory usage: 1583 MB % 300.53/42.83 % (2668301)Instructions burned: 54284 (million) % 300.53/42.83 % (2668326)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=2425242632:i=8173:av=off_2755 on theBenchmark for (2755ds/8173Mi) % 300.53/42.83 % (2668322)Instruction limit reached! % 300.53/42.83 % (2668322)------------------------------ % 300.53/42.83 % (2668322)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.53/42.83 % (2668322)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.53/42.83 % (2668322)CaDiCaL version: 2.1.3 % 300.53/42.83 % (2668322)Termination reason: Instruction limit % 300.53/42.83 % (2668322)Termination phase: Finite model building constraint generation % 300.53/42.83 % (2668322)Time elapsed: 5.006 s % 300.53/42.83 % (2668322)Peak memory usage: 910 MB % 300.53/42.83 % (2668322)Instructions burned: 14074 (million) % 300.53/42.83 % (2668328)dis+10_16:1_sil=16000:random_seed=3034349045:i=9155:fsr=off_2737 on theBenchmark for (2737ds/9155Mi) % 300.53/42.83 % (2668324)Instruction limit reached! % 300.53/42.83 % (2668324)------------------------------ % 300.53/42.83 % (2668324)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.53/42.83 % (2668324)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.53/42.83 % (2668324)CaDiCaL version: 2.1.3 % 300.53/42.83 % (2668324)Termination reason: Instruction limit % 300.53/42.83 % (2668324)Termination phase: Saturation % 300.53/42.83 % (2668324)Time elapsed: 4.772 s % 300.53/42.83 % (2668324)Peak m % 300.53/42.84 Terminated % 300.53/42.84 % Vampire exiting %------------------------------------------------------------------------------