%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : NUM709+4 : TPTP v9.3.1. Released v7.3.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % Computer : n020.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:25:28 PM UTC 2026 % Result : Timeout 300.35s 42.93s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : NUM709+4 : TPTP v9.3.1. Released v7.3.0. % 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.16/0.42 % Computer : n020.cluster.edu % 0.16/0.42 % Model : x86_64 x86_64 % 0.16/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.16/0.42 % Memory : 8046.5625MB % 0.16/0.42 % OS : Linux 6.8.0-71-generic % 0.16/0.42 % CPULimit : 300 % 0.16/0.42 % WCLimit : 300 % 0.16/0.42 % DateTime : Sun Sep 27 21:12:34 UTC 2026 % 0.16/0.43 % CPUTime : % 0.16/0.43 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.20/0.47 Running first-order model finding % 0.20/0.48 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.18/3.72 % (3746280)Will run a generic schedule for satisfiability detection. % 22.18/3.72 % (3746289)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2057982698:i=116_2999 on theBenchmark for (2999ds/116Mi) % 22.18/3.72 % (3746291)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1611523687:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 22.18/3.72 % (3746286)% WARNING: option uhcvi not known. % 22.18/3.72 % (3746285)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=123612101_2999 on theBenchmark for (2999ds/0Mi) % 22.18/3.72 % (3746286)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3065674291:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 22.18/3.72 % (3746287)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2894819293:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 22.18/3.72 % (3746290)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3189606615:i=131_2999 on theBenchmark for (2999ds/131Mi) % 22.18/3.72 % (3746288)dis+10_1_sil=32000:sp=arity:random_seed=2684749661:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 22.18/3.72 % (3746289)Instruction limit reached! % 22.18/3.72 % (3746289)------------------------------ % 22.18/3.72 % (3746289)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.18/3.72 % (3746289)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.18/3.72 % (3746289)CaDiCaL version: 2.1.3 % 22.18/3.72 % (3746289)Termination reason: Instruction limit % 22.18/3.72 % (3746289)Termination phase: Saturation % 22.18/3.72 % (3746289)Time elapsed: 0.052 s % 22.18/3.72 % (3746289)Peak memory usage: 13 MB % 22.18/3.72 % (3746289)Instructions burned: 116 (million) % 22.18/3.72 % (3746299)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3173101891:i=714:nm=2_2998 on theBenchmark for (2998ds/714Mi) % 22.18/3.72 % (3746288)Instruction limit reached! % 22.18/3.72 % (3746288)------------------------------ % 22.18/3.72 % (3746288)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.18/3.72 % (3746288)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.18/3.72 % (3746288)CaDiCaL version: 2.1.3 % 22.18/3.72 % (3746288)Termination reason: Instruction limit % 22.18/3.72 % (3746288)Termination phase: Saturation % 22.18/3.72 % (3746288)Time elapsed: 0.099 s % 22.18/3.72 % (3746288)Peak memory usage: 13 MB % 22.18/3.72 % (3746288)Instructions burned: 104 (million) % 22.18/3.72 % (3746290)Instruction limit reached! % 22.18/3.72 % (3746290)------------------------------ % 22.18/3.72 % (3746290)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.18/3.72 % (3746290)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.18/3.72 % (3746290)CaDiCaL version: 2.1.3 % 22.18/3.72 % (3746290)Termination reason: Instruction limit % 22.18/3.72 % (3746290)Termination phase: Saturation % 22.18/3.72 % (3746290)Time elapsed: 0.121 s % 22.18/3.72 % (3746290)Peak memory usage: 14 MB % 22.18/3.72 % (3746290)Instructions burned: 132 (million) % 22.18/3.72 % (3746301)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2116430864:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi) % 22.18/3.72 % (3746291)Instruction limit reached! % 22.18/3.72 % (3746291)------------------------------ % 22.18/3.72 % (3746291)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.18/3.72 % (3746291)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.18/3.72 % (3746291)CaDiCaL version: 2.1.3 % 22.18/3.72 % (3746291)Termination reason: Instruction limit % 22.18/3.72 % (3746291)Termination phase: Saturation % 22.18/3.72 % (3746291)Time elapsed: 0.157 s % 22.18/3.72 % (3746291)Peak memory usage: 15 MB % 22.18/3.72 % (3746291)Instructions burned: 159 (million) % 22.18/3.72 % (3746302)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=2078994160:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi) % 22.18/3.72 % (3746304)ott-21_1_sil=16000:fs=off:random_seed=3972293917:i=180:av=off:fsr=off_2997 on theBenchmark for (2997ds/180Mi) % 22.18/3.72 % (3746301)Instruction limit reached! % 22.18/3.72 % (3746301)------------------------------ % 22.18/3.72 % (3746301)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.18/3.72 % (3746301)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.18/3.72 % (3746301)CaDiCaL version: 2.1.3 % 77.70/11.53 % (3746301)Termination reason: Instruction limit % 77.70/11.53 % (3746301)Termination phase: Saturation % 77.70/11.53 % (3746301)Time elapsed: 0.104 s % 77.70/11.53 % (3746301)Peak memory usage: 14 MB % 77.70/11.53 % (3746301)Instructions burned: 132 (million) % 77.70/11.53 % (3746307)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=751209524:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi) % 77.70/11.53 % (3746304)Instruction limit reached! % 77.70/11.53 % (3746304)------------------------------ % 77.70/11.53 % (3746304)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 77.70/11.53 % (3746304)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 77.70/11.53 % (3746304)CaDiCaL version: 2.1.3 % 77.70/11.53 % (3746304)Termination reason: Instruction limit % 77.70/11.53 % (3746304)Termination phase: Saturation % 77.70/11.53 % (3746304)Time elapsed: 0.159 s % 77.70/11.53 % (3746304)Peak memory usage: 13 MB % 77.70/11.53 % (3746304)Instructions burned: 181 (million) % 77.70/11.53 % TRYING [1] % 77.70/11.53 % (3746309)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=204506599:fmbsr=1.3:i=865:ins=25_2995 on theBenchmark for (2995ds/865Mi) % 77.70/11.53 % TRYING [2] % 77.70/11.53 % (3746299)Instruction limit reached! % 77.70/11.53 % (3746299)------------------------------ % 77.70/11.53 % (3746299)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 77.70/11.53 % (3746299)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 77.70/11.53 % (3746299)CaDiCaL version: 2.1.3 % 77.70/11.53 % (3746299)Termination reason: Instruction limit % 77.70/11.53 % (3746299)Termination phase: Finite model building constraint generation % 77.70/11.53 % (3746299)Time elapsed: 0.332 s % 77.70/11.53 % (3746299)Peak memory usage: 25 MB % 77.70/11.53 % (3746299)Instructions burned: 716 (million) % 77.70/11.53 % (3746311)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=877718603:i=1179_2995 on theBenchmark for (2995ds/1179Mi) % 77.70/11.53 % TRYING [1] % 77.70/11.53 % TRYING [2] % 77.70/11.53 % (3746307)Instruction limit reached! % 77.70/11.53 % (3746307)------------------------------ % 77.70/11.53 % (3746307)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 77.70/11.53 % (3746307)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 77.70/11.53 % (3746307)CaDiCaL version: 2.1.3 % 77.70/11.53 % (3746307)Termination reason: Instruction limit % 77.70/11.53 % (3746307)Termination phase: Saturation % 77.70/11.53 % (3746307)Time elapsed: 0.486 s % 77.70/11.53 % (3746307)Peak memory usage: 16 MB % 77.70/11.53 % (3746307)Instructions burned: 477 (million) % 77.70/11.53 % (3746302)Instruction limit reached! % 77.70/11.53 % (3746302)------------------------------ % 77.70/11.53 % (3746302)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 77.70/11.53 % (3746302)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 77.70/11.53 % (3746302)CaDiCaL version: 2.1.3 % 77.70/11.53 % (3746302)Termination reason: Instruction limit % 77.70/11.53 % (3746302)Termination phase: Saturation % 77.70/11.53 % (3746302)Time elapsed: 0.600 s % 77.70/11.53 % (3746302)Peak memory usage: 16 MB % 77.70/11.53 % (3746302)Instructions burned: 684 (million) % 77.70/11.53 % TRYING [3] % 77.70/11.53 % (3746313)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3010502375:i=889:ins=1_2991 on theBenchmark for (2991ds/889Mi) % 77.70/11.53 % (3746314)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=1790611623: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) % 77.70/11.53 % TRYING [1] % 77.70/11.53 % (3746311)Instruction limit reached! % 77.70/11.53 % (3746311)------------------------------ % 77.70/11.53 % (3746311)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 77.70/11.53 % (3746311)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 77.70/11.53 % (3746311)CaDiCaL version: 2.1.3 % 77.70/11.53 % (3746311)Termination reason: Instruction limit % 77.70/11.53 % (3746311)Termination phase: Saturation % 77.70/11.53 % (3746311)Time elapsed: 0.628 s % 77.70/11.53 % (3746311)Peak memory usage: 24 MB % 77.70/11.53 % (3746311)Instructions burned: 1180 (million) % 77.70/11.53 % TRYING [2] % 77.70/11.53 % (3746317)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=4018556758:i=879:kws=inv_precedence:fsr=off_2988 on theBenchmark for (2988ds/879Mi) % 77.70/11.53 % (3746309)Instruction limit reached! % 77.70/11.53 % (3746309)------------------------------ % 77.70/11.53 % (3746309)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 77.70/11.53 % (3746309)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 121.16/17.67 % (3746309)CaDiCaL version: 2.1.3 % 121.16/17.67 % (3746309)Termination reason: Instruction limit % 121.16/17.67 % (3746309)Termination phase: Finite model building constraint generation % 121.16/17.67 % (3746309)Time elapsed: 0.745 s % 121.16/17.67 % (3746309)Peak memory usage: 33 MB % 121.16/17.67 % (3746309)Instructions burned: 866 (million) % 121.16/17.67 % (3746319)fmb+10_1_sil=64000:random_seed=2122380749:i=22061:nm=2:gsp=on_2988 on theBenchmark for (2988ds/22061Mi) % 121.16/17.67 % (3746313)Instruction limit reached! % 121.16/17.67 % (3746313)------------------------------ % 121.16/17.67 % (3746313)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 121.16/17.67 % (3746313)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 121.16/17.67 % (3746313)CaDiCaL version: 2.1.3 % 121.16/17.67 % (3746313)Termination reason: Instruction limit % 121.16/17.67 % (3746313)Termination phase: Finite model building constraint generation % 121.16/17.67 % (3746313)Time elapsed: 0.558 s % 121.16/17.67 % (3746313)Peak memory usage: 53 MB % 121.16/17.67 % (3746313)Instructions burned: 890 (million) % 121.16/17.67 % (3746321)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1585080210:i=9515:nm=5_2985 on theBenchmark for (2985ds/9515Mi) % 121.16/17.67 % (3746317)Instruction limit reached! % 121.16/17.67 % (3746317)------------------------------ % 121.16/17.67 % (3746317)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 121.16/17.67 % (3746317)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 121.16/17.67 % (3746317)CaDiCaL version: 2.1.3 % 121.16/17.67 % (3746317)Termination reason: Instruction limit % 121.16/17.67 % (3746317)Termination phase: Saturation % 121.16/17.67 % (3746317)Time elapsed: 0.362 s % 121.16/17.67 % (3746317)Peak memory usage: 18 MB % 121.16/17.67 % (3746317)Instructions burned: 880 (million) % 121.16/17.67 % (3746314)Instruction limit reached! % 121.16/17.67 % (3746314)------------------------------ % 121.16/17.67 % (3746314)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 121.16/17.67 % (3746314)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 121.16/17.67 % (3746314)CaDiCaL version: 2.1.3 % 121.16/17.67 % (3746314)Termination reason: Instruction limit % 121.16/17.67 % (3746314)Termination phase: Saturation % 121.16/17.67 % (3746314)Time elapsed: 0.660 s % 121.16/17.67 % (3746314)Peak memory usage: 20 MB % 121.16/17.67 % (3746314)Instructions burned: 693 (million) % 121.16/17.67 % (3746324)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=658071554:fmbsr=1.7:i=920_2984 on theBenchmark for (2984ds/920Mi) % 121.16/17.67 % (3746326)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=613213370:i=5131_2984 on theBenchmark for (2984ds/5131Mi) % 121.16/17.67 % TRYING [1] % 121.16/17.67 % TRYING [2] % 121.16/17.67 % TRYING [8] % 121.16/17.67 % TRYING [4] % 121.16/17.67 % (3746324)Instruction limit reached! % 121.16/17.67 % (3746324)------------------------------ % 121.16/17.67 % (3746324)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 121.16/17.67 % (3746324)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 121.16/17.67 % (3746324)CaDiCaL version: 2.1.3 % 121.16/17.67 % (3746324)Termination reason: Instruction limit % 121.16/17.67 % (3746324)Termination phase: Finite model building constraint generation % 121.16/17.67 % (3746324)Time elapsed: 0.407 s % 121.16/17.67 % (3746324)Peak memory usage: 41 MB % 121.16/17.67 % (3746324)Instructions burned: 922 (million) % 121.16/17.67 % (3746333)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=48728138:i=1472:ins=7:fdi=8:gsp=on_2980 on theBenchmark for (2980ds/1472Mi) % 121.16/17.67 % TRYING [20] % 121.16/17.67 % TRYING [3] % 121.16/17.67 % (3746333)Instruction limit reached! % 121.16/17.67 % (3746333)------------------------------ % 121.16/17.67 % (3746333)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 121.16/17.67 % (3746333)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 121.16/17.67 % (3746333)CaDiCaL version: 2.1.3 % 121.16/17.67 % (3746333)Termination reason: Instruction limit % 121.16/17.67 % (3746333)Termination phase: Saturation % 121.16/17.67 % (3746333)Time elapsed: 0.690 s % 121.16/17.67 % (3746333)Peak memory usage: 25 MB % 121.16/17.67 % (3746333)Instructions burned: 1473 (million) % 121.16/17.67 % (3746341)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=2957714448:i=6324_2973 on theBenchmark for (2973ds/6324Mi) % 121.16/17.67 % (3746341)Cannot represent all propositional literals internally % 121.16/17.67 % (3746341)Refutation not found, incomplete strategy % 121.16/17.67 % (3746341)------------------------------ % 284.00/40.53 % (3746341)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 284.00/40.53 % (3746341)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 284.00/40.53 % (3746341)CaDiCaL version: 2.1.3 % 284.00/40.53 % (3746341)Termination reason: Refutation not found, incomplete strategy % 284.00/40.53 % (3746341)Time elapsed: 0.560 s % 284.00/40.53 % (3746341)Peak memory usage: 24 MB % 284.00/40.53 % (3746341)Instructions burned: 672 (million) % 284.00/40.53 % (3746341)------------------------------ % 284.00/40.53 % (3746341)------------------------------ % 284.00/40.53 % (3746345)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1935243842:fmbsr=2.30978:i=2174_2967 on theBenchmark for (2967ds/2174Mi) % 284.00/40.53 % TRYING [16] % 284.00/40.53 % TRYING [4] % 284.00/40.53 % (3746345)Instruction limit reached! % 284.00/40.53 % (3746345)------------------------------ % 284.00/40.53 % (3746345)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 284.00/40.53 % (3746345)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 284.00/40.53 % (3746345)CaDiCaL version: 2.1.3 % 284.00/40.53 % (3746345)Termination reason: Instruction limit % 284.00/40.53 % (3746345)Termination phase: Finite model building constraint generation % 284.00/40.53 % (3746345)Time elapsed: 1.566 s % 284.00/40.53 % (3746345)Peak memory usage: 125 MB % 284.00/40.53 % (3746345)Instructions burned: 2175 (million) % 284.00/40.53 % (3746351)ott-2_1_sil=16000:newcnf=on:random_seed=2924939697:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2951 on theBenchmark for (2951ds/869Mi) % 284.00/40.53 % TRYING [5] % 284.00/40.53 % (3746351)Instruction limit reached! % 284.00/40.53 % (3746351)------------------------------ % 284.00/40.53 % (3746351)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 284.00/40.53 % (3746351)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 284.00/40.53 % (3746351)CaDiCaL version: 2.1.3 % 284.00/40.53 % (3746351)Termination reason: Instruction limit % 284.00/40.53 % (3746351)Termination phase: Saturation % 284.00/40.53 % (3746351)Time elapsed: 0.735 s % 284.00/40.53 % (3746351)Peak memory usage: 17 MB % 284.00/40.53 % (3746351)Instructions burned: 869 (million) % 284.00/40.53 % (3746357)ott+10_1_sil=32000:tgt=ground:random_seed=2647296795:i=5114:av=off_2943 on theBenchmark for (2943ds/5114Mi) % 284.00/40.53 % (3746326)Instruction limit reached! % 284.00/40.53 % (3746326)------------------------------ % 284.00/40.53 % (3746326)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 284.00/40.53 % (3746326)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 284.00/40.53 % (3746326)CaDiCaL version: 2.1.3 % 284.00/40.53 % (3746326)Termination reason: Instruction limit % 284.00/40.53 % (3746326)Termination phase: Saturation % 284.00/40.53 % (3746326)Time elapsed: 4.832 s % 284.00/40.53 % (3746326)Peak memory usage: 55 MB % 284.00/40.53 % (3746326)Instructions burned: 5131 (million) % 284.00/40.53 % (3746359)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=1732266527:i=54282_2936 on theBenchmark for (2936ds/54282Mi) % 284.00/40.53 % TRYING [1] % 284.00/40.53 % TRYING [2] % 284.00/40.53 % TRYING [3] % 284.00/40.53 % TRYING [4] % 284.00/40.53 % (3746321)Instruction limit reached! % 284.00/40.53 % (3746321)------------------------------ % 284.00/40.53 % (3746321)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 284.00/40.53 % (3746321)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 284.00/40.53 % (3746321)CaDiCaL version: 2.1.3 % 284.00/40.53 % (3746321)Termination reason: Instruction limit % 284.00/40.53 % (3746321)Termination phase: Finite model building constraint generation % 284.00/40.53 % (3746321)Time elapsed: 6.952 s % 284.00/40.53 % (3746321)Peak memory usage: 638 MB % 284.00/40.53 % (3746321)Instructions burned: 9516 (million) % 284.00/40.53 % (3746367)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=1154885410:i=3512:aac=none_2914 on theBenchmark for (2914ds/3512Mi) % 284.00/40.53 % TRYING [5] % 284.00/40.53 % (3746357)Instruction limit reached! % 284.00/40.53 % (3746357)------------------------------ % 284.00/40.53 % (3746357)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 284.00/40.53 % (3746357)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 284.00/40.53 % (3746357)CaDiCaL version: 2.1.3 % 284.00/40.53 % (3746357)Termination reason: Instruction limit % 284.00/40.53 % (3746357)Termination phase: Saturation % 284.00/40.53 % (3746357)Time elapsed: 4.908 s % 284.00/40.53 % (3746357)Peak memory usage: 62 MB % 284.00/40.53 % (3746357)Instructions burned: 5114 (million) % 284.00/40.53 % (3746377)dis+21_1_sil=32000:sas=cadical:random_seed=1751301588:i=3773:amm=off_2894 on theBenchmark for (2894ds/3773Mi) % 284.00/40.53 % (3746319)Instruction limit reached! % 300.35/42.93 % (3746319)------------------------------ % 300.35/42.93 % (3746319)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.35/42.93 % (3746319)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.35/42.93 % (3746319)CaDiCaL version: 2.1.3 % 300.35/42.93 % (3746319)Termination reason: Instruction limit % 300.35/42.93 % (3746319)Termination phase: Finite model building constraint generation % 300.35/42.93 % (3746319)Time elapsed: 9.830 s % 300.35/42.93 % (3746319)Peak memory usage: 338 MB % 300.35/42.93 % (3746319)Instructions burned: 22064 (million) % 300.35/42.93 % (3746379)ott+11_1_sil=16000:gs=on:random_seed=386196753:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2889 on theBenchmark for (2889ds/2251Mi) % 300.35/42.93 % TRYING [5] % 300.35/42.93 % (3746367)Instruction limit reached! % 300.35/42.93 % (3746367)------------------------------ % 300.35/42.93 % (3746367)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.35/42.93 % (3746367)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.35/42.93 % (3746367)CaDiCaL version: 2.1.3 % 300.35/42.93 % (3746367)Termination reason: Instruction limit % 300.35/42.93 % (3746367)Termination phase: Saturation % 300.35/42.93 % (3746367)Time elapsed: 3.241 s % 300.35/42.93 % (3746367)Peak memory usage: 47 MB % 300.35/42.93 % (3746367)Instructions burned: 3513 (million) % 300.35/42.93 % (3746381)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=4193936545:fmbsr=1.6:i=67534_2881 on theBenchmark for (2881ds/67534Mi) % 300.35/42.93 % (3746379)Instruction limit reached! % 300.35/42.93 % (3746379)------------------------------ % 300.35/42.93 % (3746379)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.35/42.93 % (3746379)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.35/42.93 % (3746379)CaDiCaL version: 2.1.3 % 300.35/42.93 % (3746379)Termination reason: Instruction limit % 300.35/42.93 % (3746379)Termination phase: Saturation % 300.35/42.93 % (3746379)Time elapsed: 1.084 s % 300.35/42.93 % (3746379)Peak memory usage: 37 MB % 300.35/42.93 % (3746379)Instructions burned: 2252 (million) % 300.35/42.93 % (3746383)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=1884844020:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2877 on theBenchmark for (2877ds/4591Mi) % 300.35/42.93 % TRYING [7] % 300.35/42.93 % (3746377)Instruction limit reached! % 300.35/42.93 % (3746377)------------------------------ % 300.35/42.93 % (3746377)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.35/42.93 % (3746377)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.35/42.93 % (3746377)CaDiCaL version: 2.1.3 % 300.35/42.93 % (3746377)Termination reason: Instruction limit % 300.35/42.93 % (3746377)Termination phase: Saturation % 300.35/42.93 % (3746377)Time elapsed: 3.425 s % 300.35/42.93 % (3746377)Peak memory usage: 51 MB % 300.35/42.93 % (3746377)Instructions burned: 3773 (million) % 300.35/42.93 % (3746385)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=432856407:i=29340_2859 on theBenchmark for (2859ds/29340Mi) % 300.35/42.93 % (3746383)Instruction limit reached! % 300.35/42.93 % (3746383)------------------------------ % 300.35/42.93 % (3746383)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.35/42.93 % (3746383)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.35/42.93 % (3746383)CaDiCaL version: 2.1.3 % 300.35/42.93 % (3746383)Termination reason: Instruction limit % 300.35/42.93 % (3746383)Termination phase: Saturation % 300.35/42.93 % (3746383)Time elapsed: 2.575 s % 300.35/42.93 % (3746383)Peak memory usage: 62 MB % 300.35/42.93 % (3746383)Instructions burned: 4593 (million) % 300.35/42.93 % (3746395)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=423054927:i=5211_2851 on theBenchmark for (2851ds/5211Mi) % 300.35/42.93 % TRYING [6] % 300.35/42.93 % (3746395)Instruction limit reached! % 300.35/42.93 % (3746395)------------------------------ % 300.35/42.93 % (3746395)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.35/42.93 % (3746395)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.35/42.93 % (3746395)CaDiCaL version: 2.1.3 % 300.35/42.93 % (3746395)Termination reason: Instruction limit % 300.35/42.93 % (3746395)Termination phase: Saturation % 300.35/42.93 % (3746395)Time elapsed: 1.999 s % 300.35/42.93 % (3746395)Peak memory usage: 37 MB % 300.35/42.93 % (3746395)Instructions burned: 5213 (million) % 300.35/42.93 % (3746399)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=2586215596:i=5497:nm=2_2831 on theBenchmark for (2831ds/5497Mi) % 300.35/42.93 % TRYI % 300.35/42.93 Terminated % 300.35/42.93 % Vampire exiting % 300.35/42.94 Terminated %------------------------------------------------------------------------------