%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWW580_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 : n004.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:28 PM UTC 2026 % Result : Timeout 299.49s 42.41s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWW580_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.09/0.17 % Computer : n004.cluster.edu % 0.09/0.17 % Model : x86_64 x86_64 % 0.09/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.17 % Memory : 8046.5625MB % 0.09/0.17 % OS : Linux 6.8.0-71-generic % 0.09/0.17 % CPULimit : 300 % 0.09/0.17 % WCLimit : 300 % 0.09/0.17 % DateTime : Mon Sep 28 14:19:52 UTC 2026 % 0.09/0.17 % CPUTime : % 0.09/0.17 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.09/0.19 Running first-order model finding % 0.09/0.19 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.96/0.81 % (378615)Will run a generic schedule for satisfiability detection. % 3.96/0.81 % (378622)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1067837247:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 3.96/0.81 % (378623)dis+10_1_sil=32000:sp=arity:random_seed=2693202738:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 3.96/0.81 % (378620)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=465885648_2999 on theBenchmark for (2999ds/0Mi) % 3.96/0.81 % (378626)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3620795650:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 3.96/0.81 % (378624)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1532220973:i=116_2999 on theBenchmark for (2999ds/116Mi) % 3.96/0.81 % (378625)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1763361088:i=131_2999 on theBenchmark for (2999ds/131Mi) % 3.96/0.81 % (378620)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.96/0.81 % (378620)Terminated due to inappropriate strategy. % 3.96/0.81 % (378620)------------------------------ % 3.96/0.81 % (378620)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.96/0.81 % (378620)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.96/0.81 % (378620)CaDiCaL version: 2.1.3 % 3.96/0.81 % (378620)Termination reason: Inappropriate % 3.96/0.81 % (378620)Time elapsed: 0.001 s % 3.96/0.81 % (378620)Peak memory usage: 10 MB % 3.96/0.81 % (378620)Instructions burned: 2 (million) % 3.96/0.81 % (378620)------------------------------ % 3.96/0.81 % (378620)------------------------------ % 3.96/0.81 % (378621)% WARNING: option uhcvi not known. % 3.96/0.81 % (378621)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1662802053:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 3.96/0.81 % (378633)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1277893813:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 3.96/0.81 % (378633)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.96/0.81 % (378633)Terminated due to inappropriate strategy. % 3.96/0.81 % (378633)------------------------------ % 3.96/0.81 % (378633)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.96/0.81 % (378633)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.96/0.81 % (378633)CaDiCaL version: 2.1.3 % 3.96/0.81 % (378633)Termination reason: Inappropriate % 3.96/0.81 % (378633)Time elapsed: 0.001 s % 3.96/0.81 % (378633)Peak memory usage: 11 MB % 3.96/0.81 % (378633)Instructions burned: 1 (million) % 3.96/0.81 % (378633)------------------------------ % 3.96/0.81 % (378633)------------------------------ % 3.96/0.81 % (378636)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2091074027:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 3.96/0.81 % (378623)Instruction limit reached! % 3.96/0.81 % (378623)------------------------------ % 3.96/0.81 % (378623)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.96/0.81 % (378623)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.96/0.81 % (378623)CaDiCaL version: 2.1.3 % 3.96/0.81 % (378623)Termination reason: Instruction limit % 3.96/0.81 % (378623)Termination phase: Saturation % 3.96/0.81 % (378623)Time elapsed: 0.062 s % 3.96/0.81 % (378623)Peak memory usage: 12 MB % 3.96/0.81 % (378623)Instructions burned: 103 (million) % 3.96/0.81 % (378624)Instruction limit reached! % 3.96/0.81 % (378624)------------------------------ % 3.96/0.81 % (378624)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.96/0.81 % (378624)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.96/0.81 % (378624)CaDiCaL version: 2.1.3 % 3.96/0.81 % (378624)Termination reason: Instruction limit % 3.96/0.81 % (378624)Termination phase: Saturation % 3.96/0.81 % (378624)Time elapsed: 0.072 s % 3.96/0.81 % (378624)Peak memory usage: 12 MB % 3.96/0.81 % (378624)Instructions burned: 116 (million) % 3.96/0.81 % (378625)Instruction limit reached! % 3.96/0.81 % (378625)------------------------------ % 3.96/0.81 % (378625)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.96/0.81 % (378625)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.96/0.81 % (378625)CaDiCaL version: 2.1.3 % 3.96/0.81 % (378625)Termination reason: Instruction limit % 3.96/0.81 % (378625)Termination phase: Saturation % 7.53/1.37 % (378625)Time elapsed: 0.072 s % 7.53/1.37 % (378625)Peak memory usage: 12 MB % 7.53/1.37 % (378625)Instructions burned: 132 (million) % 7.53/1.37 % (378638)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=3914940865:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi) % 7.53/1.37 % (378640)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=919110576:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 7.53/1.37 % (378639)ott-21_1_sil=16000:fs=off:random_seed=1722321859:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 7.53/1.37 % (378626)Instruction limit reached! % 7.53/1.37 % (378626)------------------------------ % 7.53/1.37 % (378626)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.53/1.37 % (378626)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.53/1.37 % (378626)CaDiCaL version: 2.1.3 % 7.53/1.37 % (378626)Termination reason: Instruction limit % 7.53/1.37 % (378626)Termination phase: Saturation % 7.53/1.37 % (378626)Time elapsed: 0.105 s % 7.53/1.37 % (378626)Peak memory usage: 13 MB % 7.53/1.37 % (378626)Instructions burned: 160 (million) % 7.53/1.37 % (378644)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3787430171:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 7.53/1.37 % (378644)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 7.53/1.37 % (378644)Terminated due to inappropriate strategy. % 7.53/1.37 % (378644)------------------------------ % 7.53/1.37 % (378644)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.53/1.37 % (378644)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.53/1.37 % (378644)CaDiCaL version: 2.1.3 % 7.53/1.37 % (378644)Termination reason: Inappropriate % 7.53/1.37 % (378644)Time elapsed: 0.001 s % 7.53/1.37 % (378644)Peak memory usage: 10 MB % 7.53/1.37 % (378644)Instructions burned: 1 (million) % 7.53/1.37 % (378644)------------------------------ % 7.53/1.37 % (378644)------------------------------ % 7.53/1.37 % (378636)Instruction limit reached! % 7.53/1.37 % (378636)------------------------------ % 7.53/1.37 % (378636)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.53/1.37 % (378636)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.53/1.37 % (378636)CaDiCaL version: 2.1.3 % 7.53/1.37 % (378636)Termination reason: Instruction limit % 7.53/1.37 % (378636)Termination phase: Saturation % 7.53/1.37 % (378636)Time elapsed: 0.092 s % 7.53/1.37 % (378636)Peak memory usage: 13 MB % 7.53/1.37 % (378636)Instructions burned: 131 (million) % 7.53/1.37 % (378646)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=959755507:i=1179_2998 on theBenchmark for (2998ds/1179Mi) % 7.53/1.37 % (378647)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3701112153:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi) % 7.53/1.37 % (378647)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 7.53/1.37 % (378647)Terminated due to inappropriate strategy. % 7.53/1.37 % (378647)------------------------------ % 7.53/1.37 % (378647)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.53/1.37 % (378647)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.53/1.37 % (378647)CaDiCaL version: 2.1.3 % 7.53/1.37 % (378647)Termination reason: Inappropriate % 7.53/1.37 % (378647)Time elapsed: 0.001 s % 7.53/1.37 % (378647)Peak memory usage: 10 MB % 7.53/1.37 % (378647)Instructions burned: 1 (million) % 7.53/1.37 % (378647)------------------------------ % 7.53/1.37 % (378647)------------------------------ % 7.53/1.37 % (378650)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=813107137:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2998 on theBenchmark for (2998ds/692Mi) % 7.53/1.37 % (378639)Instruction limit reached! % 7.53/1.37 % (378639)------------------------------ % 7.53/1.37 % (378639)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.53/1.37 % (378639)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.53/1.37 % (378639)CaDiCaL version: 2.1.3 % 7.53/1.37 % (378639)Termination reason: Instruction limit % 7.53/1.37 % (378639)Termination phase: Saturation % 7.53/1.37 % (378639)Time elapsed: 0.086 s % 7.53/1.37 % (378639)Peak memory usage: 12 MB % 7.53/1.37 % (378639)Instructions burned: 180 (million) % 22.27/3.45 % (378652)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3443958340:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi) % 22.27/3.45 % (378640)Instruction limit reached! % 22.27/3.45 % (378640)------------------------------ % 22.27/3.45 % (378640)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.27/3.45 % (378640)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.27/3.45 % (378640)CaDiCaL version: 2.1.3 % 22.27/3.45 % (378640)Termination reason: Instruction limit % 22.27/3.45 % (378640)Termination phase: Saturation % 22.27/3.45 % (378640)Time elapsed: 0.318 s % 22.27/3.45 % (378640)Peak memory usage: 13 MB % 22.27/3.45 % (378640)Instructions burned: 478 (million) % 22.27/3.45 % (378638)Instruction limit reached! % 22.27/3.45 % (378638)------------------------------ % 22.27/3.45 % (378638)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.27/3.45 % (378638)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.27/3.45 % (378638)CaDiCaL version: 2.1.3 % 22.27/3.45 % (378638)Termination reason: Instruction limit % 22.27/3.45 % (378638)Termination phase: Saturation % 22.27/3.45 % (378638)Time elapsed: 0.332 s % 22.27/3.45 % (378638)Peak memory usage: 17 MB % 22.27/3.45 % (378638)Instructions burned: 686 (million) % 22.27/3.45 % (378654)fmb+10_1_sil=64000:random_seed=3754606548:i=22061:nm=2:gsp=on_2995 on theBenchmark for (2995ds/22061Mi) % 22.27/3.45 % (378654)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 22.27/3.45 % (378654)Terminated due to inappropriate strategy. % 22.27/3.45 % (378654)------------------------------ % 22.27/3.45 % (378654)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.27/3.45 % (378654)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.27/3.45 % (378654)CaDiCaL version: 2.1.3 % 22.27/3.45 % (378654)Termination reason: Inappropriate % 22.27/3.45 % (378654)Time elapsed: 0.001 s % 22.27/3.45 % (378654)Peak memory usage: 10 MB % 22.27/3.45 % (378654)Instructions burned: 2 (million) % 22.27/3.45 % (378654)------------------------------ % 22.27/3.45 % (378654)------------------------------ % 22.27/3.45 % (378655)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2321100701:i=9515:nm=5_2995 on theBenchmark for (2995ds/9515Mi) % 22.27/3.45 % (378655)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 22.27/3.45 % (378655)Terminated due to inappropriate strategy. % 22.27/3.45 % (378655)------------------------------ % 22.27/3.45 % (378655)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.27/3.45 % (378655)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.27/3.45 % (378655)CaDiCaL version: 2.1.3 % 22.27/3.45 % (378655)Termination reason: Inappropriate % 22.27/3.45 % (378655)Time elapsed: 0.001 s % 22.27/3.45 % (378655)Peak memory usage: 10 MB % 22.27/3.45 % (378655)Instructions burned: 1 (million) % 22.27/3.45 % (378655)------------------------------ % 22.27/3.45 % (378655)------------------------------ % 22.27/3.45 % (378658)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2669766675:fmbsr=1.7:i=920_2995 on theBenchmark for (2995ds/920Mi) % 22.27/3.45 % (378658)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 22.27/3.45 % (378658)Terminated due to inappropriate strategy. % 22.27/3.45 % (378658)------------------------------ % 22.27/3.45 % (378658)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.27/3.45 % (378658)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.27/3.45 % (378658)CaDiCaL version: 2.1.3 % 22.27/3.45 % (378658)Termination reason: Inappropriate % 22.27/3.45 % (378658)Time elapsed: 0.001 s % 22.27/3.45 % (378658)Peak memory usage: 10 MB % 22.27/3.45 % (378658)Instructions burned: 1 (million) % 22.27/3.45 % (378658)------------------------------ % 22.27/3.45 % (378658)------------------------------ % 22.27/3.45 % (378659)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2425866268:i=5131_2995 on theBenchmark for (2995ds/5131Mi) % 22.27/3.45 % (378662)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2387567292:i=1472:ins=7:fdi=8:gsp=on_2995 on theBenchmark for (2995ds/1472Mi) % 22.27/3.45 % (378650)Instruction limit reached! % 22.27/3.45 % (378650)------------------------------ % 22.27/3.45 % (378650)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.27/3.45 % (378650)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 37.52/5.56 % (378650)CaDiCaL version: 2.1.3 % 37.52/5.56 % (378650)Termination reason: Instruction limit % 37.52/5.56 % (378650)Termination phase: Saturation % 37.52/5.56 % (378650)Time elapsed: 0.389 s % 37.52/5.56 % (378650)Peak memory usage: 20 MB % 37.52/5.56 % (378650)Instructions burned: 693 (million) % 37.52/5.56 % (378664)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=38766218:i=6324_2993 on theBenchmark for (2993ds/6324Mi) % 37.52/5.56 % (378664)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 37.52/5.56 % (378664)Terminated due to inappropriate strategy. % 37.52/5.56 % (378664)------------------------------ % 37.52/5.56 % (378664)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 37.52/5.56 % (378664)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 37.52/5.56 % (378664)CaDiCaL version: 2.1.3 % 37.52/5.56 % (378664)Termination reason: Inappropriate % 37.52/5.56 % (378664)Time elapsed: 0.001 s % 37.52/5.56 % (378664)Peak memory usage: 10 MB % 37.52/5.56 % (378664)Instructions burned: 2 (million) % 37.52/5.56 % (378664)------------------------------ % 37.52/5.56 % (378664)------------------------------ % 37.52/5.56 % (378666)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=81929144:fmbsr=2.30978:i=2174_2993 on theBenchmark for (2993ds/2174Mi) % 37.52/5.56 % (378666)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 37.52/5.56 % (378666)Terminated due to inappropriate strategy. % 37.52/5.56 % (378666)------------------------------ % 37.52/5.56 % (378666)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 37.52/5.56 % (378666)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 37.52/5.56 % (378666)CaDiCaL version: 2.1.3 % 37.52/5.56 % (378666)Termination reason: Inappropriate % 37.52/5.56 % (378666)Time elapsed: 0.001 s % 37.52/5.56 % (378666)Peak memory usage: 10 MB % 37.52/5.56 % (378666)Instructions burned: 1 (million) % 37.52/5.56 % (378666)------------------------------ % 37.52/5.56 % (378666)------------------------------ % 37.52/5.56 % (378668)ott-2_1_sil=16000:newcnf=on:random_seed=1091987931:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2993 on theBenchmark for (2993ds/869Mi) % 37.52/5.56 % (378652)Instruction limit reached! % 37.52/5.56 % (378652)------------------------------ % 37.52/5.56 % (378652)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 37.52/5.56 % (378652)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 37.52/5.56 % (378652)CaDiCaL version: 2.1.3 % 37.52/5.56 % (378652)Termination reason: Instruction limit % 37.52/5.56 % (378652)Termination phase: Saturation % 37.52/5.56 % (378652)Time elapsed: 0.484 s % 37.52/5.56 % (378652)Peak memory usage: 18 MB % 37.52/5.56 % (378652)Instructions burned: 881 (million) % 37.52/5.56 % (378670)ott+10_1_sil=32000:tgt=ground:random_seed=1331838622:i=5114:av=off_2992 on theBenchmark for (2992ds/5114Mi) % 37.52/5.56 % (378646)Instruction limit reached! % 37.52/5.56 % (378646)------------------------------ % 37.52/5.56 % (378646)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 37.52/5.56 % (378646)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 37.52/5.56 % (378646)CaDiCaL version: 2.1.3 % 37.52/5.56 % (378646)Termination reason: Instruction limit % 37.52/5.56 % (378646)Termination phase: Saturation % 37.52/5.56 % (378646)Time elapsed: 0.693 s % 37.52/5.56 % (378646)Peak memory usage: 20 MB % 37.52/5.56 % (378646)Instructions burned: 1180 (million) % 37.52/5.56 % (378672)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=1865292897:i=54282_2991 on theBenchmark for (2991ds/54282Mi) % 37.52/5.56 % (378672)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 37.52/5.56 % (378672)Terminated due to inappropriate strategy. % 37.52/5.56 % (378672)------------------------------ % 37.52/5.56 % (378672)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 37.52/5.56 % (378672)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 37.52/5.56 % (378672)CaDiCaL version: 2.1.3 % 37.52/5.56 % (378672)Termination reason: Inappropriate % 37.52/5.56 % (378672)Time elapsed: 0.001 s % 37.52/5.56 % (378672)Peak memory usage: 10 MB % 37.52/5.56 % (378672)Instructions burned: 2 (million) % 37.52/5.56 % (378672)------------------------------ % 37.52/5.56 % (378672)------------------------------ % 37.52/5.56 % (378674)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=206626489:i=3512:aac=none_2991 on theBenchmark for (2991ds/3512Mi) % 37.52/5.56 % (378668)Instruction limit reached! % 122.75/17.56 % (378668)------------------------------ % 122.75/17.56 % (378668)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 122.75/17.56 % (378668)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 122.75/17.56 % (378668)CaDiCaL version: 2.1.3 % 122.75/17.56 % (378668)Termination reason: Instruction limit % 122.75/17.56 % (378668)Termination phase: Saturation % 122.75/17.56 % (378668)Time elapsed: 0.502 s % 122.75/17.56 % (378668)Peak memory usage: 14 MB % 122.75/17.56 % (378668)Instructions burned: 869 (million) % 122.75/17.56 % (378676)dis+21_1_sil=32000:sas=cadical:random_seed=2705507771:i=3773:amm=off_2988 on theBenchmark for (2988ds/3773Mi) % 122.75/17.56 % (378662)Instruction limit reached! % 122.75/17.56 % (378662)------------------------------ % 122.75/17.56 % (378662)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 122.75/17.56 % (378662)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 122.75/17.56 % (378662)CaDiCaL version: 2.1.3 % 122.75/17.56 % (378662)Termination reason: Instruction limit % 122.75/17.56 % (378662)Termination phase: Saturation % 122.75/17.56 % (378662)Time elapsed: 0.912 s % 122.75/17.56 % (378662)Peak memory usage: 26 MB % 122.75/17.56 % (378662)Instructions burned: 1473 (million) % 122.75/17.56 % (378678)ott+11_1_sil=16000:gs=on:random_seed=4288131234:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2985 on theBenchmark for (2985ds/2251Mi) % 122.75/17.56 % (378678)Instruction limit reached! % 122.75/17.56 % (378678)------------------------------ % 122.75/17.56 % (378678)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 122.75/17.56 % (378678)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 122.75/17.56 % (378678)CaDiCaL version: 2.1.3 % 122.75/17.56 % (378678)Termination reason: Instruction limit % 122.75/17.56 % (378678)Termination phase: Saturation % 122.75/17.56 % (378678)Time elapsed: 1.262 s % 122.75/17.56 % (378678)Peak memory usage: 24 MB % 122.75/17.56 % (378678)Instructions burned: 2251 (million) % 122.75/17.56 % (378680)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=2882713520:fmbsr=1.6:i=67534_2972 on theBenchmark for (2972ds/67534Mi) % 122.75/17.56 % (378680)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 122.75/17.56 % (378680)Terminated due to inappropriate strategy. % 122.75/17.56 % (378680)------------------------------ % 122.75/17.56 % (378680)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 122.75/17.56 % (378680)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 122.75/17.56 % (378680)CaDiCaL version: 2.1.3 % 122.75/17.56 % (378680)Termination reason: Inappropriate % 122.75/17.56 % (378680)Time elapsed: 0.001 s % 122.75/17.56 % (378680)Peak memory usage: 10 MB % 122.75/17.56 % (378680)Instructions burned: 2 (million) % 122.75/17.56 % (378680)------------------------------ % 122.75/17.56 % (378680)------------------------------ % 122.75/17.56 % (378682)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=331561366:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2972 on theBenchmark for (2972ds/4591Mi) % 122.75/17.56 % (378674)Instruction limit reached! % 122.75/17.56 % (378674)------------------------------ % 122.75/17.56 % (378674)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 122.75/17.56 % (378674)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 122.75/17.56 % (378674)CaDiCaL version: 2.1.3 % 122.75/17.56 % (378674)Termination reason: Instruction limit % 122.75/17.56 % (378674)Termination phase: Saturation % 122.75/17.56 % (378674)Time elapsed: 1.933 s % 122.75/17.56 % (378674)Peak memory usage: 32 MB % 122.75/17.56 % (378674)Instructions burned: 3512 (million) % 122.75/17.56 % (378684)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=792406224:i=29340_2971 on theBenchmark for (2971ds/29340Mi) % 122.75/17.56 % (378659)Instruction limit reached! % 122.75/17.56 % (378659)------------------------------ % 122.75/17.56 % (378659)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 122.75/17.56 % (378659)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 122.75/17.56 % (378659)CaDiCaL version: 2.1.3 % 122.75/17.56 % (378659)Termination reason: Instruction limit % 122.75/17.56 % (378659)Termination phase: Saturation % 122.75/17.56 % (378659)Time elapsed: 2.725 s % 122.75/17.56 % (378659)Peak memory usage: 34 MB % 122.75/17.56 % (378659)Instructions burned: 5132 (million) % 122.75/17.56 % (378686)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=2357067914:i=5211_2967 on theBenchmark for (2967ds/5211Mi) % 122.75/17.56 % (378676)Instruction limit reached! % 143.34/20.44 % (378676)------------------------------ % 143.34/20.44 % (378676)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 143.34/20.44 % (378676)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 143.34/20.44 % (378676)CaDiCaL version: 2.1.3 % 143.34/20.44 % (378676)Termination reason: Instruction limit % 143.34/20.44 % (378676)Termination phase: Saturation % 143.34/20.44 % (378676)Time elapsed: 2.057 s % 143.34/20.44 % (378676)Peak memory usage: 32 MB % 143.34/20.44 % (378676)Instructions burned: 3773 (million) % 143.34/20.44 % (378688)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=3682418901:i=5497:nm=2_2967 on theBenchmark for (2967ds/5497Mi) % 143.34/20.44 % (378688)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 143.34/20.44 % (378688)Terminated due to inappropriate strategy. % 143.34/20.44 % (378688)------------------------------ % 143.34/20.44 % (378688)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 143.34/20.44 % (378688)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 143.34/20.44 % (378688)CaDiCaL version: 2.1.3 % 143.34/20.44 % (378688)Termination reason: Inappropriate % 143.34/20.44 % (378688)Time elapsed: 0.001 s % 143.34/20.44 % (378688)Peak memory usage: 10 MB % 143.34/20.44 % (378688)Instructions burned: 2 (million) % 143.34/20.44 % (378688)------------------------------ % 143.34/20.44 % (378688)------------------------------ % 143.34/20.44 % (378690)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=1770390961:fmbsr=2:i=46332_2967 on theBenchmark for (2967ds/46332Mi) % 143.34/20.44 % (378690)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 143.34/20.44 % (378690)Terminated due to inappropriate strategy. % 143.34/20.44 % (378690)------------------------------ % 143.34/20.44 % (378690)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 143.34/20.44 % (378690)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 143.34/20.44 % (378690)CaDiCaL version: 2.1.3 % 143.34/20.44 % (378690)Termination reason: Inappropriate % 143.34/20.44 % (378690)Time elapsed: 0.001 s % 143.34/20.44 % (378690)Peak memory usage: 10 MB % 143.34/20.44 % (378690)Instructions burned: 2 (million) % 143.34/20.44 % (378690)------------------------------ % 143.34/20.44 % (378690)------------------------------ % 143.34/20.44 % (378692)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=2799110094:i=14071_2967 on theBenchmark for (2967ds/14071Mi) % 143.34/20.44 % (378692)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 143.34/20.44 % (378692)Terminated due to inappropriate strategy. % 143.34/20.44 % (378692)------------------------------ % 143.34/20.44 % (378692)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 143.34/20.44 % (378692)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 143.34/20.44 % (378692)CaDiCaL version: 2.1.3 % 143.34/20.44 % (378692)Termination reason: Inappropriate % 143.34/20.44 % (378692)Time elapsed: 0.001 s % 143.34/20.44 % (378692)Peak memory usage: 10 MB % 143.34/20.44 % (378692)Instructions burned: 2 (million) % 143.34/20.44 % (378692)------------------------------ % 143.34/20.44 % (378692)------------------------------ % 143.34/20.44 % (378694)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=849816910:i=22565:add=on:rawr=on_2966 on theBenchmark for (2966ds/22565Mi) % 143.34/20.44 % (378670)Instruction limit reached! % 143.34/20.44 % (378670)------------------------------ % 143.34/20.44 % (378670)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 143.34/20.44 % (378670)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 143.34/20.44 % (378670)CaDiCaL version: 2.1.3 % 143.34/20.44 % (378670)Termination reason: Instruction limit % 143.34/20.44 % (378670)Termination phase: Saturation % 143.34/20.44 % (378670)Time elapsed: 3.201 s % 143.34/20.44 % (378670)Peak memory usage: 44 MB % 143.34/20.44 % (378670)Instructions burned: 5114 (million) % 143.34/20.44 % (378696)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=2874331823:i=8173:av=off_2960 on theBenchmark for (2960ds/8173Mi) % 143.34/20.44 % (378682)Instruction limit reached! % 143.34/20.44 % (378682)------------------------------ % 143.34/20.44 % (378682)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 143.34/20.44 % (378682)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 143.34/20.44 % (378682)CaDiCaL version: 2.1.3 % 143.34/20.44 % (378682)Termination reason: Instruction limit % 143.34/20.44 % (378682)Termination phase: Saturation % 143.34/20.44 % (378682)Time elapsed: 2.611 s % 151.85/21.67 % (378682)Peak memory usage: 51 MB % 151.85/21.67 % (378682)Instructions burned: 4591 (million) % 151.85/21.67 % (378698)dis+10_16:1_sil=16000:random_seed=487127769:i=9155:fsr=off_2946 on theBenchmark for (2946ds/9155Mi) % 151.85/21.67 % (378686)Instruction limit reached! % 151.85/21.67 % (378686)------------------------------ % 151.85/21.67 % (378686)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 151.85/21.67 % (378686)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 151.85/21.67 % (378686)CaDiCaL version: 2.1.3 % 151.85/21.67 % (378686)Termination reason: Instruction limit % 151.85/21.67 % (378686)Termination phase: Saturation % 151.85/21.67 % (378686)Time elapsed: 2.519 s % 151.85/21.67 % (378686)Peak memory usage: 37 MB % 151.85/21.67 % (378686)Instructions burned: 5213 (million) % 151.85/21.67 % (378700)ott-3_8_sil=64000:random_seed=3064789323:i=20139:bs=on_2942 on theBenchmark for (2942ds/20139Mi) % 151.85/21.67 % (378696)Instruction limit reached! % 151.85/21.67 % (378696)------------------------------ % 151.85/21.67 % (378696)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 151.85/21.67 % (378696)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 151.85/21.67 % (378696)CaDiCaL version: 2.1.3 % 151.85/21.67 % (378696)Termination reason: Instruction limit % 151.85/21.67 % (378696)Termination phase: Saturation % 151.85/21.67 % (378696)Time elapsed: 5.247 s % 151.85/21.67 % (378696)Peak memory usage: 59 MB % 151.85/21.67 % (378696)Instructions burned: 8173 (million) % 151.85/21.67 % (378702)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=2579025647:fmbsr=2:i=32576_2907 on theBenchmark for (2907ds/32576Mi) % 151.85/21.67 % (378702)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 151.85/21.67 % (378702)Terminated due to inappropriate strategy. % 151.85/21.67 % (378702)------------------------------ % 151.85/21.67 % (378702)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 151.85/21.67 % (378702)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 151.85/21.67 % (378702)CaDiCaL version: 2.1.3 % 151.85/21.67 % (378702)Termination reason: Inappropriate % 151.85/21.67 % (378702)Time elapsed: 0.001 s % 151.85/21.67 % (378702)Peak memory usage: 10 MB % 151.85/21.67 % (378702)Instructions burned: 2 (million) % 151.85/21.67 % (378702)------------------------------ % 151.85/21.67 % (378702)------------------------------ % 151.85/21.67 % (378704)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=1006978218:i=11404_2907 on theBenchmark for (2907ds/11404Mi) % 151.85/21.67 % (378698)Instruction limit reached! % 151.85/21.67 % (378698)------------------------------ % 151.85/21.67 % (378698)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 151.85/21.67 % (378698)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 151.85/21.67 % (378698)CaDiCaL version: 2.1.3 % 151.85/21.67 % (378698)Termination reason: Instruction limit % 151.85/21.67 % (378698)Termination phase: Saturation % 151.85/21.67 % (378698)Time elapsed: 4.711 s % 151.85/21.67 % (378698)Peak memory usage: 49 MB % 151.85/21.67 % (378698)Instructions burned: 9157 (million) % 151.85/21.67 % (378706)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=1536396381:i=14134_2899 on theBenchmark for (2899ds/14134Mi) % 151.85/21.67 % (378694)Instruction limit reached! % 151.85/21.67 % (378694)------------------------------ % 151.85/21.67 % (378694)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 151.85/21.67 % (378694)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 151.85/21.67 % (378694)CaDiCaL version: 2.1.3 % 151.85/21.67 % (378694)Termination reason: Instruction limit % 151.85/21.67 % (378694)Termination phase: Saturation % 151.85/21.67 % (378694)Time elapsed: 9.310 s % 151.85/21.67 % (378694)Peak memory usage: 29 MB % 151.85/21.67 % (378694)Instructions burned: 22565 (million) % 151.85/21.67 % (378708)dis+33_16_sil=32000:sac=on:random_seed=1107298342:i=15851:nm=0_2873 on theBenchmark for (2873ds/15851Mi) % 151.85/21.67 % (378704)Instruction limit reached! % 151.85/21.67 % (378704)------------------------------ % 151.85/21.67 % (378704)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 151.85/21.67 % (378704)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 151.85/21.67 % (378704)CaDiCaL version: 2.1.3 % 151.85/21.67 % (378704)Termination reason: Instruction limit % 151.85/21.67 % (378704)Termination phase: Saturation % 151.85/21.67 % (378704)Time elapsed: 8.046 s % 151.85/21.67 % (378704)Peak memory usage: 59 MB % 151.85/21.67 % (378704)Instructions burned: 11405 (million) % 151.85/21.67 % (379069)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=2607355137:avsq=on:i=17627:add=on:amm=off_2826 on theBenchmark for (2826ds/17627Mi) % 167.96/23.93 % (378684)Instruction limit reached! % 167.96/23.93 % (378684)------------------------------ % 167.96/23.93 % (378684)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 167.96/23.93 % (378684)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 167.96/23.93 % (378684)CaDiCaL version: 2.1.3 % 167.96/23.93 % (378684)Termination reason: Instruction limit % 167.96/23.93 % (378684)Termination phase: Saturation % 167.96/23.93 % (378684)Time elapsed: 16.037 s % 167.96/23.93 % (378684)Peak memory usage: 154 MB % 167.96/23.93 % (378684)Instructions burned: 29342 (million) % 167.96/23.93 % (379120)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=1945608577:s2a=on:i=53295_2810 on theBenchmark for (2810ds/53295Mi) % 167.96/23.93 % (378700)Instruction limit reached! % 167.96/23.93 % (378700)------------------------------ % 167.96/23.93 % (378700)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 167.96/23.93 % (378700)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 167.96/23.93 % (378700)CaDiCaL version: 2.1.3 % 167.96/23.93 % (378700)Termination reason: Instruction limit % 167.96/23.93 % (378700)Termination phase: Saturation % 167.96/23.93 % (378700)Time elapsed: 13.385 s % 167.96/23.93 % (378700)Peak memory usage: 93 MB % 167.96/23.93 % (378700)Instructions burned: 20139 (million) % 167.96/23.93 % (379122)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=3922583974:i=26857:ins=20_2808 on theBenchmark for (2808ds/26857Mi) % 167.96/23.93 % (379122)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 167.96/23.93 % (379122)Terminated due to inappropriate strategy. % 167.96/23.93 % (379122)------------------------------ % 167.96/23.93 % (379122)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 167.96/23.93 % (379122)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 167.96/23.93 % (379122)CaDiCaL version: 2.1.3 % 167.96/23.93 % (379122)Termination reason: Inappropriate % 167.96/23.93 % (379122)Time elapsed: 0.001 s % 167.96/23.93 % (379122)Peak memory usage: 10 MB % 167.96/23.93 % (379122)Instructions burned: 1 (million) % 167.96/23.93 % (379122)------------------------------ % 167.96/23.93 % (379122)------------------------------ % 167.96/23.93 % (379124)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=3259814505:i=28120:bs=on:fsr=off_2808 on theBenchmark for (2808ds/28120Mi) % 167.96/23.93 % (378706)Instruction limit reached! % 167.96/23.93 % (378706)------------------------------ % 167.96/23.93 % (378706)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 167.96/23.93 % (378706)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 167.96/23.93 % (378706)CaDiCaL version: 2.1.3 % 167.96/23.93 % (378706)Termination reason: Instruction limit % 167.96/23.93 % (378706)Termination phase: Saturation % 167.96/23.93 % (378706)Time elapsed: 10.067 s % 167.96/23.93 % (378706)Peak memory usage: 66 MB % 167.96/23.93 % (378706)Instructions burned: 14134 (million) % 167.96/23.93 % (379126)fmb+10_1_sil=256000:fmbss=7:random_seed=757772280:fmbsr=1.6:i=182295_2798 on theBenchmark for (2798ds/182295Mi) % 167.96/23.93 % (379126)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 167.96/23.93 % (379126)Terminated due to inappropriate strategy. % 167.96/23.93 % (379126)------------------------------ % 167.96/23.93 % (379126)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 167.96/23.93 % (379126)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 167.96/23.93 % (379126)CaDiCaL version: 2.1.3 % 167.96/23.93 % (379126)Termination reason: Inappropriate % 167.96/23.93 % (379126)Time elapsed: 0.001 s % 167.96/23.93 % (379126)Peak memory usage: 10 MB % 167.96/23.93 % (379126)Instructions burned: 1 (million) % 167.96/23.93 % (379126)------------------------------ % 167.96/23.93 % (379126)------------------------------ % 167.96/23.93 % (379128)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=3875648548:i=44625:gsp=on_2797 on theBenchmark for (2797ds/44625Mi) % 167.96/23.93 % (379128)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 167.96/23.93 % (379128)Terminated due to inappropriate strategy. % 167.96/23.93 % (379128)------------------------------ % 167.96/23.93 % (379128)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 167.96/23.93 % (379128)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 167.96/23.93 % (379128)CaDiCaL version: 2.1.3 % 167.96/23.93 % (379128)Termination reason: Inappropriate % 191.59/27.21 % (379128)Time elapsed: 0.001 s % 191.59/27.21 % (379128)Peak memory usage: 10 MB % 191.59/27.21 % (379128)Instructions burned: 2 (million) % 191.59/27.21 % (379128)------------------------------ % 191.59/27.21 % (379128)------------------------------ % 191.59/27.21 % (379130)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=3329255929:i=160505_2797 on theBenchmark for (2797ds/160505Mi) % 191.59/27.21 % (379130)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 191.59/27.21 % (379130)Terminated due to inappropriate strategy. % 191.59/27.21 % (379130)------------------------------ % 191.59/27.21 % (379130)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 191.59/27.21 % (379130)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 191.59/27.21 % (379130)CaDiCaL version: 2.1.3 % 191.59/27.21 % (379130)Termination reason: Inappropriate % 191.59/27.21 % (379130)Time elapsed: 0.001 s % 191.59/27.21 % (379130)Peak memory usage: 10 MB % 191.59/27.21 % (379130)Instructions burned: 1 (million) % 191.59/27.21 % (379130)------------------------------ % 191.59/27.21 % (379130)------------------------------ % 191.59/27.21 % (379132)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=3196607089:fmbsr=1.3:i=225729_2797 on theBenchmark for (2797ds/225729Mi) % 191.59/27.21 % (379132)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 191.59/27.21 % (379132)Terminated due to inappropriate strategy. % 191.59/27.21 % (379132)------------------------------ % 191.59/27.21 % (379132)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 191.59/27.21 % (379132)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 191.59/27.21 % (379132)CaDiCaL version: 2.1.3 % 191.59/27.21 % (379132)Termination reason: Inappropriate % 191.59/27.21 % (379132)Time elapsed: 0.001 s % 191.59/27.21 % (379132)Peak memory usage: 10 MB % 191.59/27.21 % (379132)Instructions burned: 2 (million) % 191.59/27.21 % (379132)------------------------------ % 191.59/27.21 % (379132)------------------------------ % 191.59/27.21 % (379134)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=2087601945:fmbsr=2:i=185024:ins=7_2797 on theBenchmark for (2797ds/185024Mi) % 191.59/27.21 % (379134)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 191.59/27.21 % (379134)Terminated due to inappropriate strategy. % 191.59/27.21 % (379134)------------------------------ % 191.59/27.21 % (379134)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 191.59/27.21 % (379134)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 191.59/27.21 % (379134)CaDiCaL version: 2.1.3 % 191.59/27.21 % (379134)Termination reason: Inappropriate % 191.59/27.21 % (379134)Time elapsed: 0.001 s % 191.59/27.21 % (379134)Peak memory usage: 10 MB % 191.59/27.21 % (379134)Instructions burned: 2 (million) % 191.59/27.21 % (379134)------------------------------ % 191.59/27.21 % (379134)------------------------------ % 191.59/27.21 % (379136)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=1177609788:rtra=on_2796 on theBenchmark for (2796ds/0Mi) % 191.59/27.21 % (379136)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 191.59/27.21 % (379136)Terminated due to inappropriate strategy. % 191.59/27.21 % (379136)------------------------------ % 191.59/27.21 % (379136)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 191.59/27.21 % (379136)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 191.59/27.21 % (379136)CaDiCaL version: 2.1.3 % 191.59/27.21 % (379136)Termination reason: Inappropriate % 191.59/27.21 % (379136)Time elapsed: 0.001 s % 191.59/27.21 % (379136)Peak memory usage: 10 MB % 191.59/27.21 % (379136)Instructions burned: 2 (million) % 191.59/27.21 % (379136)------------------------------ % 191.59/27.21 % (379136)------------------------------ % 191.59/27.21 % (379138)% WARNING: option uhcvi not known. % 191.59/27.21 % (379138)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1686651313:i=271062:add=off:rtra=on:rawr=on_2796 on theBenchmark for (2796ds/271062Mi) % 191.59/27.21 % (378622)Instruction limit reached! % 191.59/27.21 % (378622)------------------------------ % 191.59/27.21 % (378622)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 191.59/27.21 % (378622)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 191.59/27.21 % (378622)CaDiCaL version: 2.1.3 % 191.59/27.21 % (378622)Termination reason: Instruction limit % 191.59/27.21 % (378622)Termination phase: Saturation % 191.59/27.21 % (378622)Time elapsed: 21.392 s % 191.59/27.21 % (378622)Peak memory usage: 464 MB % 191.59/27.21 % (378622)Instructions burned: 88027 (million) % 191.59/27.21 % (379140)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=4177358758:i=176048:add=on:rtra=on:rawr=on_2785 on theBenchmark for (2785ds/176048Mi) % 198.70/28.21 % (378708)Instruction limit reached! % 198.70/28.21 % (378708)------------------------------ % 198.70/28.21 % (378708)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 198.70/28.21 % (378708)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 198.70/28.21 % (378708)CaDiCaL version: 2.1.3 % 198.70/28.21 % (378708)Termination reason: Instruction limit % 198.70/28.21 % (378708)Termination phase: Saturation % 198.70/28.21 % (378708)Time elapsed: 10.286 s % 198.70/28.21 % (378708)Peak memory usage: 140 MB % 198.70/28.21 % (378708)Instructions burned: 15852 (million) % 198.70/28.21 % (379142)dis+10_1_sil=32000:si=on:sp=arity:random_seed=2457803171:i=206:fgj=on:rtra=on_2770 on theBenchmark for (2770ds/206Mi) % 198.70/28.21 % (379142)Instruction limit reached! % 198.70/28.21 % (379142)------------------------------ % 198.70/28.21 % (379142)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 198.70/28.21 % (379142)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 198.70/28.21 % (379142)CaDiCaL version: 2.1.3 % 198.70/28.21 % (379142)Termination reason: Instruction limit % 198.70/28.21 % (379142)Termination phase: Saturation % 198.70/28.21 % (379142)Time elapsed: 0.125 s % 198.70/28.21 % (379142)Peak memory usage: 13 MB % 198.70/28.21 % (379142)Instructions burned: 206 (million) % 198.70/28.21 % (379144)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=2355024522:i=232:rtra=on_2768 on theBenchmark for (2768ds/232Mi) % 198.70/28.21 % (379144)Instruction limit reached! % 198.70/28.21 % (379144)------------------------------ % 198.70/28.21 % (379144)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 198.70/28.21 % (379144)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 198.70/28.21 % (379144)CaDiCaL version: 2.1.3 % 198.70/28.21 % (379144)Termination reason: Instruction limit % 198.70/28.21 % (379144)Termination phase: Saturation % 198.70/28.21 % (379144)Time elapsed: 0.148 s % 198.70/28.21 % (379144)Peak memory usage: 13 MB % 198.70/28.21 % (379144)Instructions burned: 232 (million) % 198.70/28.21 % (379146)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=3810160796:i=262:rtra=on_2767 on theBenchmark for (2767ds/262Mi) % 198.70/28.21 % (379146)Instruction limit reached! % 198.70/28.21 % (379146)------------------------------ % 198.70/28.21 % (379146)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 198.70/28.21 % (379146)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 198.70/28.21 % (379146)CaDiCaL version: 2.1.3 % 198.70/28.21 % (379146)Termination reason: Instruction limit % 198.70/28.21 % (379146)Termination phase: Saturation % 198.70/28.21 % (379146)Time elapsed: 0.160 s % 198.70/28.21 % (379146)Peak memory usage: 14 MB % 198.70/28.21 % (379146)Instructions burned: 263 (million) % 198.70/28.21 % (379148)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=3927505977:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2765 on theBenchmark for (2765ds/318Mi) % 198.70/28.21 % (379148)Instruction limit reached! % 198.70/28.21 % (379148)------------------------------ % 198.70/28.21 % (379148)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 198.70/28.21 % (379148)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 198.70/28.21 % (379148)CaDiCaL version: 2.1.3 % 198.70/28.21 % (379148)Termination reason: Instruction limit % 198.70/28.21 % (379148)Termination phase: Saturation % 198.70/28.21 % (379148)Time elapsed: 0.225 s % 198.70/28.21 % (379148)Peak memory usage: 15 MB % 198.70/28.21 % (379148)Instructions burned: 318 (million) % 198.70/28.21 % (379150)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=364331441:i=1428:nm=2:rtra=on_2762 on theBenchmark for (2762ds/1428Mi) % 198.70/28.21 % (379150)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 198.70/28.21 % (379150)Terminated due to inappropriate strategy. % 198.70/28.21 % (379150)------------------------------ % 198.70/28.21 % (379150)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 198.70/28.21 % (379150)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 198.70/28.21 % (379150)CaDiCaL version: 2.1.3 % 198.70/28.21 % (379150)Termination reason: Inappropriate % 198.70/28.21 % (379150)Time elapsed: 0.001 s % 198.70/28.21 % (379150)Peak memory usage: 10 MB % 198.70/28.21 % (379150)Instructions burned: 2 (million) % 198.70/28.21 % (379150)------------------------------ % 198.70/28.21 % (379150)------------------------------ % 222.83/31.63 % (379152)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=3967254713:i=262:bd=preordered:rtra=on:fsd=on_2762 on theBenchmark for (2762ds/262Mi) % 222.83/31.63 % (379152)Instruction limit reached! % 222.83/31.63 % (379152)------------------------------ % 222.83/31.63 % (379152)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 222.83/31.63 % (379152)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 222.83/31.63 % (379152)CaDiCaL version: 2.1.3 % 222.83/31.63 % (379152)Termination reason: Instruction limit % 222.83/31.63 % (379152)Termination phase: Saturation % 222.83/31.63 % (379152)Time elapsed: 0.181 s % 222.83/31.63 % (379152)Peak memory usage: 14 MB % 222.83/31.63 % (379152)Instructions burned: 262 (million) % 222.83/31.63 % (379154)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=3952531498:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2760 on theBenchmark for (2760ds/1368Mi) % 222.83/31.63 % (379154)Instruction limit reached! % 222.83/31.63 % (379154)------------------------------ % 222.83/31.63 % (379154)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 222.83/31.63 % (379154)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 222.83/31.63 % (379154)CaDiCaL version: 2.1.3 % 222.83/31.63 % (379154)Termination reason: Instruction limit % 222.83/31.63 % (379154)Termination phase: Saturation % 222.83/31.63 % (379154)Time elapsed: 0.703 s % 222.83/31.63 % (379154)Peak memory usage: 17 MB % 222.83/31.63 % (379154)Instructions burned: 1369 (million) % 222.83/31.63 % (379156)ott-21_1_sil=16000:si=on:fs=off:random_seed=3233701268:i=360:av=off:fsr=off:rtra=on_2753 on theBenchmark for (2753ds/360Mi) % 222.83/31.63 % (379156)Instruction limit reached! % 222.83/31.63 % (379156)------------------------------ % 222.83/31.63 % (379156)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 222.83/31.63 % (379156)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 222.83/31.63 % (379156)CaDiCaL version: 2.1.3 % 222.83/31.63 % (379156)Termination reason: Instruction limit % 222.83/31.63 % (379156)Termination phase: Saturation % 222.83/31.63 % (379156)Time elapsed: 0.165 s % 222.83/31.63 % (379156)Peak memory usage: 13 MB % 222.83/31.63 % (379156)Instructions burned: 360 (million) % 222.83/31.63 % (379158)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=416672263:i=954:bd=all:rtra=on_2751 on theBenchmark for (2751ds/954Mi) % 222.83/31.63 % (379158)Instruction limit reached! % 222.83/31.63 % (379158)------------------------------ % 222.83/31.63 % (379158)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 222.83/31.63 % (379158)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 222.83/31.63 % (379158)CaDiCaL version: 2.1.3 % 222.83/31.63 % (379158)Termination reason: Instruction limit % 222.83/31.63 % (379158)Termination phase: Saturation % 222.83/31.63 % (379158)Time elapsed: 0.622 s % 222.83/31.63 % (379158)Peak memory usage: 16 MB % 222.83/31.63 % (379158)Instructions burned: 954 (million) % 222.83/31.63 % (379160)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=296615167:fmbsr=1.3:i=1730:ins=25:rtra=on_2745 on theBenchmark for (2745ds/1730Mi) % 222.83/31.63 % (379160)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 222.83/31.63 % (379160)Terminated due to inappropriate strategy. % 222.83/31.63 % (379160)------------------------------ % 222.83/31.63 % (379160)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 222.83/31.63 % (379160)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 222.83/31.63 % (379160)CaDiCaL version: 2.1.3 % 222.83/31.63 % (379160)Termination reason: Inappropriate % 222.83/31.63 % (379160)Time elapsed: 0.001 s % 222.83/31.63 % (379160)Peak memory usage: 10 MB % 222.83/31.63 % (379160)Instructions burned: 1 (million) % 222.83/31.63 % (379160)------------------------------ % 222.83/31.63 % (379160)------------------------------ % 222.83/31.63 % (379162)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=865231822:i=2358:rtra=on_2744 on theBenchmark for (2744ds/2358Mi) % 222.83/31.63 % (379162)Instruction limit reached! % 222.83/31.63 % (379162)------------------------------ % 222.83/31.63 % (379162)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 222.83/31.63 % (379162)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 222.83/31.63 % (379162)CaDiCaL version: 2.1.3 % 222.83/31.63 % (379162)Termination reason: Instruction limit % 222.83/31.63 % (379162)Termination phase: Saturation % 272.52/38.61 % (379162)Time elapsed: 1.487 s % 272.52/38.61 % (379162)Peak memory usage: 27 MB % 272.52/38.61 % (379162)Instructions burned: 2358 (million) % 272.52/38.61 % (379164)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=1239049997:i=1778:ins=1:rtra=on_2729 on theBenchmark for (2729ds/1778Mi) % 272.52/38.61 % (379164)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 272.52/38.61 % (379164)Terminated due to inappropriate strategy. % 272.52/38.61 % (379164)------------------------------ % 272.52/38.61 % (379164)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 272.52/38.61 % (379164)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 272.52/38.61 % (379164)CaDiCaL version: 2.1.3 % 272.52/38.61 % (379164)Termination reason: Inappropriate % 272.52/38.61 % (379164)Time elapsed: 0.001 s % 272.52/38.61 % (379164)Peak memory usage: 10 MB % 272.52/38.61 % (379164)Instructions burned: 2 (million) % 272.52/38.61 % (379164)------------------------------ % 272.52/38.61 % (379164)------------------------------ % 272.52/38.61 % (379166)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=3065075048:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2729 on theBenchmark for (2729ds/1384Mi) % 272.52/38.61 % (379069)Instruction limit reached! % 272.52/38.61 % (379069)------------------------------ % 272.52/38.61 % (379069)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 272.52/38.61 % (379069)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 272.52/38.61 % (379069)CaDiCaL version: 2.1.3 % 272.52/38.61 % (379069)Termination reason: Instruction limit % 272.52/38.61 % (379069)Termination phase: Saturation % 272.52/38.61 % (379069)Time elapsed: 10.322 s % 272.52/38.61 % (379069)Peak memory usage: 234 MB % 272.52/38.61 % (379069)Instructions burned: 17627 (million) % 272.52/38.61 % (379168)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=1719706382:i=1758:kws=inv_precedence:fsr=off:rtra=on_2722 on theBenchmark for (2722ds/1758Mi) % 272.52/38.61 % (379166)Instruction limit reached! % 272.52/38.61 % (379166)------------------------------ % 272.52/38.61 % (379166)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 272.52/38.61 % (379166)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 272.52/38.61 % (379166)CaDiCaL version: 2.1.3 % 272.52/38.61 % (379166)Termination reason: Instruction limit % 272.52/38.61 % (379166)Termination phase: Saturation % 272.52/38.61 % (379166)Time elapsed: 0.890 s % 272.52/38.61 % (379166)Peak memory usage: 24 MB % 272.52/38.61 % (379166)Instructions burned: 1384 (million) % 272.52/38.61 % (379170)fmb+10_1_sil=64000:si=on:random_seed=3732304779:i=44122:nm=2:rtra=on:gsp=on_2720 on theBenchmark for (2720ds/44122Mi) % 272.52/38.61 % (379170)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 272.52/38.61 % (379170)Terminated due to inappropriate strategy. % 272.52/38.61 % (379170)------------------------------ % 272.52/38.61 % (379170)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 272.52/38.61 % (379170)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 272.52/38.61 % (379170)CaDiCaL version: 2.1.3 % 272.52/38.61 % (379170)Termination reason: Inappropriate % 272.52/38.61 % (379170)Time elapsed: 0.001 s % 272.52/38.61 % (379170)Peak memory usage: 10 MB % 272.52/38.61 % (379170)Instructions burned: 2 (million) % 272.52/38.61 % (379170)------------------------------ % 272.52/38.61 % (379170)------------------------------ % 272.52/38.61 % (379172)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=4243930417:i=19030:nm=5:rtra=on_2720 on theBenchmark for (2720ds/19030Mi) % 272.52/38.61 % (379172)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 272.52/38.61 % (379172)Terminated due to inappropriate strategy. % 272.52/38.61 % (379172)------------------------------ % 272.52/38.61 % (379172)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 272.52/38.61 % (379172)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 272.52/38.61 % (379172)CaDiCaL version: 2.1.3 % 272.52/38.61 % (379172)Termination reason: Inappropriate % 272.52/38.61 % (379172)Time elapsed: 0.001 s % 272.52/38.61 % (379172)Peak memory usage: 10 MB % 272.52/38.61 % (379172)Instructions burned: 2 (million) % 272.52/38.61 % (379172)------------------------------ % 272.52/38.61 % (379172)------------------------------ % 272.52/38.61 % (379174)fmb+10_1_sil=64000:sas=cadical:si=on:fmbss=8:random_seed=2551884002:fmbsr=1.7:i=1840:rtra=on_2720 on theBenchmark for (2720ds/1840Mi) % 299.49/42.41 % (379174)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 299.49/42.41 % (379174)Terminated due to inappropriate strategy. % 299.49/42.41 % (379174)------------------------------ % 299.49/42.41 % (379174)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 299.49/42.41 % (379174)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 299.49/42.41 % (379174)CaDiCaL version: 2.1.3 % 299.49/42.41 % (379174)Termination reason: Inappropriate % 299.49/42.41 % (379174)Time elapsed: 0.001 s % 299.49/42.41 % (379174)Peak memory usage: 10 MB % 299.49/42.41 % (379174)Instructions burned: 2 (million) % 299.49/42.41 % (379174)------------------------------ % 299.49/42.41 % (379174)------------------------------ % 299.49/42.41 % (379176)dis-4_1_sil=16000:drc=ordering:si=on:sp=const_frequency:sac=on:newcnf=on:random_seed=3829149767:i=10262:rtra=on_2719 on theBenchmark for (2719ds/10262Mi) % 299.49/42.41 % (379168)Instruction limit reached! % 299.49/42.41 % (379168)------------------------------ % 299.49/42.41 % (379168)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 299.49/42.41 % (379168)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 299.49/42.41 % (379168)CaDiCaL version: 2.1.3 % 299.49/42.41 % (379168)Termination reason: Instruction limit % 299.49/42.41 % (379168)Termination phase: Saturation % 299.49/42.41 % (379168)Time elapsed: 0.979 s % 299.49/42.41 % (379168)Peak memory usage: 24 MB % 299.49/42.41 % (379168)Instructions burned: 1759 (million) % 299.49/42.41 % (379179)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:si=on:sp=arity:spb=units:lsd=10:nwc=3:random_seed=553777361:i=2944:ins=7:rtra=on:fdi=8:gsp=on_2712 on theBenchmark for (2712ds/2944Mi) % 299.49/42.41 % (379179)Instruction limit reached! % 299.49/42.41 % (379179)------------------------------ % 299.49/42.41 % (379179)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 299.49/42.41 % (379179)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 299.49/42.41 % (379179)CaDiCaL version: 2.1.3 % 299.49/42.41 % (379179)Termination reason: Instruction limit % 299.49/42.41 % (379179)Termination phase: Saturation % 299.49/42.41 % (379179)Time elapsed: 1.525 s % 299.49/42.41 % (379179)Peak memory usage: 54 MB % 299.49/42.41 % (379179)Instructions burned: 2944 (million) % 299.49/42.41 % (379181)fmb+10_1_sil=16000:sas=cadical:si=on:bce=on:fmbss=77:random_seed=3019914159:i=12648:rtra=on_2697 on theBenchmark for (2697ds/12648Mi) % 299.49/42.41 % (379181)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 299.49/42.41 % (379181)Terminated due to inappropriate strategy. % 299.49/42.41 % (379181)------------------------------ % 299.49/42.41 % (379181)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 299.49/42.41 % (379181)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 299.49/42.41 % (379181)CaDiCaL version: 2.1.3 % 299.49/42.41 % (379181)Termination reason: Inappropriate % 299.49/42.41 % (379181)Time elapsed: 0.001 s % 299.49/42.41 % (379181)Peak memory usage: 10 MB % 299.49/42.41 % (379181)Instructions burned: 2 (million) % 299.49/42.41 % (379181)------------------------------ % 299.49/42.41 % (379181)------------------------------ % 299.49/42.41 % (379183)fmb+10_1_fmbas=function:sil=32000:sas=cadical:si=on:fmbss=16:random_seed=3340765525:fmbsr=2.30978:i=4348:rtra=on_2697 on theBenchmark for (2697ds/4348Mi) % 299.49/42.41 % (379183)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 299.49/42.41 % (379183)Terminated due to inappropriate strategy. % 299.49/42.41 % (379183)------------------------------ % 299.49/42.41 % (379183)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 299.49/42.41 % (379183)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 299.49/42.41 % (379183)CaDiCaL version: 2.1.3 % 299.49/42.41 % (379183)Termination reason: Inappropriate % 299.49/42.41 % (379183)Time elapsed: 0.001 s % 299.49/42.41 % (379183)Peak memory usage: 10 MB % 299.49/42.41 % (379183)Instructions burned: 2 (million) % 299.49/42.41 % (379183)------------------------------ % 299.49/42.41 % (379183)------------------------------ % 299.49/42.41 % (379185)ott-2_1_sil=16000:si=on:newcnf=on:random_seed=2670520315:avsq=on:i=1738:avsqr=1,16:kws=inv_arity_squared:rtra=on_2696 on theBenchmark for (2696ds/1738Mi) % 299.49/42.41 % (379185)Instruction limit reached! % 299.49/42.41 % (379185)------------------------------ % 299.49/42.41 % (379185)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 299.49/42.41 % (379185)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9aTerminated % 300.16/42.54 % Vampire exiting %------------------------------------------------------------------------------