%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWW831_1 : TPTP v9.3.1. Released v7.0.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % Computer : n016.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:45:02 PM UTC 2026 % Result : Timeout 300.66s 42.63s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : SWW831_1 : TPTP v9.3.1. Released v7.0.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.06/0.19 % Computer : n016.cluster.edu % 0.06/0.19 % Model : x86_64 x86_64 % 0.06/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.06/0.19 % Memory : 8046.5625MB % 0.06/0.19 % OS : Linux 6.8.0-71-generic % 0.06/0.19 % CPULimit : 300 % 0.06/0.19 % WCLimit : 300 % 0.06/0.19 % DateTime : Mon Sep 28 14:36:04 UTC 2026 % 0.06/0.19 % CPUTime : % 0.06/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.06/0.22 Running first-order model finding % 0.06/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.93/0.89 % (3672235)Will run a generic schedule for satisfiability detection. % 3.93/0.89 % (3672245)% WARNING: option uhcvi not known. % 3.93/0.89 % (3672245)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=386775262:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 3.93/0.89 % (3672247)dis+10_1_sil=32000:sp=arity:random_seed=3744516940:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 3.93/0.89 % (3672246)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1564723486:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 3.93/0.89 % (3672244)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=324890135_2999 on theBenchmark for (2999ds/0Mi) % 3.93/0.89 % (3672248)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3651139773:i=116_2999 on theBenchmark for (2999ds/116Mi) % 3.93/0.89 % (3672250)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=257545242:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 3.93/0.89 % (3672249)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2158617560:i=131_2999 on theBenchmark for (2999ds/131Mi) % 3.93/0.89 % (3672244)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.93/0.89 % (3672244)Terminated due to inappropriate strategy. % 3.93/0.89 % (3672244)------------------------------ % 3.93/0.89 % (3672244)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.93/0.89 % (3672244)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.93/0.89 % (3672244)CaDiCaL version: 2.1.3 % 3.93/0.89 % (3672244)Termination reason: Inappropriate % 3.93/0.89 % (3672244)Time elapsed: 0.029 s % 3.93/0.89 % (3672244)Peak memory usage: 12 MB % 3.93/0.89 % (3672244)Instructions burned: 65 (million) % 3.93/0.89 % (3672244)------------------------------ % 3.93/0.89 % (3672244)------------------------------ % 3.93/0.89 % (3672258)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2427944401:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 3.93/0.89 % (3672247)Instruction limit reached! % 3.93/0.89 % (3672247)------------------------------ % 3.93/0.89 % (3672247)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.93/0.89 % (3672247)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.93/0.89 % (3672247)CaDiCaL version: 2.1.3 % 3.93/0.89 % (3672247)Termination reason: Instruction limit % 3.93/0.89 % (3672247)Termination phase: Saturation % 3.93/0.89 % (3672247)Time elapsed: 0.053 s % 3.93/0.89 % (3672247)Peak memory usage: 13 MB % 3.93/0.89 % (3672247)Instructions burned: 104 (million) % 3.93/0.89 % (3672248)Instruction limit reached! % 3.93/0.89 % (3672248)------------------------------ % 3.93/0.89 % (3672248)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.93/0.89 % (3672248)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.93/0.89 % (3672248)CaDiCaL version: 2.1.3 % 3.93/0.89 % (3672248)Termination reason: Instruction limit % 3.93/0.89 % (3672248)Termination phase: Saturation % 3.93/0.89 % (3672248)Time elapsed: 0.060 s % 3.93/0.89 % (3672248)Peak memory usage: 14 MB % 3.93/0.89 % (3672248)Instructions burned: 117 (million) % 3.93/0.89 % (3672249)Instruction limit reached! % 3.93/0.89 % (3672249)------------------------------ % 3.93/0.89 % (3672249)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.93/0.89 % (3672249)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.93/0.89 % (3672249)CaDiCaL version: 2.1.3 % 3.93/0.89 % (3672249)Termination reason: Instruction limit % 3.93/0.89 % (3672249)Termination phase: Saturation % 3.93/0.89 % (3672249)Time elapsed: 0.068 s % 3.93/0.89 % (3672249)Peak memory usage: 14 MB % 3.93/0.89 % (3672249)Instructions burned: 132 (million) % 3.93/0.89 % (3672260)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=836778581:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 3.93/0.89 % (3672261)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=645414968:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi) % 3.93/0.89 % (3672258)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.93/0.89 % (3672258)Terminated due to inappropriate strategy. % 3.93/0.89 % (3672258)------------------------------ % 3.93/0.89 % (3672258)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.63/1.12 % (3672258)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.63/1.12 % (3672258)CaDiCaL version: 2.1.3 % 5.63/1.12 % (3672258)Termination reason: Inappropriate % 5.63/1.12 % (3672258)Time elapsed: 0.030 s % 5.63/1.12 % (3672258)Peak memory usage: 12 MB % 5.63/1.12 % (3672258)Instructions burned: 65 (million) % 5.63/1.12 % (3672258)------------------------------ % 5.63/1.12 % (3672258)------------------------------ % 5.63/1.12 % (3672262)ott-21_1_sil=16000:fs=off:random_seed=3869400287:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 5.63/1.12 % (3672250)Instruction limit reached! % 5.63/1.12 % (3672250)------------------------------ % 5.63/1.12 % (3672250)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.63/1.12 % (3672250)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.63/1.12 % (3672250)CaDiCaL version: 2.1.3 % 5.63/1.12 % (3672250)Termination reason: Instruction limit % 5.63/1.12 % (3672250)Termination phase: Saturation % 5.63/1.12 % (3672250)Time elapsed: 0.092 s % 5.63/1.12 % (3672250)Peak memory usage: 14 MB % 5.63/1.12 % (3672250)Instructions burned: 160 (million) % 5.63/1.12 % (3672265)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3240645534:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 5.63/1.12 % (3672267)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3137059950:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 5.63/1.12 % (3672267)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 5.63/1.12 % (3672267)Terminated due to inappropriate strategy. % 5.63/1.12 % (3672267)------------------------------ % 5.63/1.12 % (3672267)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.63/1.12 % (3672267)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.63/1.12 % (3672267)CaDiCaL version: 2.1.3 % 5.63/1.12 % (3672267)Termination reason: Inappropriate % 5.63/1.12 % (3672267)Time elapsed: 0.029 s % 5.63/1.12 % (3672267)Peak memory usage: 12 MB % 5.63/1.12 % (3672267)Instructions burned: 64 (million) % 5.63/1.12 % (3672260)Instruction limit reached! % 5.63/1.12 % (3672260)------------------------------ % 5.63/1.12 % (3672260)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.63/1.12 % (3672260)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.63/1.12 % (3672260)CaDiCaL version: 2.1.3 % 5.63/1.12 % (3672260)Termination reason: Instruction limit % 5.63/1.12 % (3672260)Termination phase: Saturation % 5.63/1.12 % (3672260)Time elapsed: 0.069 s % 5.63/1.12 % (3672260)Peak memory usage: 14 MB % 5.63/1.12 % (3672260)Instructions burned: 131 (million) % 5.63/1.12 % (3672267)------------------------------ % 5.63/1.12 % (3672267)------------------------------ % 5.63/1.12 % (3672270)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1637028053:i=1179_2998 on theBenchmark for (2998ds/1179Mi) % 5.63/1.12 % (3672271)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3367018096:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi) % 5.63/1.12 % (3672262)Instruction limit reached! % 5.63/1.12 % (3672262)------------------------------ % 5.63/1.12 % (3672262)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.63/1.12 % (3672262)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.63/1.12 % (3672262)CaDiCaL version: 2.1.3 % 5.63/1.12 % (3672262)Termination reason: Instruction limit % 5.63/1.12 % (3672262)Termination phase: Saturation % 5.63/1.12 % (3672262)Time elapsed: 0.084 s % 5.63/1.12 % (3672262)Peak memory usage: 14 MB % 5.63/1.12 % (3672262)Instructions burned: 182 (million) % 5.63/1.12 % (3672274)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=3718298376:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2997 on theBenchmark for (2997ds/692Mi) % 5.63/1.12 % (3672271)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 5.63/1.12 % (3672271)Terminated due to inappropriate strategy. % 5.63/1.12 % (3672271)------------------------------ % 5.63/1.12 % (3672271)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.63/1.12 % (3672271)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.63/1.12 % (3672271)CaDiCaL version: 2.1.3 % 5.63/1.12 % (3672271)Termination reason: Inappropriate % 5.63/1.12 % (3672271)Time elapsed: 0.031 s % 5.63/1.12 % (3672271)Peak memory usage: 12 MB % 22.41/3.48 % (3672271)Instructions burned: 65 (million) % 22.41/3.48 % (3672271)------------------------------ % 22.41/3.48 % (3672271)------------------------------ % 22.41/3.48 % (3672276)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2837690271:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi) % 22.41/3.48 % (3672265)Instruction limit reached! % 22.41/3.48 % (3672265)------------------------------ % 22.41/3.48 % (3672265)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.41/3.48 % (3672265)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.41/3.48 % (3672265)CaDiCaL version: 2.1.3 % 22.41/3.48 % (3672265)Termination reason: Instruction limit % 22.41/3.48 % (3672265)Termination phase: Saturation % 22.41/3.48 % (3672265)Time elapsed: 0.288 s % 22.41/3.48 % (3672265)Peak memory usage: 16 MB % 22.41/3.48 % (3672265)Instructions burned: 477 (million) % 22.41/3.48 % (3672278)fmb+10_1_sil=64000:random_seed=529536834:i=22061:nm=2:gsp=on_2995 on theBenchmark for (2995ds/22061Mi) % 22.41/3.48 % (3672278)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 22.41/3.48 % (3672278)Terminated due to inappropriate strategy. % 22.41/3.48 % (3672278)------------------------------ % 22.41/3.48 % (3672278)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.41/3.48 % (3672278)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.41/3.48 % (3672278)CaDiCaL version: 2.1.3 % 22.41/3.48 % (3672278)Termination reason: Inappropriate % 22.41/3.48 % (3672278)Time elapsed: 0.029 s % 22.41/3.48 % (3672278)Peak memory usage: 12 MB % 22.41/3.48 % (3672278)Instructions burned: 65 (million) % 22.41/3.48 % (3672278)------------------------------ % 22.41/3.48 % (3672278)------------------------------ % 22.41/3.48 % (3672261)Instruction limit reached! % 22.41/3.48 % (3672261)------------------------------ % 22.41/3.48 % (3672261)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.41/3.48 % (3672261)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.41/3.48 % (3672261)CaDiCaL version: 2.1.3 % 22.41/3.48 % (3672261)Termination reason: Instruction limit % 22.41/3.48 % (3672261)Termination phase: Saturation % 22.41/3.48 % (3672261)Time elapsed: 0.371 s % 22.41/3.48 % (3672261)Peak memory usage: 17 MB % 22.41/3.48 % (3672261)Instructions burned: 684 (million) % 22.41/3.48 % (3672280)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2605638052:i=9515:nm=5_2995 on theBenchmark for (2995ds/9515Mi) % 22.41/3.48 % (3672281)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1928166878:fmbsr=1.7:i=920_2995 on theBenchmark for (2995ds/920Mi) % 22.41/3.48 % (3672280)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 22.41/3.48 % (3672280)Terminated due to inappropriate strategy. % 22.41/3.48 % (3672280)------------------------------ % 22.41/3.48 % (3672280)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.41/3.48 % (3672280)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.41/3.48 % (3672280)CaDiCaL version: 2.1.3 % 22.41/3.48 % (3672280)Termination reason: Inappropriate % 22.41/3.48 % (3672280)Time elapsed: 0.029 s % 22.41/3.48 % (3672280)Peak memory usage: 12 MB % 22.41/3.48 % (3672280)Instructions burned: 65 (million) % 22.41/3.48 % (3672280)------------------------------ % 22.41/3.48 % (3672280)------------------------------ % 22.41/3.48 % (3672281)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 22.41/3.48 % (3672281)Terminated due to inappropriate strategy. % 22.41/3.48 % (3672281)------------------------------ % 22.41/3.48 % (3672281)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.41/3.48 % (3672281)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.41/3.48 % (3672281)CaDiCaL version: 2.1.3 % 22.41/3.48 % (3672281)Termination reason: Inappropriate % 22.41/3.48 % (3672281)Time elapsed: 0.029 s % 22.41/3.48 % (3672281)Peak memory usage: 12 MB % 22.41/3.48 % (3672281)Instructions burned: 65 (million) % 22.41/3.48 % (3672281)------------------------------ % 22.41/3.48 % (3672281)------------------------------ % 22.41/3.48 % (3672284)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1667613037:i=5131_2994 on theBenchmark for (2994ds/5131Mi) % 22.41/3.48 % (3672285)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2388632467:i=1472:ins=7:fdi=8:gsp=on_2994 on theBenchmark for (2994ds/1472Mi) % 22.41/3.48 % (3672274)Instruction limit reached! % 22.41/3.48 % (3672274)------------------------------ % 36.61/5.46 % (3672274)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 36.61/5.46 % (3672274)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 36.61/5.46 % (3672274)CaDiCaL version: 2.1.3 % 36.61/5.46 % (3672274)Termination reason: Instruction limit % 36.61/5.46 % (3672274)Termination phase: Saturation % 36.61/5.46 % (3672274)Time elapsed: 0.414 s % 36.61/5.46 % (3672274)Peak memory usage: 19 MB % 36.61/5.46 % (3672274)Instructions burned: 692 (million) % 36.61/5.46 % (3672288)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=2086448960:i=6324_2993 on theBenchmark for (2993ds/6324Mi) % 36.61/5.46 % (3672288)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 36.61/5.46 % (3672288)Terminated due to inappropriate strategy. % 36.61/5.46 % (3672288)------------------------------ % 36.61/5.46 % (3672288)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 36.61/5.46 % (3672288)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 36.61/5.46 % (3672288)CaDiCaL version: 2.1.3 % 36.61/5.46 % (3672288)Termination reason: Inappropriate % 36.61/5.46 % (3672288)Time elapsed: 0.029 s % 36.61/5.46 % (3672288)Peak memory usage: 12 MB % 36.61/5.46 % (3672288)Instructions burned: 65 (million) % 36.61/5.46 % (3672288)------------------------------ % 36.61/5.46 % (3672288)------------------------------ % 36.61/5.46 % (3672290)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=687067202:fmbsr=2.30978:i=2174_2992 on theBenchmark for (2992ds/2174Mi) % 36.61/5.46 % (3672276)Instruction limit reached! % 36.61/5.46 % (3672276)------------------------------ % 36.61/5.46 % (3672276)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 36.61/5.46 % (3672276)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 36.61/5.46 % (3672276)CaDiCaL version: 2.1.3 % 36.61/5.46 % (3672276)Termination reason: Instruction limit % 36.61/5.46 % (3672276)Termination phase: Saturation % 36.61/5.46 % (3672276)Time elapsed: 0.486 s % 36.61/5.46 % (3672276)Peak memory usage: 18 MB % 36.61/5.46 % (3672276)Instructions burned: 879 (million) % 36.61/5.46 % (3672290)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 36.61/5.46 % (3672290)Terminated due to inappropriate strategy. % 36.61/5.46 % (3672290)------------------------------ % 36.61/5.46 % (3672290)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 36.61/5.46 % (3672290)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 36.61/5.46 % (3672290)CaDiCaL version: 2.1.3 % 36.61/5.46 % (3672290)Termination reason: Inappropriate % 36.61/5.46 % (3672290)Time elapsed: 0.029 s % 36.61/5.46 % (3672290)Peak memory usage: 12 MB % 36.61/5.46 % (3672290)Instructions burned: 65 (million) % 36.61/5.46 % (3672290)------------------------------ % 36.61/5.46 % (3672290)------------------------------ % 36.61/5.46 % (3672292)ott-2_1_sil=16000:newcnf=on:random_seed=2648596363:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2992 on theBenchmark for (2992ds/869Mi) % 36.61/5.46 % (3672293)ott+10_1_sil=32000:tgt=ground:random_seed=1249961907:i=5114:av=off_2992 on theBenchmark for (2992ds/5114Mi) % 36.61/5.46 % (3672270)Instruction limit reached! % 36.61/5.46 % (3672270)------------------------------ % 36.61/5.46 % (3672270)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 36.61/5.46 % (3672270)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 36.61/5.46 % (3672270)CaDiCaL version: 2.1.3 % 36.61/5.46 % (3672270)Termination reason: Instruction limit % 36.61/5.46 % (3672270)Termination phase: Saturation % 36.61/5.46 % (3672270)Time elapsed: 0.631 s % 36.61/5.46 % (3672270)Peak memory usage: 22 MB % 36.61/5.46 % (3672270)Instructions burned: 1180 (million) % 36.61/5.46 % (3672296)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2961941906:i=54282_2991 on theBenchmark for (2991ds/54282Mi) % 36.61/5.46 % (3672296)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 36.61/5.46 % (3672296)Terminated due to inappropriate strategy. % 36.61/5.46 % (3672296)------------------------------ % 36.61/5.46 % (3672296)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 36.61/5.46 % (3672296)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 36.61/5.46 % (3672296)CaDiCaL version: 2.1.3 % 36.61/5.46 % (3672296)Termination reason: Inappropriate % 36.61/5.46 % (3672296)Time elapsed: 0.029 s % 36.61/5.46 % (3672296)Peak memory usage: 12 MB % 36.61/5.46 % (3672296)Instructions burned: 65 (million) % 106.17/15.20 % (3672296)------------------------------ % 106.17/15.20 % (3672296)------------------------------ % 106.17/15.20 % (3672298)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=2821202984:i=3512:aac=none_2991 on theBenchmark for (2991ds/3512Mi) % 106.17/15.20 % (3672292)Instruction limit reached! % 106.17/15.20 % (3672292)------------------------------ % 106.17/15.20 % (3672292)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 106.17/15.20 % (3672292)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 106.17/15.20 % (3672292)CaDiCaL version: 2.1.3 % 106.17/15.20 % (3672292)Termination reason: Instruction limit % 106.17/15.20 % (3672292)Termination phase: Saturation % 106.17/15.20 % (3672292)Time elapsed: 0.486 s % 106.17/15.20 % (3672292)Peak memory usage: 19 MB % 106.17/15.20 % (3672292)Instructions burned: 869 (million) % 106.17/15.20 % (3672300)dis+21_1_sil=32000:sas=cadical:random_seed=463640336:i=3773:amm=off_2987 on theBenchmark for (2987ds/3773Mi) % 106.17/15.20 % (3672285)Instruction limit reached! % 106.17/15.20 % (3672285)------------------------------ % 106.17/15.20 % (3672285)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 106.17/15.20 % (3672285)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 106.17/15.20 % (3672285)CaDiCaL version: 2.1.3 % 106.17/15.20 % (3672285)Termination reason: Instruction limit % 106.17/15.20 % (3672285)Termination phase: Saturation % 106.17/15.20 % (3672285)Time elapsed: 0.771 s % 106.17/15.20 % (3672285)Peak memory usage: 31 MB % 106.17/15.20 % (3672285)Instructions burned: 1474 (million) % 106.17/15.20 % (3672302)ott+11_1_sil=16000:gs=on:random_seed=2569782744:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2986 on theBenchmark for (2986ds/2251Mi) % 106.17/15.20 % (3672302)Instruction limit reached! % 106.17/15.20 % (3672302)------------------------------ % 106.17/15.20 % (3672302)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 106.17/15.20 % (3672302)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 106.17/15.20 % (3672302)CaDiCaL version: 2.1.3 % 106.17/15.20 % (3672302)Termination reason: Instruction limit % 106.17/15.20 % (3672302)Termination phase: Saturation % 106.17/15.20 % (3672302)Time elapsed: 1.271 s % 106.17/15.20 % (3672302)Peak memory usage: 36 MB % 106.17/15.20 % (3672302)Instructions burned: 2252 (million) % 106.17/15.20 % (3672304)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=2548833107:fmbsr=1.6:i=67534_2973 on theBenchmark for (2973ds/67534Mi) % 106.17/15.20 % (3672304)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 106.17/15.20 % (3672304)Terminated due to inappropriate strategy. % 106.17/15.20 % (3672304)------------------------------ % 106.17/15.20 % (3672304)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 106.17/15.20 % (3672304)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 106.17/15.20 % (3672304)CaDiCaL version: 2.1.3 % 106.17/15.20 % (3672304)Termination reason: Inappropriate % 106.17/15.20 % (3672304)Time elapsed: 0.030 s % 106.17/15.20 % (3672304)Peak memory usage: 12 MB % 106.17/15.20 % (3672304)Instructions burned: 65 (million) % 106.17/15.20 % (3672304)------------------------------ % 106.17/15.20 % (3672304)------------------------------ % 106.17/15.20 % (3672306)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=1430548523:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2973 on theBenchmark for (2973ds/4591Mi) % 106.17/15.20 % (3672298)Instruction limit reached! % 106.17/15.20 % (3672298)------------------------------ % 106.17/15.20 % (3672298)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 106.17/15.20 % (3672298)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 106.17/15.20 % (3672298)CaDiCaL version: 2.1.3 % 106.17/15.20 % (3672298)Termination reason: Instruction limit % 106.17/15.20 % (3672298)Termination phase: Saturation % 106.17/15.20 % (3672298)Time elapsed: 1.844 s % 106.17/15.20 % (3672298)Peak memory usage: 40 MB % 106.17/15.20 % (3672298)Instructions burned: 3512 (million) % 106.17/15.20 % (3672308)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=2022413906:i=29340_2972 on theBenchmark for (2972ds/29340Mi) % 106.17/15.20 % (3672300)Instruction limit reached! % 106.17/15.20 % (3672300)------------------------------ % 106.17/15.20 % (3672300)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 106.17/15.20 % (3672300)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 106.17/15.20 % (3672300)CaDiCaL version: 2.1.3 % 106.17/15.20 % (3672300)Termination reason: Instruction limit % 127.01/18.19 % (3672300)Termination phase: Saturation % 127.01/18.19 % (3672300)Time elapsed: 1.971 s % 127.01/18.19 % (3672300)Peak memory usage: 41 MB % 127.01/18.19 % (3672300)Instructions burned: 3776 (million) % 127.01/18.19 % (3672284)Instruction limit reached! % 127.01/18.19 % (3672284)------------------------------ % 127.01/18.19 % (3672284)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 127.01/18.19 % (3672284)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 127.01/18.19 % (3672284)CaDiCaL version: 2.1.3 % 127.01/18.19 % (3672284)Termination reason: Instruction limit % 127.01/18.19 % (3672284)Termination phase: Saturation % 127.01/18.19 % (3672284)Time elapsed: 2.711 s % 127.01/18.19 % (3672284)Peak memory usage: 46 MB % 127.01/18.19 % (3672284)Instructions burned: 5133 (million) % 127.01/18.19 % (3672310)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=83500690:i=5211_2967 on theBenchmark for (2967ds/5211Mi) % 127.01/18.19 % (3672312)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=1997015646:i=5497:nm=2_2967 on theBenchmark for (2967ds/5497Mi) % 127.01/18.19 % (3672312)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 127.01/18.19 % (3672312)Terminated due to inappropriate strategy. % 127.01/18.19 % (3672312)------------------------------ % 127.01/18.19 % (3672312)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 127.01/18.19 % (3672312)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 127.01/18.19 % (3672312)CaDiCaL version: 2.1.3 % 127.01/18.19 % (3672312)Termination reason: Inappropriate % 127.01/18.19 % (3672312)Time elapsed: 0.029 s % 127.01/18.19 % (3672312)Peak memory usage: 12 MB % 127.01/18.19 % (3672312)Instructions burned: 65 (million) % 127.01/18.19 % (3672312)------------------------------ % 127.01/18.19 % (3672312)------------------------------ % 127.01/18.19 % (3672314)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=2205566695:fmbsr=2:i=46332_2966 on theBenchmark for (2966ds/46332Mi) % 127.01/18.19 % (3672314)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 127.01/18.19 % (3672314)Terminated due to inappropriate strategy. % 127.01/18.19 % (3672314)------------------------------ % 127.01/18.19 % (3672314)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 127.01/18.19 % (3672314)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 127.01/18.19 % (3672314)CaDiCaL version: 2.1.3 % 127.01/18.19 % (3672314)Termination reason: Inappropriate % 127.01/18.19 % (3672314)Time elapsed: 0.029 s % 127.01/18.19 % (3672314)Peak memory usage: 12 MB % 127.01/18.19 % (3672314)Instructions burned: 65 (million) % 127.01/18.19 % (3672314)------------------------------ % 127.01/18.19 % (3672314)------------------------------ % 127.01/18.19 % (3672316)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=3008175343:i=14071_2966 on theBenchmark for (2966ds/14071Mi) % 127.01/18.19 % (3672316)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 127.01/18.19 % (3672316)Terminated due to inappropriate strategy. % 127.01/18.19 % (3672316)------------------------------ % 127.01/18.19 % (3672316)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 127.01/18.19 % (3672316)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 127.01/18.19 % (3672316)CaDiCaL version: 2.1.3 % 127.01/18.19 % (3672316)Termination reason: Inappropriate % 127.01/18.19 % (3672316)Time elapsed: 0.029 s % 127.01/18.19 % (3672316)Peak memory usage: 12 MB % 127.01/18.19 % (3672316)Instructions burned: 65 (million) % 127.01/18.19 % (3672316)------------------------------ % 127.01/18.19 % (3672316)------------------------------ % 127.01/18.19 % (3672318)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3339991162:i=22565:add=on:rawr=on_2965 on theBenchmark for (2965ds/22565Mi) % 127.01/18.19 % (3672293)Instruction limit reached! % 127.01/18.19 % (3672293)------------------------------ % 127.01/18.19 % (3672293)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 127.01/18.19 % (3672293)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 127.01/18.19 % (3672293)CaDiCaL version: 2.1.3 % 127.01/18.19 % (3672293)Termination reason: Instruction limit % 127.01/18.19 % (3672293)Termination phase: Saturation % 127.01/18.19 % (3672293)Time elapsed: 2.847 s % 127.01/18.19 % (3672293)Peak memory usage: 53 MB % 127.01/18.19 % (3672293)Instructions burned: 5115 (million) % 127.01/18.19 % (3672320)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=2009110046:i=8173:av=off_2963 on theBenchmark for (2963ds/8173Mi) % 128.87/18.45 % (3672306)Instruction limit reached! % 128.87/18.45 % (3672306)------------------------------ % 128.87/18.45 % (3672306)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 128.87/18.45 % (3672306)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 128.87/18.45 % (3672306)CaDiCaL version: 2.1.3 % 128.87/18.45 % (3672306)Termination reason: Instruction limit % 128.87/18.45 % (3672306)Termination phase: Saturation % 128.87/18.45 % (3672306)Time elapsed: 2.516 s % 128.87/18.45 % (3672306)Peak memory usage: 64 MB % 128.87/18.45 % (3672306)Instructions burned: 4592 (million) % 128.87/18.45 % (3672322)dis+10_16:1_sil=16000:random_seed=4238850526:i=9155:fsr=off_2947 on theBenchmark for (2947ds/9155Mi) % 128.87/18.45 % (3672310)Instruction limit reached! % 128.87/18.45 % (3672310)------------------------------ % 128.87/18.45 % (3672310)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 128.87/18.45 % (3672310)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 128.87/18.45 % (3672310)CaDiCaL version: 2.1.3 % 128.87/18.45 % (3672310)Termination reason: Instruction limit % 128.87/18.45 % (3672310)Termination phase: Saturation % 128.87/18.45 % (3672310)Time elapsed: 2.830 s % 128.87/18.45 % (3672310)Peak memory usage: 48 MB % 128.87/18.45 % (3672310)Instructions burned: 5211 (million) % 128.87/18.45 % (3672324)ott-3_8_sil=64000:random_seed=2833625438:i=20139:bs=on_2938 on theBenchmark for (2938ds/20139Mi) % 128.87/18.45 % (3672320)Instruction limit reached! % 128.87/18.45 % (3672320)------------------------------ % 128.87/18.45 % (3672320)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 128.87/18.45 % (3672320)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 128.87/18.45 % (3672320)CaDiCaL version: 2.1.3 % 128.87/18.45 % (3672320)Termination reason: Instruction limit % 128.87/18.45 % (3672320)Termination phase: Saturation % 128.87/18.45 % (3672320)Time elapsed: 4.706 s % 128.87/18.45 % (3672320)Peak memory usage: 80 MB % 128.87/18.45 % (3672320)Instructions burned: 8174 (million) % 128.87/18.45 % (3672326)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=2547146417:fmbsr=2:i=32576_2916 on theBenchmark for (2916ds/32576Mi) % 128.87/18.45 % (3672326)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 128.87/18.45 % (3672326)Terminated due to inappropriate strategy. % 128.87/18.45 % (3672326)------------------------------ % 128.87/18.45 % (3672326)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 128.87/18.45 % (3672326)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 128.87/18.45 % (3672326)CaDiCaL version: 2.1.3 % 128.87/18.45 % (3672326)Termination reason: Inappropriate % 128.87/18.45 % (3672326)Time elapsed: 0.029 s % 128.87/18.45 % (3672326)Peak memory usage: 12 MB % 128.87/18.45 % (3672326)Instructions burned: 65 (million) % 128.87/18.45 % (3672326)------------------------------ % 128.87/18.45 % (3672326)------------------------------ % 128.87/18.45 % (3672328)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=1564412191:i=11404_2915 on theBenchmark for (2915ds/11404Mi) % 128.87/18.45 % (3672322)Instruction limit reached! % 128.87/18.45 % (3672322)------------------------------ % 128.87/18.45 % (3672322)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 128.87/18.45 % (3672322)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 128.87/18.45 % (3672322)CaDiCaL version: 2.1.3 % 128.87/18.45 % (3672322)Termination reason: Instruction limit % 128.87/18.45 % (3672322)Termination phase: Saturation % 128.87/18.45 % (3672322)Time elapsed: 4.646 s % 128.87/18.45 % (3672322)Peak memory usage: 57 MB % 128.87/18.45 % (3672322)Instructions burned: 9157 (million) % 128.87/18.45 % (3672330)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=824638308:i=14134_2900 on theBenchmark for (2900ds/14134Mi) % 128.87/18.45 % (3672318)Instruction limit reached! % 128.87/18.45 % (3672318)------------------------------ % 128.87/18.45 % (3672318)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 128.87/18.45 % (3672318)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 128.87/18.45 % (3672318)CaDiCaL version: 2.1.3 % 128.87/18.45 % (3672318)Termination reason: Instruction limit % 128.87/18.45 % (3672318)Termination phase: Saturation % 128.87/18.45 % (3672318)Time elapsed: 9.745 s % 128.87/18.45 % (3672318)Peak memory usage: 84 MB % 128.87/18.45 % (3672318)Instructions burned: 22566 (million) % 128.87/18.45 % (3672341)dis+33_16_sil=32000:sac=on:random_seed=2963655176:i=15851:nm=0_2868 on theBenchmark for (2868ds/15851Mi) % 128.87/18.45 % (3672328)Instruction limit reached! % 128.87/18.45 % (3672328)------------------------------ % 128.87/18.45 % (3672328)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 177.03/25.29 % (3672328)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 177.03/25.29 % (3672328)CaDiCaL version: 2.1.3 % 177.03/25.29 % (3672328)Termination reason: Instruction limit % 177.03/25.29 % (3672328)Termination phase: Saturation % 177.03/25.29 % (3672328)Time elapsed: 6.537 s % 177.03/25.29 % (3672328)Peak memory usage: 91 MB % 177.03/25.29 % (3672328)Instructions burned: 11407 (million) % 177.03/25.29 % (3672677)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=1385778450:avsq=on:i=17627:add=on:amm=off_2850 on theBenchmark for (2850ds/17627Mi) % 177.03/25.29 % (3672308)Instruction limit reached! % 177.03/25.29 % (3672308)------------------------------ % 177.03/25.29 % (3672308)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 177.03/25.29 % (3672308)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 177.03/25.29 % (3672308)CaDiCaL version: 2.1.3 % 177.03/25.29 % (3672308)Termination reason: Instruction limit % 177.03/25.29 % (3672308)Termination phase: Saturation % 177.03/25.29 % (3672308)Time elapsed: 13.072 s % 177.03/25.29 % (3672308)Peak memory usage: 50 MB % 177.03/25.29 % (3672308)Instructions burned: 29342 (million) % 177.03/25.29 % (3672679)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=2371989358:s2a=on:i=53295_2841 on theBenchmark for (2841ds/53295Mi) % 177.03/25.29 % (3672324)Instruction limit reached! % 177.03/25.29 % (3672324)------------------------------ % 177.03/25.29 % (3672324)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 177.03/25.29 % (3672324)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 177.03/25.29 % (3672324)CaDiCaL version: 2.1.3 % 177.03/25.29 % (3672324)Termination reason: Instruction limit % 177.03/25.29 % (3672324)Termination phase: Saturation % 177.03/25.29 % (3672324)Time elapsed: 10.025 s % 177.03/25.29 % (3672324)Peak memory usage: 96 MB % 177.03/25.29 % (3672324)Instructions burned: 20140 (million) % 177.03/25.29 % (3672681)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=2126016948:i=26857:ins=20_2838 on theBenchmark for (2838ds/26857Mi) % 177.03/25.29 % (3672681)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 177.03/25.29 % (3672681)Terminated due to inappropriate strategy. % 177.03/25.29 % (3672681)------------------------------ % 177.03/25.29 % (3672681)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 177.03/25.29 % (3672681)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 177.03/25.29 % (3672681)CaDiCaL version: 2.1.3 % 177.03/25.29 % (3672681)Termination reason: Inappropriate % 177.03/25.29 % (3672681)Time elapsed: 0.029 s % 177.03/25.29 % (3672681)Peak memory usage: 12 MB % 177.03/25.29 % (3672681)Instructions burned: 65 (million) % 177.03/25.29 % (3672681)------------------------------ % 177.03/25.29 % (3672681)------------------------------ % 177.03/25.29 % (3672683)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=118094738:i=28120:bs=on:fsr=off_2837 on theBenchmark for (2837ds/28120Mi) % 177.03/25.29 % (3672330)Instruction limit reached! % 177.03/25.29 % (3672330)------------------------------ % 177.03/25.29 % (3672330)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 177.03/25.29 % (3672330)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 177.03/25.29 % (3672330)CaDiCaL version: 2.1.3 % 177.03/25.29 % (3672330)Termination reason: Instruction limit % 177.03/25.29 % (3672330)Termination phase: Saturation % 177.03/25.29 % (3672330)Time elapsed: 7.949 s % 177.03/25.29 % (3672330)Peak memory usage: 95 MB % 177.03/25.29 % (3672330)Instructions burned: 14135 (million) % 177.03/25.29 % (3672685)fmb+10_1_sil=256000:fmbss=7:random_seed=2667424399:fmbsr=1.6:i=182295_2821 on theBenchmark for (2821ds/182295Mi) % 177.03/25.29 % (3672685)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 177.03/25.29 % (3672685)Terminated due to inappropriate strategy. % 177.03/25.29 % (3672685)------------------------------ % 177.03/25.29 % (3672685)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 177.03/25.29 % (3672685)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 177.03/25.29 % (3672685)CaDiCaL version: 2.1.3 % 177.03/25.29 % (3672685)Termination reason: Inappropriate % 177.03/25.29 % (3672685)Time elapsed: 0.030 s % 177.03/25.29 % (3672685)Peak memory usage: 12 MB % 177.03/25.29 % (3672685)Instructions burned: 65 (million) % 177.03/25.29 % (3672685)------------------------------ % 177.03/25.29 % (3672685)------------------------------ % 177.03/25.29 % (3672687)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=2098350150:i=44625:gsp=on_2820 on theBenchmark for (2820ds/44625Mi) % 190.86/27.19 % (3672687)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 190.86/27.19 % (3672687)Terminated due to inappropriate strategy. % 190.86/27.19 % (3672687)------------------------------ % 190.86/27.19 % (3672687)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 190.86/27.19 % (3672687)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 190.86/27.19 % (3672687)CaDiCaL version: 2.1.3 % 190.86/27.19 % (3672687)Termination reason: Inappropriate % 190.86/27.19 % (3672687)Time elapsed: 0.030 s % 190.86/27.19 % (3672687)Peak memory usage: 12 MB % 190.86/27.19 % (3672687)Instructions burned: 65 (million) % 190.86/27.19 % (3672687)------------------------------ % 190.86/27.19 % (3672687)------------------------------ % 190.86/27.19 % (3672689)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=913396849:i=160505_2820 on theBenchmark for (2820ds/160505Mi) % 190.86/27.19 % (3672689)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 190.86/27.19 % (3672689)Terminated due to inappropriate strategy. % 190.86/27.19 % (3672689)------------------------------ % 190.86/27.19 % (3672689)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 190.86/27.19 % (3672689)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 190.86/27.19 % (3672689)CaDiCaL version: 2.1.3 % 190.86/27.19 % (3672689)Termination reason: Inappropriate % 190.86/27.19 % (3672689)Time elapsed: 0.029 s % 190.86/27.19 % (3672689)Peak memory usage: 12 MB % 190.86/27.19 % (3672689)Instructions burned: 65 (million) % 190.86/27.19 % (3672689)------------------------------ % 190.86/27.19 % (3672689)------------------------------ % 190.86/27.19 % (3672691)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=4137651091:fmbsr=1.3:i=225729_2819 on theBenchmark for (2819ds/225729Mi) % 190.86/27.19 % (3672691)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 190.86/27.19 % (3672691)Terminated due to inappropriate strategy. % 190.86/27.19 % (3672691)------------------------------ % 190.86/27.19 % (3672691)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 190.86/27.19 % (3672691)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 190.86/27.19 % (3672691)CaDiCaL version: 2.1.3 % 190.86/27.19 % (3672691)Termination reason: Inappropriate % 190.86/27.19 % (3672691)Time elapsed: 0.029 s % 190.86/27.19 % (3672691)Peak memory usage: 12 MB % 190.86/27.19 % (3672691)Instructions burned: 65 (million) % 190.86/27.19 % (3672691)------------------------------ % 190.86/27.19 % (3672691)------------------------------ % 190.86/27.19 % (3672693)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=2013527792:fmbsr=2:i=185024:ins=7_2819 on theBenchmark for (2819ds/185024Mi) % 190.86/27.19 % (3672693)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 190.86/27.19 % (3672693)Terminated due to inappropriate strategy. % 190.86/27.19 % (3672693)------------------------------ % 190.86/27.19 % (3672693)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 190.86/27.19 % (3672693)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 190.86/27.19 % (3672693)CaDiCaL version: 2.1.3 % 190.86/27.19 % (3672693)Termination reason: Inappropriate % 190.86/27.19 % (3672693)Time elapsed: 0.029 s % 190.86/27.19 % (3672693)Peak memory usage: 12 MB % 190.86/27.19 % (3672693)Instructions burned: 65 (million) % 190.86/27.19 % (3672693)------------------------------ % 190.86/27.19 % (3672693)------------------------------ % 190.86/27.19 % (3672695)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=3351287382:rtra=on_2818 on theBenchmark for (2818ds/0Mi) % 190.86/27.19 % (3672695)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 190.86/27.19 % (3672695)Terminated due to inappropriate strategy. % 190.86/27.19 % (3672695)------------------------------ % 190.86/27.19 % (3672695)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 190.86/27.19 % (3672695)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 190.86/27.19 % (3672695)CaDiCaL version: 2.1.3 % 190.86/27.19 % (3672695)Termination reason: Inappropriate % 190.86/27.19 % (3672695)Time elapsed: 0.034 s % 190.86/27.19 % (3672695)Peak memory usage: 12 MB % 190.86/27.19 % (3672695)Instructions burned: 70 (million) % 190.86/27.19 % (3672695)------------------------------ % 190.86/27.19 % (3672695)------------------------------ % 190.86/27.19 % (3672697)% WARNING: option uhcvi not known. % 190.86/27.19 % (3672697)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=22175115:i=271062:add=off:rtra=on:rawr=on_2818 on theBenchmark for (2818ds/271062Mi) % 214.73/30.50 % (3672341)Instruction limit reached! % 214.73/30.50 % (3672341)------------------------------ % 214.73/30.50 % (3672341)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 214.73/30.50 % (3672341)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 214.73/30.50 % (3672341)CaDiCaL version: 2.1.3 % 214.73/30.50 % (3672341)Termination reason: Instruction limit % 214.73/30.50 % (3672341)Termination phase: Saturation % 214.73/30.50 % (3672341)Time elapsed: 6.742 s % 214.73/30.50 % (3672341)Peak memory usage: 19 MB % 214.73/30.50 % (3672341)Instructions burned: 15852 (million) % 214.73/30.50 % (3672699)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=4258845711:i=176048:add=on:rtra=on:rawr=on_2800 on theBenchmark for (2800ds/176048Mi) % 214.73/30.50 % (3672677)Instruction limit reached! % 214.73/30.50 % (3672677)------------------------------ % 214.73/30.50 % (3672677)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 214.73/30.50 % (3672677)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 214.73/30.50 % (3672677)CaDiCaL version: 2.1.3 % 214.73/30.50 % (3672677)Termination reason: Instruction limit % 214.73/30.50 % (3672677)Termination phase: Saturation % 214.73/30.50 % (3672677)Time elapsed: 9.339 s % 214.73/30.50 % (3672677)Peak memory usage: 194 MB % 214.73/30.50 % (3672677)Instructions burned: 17627 (million) % 214.73/30.50 % (3672701)dis+10_1_sil=32000:si=on:sp=arity:random_seed=2330235211:i=206:fgj=on:rtra=on_2756 on theBenchmark for (2756ds/206Mi) % 214.73/30.50 % (3672701)Instruction limit reached! % 214.73/30.50 % (3672701)------------------------------ % 214.73/30.50 % (3672701)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 214.73/30.50 % (3672701)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 214.73/30.50 % (3672701)CaDiCaL version: 2.1.3 % 214.73/30.50 % (3672701)Termination reason: Instruction limit % 214.73/30.50 % (3672701)Termination phase: Saturation % 214.73/30.50 % (3672701)Time elapsed: 0.118 s % 214.73/30.50 % (3672701)Peak memory usage: 15 MB % 214.73/30.50 % (3672701)Instructions burned: 207 (million) % 214.73/30.50 % (3672703)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=1903528534:i=232:rtra=on_2755 on theBenchmark for (2755ds/232Mi) % 214.73/30.50 % (3672703)Instruction limit reached! % 214.73/30.50 % (3672703)------------------------------ % 214.73/30.50 % (3672703)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 214.73/30.50 % (3672703)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 214.73/30.50 % (3672703)CaDiCaL version: 2.1.3 % 214.73/30.50 % (3672703)Termination reason: Instruction limit % 214.73/30.50 % (3672703)Termination phase: Saturation % 214.73/30.50 % (3672703)Time elapsed: 0.135 s % 214.73/30.50 % (3672703)Peak memory usage: 15 MB % 214.73/30.50 % (3672703)Instructions burned: 233 (million) % 214.73/30.50 % (3672705)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=1894514405:i=262:rtra=on_2753 on theBenchmark for (2753ds/262Mi) % 214.73/30.50 % (3672705)Instruction limit reached! % 214.73/30.50 % (3672705)------------------------------ % 214.73/30.50 % (3672705)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 214.73/30.50 % (3672705)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 214.73/30.50 % (3672705)CaDiCaL version: 2.1.3 % 214.73/30.50 % (3672705)Termination reason: Instruction limit % 214.73/30.50 % (3672705)Termination phase: Saturation % 214.73/30.50 % (3672705)Time elapsed: 0.151 s % 214.73/30.50 % (3672705)Peak memory usage: 16 MB % 214.73/30.50 % (3672705)Instructions burned: 263 (million) % 214.73/30.50 % (3672707)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=1554748568:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2751 on theBenchmark for (2751ds/318Mi) % 214.73/30.50 % (3672707)Instruction limit reached! % 214.73/30.50 % (3672707)------------------------------ % 214.73/30.50 % (3672707)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 214.73/30.50 % (3672707)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 214.73/30.50 % (3672707)CaDiCaL version: 2.1.3 % 214.73/30.50 % (3672707)Termination reason: Instruction limit % 214.73/30.50 % (3672707)Termination phase: Saturation % 214.73/30.50 % (3672707)Time elapsed: 0.196 s % 214.73/30.50 % (3672707)Peak memory usage: 16 MB % 214.73/30.50 % (3672707)Instructions burned: 318 (million) % 214.73/30.50 % (3672709)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=2731181500:i=1428:nm=2:rtra=on_2749 on theBenchmark for (2749ds/1428Mi) % 229.64/32.66 % (3672709)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 229.64/32.66 % (3672709)Terminated due to inappropriate strategy. % 229.64/32.66 % (3672709)------------------------------ % 229.64/32.66 % (3672709)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 229.64/32.66 % (3672709)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 229.64/32.66 % (3672709)CaDiCaL version: 2.1.3 % 229.64/32.66 % (3672709)Termination reason: Inappropriate % 229.64/32.66 % (3672709)Time elapsed: 0.033 s % 229.64/32.66 % (3672709)Peak memory usage: 12 MB % 229.64/32.66 % (3672709)Instructions burned: 70 (million) % 229.64/32.66 % (3672709)------------------------------ % 229.64/32.66 % (3672709)------------------------------ % 229.64/32.66 % (3672711)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=3240269484:i=262:bd=preordered:rtra=on:fsd=on_2749 on theBenchmark for (2749ds/262Mi) % 229.64/32.66 % (3672711)Instruction limit reached! % 229.64/32.66 % (3672711)------------------------------ % 229.64/32.66 % (3672711)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 229.64/32.66 % (3672711)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 229.64/32.66 % (3672711)CaDiCaL version: 2.1.3 % 229.64/32.66 % (3672711)Termination reason: Instruction limit % 229.64/32.66 % (3672711)Termination phase: Saturation % 229.64/32.66 % (3672711)Time elapsed: 0.165 s % 229.64/32.66 % (3672711)Peak memory usage: 16 MB % 229.64/32.66 % (3672711)Instructions burned: 262 (million) % 229.64/32.66 % (3672713)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=2879367946:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2747 on theBenchmark for (2747ds/1368Mi) % 229.64/32.66 % (3672713)Instruction limit reached! % 229.64/32.66 % (3672713)------------------------------ % 229.64/32.66 % (3672713)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 229.64/32.66 % (3672713)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 229.64/32.66 % (3672713)CaDiCaL version: 2.1.3 % 229.64/32.66 % (3672713)Termination reason: Instruction limit % 229.64/32.66 % (3672713)Termination phase: Saturation % 229.64/32.66 % (3672713)Time elapsed: 0.801 s % 229.64/32.66 % (3672713)Peak memory usage: 22 MB % 229.64/32.66 % (3672713)Instructions burned: 1369 (million) % 229.64/32.66 % (3672715)ott-21_1_sil=16000:si=on:fs=off:random_seed=2119354880:i=360:av=off:fsr=off:rtra=on_2738 on theBenchmark for (2738ds/360Mi) % 229.64/32.66 % (3672715)Instruction limit reached! % 229.64/32.66 % (3672715)------------------------------ % 229.64/32.66 % (3672715)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 229.64/32.66 % (3672715)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 229.64/32.66 % (3672715)CaDiCaL version: 2.1.3 % 229.64/32.66 % (3672715)Termination reason: Instruction limit % 229.64/32.66 % (3672715)Termination phase: Saturation % 229.64/32.66 % (3672715)Time elapsed: 0.174 s % 229.64/32.66 % (3672715)Peak memory usage: 15 MB % 229.64/32.66 % (3672715)Instructions burned: 361 (million) % 229.64/32.66 % (3672717)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1565081771:i=954:bd=all:rtra=on_2736 on theBenchmark for (2736ds/954Mi) % 229.64/32.66 % (3672717)Instruction limit reached! % 229.64/32.66 % (3672717)------------------------------ % 229.64/32.66 % (3672717)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 229.64/32.66 % (3672717)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 229.64/32.66 % (3672717)CaDiCaL version: 2.1.3 % 229.64/32.66 % (3672717)Termination reason: Instruction limit % 229.64/32.66 % (3672717)Termination phase: Saturation % 229.64/32.66 % (3672717)Time elapsed: 0.580 s % 229.64/32.66 % (3672717)Peak memory usage: 19 MB % 229.64/32.66 % (3672717)Instructions burned: 956 (million) % 229.64/32.66 % (3672719)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=4260464886:fmbsr=1.3:i=1730:ins=25:rtra=on_2730 on theBenchmark for (2730ds/1730Mi) % 229.64/32.66 % (3672719)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 229.64/32.66 % (3672719)Terminated due to inappropriate strategy. % 229.64/32.66 % (3672719)------------------------------ % 229.64/32.66 % (3672719)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 229.64/32.66 % (3672719)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 229.64/32.66 % (3672719)CaDiCaL version: 2.1.3 % 229.64/32.66 % (3672719)Termination reason: Inappropriate % 282.46/40.08 % (3672719)Time elapsed: 0.033 s % 282.46/40.08 % (3672719)Peak memory usage: 12 MB % 282.46/40.08 % (3672719)Instructions burned: 70 (million) % 282.46/40.08 % (3672719)------------------------------ % 282.46/40.08 % (3672719)------------------------------ % 282.46/40.08 % (3672721)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=4279896417:i=2358:rtra=on_2730 on theBenchmark for (2730ds/2358Mi) % 282.46/40.08 % (3672721)Instruction limit reached! % 282.46/40.08 % (3672721)------------------------------ % 282.46/40.08 % (3672721)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 282.46/40.08 % (3672721)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 282.46/40.08 % (3672721)CaDiCaL version: 2.1.3 % 282.46/40.08 % (3672721)Termination reason: Instruction limit % 282.46/40.08 % (3672721)Termination phase: Saturation % 282.46/40.08 % (3672721)Time elapsed: 1.302 s % 282.46/40.08 % (3672721)Peak memory usage: 30 MB % 282.46/40.08 % (3672721)Instructions burned: 2358 (million) % 282.46/40.08 % (3672781)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=492544661:i=1778:ins=1:rtra=on_2717 on theBenchmark for (2717ds/1778Mi) % 282.46/40.08 % (3672781)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 282.46/40.08 % (3672781)Terminated due to inappropriate strategy. % 282.46/40.08 % (3672781)------------------------------ % 282.46/40.08 % (3672781)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 282.46/40.08 % (3672781)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 282.46/40.08 % (3672781)CaDiCaL version: 2.1.3 % 282.46/40.08 % (3672781)Termination reason: Inappropriate % 282.46/40.08 % (3672781)Time elapsed: 0.034 s % 282.46/40.08 % (3672781)Peak memory usage: 12 MB % 282.46/40.08 % (3672781)Instructions burned: 70 (million) % 282.46/40.08 % (3672781)------------------------------ % 282.46/40.08 % (3672781)------------------------------ % 282.46/40.08 % (3672812)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=1430144611:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2716 on theBenchmark for (2716ds/1384Mi) % 282.46/40.08 % (3672812)Instruction limit reached! % 282.46/40.08 % (3672812)------------------------------ % 282.46/40.08 % (3672812)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 282.46/40.08 % (3672812)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 282.46/40.08 % (3672812)CaDiCaL version: 2.1.3 % 282.46/40.08 % (3672812)Termination reason: Instruction limit % 282.46/40.08 % (3672812)Termination phase: Saturation % 282.46/40.08 % (3672812)Time elapsed: 0.866 s % 282.46/40.08 % (3672812)Peak memory usage: 26 MB % 282.46/40.08 % (3672812)Instructions burned: 1386 (million) % 282.46/40.08 % (3673015)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=3516485227:i=1758:kws=inv_precedence:fsr=off:rtra=on_2707 on theBenchmark for (2707ds/1758Mi) % 282.46/40.08 % (3672683)Instruction limit reached! % 282.46/40.08 % (3672683)------------------------------ % 282.46/40.08 % (3672683)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 282.46/40.08 % (3672683)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 282.46/40.08 % (3672683)CaDiCaL version: 2.1.3 % 282.46/40.08 % (3672683)Termination reason: Instruction limit % 282.46/40.08 % (3672683)Termination phase: Saturation % 282.46/40.08 % (3672683)Time elapsed: 13.975 s % 282.46/40.08 % (3672683)Peak memory usage: 44 MB % 282.46/40.08 % (3672683)Instructions burned: 28123 (million) % 282.46/40.08 % (3673072)fmb+10_1_sil=64000:si=on:random_seed=614875903:i=44122:nm=2:rtra=on:gsp=on_2697 on theBenchmark for (2697ds/44122Mi) % 282.46/40.08 % (3673015)Instruction limit reached! % 282.46/40.08 % (3673015)------------------------------ % 282.46/40.08 % (3673015)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 282.46/40.08 % (3673015)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 282.46/40.08 % (3673015)CaDiCaL version: 2.1.3 % 282.46/40.08 % (3673015)Termination reason: Instruction limit % 282.46/40.08 % (3673015)Termination phase: Saturation % 282.46/40.08 % (3673015)Time elapsed: 0.985 s % 282.46/40.08 % (3673015)Peak memory usage: 24 MB % 282.46/40.08 % (3673015)Instructions burned: 1758 (million) % 282.46/40.08 % (3673074)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=2427648571:i=19030:nm=5:rtra=on_2697 on theBenchmark for (2697ds/19030Mi) % 282.46/40.08 % (3673072)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 282.46/40.08 % (3673072)Terminated due to inappropriate strategy. % 300.66/42.63 % (3673072)------------------------------ % 300.66/42.63 % (3673072)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.66/42.63 % (3673072)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.66/42.63 % (3673072)CaDiCaL version: 2.1.3 % 300.66/42.63 % (3673072)Termination reason: Inappropriate % 300.66/42.63 % (3673072)Time elapsed: 0.034 s % 300.66/42.63 % (3673072)Peak memory usage: 12 MB % 300.66/42.63 % (3673072)Instructions burned: 70 (million) % 300.66/42.63 % (3673072)------------------------------ % 300.66/42.63 % (3673072)------------------------------ % 300.66/42.63 % (3673076)fmb+10_1_sil=64000:sas=cadical:si=on:fmbss=8:random_seed=1403471259:fmbsr=1.7:i=1840:rtra=on_2697 on theBenchmark for (2697ds/1840Mi) % 300.66/42.63 % (3673074)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 300.66/42.63 % (3673074)Terminated due to inappropriate strategy. % 300.66/42.63 % (3673074)------------------------------ % 300.66/42.63 % (3673074)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.66/42.63 % (3673074)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.66/42.63 % (3673074)CaDiCaL version: 2.1.3 % 300.66/42.63 % (3673074)Termination reason: Inappropriate % 300.66/42.63 % (3673074)Time elapsed: 0.034 s % 300.66/42.63 % (3673074)Peak memory usage: 12 MB % 300.66/42.63 % (3673074)Instructions burned: 70 (million) % 300.66/42.63 % (3673074)------------------------------ % 300.66/42.63 % (3673074)------------------------------ % 300.66/42.63 % (3673078)dis-4_1_sil=16000:drc=ordering:si=on:sp=const_frequency:sac=on:newcnf=on:random_seed=4886040:i=10262:rtra=on_2697 on theBenchmark for (2697ds/10262Mi) % 300.66/42.63 % (3673076)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 300.66/42.63 % (3673076)Terminated due to inappropriate strategy. % 300.66/42.63 % (3673076)------------------------------ % 300.66/42.63 % (3673076)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.66/42.63 % (3673076)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.66/42.63 % (3673076)CaDiCaL version: 2.1.3 % 300.66/42.63 % (3673076)Termination reason: Inappropriate % 300.66/42.63 % (3673076)Time elapsed: 0.034 s % 300.66/42.63 % (3673076)Peak memory usage: 12 MB % 300.66/42.63 % (3673076)Instructions burned: 70 (million) % 300.66/42.63 % (3673076)------------------------------ % 300.66/42.63 % (3673076)------------------------------ % 300.66/42.63 % (3673080)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:si=on:sp=arity:spb=units:lsd=10:nwc=3:random_seed=54151147:i=2944:ins=7:rtra=on:fdi=8:gsp=on_2696 on theBenchmark for (2696ds/2944Mi) % 300.66/42.63 % (3673080)Instruction limit reached! % 300.66/42.63 % (3673080)------------------------------ % 300.66/42.63 % (3673080)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.66/42.63 % (3673080)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.66/42.63 % (3673080)CaDiCaL version: 2.1.3 % 300.66/42.63 % (3673080)Termination reason: Instruction limit % 300.66/42.63 % (3673080)Termination phase: Saturation % 300.66/42.63 % (3673080)Time elapsed: 1.967 s % 300.66/42.63 % (3673080)Peak memory usage: 43 MB % 300.66/42.63 % (3673080)Instructions burned: 2945 (million) % 300.66/42.63 % (3673082)fmb+10_1_sil=16000:sas=cadical:si=on:bce=on:fmbss=77:random_seed=620629858:i=12648:rtra=on_2676 on theBenchmark for (2676ds/12648Mi) % 300.66/42.63 % (3673082)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 300.66/42.64 % (3673082)Terminated due to inappropriate strategy. % 300.66/42.64 % (3673082)------------------------------ % 300.66/42.64 % (3673082)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.66/42.64 % (3673082)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.66/42.64 % (3673082)CaDiCaL version: 2.1.3 % 300.66/42.64 % (3673082)Termination reason: Inappropriate % 300.66/42.64 % (3673082)Time elapsed: 0.034 s % 300.66/42.64 % (3673082)Peak memory usage: 12 MB % 300.66/42.64 % (3673082)Instructions burned: 70 (million) % 300.66/42.64 % (3673082)------------------------------ % 300.66/42.64 % (3673082)------------------------------ % 300.66/42.64 % (3673084)fmb+10_1_fmbas=function:sil=32000:sas=cadical:si=on:fmbss=16:random_seed=568302891:fmbsr=2.30978:i=4348:rtra=on_2676 on theBenchmark for (2676ds/4348Mi) % 300.66/42.64 % (3673084)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 300.66/42.64 % (3673084)Terminated due to inappropriate strategy. % 300.66/42.64 % (3673084)----------------------------- % 300.66/42.64 Terminated % 300.66/42.64 % Vampire exiting %------------------------------------------------------------------------------