%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWC483_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 : n015.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:03 PM UTC 2026 % Result : Timeout 288.73s 40.91s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWC483_1 : TPTP v9.3.1. Bugfixed v9.1.0. % 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.09/0.19 % Computer : n015.cluster.edu % 0.09/0.19 % Model : x86_64 x86_64 % 0.09/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.19 % Memory : 8046.5625MB % 0.09/0.19 % OS : Linux 6.8.0-71-generic % 0.09/0.19 % CPULimit : 300 % 0.09/0.19 % WCLimit : 300 % 0.09/0.19 % DateTime : Mon Sep 28 09:43:47 UTC 2026 % 0.09/0.20 % CPUTime : % 0.09/0.20 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.09/0.23 Running first-order model finding % 0.09/0.23 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.84/0.82 % (2507662)Will run a generic schedule for satisfiability detection. % 3.84/0.82 % (2507669)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=11387670:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 3.84/0.82 % (2507668)% WARNING: option uhcvi not known. % 3.84/0.82 % (2507667)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=334590928_2999 on theBenchmark for (2999ds/0Mi) % 3.84/0.82 % (2507668)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=4187580236:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 3.84/0.82 % (2507670)dis+10_1_sil=32000:sp=arity:random_seed=3023271427:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 3.84/0.82 % (2507673)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2977080834:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 3.84/0.82 % (2507671)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1438261914:i=116_2999 on theBenchmark for (2999ds/116Mi) % 3.84/0.82 % (2507672)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=832788329:i=131_2999 on theBenchmark for (2999ds/131Mi) % 3.84/0.82 % (2507667)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.84/0.82 % (2507667)Terminated due to inappropriate strategy. % 3.84/0.82 % (2507667)------------------------------ % 3.84/0.82 % (2507667)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.84/0.82 % (2507667)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.84/0.82 % (2507667)CaDiCaL version: 2.1.3 % 3.84/0.82 % (2507667)Termination reason: Inappropriate % 3.84/0.82 % (2507667)Time elapsed: 0.001 s % 3.84/0.82 % (2507667)Peak memory usage: 10 MB % 3.84/0.82 % (2507667)Instructions burned: 1 (million) % 3.84/0.82 % (2507667)------------------------------ % 3.84/0.82 % (2507667)------------------------------ % 3.84/0.82 % (2507681)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=4136825650:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 3.84/0.82 % (2507681)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.84/0.82 % (2507681)Terminated due to inappropriate strategy. % 3.84/0.82 % (2507681)------------------------------ % 3.84/0.82 % (2507681)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.84/0.82 % (2507681)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.84/0.82 % (2507681)CaDiCaL version: 2.1.3 % 3.84/0.82 % (2507681)Termination reason: Inappropriate % 3.84/0.82 % (2507681)Time elapsed: 0.001 s % 3.84/0.82 % (2507681)Peak memory usage: 10 MB % 3.84/0.82 % (2507681)Instructions burned: 1 (million) % 3.84/0.82 % (2507681)------------------------------ % 3.84/0.82 % (2507681)------------------------------ % 3.84/0.82 % (2507683)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1413816275:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 3.84/0.82 % (2507670)Instruction limit reached! % 3.84/0.82 % (2507670)------------------------------ % 3.84/0.82 % (2507670)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.84/0.82 % (2507670)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.84/0.82 % (2507670)CaDiCaL version: 2.1.3 % 3.84/0.82 % (2507670)Termination reason: Instruction limit % 3.84/0.82 % (2507670)Termination phase: Saturation % 3.84/0.82 % (2507670)Time elapsed: 0.064 s % 3.84/0.82 % (2507670)Peak memory usage: 12 MB % 3.84/0.82 % (2507670)Instructions burned: 104 (million) % 3.84/0.82 % (2507671)Instruction limit reached! % 3.84/0.82 % (2507671)------------------------------ % 3.84/0.82 % (2507671)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.84/0.82 % (2507671)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.84/0.82 % (2507671)CaDiCaL version: 2.1.3 % 3.84/0.82 % (2507671)Termination reason: Instruction limit % 3.84/0.82 % (2507671)Termination phase: Saturation % 3.84/0.82 % (2507671)Time elapsed: 0.070 s % 3.84/0.82 % (2507671)Peak memory usage: 12 MB % 3.84/0.82 % (2507671)Instructions burned: 116 (million) % 3.84/0.82 % (2507672)Instruction limit reached! % 3.84/0.82 % (2507672)------------------------------ % 3.84/0.82 % (2507672)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.84/0.82 % (2507672)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.84/0.82 % (2507672)CaDiCaL version: 2.1.3 % 3.84/0.82 % (2507672)Termination reason: Instruction limit % 6.37/1.14 % (2507672)Termination phase: Saturation % 6.37/1.14 % (2507672)Time elapsed: 0.079 s % 6.37/1.14 % (2507672)Peak memory usage: 13 MB % 6.37/1.14 % (2507672)Instructions burned: 131 (million) % 6.37/1.14 % (2507685)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=1486612654:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi) % 6.37/1.14 % (2507686)ott-21_1_sil=16000:fs=off:random_seed=1883793610:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 6.37/1.14 % (2507687)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=645206563:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 6.37/1.14 % (2507673)Instruction limit reached! % 6.37/1.14 % (2507673)------------------------------ % 6.37/1.14 % (2507673)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.37/1.14 % (2507673)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.37/1.14 % (2507673)CaDiCaL version: 2.1.3 % 6.37/1.14 % (2507673)Termination reason: Instruction limit % 6.37/1.14 % (2507673)Termination phase: Saturation % 6.37/1.14 % (2507673)Time elapsed: 0.108 s % 6.37/1.14 % (2507673)Peak memory usage: 13 MB % 6.37/1.14 % (2507673)Instructions burned: 160 (million) % 6.37/1.14 % (2507691)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2137025937:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 6.37/1.14 % (2507683)Instruction limit reached! % 6.37/1.14 % (2507683)------------------------------ % 6.37/1.14 % (2507683)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.37/1.14 % (2507683)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.37/1.14 % (2507683)CaDiCaL version: 2.1.3 % 6.37/1.14 % (2507683)Termination reason: Instruction limit % 6.37/1.14 % (2507683)Termination phase: Saturation % 6.37/1.14 % (2507683)Time elapsed: 0.086 s % 6.37/1.14 % (2507683)Peak memory usage: 12 MB % 6.37/1.14 % (2507683)Instructions burned: 131 (million) % 6.37/1.14 % (2507691)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 6.37/1.14 % (2507691)Terminated due to inappropriate strategy. % 6.37/1.14 % (2507691)------------------------------ % 6.37/1.14 % (2507691)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.37/1.14 % (2507691)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.37/1.14 % (2507691)CaDiCaL version: 2.1.3 % 6.37/1.14 % (2507691)Termination reason: Inappropriate % 6.37/1.14 % (2507691)Time elapsed: 0.001 s % 6.37/1.14 % (2507691)Peak memory usage: 10 MB % 6.37/1.14 % (2507691)Instructions burned: 1 (million) % 6.37/1.14 % (2507691)------------------------------ % 6.37/1.14 % (2507691)------------------------------ % 6.37/1.14 % (2507693)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=367101618:i=1179_2998 on theBenchmark for (2998ds/1179Mi) % 6.37/1.14 % (2507694)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2263648647:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi) % 6.37/1.14 % (2507694)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 6.37/1.14 % (2507694)Terminated due to inappropriate strategy. % 6.37/1.14 % (2507694)------------------------------ % 6.37/1.14 % (2507694)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.37/1.14 % (2507694)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.37/1.14 % (2507694)CaDiCaL version: 2.1.3 % 6.37/1.14 % (2507694)Termination reason: Inappropriate % 6.37/1.14 % (2507694)Time elapsed: 0.001 s % 6.37/1.14 % (2507694)Peak memory usage: 10 MB % 6.37/1.14 % (2507694)Instructions burned: 1 (million) % 6.37/1.14 % (2507694)------------------------------ % 6.37/1.14 % (2507694)------------------------------ % 6.37/1.14 % (2507697)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=1134412099: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) % 6.37/1.14 % (2507686)Instruction limit reached! % 6.37/1.14 % (2507686)------------------------------ % 6.37/1.14 % (2507686)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.37/1.14 % (2507686)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.37/1.14 % (2507686)CaDiCaL version: 2.1.3 % 6.37/1.14 % (2507686)Termination reason: Instruction limit % 6.37/1.14 % (2507686)Termination phase: Saturation % 22.07/3.43 % (2507686)Time elapsed: 0.079 s % 22.07/3.43 % (2507686)Peak memory usage: 12 MB % 22.07/3.43 % (2507686)Instructions burned: 180 (million) % 22.07/3.43 % (2507699)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2718713779:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi) % 22.07/3.43 % (2507687)Instruction limit reached! % 22.07/3.43 % (2507687)------------------------------ % 22.07/3.43 % (2507687)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.07/3.43 % (2507687)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.07/3.43 % (2507687)CaDiCaL version: 2.1.3 % 22.07/3.43 % (2507687)Termination reason: Instruction limit % 22.07/3.43 % (2507687)Termination phase: Saturation % 22.07/3.43 % (2507687)Time elapsed: 0.287 s % 22.07/3.43 % (2507687)Peak memory usage: 14 MB % 22.07/3.43 % (2507687)Instructions burned: 478 (million) % 22.07/3.43 % (2507701)fmb+10_1_sil=64000:random_seed=3735683758:i=22061:nm=2:gsp=on_2995 on theBenchmark for (2995ds/22061Mi) % 22.07/3.43 % (2507701)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 22.07/3.43 % (2507701)Terminated due to inappropriate strategy. % 22.07/3.43 % (2507701)------------------------------ % 22.07/3.43 % (2507701)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.07/3.43 % (2507701)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.07/3.43 % (2507701)CaDiCaL version: 2.1.3 % 22.07/3.43 % (2507701)Termination reason: Inappropriate % 22.07/3.43 % (2507701)Time elapsed: 0.001 s % 22.07/3.43 % (2507701)Peak memory usage: 10 MB % 22.07/3.43 % (2507701)Instructions burned: 1 (million) % 22.07/3.43 % (2507701)------------------------------ % 22.07/3.43 % (2507701)------------------------------ % 22.07/3.43 % (2507703)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1138096169:i=9515:nm=5_2995 on theBenchmark for (2995ds/9515Mi) % 22.07/3.43 % (2507703)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 22.07/3.43 % (2507703)Terminated due to inappropriate strategy. % 22.07/3.43 % (2507703)------------------------------ % 22.07/3.43 % (2507703)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.07/3.43 % (2507703)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.07/3.43 % (2507703)CaDiCaL version: 2.1.3 % 22.07/3.43 % (2507703)Termination reason: Inappropriate % 22.07/3.43 % (2507703)Time elapsed: 0.001 s % 22.07/3.43 % (2507703)Peak memory usage: 10 MB % 22.07/3.43 % (2507703)Instructions burned: 1 (million) % 22.07/3.43 % (2507703)------------------------------ % 22.07/3.43 % (2507703)------------------------------ % 22.07/3.43 % (2507685)Instruction limit reached! % 22.07/3.43 % (2507685)------------------------------ % 22.07/3.43 % (2507685)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.07/3.43 % (2507685)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.07/3.43 % (2507685)CaDiCaL version: 2.1.3 % 22.07/3.43 % (2507685)Termination reason: Instruction limit % 22.07/3.43 % (2507685)Termination phase: Saturation % 22.07/3.43 % (2507685)Time elapsed: 0.356 s % 22.07/3.43 % (2507685)Peak memory usage: 17 MB % 22.07/3.43 % (2507685)Instructions burned: 685 (million) % 22.07/3.43 % (2507705)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1248858341:fmbsr=1.7:i=920_2995 on theBenchmark for (2995ds/920Mi) % 22.07/3.43 % (2507705)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 22.07/3.43 % (2507705)Terminated due to inappropriate strategy. % 22.07/3.43 % (2507705)------------------------------ % 22.07/3.43 % (2507705)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.07/3.43 % (2507705)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.07/3.43 % (2507705)CaDiCaL version: 2.1.3 % 22.07/3.43 % (2507705)Termination reason: Inappropriate % 22.07/3.43 % (2507705)Time elapsed: 0.001 s % 22.07/3.43 % (2507705)Peak memory usage: 10 MB % 22.07/3.43 % (2507705)Instructions burned: 1 (million) % 22.07/3.43 % (2507705)------------------------------ % 22.07/3.43 % (2507705)------------------------------ % 22.07/3.43 % (2507706)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1771518288:i=5131_2995 on theBenchmark for (2995ds/5131Mi) % 22.07/3.43 % (2507708)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2437083627:i=1472:ins=7:fdi=8:gsp=on_2995 on theBenchmark for (2995ds/1472Mi) % 22.07/3.43 % (2507697)Instruction limit reached! % 22.07/3.43 % (2507697)------------------------------ % 31.73/4.87 % (2507697)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 31.73/4.87 % (2507697)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.73/4.87 % (2507697)CaDiCaL version: 2.1.3 % 31.73/4.87 % (2507697)Termination reason: Instruction limit % 31.73/4.87 % (2507697)Termination phase: Saturation % 31.73/4.87 % (2507697)Time elapsed: 0.383 s % 31.73/4.87 % (2507697)Peak memory usage: 18 MB % 31.73/4.87 % (2507697)Instructions burned: 692 (million) % 31.73/4.87 % (2507711)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3377712226:i=6324_2994 on theBenchmark for (2994ds/6324Mi) % 31.73/4.87 % (2507711)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 31.73/4.87 % (2507711)Terminated due to inappropriate strategy. % 31.73/4.87 % (2507711)------------------------------ % 31.73/4.87 % (2507711)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 31.73/4.87 % (2507711)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.73/4.87 % (2507711)CaDiCaL version: 2.1.3 % 31.73/4.87 % (2507711)Termination reason: Inappropriate % 31.73/4.87 % (2507711)Time elapsed: 0.001 s % 31.73/4.87 % (2507711)Peak memory usage: 10 MB % 31.73/4.87 % (2507711)Instructions burned: 1 (million) % 31.73/4.87 % (2507711)------------------------------ % 31.73/4.87 % (2507711)------------------------------ % 31.73/4.87 % (2507713)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=3033354882:fmbsr=2.30978:i=2174_2993 on theBenchmark for (2993ds/2174Mi) % 31.73/4.87 % (2507713)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 31.73/4.87 % (2507713)Terminated due to inappropriate strategy. % 31.73/4.87 % (2507713)------------------------------ % 31.73/4.87 % (2507713)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 31.73/4.87 % (2507713)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.73/4.87 % (2507713)CaDiCaL version: 2.1.3 % 31.73/4.87 % (2507713)Termination reason: Inappropriate % 31.73/4.87 % (2507713)Time elapsed: 0.001 s % 31.73/4.87 % (2507713)Peak memory usage: 10 MB % 31.73/4.87 % (2507713)Instructions burned: 1 (million) % 31.73/4.87 % (2507713)------------------------------ % 31.73/4.87 % (2507713)------------------------------ % 31.73/4.87 % (2507715)ott-2_1_sil=16000:newcnf=on:random_seed=2378427918:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2993 on theBenchmark for (2993ds/869Mi) % 31.73/4.87 % (2507699)Instruction limit reached! % 31.73/4.87 % (2507699)------------------------------ % 31.73/4.87 % (2507699)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 31.73/4.87 % (2507699)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.73/4.87 % (2507699)CaDiCaL version: 2.1.3 % 31.73/4.87 % (2507699)Termination reason: Instruction limit % 31.73/4.87 % (2507699)Termination phase: Saturation % 31.73/4.87 % (2507699)Time elapsed: 0.480 s % 31.73/4.87 % (2507699)Peak memory usage: 19 MB % 31.73/4.87 % (2507699)Instructions burned: 880 (million) % 31.73/4.87 % (2507717)ott+10_1_sil=32000:tgt=ground:random_seed=3514604110:i=5114:av=off_2992 on theBenchmark for (2992ds/5114Mi) % 31.73/4.87 % (2507693)Instruction limit reached! % 31.73/4.87 % (2507693)------------------------------ % 31.73/4.87 % (2507693)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 31.73/4.87 % (2507693)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.73/4.87 % (2507693)CaDiCaL version: 2.1.3 % 31.73/4.87 % (2507693)Termination reason: Instruction limit % 31.73/4.87 % (2507693)Termination phase: Saturation % 31.73/4.87 % (2507693)Time elapsed: 0.704 s % 31.73/4.87 % (2507693)Peak memory usage: 19 MB % 31.73/4.87 % (2507693)Instructions burned: 1180 (million) % 31.73/4.87 % (2507719)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=1485731575:i=54282_2991 on theBenchmark for (2991ds/54282Mi) % 31.73/4.87 % (2507719)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 31.73/4.87 % (2507719)Terminated due to inappropriate strategy. % 31.73/4.87 % (2507719)------------------------------ % 31.73/4.87 % (2507719)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 31.73/4.87 % (2507719)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.73/4.87 % (2507719)CaDiCaL version: 2.1.3 % 31.73/4.87 % (2507719)Termination reason: Inappropriate % 31.73/4.87 % (2507719)Time elapsed: 0.001 s % 31.73/4.87 % (2507719)Peak memory usage: 10 MB % 31.73/4.87 % (2507719)Instructions burned: 1 (million) % 113.33/16.29 % (2507719)------------------------------ % 113.33/16.29 % (2507719)------------------------------ % 113.33/16.29 % (2507721)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=674939290:i=3512:aac=none_2990 on theBenchmark for (2990ds/3512Mi) % 113.33/16.29 % (2507715)Instruction limit reached! % 113.33/16.29 % (2507715)------------------------------ % 113.33/16.29 % (2507715)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 113.33/16.29 % (2507715)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 113.33/16.29 % (2507715)CaDiCaL version: 2.1.3 % 113.33/16.29 % (2507715)Termination reason: Instruction limit % 113.33/16.29 % (2507715)Termination phase: Saturation % 113.33/16.29 % (2507715)Time elapsed: 0.502 s % 113.33/16.29 % (2507715)Peak memory usage: 15 MB % 113.33/16.29 % (2507715)Instructions burned: 870 (million) % 113.33/16.29 % (2507723)dis+21_1_sil=32000:sas=cadical:random_seed=2117217219:i=3773:amm=off_2988 on theBenchmark for (2988ds/3773Mi) % 113.33/16.29 % (2507708)Instruction limit reached! % 113.33/16.29 % (2507708)------------------------------ % 113.33/16.29 % (2507708)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 113.33/16.29 % (2507708)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 113.33/16.29 % (2507708)CaDiCaL version: 2.1.3 % 113.33/16.29 % (2507708)Termination reason: Instruction limit % 113.33/16.29 % (2507708)Termination phase: Saturation % 113.33/16.29 % (2507708)Time elapsed: 0.697 s % 113.33/16.29 % (2507708)Peak memory usage: 22 MB % 113.33/16.29 % (2507708)Instructions burned: 1474 (million) % 113.33/16.29 % (2507725)ott+11_1_sil=16000:gs=on:random_seed=2095369457:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2987 on theBenchmark for (2987ds/2251Mi) % 113.33/16.29 % (2507725)Instruction limit reached! % 113.33/16.29 % (2507725)------------------------------ % 113.33/16.29 % (2507725)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 113.33/16.29 % (2507725)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 113.33/16.29 % (2507725)CaDiCaL version: 2.1.3 % 113.33/16.29 % (2507725)Termination reason: Instruction limit % 113.33/16.29 % (2507725)Termination phase: Saturation % 113.33/16.29 % (2507725)Time elapsed: 1.208 s % 113.33/16.29 % (2507725)Peak memory usage: 24 MB % 113.33/16.29 % (2507725)Instructions burned: 2251 (million) % 113.33/16.29 % (2507727)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=573796053:fmbsr=1.6:i=67534_2975 on theBenchmark for (2975ds/67534Mi) % 113.33/16.29 % (2507727)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 113.33/16.29 % (2507727)Terminated due to inappropriate strategy. % 113.33/16.29 % (2507727)------------------------------ % 113.33/16.29 % (2507727)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 113.33/16.29 % (2507727)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 113.33/16.29 % (2507727)CaDiCaL version: 2.1.3 % 113.33/16.29 % (2507727)Termination reason: Inappropriate % 113.33/16.29 % (2507727)Time elapsed: 0.001 s % 113.33/16.29 % (2507727)Peak memory usage: 10 MB % 113.33/16.29 % (2507727)Instructions burned: 1 (million) % 113.33/16.29 % (2507727)------------------------------ % 113.33/16.29 % (2507727)------------------------------ % 113.33/16.29 % (2507729)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=1770908167:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2975 on theBenchmark for (2975ds/4591Mi) % 113.33/16.29 % (2507721)Instruction limit reached! % 113.33/16.29 % (2507721)------------------------------ % 113.33/16.29 % (2507721)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 113.33/16.29 % (2507721)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 113.33/16.29 % (2507721)CaDiCaL version: 2.1.3 % 113.33/16.29 % (2507721)Termination reason: Instruction limit % 113.33/16.29 % (2507721)Termination phase: Saturation % 113.33/16.29 % (2507721)Time elapsed: 1.837 s % 113.33/16.29 % (2507721)Peak memory usage: 35 MB % 113.33/16.29 % (2507721)Instructions burned: 3518 (million) % 113.33/16.29 % (2507731)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=3811092492:i=29340_2972 on theBenchmark for (2972ds/29340Mi) % 113.33/16.29 % (2507723)Instruction limit reached! % 113.33/16.29 % (2507723)------------------------------ % 113.33/16.29 % (2507723)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 113.33/16.29 % (2507723)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 113.33/16.29 % (2507723)CaDiCaL version: 2.1.3 % 113.33/16.29 % (2507723)Termination reason: Instruction limit % 129.70/18.53 % (2507723)Termination phase: Saturation % 129.70/18.53 % (2507723)Time elapsed: 2.021 s % 129.70/18.53 % (2507723)Peak memory usage: 31 MB % 129.70/18.53 % (2507723)Instructions burned: 3775 (million) % 129.70/18.53 % (2507733)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=2084233243:i=5211_2968 on theBenchmark for (2968ds/5211Mi) % 129.70/18.53 % (2507706)Instruction limit reached! % 129.70/18.53 % (2507706)------------------------------ % 129.70/18.53 % (2507706)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 129.70/18.53 % (2507706)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 129.70/18.53 % (2507706)CaDiCaL version: 2.1.3 % 129.70/18.53 % (2507706)Termination reason: Instruction limit % 129.70/18.53 % (2507706)Termination phase: Saturation % 129.70/18.53 % (2507706)Time elapsed: 2.753 s % 129.70/18.53 % (2507706)Peak memory usage: 41 MB % 129.70/18.53 % (2507706)Instructions burned: 5131 (million) % 129.70/18.53 % (2507735)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=1863205413:i=5497:nm=2_2967 on theBenchmark for (2967ds/5497Mi) % 129.70/18.53 % (2507735)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 129.70/18.53 % (2507735)Terminated due to inappropriate strategy. % 129.70/18.53 % (2507735)------------------------------ % 129.70/18.53 % (2507735)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 129.70/18.53 % (2507735)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 129.70/18.53 % (2507735)CaDiCaL version: 2.1.3 % 129.70/18.53 % (2507735)Termination reason: Inappropriate % 129.70/18.53 % (2507735)Time elapsed: 0.001 s % 129.70/18.53 % (2507735)Peak memory usage: 10 MB % 129.70/18.53 % (2507735)Instructions burned: 1 (million) % 129.70/18.53 % (2507735)------------------------------ % 129.70/18.53 % (2507735)------------------------------ % 129.70/18.53 % (2507737)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=1875940882:fmbsr=2:i=46332_2967 on theBenchmark for (2967ds/46332Mi) % 129.70/18.53 % (2507737)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 129.70/18.53 % (2507737)Terminated due to inappropriate strategy. % 129.70/18.53 % (2507737)------------------------------ % 129.70/18.53 % (2507737)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 129.70/18.53 % (2507737)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 129.70/18.53 % (2507737)CaDiCaL version: 2.1.3 % 129.70/18.53 % (2507737)Termination reason: Inappropriate % 129.70/18.53 % (2507737)Time elapsed: 0.001 s % 129.70/18.53 % (2507737)Peak memory usage: 10 MB % 129.70/18.53 % (2507737)Instructions burned: 1 (million) % 129.70/18.53 % (2507737)------------------------------ % 129.70/18.53 % (2507737)------------------------------ % 129.70/18.53 % (2507739)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=343000376:i=14071_2967 on theBenchmark for (2967ds/14071Mi) % 129.70/18.53 % (2507739)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 129.70/18.53 % (2507739)Terminated due to inappropriate strategy. % 129.70/18.53 % (2507739)------------------------------ % 129.70/18.53 % (2507739)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 129.70/18.53 % (2507739)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 129.70/18.53 % (2507739)CaDiCaL version: 2.1.3 % 129.70/18.53 % (2507739)Termination reason: Inappropriate % 129.70/18.53 % (2507739)Time elapsed: 0.001 s % 129.70/18.53 % (2507739)Peak memory usage: 10 MB % 129.70/18.53 % (2507739)Instructions burned: 1 (million) % 129.70/18.53 % (2507739)------------------------------ % 129.70/18.53 % (2507739)------------------------------ % 129.70/18.53 % (2507741)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=15819516:i=22565:add=on:rawr=on_2966 on theBenchmark for (2966ds/22565Mi) % 129.70/18.53 % (2507717)Instruction limit reached! % 129.70/18.53 % (2507717)------------------------------ % 129.70/18.53 % (2507717)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 129.70/18.53 % (2507717)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 129.70/18.53 % (2507717)CaDiCaL version: 2.1.3 % 129.70/18.53 % (2507717)Termination reason: Instruction limit % 129.70/18.53 % (2507717)Termination phase: Saturation % 129.70/18.53 % (2507717)Time elapsed: 3.187 s % 129.70/18.53 % (2507717)Peak memory usage: 41 MB % 129.70/18.53 % (2507717)Instructions burned: 5114 (million) % 129.70/18.53 % (2507743)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=2643731624:i=8173:av=off_2960 on theBenchmark for (2960ds/8173Mi) % 129.70/18.53 % (2507729)Instruction limit reached! % 130.42/18.64 % (2507729)------------------------------ % 130.42/18.64 % (2507729)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 130.42/18.64 % (2507729)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 130.42/18.64 % (2507729)CaDiCaL version: 2.1.3 % 130.42/18.64 % (2507729)Termination reason: Instruction limit % 130.42/18.64 % (2507729)Termination phase: Saturation % 130.42/18.64 % (2507729)Time elapsed: 2.161 s % 130.42/18.64 % (2507729)Peak memory usage: 52 MB % 130.42/18.64 % (2507729)Instructions burned: 4591 (million) % 130.42/18.64 % (2507745)dis+10_16:1_sil=16000:random_seed=1096267872:i=9155:fsr=off_2953 on theBenchmark for (2953ds/9155Mi) % 130.42/18.64 % (2507733)Instruction limit reached! % 130.42/18.64 % (2507733)------------------------------ % 130.42/18.64 % (2507733)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 130.42/18.64 % (2507733)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 130.42/18.64 % (2507733)CaDiCaL version: 2.1.3 % 130.42/18.64 % (2507733)Termination reason: Instruction limit % 130.42/18.64 % (2507733)Termination phase: Saturation % 130.42/18.64 % (2507733)Time elapsed: 2.748 s % 130.42/18.64 % (2507733)Peak memory usage: 50 MB % 130.42/18.64 % (2507733)Instructions burned: 5211 (million) % 130.42/18.64 % (2507747)ott-3_8_sil=64000:random_seed=2153719835:i=20139:bs=on_2940 on theBenchmark for (2940ds/20139Mi) % 130.42/18.64 % (2507743)Instruction limit reached! % 130.42/18.64 % (2507743)------------------------------ % 130.42/18.64 % (2507743)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 130.42/18.64 % (2507743)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 130.42/18.64 % (2507743)CaDiCaL version: 2.1.3 % 130.42/18.64 % (2507743)Termination reason: Instruction limit % 130.42/18.64 % (2507743)Termination phase: Saturation % 130.42/18.64 % (2507743)Time elapsed: 5.062 s % 130.42/18.64 % (2507743)Peak memory usage: 52 MB % 130.42/18.64 % (2507743)Instructions burned: 8175 (million) % 130.42/18.64 % (2507749)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=3041766344:fmbsr=2:i=32576_2909 on theBenchmark for (2909ds/32576Mi) % 130.42/18.64 % (2507749)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 130.42/18.64 % (2507749)Terminated due to inappropriate strategy. % 130.42/18.64 % (2507749)------------------------------ % 130.42/18.64 % (2507749)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 130.42/18.64 % (2507749)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 130.42/18.64 % (2507749)CaDiCaL version: 2.1.3 % 130.42/18.64 % (2507749)Termination reason: Inappropriate % 130.42/18.64 % (2507749)Time elapsed: 0.001 s % 130.42/18.64 % (2507749)Peak memory usage: 10 MB % 130.42/18.64 % (2507749)Instructions burned: 1 (million) % 130.42/18.64 % (2507749)------------------------------ % 130.42/18.64 % (2507749)------------------------------ % 130.42/18.64 % (2507751)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=2682795624:i=11404_2909 on theBenchmark for (2909ds/11404Mi) % 130.42/18.64 % (2507745)Instruction limit reached! % 130.42/18.64 % (2507745)------------------------------ % 130.42/18.64 % (2507745)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 130.42/18.64 % (2507745)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 130.42/18.64 % (2507745)CaDiCaL version: 2.1.3 % 130.42/18.64 % (2507745)Termination reason: Instruction limit % 130.42/18.64 % (2507745)Termination phase: Saturation % 130.42/18.64 % (2507745)Time elapsed: 4.588 s % 130.42/18.64 % (2507745)Peak memory usage: 52 MB % 130.42/18.64 % (2507745)Instructions burned: 9156 (million) % 130.42/18.64 % (2507753)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=3746095018:i=14134_2907 on theBenchmark for (2907ds/14134Mi) % 130.42/18.64 % (2507731)Instruction limit reached! % 130.42/18.64 % (2507731)------------------------------ % 130.42/18.64 % (2507731)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 130.42/18.64 % (2507731)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 130.42/18.64 % (2507731)CaDiCaL version: 2.1.3 % 130.42/18.64 % (2507731)Termination reason: Instruction limit % 130.42/18.64 % (2507731)Termination phase: Saturation % 130.42/18.64 % (2507731)Time elapsed: 12.788 s % 130.42/18.64 % (2507731)Peak memory usage: 171 MB % 130.42/18.64 % (2507731)Instructions burned: 29342 (million) % 130.42/18.64 % (2508001)dis+33_16_sil=32000:sac=on:random_seed=1723127658:i=15851:nm=0_2844 on theBenchmark for (2844ds/15851Mi) % 130.42/18.64 % (2507751)Instruction limit reached! % 130.42/18.64 % (2507751)------------------------------ % 130.42/18.64 % (2507751)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 169.67/24.14 % (2507751)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 169.67/24.14 % (2507751)CaDiCaL version: 2.1.3 % 169.67/24.14 % (2507751)Termination reason: Instruction limit % 169.67/24.14 % (2507751)Termination phase: Saturation % 169.67/24.14 % (2507751)Time elapsed: 7.009 s % 169.67/24.14 % (2507751)Peak memory usage: 71 MB % 169.67/24.14 % (2507751)Instructions burned: 11405 (million) % 169.67/24.14 % (2508003)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=2530433580:avsq=on:i=17627:add=on:amm=off_2839 on theBenchmark for (2839ds/17627Mi) % 169.67/24.14 % (2507747)Instruction limit reached! % 169.67/24.14 % (2507747)------------------------------ % 169.67/24.14 % (2507747)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 169.67/24.14 % (2507747)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 169.67/24.14 % (2507747)CaDiCaL version: 2.1.3 % 169.67/24.14 % (2507747)Termination reason: Instruction limit % 169.67/24.14 % (2507747)Termination phase: Saturation % 169.67/24.14 % (2507747)Time elapsed: 11.286 s % 169.67/24.14 % (2507747)Peak memory usage: 55 MB % 169.67/24.14 % (2507747)Instructions burned: 20140 (million) % 169.67/24.14 % (2508051)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=1677085192:s2a=on:i=53295_2827 on theBenchmark for (2827ds/53295Mi) % 169.67/24.14 % (2507741)Instruction limit reached! % 169.67/24.14 % (2507741)------------------------------ % 169.67/24.14 % (2507741)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 169.67/24.14 % (2507741)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 169.67/24.14 % (2507741)CaDiCaL version: 2.1.3 % 169.67/24.14 % (2507741)Termination reason: Instruction limit % 169.67/24.14 % (2507741)Termination phase: Saturation % 169.67/24.14 % (2507741)Time elapsed: 14.061 s % 169.67/24.14 % (2507741)Peak memory usage: 729 MB % 169.67/24.14 % (2507741)Instructions burned: 22565 (million) % 169.67/24.14 % (2508054)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=540354217:i=26857:ins=20_2824 on theBenchmark for (2824ds/26857Mi) % 169.67/24.14 % (2508054)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 169.67/24.14 % (2508054)Terminated due to inappropriate strategy. % 169.67/24.14 % (2508054)------------------------------ % 169.67/24.14 % (2508054)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 169.67/24.14 % (2508054)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 169.67/24.14 % (2508054)CaDiCaL version: 2.1.3 % 169.67/24.14 % (2508054)Termination reason: Inappropriate % 169.67/24.14 % (2508054)Time elapsed: 0.001 s % 169.67/24.14 % (2508054)Peak memory usage: 10 MB % 169.67/24.14 % (2508054)Instructions burned: 1 (million) % 169.67/24.14 % (2508054)------------------------------ % 169.67/24.14 % (2508054)------------------------------ % 169.67/24.14 % (2508056)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=1813515102:i=28120:bs=on:fsr=off_2824 on theBenchmark for (2824ds/28120Mi) % 169.67/24.14 % (2507753)Instruction limit reached! % 169.67/24.14 % (2507753)------------------------------ % 169.67/24.14 % (2507753)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 169.67/24.14 % (2507753)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 169.67/24.14 % (2507753)CaDiCaL version: 2.1.3 % 169.67/24.14 % (2507753)Termination reason: Instruction limit % 169.67/24.14 % (2507753)Termination phase: Saturation % 169.67/24.14 % (2507753)Time elapsed: 8.970 s % 169.67/24.14 % (2507753)Peak memory usage: 73 MB % 169.67/24.14 % (2507753)Instructions burned: 14135 (million) % 169.67/24.14 % (2508163)fmb+10_1_sil=256000:fmbss=7:random_seed=3314132895:fmbsr=1.6:i=182295_2817 on theBenchmark for (2817ds/182295Mi) % 169.67/24.14 % (2508163)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 169.67/24.14 % (2508163)Terminated due to inappropriate strategy. % 169.67/24.14 % (2508163)------------------------------ % 169.67/24.14 % (2508163)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 169.67/24.14 % (2508163)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 169.67/24.14 % (2508163)CaDiCaL version: 2.1.3 % 169.67/24.14 % (2508163)Termination reason: Inappropriate % 169.67/24.14 % (2508163)Time elapsed: 0.001 s % 169.67/24.14 % (2508163)Peak memory usage: 10 MB % 169.67/24.14 % (2508163)Instructions burned: 1 (million) % 169.67/24.14 % (2508163)------------------------------ % 169.67/24.14 % (2508163)------------------------------ % 169.67/24.14 % (2508165)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=2973378058:i=44625:gsp=on_2817 on theBenchmark for (2817ds/44625Mi) % 176.06/25.11 % (2508165)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 176.06/25.11 % (2508165)Terminated due to inappropriate strategy. % 176.06/25.11 % (2508165)------------------------------ % 176.06/25.11 % (2508165)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 176.06/25.11 % (2508165)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 176.06/25.11 % (2508165)CaDiCaL version: 2.1.3 % 176.06/25.11 % (2508165)Termination reason: Inappropriate % 176.06/25.11 % (2508165)Time elapsed: 0.001 s % 176.06/25.11 % (2508165)Peak memory usage: 10 MB % 176.06/25.11 % (2508165)Instructions burned: 1 (million) % 176.06/25.11 % (2508165)------------------------------ % 176.06/25.11 % (2508165)------------------------------ % 176.06/25.11 % (2508167)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=420292987:i=160505_2817 on theBenchmark for (2817ds/160505Mi) % 176.06/25.11 % (2508167)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 176.06/25.11 % (2508167)Terminated due to inappropriate strategy. % 176.06/25.11 % (2508167)------------------------------ % 176.06/25.11 % (2508167)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 176.06/25.11 % (2508167)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 176.06/25.11 % (2508167)CaDiCaL version: 2.1.3 % 176.06/25.11 % (2508167)Termination reason: Inappropriate % 176.06/25.11 % (2508167)Time elapsed: 0.001 s % 176.06/25.11 % (2508167)Peak memory usage: 10 MB % 176.06/25.11 % (2508167)Instructions burned: 1 (million) % 176.06/25.11 % (2508167)------------------------------ % 176.06/25.11 % (2508167)------------------------------ % 176.06/25.11 % (2508169)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=639916965:fmbsr=1.3:i=225729_2816 on theBenchmark for (2816ds/225729Mi) % 176.06/25.11 % (2508169)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 176.06/25.11 % (2508169)Terminated due to inappropriate strategy. % 176.06/25.11 % (2508169)------------------------------ % 176.06/25.11 % (2508169)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 176.06/25.11 % (2508169)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 176.06/25.11 % (2508169)CaDiCaL version: 2.1.3 % 176.06/25.11 % (2508169)Termination reason: Inappropriate % 176.06/25.11 % (2508169)Time elapsed: 0.001 s % 176.06/25.11 % (2508169)Peak memory usage: 10 MB % 176.06/25.11 % (2508169)Instructions burned: 1 (million) % 176.06/25.11 % (2508169)------------------------------ % 176.06/25.11 % (2508169)------------------------------ % 176.06/25.11 % (2508171)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=1039069665:fmbsr=2:i=185024:ins=7_2816 on theBenchmark for (2816ds/185024Mi) % 176.06/25.11 % (2508171)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 176.06/25.11 % (2508171)Terminated due to inappropriate strategy. % 176.06/25.11 % (2508171)------------------------------ % 176.06/25.11 % (2508171)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 176.06/25.11 % (2508171)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 176.06/25.11 % (2508171)CaDiCaL version: 2.1.3 % 176.06/25.11 % (2508171)Termination reason: Inappropriate % 176.06/25.11 % (2508171)Time elapsed: 0.001 s % 176.06/25.11 % (2508171)Peak memory usage: 10 MB % 176.06/25.11 % (2508171)Instructions burned: 1 (million) % 176.06/25.11 % (2508171)------------------------------ % 176.06/25.11 % (2508171)------------------------------ % 176.06/25.11 % (2508173)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=2817529923:rtra=on_2816 on theBenchmark for (2816ds/0Mi) % 176.06/25.11 % (2508173)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 176.06/25.11 % (2508173)Terminated due to inappropriate strategy. % 176.06/25.11 % (2508173)------------------------------ % 176.06/25.11 % (2508173)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 176.06/25.11 % (2508173)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 176.06/25.11 % (2508173)CaDiCaL version: 2.1.3 % 176.06/25.11 % (2508173)Termination reason: Inappropriate % 176.06/25.11 % (2508173)Time elapsed: 0.001 s % 176.06/25.11 % (2508173)Peak memory usage: 10 MB % 176.06/25.11 % (2508173)Instructions burned: 1 (million) % 176.06/25.11 % (2508173)------------------------------ % 176.06/25.11 % (2508173)------------------------------ % 176.06/25.11 % (2508175)% WARNING: option uhcvi not known. % 176.06/25.11 % (2508175)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3925152106:i=271062:add=off:rtra=on:rawr=on_2816 on theBenchmark for (2816ds/271062Mi) % 184.88/26.39 % (2507669)Instruction limit reached! % 184.88/26.39 % (2507669)------------------------------ % 184.88/26.39 % (2507669)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 184.88/26.39 % (2507669)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 184.88/26.39 % (2507669)CaDiCaL version: 2.1.3 % 184.88/26.39 % (2507669)Termination reason: Instruction limit % 184.88/26.39 % (2507669)Termination phase: Saturation % 184.88/26.39 % (2507669)Time elapsed: 18.738 s % 184.88/26.39 % (2507669)Peak memory usage: 344 MB % 184.88/26.39 % (2507669)Instructions burned: 88033 (million) % 184.88/26.39 % (2508224)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1663071989:i=176048:add=on:rtra=on:rawr=on_2812 on theBenchmark for (2812ds/176048Mi) % 184.88/26.39 % (2508001)Instruction limit reached! % 184.88/26.39 % (2508001)------------------------------ % 184.88/26.39 % (2508001)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 184.88/26.39 % (2508001)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 184.88/26.39 % (2508001)CaDiCaL version: 2.1.3 % 184.88/26.39 % (2508001)Termination reason: Instruction limit % 184.88/26.39 % (2508001)Termination phase: Saturation % 184.88/26.39 % (2508001)Time elapsed: 7.505 s % 184.88/26.39 % (2508001)Peak memory usage: 205 MB % 184.88/26.39 % (2508001)Instructions burned: 15853 (million) % 184.88/26.39 % (2508226)dis+10_1_sil=32000:si=on:sp=arity:random_seed=1482463512:i=206:fgj=on:rtra=on_2768 on theBenchmark for (2768ds/206Mi) % 184.88/26.39 % (2508226)Instruction limit reached! % 184.88/26.39 % (2508226)------------------------------ % 184.88/26.39 % (2508226)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 184.88/26.39 % (2508226)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 184.88/26.39 % (2508226)CaDiCaL version: 2.1.3 % 184.88/26.39 % (2508226)Termination reason: Instruction limit % 184.88/26.39 % (2508226)Termination phase: Saturation % 184.88/26.39 % (2508226)Time elapsed: 0.125 s % 184.88/26.39 % (2508226)Peak memory usage: 13 MB % 184.88/26.39 % (2508226)Instructions burned: 207 (million) % 184.88/26.39 % (2508228)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=159147796:i=232:rtra=on_2767 on theBenchmark for (2767ds/232Mi) % 184.88/26.39 % (2508228)Instruction limit reached! % 184.88/26.39 % (2508228)------------------------------ % 184.88/26.39 % (2508228)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 184.88/26.39 % (2508228)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 184.88/26.39 % (2508228)CaDiCaL version: 2.1.3 % 184.88/26.39 % (2508228)Termination reason: Instruction limit % 184.88/26.39 % (2508228)Termination phase: Saturation % 184.88/26.39 % (2508228)Time elapsed: 0.149 s % 184.88/26.39 % (2508228)Peak memory usage: 13 MB % 184.88/26.39 % (2508228)Instructions burned: 233 (million) % 184.88/26.39 % (2508230)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=3893267840:i=262:rtra=on_2765 on theBenchmark for (2765ds/262Mi) % 184.88/26.39 % (2508230)Instruction limit reached! % 184.88/26.39 % (2508230)------------------------------ % 184.88/26.39 % (2508230)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 184.88/26.39 % (2508230)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 184.88/26.39 % (2508230)CaDiCaL version: 2.1.3 % 184.88/26.39 % (2508230)Termination reason: Instruction limit % 184.88/26.39 % (2508230)Termination phase: Saturation % 184.88/26.39 % (2508230)Time elapsed: 0.163 s % 184.88/26.39 % (2508230)Peak memory usage: 14 MB % 184.88/26.39 % (2508230)Instructions burned: 263 (million) % 184.88/26.39 % (2508232)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=3409889515:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2763 on theBenchmark for (2763ds/318Mi) % 184.88/26.39 % (2508232)Instruction limit reached! % 184.88/26.39 % (2508232)------------------------------ % 184.88/26.39 % (2508232)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 184.88/26.39 % (2508232)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 184.88/26.39 % (2508232)CaDiCaL version: 2.1.3 % 184.88/26.39 % (2508232)Termination reason: Instruction limit % 184.88/26.39 % (2508232)Termination phase: Saturation % 184.88/26.39 % (2508232)Time elapsed: 0.216 s % 184.88/26.39 % (2508232)Peak memory usage: 15 MB % 184.88/26.39 % (2508232)Instructions burned: 319 (million) % 184.88/26.39 % (2508234)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=2357689340:i=1428:nm=2:rtra=on_2761 on theBenchmark for (2761ds/1428Mi) % 200.51/28.74 % (2508234)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 200.51/28.74 % (2508234)Terminated due to inappropriate strategy. % 200.51/28.74 % (2508234)------------------------------ % 200.51/28.74 % (2508234)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 200.51/28.74 % (2508234)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 200.51/28.74 % (2508234)CaDiCaL version: 2.1.3 % 200.51/28.74 % (2508234)Termination reason: Inappropriate % 200.51/28.74 % (2508234)Time elapsed: 0.001 s % 200.51/28.74 % (2508234)Peak memory usage: 10 MB % 200.51/28.74 % (2508234)Instructions burned: 1 (million) % 200.51/28.74 % (2508234)------------------------------ % 200.51/28.74 % (2508234)------------------------------ % 200.51/28.74 % (2508236)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=3406780643:i=262:bd=preordered:rtra=on:fsd=on_2760 on theBenchmark for (2760ds/262Mi) % 200.51/28.74 % (2508236)Instruction limit reached! % 200.51/28.74 % (2508236)------------------------------ % 200.51/28.74 % (2508236)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 200.51/28.74 % (2508236)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 200.51/28.74 % (2508236)CaDiCaL version: 2.1.3 % 200.51/28.74 % (2508236)Termination reason: Instruction limit % 200.51/28.74 % (2508236)Termination phase: Saturation % 200.51/28.74 % (2508236)Time elapsed: 0.173 s % 200.51/28.74 % (2508236)Peak memory usage: 14 MB % 200.51/28.74 % (2508236)Instructions burned: 263 (million) % 200.51/28.74 % (2508238)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=2774211713:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2759 on theBenchmark for (2759ds/1368Mi) % 200.51/28.74 % (2508003)Instruction limit reached! % 200.51/28.74 % (2508003)------------------------------ % 200.51/28.74 % (2508003)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 200.51/28.74 % (2508003)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 200.51/28.74 % (2508003)CaDiCaL version: 2.1.3 % 200.51/28.74 % (2508003)Termination reason: Instruction limit % 200.51/28.74 % (2508003)Termination phase: Saturation % 200.51/28.74 % (2508003)Time elapsed: 8.407 s % 200.51/28.74 % (2508003)Peak memory usage: 233 MB % 200.51/28.74 % (2508003)Instructions burned: 17627 (million) % 200.51/28.74 % (2508240)ott-21_1_sil=16000:si=on:fs=off:random_seed=4127319648:i=360:av=off:fsr=off:rtra=on_2754 on theBenchmark for (2754ds/360Mi) % 200.51/28.74 % (2508240)Instruction limit reached! % 200.51/28.74 % (2508240)------------------------------ % 200.51/28.74 % (2508240)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 200.51/28.74 % (2508240)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 200.51/28.74 % (2508240)CaDiCaL version: 2.1.3 % 200.51/28.74 % (2508240)Termination reason: Instruction limit % 200.51/28.74 % (2508240)Termination phase: Saturation % 200.51/28.74 % (2508240)Time elapsed: 0.161 s % 200.51/28.74 % (2508240)Peak memory usage: 13 MB % 200.51/28.74 % (2508240)Instructions burned: 360 (million) % 200.51/28.74 % (2508242)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=4058982651:i=954:bd=all:rtra=on_2752 on theBenchmark for (2752ds/954Mi) % 200.51/28.74 % (2508238)Instruction limit reached! % 200.51/28.74 % (2508238)------------------------------ % 200.51/28.74 % (2508238)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 200.51/28.74 % (2508238)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 200.51/28.74 % (2508238)CaDiCaL version: 2.1.3 % 200.51/28.74 % (2508238)Termination reason: Instruction limit % 200.51/28.74 % (2508238)Termination phase: Saturation % 200.51/28.74 % (2508238)Time elapsed: 0.734 s % 200.51/28.74 % (2508238)Peak memory usage: 21 MB % 200.51/28.74 % (2508238)Instructions burned: 1370 (million) % 200.51/28.74 % (2508244)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=3110165684:fmbsr=1.3:i=1730:ins=25:rtra=on_2751 on theBenchmark for (2751ds/1730Mi) % 200.51/28.74 % (2508244)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 200.51/28.74 % (2508244)Terminated due to inappropriate strategy. % 200.51/28.74 % (2508244)------------------------------ % 200.51/28.74 % (2508244)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 200.51/28.74 % (2508244)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 200.51/28.74 % (2508244)CaDiCaL version: 2.1.3 % 200.51/28.74 % (2508244)Termination reason: Inappropriate % 241.14/34.29 % (2508244)Time elapsed: 0.001 s % 241.14/34.29 % (2508244)Peak memory usage: 10 MB % 241.14/34.29 % (2508244)Instructions burned: 1 (million) % 241.14/34.29 % (2508244)------------------------------ % 241.14/34.29 % (2508244)------------------------------ % 241.14/34.29 % (2508246)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=1207024349:i=2358:rtra=on_2751 on theBenchmark for (2751ds/2358Mi) % 241.14/34.29 % (2508242)Instruction limit reached! % 241.14/34.29 % (2508242)------------------------------ % 241.14/34.29 % (2508242)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 241.14/34.29 % (2508242)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 241.14/34.29 % (2508242)CaDiCaL version: 2.1.3 % 241.14/34.29 % (2508242)Termination reason: Instruction limit % 241.14/34.29 % (2508242)Termination phase: Saturation % 241.14/34.29 % (2508242)Time elapsed: 0.629 s % 241.14/34.29 % (2508242)Peak memory usage: 15 MB % 241.14/34.29 % (2508242)Instructions burned: 954 (million) % 241.14/34.29 % (2508248)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=2527177139:i=1778:ins=1:rtra=on_2746 on theBenchmark for (2746ds/1778Mi) % 241.14/34.29 % (2508248)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 241.14/34.30 % (2508248)Terminated due to inappropriate strategy. % 241.14/34.30 % (2508248)------------------------------ % 241.14/34.30 % (2508248)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 241.14/34.30 % (2508248)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 241.14/34.30 % (2508248)CaDiCaL version: 2.1.3 % 241.14/34.30 % (2508248)Termination reason: Inappropriate % 241.14/34.30 % (2508248)Time elapsed: 0.001 s % 241.14/34.30 % (2508248)Peak memory usage: 10 MB % 241.14/34.30 % (2508248)Instructions burned: 1 (million) % 241.14/34.30 % (2508248)------------------------------ % 241.14/34.30 % (2508248)------------------------------ % 241.14/34.30 % (2508250)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=386390028:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2746 on theBenchmark for (2746ds/1384Mi) % 241.14/34.30 % (2508246)Instruction limit reached! % 241.14/34.30 % (2508246)------------------------------ % 241.14/34.30 % (2508246)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 241.14/34.30 % (2508246)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 241.14/34.30 % (2508246)CaDiCaL version: 2.1.3 % 241.14/34.30 % (2508246)Termination reason: Instruction limit % 241.14/34.30 % (2508246)Termination phase: Saturation % 241.14/34.30 % (2508246)Time elapsed: 0.996 s % 241.14/34.30 % (2508246)Peak memory usage: 21 MB % 241.14/34.30 % (2508246)Instructions burned: 2359 (million) % 241.14/34.30 % (2508252)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=1149838318:i=1758:kws=inv_precedence:fsr=off:rtra=on_2741 on theBenchmark for (2741ds/1758Mi) % 241.14/34.30 % (2508250)Instruction limit reached! % 241.14/34.30 % (2508250)------------------------------ % 241.14/34.30 % (2508250)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 241.14/34.30 % (2508250)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 241.14/34.30 % (2508250)CaDiCaL version: 2.1.3 % 241.14/34.30 % (2508250)Termination reason: Instruction limit % 241.14/34.30 % (2508250)Termination phase: Saturation % 241.14/34.30 % (2508250)Time elapsed: 0.715 s % 241.14/34.30 % (2508250)Peak memory usage: 25 MB % 241.14/34.30 % (2508250)Instructions burned: 1386 (million) % 241.14/34.30 % (2508254)fmb+10_1_sil=64000:si=on:random_seed=1944279445:i=44122:nm=2:rtra=on:gsp=on_2738 on theBenchmark for (2738ds/44122Mi) % 241.14/34.30 % (2508254)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 241.14/34.30 % (2508254)Terminated due to inappropriate strategy. % 241.14/34.30 % (2508254)------------------------------ % 241.14/34.30 % (2508254)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 241.14/34.30 % (2508254)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 241.14/34.30 % (2508254)CaDiCaL version: 2.1.3 % 241.14/34.30 % (2508254)Termination reason: Inappropriate % 241.14/34.30 % (2508254)Time elapsed: 0.001 s % 241.14/34.30 % (2508254)Peak memory usage: 10 MB % 241.14/34.30 % (2508254)Instructions burned: 1 (million) % 241.14/34.30 % (2508254)------------------------------ % 241.14/34.30 % (2508254)------------------------------ % 241.14/34.30 % (2508256)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=2535899175:i=19030:nm=5:rtra=on_2738 on theBenchmark for (2738ds/19030Mi) % 288.73/40.91 % (2508256)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 288.73/40.91 % (2508256)Terminated due to inappropriate strategy. % 288.73/40.91 % (2508256)------------------------------ % 288.73/40.91 % (2508256)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 288.73/40.91 % (2508256)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 288.73/40.91 % (2508256)CaDiCaL version: 2.1.3 % 288.73/40.91 % (2508256)Termination reason: Inappropriate % 288.73/40.91 % (2508256)Time elapsed: 0.001 s % 288.73/40.91 % (2508256)Peak memory usage: 10 MB % 288.73/40.91 % (2508256)Instructions burned: 1 (million) % 288.73/40.91 % (2508256)------------------------------ % 288.73/40.91 % (2508256)------------------------------ % 288.73/40.91 % (2508258)fmb+10_1_sil=64000:sas=cadical:si=on:fmbss=8:random_seed=585419151:fmbsr=1.7:i=1840:rtra=on_2738 on theBenchmark for (2738ds/1840Mi) % 288.73/40.91 % (2508258)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 288.73/40.91 % (2508258)Terminated due to inappropriate strategy. % 288.73/40.91 % (2508258)------------------------------ % 288.73/40.91 % (2508258)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 288.73/40.91 % (2508258)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 288.73/40.91 % (2508258)CaDiCaL version: 2.1.3 % 288.73/40.91 % (2508258)Termination reason: Inappropriate % 288.73/40.91 % (2508258)Time elapsed: 0.001 s % 288.73/40.91 % (2508258)Peak memory usage: 10 MB % 288.73/40.91 % (2508258)Instructions burned: 1 (million) % 288.73/40.91 % (2508258)------------------------------ % 288.73/40.91 % (2508258)------------------------------ % 288.73/40.91 % (2508260)dis-4_1_sil=16000:drc=ordering:si=on:sp=const_frequency:sac=on:newcnf=on:random_seed=2439341558:i=10262:rtra=on_2738 on theBenchmark for (2738ds/10262Mi) % 288.73/40.91 % (2508252)Instruction limit reached! % 288.73/40.91 % (2508252)------------------------------ % 288.73/40.91 % (2508252)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 288.73/40.91 % (2508252)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 288.73/40.91 % (2508252)CaDiCaL version: 2.1.3 % 288.73/40.91 % (2508252)Termination reason: Instruction limit % 288.73/40.91 % (2508252)Termination phase: Saturation % 288.73/40.91 % (2508252)Time elapsed: 0.972 s % 288.73/40.91 % (2508252)Peak memory usage: 26 MB % 288.73/40.91 % (2508252)Instructions burned: 1758 (million) % 288.73/40.91 % (2508262)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:si=on:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1325963508:i=2944:ins=7:rtra=on:fdi=8:gsp=on_2731 on theBenchmark for (2731ds/2944Mi) % 288.73/40.91 % (2508262)Instruction limit reached! % 288.73/40.91 % (2508262)------------------------------ % 288.73/40.91 % (2508262)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 288.73/40.91 % (2508262)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 288.73/40.91 % (2508262)CaDiCaL version: 2.1.3 % 288.73/40.91 % (2508262)Termination reason: Instruction limit % 288.73/40.91 % (2508262)Termination phase: Saturation % 288.73/40.91 % (2508262)Time elapsed: 1.551 s % 288.73/40.91 % (2508262)Peak memory usage: 58 MB % 288.73/40.91 % (2508262)Instructions burned: 2944 (million) % 288.73/40.91 % (2508380)fmb+10_1_sil=16000:sas=cadical:si=on:bce=on:fmbss=77:random_seed=2872792647:i=12648:rtra=on_2715 on theBenchmark for (2715ds/12648Mi) % 288.73/40.91 % (2508380)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 288.73/40.91 % (2508380)Terminated due to inappropriate strategy. % 288.73/40.91 % (2508380)------------------------------ % 288.73/40.91 % (2508380)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 288.73/40.91 % (2508380)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 288.73/40.91 % (2508380)CaDiCaL version: 2.1.3 % 288.73/40.91 % (2508380)Termination reason: Inappropriate % 288.73/40.91 % (2508380)Time elapsed: 0.001 s % 288.73/40.91 % (2508380)Peak memory usage: 10 MB % 288.73/40.91 % (2508380)Instructions burned: 1 (million) % 288.73/40.91 % (2508380)------------------------------ % 288.73/40.91 % (2508380)------------------------------ % 288.73/40.91 % (2508382)fmb+10_1_fmbas=function:sil=32000:sas=cadical:si=on:fmbss=16:random_seed=2395705288:fmbsr=2.30978:i=4348:rtra=on_2715 on theBenchmark for (2715ds/4348Mi) % 288.73/40.91 % (2508382)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 288.73/40.91 % (2508382)Terminated due to inappropriate strategy. % 288.73/40.91 % (2508382)------------------------------ % 288.73/40.91 % (2508382)VersTerminated % 300.08/42.54 % Vampire exiting %------------------------------------------------------------------------------