%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWW307+1 : TPTP v9.3.1. Released v5.2.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % Computer : n002.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:48 PM UTC 2026 % Result : Timeout 300.53s 42.94s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWW307+1 : TPTP v9.3.1. Released v5.2.0. % 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.08/0.19 % Computer : n002.cluster.edu % 0.08/0.19 % Model : x86_64 x86_64 % 0.08/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.08/0.19 % Memory : 8046.5625MB % 0.08/0.19 % OS : Linux 6.8.0-71-generic % 0.08/0.19 % CPULimit : 300 % 0.08/0.19 % WCLimit : 300 % 0.08/0.19 % DateTime : Mon Sep 28 13:34:22 UTC 2026 % 0.08/0.19 % CPUTime : % 0.08/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.08/0.22 Running first-order model finding % 0.08/0.22 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 22.52/3.79 % (354296)Will run a generic schedule for satisfiability detection. % 22.52/3.79 % (354305)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=617936791:i=116_2996 on theBenchmark for (2996ds/116Mi) % 22.52/3.79 % (354302)% WARNING: option uhcvi not known. % 22.52/3.79 % (354301)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=204446842_2996 on theBenchmark for (2996ds/0Mi) % 22.52/3.79 % (354302)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3595289267:i=135531:add=off:rawr=on_2996 on theBenchmark for (2996ds/135531Mi) % 22.52/3.79 % (354303)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2693265531:i=88024:add=on:rawr=on_2996 on theBenchmark for (2996ds/88024Mi) % 22.52/3.79 % (354304)dis+10_1_sil=32000:sp=arity:random_seed=50743395:i=103:fgj=on_2996 on theBenchmark for (2996ds/103Mi) % 22.52/3.79 % (354307)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3660129291:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2996 on theBenchmark for (2996ds/159Mi) % 22.52/3.79 % (354306)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=812670618:i=131_2996 on theBenchmark for (2996ds/131Mi) % 22.52/3.79 % (354305)Instruction limit reached! % 22.52/3.79 % (354305)------------------------------ % 22.52/3.79 % (354305)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.52/3.79 % (354305)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.52/3.79 % (354305)CaDiCaL version: 2.1.3 % 22.52/3.79 % (354305)Termination reason: Instruction limit % 22.52/3.79 % (354305)Termination phase: NewCNF % 22.52/3.79 % (354305)Time elapsed: 0.047 s % 22.52/3.79 % (354305)Peak memory usage: 21 MB % 22.52/3.79 % (354305)Instructions burned: 119 (million) % 22.52/3.79 % (354315)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1161324375:i=714:nm=2_2995 on theBenchmark for (2995ds/714Mi) % 22.52/3.79 % (354304)Instruction limit reached! % 22.52/3.79 % (354304)------------------------------ % 22.52/3.79 % (354304)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.52/3.79 % (354304)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.52/3.79 % (354304)CaDiCaL version: 2.1.3 % 22.52/3.79 % (354304)Termination reason: Instruction limit % 22.52/3.79 % (354304)Termination phase: Preprocessing 3 % 22.52/3.79 % (354304)Time elapsed: 0.066 s % 22.52/3.79 % (354304)Peak memory usage: 20 MB % 22.52/3.79 % (354304)Instructions burned: 105 (million) % 22.52/3.79 % (354306)Instruction limit reached! % 22.52/3.79 % (354306)------------------------------ % 22.52/3.79 % (354306)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.52/3.79 % (354306)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.52/3.79 % (354306)CaDiCaL version: 2.1.3 % 22.52/3.79 % (354306)Termination reason: Instruction limit % 22.52/3.79 % (354306)Termination phase: Preprocessing 3 % 22.52/3.79 % (354306)Time elapsed: 0.081 s % 22.52/3.79 % (354306)Peak memory usage: 20 MB % 22.52/3.79 % (354306)Instructions burned: 132 (million) % 22.52/3.79 % (354317)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2279985608:i=131:bd=preordered:fsd=on_2995 on theBenchmark for (2995ds/131Mi) % 22.52/3.79 % (354307)Instruction limit reached! % 22.52/3.79 % (354307)------------------------------ % 22.52/3.79 % (354307)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.52/3.79 % (354307)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.52/3.79 % (354307)CaDiCaL version: 2.1.3 % 22.52/3.79 % (354307)Termination reason: Instruction limit % 22.52/3.79 % (354307)Termination phase: Clausification % 22.52/3.79 % (354307)Time elapsed: 0.099 s % 22.52/3.79 % (354307)Peak memory usage: 21 MB % 22.52/3.79 % (354307)Instructions burned: 160 (million) % 22.52/3.79 % (354318)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=901507058:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2995 on theBenchmark for (2995ds/684Mi) % 22.52/3.79 % (354320)ott-21_1_sil=16000:fs=off:random_seed=745388062:i=180:av=off:fsr=off_2995 on theBenchmark for (2995ds/180Mi) % 22.52/3.79 % (354317)Instruction limit reached! % 22.52/3.79 % (354317)------------------------------ % 22.52/3.79 % (354317)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.52/3.79 % (354317)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.52/3.79 % (354317)CaDiCaL version: 2.1.3 % 22.52/3.79 % (354317)Termination reason: Instruction limit % 50.31/7.77 % (354317)Termination phase: Preprocessing 3 % 50.31/7.77 % (354317)Time elapsed: 0.080 s % 50.31/7.77 % (354317)Peak memory usage: 20 MB % 50.31/7.77 % (354317)Instructions burned: 132 (million) % 50.31/7.77 % (354323)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1368786395:i=477:bd=all_2994 on theBenchmark for (2994ds/477Mi) % 50.31/7.77 % (354320)Instruction limit reached! % 50.31/7.77 % (354320)------------------------------ % 50.31/7.77 % (354320)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 50.31/7.77 % (354320)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 50.31/7.77 % (354320)CaDiCaL version: 2.1.3 % 50.31/7.77 % (354320)Termination reason: Instruction limit % 50.31/7.77 % (354320)Termination phase: Property scanning % 50.31/7.77 % (354320)Time elapsed: 0.105 s % 50.31/7.77 % (354320)Peak memory usage: 21 MB % 50.31/7.77 % (354320)Instructions burned: 182 (million) % 50.31/7.77 % (354315)Instruction limit reached! % 50.31/7.77 % (354315)------------------------------ % 50.31/7.77 % (354315)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 50.31/7.77 % (354315)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 50.31/7.77 % (354315)CaDiCaL version: 2.1.3 % 50.31/7.77 % (354315)Termination reason: Instruction limit % 50.31/7.77 % (354315)Termination phase: Finite model building preprocessing % 50.31/7.77 % (354315)Time elapsed: 0.182 s % 50.31/7.77 % (354315)Peak memory usage: 25 MB % 50.31/7.77 % (354315)Instructions burned: 716 (million) % 50.31/7.77 % (354326)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=4266429068:i=1179_2993 on theBenchmark for (2993ds/1179Mi) % 50.31/7.77 % (354325)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1236177022:fmbsr=1.3:i=865:ins=25_2993 on theBenchmark for (2993ds/865Mi) % 50.31/7.77 % (354323)Instruction limit reached! % 50.31/7.77 % (354323)------------------------------ % 50.31/7.77 % (354323)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 50.31/7.77 % (354323)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 50.31/7.77 % (354323)CaDiCaL version: 2.1.3 % 50.31/7.77 % (354323)Termination reason: Instruction limit % 50.31/7.77 % (354323)Termination phase: Property scanning % 50.31/7.77 % (354323)Time elapsed: 0.223 s % 50.31/7.77 % (354323)Peak memory usage: 23 MB % 50.31/7.77 % (354323)Instructions burned: 479 (million) % 50.31/7.77 % (354318)Instruction limit reached! % 50.31/7.77 % (354318)------------------------------ % 50.31/7.77 % (354318)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 50.31/7.77 % (354318)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 50.31/7.77 % (354318)CaDiCaL version: 2.1.3 % 50.31/7.77 % (354318)Termination reason: Instruction limit % 50.31/7.77 % (354318)Termination phase: Saturation % 50.31/7.77 % (354318)Time elapsed: 0.325 s % 50.31/7.77 % (354318)Peak memory usage: 24 MB % 50.31/7.77 % (354318)Instructions burned: 686 (million) % 50.31/7.77 % (354329)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=145413097:i=889:ins=1_2992 on theBenchmark for (2992ds/889Mi) % 50.31/7.77 % (354330)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=715516574:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2991 on theBenchmark for (2991ds/692Mi) % 50.31/7.77 % (354326)Instruction limit reached! % 50.31/7.77 % (354326)------------------------------ % 50.31/7.77 % (354326)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 50.31/7.77 % (354326)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 50.31/7.77 % (354326)CaDiCaL version: 2.1.3 % 50.31/7.77 % (354326)Termination reason: Instruction limit % 50.31/7.77 % (354326)Termination phase: Saturation % 50.31/7.77 % (354326)Time elapsed: 0.344 s % 50.31/7.77 % (354326)Peak memory usage: 30 MB % 50.31/7.77 % (354326)Instructions burned: 1181 (million) % 50.31/7.77 % (354333)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3098569595:i=879:kws=inv_precedence:fsr=off_2990 on theBenchmark for (2990ds/879Mi) % 50.31/7.77 % (354325)Instruction limit reached! % 50.31/7.77 % (354325)------------------------------ % 50.31/7.77 % (354325)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 50.31/7.77 % (354325)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 50.31/7.77 % (354325)CaDiCaL version: 2.1.3 % 50.31/7.77 % (354325)Termination reason: Instruction limit % 50.31/7.77 % (354325)Termination phase: Finite model building preprocessing % 102.87/15.05 % (354325)Time elapsed: 0.408 s % 102.87/15.05 % (354325)Peak memory usage: 30 MB % 102.87/15.05 % (354325)Instructions burned: 865 (million) % 102.87/15.05 % (354335)fmb+10_1_sil=64000:random_seed=2003036284:i=22061:nm=2:gsp=on_2989 on theBenchmark for (2989ds/22061Mi) % 102.87/15.05 % (354330)Instruction limit reached! % 102.87/15.05 % (354330)------------------------------ % 102.87/15.05 % (354330)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 102.87/15.05 % (354330)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 102.87/15.05 % (354330)CaDiCaL version: 2.1.3 % 102.87/15.05 % (354330)Termination reason: Instruction limit % 102.87/15.05 % (354330)Termination phase: Saturation % 102.87/15.05 % (354330)Time elapsed: 0.347 s % 102.87/15.05 % (354330)Peak memory usage: 28 MB % 102.87/15.05 % (354330)Instructions burned: 692 (million) % 102.87/15.05 % (354337)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1912068760:i=9515:nm=5_2988 on theBenchmark for (2988ds/9515Mi) % 102.87/15.05 % (354333)Instruction limit reached! % 102.87/15.05 % (354333)------------------------------ % 102.87/15.05 % (354333)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 102.87/15.05 % (354333)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 102.87/15.05 % (354333)CaDiCaL version: 2.1.3 % 102.87/15.05 % (354333)Termination reason: Instruction limit % 102.87/15.05 % (354333)Termination phase: Saturation % 102.87/15.05 % (354333)Time elapsed: 0.231 s % 102.87/15.05 % (354333)Peak memory usage: 30 MB % 102.87/15.05 % (354333)Instructions burned: 883 (million) % 102.87/15.05 % (354339)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2427405700:fmbsr=1.7:i=920_2987 on theBenchmark for (2987ds/920Mi) % 102.87/15.05 % (354329)Instruction limit reached! % 102.87/15.05 % (354329)------------------------------ % 102.87/15.05 % (354329)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 102.87/15.05 % (354329)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 102.87/15.05 % (354329)CaDiCaL version: 2.1.3 % 102.87/15.05 % (354329)Termination reason: Instruction limit % 102.87/15.05 % (354329)Termination phase: Finite model building preprocessing % 102.87/15.05 % (354329)Time elapsed: 0.421 s % 102.87/15.05 % (354329)Peak memory usage: 31 MB % 102.87/15.05 % (354329)Instructions burned: 891 (million) % 102.87/15.05 % (354341)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2627485164:i=5131_2987 on theBenchmark for (2987ds/5131Mi) % 102.87/15.05 % (354339)Instruction limit reached! % 102.87/15.05 % (354339)------------------------------ % 102.87/15.05 % (354339)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 102.87/15.05 % (354339)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 102.87/15.05 % (354339)CaDiCaL version: 2.1.3 % 102.87/15.05 % (354339)Termination reason: Instruction limit % 102.87/15.05 % (354339)Termination phase: Finite model building preprocessing % 102.87/15.05 % (354339)Time elapsed: 0.240 s % 102.87/15.05 % (354339)Peak memory usage: 32 MB % 102.87/15.05 % (354339)Instructions burned: 920 (million) % 102.87/15.05 % (354343)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3601349113:i=1472:ins=7:fdi=8:gsp=on_2985 on theBenchmark for (2985ds/1472Mi) % 102.87/15.05 % (354343)Instruction limit reached! % 102.87/15.05 % (354343)------------------------------ % 102.87/15.05 % (354343)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 102.87/15.05 % (354343)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 102.87/15.05 % (354343)CaDiCaL version: 2.1.3 % 102.87/15.05 % (354343)Termination reason: Instruction limit % 102.87/15.05 % (354343)Termination phase: Saturation % 102.87/15.05 % (354343)Time elapsed: 0.343 s % 102.87/15.05 % (354343)Peak memory usage: 28 MB % 102.87/15.05 % (354343)Instructions burned: 1474 (million) % 102.87/15.05 % (354345)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=2461039900:i=6324_2981 on theBenchmark for (2981ds/6324Mi) % 102.87/15.05 % (354345)Instruction limit reached! % 102.87/15.05 % (354345)------------------------------ % 102.87/15.05 % (354345)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 102.87/15.05 % (354345)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 102.87/15.05 % (354345)CaDiCaL version: 2.1.3 % 102.87/15.05 % (354345)Termination reason: Instruction limit % 102.87/15.05 % (354345)Termination phase: Finite model building preprocessing % 102.87/15.05 % (354345)Time elapsed: 1.711 s % 102.87/15.05 % (354345)Peak memory usage: 66 MB % 102.87/15.05 % (354345)Instructions burned: 6324 (million) % 199.82/28.75 % (354347)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=733270237:fmbsr=2.30978:i=2174_2964 on theBenchmark for (2964ds/2174Mi) % 199.82/28.75 % (354341)Instruction limit reached! % 199.82/28.75 % (354341)------------------------------ % 199.82/28.75 % (354341)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 199.82/28.75 % (354341)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 199.82/28.75 % (354341)CaDiCaL version: 2.1.3 % 199.82/28.75 % (354341)Termination reason: Instruction limit % 199.82/28.75 % (354341)Termination phase: Saturation % 199.82/28.75 % (354341)Time elapsed: 2.498 s % 199.82/28.75 % (354341)Peak memory usage: 51 MB % 199.82/28.75 % (354341)Instructions burned: 5132 (million) % 199.82/28.75 % (354349)ott-2_1_sil=16000:newcnf=on:random_seed=663838736:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2962 on theBenchmark for (2962ds/869Mi) % 199.82/28.75 % (354347)Instruction limit reached! % 199.82/28.75 % (354347)------------------------------ % 199.82/28.75 % (354347)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 199.82/28.75 % (354347)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 199.82/28.75 % (354347)CaDiCaL version: 2.1.3 % 199.82/28.75 % (354347)Termination reason: Instruction limit % 199.82/28.75 % (354347)Termination phase: Finite model building preprocessing % 199.82/28.75 % (354347)Time elapsed: 0.555 s % 199.82/28.75 % (354347)Peak memory usage: 48 MB % 199.82/28.75 % (354347)Instructions burned: 2177 (million) % 199.82/28.75 % (354351)ott+10_1_sil=32000:tgt=ground:random_seed=2807918549:i=5114:av=off_2958 on theBenchmark for (2958ds/5114Mi) % 199.82/28.75 % (354349)Instruction limit reached! % 199.82/28.75 % (354349)------------------------------ % 199.82/28.75 % (354349)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 199.82/28.75 % (354349)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 199.82/28.75 % (354349)CaDiCaL version: 2.1.3 % 199.82/28.75 % (354349)Termination reason: Instruction limit % 199.82/28.75 % (354349)Termination phase: Saturation % 199.82/28.75 % (354349)Time elapsed: 0.447 s % 199.82/28.75 % (354349)Peak memory usage: 28 MB % 199.82/28.75 % (354349)Instructions burned: 869 (million) % 199.82/28.75 % (354353)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2864468668:i=54282_2957 on theBenchmark for (2957ds/54282Mi) % 199.82/28.75 % (354351)Instruction limit reached! % 199.82/28.75 % (354351)------------------------------ % 199.82/28.75 % (354351)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 199.82/28.75 % (354351)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 199.82/28.75 % (354351)CaDiCaL version: 2.1.3 % 199.82/28.75 % (354351)Termination reason: Instruction limit % 199.82/28.75 % (354351)Termination phase: Saturation % 199.82/28.75 % (354351)Time elapsed: 1.680 s % 199.82/28.75 % (354351)Peak memory usage: 65 MB % 199.82/28.75 % (354351)Instructions burned: 5117 (million) % 199.82/28.75 % (354355)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=1717257767:i=3512:aac=none_2941 on theBenchmark for (2941ds/3512Mi) % 199.82/28.75 % (354337)Instruction limit reached! % 199.82/28.75 % (354337)------------------------------ % 199.82/28.75 % (354337)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 199.82/28.75 % (354337)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 199.82/28.75 % (354337)CaDiCaL version: 2.1.3 % 199.82/28.75 % (354337)Termination reason: Instruction limit % 199.82/28.75 % (354337)Termination phase: Finite model building preprocessing % 199.82/28.75 % (354337)Time elapsed: 4.925 s % 199.82/28.75 % (354337)Peak memory usage: 96 MB % 199.82/28.75 % (354337)Instructions burned: 9515 (million) % 199.82/28.75 % (354357)dis+21_1_sil=32000:sas=cadical:random_seed=3607053223:i=3773:amm=off_2938 on theBenchmark for (2938ds/3773Mi) % 199.82/28.75 % (354355)Instruction limit reached! % 199.82/28.75 % (354355)------------------------------ % 199.82/28.75 % (354355)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 199.82/28.75 % (354355)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 199.82/28.75 % (354355)CaDiCaL version: 2.1.3 % 199.82/28.75 % (354355)Termination reason: Instruction limit % 199.82/28.75 % (354355)Termination phase: Saturation % 199.82/28.75 % (354355)Time elapsed: 1.046 s % 199.82/28.75 % (354355)Peak memory usage: 51 MB % 199.82/28.75 % (354355)Instructions burned: 3515 (million) % 199.82/28.75 % (354359)ott+11_1_sil=16000:gs=on:random_seed=2381610452:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2931 on theBenchmark for (2931ds/2251Mi) % 199.82/28.75 % (354359)Instruction limit reached! % 262.34/38.72 % (354359)------------------------------ % 262.34/38.72 % (354359)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 262.34/38.72 % (354359)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 262.34/38.72 % (354359)CaDiCaL version: 2.1.3 % 262.34/38.72 % (354359)Termination reason: Instruction limit % 262.34/38.72 % (354359)Termination phase: Saturation % 262.34/38.72 % (354359)Time elapsed: 0.639 s % 262.34/38.72 % (354359)Peak memory usage: 34 MB % 262.34/38.72 % (354359)Instructions burned: 2253 (million) % 262.34/38.72 % (354361)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=2451063917:fmbsr=1.6:i=67534_2924 on theBenchmark for (2924ds/67534Mi) % 262.34/38.72 % (354357)Instruction limit reached! % 262.34/38.72 % (354357)------------------------------ % 262.34/38.72 % (354357)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 262.34/38.72 % (354357)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 262.34/38.72 % (354357)CaDiCaL version: 2.1.3 % 262.34/38.72 % (354357)Termination reason: Instruction limit % 262.34/38.72 % (354357)Termination phase: Saturation % 262.34/38.72 % (354357)Time elapsed: 2.107 s % 262.34/38.72 % (354357)Peak memory usage: 56 MB % 262.34/38.72 % (354357)Instructions burned: 3774 (million) % 262.34/38.72 % (354363)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=3607064984:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2917 on theBenchmark for (2917ds/4591Mi) % 262.34/38.72 % (354363)Instruction limit reached! % 262.34/38.72 % (354363)------------------------------ % 262.34/38.72 % (354363)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 262.34/38.72 % (354363)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 262.34/38.72 % (354363)CaDiCaL version: 2.1.3 % 262.34/38.72 % (354363)Termination reason: Instruction limit % 262.34/38.72 % (354363)Termination phase: Saturation % 262.34/38.72 % (354363)Time elapsed: 1.711 s % 262.34/38.72 % (354363)Peak memory usage: 31 MB % 262.34/38.72 % (354363)Instructions burned: 4593 (million) % 262.34/38.72 % (354365)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=2689576908:i=29340_2899 on theBenchmark for (2899ds/29340Mi) % 262.34/38.72 % (354335)Instruction limit reached! % 262.34/38.72 % (354335)------------------------------ % 262.34/38.72 % (354335)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 262.34/38.72 % (354335)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 262.34/38.72 % (354335)CaDiCaL version: 2.1.3 % 262.34/38.72 % (354335)Termination reason: Instruction limit % 262.34/38.72 % (354335)Termination phase: Finite model building preprocessing % 262.34/38.72 % (354335)Time elapsed: 11.561 s % 262.34/38.72 % (354335)Peak memory usage: 214 MB % 262.34/38.72 % (354335)Instructions burned: 22061 (million) % 262.34/38.72 % (354367)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=2443517608:i=5211_2873 on theBenchmark for (2873ds/5211Mi) % 262.34/38.72 % TRYING [1] % 262.34/38.72 % TRYING [2] % 262.34/38.72 % (354361)Cannot represent all propositional literals internally % 262.34/38.72 % (354361)Refutation not found, incomplete strategy % 262.34/38.72 % (354361)------------------------------ % 262.34/38.72 % (354361)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 262.34/38.72 % (354361)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 262.34/38.72 % (354361)CaDiCaL version: 2.1.3 % 262.34/38.72 % (354361)Termination reason: Refutation not found, incomplete strategy % 262.34/38.72 % (354361)Time elapsed: 6.638 s % 262.34/38.72 % (354361)Peak memory usage: 189 MB % 262.34/38.72 % (354361)Instructions burned: 23575 (million) % 262.34/38.72 % (354361)------------------------------ % 262.34/38.72 % (354361)------------------------------ % 262.34/38.72 % (354369)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=3243028539:i=5497:nm=2_2857 on theBenchmark for (2857ds/5497Mi) % 262.34/38.72 % (354367)Instruction limit reached! % 262.34/38.72 % (354367)------------------------------ % 262.34/38.72 % (354367)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 262.34/38.72 % (354367)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 262.34/38.72 % (354367)CaDiCaL version: 2.1.3 % 262.34/38.72 % (354367)Termination reason: Instruction limit % 262.34/38.72 % (354367)Termination phase: Saturation % 262.34/38.72 % (354367)Time elapsed: 2.122 s % 262.34/38.72 % (354367)Peak memory usage: 45 MB % 262.34/38.72 % (354367)Instructions burned: 5212 (million) % 262.34/38.72 % (354371)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=1501280001:fmbsr=Terminated %------------------------------------------------------------------------------