%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWW668_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 : n007.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:37 PM UTC 2026 % Result : Timeout 300.67s 42.54s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWW668_2 : TPTP v9.3.1. Released v6.1.0. % 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.09/0.19 % Computer : n007.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 14:22:25 UTC 2026 % 0.09/0.20 % CPUTime : % 0.09/0.20 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.09/0.22 Running first-order model finding % 0.09/0.22 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 % 3.69/0.88 % (2418399)Will run a generic schedule for satisfiability detection. % 3.69/0.88 % (2418404)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=333394563_2999 on theBenchmark for (2999ds/0Mi) % 3.69/0.88 % (2418405)% WARNING: option uhcvi not known. % 3.69/0.88 % (2418404)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.69/0.88 % (2418404)Terminated due to inappropriate strategy. % 3.69/0.88 % (2418404)------------------------------ % 3.69/0.88 % (2418404)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.69/0.88 % (2418404)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.69/0.88 % (2418404)CaDiCaL version: 2.1.3 % 3.69/0.88 % (2418404)Termination reason: Inappropriate % 3.69/0.88 % (2418404)Time elapsed: 0.002 s % 3.69/0.88 % (2418404)Peak memory usage: 11 MB % 3.69/0.88 % (2418404)Instructions burned: 7 (million) % 3.69/0.88 % (2418404)------------------------------ % 3.69/0.88 % (2418404)------------------------------ % 3.69/0.88 % (2418406)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1110416614:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 3.69/0.88 % (2418405)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3284817669:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 3.69/0.88 % (2418407)dis+10_1_sil=32000:sp=arity:random_seed=1688569037:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 3.69/0.88 % (2418408)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2955809738:i=116_2999 on theBenchmark for (2999ds/116Mi) % 3.69/0.88 % (2418409)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1012933723:i=131_2999 on theBenchmark for (2999ds/131Mi) % 3.69/0.88 % (2418410)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=4109714846:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 3.69/0.88 % (2418412)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1063797023:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 3.69/0.88 % (2418412)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.69/0.88 % (2418412)Terminated due to inappropriate strategy. % 3.69/0.88 % (2418412)------------------------------ % 3.69/0.88 % (2418412)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.69/0.88 % (2418412)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.69/0.88 % (2418412)CaDiCaL version: 2.1.3 % 3.69/0.88 % (2418412)Termination reason: Inappropriate % 3.69/0.88 % (2418412)Time elapsed: 0.004 s % 3.69/0.88 % (2418412)Peak memory usage: 10 MB % 3.69/0.88 % (2418412)Instructions burned: 6 (million) % 3.69/0.88 % (2418412)------------------------------ % 3.69/0.88 % (2418412)------------------------------ % 3.69/0.88 % (2418420)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3042603270:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 3.69/0.88 % (2418407)Instruction limit reached! % 3.69/0.88 % (2418407)------------------------------ % 3.69/0.88 % (2418407)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.69/0.88 % (2418407)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.69/0.88 % (2418407)CaDiCaL version: 2.1.3 % 3.69/0.88 % (2418407)Termination reason: Instruction limit % 3.69/0.88 % (2418407)Termination phase: Saturation % 3.69/0.88 % (2418407)Time elapsed: 0.067 s % 3.69/0.88 % (2418407)Peak memory usage: 13 MB % 3.69/0.88 % (2418407)Instructions burned: 105 (million) % 3.69/0.88 % (2418408)Instruction limit reached! % 3.69/0.88 % (2418408)------------------------------ % 3.69/0.88 % (2418408)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.69/0.88 % (2418408)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.69/0.88 % (2418408)CaDiCaL version: 2.1.3 % 3.69/0.88 % (2418408)Termination reason: Instruction limit % 3.69/0.88 % (2418408)Termination phase: Saturation % 3.69/0.88 % (2418408)Time elapsed: 0.076 s % 3.69/0.88 % (2418408)Peak memory usage: 13 MB % 3.69/0.88 % (2418408)Instructions burned: 117 (million) % 3.69/0.88 % (2418409)Instruction limit reached! % 3.69/0.88 % (2418409)------------------------------ % 3.69/0.88 % (2418409)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.69/0.88 % (2418409)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.69/0.88 % (2418409)CaDiCaL version: 2.1.3 % 3.69/0.88 % (2418409)Termination reason: Instruction limit % 7.35/1.34 % (2418409)Termination phase: Saturation % 7.35/1.34 % (2418409)Time elapsed: 0.081 s % 7.35/1.34 % (2418409)Peak memory usage: 13 MB % 7.35/1.34 % (2418409)Instructions burned: 131 (million) % 7.35/1.34 % (2418422)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=768174957:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi) % 7.35/1.34 % (2418424)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3672277730:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 7.35/1.34 % (2418423)ott-21_1_sil=16000:fs=off:random_seed=1392314380:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 7.35/1.34 % (2418420)Instruction limit reached! % 7.35/1.34 % (2418420)------------------------------ % 7.35/1.34 % (2418420)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.35/1.34 % (2418420)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.35/1.34 % (2418420)CaDiCaL version: 2.1.3 % 7.35/1.34 % (2418420)Termination reason: Instruction limit % 7.35/1.34 % (2418420)Termination phase: Saturation % 7.35/1.34 % (2418420)Time elapsed: 0.112 s % 7.35/1.34 % (2418420)Peak memory usage: 13 MB % 7.35/1.34 % (2418420)Instructions burned: 133 (million) % 7.35/1.34 % (2418428)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3167509214:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 7.35/1.34 % (2418428)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 7.35/1.34 % (2418428)Terminated due to inappropriate strategy. % 7.35/1.34 % (2418428)------------------------------ % 7.35/1.34 % (2418428)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.35/1.34 % (2418428)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.35/1.34 % (2418428)CaDiCaL version: 2.1.3 % 7.35/1.34 % (2418428)Termination reason: Inappropriate % 7.35/1.34 % (2418428)Time elapsed: 0.004 s % 7.35/1.34 % (2418428)Peak memory usage: 10 MB % 7.35/1.34 % (2418428)Instructions burned: 6 (million) % 7.35/1.34 % (2418428)------------------------------ % 7.35/1.34 % (2418428)------------------------------ % 7.35/1.34 % (2418423)Instruction limit reached! % 7.35/1.34 % (2418423)------------------------------ % 7.35/1.34 % (2418423)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.35/1.34 % (2418423)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.35/1.34 % (2418423)CaDiCaL version: 2.1.3 % 7.35/1.34 % (2418423)Termination reason: Instruction limit % 7.35/1.34 % (2418423)Termination phase: Saturation % 7.35/1.34 % (2418423)Time elapsed: 0.090 s % 7.35/1.34 % (2418423)Peak memory usage: 12 MB % 7.35/1.34 % (2418423)Instructions burned: 180 (million) % 7.35/1.34 % (2418410)Instruction limit reached! % 7.35/1.34 % (2418410)------------------------------ % 7.35/1.34 % (2418410)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.35/1.34 % (2418410)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.35/1.34 % (2418410)CaDiCaL version: 2.1.3 % 7.35/1.34 % (2418410)Termination reason: Instruction limit % 7.35/1.34 % (2418410)Termination phase: Saturation % 7.35/1.34 % (2418410)Time elapsed: 0.173 s % 7.35/1.34 % (2418410)Peak memory usage: 13 MB % 7.35/1.34 % (2418410)Instructions burned: 159 (million) % 7.35/1.34 % (2418430)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1989368186:i=1179_2997 on theBenchmark for (2997ds/1179Mi) % 7.35/1.34 % (2418432)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=2440538625: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) % 7.35/1.34 % (2418431)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3995531421:i=889:ins=1_2997 on theBenchmark for (2997ds/889Mi) % 7.35/1.34 % (2418431)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 7.35/1.34 % (2418431)Terminated due to inappropriate strategy. % 7.35/1.34 % (2418431)------------------------------ % 7.35/1.34 % (2418431)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.35/1.34 % (2418431)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.35/1.34 % (2418431)CaDiCaL version: 2.1.3 % 7.35/1.34 % (2418431)Termination reason: Inappropriate % 7.35/1.34 % (2418431)Time elapsed: 0.004 s % 7.35/1.34 % (2418431)Peak memory usage: 10 MB % 29.59/4.49 % (2418431)Instructions burned: 6 (million) % 29.59/4.49 % (2418431)------------------------------ % 29.59/4.49 % (2418431)------------------------------ % 29.59/4.49 % (2418446)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=301796858:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi) % 29.59/4.49 % (2418424)Instruction limit reached! % 29.59/4.49 % (2418424)------------------------------ % 29.59/4.49 % (2418424)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 29.59/4.49 % (2418424)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.59/4.49 % (2418424)CaDiCaL version: 2.1.3 % 29.59/4.49 % (2418424)Termination reason: Instruction limit % 29.59/4.49 % (2418424)Termination phase: Saturation % 29.59/4.49 % (2418424)Time elapsed: 0.173 s % 29.59/4.49 % (2418424)Peak memory usage: 14 MB % 29.59/4.49 % (2418424)Instructions burned: 477 (million) % 29.59/4.49 % (2418460)fmb+10_1_sil=64000:random_seed=15956114:i=22061:nm=2:gsp=on_2996 on theBenchmark for (2996ds/22061Mi) % 29.59/4.49 % (2418460)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 29.59/4.49 % (2418460)Terminated due to inappropriate strategy. % 29.59/4.49 % (2418460)------------------------------ % 29.59/4.49 % (2418460)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 29.59/4.49 % (2418460)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.59/4.49 % (2418460)CaDiCaL version: 2.1.3 % 29.59/4.49 % (2418460)Termination reason: Inappropriate % 29.59/4.49 % (2418460)Time elapsed: 0.002 s % 29.59/4.49 % (2418460)Peak memory usage: 10 MB % 29.59/4.49 % (2418460)Instructions burned: 6 (million) % 29.59/4.49 % (2418460)------------------------------ % 29.59/4.49 % (2418460)------------------------------ % 29.59/4.49 % (2418468)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3820586568:i=9515:nm=5_2996 on theBenchmark for (2996ds/9515Mi) % 29.59/4.49 % (2418468)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 29.59/4.49 % (2418468)Terminated due to inappropriate strategy. % 29.59/4.49 % (2418468)------------------------------ % 29.59/4.49 % (2418468)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 29.59/4.49 % (2418468)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.59/4.49 % (2418468)CaDiCaL version: 2.1.3 % 29.59/4.49 % (2418468)Termination reason: Inappropriate % 29.59/4.49 % (2418468)Time elapsed: 0.002 s % 29.59/4.49 % (2418468)Peak memory usage: 11 MB % 29.59/4.49 % (2418468)Instructions burned: 6 (million) % 29.59/4.49 % (2418468)------------------------------ % 29.59/4.49 % (2418468)------------------------------ % 29.59/4.49 % (2418476)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=587839453:fmbsr=1.7:i=920_2996 on theBenchmark for (2996ds/920Mi) % 29.59/4.49 % (2418476)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 29.59/4.49 % (2418476)Terminated due to inappropriate strategy. % 29.59/4.49 % (2418476)------------------------------ % 29.59/4.49 % (2418476)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 29.59/4.49 % (2418476)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.59/4.49 % (2418476)CaDiCaL version: 2.1.3 % 29.59/4.49 % (2418476)Termination reason: Inappropriate % 29.59/4.49 % (2418476)Time elapsed: 0.002 s % 29.59/4.49 % (2418476)Peak memory usage: 11 MB % 29.59/4.49 % (2418476)Instructions burned: 6 (million) % 29.59/4.49 % (2418476)------------------------------ % 29.59/4.49 % (2418476)------------------------------ % 29.59/4.49 % (2418483)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=3853410766:i=5131_2996 on theBenchmark for (2996ds/5131Mi) % 29.59/4.49 % (2418422)Instruction limit reached! % 29.59/4.49 % (2418422)------------------------------ % 29.59/4.49 % (2418422)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 29.59/4.49 % (2418422)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.59/4.49 % (2418422)CaDiCaL version: 2.1.3 % 29.59/4.49 % (2418422)Termination reason: Instruction limit % 29.59/4.49 % (2418422)Termination phase: Saturation % 29.59/4.49 % (2418422)Time elapsed: 0.360 s % 29.59/4.49 % (2418422)Peak memory usage: 17 MB % 29.59/4.49 % (2418422)Instructions burned: 686 (million) % 29.59/4.49 % (2418531)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2547559306:i=1472:ins=7:fdi=8:gsp=on_2995 on theBenchmark for (2995ds/1472Mi) % 29.59/4.49 % (2418432)Instruction limit reached! % 29.59/4.49 % (2418432)------------------------------ % 41.22/6.13 % (2418432)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 41.22/6.13 % (2418432)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 41.22/6.13 % (2418432)CaDiCaL version: 2.1.3 % 41.22/6.13 % (2418432)Termination reason: Instruction limit % 41.22/6.13 % (2418432)Termination phase: Saturation % 41.22/6.13 % (2418432)Time elapsed: 0.401 s % 41.22/6.13 % (2418432)Peak memory usage: 17 MB % 41.22/6.13 % (2418432)Instructions burned: 694 (million) % 41.22/6.13 % (2418569)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=2205021078:i=6324_2993 on theBenchmark for (2993ds/6324Mi) % 41.22/6.13 % (2418569)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 41.22/6.13 % (2418569)Terminated due to inappropriate strategy. % 41.22/6.13 % (2418569)------------------------------ % 41.22/6.13 % (2418569)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 41.22/6.13 % (2418569)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 41.22/6.13 % (2418569)CaDiCaL version: 2.1.3 % 41.22/6.13 % (2418569)Termination reason: Inappropriate % 41.22/6.13 % (2418569)Time elapsed: 0.005 s % 41.22/6.13 % (2418569)Peak memory usage: 11 MB % 41.22/6.13 % (2418569)Instructions burned: 7 (million) % 41.22/6.13 % (2418569)------------------------------ % 41.22/6.13 % (2418569)------------------------------ % 41.22/6.13 % (2418575)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1024594029:fmbsr=2.30978:i=2174_2993 on theBenchmark for (2993ds/2174Mi) % 41.22/6.13 % (2418575)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 41.22/6.13 % (2418575)Terminated due to inappropriate strategy. % 41.22/6.13 % (2418575)------------------------------ % 41.22/6.13 % (2418575)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 41.22/6.13 % (2418575)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 41.22/6.13 % (2418575)CaDiCaL version: 2.1.3 % 41.22/6.13 % (2418575)Termination reason: Inappropriate % 41.22/6.13 % (2418575)Time elapsed: 0.006 s % 41.22/6.13 % (2418575)Peak memory usage: 10 MB % 41.22/6.13 % (2418575)Instructions burned: 6 (million) % 41.22/6.13 % (2418575)------------------------------ % 41.22/6.13 % (2418575)------------------------------ % 41.22/6.13 % (2418591)ott-2_1_sil=16000:newcnf=on:random_seed=329264259:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2992 on theBenchmark for (2992ds/869Mi) % 41.22/6.13 % (2418446)Instruction limit reached! % 41.22/6.13 % (2418446)------------------------------ % 41.22/6.13 % (2418446)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 41.22/6.13 % (2418446)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 41.22/6.13 % (2418446)CaDiCaL version: 2.1.3 % 41.22/6.13 % (2418446)Termination reason: Instruction limit % 41.22/6.13 % (2418446)Termination phase: Saturation % 41.22/6.13 % (2418446)Time elapsed: 0.595 s % 41.22/6.13 % (2418446)Peak memory usage: 19 MB % 41.22/6.13 % (2418446)Instructions burned: 879 (million) % 41.22/6.13 % (2418608)ott+10_1_sil=32000:tgt=ground:random_seed=3798950551:i=5114:av=off_2991 on theBenchmark for (2991ds/5114Mi) % 41.22/6.13 % (2418430)Instruction limit reached! % 41.22/6.13 % (2418430)------------------------------ % 41.22/6.13 % (2418430)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 41.22/6.13 % (2418430)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 41.22/6.13 % (2418430)CaDiCaL version: 2.1.3 % 41.22/6.13 % (2418430)Termination reason: Instruction limit % 41.22/6.13 % (2418430)Termination phase: Saturation % 41.22/6.13 % (2418430)Time elapsed: 0.840 s % 41.22/6.13 % (2418430)Peak memory usage: 20 MB % 41.22/6.13 % (2418430)Instructions burned: 1179 (million) % 41.22/6.13 % (2418620)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=1102344033:i=54282_2989 on theBenchmark for (2989ds/54282Mi) % 41.22/6.13 % (2418620)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 41.22/6.13 % (2418620)Terminated due to inappropriate strategy. % 41.22/6.13 % (2418620)------------------------------ % 41.22/6.13 % (2418620)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 41.22/6.13 % (2418620)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 41.22/6.13 % (2418620)CaDiCaL version: 2.1.3 % 41.22/6.13 % (2418620)Termination reason: Inappropriate % 41.22/6.13 % (2418620)Time elapsed: 0.006 s % 41.22/6.13 % (2418620)Peak memory usage: 11 MB % 41.22/6.13 % (2418620)Instructions burned: 7 (million) % 135.62/19.31 % (2418620)------------------------------ % 135.62/19.31 % (2418620)------------------------------ % 135.62/19.31 % (2418622)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=2854718149:i=3512:aac=none_2988 on theBenchmark for (2988ds/3512Mi) % 135.62/19.31 % (2418591)Instruction limit reached! % 135.62/19.31 % (2418591)------------------------------ % 135.62/19.31 % (2418591)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 135.62/19.31 % (2418591)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 135.62/19.31 % (2418591)CaDiCaL version: 2.1.3 % 135.62/19.31 % (2418591)Termination reason: Instruction limit % 135.62/19.31 % (2418591)Termination phase: Saturation % 135.62/19.31 % (2418591)Time elapsed: 0.818 s % 135.62/19.31 % (2418591)Peak memory usage: 16 MB % 135.62/19.31 % (2418591)Instructions burned: 870 (million) % 135.62/19.31 % (2418634)dis+21_1_sil=32000:sas=cadical:random_seed=548752789:i=3773:amm=off_2984 on theBenchmark for (2984ds/3773Mi) % 135.62/19.31 % (2418531)Instruction limit reached! % 135.62/19.31 % (2418531)------------------------------ % 135.62/19.31 % (2418531)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 135.62/19.31 % (2418531)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 135.62/19.31 % (2418531)CaDiCaL version: 2.1.3 % 135.62/19.31 % (2418531)Termination reason: Instruction limit % 135.62/19.31 % (2418531)Termination phase: Saturation % 135.62/19.31 % (2418531)Time elapsed: 1.142 s % 135.62/19.31 % (2418531)Peak memory usage: 20 MB % 135.62/19.31 % (2418531)Instructions burned: 1472 (million) % 135.62/19.31 % (2418641)ott+11_1_sil=16000:gs=on:random_seed=1643358582:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2983 on theBenchmark for (2983ds/2251Mi) % 135.62/19.31 % (2418641)Instruction limit reached! % 135.62/19.31 % (2418641)------------------------------ % 135.62/19.31 % (2418641)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 135.62/19.31 % (2418641)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 135.62/19.31 % (2418641)CaDiCaL version: 2.1.3 % 135.62/19.31 % (2418641)Termination reason: Instruction limit % 135.62/19.31 % (2418641)Termination phase: Saturation % 135.62/19.31 % (2418641)Time elapsed: 0.690 s % 135.62/19.31 % (2418641)Peak memory usage: 15 MB % 135.62/19.31 % (2418641)Instructions burned: 2253 (million) % 135.62/19.31 % (2418652)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=3408068328:fmbsr=1.6:i=67534_2976 on theBenchmark for (2976ds/67534Mi) % 135.62/19.31 % (2418652)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 135.62/19.31 % (2418652)Terminated due to inappropriate strategy. % 135.62/19.31 % (2418652)------------------------------ % 135.62/19.31 % (2418652)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 135.62/19.31 % (2418652)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 135.62/19.31 % (2418652)CaDiCaL version: 2.1.3 % 135.62/19.31 % (2418652)Termination reason: Inappropriate % 135.62/19.31 % (2418652)Time elapsed: 0.002 s % 135.62/19.31 % (2418652)Peak memory usage: 11 MB % 135.62/19.31 % (2418652)Instructions burned: 7 (million) % 135.62/19.31 % (2418652)------------------------------ % 135.62/19.31 % (2418652)------------------------------ % 135.62/19.31 % (2418654)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=2252918177:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2976 on theBenchmark for (2976ds/4591Mi) % 135.62/19.31 % (2418483)Instruction limit reached! % 135.62/19.31 % (2418483)------------------------------ % 135.62/19.31 % (2418483)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 135.62/19.31 % (2418483)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 135.62/19.31 % (2418483)CaDiCaL version: 2.1.3 % 135.62/19.31 % (2418483)Termination reason: Instruction limit % 135.62/19.31 % (2418483)Termination phase: Saturation % 135.62/19.31 % (2418483)Time elapsed: 3.255 s % 135.62/19.31 % (2418483)Peak memory usage: 35 MB % 135.62/19.31 % (2418483)Instructions burned: 5131 (million) % 135.62/19.31 % (2418659)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=2578751932:i=29340_2963 on theBenchmark for (2963ds/29340Mi) % 135.62/19.31 % (2418654)Instruction limit reached! % 135.62/19.31 % (2418654)------------------------------ % 135.62/19.31 % (2418654)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 135.62/19.31 % (2418654)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 135.62/19.31 % (2418654)CaDiCaL version: 2.1.3 % 135.62/19.31 % (2418654)Termination reason: Instruction limit % 193.69/27.52 % (2418654)Termination phase: Saturation % 193.69/27.52 % (2418654)Time elapsed: 1.874 s % 193.69/27.52 % (2418654)Peak memory usage: 25 MB % 193.69/27.52 % (2418654)Instructions burned: 4593 (million) % 193.69/27.52 % (2418665)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=3326921257:i=5211_2957 on theBenchmark for (2957ds/5211Mi) % 193.69/27.52 % (2418622)Instruction limit reached! % 193.69/27.52 % (2418622)------------------------------ % 193.69/27.52 % (2418622)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 193.69/27.52 % (2418622)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 193.69/27.52 % (2418622)CaDiCaL version: 2.1.3 % 193.69/27.52 % (2418622)Termination reason: Instruction limit % 193.69/27.52 % (2418622)Termination phase: Saturation % 193.69/27.52 % (2418622)Time elapsed: 3.264 s % 193.69/27.52 % (2418622)Peak memory usage: 30 MB % 193.69/27.52 % (2418622)Instructions burned: 3512 (million) % 193.69/27.52 % (2418667)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=325743400:i=5497:nm=2_2955 on theBenchmark for (2955ds/5497Mi) % 193.69/27.52 % (2418667)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 193.69/27.52 % (2418667)Terminated due to inappropriate strategy. % 193.69/27.52 % (2418667)------------------------------ % 193.69/27.52 % (2418667)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 193.69/27.52 % (2418667)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 193.69/27.52 % (2418667)CaDiCaL version: 2.1.3 % 193.69/27.52 % (2418667)Termination reason: Inappropriate % 193.69/27.52 % (2418667)Time elapsed: 0.004 s % 193.69/27.52 % (2418667)Peak memory usage: 11 MB % 193.69/27.52 % (2418667)Instructions burned: 7 (million) % 193.69/27.52 % (2418667)------------------------------ % 193.69/27.52 % (2418667)------------------------------ % 193.69/27.52 % (2418669)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=1385158917:fmbsr=2:i=46332_2955 on theBenchmark for (2955ds/46332Mi) % 193.69/27.52 % (2418669)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 193.69/27.52 % (2418669)Terminated due to inappropriate strategy. % 193.69/27.52 % (2418669)------------------------------ % 193.69/27.52 % (2418669)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 193.69/27.52 % (2418669)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 193.69/27.52 % (2418669)CaDiCaL version: 2.1.3 % 193.69/27.52 % (2418669)Termination reason: Inappropriate % 193.69/27.52 % (2418669)Time elapsed: 0.004 s % 193.69/27.52 % (2418669)Peak memory usage: 11 MB % 193.69/27.52 % (2418669)Instructions burned: 7 (million) % 193.69/27.52 % (2418669)------------------------------ % 193.69/27.52 % (2418669)------------------------------ % 193.69/27.52 % (2418671)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=3226810139:i=14071_2955 on theBenchmark for (2955ds/14071Mi) % 193.69/27.52 % (2418671)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 193.69/27.52 % (2418671)Terminated due to inappropriate strategy. % 193.69/27.52 % (2418671)------------------------------ % 193.69/27.52 % (2418671)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 193.69/27.52 % (2418671)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 193.69/27.52 % (2418671)CaDiCaL version: 2.1.3 % 193.69/27.52 % (2418671)Termination reason: Inappropriate % 193.69/27.52 % (2418671)Time elapsed: 0.004 s % 193.69/27.52 % (2418671)Peak memory usage: 10 MB % 193.69/27.52 % (2418671)Instructions burned: 7 (million) % 193.69/27.52 % (2418671)------------------------------ % 193.69/27.52 % (2418671)------------------------------ % 193.69/27.52 % (2418673)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1212857518:i=22565:add=on:rawr=on_2955 on theBenchmark for (2955ds/22565Mi) % 193.69/27.52 % (2418634)Instruction limit reached! % 193.69/27.52 % (2418634)------------------------------ % 193.69/27.52 % (2418634)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 193.69/27.52 % (2418634)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 193.69/27.52 % (2418634)CaDiCaL version: 2.1.3 % 193.69/27.52 % (2418634)Termination reason: Instruction limit % 193.69/27.52 % (2418634)Termination phase: Saturation % 193.69/27.52 % (2418634)Time elapsed: 3.331 s % 193.69/27.52 % (2418634)Peak memory usage: 33 MB % 193.69/27.52 % (2418634)Instructions burned: 3774 (million) % 193.69/27.52 % (2418677)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=2095128374:i=8173:av=off_2950 on theBenchmark for (2950ds/8173Mi) % 193.69/27.52 % (2418608)Instruction limit reached! % 194.23/27.68 % (2418608)------------------------------ % 194.23/27.68 % (2418608)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 194.23/27.68 % (2418608)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 194.23/27.68 % (2418608)CaDiCaL version: 2.1.3 % 194.23/27.68 % (2418608)Termination reason: Instruction limit % 194.23/27.68 % (2418608)Termination phase: Saturation % 194.23/27.68 % (2418608)Time elapsed: 4.991 s % 194.23/27.68 % (2418608)Peak memory usage: 39 MB % 194.23/27.68 % (2418608)Instructions burned: 5115 (million) % 194.23/27.68 % (2418681)dis+10_16:1_sil=16000:random_seed=578218014:i=9155:fsr=off_2940 on theBenchmark for (2940ds/9155Mi) % 194.23/27.68 % (2418665)Instruction limit reached! % 194.23/27.68 % (2418665)------------------------------ % 194.23/27.68 % (2418665)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 194.23/27.68 % (2418665)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 194.23/27.68 % (2418665)CaDiCaL version: 2.1.3 % 194.23/27.68 % (2418665)Termination reason: Instruction limit % 194.23/27.68 % (2418665)Termination phase: Saturation % 194.23/27.68 % (2418665)Time elapsed: 4.335 s % 194.23/27.68 % (2418665)Peak memory usage: 45 MB % 194.23/27.68 % (2418665)Instructions burned: 5211 (million) % 194.23/27.68 % (2418695)ott-3_8_sil=64000:random_seed=873731850:i=20139:bs=on_2913 on theBenchmark for (2913ds/20139Mi) % 194.23/27.68 % (2418673)Instruction limit reached! % 194.23/27.68 % (2418673)------------------------------ % 194.23/27.68 % (2418673)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 194.23/27.68 % (2418673)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 194.23/27.68 % (2418673)CaDiCaL version: 2.1.3 % 194.23/27.68 % (2418673)Termination reason: Instruction limit % 194.23/27.68 % (2418673)Termination phase: Saturation % 194.23/27.68 % (2418673)Time elapsed: 8.505 s % 194.23/27.68 % (2418673)Peak memory usage: 21 MB % 194.23/27.68 % (2418673)Instructions burned: 22568 (million) % 194.23/27.68 % (2418703)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=1285238517:fmbsr=2:i=32576_2869 on theBenchmark for (2869ds/32576Mi) % 194.23/27.68 % (2418703)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 194.23/27.68 % (2418703)Terminated due to inappropriate strategy. % 194.23/27.68 % (2418703)------------------------------ % 194.23/27.68 % (2418703)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 194.23/27.68 % (2418703)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 194.23/27.68 % (2418703)CaDiCaL version: 2.1.3 % 194.23/27.68 % (2418703)Termination reason: Inappropriate % 194.23/27.68 % (2418703)Time elapsed: 0.004 s % 194.23/27.68 % (2418703)Peak memory usage: 11 MB % 194.23/27.68 % (2418703)Instructions burned: 7 (million) % 194.23/27.68 % (2418703)------------------------------ % 194.23/27.68 % (2418703)------------------------------ % 194.23/27.68 % (2418677)Instruction limit reached! % 194.23/27.68 % (2418677)------------------------------ % 194.23/27.68 % (2418677)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 194.23/27.68 % (2418677)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 194.23/27.68 % (2418677)CaDiCaL version: 2.1.3 % 194.23/27.68 % (2418677)Termination reason: Instruction limit % 194.23/27.68 % (2418677)Termination phase: Saturation % 194.23/27.68 % (2418677)Time elapsed: 8.111 s % 194.23/27.68 % (2418677)Peak memory usage: 79 MB % 194.23/27.68 % (2418677)Instructions burned: 8174 (million) % 194.23/27.68 % (2418705)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=1549783953:i=11404_2869 on theBenchmark for (2869ds/11404Mi) % 194.23/27.68 % (2418707)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=3101313815:i=14134_2869 on theBenchmark for (2869ds/14134Mi) % 194.23/27.68 % (2418681)Instruction limit reached! % 194.23/27.68 % (2418681)------------------------------ % 194.23/27.68 % (2418681)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 194.23/27.68 % (2418681)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 194.23/27.68 % (2418681)CaDiCaL version: 2.1.3 % 194.23/27.68 % (2418681)Termination reason: Instruction limit % 194.23/27.68 % (2418681)Termination phase: Saturation % 194.23/27.68 % (2418681)Time elapsed: 8.254 s % 194.23/27.68 % (2418681)Peak memory usage: 52 MB % 194.23/27.68 % (2418681)Instructions burned: 9155 (million) % 194.23/27.68 % (2418709)dis+33_16_sil=32000:sac=on:random_seed=3585070895:i=15851:nm=0_2857 on theBenchmark for (2857ds/15851Mi) % 194.23/27.68 % (2418705)Instruction limit reached! % 194.23/27.68 % (2418705)------------------------------ % 194.23/27.68 % (2418705)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 206.02/29.28 % (2418705)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 206.02/29.28 % (2418705)CaDiCaL version: 2.1.3 % 206.02/29.28 % (2418705)Termination reason: Instruction limit % 206.02/29.28 % (2418705)Termination phase: Saturation % 206.02/29.28 % (2418705)Time elapsed: 6.016 s % 206.02/29.28 % (2418705)Peak memory usage: 65 MB % 206.02/29.28 % (2418705)Instructions burned: 11406 (million) % 206.02/29.28 % (2418715)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=2719022363:avsq=on:i=17627:add=on:amm=off_2809 on theBenchmark for (2809ds/17627Mi) % 206.02/29.28 % (2418695)Instruction limit reached! % 206.02/29.28 % (2418695)------------------------------ % 206.02/29.28 % (2418695)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 206.02/29.28 % (2418695)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 206.02/29.28 % (2418695)CaDiCaL version: 2.1.3 % 206.02/29.28 % (2418695)Termination reason: Instruction limit % 206.02/29.28 % (2418695)Termination phase: Saturation % 206.02/29.28 % (2418695)Time elapsed: 18.406 s % 206.02/29.28 % (2418695)Peak memory usage: 77 MB % 206.02/29.28 % (2418695)Instructions burned: 20139 (million) % 206.02/29.28 % (2418715)Instruction limit reached! % 206.02/29.28 % (2418715)------------------------------ % 206.02/29.28 % (2418715)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 206.02/29.28 % (2418715)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 206.02/29.28 % (2418715)CaDiCaL version: 2.1.3 % 206.02/29.28 % (2418715)Termination reason: Instruction limit % 206.02/29.28 % (2418715)Termination phase: Saturation % 206.02/29.28 % (2418715)Time elapsed: 7.974 s % 206.02/29.28 % (2418715)Peak memory usage: 206 MB % 206.02/29.28 % (2418715)Instructions burned: 17627 (million) % 206.02/29.28 % (2418723)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=3380256580:s2a=on:i=53295_2729 on theBenchmark for (2729ds/53295Mi) % 206.02/29.28 % (2418726)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=2342805772:i=26857:ins=20_2728 on theBenchmark for (2728ds/26857Mi) % 206.02/29.28 % (2418726)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 206.02/29.28 % (2418726)Terminated due to inappropriate strategy. % 206.02/29.29 % (2418726)------------------------------ % 206.02/29.29 % (2418726)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 206.02/29.29 % (2418726)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 206.02/29.29 % (2418726)CaDiCaL version: 2.1.3 % 206.02/29.29 % (2418726)Termination reason: Inappropriate % 206.02/29.29 % (2418726)Time elapsed: 0.004 s % 206.02/29.29 % (2418726)Peak memory usage: 10 MB % 206.02/29.29 % (2418726)Instructions burned: 6 (million) % 206.02/29.29 % (2418726)------------------------------ % 206.02/29.29 % (2418726)------------------------------ % 206.02/29.29 % (2418729)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=1761424555:i=28120:bs=on:fsr=off_2728 on theBenchmark for (2728ds/28120Mi) % 206.02/29.29 % (2418707)Instruction limit reached! % 206.02/29.29 % (2418707)------------------------------ % 206.02/29.29 % (2418707)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 206.02/29.29 % (2418707)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 206.02/29.29 % (2418707)CaDiCaL version: 2.1.3 % 206.02/29.29 % (2418707)Termination reason: Instruction limit % 206.02/29.29 % (2418707)Termination phase: Saturation % 206.02/29.29 % (2418707)Time elapsed: 14.134 s % 206.02/29.29 % (2418707)Peak memory usage: 80 MB % 206.02/29.29 % (2418707)Instructions burned: 14135 (million) % 206.02/29.29 % (2418731)fmb+10_1_sil=256000:fmbss=7:random_seed=3428970067:fmbsr=1.6:i=182295_2727 on theBenchmark for (2727ds/182295Mi) % 206.02/29.29 % (2418731)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 206.02/29.29 % (2418731)Terminated due to inappropriate strategy. % 206.02/29.29 % (2418731)------------------------------ % 206.02/29.29 % (2418731)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 206.02/29.29 % (2418731)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 206.02/29.29 % (2418731)CaDiCaL version: 2.1.3 % 206.02/29.29 % (2418731)Termination reason: Inappropriate % 206.02/29.29 % (2418731)Time elapsed: 0.003 s % 206.02/29.29 % (2418731)Peak memory usage: 10 MB % 206.02/29.29 % (2418731)Instructions burned: 6 (million) % 206.02/29.29 % (2418731)------------------------------ % 206.02/29.29 % (2418731)------------------------------ % 206.02/29.29 % (2418733)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=2393904054:i=44625:gsp=on_2727 on theBenchmark for (2727ds/44625Mi) % 227.35/32.24 % (2418733)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 227.35/32.24 % (2418733)Terminated due to inappropriate strategy. % 227.35/32.24 % (2418733)------------------------------ % 227.35/32.24 % (2418733)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 227.35/32.24 % (2418733)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 227.35/32.24 % (2418733)CaDiCaL version: 2.1.3 % 227.35/32.24 % (2418733)Termination reason: Inappropriate % 227.35/32.24 % (2418733)Time elapsed: 0.004 s % 227.35/32.24 % (2418733)Peak memory usage: 11 MB % 227.35/32.24 % (2418733)Instructions burned: 9 (million) % 227.35/32.24 % (2418733)------------------------------ % 227.35/32.24 % (2418733)------------------------------ % 227.35/32.24 % (2418735)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=1532140335:i=160505_2726 on theBenchmark for (2726ds/160505Mi) % 227.35/32.24 % (2418735)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 227.35/32.24 % (2418735)Terminated due to inappropriate strategy. % 227.35/32.24 % (2418735)------------------------------ % 227.35/32.24 % (2418735)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 227.35/32.24 % (2418735)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 227.35/32.24 % (2418735)CaDiCaL version: 2.1.3 % 227.35/32.24 % (2418735)Termination reason: Inappropriate % 227.35/32.24 % (2418735)Time elapsed: 0.004 s % 227.35/32.24 % (2418735)Peak memory usage: 11 MB % 227.35/32.24 % (2418735)Instructions burned: 6 (million) % 227.35/32.24 % (2418735)------------------------------ % 227.35/32.24 % (2418735)------------------------------ % 227.35/32.24 % (2418737)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=971131270:fmbsr=1.3:i=225729_2726 on theBenchmark for (2726ds/225729Mi) % 227.35/32.24 % (2418737)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 227.35/32.24 % (2418737)Terminated due to inappropriate strategy. % 227.35/32.24 % (2418737)------------------------------ % 227.35/32.24 % (2418737)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 227.35/32.24 % (2418737)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 227.35/32.24 % (2418737)CaDiCaL version: 2.1.3 % 227.35/32.24 % (2418737)Termination reason: Inappropriate % 227.35/32.24 % (2418737)Time elapsed: 0.004 s % 227.35/32.24 % (2418737)Peak memory usage: 11 MB % 227.35/32.24 % (2418737)Instructions burned: 7 (million) % 227.35/32.24 % (2418737)------------------------------ % 227.35/32.24 % (2418737)------------------------------ % 227.35/32.24 % (2418739)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=1241839861:fmbsr=2:i=185024:ins=7_2726 on theBenchmark for (2726ds/185024Mi) % 227.35/32.24 % (2418739)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 227.35/32.24 % (2418739)Terminated due to inappropriate strategy. % 227.35/32.24 % (2418739)------------------------------ % 227.35/32.24 % (2418739)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 227.35/32.24 % (2418739)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 227.35/32.24 % (2418739)CaDiCaL version: 2.1.3 % 227.35/32.24 % (2418739)Termination reason: Inappropriate % 227.35/32.24 % (2418739)Time elapsed: 0.003 s % 227.35/32.24 % (2418739)Peak memory usage: 10 MB % 227.35/32.24 % (2418739)Instructions burned: 7 (million) % 227.35/32.24 % (2418739)------------------------------ % 227.35/32.24 % (2418739)------------------------------ % 227.35/32.24 % (2418741)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=3101845617:rtra=on_2726 on theBenchmark for (2726ds/0Mi) % 227.35/32.24 % (2418741)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 227.35/32.24 % (2418741)Terminated due to inappropriate strategy. % 227.35/32.24 % (2418741)------------------------------ % 227.35/32.24 % (2418741)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 227.35/32.24 % (2418741)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 227.35/32.24 % (2418741)CaDiCaL version: 2.1.3 % 227.35/32.24 % (2418741)Termination reason: Inappropriate % 227.35/32.24 % (2418741)Time elapsed: 0.008 s % 227.35/32.24 % (2418741)Peak memory usage: 11 MB % 227.35/32.24 % (2418741)Instructions burned: 8 (million) % 227.35/32.24 % (2418741)------------------------------ % 227.35/32.24 % (2418741)------------------------------ % 227.35/32.24 % (2418743)% WARNING: option uhcvi not known. % 227.35/32.24 % (2418743)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3125676208:i=271062:add=off:rtra=on:rawr=on_2725 on theBenchmark for (2725ds/271062Mi) % 267.93/37.99 % (2418659)Instruction limit reached! % 267.93/37.99 % (2418659)------------------------------ % 267.93/37.99 % (2418659)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 267.93/37.99 % (2418659)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 267.93/37.99 % (2418659)CaDiCaL version: 2.1.3 % 267.93/37.99 % (2418659)Termination reason: Instruction limit % 267.93/37.99 % (2418659)Termination phase: Saturation % 267.93/37.99 % (2418659)Time elapsed: 24.064 s % 267.93/37.99 % (2418659)Peak memory usage: 56 MB % 267.93/37.99 % (2418659)Instructions burned: 29341 (million) % 267.93/37.99 % (2418745)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2018687534:i=176048:add=on:rtra=on:rawr=on_2722 on theBenchmark for (2722ds/176048Mi) % 267.93/37.99 % (2418709)Instruction limit reached! % 267.93/37.99 % (2418709)------------------------------ % 267.93/37.99 % (2418709)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 267.93/37.99 % (2418709)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 267.93/37.99 % (2418709)CaDiCaL version: 2.1.3 % 267.93/37.99 % (2418709)Termination reason: Instruction limit % 267.93/37.99 % (2418709)Termination phase: Saturation % 267.93/37.99 % (2418709)Time elapsed: 13.620 s % 267.93/37.99 % (2418709)Peak memory usage: 157 MB % 267.93/37.99 % (2418709)Instructions burned: 15851 (million) % 267.93/37.99 % (2418747)dis+10_1_sil=32000:si=on:sp=arity:random_seed=2796428876:i=206:fgj=on:rtra=on_2721 on theBenchmark for (2721ds/206Mi) % 267.93/37.99 % (2418747)Instruction limit reached! % 267.93/37.99 % (2418747)------------------------------ % 267.93/37.99 % (2418747)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 267.93/37.99 % (2418747)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 267.93/37.99 % (2418747)CaDiCaL version: 2.1.3 % 267.93/37.99 % (2418747)Termination reason: Instruction limit % 267.93/37.99 % (2418747)Termination phase: Saturation % 267.93/37.99 % (2418747)Time elapsed: 0.173 s % 267.93/37.99 % (2418747)Peak memory usage: 14 MB % 267.93/37.99 % (2418747)Instructions burned: 207 (million) % 267.93/37.99 % (2418749)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=317461944:i=232:rtra=on_2719 on theBenchmark for (2719ds/232Mi) % 267.93/37.99 % (2418749)Instruction limit reached! % 267.93/37.99 % (2418749)------------------------------ % 267.93/37.99 % (2418749)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 267.93/37.99 % (2418749)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 267.93/37.99 % (2418749)CaDiCaL version: 2.1.3 % 267.93/37.99 % (2418749)Termination reason: Instruction limit % 267.93/37.99 % (2418749)Termination phase: Saturation % 267.93/37.99 % (2418749)Time elapsed: 0.218 s % 267.93/37.99 % (2418749)Peak memory usage: 14 MB % 267.93/37.99 % (2418749)Instructions burned: 232 (million) % 267.93/37.99 % (2418751)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=1634783829:i=262:rtra=on_2716 on theBenchmark for (2716ds/262Mi) % 267.93/37.99 % (2418751)Instruction limit reached! % 267.93/37.99 % (2418751)------------------------------ % 267.93/37.99 % (2418751)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 267.93/37.99 % (2418751)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 267.93/37.99 % (2418751)CaDiCaL version: 2.1.3 % 267.93/37.99 % (2418751)Termination reason: Instruction limit % 267.93/37.99 % (2418751)Termination phase: Saturation % 267.93/37.99 % (2418751)Time elapsed: 0.268 s % 267.93/37.99 % (2418751)Peak memory usage: 14 MB % 267.93/37.99 % (2418751)Instructions burned: 262 (million) % 267.93/37.99 % (2418753)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=2531546294:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2713 on theBenchmark for (2713ds/318Mi) % 267.93/37.99 % (2418753)Instruction limit reached! % 267.93/37.99 % (2418753)------------------------------ % 267.93/37.99 % (2418753)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 267.93/37.99 % (2418753)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 267.93/37.99 % (2418753)CaDiCaL version: 2.1.3 % 267.93/37.99 % (2418753)Termination reason: Instruction limit % 267.93/37.99 % (2418753)Termination phase: Saturation % 267.93/37.99 % (2418753)Time elapsed: 0.349 s % 267.93/37.99 % (2418753)Peak memory usage: 14 MB % 267.93/37.99 % (2418753)Instructions burned: 319 (million) % 267.93/37.99 % (2418755)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=22495194:i=1428:nm=2:rtra=on_2709 onTerminated % 300.67/42.54 % Vampire exiting % 300.67/42.54 Terminated %------------------------------------------------------------------------------