%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWW606_2 : TPTP v9.3.1. Released v6.1.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % Computer : n001.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:40:31 PM UTC 2026 % Result : Timeout 300.35s 42.64s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.04 % Problem : SWW606_2 : TPTP v9.3.1. Released v6.1.0. % 0.00/0.08 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.24/0.28 % Computer : n001.cluster.edu % 0.24/0.28 % Model : x86_64 x86_64 % 0.24/0.28 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.24/0.28 % Memory : 8046.5625MB % 0.24/0.28 % OS : Linux 6.8.0-71-generic % 0.24/0.28 % CPULimit : 300 % 0.24/0.28 % WCLimit : 300 % 0.24/0.28 % DateTime : Mon Sep 28 14:27:32 UTC 2026 % 0.24/0.28 % CPUTime : % 0.24/0.28 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.24/0.31 Running first-order model finding % 0.24/0.31 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 % 5.96/1.19 % (380094)Will run a generic schedule for satisfiability detection. % 5.96/1.19 % (380103)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=441301847:i=116_2999 on theBenchmark for (2999ds/116Mi) % 5.96/1.19 % (380100)% WARNING: option uhcvi not known. % 5.96/1.19 % (380102)dis+10_1_sil=32000:sp=arity:random_seed=2665695752:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 5.96/1.19 % (380100)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1989067430:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 5.96/1.19 % (380099)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1356229814_2999 on theBenchmark for (2999ds/0Mi) % 5.96/1.19 % (380101)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2864371608:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 5.96/1.19 % (380104)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2285327294:i=131_2999 on theBenchmark for (2999ds/131Mi) % 5.96/1.19 % (380105)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1402718434:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 5.96/1.19 % (380099)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 5.96/1.19 % (380099)Terminated due to inappropriate strategy. % 5.96/1.19 % (380099)------------------------------ % 5.96/1.19 % (380099)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.96/1.19 % (380099)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.96/1.19 % (380099)CaDiCaL version: 2.1.3 % 5.96/1.19 % (380099)Termination reason: Inappropriate % 5.96/1.19 % (380099)Time elapsed: 0.011 s % 5.96/1.19 % (380099)Peak memory usage: 11 MB % 5.96/1.19 % (380099)Instructions burned: 11 (million) % 5.96/1.19 % (380099)------------------------------ % 5.96/1.19 % (380099)------------------------------ % 5.96/1.19 % (380103)Instruction limit reached! % 5.96/1.19 % (380103)------------------------------ % 5.96/1.19 % (380103)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.96/1.19 % (380103)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.96/1.19 % (380103)CaDiCaL version: 2.1.3 % 5.96/1.19 % (380103)Termination reason: Instruction limit % 5.96/1.19 % (380103)Termination phase: Saturation % 5.96/1.19 % (380103)Time elapsed: 0.056 s % 5.96/1.19 % (380103)Peak memory usage: 13 MB % 5.96/1.19 % (380103)Instructions burned: 117 (million) % 5.96/1.19 % (380116)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=746104585:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 5.96/1.19 % (380119)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3369042056:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 5.96/1.19 % (380116)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 5.96/1.19 % (380116)Terminated due to inappropriate strategy. % 5.96/1.19 % (380116)------------------------------ % 5.96/1.19 % (380116)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.96/1.19 % (380116)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.96/1.19 % (380116)CaDiCaL version: 2.1.3 % 5.96/1.19 % (380116)Termination reason: Inappropriate % 5.96/1.19 % (380116)Time elapsed: 0.009 s % 5.96/1.19 % (380116)Peak memory usage: 11 MB % 5.96/1.19 % (380116)Instructions burned: 9 (million) % 5.96/1.19 % (380116)------------------------------ % 5.96/1.19 % (380116)------------------------------ % 5.96/1.19 % (380119)Instruction limit reached! % 5.96/1.19 % (380119)------------------------------ % 5.96/1.19 % (380119)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.96/1.19 % (380119)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.96/1.19 % (380119)CaDiCaL version: 2.1.3 % 5.96/1.19 % (380119)Termination reason: Instruction limit % 5.96/1.19 % (380119)Termination phase: Saturation % 5.96/1.19 % (380119)Time elapsed: 0.049 s % 5.96/1.19 % (380119)Peak memory usage: 13 MB % 5.96/1.19 % (380119)Instructions burned: 132 (million) % 5.96/1.19 % (380102)Instruction limit reached! % 5.96/1.19 % (380102)------------------------------ % 5.96/1.19 % (380102)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.96/1.19 % (380102)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.96/1.19 % (380102)CaDiCaL version: 2.1.3 % 5.96/1.19 % (380102)Termination reason: Instruction limit % 5.96/1.19 % (380102)Termination phase: Saturation % 7.81/1.72 % (380102)Time elapsed: 0.108 s % 7.81/1.72 % (380102)Peak memory usage: 13 MB % 7.81/1.72 % (380102)Instructions burned: 103 (million) % 7.81/1.72 % (380123)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=1400528578:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi) % 7.81/1.72 % (380104)Instruction limit reached! % 7.81/1.72 % (380104)------------------------------ % 7.81/1.72 % (380104)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.81/1.72 % (380104)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.81/1.72 % (380104)CaDiCaL version: 2.1.3 % 7.81/1.72 % (380104)Termination reason: Instruction limit % 7.81/1.72 % (380104)Termination phase: Saturation % 7.81/1.72 % (380104)Time elapsed: 0.133 s % 7.81/1.72 % (380104)Peak memory usage: 13 MB % 7.81/1.72 % (380104)Instructions burned: 132 (million) % 7.81/1.72 % (380124)ott-21_1_sil=16000:fs=off:random_seed=2393000572:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 7.81/1.72 % (380125)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1007483569:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 7.81/1.72 % (380128)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2130416355:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 7.81/1.72 % (380128)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 7.81/1.72 % (380128)Terminated due to inappropriate strategy. % 7.81/1.72 % (380128)------------------------------ % 7.81/1.72 % (380128)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.81/1.72 % (380128)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.81/1.72 % (380128)CaDiCaL version: 2.1.3 % 7.81/1.72 % (380128)Termination reason: Inappropriate % 7.81/1.72 % (380128)Time elapsed: 0.003 s % 7.81/1.72 % (380128)Peak memory usage: 10 MB % 7.81/1.72 % (380128)Instructions burned: 9 (million) % 7.81/1.72 % (380128)------------------------------ % 7.81/1.72 % (380128)------------------------------ % 7.81/1.72 % (380131)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3333148848:i=1179_2998 on theBenchmark for (2998ds/1179Mi) % 7.81/1.72 % (380105)Instruction limit reached! % 7.81/1.72 % (380105)------------------------------ % 7.81/1.72 % (380105)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.81/1.72 % (380105)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.81/1.72 % (380105)CaDiCaL version: 2.1.3 % 7.81/1.72 % (380105)Termination reason: Instruction limit % 7.81/1.72 % (380105)Termination phase: Saturation % 7.81/1.72 % (380105)Time elapsed: 0.170 s % 7.81/1.72 % (380105)Peak memory usage: 13 MB % 7.81/1.72 % (380105)Instructions burned: 159 (million) % 7.81/1.72 % (380133)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=4233166143:i=889:ins=1_2997 on theBenchmark for (2997ds/889Mi) % 7.81/1.72 % (380133)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 7.81/1.72 % (380133)Terminated due to inappropriate strategy. % 7.81/1.72 % (380133)------------------------------ % 7.81/1.72 % (380133)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.81/1.72 % (380133)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.81/1.72 % (380133)CaDiCaL version: 2.1.3 % 7.81/1.72 % (380133)Termination reason: Inappropriate % 7.81/1.72 % (380133)Time elapsed: 0.009 s % 7.81/1.72 % (380133)Peak memory usage: 10 MB % 7.81/1.72 % (380133)Instructions burned: 9 (million) % 7.81/1.72 % (380133)------------------------------ % 7.81/1.72 % (380133)------------------------------ % 7.81/1.72 % (380135)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=1389194449:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2997 on theBenchmark for (2997ds/692Mi) % 7.81/1.72 % (380124)Instruction limit reached! % 7.81/1.72 % (380124)------------------------------ % 7.81/1.72 % (380124)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.81/1.72 % (380124)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.81/1.72 % (380124)CaDiCaL version: 2.1.3 % 7.81/1.72 % (380124)Termination reason: Instruction limit % 7.81/1.72 % (380124)Termination phase: Saturation % 7.81/1.72 % (380124)Time elapsed: 0.163 s % 7.81/1.72 % (380124)Peak memory usage: 13 MB % 7.81/1.72 % (380124)Instructions burned: 180 (million) % 39.71/5.90 % (380137)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3492494932:i=879:kws=inv_precedence:fsr=off_2996 on theBenchmark for (2996ds/879Mi) % 39.71/5.90 % (380125)Instruction limit reached! % 39.71/5.90 % (380125)------------------------------ % 39.71/5.90 % (380125)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 39.71/5.90 % (380125)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.71/5.90 % (380125)CaDiCaL version: 2.1.3 % 39.71/5.90 % (380125)Termination reason: Instruction limit % 39.71/5.90 % (380125)Termination phase: Saturation % 39.71/5.90 % (380125)Time elapsed: 0.515 s % 39.71/5.90 % (380125)Peak memory usage: 14 MB % 39.71/5.90 % (380125)Instructions burned: 477 (million) % 39.71/5.90 % (380123)Instruction limit reached! % 39.71/5.90 % (380123)------------------------------ % 39.71/5.90 % (380123)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 39.71/5.90 % (380123)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.71/5.90 % (380123)CaDiCaL version: 2.1.3 % 39.71/5.90 % (380123)Termination reason: Instruction limit % 39.71/5.90 % (380123)Termination phase: Saturation % 39.71/5.90 % (380123)Time elapsed: 0.576 s % 39.71/5.90 % (380123)Peak memory usage: 16 MB % 39.71/5.90 % (380123)Instructions burned: 684 (million) % 39.71/5.90 % (380141)fmb+10_1_sil=64000:random_seed=2619686987:i=22061:nm=2:gsp=on_2993 on theBenchmark for (2993ds/22061Mi) % 39.71/5.90 % (380141)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 39.71/5.90 % (380141)Terminated due to inappropriate strategy. % 39.71/5.90 % (380141)------------------------------ % 39.71/5.90 % (380141)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 39.71/5.90 % (380141)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.71/5.90 % (380141)CaDiCaL version: 2.1.3 % 39.71/5.90 % (380141)Termination reason: Inappropriate % 39.71/5.90 % (380141)Time elapsed: 0.010 s % 39.71/5.90 % (380141)Peak memory usage: 11 MB % 39.71/5.90 % (380141)Instructions burned: 10 (million) % 39.71/5.90 % (380141)------------------------------ % 39.71/5.90 % (380141)------------------------------ % 39.71/5.90 % (380142)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=979768052:i=9515:nm=5_2992 on theBenchmark for (2992ds/9515Mi) % 39.71/5.90 % (380142)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 39.71/5.90 % (380142)Terminated due to inappropriate strategy. % 39.71/5.90 % (380142)------------------------------ % 39.71/5.90 % (380142)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 39.71/5.90 % (380142)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.71/5.90 % (380142)CaDiCaL version: 2.1.3 % 39.71/5.90 % (380142)Termination reason: Inappropriate % 39.71/5.90 % (380142)Time elapsed: 0.006 s % 39.71/5.90 % (380142)Peak memory usage: 11 MB % 39.71/5.90 % (380142)Instructions burned: 9 (million) % 39.71/5.90 % (380142)------------------------------ % 39.71/5.90 % (380142)------------------------------ % 39.71/5.90 % (380146)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2417876205:i=5131_2992 on theBenchmark for (2992ds/5131Mi) % 39.71/5.90 % (380145)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=4092824086:fmbsr=1.7:i=920_2992 on theBenchmark for (2992ds/920Mi) % 39.71/5.90 % (380145)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 39.71/5.90 % (380145)Terminated due to inappropriate strategy. % 39.71/5.90 % (380145)------------------------------ % 39.71/5.90 % (380145)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 39.71/5.90 % (380145)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.71/5.90 % (380145)CaDiCaL version: 2.1.3 % 39.71/5.90 % (380145)Termination reason: Inappropriate % 39.71/5.90 % (380145)Time elapsed: 0.009 s % 39.71/5.90 % (380145)Peak memory usage: 11 MB % 39.71/5.90 % (380145)Instructions burned: 9 (million) % 39.71/5.90 % (380145)------------------------------ % 39.71/5.90 % (380145)------------------------------ % 39.71/5.90 % (380149)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2224563038:i=1472:ins=7:fdi=8:gsp=on_2991 on theBenchmark for (2991ds/1472Mi) % 39.71/5.90 % (380131)Instruction limit reached! % 39.71/5.90 % (380131)------------------------------ % 39.71/5.90 % (380131)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 39.71/5.90 % (380131)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 43.19/6.50 % (380131)CaDiCaL version: 2.1.3 % 43.19/6.50 % (380131)Termination reason: Instruction limit % 43.19/6.50 % (380131)Termination phase: Saturation % 43.19/6.50 % (380131)Time elapsed: 0.658 s % 43.19/6.50 % (380131)Peak memory usage: 20 MB % 43.19/6.50 % (380131)Instructions burned: 1180 (million) % 43.19/6.50 % (380151)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3513787353:i=6324_2991 on theBenchmark for (2991ds/6324Mi) % 43.19/6.50 % (380151)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 43.19/6.50 % (380151)Terminated due to inappropriate strategy. % 43.19/6.50 % (380151)------------------------------ % 43.19/6.50 % (380151)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 43.19/6.50 % (380151)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 43.19/6.50 % (380151)CaDiCaL version: 2.1.3 % 43.19/6.50 % (380151)Termination reason: Inappropriate % 43.19/6.50 % (380151)Time elapsed: 0.006 s % 43.19/6.50 % (380151)Peak memory usage: 11 MB % 43.19/6.50 % (380151)Instructions burned: 11 (million) % 43.19/6.50 % (380151)------------------------------ % 43.19/6.50 % (380151)------------------------------ % 43.19/6.51 % (380153)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=2531639643:fmbsr=2.30978:i=2174_2991 on theBenchmark for (2991ds/2174Mi) % 43.19/6.51 % (380153)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 43.19/6.51 % (380153)Terminated due to inappropriate strategy. % 43.19/6.51 % (380153)------------------------------ % 43.19/6.51 % (380153)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 43.19/6.51 % (380153)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 43.19/6.51 % (380153)CaDiCaL version: 2.1.3 % 43.19/6.51 % (380153)Termination reason: Inappropriate % 43.19/6.51 % (380153)Time elapsed: 0.006 s % 43.19/6.51 % (380153)Peak memory usage: 11 MB % 43.19/6.51 % (380153)Instructions burned: 9 (million) % 43.19/6.51 % (380153)------------------------------ % 43.19/6.51 % (380153)------------------------------ % 43.19/6.51 % (380155)ott-2_1_sil=16000:newcnf=on:random_seed=3960679424:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2990 on theBenchmark for (2990ds/869Mi) % 43.19/6.51 % (380135)Instruction limit reached! % 43.19/6.51 % (380135)------------------------------ % 43.19/6.51 % (380135)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 43.19/6.51 % (380135)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 43.19/6.51 % (380135)CaDiCaL version: 2.1.3 % 43.19/6.51 % (380135)Termination reason: Instruction limit % 43.19/6.51 % (380135)Termination phase: Saturation % 43.19/6.51 % (380135)Time elapsed: 0.739 s % 43.19/6.51 % (380135)Peak memory usage: 19 MB % 43.19/6.51 % (380135)Instructions burned: 693 (million) % 43.19/6.51 % (380159)ott+10_1_sil=32000:tgt=ground:random_seed=3787242125:i=5114:av=off_2989 on theBenchmark for (2989ds/5114Mi) % 43.19/6.51 % (380137)Instruction limit reached! % 43.19/6.51 % (380137)------------------------------ % 43.19/6.51 % (380137)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 43.19/6.51 % (380137)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 43.19/6.51 % (380137)CaDiCaL version: 2.1.3 % 43.19/6.51 % (380137)Termination reason: Instruction limit % 43.19/6.51 % (380137)Termination phase: Saturation % 43.19/6.51 % (380137)Time elapsed: 0.810 s % 43.19/6.51 % (380137)Peak memory usage: 19 MB % 43.19/6.51 % (380137)Instructions burned: 880 (million) % 43.19/6.51 % (380163)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=880318108:i=54282_2988 on theBenchmark for (2988ds/54282Mi) % 43.19/6.51 % (380163)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 43.19/6.51 % (380163)Terminated due to inappropriate strategy. % 43.19/6.51 % (380163)------------------------------ % 43.19/6.51 % (380163)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 43.19/6.51 % (380163)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 43.19/6.51 % (380163)CaDiCaL version: 2.1.3 % 43.19/6.51 % (380163)Termination reason: Inappropriate % 43.19/6.51 % (380163)Time elapsed: 0.011 s % 43.19/6.51 % (380163)Peak memory usage: 11 MB % 43.19/6.51 % (380163)Instructions burned: 11 (million) % 43.19/6.51 % (380163)------------------------------ % 43.19/6.51 % (380163)------------------------------ % 43.19/6.51 % (380165)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=410153218:i=3512:aac=none_2987 on theBenchmark for (2987ds/3512Mi) % 43.19/6.51 % (380155)Instruction limit reached! % 136.38/20.14 % (380155)------------------------------ % 136.38/20.14 % (380155)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 136.38/20.14 % (380155)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 136.38/20.14 % (380155)CaDiCaL version: 2.1.3 % 136.38/20.14 % (380155)Termination reason: Instruction limit % 136.38/20.14 % (380155)Termination phase: Saturation % 136.38/20.14 % (380155)Time elapsed: 0.452 s % 136.38/20.14 % (380155)Peak memory usage: 16 MB % 136.38/20.14 % (380155)Instructions burned: 870 (million) % 136.38/20.14 % (380167)dis+21_1_sil=32000:sas=cadical:random_seed=3964995678:i=3773:amm=off_2985 on theBenchmark for (2985ds/3773Mi) % 136.38/20.14 % (380149)Instruction limit reached! % 136.38/20.14 % (380149)------------------------------ % 136.38/20.14 % (380149)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 136.38/20.14 % (380149)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 136.38/20.14 % (380149)CaDiCaL version: 2.1.3 % 136.38/20.14 % (380149)Termination reason: Instruction limit % 136.38/20.14 % (380149)Termination phase: Saturation % 136.38/20.14 % (380149)Time elapsed: 1.439 s % 136.38/20.15 % (380149)Peak memory usage: 27 MB % 136.38/20.15 % (380149)Instructions burned: 1473 (million) % 136.38/20.15 % (380169)ott+11_1_sil=16000:gs=on:random_seed=4146600662:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2977 on theBenchmark for (2977ds/2251Mi) % 136.38/20.15 % (380167)Instruction limit reached! % 136.38/20.15 % (380167)------------------------------ % 136.38/20.15 % (380167)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 136.38/20.15 % (380167)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 136.38/20.15 % (380167)CaDiCaL version: 2.1.3 % 136.38/20.15 % (380167)Termination reason: Instruction limit % 136.38/20.15 % (380167)Termination phase: Saturation % 136.38/20.15 % (380167)Time elapsed: 1.895 s % 136.38/20.15 % (380167)Peak memory usage: 35 MB % 136.38/20.15 % (380167)Instructions burned: 3775 (million) % 136.38/20.15 % (380171)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=993784525:fmbsr=1.6:i=67534_2966 on theBenchmark for (2966ds/67534Mi) % 136.38/20.15 % (380171)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 136.38/20.15 % (380171)Terminated due to inappropriate strategy. % 136.38/20.15 % (380171)------------------------------ % 136.38/20.15 % (380171)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 136.38/20.15 % (380171)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 136.38/20.15 % (380171)CaDiCaL version: 2.1.3 % 136.38/20.15 % (380171)Termination reason: Inappropriate % 136.38/20.15 % (380171)Time elapsed: 0.006 s % 136.38/20.15 % (380171)Peak memory usage: 11 MB % 136.38/20.15 % (380171)Instructions burned: 9 (million) % 136.38/20.15 % (380171)------------------------------ % 136.38/20.15 % (380171)------------------------------ % 136.38/20.15 % (380173)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=3809209868:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2966 on theBenchmark for (2966ds/4591Mi) % 136.38/20.15 % (380169)Instruction limit reached! % 136.38/20.15 % (380169)------------------------------ % 136.38/20.15 % (380169)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 136.38/20.15 % (380169)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 136.38/20.15 % (380169)CaDiCaL version: 2.1.3 % 136.38/20.15 % (380169)Termination reason: Instruction limit % 136.38/20.15 % (380169)Termination phase: Saturation % 136.38/20.15 % (380169)Time elapsed: 2.058 s % 136.38/20.15 % (380169)Peak memory usage: 18 MB % 136.38/20.15 % (380169)Instructions burned: 2252 (million) % 136.38/20.15 % (380175)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=2477048473:i=29340_2956 on theBenchmark for (2956ds/29340Mi) % 136.38/20.15 % (380165)Instruction limit reached! % 136.38/20.15 % (380165)------------------------------ % 136.38/20.15 % (380165)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 136.38/20.15 % (380165)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 136.38/20.15 % (380165)CaDiCaL version: 2.1.3 % 136.38/20.15 % (380165)Termination reason: Instruction limit % 136.38/20.15 % (380165)Termination phase: Saturation % 136.38/20.15 % (380165)Time elapsed: 3.259 s % 136.38/20.15 % (380165)Peak memory usage: 32 MB % 136.38/20.15 % (380165)Instructions burned: 3513 (million) % 136.38/20.15 % (380179)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=3288344135:i=5211_2954 on theBenchmark for (2954ds/5211Mi) % 136.38/20.15 % (380146)Instruction limit reached! % 159.79/22.85 % (380146)------------------------------ % 159.79/22.85 % (380146)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 159.79/22.85 % (380146)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 159.79/22.85 % (380146)CaDiCaL version: 2.1.3 % 159.79/22.85 % (380146)Termination reason: Instruction limit % 159.79/22.85 % (380146)Termination phase: Saturation % 159.79/22.85 % (380146)Time elapsed: 4.787 s % 159.79/22.85 % (380146)Peak memory usage: 42 MB % 159.79/22.85 % (380146)Instructions burned: 5132 (million) % 159.79/22.85 % (380181)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=566265453:i=5497:nm=2_2944 on theBenchmark for (2944ds/5497Mi) % 159.79/22.85 % (380181)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 159.79/22.85 % (380181)Terminated due to inappropriate strategy. % 159.79/22.85 % (380181)------------------------------ % 159.79/22.85 % (380181)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 159.79/22.85 % (380181)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 159.79/22.85 % (380181)CaDiCaL version: 2.1.3 % 159.79/22.85 % (380181)Termination reason: Inappropriate % 159.79/22.85 % (380181)Time elapsed: 0.007 s % 159.79/22.85 % (380181)Peak memory usage: 11 MB % 159.79/22.85 % (380181)Instructions burned: 11 (million) % 159.79/22.85 % (380181)------------------------------ % 159.79/22.85 % (380181)------------------------------ % 159.79/22.85 % (380183)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=488760360:fmbsr=2:i=46332_2943 on theBenchmark for (2943ds/46332Mi) % 159.79/22.85 % (380183)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 159.79/22.85 % (380183)Terminated due to inappropriate strategy. % 159.79/22.85 % (380183)------------------------------ % 159.79/22.85 % (380183)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 159.79/22.85 % (380183)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 159.79/22.85 % (380183)CaDiCaL version: 2.1.3 % 159.79/22.85 % (380183)Termination reason: Inappropriate % 159.79/22.85 % (380183)Time elapsed: 0.006 s % 159.79/22.85 % (380183)Peak memory usage: 11 MB % 159.79/22.85 % (380183)Instructions burned: 10 (million) % 159.79/22.85 % (380183)------------------------------ % 159.79/22.85 % (380183)------------------------------ % 159.79/22.85 % (380185)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=3179650084:i=14071_2943 on theBenchmark for (2943ds/14071Mi) % 159.79/22.85 % (380185)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 159.79/22.85 % (380185)Terminated due to inappropriate strategy. % 159.79/22.85 % (380185)------------------------------ % 159.79/22.85 % (380185)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 159.79/22.85 % (380185)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 159.79/22.85 % (380185)CaDiCaL version: 2.1.3 % 159.79/22.85 % (380185)Termination reason: Inappropriate % 159.79/22.85 % (380185)Time elapsed: 0.008 s % 159.79/22.85 % (380185)Peak memory usage: 11 MB % 159.79/22.85 % (380185)Instructions burned: 10 (million) % 159.79/22.85 % (380185)------------------------------ % 159.79/22.85 % (380185)------------------------------ % 159.79/22.85 % (380187)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1416659216:i=22565:add=on:rawr=on_2943 on theBenchmark for (2943ds/22565Mi) % 159.79/22.85 % (380173)Instruction limit reached! % 159.79/22.85 % (380173)------------------------------ % 159.79/22.85 % (380173)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 159.79/22.85 % (380173)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 159.79/22.85 % (380173)CaDiCaL version: 2.1.3 % 159.79/22.85 % (380173)Termination reason: Instruction limit % 159.79/22.85 % (380173)Termination phase: Saturation % 159.79/22.85 % (380173)Time elapsed: 2.483 s % 159.79/22.85 % (380173)Peak memory usage: 37 MB % 159.79/22.85 % (380173)Instructions burned: 4591 (million) % 159.79/22.85 % (380189)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=2735100385:i=8173:av=off_2941 on theBenchmark for (2941ds/8173Mi) % 159.79/22.85 % (380159)Instruction limit reached! % 159.79/22.85 % (380159)------------------------------ % 159.79/22.85 % (380159)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 159.79/22.85 % (380159)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 159.79/22.85 % (380159)CaDiCaL version: 2.1.3 % 159.79/22.85 % (380159)Termination reason: Instruction limit % 159.79/22.85 % (380159)Termination phase: Saturation % 165.48/23.69 % (380159)Time elapsed: 5.108 s % 165.48/23.69 % (380159)Peak memory usage: 42 MB % 165.48/23.69 % (380159)Instructions burned: 5115 (million) % 165.48/23.69 % (380192)dis+10_16:1_sil=16000:random_seed=3053117210:i=9155:fsr=off_2938 on theBenchmark for (2938ds/9155Mi) % 165.48/23.69 % (380179)Instruction limit reached! % 165.48/23.69 % (380179)------------------------------ % 165.48/23.69 % (380179)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 165.48/23.69 % (380179)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 165.48/23.69 % (380179)CaDiCaL version: 2.1.3 % 165.48/23.69 % (380179)Termination reason: Instruction limit % 165.48/23.69 % (380179)Termination phase: Saturation % 165.48/23.69 % (380179)Time elapsed: 4.721 s % 165.48/23.69 % (380179)Peak memory usage: 50 MB % 165.48/23.69 % (380179)Instructions burned: 5211 (million) % 165.48/23.69 % (380199)ott-3_8_sil=64000:random_seed=2383473215:i=20139:bs=on_2907 on theBenchmark for (2907ds/20139Mi) % 165.48/23.69 % (380189)Instruction limit reached! % 165.48/23.69 % (380189)------------------------------ % 165.48/23.69 % (380189)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 165.48/23.69 % (380189)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 165.48/23.69 % (380189)CaDiCaL version: 2.1.3 % 165.48/23.69 % (380189)Termination reason: Instruction limit % 165.48/23.69 % (380189)Termination phase: Saturation % 165.48/23.69 % (380189)Time elapsed: 4.418 s % 165.48/23.69 % (380189)Peak memory usage: 65 MB % 165.48/23.69 % (380189)Instructions burned: 8173 (million) % 165.48/23.69 % (380202)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=1342550755:fmbsr=2:i=32576_2896 on theBenchmark for (2896ds/32576Mi) % 165.48/23.69 % (380202)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 165.48/23.69 % (380202)Terminated due to inappropriate strategy. % 165.48/23.69 % (380202)------------------------------ % 165.48/23.69 % (380202)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 165.48/23.69 % (380202)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 165.48/23.69 % (380202)CaDiCaL version: 2.1.3 % 165.48/23.69 % (380202)Termination reason: Inappropriate % 165.48/23.69 % (380202)Time elapsed: 0.012 s % 165.48/23.69 % (380202)Peak memory usage: 11 MB % 165.48/23.69 % (380202)Instructions burned: 12 (million) % 165.48/23.69 % (380202)------------------------------ % 165.48/23.69 % (380202)------------------------------ % 165.48/23.69 % (380205)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=2270243964:i=11404_2896 on theBenchmark for (2896ds/11404Mi) % 165.48/23.69 % (380192)Instruction limit reached! % 165.48/23.69 % (380192)------------------------------ % 165.48/23.69 % (380192)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 165.48/23.69 % (380192)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 165.48/23.69 % (380192)CaDiCaL version: 2.1.3 % 165.48/23.69 % (380192)Termination reason: Instruction limit % 165.48/23.69 % (380192)Termination phase: Saturation % 165.48/23.69 % (380192)Time elapsed: 7.648 s % 165.48/23.69 % (380192)Peak memory usage: 52 MB % 165.48/23.69 % (380192)Instructions burned: 9157 (million) % 165.48/23.69 % (380250)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=1705425460:i=14134_2861 on theBenchmark for (2861ds/14134Mi) % 165.48/23.69 % (380205)Instruction limit reached! % 165.48/23.69 % (380205)------------------------------ % 165.48/23.69 % (380205)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 165.48/23.69 % (380205)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 165.48/23.69 % (380205)CaDiCaL version: 2.1.3 % 165.48/23.69 % (380205)Termination reason: Instruction limit % 165.48/23.69 % (380205)Termination phase: Saturation % 165.48/23.69 % (380205)Time elapsed: 4.958 s % 165.48/23.69 % (380205)Peak memory usage: 93 MB % 165.48/23.69 % (380205)Instructions burned: 11407 (million) % 165.48/23.69 % (380252)dis+33_16_sil=32000:sac=on:random_seed=1040982931:i=15851:nm=0_2846 on theBenchmark for (2846ds/15851Mi) % 165.48/23.69 % (380252)Instruction limit reached! % 165.48/23.69 % (380252)------------------------------ % 165.48/23.69 % (380252)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 165.48/23.69 % (380252)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 165.48/23.69 % (380252)CaDiCaL version: 2.1.3 % 165.48/23.69 % (380252)Termination reason: Instruction limit % 165.48/23.69 % (380252)Termination phase: Saturation % 165.48/23.69 % (380252)Time elapsed: 4.411 s % 165.48/23.69 % (380252)Peak memory usage: 144 MB % 165.48/23.69 % (380252)Instructions burned: 15855 (million) % 165.48/23.69 % (380254)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=1052230185:avsq=on:i=17627:add=on:amm=off_2801 on theBenchmark for (2801ds/17627Mi) % 176.73/25.24 % (380175)Instruction limit reached! % 176.73/25.24 % (380175)------------------------------ % 176.73/25.24 % (380175)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 176.73/25.24 % (380175)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 176.73/25.24 % (380175)CaDiCaL version: 2.1.3 % 176.73/25.24 % (380175)Termination reason: Instruction limit % 176.73/25.24 % (380175)Termination phase: Saturation % 176.73/25.24 % (380175)Time elapsed: 16.155 s % 176.73/25.24 % (380175)Peak memory usage: 136 MB % 176.73/25.24 % (380175)Instructions burned: 29340 (million) % 176.73/25.24 % (380256)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=1642453374:s2a=on:i=53295_2794 on theBenchmark for (2794ds/53295Mi) % 176.73/25.24 % (380250)Instruction limit reached! % 176.73/25.24 % (380250)------------------------------ % 176.73/25.24 % (380250)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 176.73/25.24 % (380250)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 176.73/25.24 % (380250)CaDiCaL version: 2.1.3 % 176.73/25.24 % (380250)Termination reason: Instruction limit % 176.73/25.24 % (380250)Termination phase: Saturation % 176.73/25.24 % (380250)Time elapsed: 8.548 s % 176.73/25.24 % (380250)Peak memory usage: 105 MB % 176.73/25.24 % (380250)Instructions burned: 14134 (million) % 176.73/25.24 % (380199)Instruction limit reached! % 176.73/25.24 % (380199)------------------------------ % 176.73/25.24 % (380199)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 176.73/25.24 % (380199)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 176.73/25.24 % (380199)CaDiCaL version: 2.1.3 % 176.73/25.24 % (380199)Termination reason: Instruction limit % 176.73/25.24 % (380199)Termination phase: Saturation % 176.73/25.24 % (380199)Time elapsed: 13.140 s % 176.73/25.24 % (380199)Peak memory usage: 85 MB % 176.73/25.24 % (380199)Instructions burned: 20139 (million) % 176.73/25.24 % (380258)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=3595520590:i=26857:ins=20_2775 on theBenchmark for (2775ds/26857Mi) % 176.73/25.24 % (380258)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 176.73/25.24 % (380258)Terminated due to inappropriate strategy. % 176.73/25.24 % (380258)------------------------------ % 176.73/25.24 % (380258)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 176.73/25.24 % (380258)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 176.73/25.24 % (380258)CaDiCaL version: 2.1.3 % 176.73/25.24 % (380258)Termination reason: Inappropriate % 176.73/25.24 % (380258)Time elapsed: 0.005 s % 176.73/25.24 % (380258)Peak memory usage: 11 MB % 176.73/25.24 % (380258)Instructions burned: 9 (million) % 176.73/25.24 % (380258)------------------------------ % 176.73/25.24 % (380258)------------------------------ % 176.73/25.24 % (380259)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=3133326722:i=28120:bs=on:fsr=off_2775 on theBenchmark for (2775ds/28120Mi) % 176.73/25.24 % (380261)fmb+10_1_sil=256000:fmbss=7:random_seed=2245426305:fmbsr=1.6:i=182295_2775 on theBenchmark for (2775ds/182295Mi) % 176.73/25.24 % (380261)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 176.73/25.24 % (380261)Terminated due to inappropriate strategy. % 176.73/25.24 % (380261)------------------------------ % 176.73/25.24 % (380261)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 176.73/25.24 % (380261)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 176.73/25.24 % (380261)CaDiCaL version: 2.1.3 % 176.73/25.24 % (380261)Termination reason: Inappropriate % 176.73/25.24 % (380261)Time elapsed: 0.005 s % 176.73/25.24 % (380261)Peak memory usage: 11 MB % 176.73/25.24 % (380261)Instructions burned: 9 (million) % 176.73/25.24 % (380261)------------------------------ % 176.73/25.24 % (380261)------------------------------ % 176.73/25.24 % (380264)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=2140257129:i=44625:gsp=on_2774 on theBenchmark for (2774ds/44625Mi) % 176.73/25.24 % (380264)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 176.73/25.24 % (380264)Terminated due to inappropriate strategy. % 176.73/25.24 % (380264)------------------------------ % 176.73/25.24 % (380264)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 176.73/25.24 % (380264)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 176.73/25.24 % (380264)CaDiCaL version: 2.1.3 % 176.73/25.24 % (380264)Termination reason: Inappropriate % 189.82/27.04 % (380264)Time elapsed: 0.005 s % 189.82/27.04 % (380264)Peak memory usage: 11 MB % 189.82/27.04 % (380264)Instructions burned: 10 (million) % 189.82/27.04 % (380264)------------------------------ % 189.82/27.04 % (380264)------------------------------ % 189.82/27.04 % (380266)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=1588391899:i=160505_2774 on theBenchmark for (2774ds/160505Mi) % 189.82/27.04 % (380266)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 189.82/27.04 % (380266)Terminated due to inappropriate strategy. % 189.82/27.04 % (380266)------------------------------ % 189.82/27.04 % (380266)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 189.82/27.04 % (380266)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 189.82/27.04 % (380266)CaDiCaL version: 2.1.3 % 189.82/27.04 % (380266)Termination reason: Inappropriate % 189.82/27.04 % (380266)Time elapsed: 0.005 s % 189.82/27.04 % (380266)Peak memory usage: 11 MB % 189.82/27.04 % (380266)Instructions burned: 9 (million) % 189.82/27.04 % (380266)------------------------------ % 189.82/27.04 % (380266)------------------------------ % 189.82/27.04 % (380268)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=511821958:fmbsr=1.3:i=225729_2774 on theBenchmark for (2774ds/225729Mi) % 189.82/27.04 % (380268)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 189.82/27.04 % (380268)Terminated due to inappropriate strategy. % 189.82/27.04 % (380268)------------------------------ % 189.82/27.04 % (380268)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 189.82/27.04 % (380268)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 189.82/27.04 % (380268)CaDiCaL version: 2.1.3 % 189.82/27.04 % (380268)Termination reason: Inappropriate % 189.82/27.04 % (380268)Time elapsed: 0.005 s % 189.82/27.04 % (380268)Peak memory usage: 11 MB % 189.82/27.04 % (380268)Instructions burned: 10 (million) % 189.82/27.04 % (380268)------------------------------ % 189.82/27.04 % (380268)------------------------------ % 189.82/27.04 % (380270)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=4009038068:fmbsr=2:i=185024:ins=7_2774 on theBenchmark for (2774ds/185024Mi) % 189.82/27.04 % (380270)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 189.82/27.04 % (380270)Terminated due to inappropriate strategy. % 189.82/27.04 % (380270)------------------------------ % 189.82/27.04 % (380270)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 189.82/27.04 % (380270)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 189.82/27.04 % (380270)CaDiCaL version: 2.1.3 % 189.82/27.04 % (380270)Termination reason: Inappropriate % 189.82/27.04 % (380270)Time elapsed: 0.005 s % 189.82/27.04 % (380270)Peak memory usage: 11 MB % 189.82/27.04 % (380270)Instructions burned: 10 (million) % 189.82/27.04 % (380270)------------------------------ % 189.82/27.04 % (380270)------------------------------ % 189.82/27.04 % (380272)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=2761067178:rtra=on_2773 on theBenchmark for (2773ds/0Mi) % 189.82/27.04 % (380272)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 189.82/27.04 % (380272)Terminated due to inappropriate strategy. % 189.82/27.04 % (380272)------------------------------ % 189.82/27.04 % (380272)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 189.82/27.04 % (380272)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 189.82/27.04 % (380272)CaDiCaL version: 2.1.3 % 189.82/27.04 % (380272)Termination reason: Inappropriate % 189.82/27.04 % (380272)Time elapsed: 0.007 s % 189.82/27.04 % (380272)Peak memory usage: 11 MB % 189.82/27.04 % (380272)Instructions burned: 13 (million) % 189.82/27.04 % (380272)------------------------------ % 189.82/27.04 % (380272)------------------------------ % 189.82/27.04 % (380274)% WARNING: option uhcvi not known. % 189.82/27.04 % (380274)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1934522846:i=271062:add=off:rtra=on:rawr=on_2773 on theBenchmark for (2773ds/271062Mi) % 189.82/27.04 % (380187)Instruction limit reached! % 189.82/27.04 % (380187)------------------------------ % 189.82/27.04 % (380187)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 189.82/27.04 % (380187)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 189.82/27.04 % (380187)CaDiCaL version: 2.1.3 % 189.82/27.04 % (380187)Termination reason: Instruction limit % 189.82/27.04 % (380187)Termination phase: Saturation % 189.82/27.04 % (380187)Time elapsed: 17.629 s % 189.82/27.04 % (380187)Peak memory usage: 115 MB % 189.82/27.04 % (380187)Instructions burned: 22565 (million) % 197.68/28.18 % (380276)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2208255959:i=176048:add=on:rtra=on:rawr=on_2766 on theBenchmark for (2766ds/176048Mi) % 197.68/28.18 % (380254)Instruction limit reached! % 197.68/28.18 % (380254)------------------------------ % 197.68/28.18 % (380254)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 197.68/28.18 % (380254)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 197.68/28.18 % (380254)CaDiCaL version: 2.1.3 % 197.68/28.18 % (380254)Termination reason: Instruction limit % 197.68/28.18 % (380254)Termination phase: Saturation % 197.68/28.18 % (380254)Time elapsed: 4.665 s % 197.68/28.18 % (380254)Peak memory usage: 89 MB % 197.68/28.18 % (380254)Instructions burned: 17631 (million) % 197.68/28.18 % (380278)dis+10_1_sil=32000:si=on:sp=arity:random_seed=2761042518:i=206:fgj=on:rtra=on_2755 on theBenchmark for (2755ds/206Mi) % 197.68/28.18 % (380278)Instruction limit reached! % 197.68/28.18 % (380278)------------------------------ % 197.68/28.18 % (380278)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 197.68/28.18 % (380278)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 197.68/28.18 % (380278)CaDiCaL version: 2.1.3 % 197.68/28.18 % (380278)Termination reason: Instruction limit % 197.68/28.18 % (380278)Termination phase: Saturation % 197.68/28.18 % (380278)Time elapsed: 0.070 s % 197.68/28.18 % (380278)Peak memory usage: 14 MB % 197.68/28.18 % (380278)Instructions burned: 209 (million) % 197.68/28.18 % (380280)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=4277013955:i=232:rtra=on_2754 on theBenchmark for (2754ds/232Mi) % 197.68/28.18 % (380280)Instruction limit reached! % 197.68/28.18 % (380280)------------------------------ % 197.68/28.18 % (380280)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 197.68/28.18 % (380280)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 197.68/28.18 % (380280)CaDiCaL version: 2.1.3 % 197.68/28.18 % (380280)Termination reason: Instruction limit % 197.68/28.18 % (380280)Termination phase: Saturation % 197.68/28.18 % (380280)Time elapsed: 0.083 s % 197.68/28.18 % (380280)Peak memory usage: 14 MB % 197.68/28.18 % (380280)Instructions burned: 235 (million) % 197.68/28.18 % (380282)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=3529904952:i=262:rtra=on_2753 on theBenchmark for (2753ds/262Mi) % 197.68/28.18 % (380282)Instruction limit reached! % 197.68/28.18 % (380282)------------------------------ % 197.68/28.18 % (380282)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 197.68/28.18 % (380282)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 197.68/28.18 % (380282)CaDiCaL version: 2.1.3 % 197.68/28.18 % (380282)Termination reason: Instruction limit % 197.68/28.18 % (380282)Termination phase: Saturation % 197.68/28.18 % (380282)Time elapsed: 0.084 s % 197.68/28.18 % (380282)Peak memory usage: 14 MB % 197.68/28.18 % (380282)Instructions burned: 264 (million) % 197.68/28.18 % (380284)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=1355242120:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2752 on theBenchmark for (2752ds/318Mi) % 197.68/28.18 % (380284)Instruction limit reached! % 197.68/28.18 % (380284)------------------------------ % 197.68/28.18 % (380284)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 197.68/28.18 % (380284)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 197.68/28.18 % (380284)CaDiCaL version: 2.1.3 % 197.68/28.18 % (380284)Termination reason: Instruction limit % 197.68/28.18 % (380284)Termination phase: Saturation % 197.68/28.18 % (380284)Time elapsed: 0.119 s % 197.68/28.18 % (380284)Peak memory usage: 15 MB % 197.68/28.18 % (380284)Instructions burned: 318 (million) % 197.68/28.18 % (380286)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=2298463937:i=1428:nm=2:rtra=on_2750 on theBenchmark for (2750ds/1428Mi) % 197.68/28.18 % (380286)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 197.68/28.18 % (380286)Terminated due to inappropriate strategy. % 197.68/28.18 % (380286)------------------------------ % 197.68/28.18 % (380286)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 197.68/28.18 % (380286)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 197.68/28.18 % (380286)CaDiCaL version: 2.1.3 % 197.68/28.18 % (380286)Termination reason: Inappropriate % 197.68/28.18 % (380286)Time elapsed: 0.003 s % 197.68/28.18 % (380286)Peak memory usage: 11 MB % 197.68/28.18 % (380286)Instructions burned: 10 (million) % 197.68/28.18 % (380286)------------------------------ % 225.31/32.10 % (380286)------------------------------ % 225.31/32.10 % (380288)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=2946927028:i=262:bd=preordered:rtra=on:fsd=on_2750 on theBenchmark for (2750ds/262Mi) % 225.31/32.10 % (380288)Instruction limit reached! % 225.31/32.10 % (380288)------------------------------ % 225.31/32.10 % (380288)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 225.31/32.10 % (380288)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 225.31/32.10 % (380288)CaDiCaL version: 2.1.3 % 225.31/32.10 % (380288)Termination reason: Instruction limit % 225.31/32.10 % (380288)Termination phase: Saturation % 225.31/32.10 % (380288)Time elapsed: 0.094 s % 225.31/32.10 % (380288)Peak memory usage: 14 MB % 225.31/32.10 % (380288)Instructions burned: 263 (million) % 225.31/32.10 % (380290)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:si=on:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=2766437908:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2749 on theBenchmark for (2749ds/1368Mi) % 225.31/32.10 % (380290)Instruction limit reached! % 225.31/32.10 % (380290)------------------------------ % 225.31/32.10 % (380290)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 225.31/32.10 % (380290)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 225.31/32.10 % (380290)CaDiCaL version: 2.1.3 % 225.31/32.10 % (380290)Termination reason: Instruction limit % 225.31/32.10 % (380290)Termination phase: Saturation % 225.31/32.10 % (380290)Time elapsed: 0.363 s % 225.31/32.10 % (380290)Peak memory usage: 19 MB % 225.31/32.10 % (380290)Instructions burned: 1372 (million) % 225.31/32.10 % (380292)ott-21_1_sil=16000:si=on:fs=off:random_seed=2436016343:i=360:av=off:fsr=off:rtra=on_2746 on theBenchmark for (2746ds/360Mi) % 225.31/32.10 % (380292)Instruction limit reached! % 225.31/32.10 % (380292)------------------------------ % 225.31/32.10 % (380292)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 225.31/32.10 % (380292)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 225.31/32.10 % (380292)CaDiCaL version: 2.1.3 % 225.31/32.10 % (380292)Termination reason: Instruction limit % 225.31/32.10 % (380292)Termination phase: Saturation % 225.31/32.10 % (380292)Time elapsed: 0.095 s % 225.31/32.10 % (380292)Peak memory usage: 14 MB % 225.31/32.10 % (380292)Instructions burned: 362 (million) % 225.31/32.10 % (380294)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3559186664:i=954:bd=all:rtra=on_2744 on theBenchmark for (2744ds/954Mi) % 225.31/32.10 % (380294)Instruction limit reached! % 225.31/32.10 % (380294)------------------------------ % 225.31/32.10 % (380294)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 225.31/32.10 % (380294)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 225.31/32.10 % (380294)CaDiCaL version: 2.1.3 % 225.31/32.10 % (380294)Termination reason: Instruction limit % 225.31/32.10 % (380294)Termination phase: Saturation % 225.31/32.10 % (380294)Time elapsed: 0.334 s % 225.31/32.10 % (380294)Peak memory usage: 16 MB % 225.31/32.10 % (380294)Instructions burned: 956 (million) % 225.31/32.10 % (380296)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=2157205278:fmbsr=1.3:i=1730:ins=25:rtra=on_2741 on theBenchmark for (2741ds/1730Mi) % 225.31/32.10 % (380296)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 225.31/32.10 % (380296)Terminated due to inappropriate strategy. % 225.31/32.10 % (380296)------------------------------ % 225.31/32.10 % (380296)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 225.31/32.10 % (380296)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 225.31/32.10 % (380296)CaDiCaL version: 2.1.3 % 225.31/32.10 % (380296)Termination reason: Inappropriate % 225.31/32.10 % (380296)Time elapsed: 0.003 s % 225.31/32.10 % (380296)Peak memory usage: 10 MB % 225.31/32.10 % (380296)Instructions burned: 10 (million) % 225.31/32.10 % (380296)------------------------------ % 225.31/32.10 % (380296)------------------------------ % 225.31/32.10 % (380298)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=3698786999:i=2358:rtra=on_2741 on theBenchmark for (2741ds/2358Mi) % 225.31/32.10 % (380298)Instruction limit reached! % 225.31/32.10 % (380298)------------------------------ % 225.31/32.10 % (380298)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 225.31/32.10 % (380298)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 225.31/32.10 % (380298)CaDiCaL version: 2.1.3 % 225.31/32.10 % (380298)Termination reason: Instruction limit % 269.82/38.35 % (380298)Termination phase: Saturation % 269.82/38.35 % (380298)Time elapsed: 0.836 s % 269.82/38.35 % (380298)Peak memory usage: 30 MB % 269.82/38.35 % (380298)Instructions burned: 2358 (million) % 269.82/38.35 % (380300)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=2600816039:i=1778:ins=1:rtra=on_2732 on theBenchmark for (2732ds/1778Mi) % 269.82/38.35 % (380300)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 269.82/38.35 % (380300)Terminated due to inappropriate strategy. % 269.82/38.35 % (380300)------------------------------ % 269.82/38.35 % (380300)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 269.82/38.35 % (380300)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 269.82/38.35 % (380300)CaDiCaL version: 2.1.3 % 269.82/38.35 % (380300)Termination reason: Inappropriate % 269.82/38.35 % (380300)Time elapsed: 0.003 s % 269.82/38.35 % (380300)Peak memory usage: 10 MB % 269.82/38.35 % (380300)Instructions burned: 10 (million) % 269.82/38.35 % (380300)------------------------------ % 269.82/38.35 % (380300)------------------------------ % 269.82/38.35 % (380302)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:si=on:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=1504127106:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2732 on theBenchmark for (2732ds/1384Mi) % 269.82/38.35 % (380302)Instruction limit reached! % 269.82/38.35 % (380302)------------------------------ % 269.82/38.35 % (380302)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 269.82/38.35 % (380302)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 269.82/38.35 % (380302)CaDiCaL version: 2.1.3 % 269.82/38.35 % (380302)Termination reason: Instruction limit % 269.82/38.35 % (380302)Termination phase: Saturation % 269.82/38.35 % (380302)Time elapsed: 0.518 s % 269.82/38.35 % (380302)Peak memory usage: 32 MB % 269.82/38.35 % (380302)Instructions burned: 1385 (million) % 269.82/38.35 % (380304)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=1032156953:i=1758:kws=inv_precedence:fsr=off:rtra=on_2727 on theBenchmark for (2727ds/1758Mi) % 269.82/38.35 % (380304)Instruction limit reached! % 269.82/38.35 % (380304)------------------------------ % 269.82/38.35 % (380304)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 269.82/38.35 % (380304)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 269.82/38.35 % (380304)CaDiCaL version: 2.1.3 % 269.82/38.35 % (380304)Termination reason: Instruction limit % 269.82/38.35 % (380304)Termination phase: Saturation % 269.82/38.35 % (380304)Time elapsed: 0.537 s % 269.82/38.35 % (380304)Peak memory usage: 24 MB % 269.82/38.35 % (380304)Instructions burned: 1760 (million) % 269.82/38.35 % (380306)fmb+10_1_sil=64000:si=on:random_seed=1238668530:i=44122:nm=2:rtra=on:gsp=on_2721 on theBenchmark for (2721ds/44122Mi) % 269.82/38.35 % (380306)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 269.82/38.35 % (380306)Terminated due to inappropriate strategy. % 269.82/38.35 % (380306)------------------------------ % 269.82/38.35 % (380306)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 269.82/38.35 % (380306)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 269.82/38.35 % (380306)CaDiCaL version: 2.1.3 % 269.82/38.35 % (380306)Termination reason: Inappropriate % 269.82/38.35 % (380306)Time elapsed: 0.003 s % 269.82/38.35 % (380306)Peak memory usage: 11 MB % 269.82/38.35 % (380306)Instructions burned: 11 (million) % 269.82/38.35 % (380306)------------------------------ % 269.82/38.35 % (380306)------------------------------ % 269.82/38.35 % (380308)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=1725249058:i=19030:nm=5:rtra=on_2721 on theBenchmark for (2721ds/19030Mi) % 269.82/38.35 % (380308)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 269.82/38.35 % (380308)Terminated due to inappropriate strategy. % 269.82/38.35 % (380308)------------------------------ % 269.82/38.35 % (380308)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 269.82/38.35 % (380308)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 269.82/38.35 % (380308)CaDiCaL version: 2.1.3 % 269.82/38.35 % (380308)Termination reason: Inappropriate % 269.82/38.35 % (380308)Time elapsed: 0.003 s % 269.82/38.35 % (380308)Peak memory usage: 11 MB % 269.82/38.35 % (380308)Instructions burned: 10 (million) % 269.82/38.35 % (380308)------------------------------ % 269.82/38.35 % (380308)------------------------------ % 269.82/38.35 % (380310)fmb+10_1_sil=64000:sas=cadical:si=on:fmbss=8:random_seed=1974935363:fmbsr=1Terminated % 300.35/42.64 % Vampire exiting %------------------------------------------------------------------------------