%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWX101_1 : TPTP v9.3.1. Released v9.1.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % Computer : n004.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:46:29 PM UTC 2026 % Result : Timeout 300.22s 42.54s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWX101_1 : TPTP v9.3.1. Released v9.1.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.08/0.17 % Computer : n004.cluster.edu % 0.08/0.17 % Model : x86_64 x86_64 % 0.08/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.08/0.17 % Memory : 8046.5625MB % 0.08/0.17 % OS : Linux 6.8.0-71-generic % 0.08/0.17 % CPULimit : 300 % 0.08/0.17 % WCLimit : 300 % 0.08/0.17 % DateTime : Mon Sep 28 15:01:07 UTC 2026 % 0.08/0.17 % CPUTime : % 0.08/0.17 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.08/0.20 Running first-order model finding % 0.08/0.20 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 % 3.95/0.80 % (439100)Will run a generic schedule for satisfiability detection. % 3.95/0.80 % (439106)% WARNING: option uhcvi not known. % 3.95/0.80 % (439105)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1264171128_2999 on theBenchmark for (2999ds/0Mi) % 3.95/0.80 % (439107)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=4123813816:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 3.95/0.80 % (439106)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1877822388:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 3.95/0.80 % (439108)dis+10_1_sil=32000:sp=arity:random_seed=331687296:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 3.95/0.80 % (439109)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3398477016:i=116_2999 on theBenchmark for (2999ds/116Mi) % 3.95/0.80 % (439110)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1688761122:i=131_2999 on theBenchmark for (2999ds/131Mi) % 3.95/0.80 % (439111)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1199828534:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 3.95/0.80 % (439105)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.95/0.80 % (439105)Terminated due to inappropriate strategy. % 3.95/0.80 % (439105)------------------------------ % 3.95/0.80 % (439105)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.95/0.80 % (439105)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.95/0.80 % (439105)CaDiCaL version: 2.1.3 % 3.95/0.80 % (439105)Termination reason: Inappropriate % 3.95/0.80 % (439105)Time elapsed: 0.004 s % 3.95/0.80 % (439105)Peak memory usage: 10 MB % 3.95/0.80 % (439105)Instructions burned: 6 (million) % 3.95/0.80 % (439105)------------------------------ % 3.95/0.80 % (439105)------------------------------ % 3.95/0.80 % (439119)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=218245803:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 3.95/0.80 % (439119)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.95/0.80 % (439119)Terminated due to inappropriate strategy. % 3.95/0.80 % (439119)------------------------------ % 3.95/0.80 % (439119)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.95/0.80 % (439119)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.95/0.80 % (439119)CaDiCaL version: 2.1.3 % 3.95/0.80 % (439119)Termination reason: Inappropriate % 3.95/0.80 % (439119)Time elapsed: 0.001 s % 3.95/0.80 % (439119)Peak memory usage: 10 MB % 3.95/0.80 % (439119)Instructions burned: 5 (million) % 3.95/0.80 % (439119)------------------------------ % 3.95/0.80 % (439119)------------------------------ % 3.95/0.80 % (439121)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1667671838:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 3.95/0.80 % (439108)Instruction limit reached! % 3.95/0.80 % (439108)------------------------------ % 3.95/0.80 % (439108)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.95/0.80 % (439108)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.95/0.80 % (439108)CaDiCaL version: 2.1.3 % 3.95/0.80 % (439108)Termination reason: Instruction limit % 3.95/0.80 % (439108)Termination phase: Saturation % 3.95/0.80 % (439108)Time elapsed: 0.068 s % 3.95/0.80 % (439108)Peak memory usage: 13 MB % 3.95/0.80 % (439108)Instructions burned: 103 (million) % 3.95/0.80 % (439109)Instruction limit reached! % 3.95/0.80 % (439109)------------------------------ % 3.95/0.80 % (439109)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.95/0.80 % (439109)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.95/0.80 % (439109)CaDiCaL version: 2.1.3 % 3.95/0.80 % (439109)Termination reason: Instruction limit % 3.95/0.80 % (439109)Termination phase: Saturation % 3.95/0.80 % (439109)Time elapsed: 0.071 s % 3.95/0.80 % (439109)Peak memory usage: 13 MB % 3.95/0.80 % (439109)Instructions burned: 116 (million) % 3.95/0.80 % (439121)Instruction limit reached! % 3.95/0.80 % (439121)------------------------------ % 3.95/0.80 % (439121)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.95/0.80 % (439121)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.95/0.80 % (439121)CaDiCaL version: 2.1.3 % 3.95/0.80 % (439121)Termination reason: Instruction limit % 3.95/0.80 % (439121)Termination phase: Saturation % 7.57/1.36 % (439121)Time elapsed: 0.045 s % 7.57/1.36 % (439121)Peak memory usage: 13 MB % 7.57/1.36 % (439121)Instructions burned: 132 (million) % 7.57/1.36 % (439110)Instruction limit reached! % 7.57/1.36 % (439110)------------------------------ % 7.57/1.36 % (439110)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.57/1.36 % (439110)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.57/1.36 % (439110)CaDiCaL version: 2.1.3 % 7.57/1.36 % (439110)Termination reason: Instruction limit % 7.57/1.36 % (439110)Termination phase: Saturation % 7.57/1.36 % (439110)Time elapsed: 0.083 s % 7.57/1.36 % (439110)Peak memory usage: 13 MB % 7.57/1.36 % (439110)Instructions burned: 131 (million) % 7.57/1.36 % (439123)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=3388827383:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi) % 7.57/1.36 % (439125)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=441034785:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 7.57/1.36 % (439124)ott-21_1_sil=16000:fs=off:random_seed=2738670357:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 7.57/1.36 % (439126)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1582876494:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 7.57/1.36 % (439126)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 7.57/1.36 % (439126)Terminated due to inappropriate strategy. % 7.57/1.36 % (439126)------------------------------ % 7.57/1.36 % (439126)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.57/1.36 % (439126)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.57/1.36 % (439126)CaDiCaL version: 2.1.3 % 7.57/1.36 % (439126)Termination reason: Inappropriate % 7.57/1.36 % (439126)Time elapsed: 0.002 s % 7.57/1.36 % (439126)Peak memory usage: 10 MB % 7.57/1.36 % (439126)Instructions burned: 3 (million) % 7.57/1.36 % (439126)------------------------------ % 7.57/1.36 % (439126)------------------------------ % 7.57/1.36 % (439111)Instruction limit reached! % 7.57/1.36 % (439111)------------------------------ % 7.57/1.36 % (439111)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.57/1.36 % (439111)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.57/1.36 % (439111)CaDiCaL version: 2.1.3 % 7.57/1.36 % (439111)Termination reason: Instruction limit % 7.57/1.36 % (439111)Termination phase: Saturation % 7.57/1.36 % (439111)Time elapsed: 0.111 s % 7.57/1.36 % (439111)Peak memory usage: 14 MB % 7.57/1.36 % (439111)Instructions burned: 159 (million) % 7.57/1.36 % (439131)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=598288744:i=1179_2998 on theBenchmark for (2998ds/1179Mi) % 7.57/1.36 % (439132)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=564337092:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi) % 7.57/1.36 % (439132)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 7.57/1.36 % (439132)Terminated due to inappropriate strategy. % 7.57/1.36 % (439132)------------------------------ % 7.57/1.36 % (439132)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.57/1.36 % (439132)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.57/1.36 % (439132)CaDiCaL version: 2.1.3 % 7.57/1.36 % (439132)Termination reason: Inappropriate % 7.57/1.36 % (439132)Time elapsed: 0.003 s % 7.57/1.36 % (439132)Peak memory usage: 10 MB % 7.57/1.36 % (439132)Instructions burned: 4 (million) % 7.57/1.36 % (439132)------------------------------ % 7.57/1.36 % (439132)------------------------------ % 7.57/1.36 % (439135)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=2084749181:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2998 on theBenchmark for (2998ds/692Mi) % 7.57/1.36 % (439124)Instruction limit reached! % 7.57/1.36 % (439124)------------------------------ % 7.57/1.36 % (439124)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.57/1.36 % (439124)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.57/1.36 % (439124)CaDiCaL version: 2.1.3 % 7.57/1.36 % (439124)Termination reason: Instruction limit % 7.57/1.36 % (439124)Termination phase: Saturation % 7.57/1.36 % (439124)Time elapsed: 0.087 s % 7.57/1.36 % (439124)Peak memory usage: 12 MB % 7.57/1.36 % (439124)Instructions burned: 180 (million) % 20.93/3.21 % (439137)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1385805991:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi) % 20.93/3.21 % (439125)Instruction limit reached! % 20.93/3.21 % (439125)------------------------------ % 20.93/3.21 % (439125)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 20.93/3.21 % (439125)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.93/3.21 % (439125)CaDiCaL version: 2.1.3 % 20.93/3.21 % (439125)Termination reason: Instruction limit % 20.93/3.21 % (439125)Termination phase: Saturation % 20.93/3.21 % (439125)Time elapsed: 0.173 s % 20.93/3.21 % (439125)Peak memory usage: 14 MB % 20.93/3.21 % (439125)Instructions burned: 478 (million) % 20.93/3.21 % (439139)fmb+10_1_sil=64000:random_seed=1716281542:i=22061:nm=2:gsp=on_2997 on theBenchmark for (2997ds/22061Mi) % 20.93/3.21 % (439139)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 20.93/3.21 % (439139)Terminated due to inappropriate strategy. % 20.93/3.21 % (439139)------------------------------ % 20.93/3.21 % (439139)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 20.93/3.21 % (439139)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.93/3.21 % (439139)CaDiCaL version: 2.1.3 % 20.93/3.21 % (439139)Termination reason: Inappropriate % 20.93/3.21 % (439139)Time elapsed: 0.002 s % 20.93/3.21 % (439139)Peak memory usage: 10 MB % 20.93/3.21 % (439139)Instructions burned: 5 (million) % 20.93/3.21 % (439139)------------------------------ % 20.93/3.21 % (439139)------------------------------ % 20.93/3.21 % (439141)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1195214378:i=9515:nm=5_2996 on theBenchmark for (2996ds/9515Mi) % 20.93/3.21 % (439141)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 20.93/3.21 % (439141)Terminated due to inappropriate strategy. % 20.93/3.21 % (439141)------------------------------ % 20.93/3.21 % (439141)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 20.93/3.21 % (439141)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.93/3.21 % (439141)CaDiCaL version: 2.1.3 % 20.93/3.21 % (439141)Termination reason: Inappropriate % 20.93/3.21 % (439141)Time elapsed: 0.001 s % 20.93/3.21 % (439141)Peak memory usage: 10 MB % 20.93/3.21 % (439141)Instructions burned: 5 (million) % 20.93/3.21 % (439141)------------------------------ % 20.93/3.21 % (439141)------------------------------ % 20.93/3.21 % (439143)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2754562345:fmbsr=1.7:i=920_2996 on theBenchmark for (2996ds/920Mi) % 20.93/3.21 % (439143)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 20.93/3.21 % (439143)Terminated due to inappropriate strategy. % 20.93/3.21 % (439143)------------------------------ % 20.93/3.21 % (439143)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 20.93/3.21 % (439143)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.93/3.21 % (439143)CaDiCaL version: 2.1.3 % 20.93/3.21 % (439143)Termination reason: Inappropriate % 20.93/3.21 % (439143)Time elapsed: 0.001 s % 20.93/3.21 % (439143)Peak memory usage: 10 MB % 20.93/3.21 % (439143)Instructions burned: 5 (million) % 20.93/3.21 % (439143)------------------------------ % 20.93/3.21 % (439143)------------------------------ % 20.93/3.21 % (439145)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2800058913:i=5131_2996 on theBenchmark for (2996ds/5131Mi) % 20.93/3.21 % (439123)Instruction limit reached! % 20.93/3.21 % (439123)------------------------------ % 20.93/3.21 % (439123)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 20.93/3.21 % (439123)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.93/3.21 % (439123)CaDiCaL version: 2.1.3 % 20.93/3.21 % (439123)Termination reason: Instruction limit % 20.93/3.21 % (439123)Termination phase: Saturation % 20.93/3.21 % (439123)Time elapsed: 0.434 s % 20.93/3.21 % (439123)Peak memory usage: 18 MB % 20.93/3.21 % (439123)Instructions burned: 685 (million) % 20.93/3.21 % (439147)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=128384554:i=1472:ins=7:fdi=8:gsp=on_2994 on theBenchmark for (2994ds/1472Mi) % 20.93/3.21 % (439135)Instruction limit reached! % 20.93/3.21 % (439135)------------------------------ % 20.93/3.21 % (439135)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 20.93/3.21 % (439135)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.77/3.77 % (439135)CaDiCaL version: 2.1.3 % 22.77/3.77 % (439135)Termination reason: Instruction limit % 22.77/3.77 % (439135)Termination phase: Saturation % 22.77/3.77 % (439135)Time elapsed: 0.414 s % 22.77/3.77 % (439135)Peak memory usage: 17 MB % 22.77/3.77 % (439135)Instructions burned: 693 (million) % 22.77/3.77 % (439149)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=4023042542:i=6324_2993 on theBenchmark for (2993ds/6324Mi) % 22.77/3.77 % (439149)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 22.77/3.77 % (439149)Terminated due to inappropriate strategy. % 22.77/3.77 % (439149)------------------------------ % 22.77/3.77 % (439149)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.77/3.77 % (439149)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.77/3.77 % (439149)CaDiCaL version: 2.1.3 % 22.77/3.77 % (439149)Termination reason: Inappropriate % 22.77/3.77 % (439149)Time elapsed: 0.004 s % 22.77/3.77 % (439149)Peak memory usage: 11 MB % 22.77/3.77 % (439149)Instructions burned: 6 (million) % 22.77/3.77 % (439149)------------------------------ % 22.77/3.77 % (439149)------------------------------ % 22.77/3.77 % (439151)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=770172241:fmbsr=2.30978:i=2174_2993 on theBenchmark for (2993ds/2174Mi) % 22.77/3.77 % (439151)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 22.77/3.77 % (439151)Terminated due to inappropriate strategy. % 22.77/3.77 % (439151)------------------------------ % 22.77/3.77 % (439151)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.77/3.77 % (439151)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.77/3.77 % (439151)CaDiCaL version: 2.1.3 % 22.77/3.77 % (439151)Termination reason: Inappropriate % 22.77/3.77 % (439151)Time elapsed: 0.003 s % 22.77/3.77 % (439151)Peak memory usage: 10 MB % 22.77/3.77 % (439151)Instructions burned: 5 (million) % 22.77/3.77 % (439151)------------------------------ % 22.77/3.77 % (439151)------------------------------ % 22.77/3.77 % (439153)ott-2_1_sil=16000:newcnf=on:random_seed=694285653:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2993 on theBenchmark for (2993ds/869Mi) % 22.77/3.77 % (439137)Instruction limit reached! % 22.77/3.77 % (439137)------------------------------ % 22.77/3.77 % (439137)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.77/3.77 % (439137)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.77/3.77 % (439137)CaDiCaL version: 2.1.3 % 22.77/3.77 % (439137)Termination reason: Instruction limit % 22.77/3.77 % (439137)Termination phase: Saturation % 22.77/3.77 % (439137)Time elapsed: 0.492 s % 22.77/3.77 % (439137)Peak memory usage: 19 MB % 22.77/3.77 % (439137)Instructions burned: 880 (million) % 22.77/3.77 % (439155)ott+10_1_sil=32000:tgt=ground:random_seed=1271373108:i=5114:av=off_2992 on theBenchmark for (2992ds/5114Mi) % 22.77/3.77 % (439131)Instruction limit reached! % 22.77/3.77 % (439131)------------------------------ % 22.77/3.77 % (439131)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.77/3.77 % (439131)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.77/3.77 % (439131)CaDiCaL version: 2.1.3 % 22.77/3.77 % (439131)Termination reason: Instruction limit % 22.77/3.77 % (439131)Termination phase: Saturation % 22.77/3.77 % (439131)Time elapsed: 0.701 s % 22.77/3.77 % (439131)Peak memory usage: 22 MB % 22.77/3.77 % (439131)Instructions burned: 1179 (million) % 22.77/3.77 % (439157)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=3545051063:i=54282_2991 on theBenchmark for (2991ds/54282Mi) % 22.77/3.77 % (439157)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 22.77/3.77 % (439157)Terminated due to inappropriate strategy. % 22.77/3.77 % (439157)------------------------------ % 22.77/3.77 % (439157)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.77/3.77 % (439157)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.77/3.77 % (439157)CaDiCaL version: 2.1.3 % 22.77/3.77 % (439157)Termination reason: Inappropriate % 22.77/3.77 % (439157)Time elapsed: 0.004 s % 22.77/3.77 % (439157)Peak memory usage: 11 MB % 22.77/3.77 % (439157)Instructions burned: 6 (million) % 22.77/3.77 % (439157)------------------------------ % 22.77/3.77 % (439157)------------------------------ % 22.77/3.77 % (439159)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=676997540:i=3512:aac=none_2991 on theBenchmark for (2991ds/3512Mi) % 22.77/3.77 % (439153)Instruction limit reached! % 92.26/13.25 % (439153)------------------------------ % 92.26/13.25 % (439153)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 92.26/13.25 % (439153)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 92.26/13.25 % (439153)CaDiCaL version: 2.1.3 % 92.26/13.25 % (439153)Termination reason: Instruction limit % 92.26/13.25 % (439153)Termination phase: Saturation % 92.26/13.25 % (439153)Time elapsed: 0.487 s % 92.26/13.25 % (439153)Peak memory usage: 19 MB % 92.26/13.25 % (439153)Instructions burned: 869 (million) % 92.26/13.25 % (439161)dis+21_1_sil=32000:sas=cadical:random_seed=1782774169:i=3773:amm=off_2988 on theBenchmark for (2988ds/3773Mi) % 92.26/13.25 % (439147)Instruction limit reached! % 92.26/13.25 % (439147)------------------------------ % 92.26/13.25 % (439147)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 92.26/13.25 % (439147)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 92.26/13.25 % (439147)CaDiCaL version: 2.1.3 % 92.26/13.25 % (439147)Termination reason: Instruction limit % 92.26/13.25 % (439147)Termination phase: Saturation % 92.26/13.25 % (439147)Time elapsed: 0.883 s % 92.26/13.25 % (439147)Peak memory usage: 33 MB % 92.26/13.25 % (439147)Instructions burned: 1473 (million) % 92.26/13.25 % (439163)ott+11_1_sil=16000:gs=on:random_seed=3487961962:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2985 on theBenchmark for (2985ds/2251Mi) % 92.26/13.25 % (439145)Instruction limit reached! % 92.26/13.25 % (439145)------------------------------ % 92.26/13.25 % (439145)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 92.26/13.25 % (439145)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 92.26/13.25 % (439145)CaDiCaL version: 2.1.3 % 92.26/13.25 % (439145)Termination reason: Instruction limit % 92.26/13.25 % (439145)Termination phase: Saturation % 92.26/13.25 % (439145)Time elapsed: 1.450 s % 92.26/13.25 % (439145)Peak memory usage: 41 MB % 92.26/13.25 % (439145)Instructions burned: 5133 (million) % 92.26/13.25 % (439165)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=2726386110:fmbsr=1.6:i=67534_2982 on theBenchmark for (2982ds/67534Mi) % 92.26/13.25 % (439165)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 92.26/13.25 % (439165)Terminated due to inappropriate strategy. % 92.26/13.25 % (439165)------------------------------ % 92.26/13.25 % (439165)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 92.26/13.25 % (439165)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 92.26/13.25 % (439165)CaDiCaL version: 2.1.3 % 92.26/13.25 % (439165)Termination reason: Inappropriate % 92.26/13.25 % (439165)Time elapsed: 0.002 s % 92.26/13.25 % (439165)Peak memory usage: 11 MB % 92.26/13.25 % (439165)Instructions burned: 5 (million) % 92.26/13.25 % (439165)------------------------------ % 92.26/13.25 % (439165)------------------------------ % 92.26/13.25 % (439167)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=3945683697:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2981 on theBenchmark for (2981ds/4591Mi) % 92.26/13.25 % (439159)Instruction limit reached! % 92.26/13.25 % (439159)------------------------------ % 92.26/13.25 % (439159)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 92.26/13.25 % (439159)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 92.26/13.25 % (439159)CaDiCaL version: 2.1.3 % 92.26/13.25 % (439159)Termination reason: Instruction limit % 92.26/13.25 % (439159)Termination phase: Saturation % 92.26/13.25 % (439159)Time elapsed: 1.904 s % 92.26/13.25 % (439159)Peak memory usage: 36 MB % 92.26/13.25 % (439159)Instructions burned: 3513 (million) % 92.26/13.25 % (439163)Instruction limit reached! % 92.26/13.25 % (439163)------------------------------ % 92.26/13.25 % (439163)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 92.26/13.25 % (439163)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 92.26/13.25 % (439163)CaDiCaL version: 2.1.3 % 92.26/13.25 % (439163)Termination reason: Instruction limit % 92.26/13.25 % (439163)Termination phase: Saturation % 92.26/13.25 % (439163)Time elapsed: 1.343 s % 92.26/13.25 % (439163)Peak memory usage: 27 MB % 92.26/13.25 % (439163)Instructions burned: 2251 (million) % 92.26/13.25 % (439169)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=823764066:i=29340_2971 on theBenchmark for (2971ds/29340Mi) % 92.26/13.25 % (439170)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=878239608:i=5211_2971 on theBenchmark for (2971ds/5211Mi) % 92.26/13.25 % (439167)Instruction limit reached! % 122.60/17.59 % (439167)------------------------------ % 122.60/17.59 % (439167)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 122.60/17.59 % (439167)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 122.60/17.59 % (439167)CaDiCaL version: 2.1.3 % 122.60/17.59 % (439167)Termination reason: Instruction limit % 122.60/17.59 % (439167)Termination phase: Saturation % 122.60/17.59 % (439167)Time elapsed: 1.182 s % 122.60/17.59 % (439167)Peak memory usage: 41 MB % 122.60/17.59 % (439167)Instructions burned: 4600 (million) % 122.60/17.59 % (439173)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=2331193794:i=5497:nm=2_2969 on theBenchmark for (2969ds/5497Mi) % 122.60/17.59 % (439173)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 122.60/17.59 % (439173)Terminated due to inappropriate strategy. % 122.60/17.59 % (439173)------------------------------ % 122.60/17.59 % (439173)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 122.60/17.59 % (439173)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 122.60/17.59 % (439173)CaDiCaL version: 2.1.3 % 122.60/17.59 % (439173)Termination reason: Inappropriate % 122.60/17.59 % (439173)Time elapsed: 0.002 s % 122.60/17.59 % (439173)Peak memory usage: 11 MB % 122.60/17.59 % (439173)Instructions burned: 6 (million) % 122.60/17.59 % (439173)------------------------------ % 122.60/17.59 % (439173)------------------------------ % 122.60/17.59 % (439175)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=1340265098:fmbsr=2:i=46332_2969 on theBenchmark for (2969ds/46332Mi) % 122.60/17.59 % (439175)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 122.60/17.59 % (439175)Terminated due to inappropriate strategy. % 122.60/17.59 % (439175)------------------------------ % 122.60/17.59 % (439175)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 122.60/17.59 % (439175)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 122.60/17.59 % (439175)CaDiCaL version: 2.1.3 % 122.60/17.59 % (439175)Termination reason: Inappropriate % 122.60/17.59 % (439175)Time elapsed: 0.001 s % 122.60/17.59 % (439175)Peak memory usage: 11 MB % 122.60/17.59 % (439175)Instructions burned: 5 (million) % 122.60/17.59 % (439175)------------------------------ % 122.60/17.59 % (439175)------------------------------ % 122.60/17.59 % (439177)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=3764166290:i=14071_2969 on theBenchmark for (2969ds/14071Mi) % 122.60/17.59 % (439177)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 122.60/17.59 % (439177)Terminated due to inappropriate strategy. % 122.60/17.59 % (439177)------------------------------ % 122.60/17.59 % (439177)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 122.60/17.59 % (439177)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 122.60/17.59 % (439177)CaDiCaL version: 2.1.3 % 122.60/17.59 % (439177)Termination reason: Inappropriate % 122.60/17.59 % (439177)Time elapsed: 0.001 s % 122.60/17.59 % (439177)Peak memory usage: 11 MB % 122.60/17.59 % (439177)Instructions burned: 5 (million) % 122.60/17.59 % (439177)------------------------------ % 122.60/17.59 % (439177)------------------------------ % 122.60/17.59 % (439179)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2353392034:i=22565:add=on:rawr=on_2969 on theBenchmark for (2969ds/22565Mi) % 122.60/17.59 % (439161)Instruction limit reached! % 122.60/17.59 % (439161)------------------------------ % 122.60/17.59 % (439161)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 122.60/17.59 % (439161)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 122.60/17.59 % (439161)CaDiCaL version: 2.1.3 % 122.60/17.59 % (439161)Termination reason: Instruction limit % 122.60/17.59 % (439161)Termination phase: Saturation % 122.60/17.59 % (439161)Time elapsed: 2.051 s % 122.60/17.59 % (439161)Peak memory usage: 35 MB % 122.60/17.59 % (439161)Instructions burned: 3774 (million) % 122.60/17.59 % (439181)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=2403055390:i=8173:av=off_2967 on theBenchmark for (2967ds/8173Mi) % 122.60/17.59 % (439155)Instruction limit reached! % 122.60/17.59 % (439155)------------------------------ % 122.60/17.59 % (439155)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 122.60/17.59 % (439155)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 122.60/17.59 % (439155)CaDiCaL version: 2.1.3 % 122.60/17.59 % (439155)Termination reason: Instruction limit % 122.60/17.59 % (439155)Termination phase: Saturation % 122.60/17.59 % (439155)Time elapsed: 2.822 s % 127.75/18.26 % (439155)Peak memory usage: 31 MB % 127.75/18.26 % (439155)Instructions burned: 5114 (million) % 127.75/18.26 % (439183)dis+10_16:1_sil=16000:random_seed=3039372628:i=9155:fsr=off_2964 on theBenchmark for (2964ds/9155Mi) % 127.75/18.26 % (439170)Instruction limit reached! % 127.75/18.26 % (439170)------------------------------ % 127.75/18.26 % (439170)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 127.75/18.26 % (439170)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 127.75/18.26 % (439170)CaDiCaL version: 2.1.3 % 127.75/18.26 % (439170)Termination reason: Instruction limit % 127.75/18.26 % (439170)Termination phase: Saturation % 127.75/18.26 % (439170)Time elapsed: 2.634 s % 127.75/18.26 % (439170)Peak memory usage: 45 MB % 127.75/18.26 % (439170)Instructions burned: 5211 (million) % 127.75/18.26 % (439185)ott-3_8_sil=64000:random_seed=870784592:i=20139:bs=on_2945 on theBenchmark for (2945ds/20139Mi) % 127.75/18.26 % (439181)Instruction limit reached! % 127.75/18.26 % (439181)------------------------------ % 127.75/18.26 % (439181)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 127.75/18.26 % (439181)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 127.75/18.26 % (439181)CaDiCaL version: 2.1.3 % 127.75/18.26 % (439181)Termination reason: Instruction limit % 127.75/18.26 % (439181)Termination phase: Saturation % 127.75/18.26 % (439181)Time elapsed: 4.783 s % 127.75/18.26 % (439181)Peak memory usage: 51 MB % 127.75/18.26 % (439181)Instructions burned: 8173 (million) % 127.75/18.26 % (439188)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=253048213:fmbsr=2:i=32576_2919 on theBenchmark for (2919ds/32576Mi) % 127.75/18.26 % (439188)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 127.75/18.26 % (439188)Terminated due to inappropriate strategy. % 127.75/18.26 % (439188)------------------------------ % 127.75/18.26 % (439188)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 127.75/18.26 % (439188)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 127.75/18.26 % (439188)CaDiCaL version: 2.1.3 % 127.75/18.26 % (439188)Termination reason: Inappropriate % 127.75/18.26 % (439188)Time elapsed: 0.004 s % 127.75/18.26 % (439188)Peak memory usage: 11 MB % 127.75/18.26 % (439188)Instructions burned: 6 (million) % 127.75/18.26 % (439188)------------------------------ % 127.75/18.26 % (439188)------------------------------ % 127.75/18.26 % (439190)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=254003789:i=11404_2919 on theBenchmark for (2919ds/11404Mi) % 127.75/18.26 % (439179)Instruction limit reached! % 127.75/18.26 % (439179)------------------------------ % 127.75/18.26 % (439179)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 127.75/18.26 % (439179)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 127.75/18.26 % (439179)CaDiCaL version: 2.1.3 % 127.75/18.26 % (439179)Termination reason: Instruction limit % 127.75/18.26 % (439179)Termination phase: Saturation % 127.75/18.26 % (439179)Time elapsed: 5.090 s % 127.75/18.26 % (439179)Peak memory usage: 81 MB % 127.75/18.26 % (439179)Instructions burned: 22568 (million) % 127.75/18.26 % (439192)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=3540273370:i=14134_2918 on theBenchmark for (2918ds/14134Mi) % 127.75/18.26 % (439183)Instruction limit reached! % 127.75/18.26 % (439183)------------------------------ % 127.75/18.26 % (439183)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 127.75/18.26 % (439183)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 127.75/18.26 % (439183)CaDiCaL version: 2.1.3 % 127.75/18.26 % (439183)Termination reason: Instruction limit % 127.75/18.26 % (439183)Termination phase: Saturation % 127.75/18.26 % (439183)Time elapsed: 4.729 s % 127.75/18.26 % (439183)Peak memory usage: 58 MB % 127.75/18.26 % (439183)Instructions burned: 9156 (million) % 127.75/18.26 % (439194)dis+33_16_sil=32000:sac=on:random_seed=1041091224:i=15851:nm=0_2916 on theBenchmark for (2916ds/15851Mi) % 127.75/18.26 % (439192)Instruction limit reached! % 127.75/18.26 % (439192)------------------------------ % 127.75/18.26 % (439192)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 127.75/18.26 % (439192)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 127.75/18.26 % (439192)CaDiCaL version: 2.1.3 % 127.75/18.26 % (439192)Termination reason: Instruction limit % 127.75/18.26 % (439192)Termination phase: Saturation % 127.75/18.26 % (439192)Time elapsed: 4.860 s % 127.75/18.26 % (439192)Peak memory usage: 72 MB % 127.75/18.26 % (439192)Instructions burned: 14135 (million) % 127.75/18.26 % (439196)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=1794778039:avsq=on:i=17627:add=on:amm=off_2869 on theBenchmark for (2869ds/17627Mi) % 136.27/19.41 % (439190)Instruction limit reached! % 136.27/19.41 % (439190)------------------------------ % 136.27/19.41 % (439190)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 136.27/19.41 % (439190)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 136.27/19.41 % (439190)CaDiCaL version: 2.1.3 % 136.27/19.41 % (439190)Termination reason: Instruction limit % 136.27/19.41 % (439190)Termination phase: Saturation % 136.27/19.41 % (439190)Time elapsed: 7.189 s % 136.27/19.41 % (439190)Peak memory usage: 74 MB % 136.27/19.41 % (439190)Instructions burned: 11404 (million) % 136.27/19.41 % (439198)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=2335044596:s2a=on:i=53295_2847 on theBenchmark for (2847ds/53295Mi) % 136.27/19.41 % (439185)Instruction limit reached! % 136.27/19.41 % (439185)------------------------------ % 136.27/19.41 % (439185)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 136.27/19.41 % (439185)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 136.27/19.41 % (439185)CaDiCaL version: 2.1.3 % 136.27/19.41 % (439185)Termination reason: Instruction limit % 136.27/19.41 % (439185)Termination phase: Saturation % 136.27/19.41 % (439185)Time elapsed: 11.569 s % 136.27/19.41 % (439185)Peak memory usage: 108 MB % 136.27/19.41 % (439185)Instructions burned: 20141 (million) % 136.27/19.41 % (439200)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=1462232230:i=26857:ins=20_2829 on theBenchmark for (2829ds/26857Mi) % 136.27/19.41 % (439200)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 136.27/19.41 % (439200)Terminated due to inappropriate strategy. % 136.27/19.41 % (439200)------------------------------ % 136.27/19.41 % (439200)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 136.27/19.41 % (439200)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 136.27/19.41 % (439200)CaDiCaL version: 2.1.3 % 136.27/19.41 % (439200)Termination reason: Inappropriate % 136.27/19.41 % (439200)Time elapsed: 0.003 s % 136.27/19.41 % (439200)Peak memory usage: 10 MB % 136.27/19.41 % (439200)Instructions burned: 5 (million) % 136.27/19.41 % (439200)------------------------------ % 136.27/19.41 % (439200)------------------------------ % 136.27/19.41 % (439202)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=1996396269:i=28120:bs=on:fsr=off_2828 on theBenchmark for (2828ds/28120Mi) % 136.27/19.41 % (439194)Instruction limit reached! % 136.27/19.41 % (439194)------------------------------ % 136.27/19.41 % (439194)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 136.27/19.41 % (439194)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 136.27/19.41 % (439194)CaDiCaL version: 2.1.3 % 136.27/19.41 % (439194)Termination reason: Instruction limit % 136.27/19.41 % (439194)Termination phase: Saturation % 136.27/19.41 % (439194)Time elapsed: 8.982 s % 136.27/19.41 % (439194)Peak memory usage: 125 MB % 136.27/19.41 % (439194)Instructions burned: 15853 (million) % 136.27/19.41 % (439204)fmb+10_1_sil=256000:fmbss=7:random_seed=3656517149:fmbsr=1.6:i=182295_2826 on theBenchmark for (2826ds/182295Mi) % 136.27/19.41 % (439204)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 136.27/19.41 % (439204)Terminated due to inappropriate strategy. % 136.27/19.41 % (439204)------------------------------ % 136.27/19.41 % (439204)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 136.27/19.41 % (439204)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 136.27/19.41 % (439204)CaDiCaL version: 2.1.3 % 136.27/19.41 % (439204)Termination reason: Inappropriate % 136.27/19.41 % (439204)Time elapsed: 0.003 s % 136.27/19.41 % (439204)Peak memory usage: 10 MB % 136.27/19.41 % (439204)Instructions burned: 5 (million) % 136.27/19.41 % (439204)------------------------------ % 136.27/19.41 % (439204)------------------------------ % 136.27/19.41 % (439206)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=795745341:i=44625:gsp=on_2826 on theBenchmark for (2826ds/44625Mi) % 136.27/19.41 % (439206)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 136.27/19.41 % (439206)Terminated due to inappropriate strategy. % 136.27/19.41 % (439206)------------------------------ % 136.27/19.41 % (439206)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 136.27/19.41 % (439206)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 136.27/19.41 % (439206)CaDiCaL version: 2.1.3 % 136.27/19.41 % (439206)Termination reason: Inappropriate % 149.76/21.30 % (439206)Time elapsed: 0.003 s % 149.76/21.30 % (439206)Peak memory usage: 11 MB % 149.76/21.30 % (439206)Instructions burned: 5 (million) % 149.76/21.30 % (439206)------------------------------ % 149.76/21.30 % (439206)------------------------------ % 149.76/21.30 % (439208)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=2690559656:i=160505_2826 on theBenchmark for (2826ds/160505Mi) % 149.76/21.30 % (439208)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 149.76/21.30 % (439208)Terminated due to inappropriate strategy. % 149.76/21.30 % (439208)------------------------------ % 149.76/21.30 % (439208)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 149.76/21.30 % (439208)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 149.76/21.30 % (439208)CaDiCaL version: 2.1.3 % 149.76/21.30 % (439208)Termination reason: Inappropriate % 149.76/21.30 % (439208)Time elapsed: 0.003 s % 149.76/21.30 % (439208)Peak memory usage: 10 MB % 149.76/21.30 % (439208)Instructions burned: 5 (million) % 149.76/21.30 % (439208)------------------------------ % 149.76/21.30 % (439208)------------------------------ % 149.76/21.30 % (439210)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=986619962:fmbsr=1.3:i=225729_2825 on theBenchmark for (2825ds/225729Mi) % 149.76/21.30 % (439210)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 149.76/21.30 % (439210)Terminated due to inappropriate strategy. % 149.76/21.30 % (439210)------------------------------ % 149.76/21.30 % (439210)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 149.76/21.30 % (439210)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 149.76/21.30 % (439210)CaDiCaL version: 2.1.3 % 149.76/21.30 % (439210)Termination reason: Inappropriate % 149.76/21.30 % (439210)Time elapsed: 0.003 s % 149.76/21.30 % (439210)Peak memory usage: 11 MB % 149.76/21.30 % (439210)Instructions burned: 5 (million) % 149.76/21.30 % (439210)------------------------------ % 149.76/21.30 % (439210)------------------------------ % 149.76/21.30 % (439212)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=61136313:fmbsr=2:i=185024:ins=7_2825 on theBenchmark for (2825ds/185024Mi) % 149.76/21.30 % (439212)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 149.76/21.30 % (439212)Terminated due to inappropriate strategy. % 149.76/21.30 % (439212)------------------------------ % 149.76/21.30 % (439212)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 149.76/21.30 % (439212)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 149.76/21.30 % (439212)CaDiCaL version: 2.1.3 % 149.76/21.30 % (439212)Termination reason: Inappropriate % 149.76/21.30 % (439212)Time elapsed: 0.003 s % 149.76/21.30 % (439212)Peak memory usage: 11 MB % 149.76/21.30 % (439212)Instructions burned: 5 (million) % 149.76/21.30 % (439212)------------------------------ % 149.76/21.30 % (439212)------------------------------ % 149.76/21.30 % (439214)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=2628209145:rtra=on_2825 on theBenchmark for (2825ds/0Mi) % 149.76/21.30 % (439214)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 149.76/21.30 % (439214)Terminated due to inappropriate strategy. % 149.76/21.30 % (439214)------------------------------ % 149.76/21.30 % (439214)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 149.76/21.30 % (439214)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 149.76/21.30 % (439214)CaDiCaL version: 2.1.3 % 149.76/21.30 % (439214)Termination reason: Inappropriate % 149.76/21.30 % (439214)Time elapsed: 0.004 s % 149.76/21.30 % (439214)Peak memory usage: 11 MB % 149.76/21.30 % (439214)Instructions burned: 6 (million) % 149.76/21.30 % (439214)------------------------------ % 149.76/21.30 % (439214)------------------------------ % 149.76/21.30 % (439216)% WARNING: option uhcvi not known. % 149.76/21.30 % (439216)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1074133690:i=271062:add=off:rtra=on:rawr=on_2825 on theBenchmark for (2825ds/271062Mi) % 149.76/21.30 % (439169)Instruction limit reached! % 149.76/21.30 % (439169)------------------------------ % 149.76/21.30 % (439169)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 149.76/21.30 % (439169)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 149.76/21.30 % (439169)CaDiCaL version: 2.1.3 % 149.76/21.30 % (439169)Termination reason: Instruction limit % 149.76/21.30 % (439169)Termination phase: Saturation % 149.76/21.30 % (439169)Time elapsed: 15.194 s % 149.76/21.30 % (439169)Peak memory usage: 65 MB % 149.76/21.30 % (439169)Instructions burned: 29340 (million) % 149.76/21.30 % (439218)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1399232583:i=176048:add=on:rtra=on:rawr=on_2819 on theBenchmark for (2819ds/176048Mi) % 156.87/22.37 % (439196)Instruction limit reached! % 156.87/22.37 % (439196)------------------------------ % 156.87/22.37 % (439196)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 156.87/22.37 % (439196)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 156.87/22.37 % (439196)CaDiCaL version: 2.1.3 % 156.87/22.37 % (439196)Termination reason: Instruction limit % 156.87/22.37 % (439196)Termination phase: Saturation % 156.87/22.37 % (439196)Time elapsed: 5.743 s % 156.87/22.37 % (439196)Peak memory usage: 89 MB % 156.87/22.37 % (439196)Instructions burned: 17628 (million) % 156.87/22.37 % (439220)dis+10_1_sil=32000:si=on:sp=arity:random_seed=698195169:i=206:fgj=on:rtra=on_2812 on theBenchmark for (2812ds/206Mi) % 156.87/22.37 % (439220)Instruction limit reached! % 156.87/22.37 % (439220)------------------------------ % 156.87/22.37 % (439220)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 156.87/22.37 % (439220)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 156.87/22.38 % (439220)CaDiCaL version: 2.1.3 % 156.87/22.38 % (439220)Termination reason: Instruction limit % 156.87/22.38 % (439220)Termination phase: Saturation % 156.87/22.38 % (439220)Time elapsed: 0.070 s % 156.87/22.38 % (439220)Peak memory usage: 14 MB % 156.87/22.38 % (439220)Instructions burned: 207 (million) % 156.87/22.38 % (439222)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=2011660306:i=232:rtra=on_2811 on theBenchmark for (2811ds/232Mi) % 156.87/22.38 % (439222)Instruction limit reached! % 156.87/22.38 % (439222)------------------------------ % 156.87/22.38 % (439222)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 156.87/22.38 % (439222)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 156.87/22.38 % (439222)CaDiCaL version: 2.1.3 % 156.87/22.38 % (439222)Termination reason: Instruction limit % 156.87/22.38 % (439222)Termination phase: Saturation % 156.87/22.38 % (439222)Time elapsed: 0.077 s % 156.87/22.38 % (439222)Peak memory usage: 14 MB % 156.87/22.38 % (439222)Instructions burned: 232 (million) % 156.87/22.38 % (439224)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=3703923988:i=262:rtra=on_2810 on theBenchmark for (2810ds/262Mi) % 156.87/22.38 % (439224)Instruction limit reached! % 156.87/22.38 % (439224)------------------------------ % 156.87/22.38 % (439224)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 156.87/22.38 % (439224)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 156.87/22.38 % (439224)CaDiCaL version: 2.1.3 % 156.87/22.38 % (439224)Termination reason: Instruction limit % 156.87/22.38 % (439224)Termination phase: Saturation % 156.87/22.38 % (439224)Time elapsed: 0.086 s % 156.87/22.38 % (439224)Peak memory usage: 14 MB % 156.87/22.38 % (439224)Instructions burned: 264 (million) % 156.87/22.38 % (439226)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=277318982:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2809 on theBenchmark for (2809ds/318Mi) % 156.87/22.38 % (439226)Instruction limit reached! % 156.87/22.38 % (439226)------------------------------ % 156.87/22.38 % (439226)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 156.87/22.38 % (439226)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 156.87/22.38 % (439226)CaDiCaL version: 2.1.3 % 156.87/22.38 % (439226)Termination reason: Instruction limit % 156.87/22.38 % (439226)Termination phase: Saturation % 156.87/22.38 % (439226)Time elapsed: 0.114 s % 156.87/22.38 % (439226)Peak memory usage: 16 MB % 156.87/22.38 % (439226)Instructions burned: 319 (million) % 156.87/22.38 % (439228)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=2241997515:i=1428:nm=2:rtra=on_2808 on theBenchmark for (2808ds/1428Mi) % 156.87/22.38 % (439228)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 156.87/22.38 % (439228)Terminated due to inappropriate strategy. % 156.87/22.38 % (439228)------------------------------ % 156.87/22.38 % (439228)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 156.87/22.38 % (439228)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 156.87/22.38 % (439228)CaDiCaL version: 2.1.3 % 156.87/22.38 % (439228)Termination reason: Inappropriate % 156.87/22.38 % (439228)Time elapsed: 0.002 s % 156.87/22.38 % (439228)Peak memory usage: 10 MB % 156.87/22.38 % (439228)Instructions burned: 5 (million) % 156.87/22.38 % (439228)------------------------------ % 156.87/22.38 % (439228)------------------------------ % 190.43/27.13 % (439230)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=2342133569:i=262:bd=preordered:rtra=on:fsd=on_2807 on theBenchmark for (2807ds/262Mi) % 190.43/27.13 % (439230)Instruction limit reached! % 190.43/27.13 % (439230)------------------------------ % 190.43/27.13 % (439230)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 190.43/27.13 % (439230)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 190.43/27.13 % (439230)CaDiCaL version: 2.1.3 % 190.43/27.13 % (439230)Termination reason: Instruction limit % 190.43/27.13 % (439230)Termination phase: Saturation % 190.43/27.13 % (439230)Time elapsed: 0.164 s % 190.43/27.13 % (439230)Peak memory usage: 13 MB % 190.43/27.13 % (439230)Instructions burned: 262 (million) % 190.43/27.13 % (439232)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=1068999307:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2806 on theBenchmark for (2806ds/1368Mi) % 190.43/27.13 % (439232)Instruction limit reached! % 190.43/27.13 % (439232)------------------------------ % 190.43/27.13 % (439232)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 190.43/27.13 % (439232)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 190.43/27.13 % (439232)CaDiCaL version: 2.1.3 % 190.43/27.13 % (439232)Termination reason: Instruction limit % 190.43/27.13 % (439232)Termination phase: Saturation % 190.43/27.13 % (439232)Time elapsed: 0.442 s % 190.43/27.13 % (439232)Peak memory usage: 27 MB % 190.43/27.13 % (439232)Instructions burned: 1370 (million) % 190.43/27.13 % (439234)ott-21_1_sil=16000:si=on:fs=off:random_seed=766849844:i=360:av=off:fsr=off:rtra=on_2801 on theBenchmark for (2801ds/360Mi) % 190.43/27.13 % (439234)Instruction limit reached! % 190.43/27.13 % (439234)------------------------------ % 190.43/27.13 % (439234)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 190.43/27.13 % (439234)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 190.43/27.13 % (439234)CaDiCaL version: 2.1.3 % 190.43/27.13 % (439234)Termination reason: Instruction limit % 190.43/27.13 % (439234)Termination phase: Saturation % 190.43/27.13 % (439234)Time elapsed: 0.088 s % 190.43/27.13 % (439234)Peak memory usage: 13 MB % 190.43/27.13 % (439234)Instructions burned: 362 (million) % 190.43/27.13 % (439236)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3907407467:i=954:bd=all:rtra=on_2800 on theBenchmark for (2800ds/954Mi) % 190.43/27.13 % (439236)Instruction limit reached! % 190.43/27.13 % (439236)------------------------------ % 190.43/27.13 % (439236)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 190.43/27.13 % (439236)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 190.43/27.13 % (439236)CaDiCaL version: 2.1.3 % 190.43/27.13 % (439236)Termination reason: Instruction limit % 190.43/27.13 % (439236)Termination phase: Saturation % 190.43/27.13 % (439236)Time elapsed: 0.350 s % 190.43/27.13 % (439236)Peak memory usage: 17 MB % 190.43/27.13 % (439236)Instructions burned: 954 (million) % 190.43/27.13 % (439238)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=3833819952:fmbsr=1.3:i=1730:ins=25:rtra=on_2796 on theBenchmark for (2796ds/1730Mi) % 190.43/27.13 % (439238)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 190.43/27.13 % (439238)Terminated due to inappropriate strategy. % 190.43/27.13 % (439238)------------------------------ % 190.43/27.13 % (439238)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 190.43/27.13 % (439238)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 190.43/27.13 % (439238)CaDiCaL version: 2.1.3 % 190.43/27.13 % (439238)Termination reason: Inappropriate % 190.43/27.13 % (439238)Time elapsed: 0.001 s % 190.43/27.13 % (439238)Peak memory usage: 10 MB % 190.43/27.13 % (439238)Instructions burned: 4 (million) % 190.43/27.13 % (439238)------------------------------ % 190.43/27.13 % (439238)------------------------------ % 190.43/27.13 % (439240)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=1864355888:i=2358:rtra=on_2796 on theBenchmark for (2796ds/2358Mi) % 190.43/27.13 % (439240)Instruction limit reached! % 190.43/27.13 % (439240)------------------------------ % 190.43/27.13 % (439240)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 190.43/27.13 % (439240)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 190.43/27.13 % (439240)CaDiCaL version: 2.1.3 % 190.43/27.13 % (439240)Termination reason: Instruction limit % 190.43/27.13 % (439240)Termination phase: Saturation % 242.04/34.33 % (439240)Time elapsed: 0.767 s % 242.04/34.33 % (439240)Peak memory usage: 27 MB % 242.04/34.33 % (439240)Instructions burned: 2362 (million) % 242.04/34.33 % (439242)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=2758225154:i=1778:ins=1:rtra=on_2789 on theBenchmark for (2789ds/1778Mi) % 242.04/34.33 % (439242)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 242.04/34.33 % (439242)Terminated due to inappropriate strategy. % 242.04/34.33 % (439242)------------------------------ % 242.04/34.33 % (439242)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 242.04/34.33 % (439242)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 242.04/34.33 % (439242)CaDiCaL version: 2.1.3 % 242.04/34.33 % (439242)Termination reason: Inappropriate % 242.04/34.33 % (439242)Time elapsed: 0.001 s % 242.04/34.33 % (439242)Peak memory usage: 10 MB % 242.04/34.33 % (439242)Instructions burned: 5 (million) % 242.04/34.33 % (439242)------------------------------ % 242.04/34.33 % (439242)------------------------------ % 242.04/34.33 % (439244)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=1626809626:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2788 on theBenchmark for (2788ds/1384Mi) % 242.04/34.33 % (439244)Instruction limit reached! % 242.04/34.33 % (439244)------------------------------ % 242.04/34.33 % (439244)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 242.04/34.33 % (439244)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 242.04/34.33 % (439244)CaDiCaL version: 2.1.3 % 242.04/34.33 % (439244)Termination reason: Instruction limit % 242.04/34.33 % (439244)Termination phase: Saturation % 242.04/34.33 % (439244)Time elapsed: 0.473 s % 242.04/34.33 % (439244)Peak memory usage: 25 MB % 242.04/34.33 % (439244)Instructions burned: 1385 (million) % 242.04/34.33 % (439246)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=1853705579:i=1758:kws=inv_precedence:fsr=off:rtra=on_2784 on theBenchmark for (2784ds/1758Mi) % 242.04/34.33 % (439246)Instruction limit reached! % 242.04/34.33 % (439246)------------------------------ % 242.04/34.33 % (439246)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 242.04/34.33 % (439246)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 242.04/34.33 % (439246)CaDiCaL version: 2.1.3 % 242.04/34.33 % (439246)Termination reason: Instruction limit % 242.04/34.33 % (439246)Termination phase: Saturation % 242.04/34.33 % (439246)Time elapsed: 0.523 s % 242.04/34.33 % (439246)Peak memory usage: 25 MB % 242.04/34.33 % (439246)Instructions burned: 1761 (million) % 242.04/34.33 % (439248)fmb+10_1_sil=64000:si=on:random_seed=3593798296:i=44122:nm=2:rtra=on:gsp=on_2778 on theBenchmark for (2778ds/44122Mi) % 242.04/34.33 % (439248)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 242.04/34.33 % (439248)Terminated due to inappropriate strategy. % 242.04/34.33 % (439248)------------------------------ % 242.04/34.33 % (439248)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 242.04/34.33 % (439248)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 242.04/34.33 % (439248)CaDiCaL version: 2.1.3 % 242.04/34.33 % (439248)Termination reason: Inappropriate % 242.04/34.33 % (439248)Time elapsed: 0.002 s % 242.04/34.33 % (439248)Peak memory usage: 10 MB % 242.04/34.33 % (439248)Instructions burned: 6 (million) % 242.04/34.33 % (439248)------------------------------ % 242.04/34.33 % (439248)------------------------------ % 242.04/34.33 % (439250)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=3665014640:i=19030:nm=5:rtra=on_2778 on theBenchmark for (2778ds/19030Mi) % 242.04/34.33 % (439250)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 242.04/34.33 % (439250)Terminated due to inappropriate strategy. % 242.04/34.33 % (439250)------------------------------ % 242.04/34.33 % (439250)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 242.04/34.33 % (439250)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 242.04/34.33 % (439250)CaDiCaL version: 2.1.3 % 242.04/34.33 % (439250)Termination reason: Inappropriate % 242.04/34.33 % (439250)Time elapsed: 0.001 s % 242.04/34.33 % (439250)Peak memory usage: 10 MB % 242.04/34.33 % (439250)Instructions burned: 5 (million) % 242.04/34.33 % (439250)------------------------------ % 242.04/34.33 % (439250)------------------------------ % 242.04/34.33 % (439252)fmb+10_1_sil=64000:sas=cadical:si=on:fmbss=8:random_seed=2059861459:fmbsr=1.7:i=1840:rtra=on_2778 on theBenchmark for (2778ds/1840Mi) % 259.76/36.80 % (439252)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 259.76/36.80 % (439252)Terminated due to inappropriate strategy. % 259.76/36.80 % (439252)------------------------------ % 259.76/36.80 % (439252)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 259.76/36.80 % (439252)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 259.76/36.80 % (439252)CaDiCaL version: 2.1.3 % 259.76/36.80 % (439252)Termination reason: Inappropriate % 259.76/36.80 % (439252)Time elapsed: 0.001 s % 259.76/36.80 % (439252)Peak memory usage: 10 MB % 259.76/36.80 % (439252)Instructions burned: 5 (million) % 259.76/36.80 % (439252)------------------------------ % 259.76/36.80 % (439252)------------------------------ % 259.76/36.80 % (439254)dis-4_1_sil=16000:drc=ordering:si=on:sp=const_frequency:sac=on:newcnf=on:random_seed=3058525294:i=10262:rtra=on_2778 on theBenchmark for (2778ds/10262Mi) % 259.76/36.80 % (439254)Instruction limit reached! % 259.76/36.80 % (439254)------------------------------ % 259.76/36.80 % (439254)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 259.76/36.80 % (439254)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 259.76/36.80 % (439254)CaDiCaL version: 2.1.3 % 259.76/36.80 % (439254)Termination reason: Instruction limit % 259.76/36.80 % (439254)Termination phase: Saturation % 259.76/36.80 % (439254)Time elapsed: 3.137 s % 259.76/36.80 % (439254)Peak memory usage: 67 MB % 259.76/36.80 % (439254)Instructions burned: 10263 (million) % 259.76/36.80 % (439256)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:si=on:sp=arity:spb=units:lsd=10:nwc=3:random_seed=588665549:i=2944:ins=7:rtra=on:fdi=8:gsp=on_2746 on theBenchmark for (2746ds/2944Mi) % 259.76/36.80 % (439256)Instruction limit reached! % 259.76/36.80 % (439256)------------------------------ % 259.76/36.80 % (439256)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 259.76/36.80 % (439256)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 259.76/36.80 % (439256)CaDiCaL version: 2.1.3 % 259.76/36.80 % (439256)Termination reason: Instruction limit % 259.76/36.80 % (439256)Termination phase: Saturation % 259.76/36.80 % (439256)Time elapsed: 0.953 s % 259.76/36.80 % (439256)Peak memory usage: 34 MB % 259.76/36.80 % (439256)Instructions burned: 2945 (million) % 259.76/36.80 % (439258)fmb+10_1_sil=16000:sas=cadical:si=on:bce=on:fmbss=77:random_seed=3475376366:i=12648:rtra=on_2737 on theBenchmark for (2737ds/12648Mi) % 259.76/36.80 % (439258)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 259.76/36.80 % (439258)Terminated due to inappropriate strategy. % 259.76/36.80 % (439258)------------------------------ % 259.76/36.80 % (439258)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 259.76/36.80 % (439258)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 259.76/36.80 % (439258)CaDiCaL version: 2.1.3 % 259.76/36.80 % (439258)Termination reason: Inappropriate % 259.76/36.80 % (439258)Time elapsed: 0.002 s % 259.76/36.80 % (439258)Peak memory usage: 11 MB % 259.76/36.80 % (439258)Instructions burned: 7 (million) % 259.76/36.80 % (439258)------------------------------ % 259.76/36.80 % (439258)------------------------------ % 259.76/36.80 % (439260)fmb+10_1_fmbas=function:sil=32000:sas=cadical:si=on:fmbss=16:random_seed=2650691869:fmbsr=2.30978:i=4348:rtra=on_2736 on theBenchmark for (2736ds/4348Mi) % 259.76/36.80 % (439260)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 259.76/36.80 % (439260)Terminated due to inappropriate strategy. % 259.76/36.80 % (439260)------------------------------ % 259.76/36.80 % (439260)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 259.76/36.80 % (439260)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 259.76/36.80 % (439260)CaDiCaL version: 2.1.3 % 259.76/36.80 % (439260)Termination reason: Inappropriate % 259.76/36.80 % (439260)Time elapsed: 0.002 s % 259.76/36.80 % (439260)Peak memory usage: 10 MB % 259.76/36.80 % (439260)Instructions burned: 5 (million) % 259.76/36.80 % (439260)------------------------------ % 259.76/36.80 % (439260)------------------------------ % 259.76/36.80 % (439262)ott-2_1_sil=16000:si=on:newcnf=on:random_seed=1340110388:avsq=on:i=1738:avsqr=1,16:kws=inv_arity_squared:rtra=on_2736 on theBenchmark for (2736ds/1738Mi) % 259.76/36.80 % (439262)Instruction limit reached! % 259.76/36.80 % (439262)------------------------------ % 259.76/36.80 % (439262)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 259.76/36.80 % (439262)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa72Terminated % 300.22/42.54 % Vampire exiting %------------------------------------------------------------------------------