%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWC471_1 : TPTP v9.3.1. Bugfixed v9.1.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % Computer : n005.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:06:02 PM UTC 2026 % Result : Timeout 300.07s 42.54s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWC471_1 : TPTP v9.3.1. Bugfixed v9.1.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.08/0.18 % Computer : n005.cluster.edu % 0.08/0.18 % Model : x86_64 x86_64 % 0.08/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.08/0.18 % Memory : 8046.5625MB % 0.08/0.18 % OS : Linux 6.8.0-71-generic % 0.08/0.18 % CPULimit : 300 % 0.08/0.18 % WCLimit : 300 % 0.08/0.18 % DateTime : Mon Sep 28 09:40:02 UTC 2026 % 0.08/0.19 % CPUTime : % 0.08/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.08/0.22 Running first-order model finding % 0.08/0.22 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.89/0.83 % (670716)Will run a generic schedule for satisfiability detection. % 3.89/0.83 % (670726)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2399145062:i=131_2999 on theBenchmark for (2999ds/131Mi) % 3.89/0.83 % (670722)% WARNING: option uhcvi not known. % 3.89/0.83 % (670721)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1779497046_2999 on theBenchmark for (2999ds/0Mi) % 3.89/0.83 % (670722)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1233217274:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 3.89/0.83 % (670723)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2589797298:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 3.89/0.83 % (670724)dis+10_1_sil=32000:sp=arity:random_seed=4034869912:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 3.89/0.83 % (670725)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3501214701:i=116_2999 on theBenchmark for (2999ds/116Mi) % 3.89/0.83 % (670727)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2223091678:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 3.89/0.83 % (670721)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.89/0.83 % (670721)Terminated due to inappropriate strategy. % 3.89/0.83 % (670721)------------------------------ % 3.89/0.83 % (670721)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.89/0.83 % (670721)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.89/0.83 % (670721)CaDiCaL version: 2.1.3 % 3.89/0.83 % (670721)Termination reason: Inappropriate % 3.89/0.83 % (670721)Time elapsed: 0.001 s % 3.89/0.83 % (670721)Peak memory usage: 10 MB % 3.89/0.83 % (670721)Instructions burned: 1 (million) % 3.89/0.83 % (670721)------------------------------ % 3.89/0.83 % (670721)------------------------------ % 3.89/0.83 % (670735)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1086654942:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 3.89/0.83 % (670735)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.89/0.83 % (670735)Terminated due to inappropriate strategy. % 3.89/0.83 % (670735)------------------------------ % 3.89/0.83 % (670735)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.89/0.83 % (670735)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.89/0.83 % (670735)CaDiCaL version: 2.1.3 % 3.89/0.83 % (670735)Termination reason: Inappropriate % 3.89/0.83 % (670735)Time elapsed: 0.001 s % 3.89/0.83 % (670735)Peak memory usage: 10 MB % 3.89/0.83 % (670735)Instructions burned: 1 (million) % 3.89/0.83 % (670735)------------------------------ % 3.89/0.83 % (670735)------------------------------ % 3.89/0.83 % (670726)Instruction limit reached! % 3.89/0.83 % (670726)------------------------------ % 3.89/0.83 % (670726)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.89/0.83 % (670726)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.89/0.83 % (670726)CaDiCaL version: 2.1.3 % 3.89/0.83 % (670726)Termination reason: Instruction limit % 3.89/0.83 % (670726)Termination phase: Saturation % 3.89/0.83 % (670726)Time elapsed: 0.044 s % 3.89/0.83 % (670726)Peak memory usage: 13 MB % 3.89/0.83 % (670726)Instructions burned: 133 (million) % 3.89/0.83 % (670737)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1279771085:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 3.89/0.83 % (670738)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=734373417:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi) % 3.89/0.83 % (670724)Instruction limit reached! % 3.89/0.83 % (670724)------------------------------ % 3.89/0.83 % (670724)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.89/0.83 % (670724)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.89/0.83 % (670724)CaDiCaL version: 2.1.3 % 3.89/0.83 % (670724)Termination reason: Instruction limit % 3.89/0.83 % (670724)Termination phase: Saturation % 3.89/0.83 % (670724)Time elapsed: 0.063 s % 3.89/0.83 % (670724)Peak memory usage: 12 MB % 3.89/0.83 % (670724)Instructions burned: 104 (million) % 3.89/0.83 % (670725)Instruction limit reached! % 3.89/0.83 % (670725)------------------------------ % 3.89/0.83 % (670725)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.43/1.39 % (670725)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.43/1.39 % (670725)CaDiCaL version: 2.1.3 % 7.43/1.39 % (670725)Termination reason: Instruction limit % 7.43/1.39 % (670725)Termination phase: Saturation % 7.43/1.39 % (670725)Time elapsed: 0.073 s % 7.43/1.39 % (670725)Peak memory usage: 12 MB % 7.43/1.39 % (670725)Instructions burned: 121 (million) % 7.43/1.39 % (670741)ott-21_1_sil=16000:fs=off:random_seed=988306900:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi) % 7.43/1.39 % (670742)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=4012124037:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 7.43/1.39 % (670727)Instruction limit reached! % 7.43/1.39 % (670727)------------------------------ % 7.43/1.39 % (670727)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.43/1.39 % (670727)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.43/1.39 % (670727)CaDiCaL version: 2.1.3 % 7.43/1.39 % (670727)Termination reason: Instruction limit % 7.43/1.39 % (670727)Termination phase: Saturation % 7.43/1.39 % (670727)Time elapsed: 0.108 s % 7.43/1.39 % (670727)Peak memory usage: 13 MB % 7.43/1.39 % (670727)Instructions burned: 160 (million) % 7.43/1.39 % (670745)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3653807523:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 7.43/1.39 % (670737)Instruction limit reached! % 7.43/1.39 % (670737)------------------------------ % 7.43/1.39 % (670737)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.43/1.39 % (670737)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.43/1.39 % (670737)CaDiCaL version: 2.1.3 % 7.43/1.39 % (670737)Termination reason: Instruction limit % 7.43/1.39 % (670737)Termination phase: Saturation % 7.43/1.39 % (670737)Time elapsed: 0.087 s % 7.43/1.39 % (670737)Peak memory usage: 12 MB % 7.43/1.39 % (670737)Instructions burned: 132 (million) % 7.43/1.39 % (670745)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 7.43/1.39 % (670745)Terminated due to inappropriate strategy. % 7.43/1.39 % (670745)------------------------------ % 7.43/1.39 % (670745)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.43/1.39 % (670745)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.43/1.39 % (670745)CaDiCaL version: 2.1.3 % 7.43/1.39 % (670745)Termination reason: Inappropriate % 7.43/1.39 % (670745)Time elapsed: 0.001 s % 7.43/1.39 % (670745)Peak memory usage: 10 MB % 7.43/1.39 % (670745)Instructions burned: 1 (million) % 7.43/1.39 % (670745)------------------------------ % 7.43/1.39 % (670745)------------------------------ % 7.43/1.39 % (670747)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1574687045:i=1179_2998 on theBenchmark for (2998ds/1179Mi) % 7.43/1.39 % (670748)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=394629454:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi) % 7.43/1.39 % (670748)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 7.43/1.39 % (670748)Terminated due to inappropriate strategy. % 7.43/1.39 % (670748)------------------------------ % 7.43/1.39 % (670748)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.43/1.39 % (670748)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.43/1.39 % (670748)CaDiCaL version: 2.1.3 % 7.43/1.39 % (670748)Termination reason: Inappropriate % 7.43/1.39 % (670748)Time elapsed: 0.001 s % 7.43/1.39 % (670748)Peak memory usage: 10 MB % 7.43/1.39 % (670748)Instructions burned: 1 (million) % 7.43/1.39 % (670748)------------------------------ % 7.43/1.39 % (670748)------------------------------ % 7.43/1.39 % (670741)Instruction limit reached! % 7.43/1.39 % (670741)------------------------------ % 7.43/1.39 % (670741)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.43/1.39 % (670741)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.43/1.39 % (670741)CaDiCaL version: 2.1.3 % 7.43/1.39 % (670741)Termination reason: Instruction limit % 7.43/1.39 % (670741)Termination phase: Saturation % 7.43/1.39 % (670741)Time elapsed: 0.080 s % 7.43/1.39 % (670741)Peak memory usage: 12 MB % 7.43/1.39 % (670741)Instructions burned: 180 (million) % 7.43/1.39 % (670751)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=3172308424: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) % 21.79/3.31 % (670752)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=303835335:i=879:kws=inv_precedence:fsr=off_2998 on theBenchmark for (2998ds/879Mi) % 21.79/3.31 % (670738)Instruction limit reached! % 21.79/3.31 % (670738)------------------------------ % 21.79/3.31 % (670738)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 21.79/3.31 % (670738)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.79/3.31 % (670738)CaDiCaL version: 2.1.3 % 21.79/3.31 % (670738)Termination reason: Instruction limit % 21.79/3.31 % (670738)Termination phase: Saturation % 21.79/3.31 % (670738)Time elapsed: 0.189 s % 21.79/3.31 % (670738)Peak memory usage: 17 MB % 21.79/3.31 % (670738)Instructions burned: 685 (million) % 21.79/3.31 % (670755)fmb+10_1_sil=64000:random_seed=4277313877:i=22061:nm=2:gsp=on_2997 on theBenchmark for (2997ds/22061Mi) % 21.79/3.31 % (670755)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 21.79/3.31 % (670755)Terminated due to inappropriate strategy. % 21.79/3.31 % (670755)------------------------------ % 21.79/3.31 % (670755)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 21.79/3.31 % (670755)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.79/3.31 % (670755)CaDiCaL version: 2.1.3 % 21.79/3.31 % (670755)Termination reason: Inappropriate % 21.79/3.31 % (670755)Time elapsed: 0.0000 s % 21.79/3.31 % (670755)Peak memory usage: 10 MB % 21.79/3.31 % (670755)Instructions burned: 1 (million) % 21.79/3.31 % (670755)------------------------------ % 21.79/3.31 % (670755)------------------------------ % 21.79/3.31 % (670757)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3918134858:i=9515:nm=5_2997 on theBenchmark for (2997ds/9515Mi) % 21.79/3.31 % (670757)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 21.79/3.31 % (670757)Terminated due to inappropriate strategy. % 21.79/3.31 % (670757)------------------------------ % 21.79/3.31 % (670757)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 21.79/3.31 % (670757)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.79/3.31 % (670757)CaDiCaL version: 2.1.3 % 21.79/3.31 % (670757)Termination reason: Inappropriate % 21.79/3.31 % (670757)Time elapsed: 0.0000 s % 21.79/3.31 % (670757)Peak memory usage: 10 MB % 21.79/3.31 % (670757)Instructions burned: 1 (million) % 21.79/3.31 % (670757)------------------------------ % 21.79/3.31 % (670757)------------------------------ % 21.79/3.31 % (670759)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=933448376:fmbsr=1.7:i=920_2997 on theBenchmark for (2997ds/920Mi) % 21.79/3.31 % (670759)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 21.79/3.31 % (670759)Terminated due to inappropriate strategy. % 21.79/3.31 % (670759)------------------------------ % 21.79/3.31 % (670759)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 21.79/3.31 % (670759)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.79/3.31 % (670759)CaDiCaL version: 2.1.3 % 21.79/3.31 % (670759)Termination reason: Inappropriate % 21.79/3.31 % (670759)Time elapsed: 0.0000 s % 21.79/3.31 % (670759)Peak memory usage: 10 MB % 21.79/3.31 % (670759)Instructions burned: 1 (million) % 21.79/3.31 % (670759)------------------------------ % 21.79/3.31 % (670759)------------------------------ % 21.79/3.31 % (670761)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=306628642:i=5131_2996 on theBenchmark for (2996ds/5131Mi) % 21.79/3.31 % (670742)Instruction limit reached! % 21.79/3.31 % (670742)------------------------------ % 21.79/3.31 % (670742)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 21.79/3.31 % (670742)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.79/3.31 % (670742)CaDiCaL version: 2.1.3 % 21.79/3.31 % (670742)Termination reason: Instruction limit % 21.79/3.31 % (670742)Termination phase: Saturation % 21.79/3.31 % (670742)Time elapsed: 0.287 s % 21.79/3.31 % (670742)Peak memory usage: 14 MB % 21.79/3.31 % (670742)Instructions burned: 478 (million) % 21.79/3.31 % (670763)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3144082387:i=1472:ins=7:fdi=8:gsp=on_2995 on theBenchmark for (2995ds/1472Mi) % 21.79/3.31 % (670751)Instruction limit reached! % 21.79/3.31 % (670751)------------------------------ % 21.79/3.31 % (670751)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 21.79/3.31 % (670751)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.02/4.13 % (670751)CaDiCaL version: 2.1.3 % 27.02/4.13 % (670751)Termination reason: Instruction limit % 27.02/4.13 % (670751)Termination phase: Saturation % 27.02/4.13 % (670751)Time elapsed: 0.399 s % 27.02/4.13 % (670751)Peak memory usage: 19 MB % 27.02/4.13 % (670751)Instructions burned: 692 (million) % 27.02/4.13 % (670765)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=1774324493:i=6324_2993 on theBenchmark for (2993ds/6324Mi) % 27.02/4.13 % (670765)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 27.02/4.13 % (670765)Terminated due to inappropriate strategy. % 27.02/4.13 % (670765)------------------------------ % 27.02/4.13 % (670765)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 27.02/4.13 % (670765)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.02/4.13 % (670765)CaDiCaL version: 2.1.3 % 27.02/4.13 % (670765)Termination reason: Inappropriate % 27.02/4.13 % (670765)Time elapsed: 0.001 s % 27.02/4.13 % (670765)Peak memory usage: 10 MB % 27.02/4.13 % (670765)Instructions burned: 1 (million) % 27.02/4.13 % (670765)------------------------------ % 27.02/4.13 % (670765)------------------------------ % 27.02/4.13 % (670767)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=2709339466:fmbsr=2.30978:i=2174_2993 on theBenchmark for (2993ds/2174Mi) % 27.02/4.13 % (670767)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 27.02/4.13 % (670767)Terminated due to inappropriate strategy. % 27.02/4.13 % (670767)------------------------------ % 27.02/4.13 % (670767)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 27.02/4.13 % (670767)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.02/4.13 % (670767)CaDiCaL version: 2.1.3 % 27.02/4.13 % (670767)Termination reason: Inappropriate % 27.02/4.13 % (670767)Time elapsed: 0.001 s % 27.02/4.13 % (670767)Peak memory usage: 10 MB % 27.02/4.13 % (670767)Instructions burned: 1 (million) % 27.02/4.13 % (670767)------------------------------ % 27.02/4.13 % (670767)------------------------------ % 27.02/4.13 % (670769)ott-2_1_sil=16000:newcnf=on:random_seed=2736328348:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2993 on theBenchmark for (2993ds/869Mi) % 27.02/4.13 % (670752)Instruction limit reached! % 27.02/4.13 % (670752)------------------------------ % 27.02/4.13 % (670752)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 27.02/4.13 % (670752)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.02/4.13 % (670752)CaDiCaL version: 2.1.3 % 27.02/4.13 % (670752)Termination reason: Instruction limit % 27.02/4.13 % (670752)Termination phase: Saturation % 27.02/4.13 % (670752)Time elapsed: 0.488 s % 27.02/4.13 % (670752)Peak memory usage: 19 MB % 27.02/4.13 % (670752)Instructions burned: 880 (million) % 27.02/4.13 % (670771)ott+10_1_sil=32000:tgt=ground:random_seed=2169901813:i=5114:av=off_2992 on theBenchmark for (2992ds/5114Mi) % 27.02/4.13 % (670747)Instruction limit reached! % 27.02/4.13 % (670747)------------------------------ % 27.02/4.13 % (670747)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 27.02/4.13 % (670747)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.02/4.13 % (670747)CaDiCaL version: 2.1.3 % 27.02/4.13 % (670747)Termination reason: Instruction limit % 27.02/4.13 % (670747)Termination phase: Saturation % 27.02/4.13 % (670747)Time elapsed: 0.693 s % 27.02/4.13 % (670747)Peak memory usage: 20 MB % 27.02/4.13 % (670747)Instructions burned: 1181 (million) % 27.02/4.13 % (670773)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2380299326:i=54282_2991 on theBenchmark for (2991ds/54282Mi) % 27.02/4.13 % (670773)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 27.02/4.13 % (670773)Terminated due to inappropriate strategy. % 27.02/4.13 % (670773)------------------------------ % 27.02/4.13 % (670773)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 27.02/4.13 % (670773)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.02/4.13 % (670773)CaDiCaL version: 2.1.3 % 27.02/4.13 % (670773)Termination reason: Inappropriate % 27.02/4.13 % (670773)Time elapsed: 0.001 s % 27.02/4.13 % (670773)Peak memory usage: 10 MB % 27.02/4.13 % (670773)Instructions burned: 1 (million) % 27.02/4.13 % (670773)------------------------------ % 27.02/4.13 % (670773)------------------------------ % 27.02/4.13 % (670775)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=450963091:i=3512:aac=none_2991 on theBenchmark for (2991ds/3512Mi) % 27.02/4.13 % (670769)Instruction limit reached! % 84.97/12.28 % (670769)------------------------------ % 84.97/12.28 % (670769)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 84.97/12.28 % (670769)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 84.97/12.28 % (670769)CaDiCaL version: 2.1.3 % 84.97/12.28 % (670769)Termination reason: Instruction limit % 84.97/12.28 % (670769)Termination phase: Saturation % 84.97/12.28 % (670769)Time elapsed: 0.503 s % 84.97/12.28 % (670769)Peak memory usage: 15 MB % 84.97/12.28 % (670769)Instructions burned: 870 (million) % 84.97/12.28 % (670777)dis+21_1_sil=32000:sas=cadical:random_seed=806170425:i=3773:amm=off_2988 on theBenchmark for (2988ds/3773Mi) % 84.97/12.28 % (670763)Instruction limit reached! % 84.97/12.28 % (670763)------------------------------ % 84.97/12.28 % (670763)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 84.97/12.28 % (670763)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 84.97/12.28 % (670763)CaDiCaL version: 2.1.3 % 84.97/12.28 % (670763)Termination reason: Instruction limit % 84.97/12.28 % (670763)Termination phase: Saturation % 84.97/12.28 % (670763)Time elapsed: 0.846 s % 84.97/12.28 % (670763)Peak memory usage: 29 MB % 84.97/12.28 % (670763)Instructions burned: 1472 (million) % 84.97/12.28 % (670779)ott+11_1_sil=16000:gs=on:random_seed=1150553008:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2987 on theBenchmark for (2987ds/2251Mi) % 84.97/12.28 % (670761)Instruction limit reached! % 84.97/12.28 % (670761)------------------------------ % 84.97/12.28 % (670761)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 84.97/12.28 % (670761)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 84.97/12.28 % (670761)CaDiCaL version: 2.1.3 % 84.97/12.28 % (670761)Termination reason: Instruction limit % 84.97/12.28 % (670761)Termination phase: Saturation % 84.97/12.28 % (670761)Time elapsed: 1.479 s % 84.97/12.28 % (670761)Peak memory usage: 41 MB % 84.97/12.28 % (670761)Instructions burned: 5134 (million) % 84.97/12.28 % (670781)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=3755556038:fmbsr=1.6:i=67534_2982 on theBenchmark for (2982ds/67534Mi) % 84.97/12.28 % (670781)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 84.97/12.28 % (670781)Terminated due to inappropriate strategy. % 84.97/12.28 % (670781)------------------------------ % 84.97/12.28 % (670781)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 84.97/12.28 % (670781)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 84.97/12.28 % (670781)CaDiCaL version: 2.1.3 % 84.97/12.28 % (670781)Termination reason: Inappropriate % 84.97/12.28 % (670781)Time elapsed: 0.0000 s % 84.97/12.28 % (670781)Peak memory usage: 11 MB % 84.97/12.28 % (670781)Instructions burned: 1 (million) % 84.97/12.28 % (670781)------------------------------ % 84.97/12.28 % (670781)------------------------------ % 84.97/12.28 % (670783)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=4028333196:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2981 on theBenchmark for (2981ds/4591Mi) % 84.97/12.28 % (670779)Instruction limit reached! % 84.97/12.28 % (670779)------------------------------ % 84.97/12.28 % (670779)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 84.97/12.28 % (670779)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 84.97/12.28 % (670779)CaDiCaL version: 2.1.3 % 84.97/12.28 % (670779)Termination reason: Instruction limit % 84.97/12.28 % (670779)Termination phase: Saturation % 84.97/12.28 % (670779)Time elapsed: 1.220 s % 84.97/12.28 % (670779)Peak memory usage: 24 MB % 84.97/12.28 % (670779)Instructions burned: 2251 (million) % 84.97/12.28 % (670785)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=618890764:i=29340_2974 on theBenchmark for (2974ds/29340Mi) % 84.97/12.28 % (670775)Instruction limit reached! % 84.97/12.28 % (670775)------------------------------ % 84.97/12.28 % (670775)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 84.97/12.28 % (670775)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 84.97/12.28 % (670775)CaDiCaL version: 2.1.3 % 84.97/12.28 % (670775)Termination reason: Instruction limit % 84.97/12.28 % (670775)Termination phase: Saturation % 84.97/12.28 % (670775)Time elapsed: 1.851 s % 84.97/12.28 % (670775)Peak memory usage: 35 MB % 84.97/12.28 % (670775)Instructions burned: 3512 (million) % 84.97/12.28 % (670787)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=2995377047:i=5211_2972 on theBenchmark for (2972ds/5211Mi) % 84.97/12.28 % (670783)Instruction limit reached! % 116.92/16.70 % (670783)------------------------------ % 116.92/16.70 % (670783)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 116.92/16.70 % (670783)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 116.92/16.70 % (670783)CaDiCaL version: 2.1.3 % 116.92/16.70 % (670783)Termination reason: Instruction limit % 116.92/16.70 % (670783)Termination phase: Saturation % 116.92/16.70 % (670783)Time elapsed: 1.264 s % 116.92/16.70 % (670783)Peak memory usage: 52 MB % 116.92/16.70 % (670783)Instructions burned: 4595 (million) % 116.92/16.70 % (670789)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=1400376908:i=5497:nm=2_2969 on theBenchmark for (2969ds/5497Mi) % 116.92/16.70 % (670789)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 116.92/16.70 % (670789)Terminated due to inappropriate strategy. % 116.92/16.70 % (670789)------------------------------ % 116.92/16.70 % (670789)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 116.92/16.70 % (670789)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 116.92/16.70 % (670789)CaDiCaL version: 2.1.3 % 116.92/16.70 % (670789)Termination reason: Inappropriate % 116.92/16.70 % (670789)Time elapsed: 0.0000 s % 116.92/16.70 % (670789)Peak memory usage: 10 MB % 116.92/16.70 % (670789)Instructions burned: 1 (million) % 116.92/16.70 % (670789)------------------------------ % 116.92/16.70 % (670789)------------------------------ % 116.92/16.70 % (670791)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=3992502874:fmbsr=2:i=46332_2969 on theBenchmark for (2969ds/46332Mi) % 116.92/16.70 % (670791)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 116.92/16.70 % (670791)Terminated due to inappropriate strategy. % 116.92/16.70 % (670791)------------------------------ % 116.92/16.70 % (670791)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 116.92/16.70 % (670791)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 116.92/16.70 % (670791)CaDiCaL version: 2.1.3 % 116.92/16.70 % (670791)Termination reason: Inappropriate % 116.92/16.70 % (670791)Time elapsed: 0.0000 s % 116.92/16.70 % (670791)Peak memory usage: 10 MB % 116.92/16.70 % (670791)Instructions burned: 1 (million) % 116.92/16.70 % (670791)------------------------------ % 116.92/16.70 % (670791)------------------------------ % 116.92/16.70 % (670793)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=1044287613:i=14071_2968 on theBenchmark for (2968ds/14071Mi) % 116.92/16.70 % (670793)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 116.92/16.70 % (670793)Terminated due to inappropriate strategy. % 116.92/16.70 % (670793)------------------------------ % 116.92/16.70 % (670793)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 116.92/16.70 % (670793)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 116.92/16.70 % (670793)CaDiCaL version: 2.1.3 % 116.92/16.70 % (670793)Termination reason: Inappropriate % 116.92/16.70 % (670793)Time elapsed: 0.0000 s % 116.92/16.70 % (670793)Peak memory usage: 10 MB % 116.92/16.70 % (670793)Instructions burned: 1 (million) % 116.92/16.70 % (670793)------------------------------ % 116.92/16.70 % (670793)------------------------------ % 116.92/16.70 % (670795)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2005485004:i=22565:add=on:rawr=on_2968 on theBenchmark for (2968ds/22565Mi) % 116.92/16.70 % (670777)Instruction limit reached! % 116.92/16.70 % (670777)------------------------------ % 116.92/16.70 % (670777)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 116.92/16.70 % (670777)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 116.92/16.70 % (670777)CaDiCaL version: 2.1.3 % 116.92/16.70 % (670777)Termination reason: Instruction limit % 116.92/16.70 % (670777)Termination phase: Saturation % 116.92/16.70 % (670777)Time elapsed: 2.017 s % 116.92/16.70 % (670777)Peak memory usage: 31 MB % 116.92/16.70 % (670777)Instructions burned: 3773 (million) % 116.92/16.70 % (670797)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=1939395542:i=8173:av=off_2967 on theBenchmark for (2967ds/8173Mi) % 116.92/16.70 % (670771)Instruction limit reached! % 116.92/16.70 % (670771)------------------------------ % 116.92/16.70 % (670771)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 116.92/16.70 % (670771)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 116.92/16.70 % (670771)CaDiCaL version: 2.1.3 % 116.92/16.70 % (670771)Termination reason: Instruction limit % 116.92/16.70 % (670771)Termination phase: Saturation % 116.92/16.76 % (670771)Time elapsed: 3.180 s % 116.92/16.76 % (670771)Peak memory usage: 42 MB % 116.92/16.76 % (670771)Instructions burned: 5115 (million) % 116.92/16.76 % (670799)dis+10_16:1_sil=16000:random_seed=5564908:i=9155:fsr=off_2960 on theBenchmark for (2960ds/9155Mi) % 116.92/16.76 % (670787)Instruction limit reached! % 116.92/16.76 % (670787)------------------------------ % 116.92/16.76 % (670787)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 116.92/16.76 % (670787)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 116.92/16.76 % (670787)CaDiCaL version: 2.1.3 % 116.92/16.76 % (670787)Termination reason: Instruction limit % 116.92/16.76 % (670787)Termination phase: Saturation % 116.92/16.76 % (670787)Time elapsed: 2.744 s % 116.92/16.76 % (670787)Peak memory usage: 50 MB % 116.92/16.76 % (670787)Instructions burned: 5212 (million) % 116.92/16.76 % (670801)ott-3_8_sil=64000:random_seed=2913982609:i=20139:bs=on_2944 on theBenchmark for (2944ds/20139Mi) % 116.92/16.76 % (670795)Instruction limit reached! % 116.92/16.76 % (670795)------------------------------ % 116.92/16.76 % (670795)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 116.92/16.76 % (670795)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 116.92/16.76 % (670795)CaDiCaL version: 2.1.3 % 116.92/16.76 % (670795)Termination reason: Instruction limit % 116.92/16.76 % (670795)Termination phase: Saturation % 116.92/16.76 % (670795)Time elapsed: 5.034 s % 116.92/16.76 % (670795)Peak memory usage: 51 MB % 116.92/16.76 % (670795)Instructions burned: 22566 (million) % 116.92/16.76 % (670804)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=3098081699:fmbsr=2:i=32576_2918 on theBenchmark for (2918ds/32576Mi) % 116.92/16.76 % (670804)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 116.92/16.76 % (670804)Terminated due to inappropriate strategy. % 116.92/16.76 % (670804)------------------------------ % 116.92/16.76 % (670804)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 116.92/16.76 % (670804)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 116.92/16.76 % (670804)CaDiCaL version: 2.1.3 % 116.92/16.76 % (670804)Termination reason: Inappropriate % 116.92/16.76 % (670804)Time elapsed: 0.0000 s % 116.92/16.76 % (670804)Peak memory usage: 10 MB % 116.92/16.76 % (670804)Instructions burned: 1 (million) % 116.92/16.76 % (670804)------------------------------ % 116.92/16.76 % (670804)------------------------------ % 116.92/16.76 % (670806)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=1786660773:i=11404_2918 on theBenchmark for (2918ds/11404Mi) % 116.92/16.76 % (670797)Instruction limit reached! % 116.92/16.76 % (670797)------------------------------ % 116.92/16.76 % (670797)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 116.92/16.76 % (670797)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 116.92/16.76 % (670797)CaDiCaL version: 2.1.3 % 116.92/16.76 % (670797)Termination reason: Instruction limit % 116.92/16.76 % (670797)Termination phase: Saturation % 116.92/16.76 % (670797)Time elapsed: 5.071 s % 116.92/16.76 % (670797)Peak memory usage: 51 MB % 116.92/16.76 % (670797)Instructions burned: 8174 (million) % 116.92/16.76 % (670808)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=1726547219:i=14134_2916 on theBenchmark for (2916ds/14134Mi) % 116.92/16.76 % (670799)Instruction limit reached! % 116.92/16.76 % (670799)------------------------------ % 116.92/16.76 % (670799)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 116.92/16.76 % (670799)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 116.92/16.76 % (670799)CaDiCaL version: 2.1.3 % 116.92/16.76 % (670799)Termination reason: Instruction limit % 116.92/16.76 % (670799)Termination phase: Saturation % 116.92/16.76 % (670799)Time elapsed: 4.623 s % 116.92/16.76 % (670799)Peak memory usage: 52 MB % 116.92/16.76 % (670799)Instructions burned: 9155 (million) % 116.92/16.76 % (670810)dis+33_16_sil=32000:sac=on:random_seed=1051424241:i=15851:nm=0_2914 on theBenchmark for (2914ds/15851Mi) % 116.92/16.76 % (670806)Instruction limit reached! % 116.92/16.76 % (670806)------------------------------ % 116.92/16.76 % (670806)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 116.92/16.76 % (670806)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 116.92/16.76 % (670806)CaDiCaL version: 2.1.3 % 116.92/16.76 % (670806)Termination reason: Instruction limit % 116.92/16.76 % (670806)Termination phase: Saturation % 116.92/16.76 % (670806)Time elapsed: 3.840 s % 116.92/16.76 % (670806)Peak memory usage: 71 MB % 116.92/16.76 % (670806)Instructions burned: 11405 (million) % 116.92/16.76 % (670812)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=3083085721:avsq=on:i=17627:add=on:amm=off_2879 on theBenchmark for (2879ds/17627Mi) % 125.28/18.01 % (670785)Instruction limit reached! % 125.28/18.01 % (670785)------------------------------ % 125.28/18.01 % (670785)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 125.28/18.01 % (670785)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 125.28/18.01 % (670785)CaDiCaL version: 2.1.3 % 125.28/18.01 % (670785)Termination reason: Instruction limit % 125.28/18.01 % (670785)Termination phase: Saturation % 125.28/18.01 % (670785)Time elapsed: 12.902 s % 125.28/18.01 % (670785)Peak memory usage: 169 MB % 125.28/18.01 % (670785)Instructions burned: 29341 (million) % 125.28/18.01 % (670814)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=2719683869:s2a=on:i=53295_2845 on theBenchmark for (2845ds/53295Mi) % 125.28/18.01 % (670810)Instruction limit reached! % 125.28/18.01 % (670810)------------------------------ % 125.28/18.01 % (670810)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 125.28/18.01 % (670810)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 125.28/18.01 % (670810)CaDiCaL version: 2.1.3 % 125.28/18.01 % (670810)Termination reason: Instruction limit % 125.28/18.01 % (670810)Termination phase: Saturation % 125.28/18.01 % (670810)Time elapsed: 7.091 s % 125.28/18.01 % (670810)Peak memory usage: 204 MB % 125.28/18.01 % (670810)Instructions burned: 15852 (million) % 125.28/18.01 % (670816)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=3203002688:i=26857:ins=20_2843 on theBenchmark for (2843ds/26857Mi) % 125.28/18.01 % (670816)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 125.28/18.01 % (670816)Terminated due to inappropriate strategy. % 125.28/18.01 % (670816)------------------------------ % 125.28/18.01 % (670816)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 125.28/18.01 % (670816)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 125.28/18.01 % (670816)CaDiCaL version: 2.1.3 % 125.28/18.01 % (670816)Termination reason: Inappropriate % 125.28/18.01 % (670816)Time elapsed: 0.001 s % 125.28/18.01 % (670816)Peak memory usage: 11 MB % 125.28/18.01 % (670816)Instructions burned: 1 (million) % 125.28/18.01 % (670816)------------------------------ % 125.28/18.01 % (670816)------------------------------ % 125.28/18.01 % (670818)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=3151603424:i=28120:bs=on:fsr=off_2842 on theBenchmark for (2842ds/28120Mi) % 125.28/18.01 % (670812)Instruction limit reached! % 125.28/18.01 % (670812)------------------------------ % 125.28/18.01 % (670812)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 125.28/18.01 % (670812)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 125.28/18.01 % (670812)CaDiCaL version: 2.1.3 % 125.28/18.01 % (670812)Termination reason: Instruction limit % 125.28/18.01 % (670812)Termination phase: Saturation % 125.28/18.01 % (670812)Time elapsed: 4.381 s % 125.28/18.01 % (670812)Peak memory usage: 234 MB % 125.28/18.01 % (670812)Instructions burned: 17629 (million) % 125.28/18.01 % (670820)fmb+10_1_sil=256000:fmbss=7:random_seed=1361624753:fmbsr=1.6:i=182295_2835 on theBenchmark for (2835ds/182295Mi) % 125.28/18.01 % (670801)Instruction limit reached! % 125.28/18.01 % (670801)------------------------------ % 125.28/18.01 % (670801)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 125.28/18.01 % (670801)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 125.28/18.01 % (670801)CaDiCaL version: 2.1.3 % 125.28/18.01 % (670801)Termination reason: Instruction limit % 125.28/18.01 % (670801)Termination phase: Saturation % 125.28/18.01 % (670801)Time elapsed: 10.904 s % 125.28/18.01 % (670801)Peak memory usage: 56 MB % 125.28/18.01 % (670801)Instructions burned: 20141 (million) % 125.28/18.01 % (670820)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 125.28/18.01 % (670820)Terminated due to inappropriate strategy. % 125.28/18.01 % (670820)------------------------------ % 125.28/18.01 % (670820)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 125.28/18.01 % (670820)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 125.28/18.01 % (670820)CaDiCaL version: 2.1.3 % 125.28/18.01 % (670820)Termination reason: Inappropriate % 125.28/18.01 % (670820)Time elapsed: 0.0000 s % 125.28/18.01 % (670820)Peak memory usage: 10 MB % 125.28/18.01 % (670820)Instructions burned: 1 (million) % 125.28/18.01 % (670820)------------------------------ % 125.28/18.01 % (670820)------------------------------ % 125.28/18.01 % (670822)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=404304452:i=44625:gsp=on_2835 on theBenchmark for (2835ds/44625Mi) % 146.03/20.87 % (670822)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 146.03/20.87 % (670822)Terminated due to inappropriate strategy. % 146.03/20.87 % (670822)------------------------------ % 146.03/20.87 % (670822)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 146.03/20.87 % (670822)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 146.03/20.87 % (670822)CaDiCaL version: 2.1.3 % 146.03/20.87 % (670822)Termination reason: Inappropriate % 146.03/20.87 % (670822)Time elapsed: 0.0000 s % 146.03/20.87 % (670822)Peak memory usage: 10 MB % 146.03/20.87 % (670822)Instructions burned: 1 (million) % 146.03/20.87 % (670822)------------------------------ % 146.03/20.87 % (670822)------------------------------ % 146.03/20.87 % (670825)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=512776815:fmbsr=1.3:i=225729_2835 on theBenchmark for (2835ds/225729Mi) % 146.03/20.87 % (670825)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 146.03/20.87 % (670825)Terminated due to inappropriate strategy. % 146.03/20.87 % (670825)------------------------------ % 146.03/20.87 % (670825)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 146.03/20.87 % (670825)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 146.03/20.87 % (670825)CaDiCaL version: 2.1.3 % 146.03/20.87 % (670825)Termination reason: Inappropriate % 146.03/20.87 % (670825)Time elapsed: 0.0000 s % 146.03/20.87 % (670825)Peak memory usage: 10 MB % 146.03/20.87 % (670825)Instructions burned: 1 (million) % 146.03/20.87 % (670825)------------------------------ % 146.03/20.87 % (670825)------------------------------ % 146.03/20.87 % (670823)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=2417932798:i=160505_2835 on theBenchmark for (2835ds/160505Mi) % 146.03/20.87 % (670823)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 146.03/20.87 % (670823)Terminated due to inappropriate strategy. % 146.03/20.87 % (670823)------------------------------ % 146.03/20.87 % (670823)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 146.03/20.87 % (670823)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 146.03/20.87 % (670823)CaDiCaL version: 2.1.3 % 146.03/20.87 % (670823)Termination reason: Inappropriate % 146.03/20.87 % (670823)Time elapsed: 0.001 s % 146.03/20.87 % (670823)Peak memory usage: 10 MB % 146.03/20.87 % (670823)Instructions burned: 1 (million) % 146.03/20.87 % (670823)------------------------------ % 146.03/20.87 % (670823)------------------------------ % 146.03/20.87 % (670827)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=3169130744:fmbsr=2:i=185024:ins=7_2835 on theBenchmark for (2835ds/185024Mi) % 146.03/20.87 % (670827)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 146.03/20.87 % (670827)Terminated due to inappropriate strategy. % 146.03/20.87 % (670827)------------------------------ % 146.03/20.87 % (670827)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 146.03/20.87 % (670827)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 146.03/20.87 % (670827)CaDiCaL version: 2.1.3 % 146.03/20.87 % (670827)Termination reason: Inappropriate % 146.03/20.87 % (670827)Time elapsed: 0.0000 s % 146.03/20.87 % (670827)Peak memory usage: 10 MB % 146.03/20.87 % (670827)Instructions burned: 1 (million) % 146.03/20.87 % (670827)------------------------------ % 146.03/20.87 % (670827)------------------------------ % 146.03/20.87 % (670829)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=1942926469:rtra=on_2835 on theBenchmark for (2835ds/0Mi) % 146.03/20.87 % (670829)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 146.03/20.87 % (670829)Terminated due to inappropriate strategy. % 146.03/20.87 % (670829)------------------------------ % 146.03/20.87 % (670829)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 146.03/20.87 % (670829)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 146.03/20.87 % (670829)CaDiCaL version: 2.1.3 % 146.03/20.87 % (670829)Termination reason: Inappropriate % 146.03/20.87 % (670829)Time elapsed: 0.001 s % 146.03/20.87 % (670829)Peak memory usage: 10 MB % 146.03/20.87 % (670829)Instructions burned: 1 (million) % 146.03/20.87 % (670829)------------------------------ % 146.03/20.87 % (670829)------------------------------ % 146.03/20.87 % (670831)% WARNING: option uhcvi not known. % 146.03/20.87 % (670831)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2114017477:i=271062:add=off:rtra=on:rawr=on_2834 on theBenchmark for (2834ds/271062Mi) % 146.03/20.87 % (670833)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=787019096:i=176048:add=on:rtra=on:rawr=on_2834 on theBenchmark for (2834ds/176048Mi) % 160.24/22.86 % (670808)Instruction limit reached! % 160.24/22.86 % (670808)------------------------------ % 160.24/22.86 % (670808)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 160.24/22.86 % (670808)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 160.24/22.86 % (670808)CaDiCaL version: 2.1.3 % 160.24/22.86 % (670808)Termination reason: Instruction limit % 160.24/22.86 % (670808)Termination phase: Saturation % 160.24/22.86 % (670808)Time elapsed: 8.689 s % 160.24/22.86 % (670808)Peak memory usage: 73 MB % 160.24/22.86 % (670808)Instructions burned: 14134 (million) % 160.24/22.86 % (670836)dis+10_1_sil=32000:si=on:sp=arity:random_seed=2980126874:i=206:fgj=on:rtra=on_2829 on theBenchmark for (2829ds/206Mi) % 160.24/22.86 % (670836)Instruction limit reached! % 160.24/22.86 % (670836)------------------------------ % 160.24/22.86 % (670836)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 160.24/22.86 % (670836)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 160.24/22.86 % (670836)CaDiCaL version: 2.1.3 % 160.24/22.86 % (670836)Termination reason: Instruction limit % 160.24/22.86 % (670836)Termination phase: Saturation % 160.24/22.86 % (670836)Time elapsed: 0.128 s % 160.24/22.86 % (670836)Peak memory usage: 13 MB % 160.24/22.86 % (670836)Instructions burned: 207 (million) % 160.24/22.86 % (670838)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=2160402648:i=232:rtra=on_2828 on theBenchmark for (2828ds/232Mi) % 160.24/22.86 % (670838)Instruction limit reached! % 160.24/22.86 % (670838)------------------------------ % 160.24/22.86 % (670838)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 160.24/22.86 % (670838)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 160.24/22.86 % (670838)CaDiCaL version: 2.1.3 % 160.24/22.86 % (670838)Termination reason: Instruction limit % 160.24/22.86 % (670838)Termination phase: Saturation % 160.24/22.86 % (670838)Time elapsed: 0.146 s % 160.24/22.86 % (670838)Peak memory usage: 13 MB % 160.24/22.86 % (670838)Instructions burned: 232 (million) % 160.24/22.86 % (670840)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=1174929237:i=262:rtra=on_2826 on theBenchmark for (2826ds/262Mi) % 160.24/22.86 % (670840)Instruction limit reached! % 160.24/22.86 % (670840)------------------------------ % 160.24/22.86 % (670840)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 160.24/22.86 % (670840)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 160.24/22.86 % (670840)CaDiCaL version: 2.1.3 % 160.24/22.86 % (670840)Termination reason: Instruction limit % 160.24/22.86 % (670840)Termination phase: Saturation % 160.24/22.86 % (670840)Time elapsed: 0.165 s % 160.24/22.86 % (670840)Peak memory usage: 14 MB % 160.24/22.86 % (670840)Instructions burned: 262 (million) % 160.24/22.86 % (670842)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=2299930286:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2824 on theBenchmark for (2824ds/318Mi) % 160.24/22.86 % (670842)Instruction limit reached! % 160.24/22.86 % (670842)------------------------------ % 160.24/22.86 % (670842)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 160.24/22.86 % (670842)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 160.24/22.86 % (670842)CaDiCaL version: 2.1.3 % 160.24/22.86 % (670842)Termination reason: Instruction limit % 160.24/22.86 % (670842)Termination phase: Saturation % 160.24/22.86 % (670842)Time elapsed: 0.215 s % 160.24/22.86 % (670842)Peak memory usage: 15 MB % 160.24/22.86 % (670842)Instructions burned: 318 (million) % 160.24/22.86 % (670844)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=4127461442:i=1428:nm=2:rtra=on_2822 on theBenchmark for (2822ds/1428Mi) % 160.24/22.86 % (670844)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 160.24/22.86 % (670844)Terminated due to inappropriate strategy. % 160.24/22.86 % (670844)------------------------------ % 160.24/22.86 % (670844)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 160.24/22.86 % (670844)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 160.24/22.86 % (670844)CaDiCaL version: 2.1.3 % 160.24/22.86 % (670844)Termination reason: Inappropriate % 160.24/22.86 % (670844)Time elapsed: 0.001 s % 160.24/22.86 % (670844)Peak memory usage: 10 MB % 160.24/22.86 % (670844)Instructions burned: 1 (million) % 160.24/22.86 % (670844)------------------------------ % 204.45/29.12 % (670844)------------------------------ % 204.45/29.12 % (670846)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=2396348140:i=262:bd=preordered:rtra=on:fsd=on_2822 on theBenchmark for (2822ds/262Mi) % 204.45/29.12 % (670846)Instruction limit reached! % 204.45/29.12 % (670846)------------------------------ % 204.45/29.12 % (670846)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 204.45/29.12 % (670846)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 204.45/29.12 % (670846)CaDiCaL version: 2.1.3 % 204.45/29.12 % (670846)Termination reason: Instruction limit % 204.45/29.12 % (670846)Termination phase: Saturation % 204.45/29.12 % (670846)Time elapsed: 0.177 s % 204.45/29.12 % (670846)Peak memory usage: 14 MB % 204.45/29.12 % (670846)Instructions burned: 263 (million) % 204.45/29.12 % (670848)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=943387172:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2820 on theBenchmark for (2820ds/1368Mi) % 204.45/29.12 % (670848)Instruction limit reached! % 204.45/29.12 % (670848)------------------------------ % 204.45/29.12 % (670848)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 204.45/29.12 % (670848)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 204.45/29.12 % (670848)CaDiCaL version: 2.1.3 % 204.45/29.12 % (670848)Termination reason: Instruction limit % 204.45/29.12 % (670848)Termination phase: Saturation % 204.45/29.12 % (670848)Time elapsed: 0.704 s % 204.45/29.12 % (670848)Peak memory usage: 21 MB % 204.45/29.12 % (670848)Instructions burned: 1369 (million) % 204.45/29.12 % (670850)ott-21_1_sil=16000:si=on:fs=off:random_seed=2489748762:i=360:av=off:fsr=off:rtra=on_2812 on theBenchmark for (2812ds/360Mi) % 204.45/29.12 % (670850)Instruction limit reached! % 204.45/29.12 % (670850)------------------------------ % 204.45/29.12 % (670850)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 204.45/29.12 % (670850)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 204.45/29.12 % (670850)CaDiCaL version: 2.1.3 % 204.45/29.12 % (670850)Termination reason: Instruction limit % 204.45/29.12 % (670850)Termination phase: Saturation % 204.45/29.12 % (670850)Time elapsed: 0.158 s % 204.45/29.12 % (670850)Peak memory usage: 12 MB % 204.45/29.12 % (670850)Instructions burned: 361 (million) % 204.45/29.12 % (670852)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=705155809:i=954:bd=all:rtra=on_2811 on theBenchmark for (2811ds/954Mi) % 204.45/29.12 % (670852)Instruction limit reached! % 204.45/29.12 % (670852)------------------------------ % 204.45/29.12 % (670852)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 204.45/29.12 % (670852)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 204.45/29.12 % (670852)CaDiCaL version: 2.1.3 % 204.45/29.12 % (670852)Termination reason: Instruction limit % 204.45/29.12 % (670852)Termination phase: Saturation % 204.45/29.12 % (670852)Time elapsed: 0.596 s % 204.45/29.12 % (670852)Peak memory usage: 17 MB % 204.45/29.12 % (670852)Instructions burned: 954 (million) % 204.45/29.12 % (670854)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=1230019361:fmbsr=1.3:i=1730:ins=25:rtra=on_2804 on theBenchmark for (2804ds/1730Mi) % 204.45/29.12 % (670854)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 204.45/29.12 % (670854)Terminated due to inappropriate strategy. % 204.45/29.12 % (670854)------------------------------ % 204.45/29.12 % (670854)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 204.45/29.12 % (670854)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 204.45/29.12 % (670854)CaDiCaL version: 2.1.3 % 204.45/29.12 % (670854)Termination reason: Inappropriate % 204.45/29.12 % (670854)Time elapsed: 0.001 s % 204.45/29.12 % (670854)Peak memory usage: 10 MB % 204.45/29.12 % (670854)Instructions burned: 1 (million) % 204.45/29.12 % (670854)------------------------------ % 204.45/29.12 % (670854)------------------------------ % 204.45/29.12 % (670856)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=1135030050:i=2358:rtra=on_2804 on theBenchmark for (2804ds/2358Mi) % 204.45/29.12 % (670856)Instruction limit reached! % 204.45/29.12 % (670856)------------------------------ % 204.45/29.12 % (670856)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 204.45/29.12 % (670856)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 204.45/29.12 % (670856)CaDiCaL version: 2.1.3 % 204.45/29.12 % (670856)Termination reason: Instruction limit % 204.45/29.12 % (670856)Termination phase: Saturation % 271.00/38.43 % (670856)Time elapsed: 1.096 s % 271.00/38.43 % (670856)Peak memory usage: 27 MB % 271.00/38.43 % (670856)Instructions burned: 2359 (million) % 271.00/38.43 % (670858)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=865126384:i=1778:ins=1:rtra=on_2793 on theBenchmark for (2793ds/1778Mi) % 271.00/38.43 % (670858)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 271.00/38.43 % (670858)Terminated due to inappropriate strategy. % 271.00/38.43 % (670858)------------------------------ % 271.00/38.43 % (670858)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 271.00/38.43 % (670858)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 271.00/38.43 % (670858)CaDiCaL version: 2.1.3 % 271.00/38.43 % (670858)Termination reason: Inappropriate % 271.00/38.43 % (670858)Time elapsed: 0.001 s % 271.00/38.43 % (670858)Peak memory usage: 10 MB % 271.00/38.43 % (670858)Instructions burned: 1 (million) % 271.00/38.43 % (670858)------------------------------ % 271.00/38.43 % (670858)------------------------------ % 271.00/38.43 % (670860)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=3536624567:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2793 on theBenchmark for (2793ds/1384Mi) % 271.00/38.43 % (670860)Instruction limit reached! % 271.00/38.43 % (670860)------------------------------ % 271.00/38.43 % (670860)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 271.00/38.43 % (670860)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 271.00/38.43 % (670860)CaDiCaL version: 2.1.3 % 271.00/38.43 % (670860)Termination reason: Instruction limit % 271.00/38.43 % (670860)Termination phase: Saturation % 271.00/38.43 % (670860)Time elapsed: 0.856 s % 271.00/38.43 % (670860)Peak memory usage: 21 MB % 271.00/38.43 % (670860)Instructions burned: 1385 (million) % 271.00/38.43 % (670862)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=3074976130:i=1758:kws=inv_precedence:fsr=off:rtra=on_2784 on theBenchmark for (2784ds/1758Mi) % 271.00/38.43 % (670862)Instruction limit reached! % 271.00/38.43 % (670862)------------------------------ % 271.00/38.43 % (670862)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 271.00/38.43 % (670862)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 271.00/38.43 % (670862)CaDiCaL version: 2.1.3 % 271.00/38.43 % (670862)Termination reason: Instruction limit % 271.00/38.43 % (670862)Termination phase: Saturation % 271.00/38.43 % (670862)Time elapsed: 0.998 s % 271.00/38.43 % (670862)Peak memory usage: 28 MB % 271.00/38.43 % (670862)Instructions burned: 1759 (million) % 271.00/38.43 % (670864)fmb+10_1_sil=64000:si=on:random_seed=785007913:i=44122:nm=2:rtra=on:gsp=on_2774 on theBenchmark for (2774ds/44122Mi) % 271.00/38.43 % (670864)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 271.00/38.43 % (670864)Terminated due to inappropriate strategy. % 271.00/38.43 % (670864)------------------------------ % 271.00/38.43 % (670864)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 271.00/38.43 % (670864)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 271.00/38.43 % (670864)CaDiCaL version: 2.1.3 % 271.00/38.43 % (670864)Termination reason: Inappropriate % 271.00/38.43 % (670864)Time elapsed: 0.001 s % 271.00/38.43 % (670864)Peak memory usage: 10 MB % 271.00/38.43 % (670864)Instructions burned: 1 (million) % 271.00/38.43 % (670864)------------------------------ % 271.00/38.43 % (670864)------------------------------ % 271.00/38.43 % (670866)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=626057938:i=19030:nm=5:rtra=on_2774 on theBenchmark for (2774ds/19030Mi) % 271.00/38.43 % (670866)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 271.00/38.43 % (670866)Terminated due to inappropriate strategy. % 271.00/38.43 % (670866)------------------------------ % 271.00/38.43 % (670866)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 271.00/38.43 % (670866)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 271.00/38.43 % (670866)CaDiCaL version: 2.1.3 % 271.00/38.43 % (670866)Termination reason: Inappropriate % 271.00/38.43 % (670866)Time elapsed: 0.001 s % 271.00/38.43 % (670866)Peak memory usage: 10 MB % 271.00/38.43 % (670866)Instructions burned: 1 (million) % 271.00/38.43 % (670866)------------------------------ % 271.00/38.43 % (670866)------------------------------ % 271.00/38.43 % (670868)fmb+10_1_sil=64000:sas=cadical:si=on:fmbss=8:random_seed=4117294664:fmbsr=1.7:i=1840:rtra=on_Terminated % 300.07/42.54 % Vampire exiting % 300.07/42.54 Terminated %------------------------------------------------------------------------------