%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWV635-1 : TPTP v9.3.1. Released v4.1.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % Computer : n015.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:26:10 PM UTC 2026 % Result : Timeout 300.05s 42.64s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWV635-1 : TPTP v9.3.1. Released v4.1.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.06/0.21 % Computer : n015.cluster.edu % 0.06/0.21 % Model : x86_64 x86_64 % 0.06/0.21 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.06/0.21 % Memory : 8046.5625MB % 0.06/0.21 % OS : Linux 6.8.0-71-generic % 0.06/0.21 % CPULimit : 300 % 0.06/0.21 % WCLimit : 300 % 0.06/0.21 % DateTime : Mon Sep 28 12:10:17 UTC 2026 % 0.06/0.21 % CPUTime : % 0.06/0.21 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.06/0.25 Running first-order model finding % 0.06/0.25 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.55/2.56 % (2581282)Will run a generic schedule for satisfiability detection. % 15.55/2.56 % (2581290)dis+10_1_sil=32000:sp=arity:random_seed=2518441200:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 15.55/2.56 % (2581288)% WARNING: option uhcvi not known. % 15.55/2.56 % (2581287)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1864012970_2999 on theBenchmark for (2999ds/0Mi) % 15.55/2.56 % (2581288)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2350203782:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 15.55/2.56 % (2581289)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3342387391:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 15.55/2.56 % (2581291)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1525690615:i=116_2999 on theBenchmark for (2999ds/116Mi) % 15.55/2.56 % (2581293)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3093233698:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 15.55/2.56 % (2581292)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=782818881:i=131_2999 on theBenchmark for (2999ds/131Mi) % 15.55/2.56 % (2581290)Instruction limit reached! % 15.55/2.56 % (2581290)------------------------------ % 15.55/2.56 % (2581290)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 15.55/2.56 % (2581290)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.55/2.56 % (2581290)CaDiCaL version: 2.1.3 % 15.55/2.56 % (2581290)Termination reason: Instruction limit % 15.55/2.56 % (2581290)Termination phase: Saturation % 15.55/2.56 % (2581290)Time elapsed: 0.037 s % 15.55/2.56 % (2581290)Peak memory usage: 14 MB % 15.55/2.56 % (2581290)Instructions burned: 105 (million) % 15.55/2.56 % (2581301)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2448616429:i=714:nm=2_2998 on theBenchmark for (2998ds/714Mi) % 15.55/2.56 % (2581291)Instruction limit reached! % 15.55/2.56 % (2581291)------------------------------ % 15.55/2.56 % (2581291)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 15.55/2.56 % (2581291)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.55/2.56 % (2581291)CaDiCaL version: 2.1.3 % 15.55/2.56 % (2581291)Termination reason: Instruction limit % 15.55/2.56 % (2581291)Termination phase: Saturation % 15.55/2.56 % (2581291)Time elapsed: 0.074 s % 15.55/2.56 % (2581291)Peak memory usage: 14 MB % 15.55/2.56 % (2581291)Instructions burned: 116 (million) % 15.55/2.56 % (2581292)Instruction limit reached! % 15.55/2.56 % (2581292)------------------------------ % 15.55/2.56 % (2581292)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 15.55/2.56 % (2581292)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.55/2.56 % (2581292)CaDiCaL version: 2.1.3 % 15.55/2.56 % (2581292)Termination reason: Instruction limit % 15.55/2.56 % (2581292)Termination phase: Saturation % 15.55/2.56 % (2581292)Time elapsed: 0.072 s % 15.55/2.56 % (2581292)Peak memory usage: 13 MB % 15.55/2.56 % (2581292)Instructions burned: 133 (million) % 15.55/2.56 % (2581304)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=148429114:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi) % 15.55/2.56 % (2581303)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=771267558:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi) % 15.55/2.56 % TRYING [1] % 15.55/2.56 % TRYING [2] % 15.55/2.56 % (2581293)Instruction limit reached! % 15.55/2.56 % (2581293)------------------------------ % 15.55/2.56 % (2581293)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 15.55/2.56 % (2581293)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.55/2.56 % (2581293)CaDiCaL version: 2.1.3 % 15.55/2.56 % (2581293)Termination reason: Instruction limit % 15.55/2.56 % (2581293)Termination phase: Saturation % 15.55/2.56 % (2581293)Time elapsed: 0.103 s % 15.55/2.56 % (2581293)Peak memory usage: 14 MB % 15.55/2.56 % (2581293)Instructions burned: 159 (million) % 15.55/2.56 % TRYING [1] % 15.55/2.56 % TRYING [2] % 15.55/2.56 % (2581307)ott-21_1_sil=16000:fs=off:random_seed=898192356:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 15.55/2.56 % TRYING [3] % 15.55/2.56 % (2581303)Instruction limit reached! % 15.55/2.56 % (2581303)------------------------------ % 15.55/2.56 % (2581303)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 15.55/2.56 % (2581303)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.72/5.99 % (2581303)CaDiCaL version: 2.1.3 % 39.72/5.99 % (2581303)Termination reason: Instruction limit % 39.72/5.99 % (2581303)Termination phase: Saturation % 39.72/5.99 % (2581303)Time elapsed: 0.082 s % 39.72/5.99 % (2581303)Peak memory usage: 14 MB % 39.72/5.99 % (2581303)Instructions burned: 132 (million) % 39.72/5.99 % TRYING [3] % 39.72/5.99 % (2581301)Instruction limit reached! % 39.72/5.99 % (2581301)------------------------------ % 39.72/5.99 % (2581301)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 39.72/5.99 % (2581301)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.72/5.99 % (2581301)CaDiCaL version: 2.1.3 % 39.72/5.99 % (2581301)Termination reason: Instruction limit % 39.72/5.99 % (2581301)Termination phase: Finite model building constraint generation % 39.72/5.99 % (2581301)Time elapsed: 0.149 s % 39.72/5.99 % (2581301)Peak memory usage: 32 MB % 39.72/5.99 % (2581301)Instructions burned: 718 (million) % 39.72/5.99 % (2581309)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3139582928:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi) % 39.72/5.99 % (2581310)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=4231234007:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi) % 39.72/5.99 % (2581307)Instruction limit reached! % 39.72/5.99 % (2581307)------------------------------ % 39.72/5.99 % (2581307)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 39.72/5.99 % (2581307)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.72/5.99 % (2581307)CaDiCaL version: 2.1.3 % 39.72/5.99 % (2581307)Termination reason: Instruction limit % 39.72/5.99 % (2581307)Termination phase: Saturation % 39.72/5.99 % (2581307)Time elapsed: 0.096 s % 39.72/5.99 % (2581307)Peak memory usage: 14 MB % 39.72/5.99 % (2581307)Instructions burned: 182 (million) % 39.72/5.99 % (2581313)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2571531990:i=1179_2996 on theBenchmark for (2996ds/1179Mi) % 39.72/5.99 % TRYING [1] % 39.72/5.99 % TRYING [2] % 39.72/5.99 % (2581310)Instruction limit reached! % 39.72/5.99 % (2581310)------------------------------ % 39.72/5.99 % (2581310)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 39.72/5.99 % (2581310)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.72/5.99 % (2581310)CaDiCaL version: 2.1.3 % 39.72/5.99 % (2581310)Termination reason: Instruction limit % 39.72/5.99 % (2581310)Termination phase: Finite model building SAT solving % 39.72/5.99 % (2581310)Time elapsed: 0.210 s % 39.72/5.99 % (2581310)Peak memory usage: 31 MB % 39.72/5.99 % (2581310)Instructions burned: 869 (million) % 39.72/5.99 % (2581315)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3511101220:i=889:ins=1_2995 on theBenchmark for (2995ds/889Mi) % 39.72/5.99 % (2581304)Instruction limit reached! % 39.72/5.99 % (2581304)------------------------------ % 39.72/5.99 % (2581304)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 39.72/5.99 % (2581304)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.72/5.99 % (2581304)CaDiCaL version: 2.1.3 % 39.72/5.99 % (2581304)Termination reason: Instruction limit % 39.72/5.99 % (2581304)Termination phase: Saturation % 39.72/5.99 % (2581304)Time elapsed: 0.386 s % 39.72/5.99 % (2581304)Peak memory usage: 18 MB % 39.72/5.99 % (2581304)Instructions burned: 684 (million) % 39.72/5.99 % (2581317)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=149840653: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) % 39.72/5.99 % (2581309)Instruction limit reached! % 39.72/5.99 % (2581309)------------------------------ % 39.72/5.99 % (2581309)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 39.72/5.99 % (2581309)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.72/5.99 % (2581309)CaDiCaL version: 2.1.3 % 39.72/5.99 % (2581309)Termination reason: Instruction limit % 39.72/5.99 % (2581309)Termination phase: Saturation % 39.72/5.99 % (2581309)Time elapsed: 0.319 s % 39.72/5.99 % (2581309)Peak memory usage: 15 MB % 39.72/5.99 % (2581309)Instructions burned: 478 (million) % 39.72/5.99 % (2581319)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3919181257:i=879:kws=inv_precedence:fsr=off_2994 on theBenchmark for (2994ds/879Mi) % 39.72/5.99 % TRYING [4] % 39.72/5.99 % (2581315)Instruction limit reached! % 39.72/5.99 % (2581315)------------------------------ % 39.72/5.99 % (2581315)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 83.24/12.04 % (2581315)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 83.24/12.04 % (2581315)CaDiCaL version: 2.1.3 % 83.24/12.04 % (2581315)Termination reason: Instruction limit % 83.24/12.04 % (2581315)Termination phase: Finite model building constraint generation % 83.24/12.04 % (2581315)Time elapsed: 0.263 s % 83.24/12.04 % (2581315)Peak memory usage: 96 MB % 83.24/12.04 % (2581315)Instructions burned: 890 (million) % 83.24/12.04 % (2581321)fmb+10_1_sil=64000:random_seed=1044993899:i=22061:nm=2:gsp=on_2992 on theBenchmark for (2992ds/22061Mi) % 83.24/12.04 % TRYING [1] % 83.24/12.04 % TRYING [2] % 83.24/12.04 % (2581317)Instruction limit reached! % 83.24/12.04 % (2581317)------------------------------ % 83.24/12.04 % (2581317)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 83.24/12.04 % (2581317)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 83.24/12.04 % (2581317)CaDiCaL version: 2.1.3 % 83.24/12.04 % (2581317)Termination reason: Instruction limit % 83.24/12.04 % (2581317)Termination phase: Saturation % 83.24/12.04 % (2581317)Time elapsed: 0.405 s % 83.24/12.04 % (2581317)Peak memory usage: 18 MB % 83.24/12.04 % (2581317)Instructions burned: 694 (million) % 83.24/12.04 % (2581323)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3823841803:i=9515:nm=5_2990 on theBenchmark for (2990ds/9515Mi) % 83.24/12.04 % TRYING [3] % 83.24/12.04 % (2581313)Instruction limit reached! % 83.24/12.04 % (2581313)------------------------------ % 83.24/12.04 % (2581313)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 83.24/12.04 % (2581313)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 83.24/12.04 % (2581313)CaDiCaL version: 2.1.3 % 83.24/12.04 % (2581313)Termination reason: Instruction limit % 83.24/12.04 % (2581313)Termination phase: Saturation % 83.24/12.04 % (2581313)Time elapsed: 0.724 s % 83.24/12.04 % (2581313)Peak memory usage: 20 MB % 83.24/12.04 % (2581313)Instructions burned: 1179 (million) % 83.24/12.04 % (2581325)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=822071368:fmbsr=1.7:i=920_2989 on theBenchmark for (2989ds/920Mi) % 83.24/12.04 % (2581319)Instruction limit reached! % 83.24/12.04 % (2581319)------------------------------ % 83.24/12.04 % (2581319)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 83.24/12.04 % (2581319)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 83.24/12.04 % (2581319)CaDiCaL version: 2.1.3 % 83.24/12.04 % (2581319)Termination reason: Instruction limit % 83.24/12.04 % (2581319)Termination phase: Saturation % 83.24/12.04 % (2581319)Time elapsed: 0.485 s % 83.24/12.04 % (2581319)Peak memory usage: 21 MB % 83.24/12.04 % (2581319)Instructions burned: 880 (million) % 83.24/12.04 % (2581327)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1666651316:i=5131_2988 on theBenchmark for (2988ds/5131Mi) % 83.24/12.04 % TRYING [20] % 83.24/12.04 % TRYING [8] % 83.24/12.04 % (2581325)Instruction limit reached! % 83.24/12.04 % (2581325)------------------------------ % 83.24/12.04 % (2581325)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 83.24/12.04 % (2581325)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 83.24/12.04 % (2581325)CaDiCaL version: 2.1.3 % 83.24/12.04 % (2581325)Termination reason: Instruction limit % 83.24/12.04 % (2581325)Termination phase: Finite model building constraint generation % 83.24/12.04 % (2581325)Time elapsed: 0.338 s % 83.24/12.04 % (2581325)Peak memory usage: 57 MB % 83.24/12.04 % (2581325)Instructions burned: 921 (million) % 83.24/12.04 % (2581329)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=776495672:i=1472:ins=7:fdi=8:gsp=on_2985 on theBenchmark for (2985ds/1472Mi) % 83.24/12.04 % TRYING [4] % 83.24/12.04 % TRYING [5] % 83.24/12.04 % (2581329)Instruction limit reached! % 83.24/12.04 % (2581329)------------------------------ % 83.24/12.04 % (2581329)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 83.24/12.04 % (2581329)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 83.24/12.04 % (2581329)CaDiCaL version: 2.1.3 % 83.24/12.04 % (2581329)Termination reason: Instruction limit % 83.24/12.04 % (2581329)Termination phase: Saturation % 83.24/12.04 % (2581329)Time elapsed: 0.749 s % 83.24/12.04 % (2581329)Peak memory usage: 25 MB % 83.24/12.04 % (2581329)Instructions burned: 1474 (million) % 83.24/12.04 % (2581331)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=1275206398:i=6324_2978 on theBenchmark for (2978ds/6324Mi) % 83.24/12.04 % (2581331)Cannot represent all propositional literals internally % 83.24/12.04 % (2581331)Refutation not found, incomplete strategy % 83.24/12.04 % (2581331)------------------------------ % 206.42/29.48 % (2581331)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 206.42/29.48 % (2581331)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 206.42/29.48 % (2581331)CaDiCaL version: 2.1.3 % 206.42/29.48 % (2581331)Termination reason: Refutation not found, incomplete strategy % 206.42/29.48 % (2581331)Time elapsed: 0.110 s % 206.42/29.48 % (2581331)Peak memory usage: 16 MB % 206.42/29.48 % (2581331)Instructions burned: 225 (million) % 206.42/29.48 % (2581331)------------------------------ % 206.42/29.48 % (2581331)------------------------------ % 206.42/29.48 % (2581333)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=186800752:fmbsr=2.30978:i=2174_2976 on theBenchmark for (2976ds/2174Mi) % 206.42/29.48 % TRYING [16] % 206.42/29.48 % (2581333)Instruction limit reached! % 206.42/29.48 % (2581333)------------------------------ % 206.42/29.48 % (2581333)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 206.42/29.48 % (2581333)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 206.42/29.48 % (2581333)CaDiCaL version: 2.1.3 % 206.42/29.48 % (2581333)Termination reason: Instruction limit % 206.42/29.48 % (2581333)Termination phase: Finite model building constraint generation % 206.42/29.48 % (2581333)Time elapsed: 0.902 s % 206.42/29.48 % (2581333)Peak memory usage: 90 MB % 206.42/29.48 % (2581333)Instructions burned: 2175 (million) % 206.42/29.48 % (2581335)ott-2_1_sil=16000:newcnf=on:random_seed=1161121249:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2967 on theBenchmark for (2967ds/869Mi) % 206.42/29.48 % (2581335)Instruction limit reached! % 206.42/29.48 % (2581335)------------------------------ % 206.42/29.48 % (2581335)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 206.42/29.48 % (2581335)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 206.42/29.48 % (2581335)CaDiCaL version: 2.1.3 % 206.42/29.48 % (2581335)Termination reason: Instruction limit % 206.42/29.48 % (2581335)Termination phase: Saturation % 206.42/29.48 % (2581335)Time elapsed: 0.536 s % 206.42/29.48 % (2581335)Peak memory usage: 20 MB % 206.42/29.48 % (2581335)Instructions burned: 869 (million) % 206.42/29.48 % (2581337)ott+10_1_sil=32000:tgt=ground:random_seed=2234286134:i=5114:av=off_2961 on theBenchmark for (2961ds/5114Mi) % 206.42/29.48 % (2581327)Instruction limit reached! % 206.42/29.48 % (2581327)------------------------------ % 206.42/29.48 % (2581327)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 206.42/29.48 % (2581327)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 206.42/29.48 % (2581327)CaDiCaL version: 2.1.3 % 206.42/29.48 % (2581327)Termination reason: Instruction limit % 206.42/29.48 % (2581327)Termination phase: Saturation % 206.42/29.48 % (2581327)Time elapsed: 2.962 s % 206.42/29.48 % (2581327)Peak memory usage: 37 MB % 206.42/29.48 % (2581327)Instructions burned: 5132 (million) % 206.42/29.48 % (2581339)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=4272667780:i=54282_2959 on theBenchmark for (2959ds/54282Mi) % 206.42/29.48 % TRYING [1] % 206.42/29.48 % TRYING [2] % 206.42/29.48 % TRYING [3] % 206.42/29.48 % (2581323)Instruction limit reached! % 206.42/29.48 % (2581323)------------------------------ % 206.42/29.48 % (2581323)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 206.42/29.48 % (2581323)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 206.42/29.48 % (2581323)CaDiCaL version: 2.1.3 % 206.42/29.48 % (2581323)Termination reason: Instruction limit % 206.42/29.48 % (2581323)Termination phase: Finite model building constraint generation % 206.42/29.48 % (2581323)Time elapsed: 3.357 s % 206.42/29.48 % (2581323)Peak memory usage: 571 MB % 206.42/29.48 % (2581323)Instructions burned: 9517 (million) % 206.42/29.48 % (2581341)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=1901333104:i=3512:aac=none_2955 on theBenchmark for (2955ds/3512Mi) % 206.42/29.48 % TRYING [4] % 206.42/29.48 % TRYING [5] % 206.42/29.48 % (2581321)Instruction limit reached! % 206.42/29.48 % (2581321)------------------------------ % 206.42/29.48 % (2581321)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 206.42/29.48 % (2581321)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 206.42/29.48 % (2581321)CaDiCaL version: 2.1.3 % 206.42/29.48 % (2581321)Termination reason: Instruction limit % 206.42/29.48 % (2581321)Termination phase: Finite model building constraint generation % 206.42/29.48 % (2581321)Time elapsed: 4.909 s % 206.42/29.48 % (2581321)Peak memory usage: 265 MB % 206.42/29.48 % (2581321)Instructions burned: 22061 (million) % 206.42/29.48 % (2581343)dis+21_1_sil=32000:sas=cadical:random_seed=3817140241:i=3773:amm=off_2942 on theBenchmark for (2942ds/3773Mi) % 282.56/40.15 % TRYING [6] % 282.56/40.15 % TRYING [5] % 282.56/40.15 % (2581341)Instruction limit reached! % 282.56/40.15 % (2581341)------------------------------ % 282.56/40.15 % (2581341)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 282.56/40.15 % (2581341)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 282.56/40.15 % (2581341)CaDiCaL version: 2.1.3 % 282.56/40.15 % (2581341)Termination reason: Instruction limit % 282.56/40.15 % (2581341)Termination phase: Saturation % 282.56/40.15 % (2581341)Time elapsed: 2.083 s % 282.56/40.15 % (2581341)Peak memory usage: 32 MB % 282.56/40.15 % (2581341)Instructions burned: 3512 (million) % 282.56/40.15 % (2581345)ott+11_1_sil=16000:gs=on:random_seed=1106346231:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2934 on theBenchmark for (2934ds/2251Mi) % 282.56/40.15 % (2581343)Instruction limit reached! % 282.56/40.15 % (2581343)------------------------------ % 282.56/40.15 % (2581343)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 282.56/40.15 % (2581343)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 282.56/40.15 % (2581343)CaDiCaL version: 2.1.3 % 282.56/40.15 % (2581343)Termination reason: Instruction limit % 282.56/40.15 % (2581343)Termination phase: Saturation % 282.56/40.15 % (2581343)Time elapsed: 1.183 s % 282.56/40.15 % (2581343)Peak memory usage: 36 MB % 282.56/40.15 % (2581343)Instructions burned: 3776 (million) % 282.56/40.15 % (2581347)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=2751462776:fmbsr=1.6:i=67534_2930 on theBenchmark for (2930ds/67534Mi) % 282.56/40.15 % (2581337)Instruction limit reached! % 282.56/40.15 % (2581337)------------------------------ % 282.56/40.15 % (2581337)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 282.56/40.15 % (2581337)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 282.56/40.15 % (2581337)CaDiCaL version: 2.1.3 % 282.56/40.15 % (2581337)Termination reason: Instruction limit % 282.56/40.15 % (2581337)Termination phase: Saturation % 282.56/40.15 % (2581337)Time elapsed: 3.307 s % 282.56/40.15 % (2581337)Peak memory usage: 35 MB % 282.56/40.15 % (2581337)Instructions burned: 5115 (million) % 282.56/40.15 % (2581349)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=4129850007:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2928 on theBenchmark for (2928ds/4591Mi) % 282.56/40.15 % TRYING [7] % 282.56/40.15 % (2581345)Instruction limit reached! % 282.56/40.15 % (2581345)------------------------------ % 282.56/40.15 % (2581345)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 282.56/40.15 % (2581345)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 282.56/40.15 % (2581345)CaDiCaL version: 2.1.3 % 282.56/40.15 % (2581345)Termination reason: Instruction limit % 282.56/40.15 % (2581345)Termination phase: Saturation % 282.56/40.15 % (2581345)Time elapsed: 1.394 s % 282.56/40.15 % (2581345)Peak memory usage: 40 MB % 282.56/40.15 % (2581345)Instructions burned: 2251 (million) % 282.56/40.15 % (2581351)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=625321789:i=29340_2920 on theBenchmark for (2920ds/29340Mi) % 282.56/40.15 % (2581349)Instruction limit reached! % 282.56/40.15 % (2581349)------------------------------ % 282.56/40.15 % (2581349)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 282.56/40.15 % (2581349)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 282.56/40.15 % (2581349)CaDiCaL version: 2.1.3 % 282.56/40.15 % (2581349)Termination reason: Instruction limit % 282.56/40.15 % (2581349)Termination phase: Saturation % 282.56/40.15 % (2581349)Time elapsed: 1.872 s % 282.56/40.15 % (2581349)Peak memory usage: 34 MB % 282.56/40.15 % (2581349)Instructions burned: 4592 (million) % 282.56/40.15 % (2581353)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=3945339440:i=5211_2909 on theBenchmark for (2909ds/5211Mi) % 282.56/40.15 % TRYING [6] % 282.56/40.15 % (2581353)Instruction limit reached! % 282.56/40.15 % (2581353)------------------------------ % 282.56/40.15 % (2581353)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 282.56/40.15 % (2581353)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 282.56/40.15 % (2581353)CaDiCaL version: 2.1.3 % 282.56/40.15 % (2581353)Termination reason: Instruction limit % 282.56/40.15 % (2581353)Termination phase: Saturation % 282.56/40.15 % (2581353)Time elapsed: 2.718 s % 282.56/40.15 % (2581353)Peak memory usage: 46 MB % 282.56/40.15 % (2581353)Instructions burned: 5211 (million) % 282.56/40.15 % (2581355)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=615272992:i=5497:nm=2_2882 on theBenchmark for (2882ds/5497Mi) % 300.05/42.64 % TRYING [17] % 300.05/42.64 % (2581355)Instruction limit reached! % 300.05/42.64 % (2581355)------------------------------ % 300.05/42.64 % (2581355)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.05/42.64 % (2581355)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.05/42.64 % (2581355)CaDiCaL version: 2.1.3 % 300.05/42.64 % (2581355)Termination reason: Instruction limit % 300.05/42.64 % (2581355)Termination phase: Finite model building constraint generation % 300.05/42.64 % (2581355)Time elapsed: 1.908 s % 300.05/42.64 % (2581355)Peak memory usage: 331 MB % 300.05/42.64 % (2581355)Instructions burned: 5499 (million) % 300.05/42.64 % (2581357)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=2296360273:fmbsr=2:i=46332_2862 on theBenchmark for (2862ds/46332Mi) % 300.05/42.64 % TRYING [15] % 300.05/42.64 % TRYING [7] % 300.05/42.64 % TRYING [7] % 300.05/42.64 % (2581351)Instruction limit reached! % 300.05/42.64 % (2581351)------------------------------ % 300.05/42.64 % (2581351)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.05/42.64 % (2581351)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.05/42.64 % (2581351)CaDiCaL version: 2.1.3 % 300.05/42.64 % (2581351)Termination reason: Instruction limit % 300.05/42.64 % (2581351)Termination phase: Saturation % 300.05/42.64 % (2581351)Time elapsed: 12.969 s % 300.05/42.64 % (2581351)Peak memory usage: 175 MB % 300.05/42.64 % (2581351)Instructions burned: 29341 (million) % 300.05/42.64 % (2581359)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=2970385899:i=14071_2790 on theBenchmark for (2790ds/14071Mi) % 300.05/42.64 % TRYING [12] % 300.05/42.64 % (2581347)Instruction limit reached! % 300.05/42.64 % (2581347)------------------------------ % 300.05/42.64 % (2581347)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.05/42.64 % (2581347)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.05/42.64 % (2581347)CaDiCaL version: 2.1.3 % 300.05/42.64 % (2581347)Termination reason: Instruction limit % 300.05/42.64 % (2581347)Termination phase: Finite model building constraint generation % 300.05/42.64 % (2581347)Time elapsed: 16.765 s % 300.05/42.64 % (2581347)Peak memory usage: 3539 MB % 300.05/42.64 % (2581347)Instructions burned: 67538 (million) % 300.05/42.64 % (2581361)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2821637174:i=22565:add=on:rawr=on_2759 on theBenchmark for (2759ds/22565Mi) % 300.05/42.64 % (2581339)Instruction limit reached! % 300.05/42.64 % (2581339)------------------------------ % 300.05/42.64 % (2581339)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.05/42.64 % (2581339)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.05/42.64 % (2581339)CaDiCaL version: 2.1.3 % 300.05/42.64 % (2581339)Termination reason: Instruction limit % 300.05/42.64 % (2581339)Termination phase: Finite model building constraint generation % 300.05/42.64 % (2581339)Time elapsed: 19.933 s % 300.05/42.64 % (2581339)Peak memory usage: 1426 MB % 300.05/42.64 % (2581339)Instructions burned: 54282 (million) % 300.05/42.64 % (2581363)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=2979525872:i=8173:av=off_2757 on theBenchmark for (2757ds/8173Mi) % 300.05/42.64 % (2581359)Instruction limit reached! % 300.05/42.64 % (2581359)------------------------------ % 300.05/42.64 % (2581359)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.05/42.64 % (2581359)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.05/42.64 % (2581359)CaDiCaL version: 2.1.3 % 300.05/42.64 % (2581359)Termination reason: Instruction limit % 300.05/42.64 % (2581359)Termination phase: Finite model building constraint generation % 300.05/42.64 % (2581359)Time elapsed: 4.788 s % 300.05/42.64 % (2581359)Peak memory usage: 816 MB % 300.05/42.64 % (2581359)Instructions burned: 14072 (million) % 300.05/42.64 % (2581365)dis+10_16:1_sil=16000:random_seed=1175497246:i=9155:fsr=off_2741 on theBenchmark for (2741ds/9155Mi) % 300.05/42.64 % (2581361)Instruction limit reached! % 300.05/42.64 % (2581361)------------------------------ % 300.05/42.64 % (2581361)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.05/42.64 % (2581361)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.05/42.64 % (2581361)CaDiCaL version: 2.1.3 % 300.05/42.64 % (2581361)Termination reason: Instruction limit % 300.05/42.64 % (2581361)Termination phase: Saturation % 300.05/42.64 % (2581361)Time elapsed: 5.172 s % 300.05/42.64 % (2581361)Peak memory usage: 37 MB % 300.05/42.64 % (2581361)Instructions burned: 22566 (million) % 300.05/42.64 % (2581367)ott-3_8_sil=64000:random_seed=21 % 300.05/42.64 Terminated % 300.05/42.64 % Vampire exiting % 300.05/42.64 Terminated %------------------------------------------------------------------------------