%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWW584_2 : TPTP v9.3.1. Released v6.1.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % Computer : n001.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 29 01:40:29 PM UTC 2026 % Result : Timeout 300.18s 42.53s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : SWW584_2 : TPTP v9.3.1. Released v6.1.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.08/0.17 % Computer : n001.cluster.edu % 0.08/0.17 % Model : x86_64 x86_64 % 0.08/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.08/0.17 % Memory : 8046.5625MB % 0.08/0.17 % OS : Linux 6.8.0-71-generic % 0.08/0.17 % CPULimit : 300 % 0.08/0.17 % WCLimit : 300 % 0.08/0.17 % DateTime : Mon Sep 28 14:25:48 UTC 2026 % 0.08/0.17 % CPUTime : % 0.08/0.17 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.08/0.20 Running first-order model finding % 0.08/0.20 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 4.42/0.95 % (378398)Will run a generic schedule for satisfiability detection. % 4.42/0.95 % (378416)dis+10_1_sil=32000:sp=arity:random_seed=2338993584:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 4.42/0.95 % (378414)% WARNING: option uhcvi not known. % 4.42/0.95 % (378413)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3748058479_2999 on theBenchmark for (2999ds/0Mi) % 4.42/0.95 % (378414)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2259917737:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 4.42/0.95 % (378415)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3323421393:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 4.42/0.95 % (378417)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=4142812275:i=116_2999 on theBenchmark for (2999ds/116Mi) % 4.42/0.95 % (378413)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 4.42/0.95 % (378413)Terminated due to inappropriate strategy. % 4.42/0.95 % (378413)------------------------------ % 4.42/0.95 % (378413)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 4.42/0.95 % (378413)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.42/0.95 % (378413)CaDiCaL version: 2.1.3 % 4.42/0.95 % (378413)Termination reason: Inappropriate % 4.42/0.95 % (378413)Time elapsed: 0.003 s % 4.42/0.95 % (378413)Peak memory usage: 11 MB % 4.42/0.95 % (378413)Instructions burned: 5 (million) % 4.42/0.95 % (378413)------------------------------ % 4.42/0.95 % (378413)------------------------------ % 4.42/0.95 % (378419)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=260177477:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 4.42/0.95 % (378418)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1114008936:i=131_2999 on theBenchmark for (2999ds/131Mi) % 4.42/0.95 % (378429)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3396215818:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 4.42/0.95 % (378429)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 4.42/0.95 % (378429)Terminated due to inappropriate strategy. % 4.42/0.95 % (378429)------------------------------ % 4.42/0.95 % (378429)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 4.42/0.95 % (378429)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.42/0.95 % (378429)CaDiCaL version: 2.1.3 % 4.42/0.95 % (378429)Termination reason: Inappropriate % 4.42/0.95 % (378429)Time elapsed: 0.003 s % 4.42/0.95 % (378429)Peak memory usage: 11 MB % 4.42/0.95 % (378429)Instructions burned: 4 (million) % 4.42/0.95 % (378416)Instruction limit reached! % 4.42/0.95 % (378416)------------------------------ % 4.42/0.95 % (378416)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 4.42/0.95 % (378416)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.42/0.95 % (378416)CaDiCaL version: 2.1.3 % 4.42/0.95 % (378416)Termination reason: Instruction limit % 4.42/0.95 % (378416)Termination phase: Saturation % 4.42/0.95 % (378429)------------------------------ % 4.42/0.95 % (378429)------------------------------ % 4.42/0.95 % (378416)Time elapsed: 0.038 s % 4.42/0.95 % (378416)Peak memory usage: 12 MB % 4.42/0.95 % (378416)Instructions burned: 104 (million) % 4.42/0.95 % (378437)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3899430519:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 4.42/0.95 % (378438)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=1293446435:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi) % 4.42/0.95 % (378417)Instruction limit reached! % 4.42/0.95 % (378417)------------------------------ % 4.42/0.95 % (378417)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 4.42/0.95 % (378417)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.42/0.95 % (378417)CaDiCaL version: 2.1.3 % 4.42/0.95 % (378417)Termination reason: Instruction limit % 4.42/0.95 % (378417)Termination phase: Saturation % 4.42/0.95 % (378417)Time elapsed: 0.076 s % 4.42/0.95 % (378417)Peak memory usage: 13 MB % 4.42/0.95 % (378417)Instructions burned: 117 (million) % 4.42/0.95 % (378455)ott-21_1_sil=16000:fs=off:random_seed=2043565407:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 4.42/0.95 % (378418)Instruction limit reached! % 4.42/0.95 % (378418)------------------------------ % 7.22/1.39 % (378418)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.22/1.39 % (378418)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.22/1.39 % (378418)CaDiCaL version: 2.1.3 % 7.22/1.39 % (378418)Termination reason: Instruction limit % 7.22/1.39 % (378418)Termination phase: Saturation % 7.22/1.39 % (378418)Time elapsed: 0.100 s % 7.22/1.39 % (378418)Peak memory usage: 13 MB % 7.22/1.39 % (378418)Instructions burned: 135 (million) % 7.22/1.39 % (378419)Instruction limit reached! % 7.22/1.39 % (378419)------------------------------ % 7.22/1.39 % (378419)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.22/1.39 % (378419)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.22/1.39 % (378419)CaDiCaL version: 2.1.3 % 7.22/1.39 % (378419)Termination reason: Instruction limit % 7.22/1.39 % (378419)Termination phase: Saturation % 7.22/1.39 % (378419)Time elapsed: 0.114 s % 7.22/1.39 % (378419)Peak memory usage: 14 MB % 7.22/1.39 % (378419)Instructions burned: 159 (million) % 7.22/1.39 % (378466)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1731021511:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 7.22/1.39 % (378467)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2162455233:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 7.22/1.39 % (378467)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 7.22/1.39 % (378467)Terminated due to inappropriate strategy. % 7.22/1.39 % (378467)------------------------------ % 7.22/1.39 % (378467)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.22/1.39 % (378467)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.22/1.39 % (378467)CaDiCaL version: 2.1.3 % 7.22/1.39 % (378467)Termination reason: Inappropriate % 7.22/1.39 % (378467)Time elapsed: 0.002 s % 7.22/1.39 % (378467)Peak memory usage: 10 MB % 7.22/1.39 % (378467)Instructions burned: 4 (million) % 7.22/1.39 % (378467)------------------------------ % 7.22/1.39 % (378467)------------------------------ % 7.22/1.39 % (378437)Instruction limit reached! % 7.22/1.39 % (378437)------------------------------ % 7.22/1.39 % (378437)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.22/1.39 % (378437)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.22/1.39 % (378437)CaDiCaL version: 2.1.3 % 7.22/1.39 % (378437)Termination reason: Instruction limit % 7.22/1.39 % (378437)Termination phase: Saturation % 7.22/1.39 % (378437)Time elapsed: 0.096 s % 7.22/1.39 % (378437)Peak memory usage: 13 MB % 7.22/1.39 % (378437)Instructions burned: 131 (million) % 7.22/1.39 % (378470)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=4209008926:i=1179_2998 on theBenchmark for (2998ds/1179Mi) % 7.22/1.39 % (378471)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=963996857:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi) % 7.22/1.39 % (378471)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 7.22/1.39 % (378471)Terminated due to inappropriate strategy. % 7.22/1.39 % (378471)------------------------------ % 7.22/1.39 % (378471)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.22/1.39 % (378471)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.22/1.39 % (378471)CaDiCaL version: 2.1.3 % 7.22/1.39 % (378471)Termination reason: Inappropriate % 7.22/1.39 % (378471)Time elapsed: 0.002 s % 7.22/1.39 % (378471)Peak memory usage: 10 MB % 7.22/1.39 % (378471)Instructions burned: 4 (million) % 7.22/1.39 % (378471)------------------------------ % 7.22/1.39 % (378471)------------------------------ % 7.22/1.39 % (378455)Instruction limit reached! % 7.22/1.39 % (378455)------------------------------ % 7.22/1.39 % (378455)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.22/1.39 % (378455)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.22/1.39 % (378455)CaDiCaL version: 2.1.3 % 7.22/1.39 % (378455)Termination reason: Instruction limit % 7.22/1.39 % (378455)Termination phase: Saturation % 7.22/1.39 % (378455)Time elapsed: 0.092 s % 7.22/1.39 % (378455)Peak memory usage: 12 MB % 7.22/1.39 % (378455)Instructions burned: 182 (million) % 7.22/1.39 % (378474)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=4119804213: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) % 30.75/4.76 % (378475)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2357354679:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi) % 30.75/4.76 % (378466)Instruction limit reached! % 30.75/4.76 % (378466)------------------------------ % 30.75/4.76 % (378466)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 30.75/4.76 % (378466)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 30.75/4.76 % (378466)CaDiCaL version: 2.1.3 % 30.75/4.76 % (378466)Termination reason: Instruction limit % 30.75/4.76 % (378466)Termination phase: Saturation % 30.75/4.76 % (378466)Time elapsed: 0.263 s % 30.75/4.76 % (378466)Peak memory usage: 13 MB % 30.75/4.76 % (378466)Instructions burned: 477 (million) % 30.75/4.76 % (378438)Instruction limit reached! % 30.75/4.76 % (378438)------------------------------ % 30.75/4.76 % (378438)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 30.75/4.76 % (378438)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 30.75/4.76 % (378438)CaDiCaL version: 2.1.3 % 30.75/4.76 % (378438)Termination reason: Instruction limit % 30.75/4.76 % (378438)Termination phase: Saturation % 30.75/4.76 % (378438)Time elapsed: 0.342 s % 30.75/4.76 % (378438)Peak memory usage: 16 MB % 30.75/4.76 % (378438)Instructions burned: 685 (million) % 30.75/4.76 % (378479)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2930466985:i=9515:nm=5_2995 on theBenchmark for (2995ds/9515Mi) % 30.75/4.76 % (378478)fmb+10_1_sil=64000:random_seed=1703003317:i=22061:nm=2:gsp=on_2995 on theBenchmark for (2995ds/22061Mi) % 30.75/4.76 % (378479)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 30.75/4.76 % (378479)Terminated due to inappropriate strategy. % 30.75/4.76 % (378479)------------------------------ % 30.75/4.76 % (378479)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 30.75/4.76 % (378479)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 30.75/4.76 % (378479)CaDiCaL version: 2.1.3 % 30.75/4.76 % (378479)Termination reason: Inappropriate % 30.75/4.76 % (378479)Time elapsed: 0.003 s % 30.75/4.76 % (378479)Peak memory usage: 10 MB % 30.75/4.76 % (378479)Instructions burned: 4 (million) % 30.75/4.76 % (378478)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 30.75/4.76 % (378478)Terminated due to inappropriate strategy. % 30.75/4.76 % (378478)------------------------------ % 30.75/4.76 % (378478)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 30.75/4.76 % (378478)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 30.75/4.76 % (378478)CaDiCaL version: 2.1.3 % 30.75/4.76 % (378478)Termination reason: Inappropriate % 30.75/4.76 % (378478)Time elapsed: 0.003 s % 30.75/4.76 % (378478)Peak memory usage: 10 MB % 30.75/4.76 % (378478)Instructions burned: 4 (million) % 30.75/4.76 % (378479)------------------------------ % 30.75/4.76 % (378479)------------------------------ % 30.75/4.76 % (378478)------------------------------ % 30.75/4.76 % (378478)------------------------------ % 30.75/4.76 % (378483)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=773259438:i=5131_2995 on theBenchmark for (2995ds/5131Mi) % 30.75/4.76 % (378482)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=498412727:fmbsr=1.7:i=920_2995 on theBenchmark for (2995ds/920Mi) % 30.75/4.76 % (378482)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 30.75/4.76 % (378482)Terminated due to inappropriate strategy. % 30.75/4.76 % (378482)------------------------------ % 30.75/4.76 % (378482)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 30.75/4.76 % (378482)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 30.75/4.76 % (378482)CaDiCaL version: 2.1.3 % 30.75/4.76 % (378482)Termination reason: Inappropriate % 30.75/4.76 % (378482)Time elapsed: 0.003 s % 30.75/4.76 % (378482)Peak memory usage: 10 MB % 30.75/4.76 % (378482)Instructions burned: 4 (million) % 30.75/4.76 % (378482)------------------------------ % 30.75/4.76 % (378482)------------------------------ % 30.75/4.76 % (378486)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3576473629:i=1472:ins=7:fdi=8:gsp=on_2995 on theBenchmark for (2995ds/1472Mi) % 30.75/4.76 % (378470)Instruction limit reached! % 30.75/4.76 % (378470)------------------------------ % 30.75/4.76 % (378470)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 30.75/4.76 % (378470)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 36.80/5.41 % (378470)CaDiCaL version: 2.1.3 % 36.80/5.41 % (378470)Termination reason: Instruction limit % 36.80/5.41 % (378470)Termination phase: Saturation % 36.80/5.41 % (378470)Time elapsed: 0.540 s % 36.80/5.41 % (378470)Peak memory usage: 19 MB % 36.80/5.41 % (378470)Instructions burned: 1179 (million) % 36.80/5.41 % (378474)Instruction limit reached! % 36.80/5.41 % (378474)------------------------------ % 36.80/5.41 % (378474)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 36.80/5.41 % (378474)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 36.80/5.41 % (378474)CaDiCaL version: 2.1.3 % 36.80/5.41 % (378474)Termination reason: Instruction limit % 36.80/5.41 % (378474)Termination phase: Saturation % 36.80/5.41 % (378474)Time elapsed: 0.535 s % 36.80/5.41 % (378474)Peak memory usage: 18 MB % 36.80/5.41 % (378474)Instructions burned: 692 (million) % 36.80/5.41 % (378507)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3607324678:i=6324_2992 on theBenchmark for (2992ds/6324Mi) % 36.80/5.41 % (378507)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 36.80/5.41 % (378507)Terminated due to inappropriate strategy. % 36.80/5.41 % (378507)------------------------------ % 36.80/5.41 % (378507)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 36.80/5.41 % (378507)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 36.80/5.41 % (378507)CaDiCaL version: 2.1.3 % 36.80/5.41 % (378507)Termination reason: Inappropriate % 36.80/5.41 % (378507)Time elapsed: 0.002 s % 36.80/5.41 % (378507)Peak memory usage: 11 MB % 36.80/5.41 % (378507)Instructions burned: 4 (million) % 36.80/5.41 % (378507)------------------------------ % 36.80/5.41 % (378507)------------------------------ % 36.80/5.41 % (378510)ott-2_1_sil=16000:newcnf=on:random_seed=3873239239:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2992 on theBenchmark for (2992ds/869Mi) % 36.80/5.41 % (378508)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1470072236:fmbsr=2.30978:i=2174_2992 on theBenchmark for (2992ds/2174Mi) % 36.80/5.41 % (378508)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 36.80/5.41 % (378508)Terminated due to inappropriate strategy. % 36.80/5.41 % (378508)------------------------------ % 36.80/5.41 % (378508)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 36.80/5.41 % (378508)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 36.80/5.41 % (378508)CaDiCaL version: 2.1.3 % 36.80/5.41 % (378508)Termination reason: Inappropriate % 36.80/5.41 % (378508)Time elapsed: 0.004 s % 36.80/5.41 % (378508)Peak memory usage: 10 MB % 36.80/5.41 % (378508)Instructions burned: 4 (million) % 36.80/5.41 % (378508)------------------------------ % 36.80/5.41 % (378508)------------------------------ % 36.80/5.41 % (378475)Instruction limit reached! % 36.80/5.41 % (378475)------------------------------ % 36.80/5.41 % (378475)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 36.80/5.41 % (378475)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 36.80/5.41 % (378475)CaDiCaL version: 2.1.3 % 36.80/5.41 % (378475)Termination reason: Instruction limit % 36.80/5.41 % (378475)Termination phase: Saturation % 36.80/5.41 % (378475)Time elapsed: 0.592 s % 36.80/5.41 % (378475)Peak memory usage: 19 MB % 36.80/5.41 % (378475)Instructions burned: 881 (million) % 36.80/5.41 % (378515)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=4177796627:i=54282_2991 on theBenchmark for (2991ds/54282Mi) % 36.80/5.41 % (378515)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 36.80/5.41 % (378515)Terminated due to inappropriate strategy. % 36.80/5.41 % (378515)------------------------------ % 36.80/5.41 % (378515)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 36.80/5.41 % (378515)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 36.80/5.41 % (378515)CaDiCaL version: 2.1.3 % 36.80/5.41 % (378515)Termination reason: Inappropriate % 36.80/5.41 % (378515)Time elapsed: 0.003 s % 36.80/5.41 % (378515)Peak memory usage: 11 MB % 36.80/5.41 % (378515)Instructions burned: 5 (million) % 36.80/5.41 % (378515)------------------------------ % 36.80/5.41 % (378515)------------------------------ % 36.80/5.41 % (378514)ott+10_1_sil=32000:tgt=ground:random_seed=1659877782:i=5114:av=off_2991 on theBenchmark for (2991ds/5114Mi) % 36.80/5.41 % (378518)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=2940509881:i=3512:aac=none_2991 on theBenchmark for (2991ds/3512Mi) % 36.80/5.41 % (378510)Instruction limit reached! % 99.98/14.30 % (378510)------------------------------ % 99.98/14.30 % (378510)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 99.98/14.30 % (378510)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 99.98/14.30 % (378510)CaDiCaL version: 2.1.3 % 99.98/14.30 % (378510)Termination reason: Instruction limit % 99.98/14.30 % (378510)Termination phase: Saturation % 99.98/14.30 % (378510)Time elapsed: 0.388 s % 99.98/14.30 % (378510)Peak memory usage: 16 MB % 99.98/14.30 % (378510)Instructions burned: 869 (million) % 99.98/14.30 % (378541)dis+21_1_sil=32000:sas=cadical:random_seed=2746289338:i=3773:amm=off_2988 on theBenchmark for (2988ds/3773Mi) % 99.98/14.30 % (378486)Instruction limit reached! % 99.98/14.30 % (378486)------------------------------ % 99.98/14.30 % (378486)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 99.98/14.30 % (378486)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 99.98/14.30 % (378486)CaDiCaL version: 2.1.3 % 99.98/14.30 % (378486)Termination reason: Instruction limit % 99.98/14.30 % (378486)Termination phase: Saturation % 99.98/14.30 % (378486)Time elapsed: 1.259 s % 99.98/14.30 % (378486)Peak memory usage: 25 MB % 99.98/14.30 % (378486)Instructions burned: 1472 (million) % 99.98/14.30 % (378573)ott+11_1_sil=16000:gs=on:random_seed=112884008:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2982 on theBenchmark for (2982ds/2251Mi) % 99.98/14.30 % (378541)Instruction limit reached! % 99.98/14.30 % (378541)------------------------------ % 99.98/14.30 % (378541)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 99.98/14.30 % (378541)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 99.98/14.30 % (378541)CaDiCaL version: 2.1.3 % 99.98/14.30 % (378541)Termination reason: Instruction limit % 99.98/14.30 % (378541)Termination phase: Saturation % 99.98/14.30 % (378541)Time elapsed: 1.695 s % 99.98/14.30 % (378541)Peak memory usage: 34 MB % 99.98/14.30 % (378541)Instructions burned: 3774 (million) % 99.98/14.30 % (378613)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=2423147815:fmbsr=1.6:i=67534_2970 on theBenchmark for (2970ds/67534Mi) % 99.98/14.30 % (378613)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 99.98/14.30 % (378613)Terminated due to inappropriate strategy. % 99.98/14.30 % (378613)------------------------------ % 99.98/14.30 % (378613)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 99.98/14.30 % (378613)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 99.98/14.30 % (378613)CaDiCaL version: 2.1.3 % 99.98/14.30 % (378613)Termination reason: Inappropriate % 99.98/14.30 % (378613)Time elapsed: 0.003 s % 99.98/14.30 % (378613)Peak memory usage: 11 MB % 99.98/14.30 % (378613)Instructions burned: 4 (million) % 99.98/14.30 % (378613)------------------------------ % 99.98/14.30 % (378613)------------------------------ % 99.98/14.30 % (378615)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=3841157910:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2970 on theBenchmark for (2970ds/4591Mi) % 99.98/14.30 % (378518)Instruction limit reached! % 99.98/14.30 % (378518)------------------------------ % 99.98/14.30 % (378518)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 99.98/14.30 % (378518)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 99.98/14.30 % (378518)CaDiCaL version: 2.1.3 % 99.98/14.30 % (378518)Termination reason: Instruction limit % 99.98/14.30 % (378518)Termination phase: Saturation % 99.98/14.30 % (378518)Time elapsed: 3.012 s % 99.98/14.30 % (378518)Peak memory usage: 31 MB % 99.98/14.30 % (378518)Instructions burned: 3513 (million) % 99.98/14.30 % (378632)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=2335811225:i=29340_2960 on theBenchmark for (2960ds/29340Mi) % 99.98/14.30 % (378573)Instruction limit reached! % 99.98/14.30 % (378573)------------------------------ % 99.98/14.30 % (378573)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 99.98/14.30 % (378573)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 99.98/14.30 % (378573)CaDiCaL version: 2.1.3 % 99.98/14.30 % (378573)Termination reason: Instruction limit % 99.98/14.30 % (378573)Termination phase: Saturation % 99.98/14.30 % (378573)Time elapsed: 2.172 s % 99.98/14.30 % (378573)Peak memory usage: 26 MB % 99.98/14.30 % (378573)Instructions burned: 2252 (million) % 99.98/14.30 % (378635)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=1044412972:i=5211_2960 on theBenchmark for (2960ds/5211Mi) % 99.98/14.30 % (378483)Instruction limit reached! % 136.17/19.48 % (378483)------------------------------ % 136.17/19.48 % (378483)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 136.17/19.48 % (378483)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 136.17/19.48 % (378483)CaDiCaL version: 2.1.3 % 136.17/19.48 % (378483)Termination reason: Instruction limit % 136.17/19.48 % (378483)Termination phase: Saturation % 136.17/19.48 % (378483)Time elapsed: 4.088 s % 136.17/19.48 % (378483)Peak memory usage: 41 MB % 136.17/19.48 % (378483)Instructions burned: 5133 (million) % 136.17/19.48 % (378785)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=2715218234:i=5497:nm=2_2954 on theBenchmark for (2954ds/5497Mi) % 136.17/19.48 % (378785)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 136.17/19.48 % (378785)Terminated due to inappropriate strategy. % 136.17/19.48 % (378785)------------------------------ % 136.17/19.48 % (378785)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 136.17/19.48 % (378785)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 136.17/19.48 % (378785)CaDiCaL version: 2.1.3 % 136.17/19.48 % (378785)Termination reason: Inappropriate % 136.17/19.48 % (378785)Time elapsed: 0.003 s % 136.17/19.48 % (378785)Peak memory usage: 11 MB % 136.17/19.48 % (378785)Instructions burned: 4 (million) % 136.17/19.48 % (378785)------------------------------ % 136.17/19.48 % (378785)------------------------------ % 136.17/19.48 % (378791)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=1206003910:fmbsr=2:i=46332_2954 on theBenchmark for (2954ds/46332Mi) % 136.17/19.48 % (378791)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 136.17/19.48 % (378791)Terminated due to inappropriate strategy. % 136.17/19.48 % (378791)------------------------------ % 136.17/19.48 % (378791)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 136.17/19.48 % (378791)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 136.17/19.48 % (378791)CaDiCaL version: 2.1.3 % 136.17/19.48 % (378791)Termination reason: Inappropriate % 136.17/19.48 % (378791)Time elapsed: 0.003 s % 136.17/19.48 % (378791)Peak memory usage: 11 MB % 136.17/19.48 % (378791)Instructions burned: 4 (million) % 136.17/19.48 % (378791)------------------------------ % 136.17/19.48 % (378791)------------------------------ % 136.17/19.48 % (378793)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=264926779:i=14071_2953 on theBenchmark for (2953ds/14071Mi) % 136.17/19.48 % (378793)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 136.17/19.48 % (378793)Terminated due to inappropriate strategy. % 136.17/19.48 % (378793)------------------------------ % 136.17/19.48 % (378793)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 136.17/19.48 % (378793)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 136.17/19.48 % (378793)CaDiCaL version: 2.1.3 % 136.17/19.48 % (378793)Termination reason: Inappropriate % 136.17/19.48 % (378793)Time elapsed: 0.003 s % 136.17/19.48 % (378793)Peak memory usage: 11 MB % 136.17/19.48 % (378793)Instructions burned: 4 (million) % 136.17/19.48 % (378793)------------------------------ % 136.17/19.48 % (378793)------------------------------ % 136.17/19.48 % (378795)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3269706254:i=22565:add=on:rawr=on_2953 on theBenchmark for (2953ds/22565Mi) % 136.17/19.48 % (378615)Instruction limit reached! % 136.17/19.48 % (378615)------------------------------ % 136.17/19.48 % (378615)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 136.17/19.48 % (378615)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 136.17/19.48 % (378615)CaDiCaL version: 2.1.3 % 136.17/19.48 % (378615)Termination reason: Instruction limit % 136.17/19.48 % (378615)Termination phase: Saturation % 136.17/19.48 % (378615)Time elapsed: 1.685 s % 136.17/19.48 % (378615)Peak memory usage: 58 MB % 136.17/19.48 % (378615)Instructions burned: 4594 (million) % 136.17/19.48 % (378797)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=1401741281:i=8173:av=off_2953 on theBenchmark for (2953ds/8173Mi) % 136.17/19.48 % (378514)Instruction limit reached! % 136.17/19.48 % (378514)------------------------------ % 136.17/19.48 % (378514)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 136.17/19.48 % (378514)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 136.17/19.48 % (378514)CaDiCaL version: 2.1.3 % 136.17/19.48 % (378514)Termination reason: Instruction limit % 136.17/19.48 % (378514)Termination phase: Saturation % 136.17/19.48 % (378514)Time elapsed: 4.310 s % 124.80/19.62 % (378514)Peak memory usage: 36 MB % 124.80/19.62 % (378514)Instructions burned: 5115 (million) % 124.80/19.62 % (378799)dis+10_16:1_sil=16000:random_seed=2202658882:i=9155:fsr=off_2947 on theBenchmark for (2947ds/9155Mi) % 124.80/19.62 % (378635)Instruction limit reached! % 124.80/19.62 % (378635)------------------------------ % 124.80/19.62 % (378635)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 124.80/19.62 % (378635)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 124.80/19.62 % (378635)CaDiCaL version: 2.1.3 % 124.80/19.62 % (378635)Termination reason: Instruction limit % 124.80/19.62 % (378635)Termination phase: Saturation % 124.80/19.62 % (378635)Time elapsed: 2.701 s % 124.80/19.62 % (378635)Peak memory usage: 42 MB % 124.80/19.62 % (378635)Instructions burned: 5211 (million) % 124.80/19.62 % (378801)ott-3_8_sil=64000:random_seed=364124117:i=20139:bs=on_2932 on theBenchmark for (2932ds/20139Mi) % 124.80/19.62 % (378797)Instruction limit reached! % 124.80/19.62 % (378797)------------------------------ % 124.80/19.62 % (378797)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 124.80/19.62 % (378797)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 124.80/19.62 % (378797)CaDiCaL version: 2.1.3 % 124.80/19.62 % (378797)Termination reason: Instruction limit % 124.80/19.62 % (378797)Termination phase: Saturation % 124.80/19.62 % (378797)Time elapsed: 2.827 s % 124.80/19.62 % (378797)Peak memory usage: 52 MB % 124.80/19.62 % (378797)Instructions burned: 8174 (million) % 124.80/19.62 % (378803)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=3134785340:fmbsr=2:i=32576_2924 on theBenchmark for (2924ds/32576Mi) % 124.80/19.62 % (378803)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 124.80/19.62 % (378803)Terminated due to inappropriate strategy. % 124.80/19.62 % (378803)------------------------------ % 124.80/19.62 % (378803)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 124.80/19.62 % (378803)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 124.80/19.62 % (378803)CaDiCaL version: 2.1.3 % 124.80/19.62 % (378803)Termination reason: Inappropriate % 124.80/19.62 % (378803)Time elapsed: 0.001 s % 124.80/19.62 % (378803)Peak memory usage: 11 MB % 124.80/19.62 % (378803)Instructions burned: 5 (million) % 124.80/19.62 % (378803)------------------------------ % 124.80/19.62 % (378803)------------------------------ % 124.80/19.62 % (378805)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=1775230843:i=11404_2924 on theBenchmark for (2924ds/11404Mi) % 124.80/19.62 % (378799)Instruction limit reached! % 124.80/19.62 % (378799)------------------------------ % 124.80/19.62 % (378799)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 124.80/19.62 % (378799)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 124.80/19.62 % (378799)CaDiCaL version: 2.1.3 % 124.80/19.62 % (378799)Termination reason: Instruction limit % 124.80/19.62 % (378799)Termination phase: Saturation % 124.80/19.62 % (378799)Time elapsed: 4.721 s % 124.80/19.62 % (378799)Peak memory usage: 52 MB % 124.80/19.62 % (378799)Instructions burned: 9155 (million) % 124.80/19.62 % (378807)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=2689537526:i=14134_2900 on theBenchmark for (2900ds/14134Mi) % 124.80/19.62 % (378805)Instruction limit reached! % 124.80/19.62 % (378805)------------------------------ % 124.80/19.62 % (378805)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 124.80/19.62 % (378805)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 124.80/19.62 % (378805)CaDiCaL version: 2.1.3 % 124.80/19.62 % (378805)Termination reason: Instruction limit % 124.80/19.62 % (378805)Termination phase: Saturation % 124.80/19.62 % (378805)Time elapsed: 3.861 s % 124.80/19.62 % (378805)Peak memory usage: 61 MB % 124.80/19.62 % (378805)Instructions burned: 11405 (million) % 124.80/19.62 % (378809)dis+33_16_sil=32000:sac=on:random_seed=2090188852:i=15851:nm=0_2885 on theBenchmark for (2885ds/15851Mi) % 124.80/19.62 % (378795)Instruction limit reached! % 124.80/19.62 % (378795)------------------------------ % 124.80/19.62 % (378795)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 124.80/19.62 % (378795)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 124.80/19.62 % (378795)CaDiCaL version: 2.1.3 % 124.80/19.62 % (378795)Termination reason: Instruction limit % 124.80/19.62 % (378795)Termination phase: Saturation % 124.80/19.62 % (378795)Time elapsed: 9.391 s % 124.80/19.62 % (378795)Peak memory usage: 216 MB % 124.80/19.62 % (378795)Instructions burned: 22566 (million) % 124.80/19.62 % (378923)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=2788293180:avsq=on:i=17627:add=on:amm=off_2859 on theBenchmark for (2859ds/17627Mi) % 178.62/25.49 % (378809)Instruction limit reached! % 178.62/25.49 % (378809)------------------------------ % 178.62/25.49 % (378809)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 178.62/25.49 % (378809)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 178.62/25.49 % (378809)CaDiCaL version: 2.1.3 % 178.62/25.49 % (378809)Termination reason: Instruction limit % 178.62/25.49 % (378809)Termination phase: Saturation % 178.62/25.49 % (378809)Time elapsed: 4.556 s % 178.62/25.49 % (378809)Peak memory usage: 124 MB % 178.62/25.49 % (378809)Instructions burned: 15855 (million) % 178.62/25.49 % (379172)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=4223524762:s2a=on:i=53295_2840 on theBenchmark for (2840ds/53295Mi) % 178.62/25.49 % (378632)Instruction limit reached! % 178.62/25.49 % (378632)------------------------------ % 178.62/25.49 % (378632)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 178.62/25.49 % (378632)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 178.62/25.49 % (378632)CaDiCaL version: 2.1.3 % 178.62/25.49 % (378632)Termination reason: Instruction limit % 178.62/25.49 % (378632)Termination phase: Saturation % 178.62/25.49 % (378632)Time elapsed: 14.488 s % 178.62/25.49 % (378632)Peak memory usage: 213 MB % 178.62/25.49 % (378632)Instructions burned: 29341 (million) % 178.62/25.49 % (379174)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=1796407254:i=26857:ins=20_2815 on theBenchmark for (2815ds/26857Mi) % 178.62/25.49 % (379174)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 178.62/25.49 % (379174)Terminated due to inappropriate strategy. % 178.62/25.49 % (379174)------------------------------ % 178.62/25.49 % (379174)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 178.62/25.49 % (379174)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 178.62/25.49 % (379174)CaDiCaL version: 2.1.3 % 178.62/25.49 % (379174)Termination reason: Inappropriate % 178.62/25.49 % (379174)Time elapsed: 0.003 s % 178.62/25.49 % (379174)Peak memory usage: 11 MB % 178.62/25.49 % (379174)Instructions burned: 4 (million) % 178.62/25.49 % (379174)------------------------------ % 178.62/25.49 % (379174)------------------------------ % 178.62/25.49 % (379176)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=1461770039:i=28120:bs=on:fsr=off_2815 on theBenchmark for (2815ds/28120Mi) % 178.62/25.49 % (378807)Instruction limit reached! % 178.62/25.49 % (378807)------------------------------ % 178.62/25.49 % (378807)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 178.62/25.49 % (378807)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 178.62/25.49 % (378807)CaDiCaL version: 2.1.3 % 178.62/25.49 % (378807)Termination reason: Instruction limit % 178.62/25.49 % (378807)Termination phase: Saturation % 178.62/25.49 % (378807)Time elapsed: 9.242 s % 178.62/25.49 % (378807)Peak memory usage: 72 MB % 178.62/25.49 % (378807)Instructions burned: 14134 (million) % 178.62/25.49 % (379178)fmb+10_1_sil=256000:fmbss=7:random_seed=1269361574:fmbsr=1.6:i=182295_2807 on theBenchmark for (2807ds/182295Mi) % 178.62/25.49 % (379178)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 178.62/25.49 % (379178)Terminated due to inappropriate strategy. % 178.62/25.49 % (379178)------------------------------ % 178.62/25.49 % (379178)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 178.62/25.49 % (379178)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 178.62/25.49 % (379178)CaDiCaL version: 2.1.3 % 178.62/25.49 % (379178)Termination reason: Inappropriate % 178.62/25.49 % (379178)Time elapsed: 0.003 s % 178.62/25.49 % (379178)Peak memory usage: 11 MB % 178.62/25.49 % (379178)Instructions burned: 4 (million) % 178.62/25.49 % (379178)------------------------------ % 178.62/25.49 % (379178)------------------------------ % 178.62/25.49 % (379180)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=3564615842:i=44625:gsp=on_2807 on theBenchmark for (2807ds/44625Mi) % 178.62/25.49 % (379180)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 178.62/25.49 % (379180)Terminated due to inappropriate strategy. % 178.62/25.49 % (379180)------------------------------ % 178.62/25.49 % (379180)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 178.62/25.49 % (379180)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 178.62/25.49 % (379180)CaDiCaL version: 2.1.3 % 178.62/25.49 % (379180)Termination reason: Inappropriate % 202.91/28.88 % (379180)Time elapsed: 0.003 s % 202.91/28.88 % (379180)Peak memory usage: 11 MB % 202.91/28.88 % (379180)Instructions burned: 4 (million) % 202.91/28.88 % (379180)------------------------------ % 202.91/28.88 % (379180)------------------------------ % 202.91/28.88 % (379182)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=1586807713:i=160505_2807 on theBenchmark for (2807ds/160505Mi) % 202.91/28.88 % (379182)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 202.91/28.88 % (379182)Terminated due to inappropriate strategy. % 202.91/28.88 % (379182)------------------------------ % 202.91/28.88 % (379182)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 202.91/28.88 % (379182)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 202.91/28.88 % (379182)CaDiCaL version: 2.1.3 % 202.91/28.88 % (379182)Termination reason: Inappropriate % 202.91/28.88 % (379182)Time elapsed: 0.003 s % 202.91/28.88 % (379182)Peak memory usage: 11 MB % 202.91/28.88 % (379182)Instructions burned: 4 (million) % 202.91/28.88 % (379182)------------------------------ % 202.91/28.88 % (379182)------------------------------ % 202.91/28.88 % (379184)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=3757729644:fmbsr=1.3:i=225729_2807 on theBenchmark for (2807ds/225729Mi) % 202.91/28.88 % (379184)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 202.91/28.88 % (379184)Terminated due to inappropriate strategy. % 202.91/28.88 % (379184)------------------------------ % 202.91/28.88 % (379184)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 202.91/28.88 % (379184)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 202.91/28.88 % (379184)CaDiCaL version: 2.1.3 % 202.91/28.88 % (379184)Termination reason: Inappropriate % 202.91/28.88 % (379184)Time elapsed: 0.003 s % 202.91/28.88 % (379184)Peak memory usage: 11 MB % 202.91/28.88 % (379184)Instructions burned: 4 (million) % 202.91/28.88 % (379184)------------------------------ % 202.91/28.88 % (379184)------------------------------ % 202.91/28.88 % (379186)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=4240925056:fmbsr=2:i=185024:ins=7_2806 on theBenchmark for (2806ds/185024Mi) % 202.91/28.88 % (379186)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 202.91/28.88 % (379186)Terminated due to inappropriate strategy. % 202.91/28.88 % (379186)------------------------------ % 202.91/28.88 % (379186)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 202.91/28.88 % (379186)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 202.91/28.88 % (379186)CaDiCaL version: 2.1.3 % 202.91/28.88 % (379186)Termination reason: Inappropriate % 202.91/28.88 % (379186)Time elapsed: 0.003 s % 202.91/28.88 % (379186)Peak memory usage: 11 MB % 202.91/28.88 % (379186)Instructions burned: 5 (million) % 202.91/28.88 % (379186)------------------------------ % 202.91/28.88 % (379186)------------------------------ % 202.91/28.88 % (379188)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=216602215:rtra=on_2806 on theBenchmark for (2806ds/0Mi) % 202.91/28.88 % (379188)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 202.91/28.88 % (379188)Terminated due to inappropriate strategy. % 202.91/28.88 % (379188)------------------------------ % 202.91/28.88 % (379188)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 202.91/28.88 % (379188)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 202.91/28.88 % (379188)CaDiCaL version: 2.1.3 % 202.91/28.88 % (379188)Termination reason: Inappropriate % 202.91/28.88 % (379188)Time elapsed: 0.003 s % 202.91/28.88 % (379188)Peak memory usage: 11 MB % 202.91/28.88 % (379188)Instructions burned: 5 (million) % 202.91/28.88 % (379188)------------------------------ % 202.91/28.88 % (379188)------------------------------ % 202.91/28.88 % (378801)Instruction limit reached! % 202.91/28.88 % (378801)------------------------------ % 202.91/28.88 % (378801)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 202.91/28.88 % (378801)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 202.91/28.88 % (378801)CaDiCaL version: 2.1.3 % 202.91/28.88 % (378801)Termination reason: Instruction limit % 202.91/28.88 % (378801)Termination phase: Saturation % 202.91/28.88 % (378801)Time elapsed: 12.661 s % 202.91/28.88 % (378801)Peak memory usage: 76 MB % 202.91/28.88 % (378801)Instructions burned: 20141 (million) % 202.91/28.88 % (379190)% WARNING: option uhcvi not known. % 202.91/28.88 % (379190)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1007795148:i=271062:add=off:rtra=on:rawr=on_2806 on theBenchmark for (2806ds/271062Mi) % 202.91/28.88 % (379191)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1656874417:i=176048:add=on:rtra=on:rawr=on_2806 on theBenchmark for (2806ds/176048Mi) % 212.89/30.23 % (378923)Instruction limit reached! % 212.89/30.23 % (378923)------------------------------ % 212.89/30.23 % (378923)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 212.89/30.23 % (378923)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 212.89/30.23 % (378923)CaDiCaL version: 2.1.3 % 212.89/30.23 % (378923)Termination reason: Instruction limit % 212.89/30.23 % (378923)Termination phase: Saturation % 212.89/30.23 % (378923)Time elapsed: 10.369 s % 212.89/30.23 % (378923)Peak memory usage: 111 MB % 212.89/30.23 % (378923)Instructions burned: 17627 (million) % 212.89/30.23 % (379195)dis+10_1_sil=32000:si=on:sp=arity:random_seed=4102989979:i=206:fgj=on:rtra=on_2755 on theBenchmark for (2755ds/206Mi) % 212.89/30.23 % (379195)Instruction limit reached! % 212.89/30.23 % (379195)------------------------------ % 212.89/30.23 % (379195)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 212.89/30.23 % (379195)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 212.89/30.23 % (379195)CaDiCaL version: 2.1.3 % 212.89/30.23 % (379195)Termination reason: Instruction limit % 212.89/30.23 % (379195)Termination phase: Saturation % 212.89/30.23 % (379195)Time elapsed: 0.135 s % 212.89/30.23 % (379195)Peak memory usage: 13 MB % 212.89/30.23 % (379195)Instructions burned: 206 (million) % 212.89/30.23 % (379197)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=314040979:i=232:rtra=on_2753 on theBenchmark for (2753ds/232Mi) % 212.89/30.23 % (379197)Instruction limit reached! % 212.89/30.23 % (379197)------------------------------ % 212.89/30.23 % (379197)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 212.89/30.23 % (379197)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 212.89/30.23 % (379197)CaDiCaL version: 2.1.3 % 212.89/30.23 % (379197)Termination reason: Instruction limit % 212.89/30.23 % (379197)Termination phase: Saturation % 212.89/30.23 % (379197)Time elapsed: 0.154 s % 212.89/30.23 % (379197)Peak memory usage: 14 MB % 212.89/30.23 % (379197)Instructions burned: 233 (million) % 212.89/30.23 % (379199)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=1234529937:i=262:rtra=on_2751 on theBenchmark for (2751ds/262Mi) % 212.89/30.23 % (379199)Instruction limit reached! % 212.89/30.23 % (379199)------------------------------ % 212.89/30.23 % (379199)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 212.89/30.23 % (379199)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 212.89/30.23 % (379199)CaDiCaL version: 2.1.3 % 212.89/30.23 % (379199)Termination reason: Instruction limit % 212.89/30.23 % (379199)Termination phase: Saturation % 212.89/30.23 % (379199)Time elapsed: 0.172 s % 212.89/30.23 % (379199)Peak memory usage: 14 MB % 212.89/30.23 % (379199)Instructions burned: 263 (million) % 212.89/30.23 % (379201)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=2720932286:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2749 on theBenchmark for (2749ds/318Mi) % 212.89/30.23 % (379201)Instruction limit reached! % 212.89/30.23 % (379201)------------------------------ % 212.89/30.23 % (379201)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 212.89/30.23 % (379201)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 212.89/30.23 % (379201)CaDiCaL version: 2.1.3 % 212.89/30.23 % (379201)Termination reason: Instruction limit % 212.89/30.23 % (379201)Termination phase: Saturation % 212.89/30.23 % (379201)Time elapsed: 0.228 s % 212.89/30.23 % (379201)Peak memory usage: 15 MB % 212.89/30.23 % (379201)Instructions burned: 319 (million) % 212.89/30.23 % (379203)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=1910486836:i=1428:nm=2:rtra=on_2747 on theBenchmark for (2747ds/1428Mi) % 212.89/30.23 % (379203)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 212.89/30.23 % (379203)Terminated due to inappropriate strategy. % 212.89/30.23 % (379203)------------------------------ % 212.89/30.23 % (379203)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 212.89/30.23 % (379203)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 212.89/30.23 % (379203)CaDiCaL version: 2.1.3 % 212.89/30.23 % (379203)Termination reason: Inappropriate % 212.89/30.23 % (379203)Time elapsed: 0.003 s % 212.89/30.23 % (379203)Peak memory usage: 11 MB % 212.89/30.23 % (379203)Instructions burned: 4 (million) % 212.89/30.23 % (379203)------------------------------ % 212.89/30.23 % (379203)------------------------------ % 229.90/32.70 % (379205)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=2206130322:i=262:bd=preordered:rtra=on:fsd=on_2747 on theBenchmark for (2747ds/262Mi) % 229.90/32.70 % (379205)Instruction limit reached! % 229.90/32.70 % (379205)------------------------------ % 229.90/32.70 % (379205)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 229.90/32.70 % (379205)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 229.90/32.70 % (379205)CaDiCaL version: 2.1.3 % 229.90/32.70 % (379205)Termination reason: Instruction limit % 229.90/32.70 % (379205)Termination phase: Saturation % 229.90/32.70 % (379205)Time elapsed: 0.184 s % 229.90/32.70 % (379205)Peak memory usage: 14 MB % 229.90/32.70 % (379205)Instructions burned: 262 (million) % 229.90/32.70 % (379207)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=1728378752:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2745 on theBenchmark for (2745ds/1368Mi) % 229.90/32.70 % (379207)Instruction limit reached! % 229.90/32.70 % (379207)------------------------------ % 229.90/32.70 % (379207)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 229.90/32.70 % (379207)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 229.90/32.70 % (379207)CaDiCaL version: 2.1.3 % 229.90/32.70 % (379207)Termination reason: Instruction limit % 229.90/32.70 % (379207)Termination phase: Saturation % 229.90/32.70 % (379207)Time elapsed: 0.712 s % 229.90/32.70 % (379207)Peak memory usage: 20 MB % 229.90/32.70 % (379207)Instructions burned: 1370 (million) % 229.90/32.70 % (379209)ott-21_1_sil=16000:si=on:fs=off:random_seed=907148709:i=360:av=off:fsr=off:rtra=on_2737 on theBenchmark for (2737ds/360Mi) % 229.90/32.70 % (379209)Instruction limit reached! % 229.90/32.70 % (379209)------------------------------ % 229.90/32.70 % (379209)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 229.90/32.70 % (379209)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 229.90/32.70 % (379209)CaDiCaL version: 2.1.3 % 229.90/32.70 % (379209)Termination reason: Instruction limit % 229.90/32.70 % (379209)Termination phase: Saturation % 229.90/32.70 % (379209)Time elapsed: 0.171 s % 229.90/32.70 % (379209)Peak memory usage: 13 MB % 229.90/32.70 % (379209)Instructions burned: 361 (million) % 229.90/32.70 % (379211)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2334332075:i=954:bd=all:rtra=on_2735 on theBenchmark for (2735ds/954Mi) % 229.90/32.70 % (379211)Instruction limit reached! % 229.90/32.70 % (379211)------------------------------ % 229.90/32.70 % (379211)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 229.90/32.70 % (379211)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 229.90/32.70 % (379211)CaDiCaL version: 2.1.3 % 229.90/32.70 % (379211)Termination reason: Instruction limit % 229.90/32.70 % (379211)Termination phase: Saturation % 229.90/32.70 % (379211)Time elapsed: 0.572 s % 229.90/32.70 % (379211)Peak memory usage: 16 MB % 229.90/32.70 % (379211)Instructions burned: 954 (million) % 229.90/32.70 % (379213)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=2565024027:fmbsr=1.3:i=1730:ins=25:rtra=on_2729 on theBenchmark for (2729ds/1730Mi) % 229.90/32.70 % (379213)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 229.90/32.70 % (379213)Terminated due to inappropriate strategy. % 229.90/32.70 % (379213)------------------------------ % 229.90/32.70 % (379213)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 229.90/32.70 % (379213)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 229.90/32.70 % (379213)CaDiCaL version: 2.1.3 % 229.90/32.70 % (379213)Termination reason: Inappropriate % 229.90/32.70 % (379213)Time elapsed: 0.003 s % 229.90/32.70 % (379213)Peak memory usage: 10 MB % 229.90/32.70 % (379213)Instructions burned: 5 (million) % 229.90/32.70 % (379213)------------------------------ % 229.90/32.70 % (379213)------------------------------ % 229.90/32.70 % (379215)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=436454720:i=2358:rtra=on_2729 on theBenchmark for (2729ds/2358Mi) % 229.90/32.70 % (379215)Instruction limit reached! % 229.90/32.70 % (379215)------------------------------ % 229.90/32.70 % (379215)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 229.90/32.70 % (379215)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 229.90/32.70 % (379215)CaDiCaL version: 2.1.3 % 229.90/32.70 % (379215)Termination reason: Instruction limit % 229.90/32.70 % (379215)Termination phase: Saturation % 264.68/37.51 % (379215)Time elapsed: 1.601 s % 264.68/37.51 % (379215)Peak memory usage: 27 MB % 264.68/37.51 % (379215)Instructions burned: 2358 (million) % 264.68/37.51 % (379217)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=4263941577:i=1778:ins=1:rtra=on_2713 on theBenchmark for (2713ds/1778Mi) % 264.68/37.51 % (379217)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 264.68/37.51 % (379217)Terminated due to inappropriate strategy. % 264.68/37.51 % (379217)------------------------------ % 264.68/37.51 % (379217)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 264.68/37.51 % (379217)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 264.68/37.51 % (379217)CaDiCaL version: 2.1.3 % 264.68/37.51 % (379217)Termination reason: Inappropriate % 264.68/37.51 % (379217)Time elapsed: 0.003 s % 264.68/37.51 % (379217)Peak memory usage: 10 MB % 264.68/37.51 % (379217)Instructions burned: 5 (million) % 264.68/37.51 % (379217)------------------------------ % 264.68/37.51 % (379217)------------------------------ % 264.68/37.51 % (379219)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=349785647:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2712 on theBenchmark for (2712ds/1384Mi) % 264.68/37.51 % (379219)Instruction limit reached! % 264.68/37.51 % (379219)------------------------------ % 264.68/37.51 % (379219)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 264.68/37.51 % (379219)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 264.68/37.51 % (379219)CaDiCaL version: 2.1.3 % 264.68/37.51 % (379219)Termination reason: Instruction limit % 264.68/37.51 % (379219)Termination phase: Saturation % 264.68/37.51 % (379219)Time elapsed: 0.954 s % 264.68/37.51 % (379219)Peak memory usage: 25 MB % 264.68/37.51 % (379219)Instructions burned: 1384 (million) % 264.68/37.51 % (379283)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=2496421265:i=1758:kws=inv_precedence:fsr=off:rtra=on_2703 on theBenchmark for (2703ds/1758Mi) % 264.68/37.51 % (379172)Instruction limit reached! % 264.68/37.51 % (379172)------------------------------ % 264.68/37.51 % (379172)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 264.68/37.51 % (379172)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 264.68/37.51 % (379172)CaDiCaL version: 2.1.3 % 264.68/37.51 % (379172)Termination reason: Instruction limit % 264.68/37.51 % (379172)Termination phase: Saturation % 264.68/37.51 % (379172)Time elapsed: 13.959 s % 264.68/37.51 % (379172)Peak memory usage: 387 MB % 264.68/37.51 % (379172)Instructions burned: 53296 (million) % 264.68/37.51 % (379285)fmb+10_1_sil=64000:si=on:random_seed=3235422374:i=44122:nm=2:rtra=on:gsp=on_2700 on theBenchmark for (2700ds/44122Mi) % 264.68/37.51 % (379285)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 264.68/37.51 % (379285)Terminated due to inappropriate strategy. % 264.68/37.51 % (379285)------------------------------ % 264.68/37.51 % (379285)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 264.68/37.51 % (379285)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 264.68/37.51 % (379285)CaDiCaL version: 2.1.3 % 264.68/37.51 % (379285)Termination reason: Inappropriate % 264.68/37.51 % (379285)Time elapsed: 0.002 s % 264.68/37.51 % (379285)Peak memory usage: 11 MB % 264.68/37.51 % (379285)Instructions burned: 5 (million) % 264.68/37.51 % (379285)------------------------------ % 264.68/37.51 % (379285)------------------------------ % 264.68/37.51 % (379287)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=3617767832:i=19030:nm=5:rtra=on_2699 on theBenchmark for (2699ds/19030Mi) % 264.68/37.51 % (379287)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 264.68/37.51 % (379287)Terminated due to inappropriate strategy. % 264.68/37.51 % (379287)------------------------------ % 264.68/37.51 % (379287)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 264.68/37.51 % (379287)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 264.68/37.51 % (379287)CaDiCaL version: 2.1.3 % 264.68/37.51 % (379287)Termination reason: Inappropriate % 264.68/37.51 % (379287)Time elapsed: 0.001 s % 264.68/37.51 % (379287)Peak memory usage: 11 MB % 264.68/37.51 % (379287)Instructions burned: 4 (million) % 264.68/37.51 % (379287)------------------------------ % 264.68/37.51 % (379287)------------------------------ % 264.68/37.51 % (379289)fmb+10_1_sil=64000:sas=cadical:si=on:fmbss=8:random_seed=308078203:fmbsr=1.7:i=1840:rtra=on_2699 on theBenchmark for (2699ds/1840Mi) % 244.93/40.58 % (379289)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 244.93/40.58 % (379289)Terminated due to inappropriate strategy. % 244.93/40.58 % (379289)------------------------------ % 244.93/40.58 % (379289)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 244.93/40.58 % (379289)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 244.93/40.58 % (379289)CaDiCaL version: 2.1.3 % 244.93/40.58 % (379289)Termination reason: Inappropriate % 244.93/40.58 % (379289)Time elapsed: 0.001 s % 244.93/40.58 % (379289)Peak memory usage: 11 MB % 244.93/40.58 % (379289)Instructions burned: 5 (million) % 244.93/40.58 % (379289)------------------------------ % 244.93/40.58 % (379289)------------------------------ % 244.93/40.58 % (379291)dis-4_1_sil=16000:drc=ordering:si=on:sp=const_frequency:sac=on:newcnf=on:random_seed=1534344178:i=10262:rtra=on_2699 on theBenchmark for (2699ds/10262Mi) % 244.93/40.58 % (379283)Instruction limit reached! % 244.93/40.58 % (379283)------------------------------ % 244.93/40.58 % (379283)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 244.93/40.58 % (379283)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 244.93/40.58 % (379283)CaDiCaL version: 2.1.3 % 244.93/40.58 % (379283)Termination reason: Instruction limit % 244.93/40.58 % (379283)Termination phase: Saturation % 244.93/40.58 % (379283)Time elapsed: 1.047 s % 244.93/40.58 % (379283)Peak memory usage: 29 MB % 244.93/40.58 % (379283)Instructions burned: 1758 (million) % 244.93/40.58 % (379293)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:si=on:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1402642069:i=2944:ins=7:rtra=on:fdi=8:gsp=on_2692 on theBenchmark for (2692ds/2944Mi) % 244.93/40.58 % (379293)Instruction limit reached! % 244.93/40.58 % (379293)------------------------------ % 244.93/40.58 % (379293)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 244.93/40.58 % (379293)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 244.93/40.58 % (379293)CaDiCaL version: 2.1.3 % 244.93/40.58 % (379293)Termination reason: Instruction limit % 244.93/40.58 % (379293)Termination phase: Saturation % 244.93/40.58 % (379293)Time elapsed: 1.662 s % 244.93/40.58 % (379293)Peak memory usage: 33 MB % 244.93/40.58 % (379293)Instructions burned: 2944 (million) % 244.93/40.58 % (379295)fmb+10_1_sil=16000:sas=cadical:si=on:bce=on:fmbss=77:random_seed=1057165656:i=12648:rtra=on_2675 on theBenchmark for (2675ds/12648Mi) % 244.93/40.58 % (379295)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 244.93/40.58 % (379295)Terminated due to inappropriate strategy. % 244.93/40.58 % (379295)------------------------------ % 244.93/40.58 % (379295)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 244.93/40.58 % (379295)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 244.93/40.58 % (379295)CaDiCaL version: 2.1.3 % 244.93/40.58 % (379295)Termination reason: Inappropriate % 244.93/40.58 % (379295)Time elapsed: 0.003 s % 244.93/40.58 % (379295)Peak memory usage: 11 MB % 244.93/40.58 % (379295)Instructions burned: 5 (million) % 244.93/40.58 % (379295)------------------------------ % 244.93/40.58 % (379295)------------------------------ % 244.93/40.58 % (379176)Instruction limit reached! % 244.93/40.58 % (379176)------------------------------ % 244.93/40.58 % (379176)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 244.93/40.58 % (379176)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 244.93/40.58 % (379176)CaDiCaL version: 2.1.3 % 244.93/40.58 % (379176)Termination reason: Instruction limit % 244.93/40.58 % (379176)Termination phase: Saturation % 244.93/40.58 % (379176)Time elapsed: 13.994 s % 244.93/40.58 % (379176)Peak memory usage: 37 MB % 244.93/40.58 % (379176)Instructions burned: 28121 (million) % 244.93/40.58 % (379297)fmb+10_1_fmbas=function:sil=32000:sas=cadical:si=on:fmbss=16:random_seed=2195385956:fmbsr=2.30978:i=4348:rtra=on_2675 on theBenchmark for (2675ds/4348Mi) % 244.93/40.58 % (379297)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 244.93/40.58 % (379297)Terminated due to inappropriate strategy. % 244.93/40.58 % (379297)------------------------------ % 244.93/40.58 % (379297)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 244.93/40.58 % (379297)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 244.93/40.58 % (379297)CaDiCaL version: 2.1.3 % 244.93/40.58 % (379297)Termination reason: Inappropriate % 244.93/40.58 % (379297)Time elapsed: 0.003 s % 244.93/40.58 % (379297)Peak memory usage: 11 MB % 244.93/40.58 % (379297)Instructions burned: 5 (million) % 300.18/42.53 % (379297)------------------------------ % 300.18/42.53 % (379297)------------------------------ % 300.18/42.53 % (379299)ott-2_1_sil=16000:si=on:newcnf=on:random_seed=91594784:avsq=on:i=1738:avsqr=1,16:kws=inv_arity_squared:rtra=on_2675 on theBenchmark for (2675ds/1738Mi) % 300.18/42.53 % (379300)ott+10_1_sil=32000:tgt=ground:si=on:random_seed=290014126:i=10228:av=off:rtra=on_2675 on theBenchmark for (2675ds/10228Mi) % 300.18/42.53 % (379291)Instruction limit reached! % 300.18/42.53 % (379291)------------------------------ % 300.18/42.53 % (379291)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.18/42.53 % (379291)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.18/42.53 % (379291)CaDiCaL version: 2.1.3 % 300.18/42.53 % (379291)Termination reason: Instruction limit % 300.18/42.53 % (379291)Termination phase: Saturation % 300.18/42.53 % (379291)Time elapsed: 3.281 s % 300.18/42.53 % (379291)Peak memory usage: 69 MB % 300.18/42.53 % (379291)Instructions burned: 10265 (million) % 300.18/42.53 % (379303)fmb+10_1_sil=64000:sas=cadical:si=on:bce=on:rp=on:random_seed=4277258448:i=108564:rtra=on_2666 on theBenchmark for (2666ds/108564Mi) % 300.18/42.53 % (379303)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 300.18/42.53 % (379303)Terminated due to inappropriate strategy. % 300.18/42.53 % (379303)------------------------------ % 300.18/42.53 % (379303)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.18/42.53 % (379303)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.18/42.53 % (379303)CaDiCaL version: 2.1.3 % 300.18/42.53 % (379303)Termination reason: Inappropriate % 300.18/42.53 % (379303)Time elapsed: 0.002 s % 300.18/42.53 % (379303)Peak memory usage: 11 MB % 300.18/42.53 % (379303)Instructions burned: 5 (million) % 300.18/42.53 % (379303)------------------------------ % 300.18/42.53 % (379303)------------------------------ % 300.18/42.53 % (379305)dis-11_1_sil=16000:si=on:sp=reverse_frequency:alpa=true:random_seed=1571495733:i=7024:aac=none:rtra=on_2666 on theBenchmark for (2666ds/7024Mi) % 300.18/42.53 % (379299)Instruction limit reached! % 300.18/42.53 % (379299)------------------------------ % 300.18/42.53 % (379299)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.18/42.53 % (379299)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.18/42.53 % (379299)CaDiCaL version: 2.1.3 % 300.18/42.53 % (379299)Termination reason: Instruction limit % 300.18/42.53 % (379299)Termination phase: Saturation % 300.18/42.53 % (379299)Time elapsed: 1.103 s % 300.18/42.53 % (379299)Peak memory usage: 20 MB % 300.18/42.53 % (379299)Instructions burned: 1739 (million) % 300.18/42.53 % (379307)dis+21_1_sil=32000:sas=cadical:si=on:random_seed=2928766070:i=7546:rtra=on:amm=off_2663 on theBenchmark for (2663ds/7546Mi) % 300.18/42.53 % (379305)Instruction limit reached! % 300.18/42.53 % (379305)------------------------------ % 300.18/42.53 % (379305)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.18/42.53 % (379305)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.18/42.53 % (379305)CaDiCaL version: 2.1.3 % 300.18/42.53 % (379305)Termination reason: Instruction limit % 300.18/42.53 % (379305)Termination phase: Saturation % 300.18/42.53 % (379305)Time elapsed: 2.346 s % 300.18/42.53 % (379305)Peak memory usage: 47 MB % 300.18/42.53 % (379305)Instructions burned: 7027 (million) % 300.18/42.53 % (379309)ott+11_1_sil=16000:si=on:gs=on:random_seed=133388092:s2a=on:i=4502:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:rtra=on:fsd=on_2642 on theBenchmark for (2642ds/4502Mi) % 300.18/42.53 % (379309)Instruction limit reached! % 300.18/42.53 % (379309)------------------------------ % 300.18/42.53 % (379309)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.18/42.53 % (379309)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.18/42.53 % (379309)CaDiCaL version: 2.1.3 % 300.18/42.53 % (379309)Termination reason: Instruction limit % 300.18/42.53 % (379309)Termination phase: Saturation % 300.18/42.53 % (379309)Time elapsed: 1.565 s % 300.18/42.53 % (379309)Peak memory usage: 37 MB % 300.18/42.53 % (379309)Instructions burned: 4502 (million) % 300.18/42.53 % (379311)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:si=on:fmbss=7:random_seed=1412551746:fmbsr=1.6:i=135068:rtra=on_2627 on theBenchmark for (2627ds/135068Mi) % 300.18/42.53 % (379311)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 300.18/42.53 % (379311)Terminated due to inappropriate strategy. % 300.18/42.53 % (379311)------------------------------ % 300.18/42.53 % (379311)Version: Vampire 5.0.1 % 300.18/42.54 Terminated % 300.18/42.54 % Vampire exiting %------------------------------------------------------------------------------