%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : NUM897_1 : TPTP v9.3.1. Released v5.0.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % Computer : n016.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 29 12:26:01 PM UTC 2026 % Result : Timeout 300.18s 42.74s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : NUM897_1 : TPTP v9.3.1. Released v5.0.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.11/0.36 % Computer : n016.cluster.edu % 0.11/0.36 % Model : x86_64 x86_64 % 0.11/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.36 % Memory : 8046.5625MB % 0.11/0.36 % OS : Linux 6.8.0-71-generic % 0.05/0.36 % CPULimit : 300 % 0.05/0.36 % WCLimit : 300 % 0.05/0.36 % DateTime : Sun Sep 27 21:43:18 UTC 2026 % 0.05/0.36 % CPUTime : % 0.05/0.36 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.05/0.39 Running first-order model finding % 0.05/0.39 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 % 2.35/0.97 % (3016399)Will run a generic schedule for satisfiability detection. % 2.35/0.97 % (3016404)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1726399817_2999 on theBenchmark for (2999ds/0Mi) % 2.35/0.97 % (3016404)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 2.35/0.97 % (3016404)Terminated due to inappropriate strategy. % 2.35/0.97 % (3016404)------------------------------ % 2.35/0.97 % (3016404)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 2.35/0.97 % (3016404)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 2.35/0.97 % (3016404)CaDiCaL version: 2.1.3 % 2.35/0.97 % (3016404)Termination reason: Inappropriate % 2.35/0.97 % (3016404)Time elapsed: 0.0000 s % 2.35/0.97 % (3016404)Peak memory usage: 10 MB % 2.35/0.97 % (3016404)------------------------------ % 2.35/0.97 % (3016404)------------------------------ % 2.35/0.97 % (3016405)% WARNING: option uhcvi not known. % 2.35/0.97 % (3016406)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3462300825:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 2.35/0.97 % (3016410)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1639610556:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 2.35/0.97 % (3016407)dis+10_1_sil=32000:sp=arity:random_seed=1546339236:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 2.35/0.97 % (3016408)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3731961954:i=116_2999 on theBenchmark for (2999ds/116Mi) % 2.35/0.97 % (3016409)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3929141309:i=131_2999 on theBenchmark for (2999ds/131Mi) % 2.35/0.97 % (3016405)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3976523123:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 2.35/0.97 % (3016412)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2606777411:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 2.35/0.97 % (3016412)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 2.35/0.97 % (3016412)Terminated due to inappropriate strategy. % 2.35/0.97 % (3016412)------------------------------ % 2.35/0.97 % (3016412)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 2.35/0.97 % (3016412)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 2.35/0.97 % (3016412)CaDiCaL version: 2.1.3 % 2.35/0.97 % (3016412)Termination reason: Inappropriate % 2.35/0.97 % (3016412)Time elapsed: 0.0000 s % 2.35/0.97 % (3016412)Peak memory usage: 10 MB % 2.35/0.97 % (3016412)------------------------------ % 2.35/0.97 % (3016412)------------------------------ % 2.35/0.97 % (3016420)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3778026419:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 2.35/0.97 % (3016420)Instruction limit reached! % 2.35/0.97 % (3016420)------------------------------ % 2.35/0.97 % (3016420)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 2.35/0.97 % (3016420)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 2.35/0.97 % (3016420)CaDiCaL version: 2.1.3 % 2.35/0.97 % (3016420)Termination reason: Instruction limit % 2.35/0.97 % (3016420)Termination phase: Saturation % 2.35/0.97 % (3016420)Time elapsed: 0.048 s % 2.35/0.97 % (3016420)Peak memory usage: 12 MB % 2.35/0.97 % (3016420)Instructions burned: 132 (million) % 2.35/0.97 % (3016407)Instruction limit reached! % 2.35/0.97 % (3016407)------------------------------ % 2.35/0.97 % (3016407)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 2.35/0.97 % (3016407)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 2.35/0.97 % (3016407)CaDiCaL version: 2.1.3 % 2.35/0.97 % (3016407)Termination reason: Instruction limit % 2.35/0.97 % (3016407)Termination phase: Saturation % 2.35/0.97 % (3016407)Time elapsed: 0.066 s % 2.35/0.97 % (3016407)Peak memory usage: 12 MB % 2.35/0.97 % (3016407)Instructions burned: 104 (million) % 2.35/0.97 % (3016408)Instruction limit reached! % 2.35/0.97 % (3016408)------------------------------ % 2.35/0.97 % (3016408)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 2.35/0.97 % (3016408)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 2.35/0.97 % (3016408)CaDiCaL version: 2.1.3 % 2.35/0.97 % (3016408)Termination reason: Instruction limit % 2.35/0.97 % (3016408)Termination phase: Saturation % 2.35/0.97 % (3016408)Time elapsed: 0.070 s % 5.85/1.30 % (3016408)Peak memory usage: 12 MB % 5.85/1.30 % (3016408)Instructions burned: 117 (million) % 5.85/1.30 % (3016422)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=3553396806:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi) % 5.85/1.30 % (3016409)Instruction limit reached! % 5.85/1.30 % (3016409)------------------------------ % 5.85/1.30 % (3016409)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.85/1.30 % (3016409)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.85/1.30 % (3016409)CaDiCaL version: 2.1.3 % 5.85/1.30 % (3016409)Termination reason: Instruction limit % 5.85/1.30 % (3016409)Termination phase: Saturation % 5.85/1.30 % (3016409)Time elapsed: 0.081 s % 5.85/1.30 % (3016409)Peak memory usage: 12 MB % 5.85/1.30 % (3016409)Instructions burned: 131 (million) % 5.85/1.30 % (3016423)ott-21_1_sil=16000:fs=off:random_seed=1165867105:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi) % 5.85/1.30 % (3016424)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3883407125:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 5.85/1.30 % (3016426)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=829697911:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 5.85/1.30 % (3016426)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 5.85/1.30 % (3016426)Terminated due to inappropriate strategy. % 5.85/1.30 % (3016426)------------------------------ % 5.85/1.30 % (3016426)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.85/1.30 % (3016426)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.85/1.30 % (3016426)CaDiCaL version: 2.1.3 % 5.85/1.30 % (3016426)Termination reason: Inappropriate % 5.85/1.30 % (3016426)Time elapsed: 0.0000 s % 5.85/1.30 % (3016426)Peak memory usage: 10 MB % 5.85/1.30 % (3016426)------------------------------ % 5.85/1.30 % (3016426)------------------------------ % 5.85/1.30 % (3016410)Instruction limit reached! % 5.85/1.30 % (3016410)------------------------------ % 5.85/1.30 % (3016410)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.85/1.30 % (3016410)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.85/1.30 % (3016410)CaDiCaL version: 2.1.3 % 5.85/1.30 % (3016410)Termination reason: Instruction limit % 5.85/1.30 % (3016410)Termination phase: Saturation % 5.85/1.30 % (3016410)Time elapsed: 0.112 s % 5.85/1.30 % (3016410)Peak memory usage: 13 MB % 5.85/1.30 % (3016410)Instructions burned: 160 (million) % 5.85/1.30 % (3016430)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=977974965:i=1179_2998 on theBenchmark for (2998ds/1179Mi) % 5.85/1.30 % (3016431)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=134383953:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi) % 5.85/1.30 % (3016431)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 5.85/1.30 % (3016431)Terminated due to inappropriate strategy. % 5.85/1.30 % (3016431)------------------------------ % 5.85/1.30 % (3016431)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.85/1.30 % (3016431)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.85/1.30 % (3016431)CaDiCaL version: 2.1.3 % 5.85/1.30 % (3016431)Termination reason: Inappropriate % 5.85/1.30 % (3016431)Time elapsed: 0.0000 s % 5.85/1.30 % (3016431)Peak memory usage: 10 MB % 5.85/1.30 % (3016431)------------------------------ % 5.85/1.30 % (3016431)------------------------------ % 5.85/1.30 % (3016434)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=916377194: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) % 5.85/1.30 % (3016423)Instruction limit reached! % 5.85/1.30 % (3016423)------------------------------ % 5.85/1.30 % (3016423)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.85/1.30 % (3016423)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.85/1.30 % (3016423)CaDiCaL version: 2.1.3 % 5.85/1.30 % (3016423)Termination reason: Instruction limit % 5.85/1.30 % (3016423)Termination phase: Saturation % 5.85/1.30 % (3016423)Time elapsed: 0.082 s % 5.85/1.30 % (3016423)Peak memory usage: 12 MB % 5.85/1.30 % (3016423)Instructions burned: 181 (million) % 5.85/1.30 % (3016436)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3352697034:i=879:kws=inv_precedence:fsr=off_2998 on theBenchmark for (2998ds/879Mi) % 21.16/3.48 % (3016422)Instruction limit reached! % 21.16/3.48 % (3016422)------------------------------ % 21.16/3.48 % (3016422)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 21.16/3.48 % (3016422)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.16/3.48 % (3016422)CaDiCaL version: 2.1.3 % 21.16/3.48 % (3016422)Termination reason: Instruction limit % 21.16/3.48 % (3016422)Termination phase: Saturation % 21.16/3.48 % (3016422)Time elapsed: 0.210 s % 21.16/3.48 % (3016422)Peak memory usage: 16 MB % 21.16/3.48 % (3016422)Instructions burned: 684 (million) % 21.16/3.48 % (3016438)fmb+10_1_sil=64000:random_seed=186242604:i=22061:nm=2:gsp=on_2996 on theBenchmark for (2996ds/22061Mi) % 21.16/3.48 % (3016438)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 21.16/3.48 % (3016438)Terminated due to inappropriate strategy. % 21.16/3.48 % (3016438)------------------------------ % 21.16/3.48 % (3016438)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 21.16/3.48 % (3016438)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.16/3.48 % (3016438)CaDiCaL version: 2.1.3 % 21.16/3.48 % (3016438)Termination reason: Inappropriate % 21.16/3.48 % (3016438)Time elapsed: 0.0000 s % 21.16/3.48 % (3016438)Peak memory usage: 10 MB % 21.16/3.48 % (3016438)------------------------------ % 21.16/3.48 % (3016438)------------------------------ % 21.16/3.48 % (3016440)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2912231171:i=9515:nm=5_2996 on theBenchmark for (2996ds/9515Mi) % 21.16/3.48 % (3016440)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 21.16/3.48 % (3016440)Terminated due to inappropriate strategy. % 21.16/3.48 % (3016440)------------------------------ % 21.16/3.48 % (3016440)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 21.16/3.48 % (3016440)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.16/3.48 % (3016440)CaDiCaL version: 2.1.3 % 21.16/3.48 % (3016440)Termination reason: Inappropriate % 21.16/3.48 % (3016440)Time elapsed: 0.0000 s % 21.16/3.48 % (3016440)Peak memory usage: 10 MB % 21.16/3.48 % (3016440)------------------------------ % 21.16/3.48 % (3016440)------------------------------ % 21.16/3.48 % (3016442)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=818394106:fmbsr=1.7:i=920_2996 on theBenchmark for (2996ds/920Mi) % 21.16/3.48 % (3016442)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 21.16/3.48 % (3016442)Terminated due to inappropriate strategy. % 21.16/3.48 % (3016442)------------------------------ % 21.16/3.48 % (3016442)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 21.16/3.48 % (3016442)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.16/3.48 % (3016442)CaDiCaL version: 2.1.3 % 21.16/3.48 % (3016442)Termination reason: Inappropriate % 21.16/3.48 % (3016442)Time elapsed: 0.0000 s % 21.16/3.48 % (3016442)Peak memory usage: 10 MB % 21.16/3.48 % (3016442)------------------------------ % 21.16/3.48 % (3016442)------------------------------ % 21.16/3.48 % (3016444)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2495973633:i=5131_2996 on theBenchmark for (2996ds/5131Mi) % 21.16/3.48 % (3016424)Instruction limit reached! % 21.16/3.48 % (3016424)------------------------------ % 21.16/3.48 % (3016424)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 21.16/3.48 % (3016424)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.16/3.48 % (3016424)CaDiCaL version: 2.1.3 % 21.16/3.48 % (3016424)Termination reason: Instruction limit % 21.16/3.48 % (3016424)Termination phase: Saturation % 21.16/3.48 % (3016424)Time elapsed: 0.306 s % 21.16/3.48 % (3016424)Peak memory usage: 13 MB % 21.16/3.48 % (3016424)Instructions burned: 477 (million) % 21.16/3.48 % (3016446)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=942850069:i=1472:ins=7:fdi=8:gsp=on_2995 on theBenchmark for (2995ds/1472Mi) % 21.16/3.48 % (3016434)Instruction limit reached! % 21.16/3.48 % (3016434)------------------------------ % 21.16/3.48 % (3016434)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 21.16/3.48 % (3016434)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.16/3.48 % (3016434)CaDiCaL version: 2.1.3 % 21.16/3.48 % (3016434)Termination reason: Instruction limit % 27.63/4.37 % (3016434)Termination phase: Saturation % 27.63/4.37 % (3016434)Time elapsed: 0.386 s % 27.63/4.37 % (3016434)Peak memory usage: 16 MB % 27.63/4.37 % (3016434)Instructions burned: 693 (million) % 27.63/4.37 % (3016448)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3624312356:i=6324_2994 on theBenchmark for (2994ds/6324Mi) % 27.63/4.37 % (3016448)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 27.63/4.37 % (3016448)Terminated due to inappropriate strategy. % 27.63/4.37 % (3016448)------------------------------ % 27.63/4.37 % (3016448)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 27.63/4.37 % (3016448)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.63/4.37 % (3016448)CaDiCaL version: 2.1.3 % 27.63/4.37 % (3016448)Termination reason: Inappropriate % 27.63/4.37 % (3016448)Time elapsed: 0.0000 s % 27.63/4.37 % (3016448)Peak memory usage: 10 MB % 27.63/4.37 % (3016448)------------------------------ % 27.63/4.37 % (3016448)------------------------------ % 27.63/4.37 % (3016450)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=2065402268:fmbsr=2.30978:i=2174_2994 on theBenchmark for (2994ds/2174Mi) % 27.63/4.37 % (3016450)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 27.63/4.37 % (3016450)Terminated due to inappropriate strategy. % 27.63/4.37 % (3016450)------------------------------ % 27.63/4.37 % (3016450)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 27.63/4.37 % (3016450)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.63/4.37 % (3016450)CaDiCaL version: 2.1.3 % 27.63/4.37 % (3016450)Termination reason: Inappropriate % 27.63/4.37 % (3016450)Time elapsed: 0.0000 s % 27.63/4.37 % (3016450)Peak memory usage: 10 MB % 27.63/4.37 % (3016450)------------------------------ % 27.63/4.37 % (3016450)------------------------------ % 27.63/4.37 % (3016452)ott-2_1_sil=16000:newcnf=on:random_seed=1603749445:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2994 on theBenchmark for (2994ds/869Mi) % 27.63/4.37 % (3016436)Instruction limit reached! % 27.63/4.37 % (3016436)------------------------------ % 27.63/4.37 % (3016436)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 27.63/4.37 % (3016436)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.63/4.37 % (3016436)CaDiCaL version: 2.1.3 % 27.63/4.37 % (3016436)Termination reason: Instruction limit % 27.63/4.37 % (3016436)Termination phase: Saturation % 27.63/4.37 % (3016436)Time elapsed: 0.503 s % 27.63/4.37 % (3016436)Peak memory usage: 19 MB % 27.63/4.37 % (3016436)Instructions burned: 880 (million) % 27.63/4.37 % (3016454)ott+10_1_sil=32000:tgt=ground:random_seed=2802171861:i=5114:av=off_2992 on theBenchmark for (2992ds/5114Mi) % 27.63/4.37 % (3016430)Instruction limit reached! % 27.63/4.37 % (3016430)------------------------------ % 27.63/4.37 % (3016430)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 27.63/4.37 % (3016430)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.63/4.37 % (3016430)CaDiCaL version: 2.1.3 % 27.63/4.37 % (3016430)Termination reason: Instruction limit % 27.63/4.37 % (3016430)Termination phase: Saturation % 27.63/4.37 % (3016430)Time elapsed: 0.728 s % 27.63/4.37 % (3016430)Peak memory usage: 17 MB % 27.63/4.37 % (3016430)Instructions burned: 1180 (million) % 27.63/4.37 % (3016452)Instruction limit reached! % 27.63/4.37 % (3016452)------------------------------ % 27.63/4.37 % (3016452)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 27.63/4.37 % (3016452)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.63/4.37 % (3016452)CaDiCaL version: 2.1.3 % 27.63/4.37 % (3016452)Termination reason: Instruction limit % 27.63/4.37 % (3016452)Termination phase: Saturation % 27.63/4.37 % (3016452)Time elapsed: 0.287 s % 27.63/4.37 % (3016452)Peak memory usage: 16 MB % 27.63/4.37 % (3016452)Instructions burned: 871 (million) % 27.63/4.37 % (3016456)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=3316452292:i=54282_2991 on theBenchmark for (2991ds/54282Mi) % 27.63/4.37 % (3016456)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 27.63/4.37 % (3016456)Terminated due to inappropriate strategy. % 27.63/4.37 % (3016456)------------------------------ % 27.63/4.37 % (3016456)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 27.63/4.37 % (3016456)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.63/4.37 % (3016456)CaDiCaL version: 2.1.3 % 27.63/4.37 % (3016456)Termination reason: Inappropriate % 97.46/14.19 % (3016456)Time elapsed: 0.0000 s % 97.46/14.19 % (3016456)Peak memory usage: 10 MB % 97.46/14.19 % (3016456)------------------------------ % 97.46/14.19 % (3016456)------------------------------ % 97.46/14.19 % (3016457)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=2890210301:i=3512:aac=none_2991 on theBenchmark for (2991ds/3512Mi) % 97.46/14.19 % (3016459)dis+21_1_sil=32000:sas=cadical:random_seed=370248294:i=3773:amm=off_2990 on theBenchmark for (2990ds/3773Mi) % 97.46/14.19 % (3016446)Instruction limit reached! % 97.46/14.19 % (3016446)------------------------------ % 97.46/14.19 % (3016446)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 97.46/14.19 % (3016446)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 97.46/14.19 % (3016446)CaDiCaL version: 2.1.3 % 97.46/14.19 % (3016446)Termination reason: Instruction limit % 97.46/14.19 % (3016446)Termination phase: Saturation % 97.46/14.19 % (3016446)Time elapsed: 0.735 s % 97.46/14.19 % (3016446)Peak memory usage: 23 MB % 97.46/14.19 % (3016446)Instructions burned: 1473 (million) % 97.46/14.19 % (3016462)ott+11_1_sil=16000:gs=on:random_seed=2024105650:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2988 on theBenchmark for (2988ds/2251Mi) % 97.46/14.19 % (3016457)Instruction limit reached! % 97.46/14.19 % (3016457)------------------------------ % 97.46/14.19 % (3016457)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 97.46/14.19 % (3016457)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 97.46/14.19 % (3016457)CaDiCaL version: 2.1.3 % 97.46/14.19 % (3016457)Termination reason: Instruction limit % 97.46/14.19 % (3016457)Termination phase: Saturation % 97.46/14.19 % (3016457)Time elapsed: 1.012 s % 97.46/14.19 % (3016457)Peak memory usage: 30 MB % 97.46/14.19 % (3016457)Instructions burned: 3516 (million) % 97.46/14.19 % (3016464)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=3976709080:fmbsr=1.6:i=67534_2980 on theBenchmark for (2980ds/67534Mi) % 97.46/14.19 % (3016464)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 97.46/14.19 % (3016464)Terminated due to inappropriate strategy. % 97.46/14.19 % (3016464)------------------------------ % 97.46/14.19 % (3016464)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 97.46/14.19 % (3016464)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 97.46/14.19 % (3016464)CaDiCaL version: 2.1.3 % 97.46/14.19 % (3016464)Termination reason: Inappropriate % 97.46/14.19 % (3016464)Time elapsed: 0.0000 s % 97.46/14.19 % (3016464)Peak memory usage: 10 MB % 97.46/14.19 % (3016464)------------------------------ % 97.46/14.19 % (3016464)------------------------------ % 97.46/14.19 % (3016466)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=3777330135:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2980 on theBenchmark for (2980ds/4591Mi) % 97.46/14.19 % (3016462)Instruction limit reached! % 97.46/14.19 % (3016462)------------------------------ % 97.46/14.19 % (3016462)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 97.46/14.19 % (3016462)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 97.46/14.19 % (3016462)CaDiCaL version: 2.1.3 % 97.46/14.19 % (3016462)Termination reason: Instruction limit % 97.46/14.19 % (3016462)Termination phase: Saturation % 97.46/14.19 % (3016462)Time elapsed: 1.209 s % 97.46/14.19 % (3016462)Peak memory usage: 21 MB % 97.46/14.19 % (3016462)Instructions burned: 2251 (million) % 97.46/14.19 % (3016468)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=4014787429:i=29340_2975 on theBenchmark for (2975ds/29340Mi) % 97.46/14.19 % (3016459)Instruction limit reached! % 97.46/14.19 % (3016459)------------------------------ % 97.46/14.19 % (3016459)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 97.46/14.19 % (3016459)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 97.46/14.19 % (3016459)CaDiCaL version: 2.1.3 % 97.46/14.19 % (3016459)Termination reason: Instruction limit % 97.46/14.19 % (3016459)Termination phase: Saturation % 97.46/14.19 % (3016459)Time elapsed: 1.994 s % 97.46/14.19 % (3016459)Peak memory usage: 29 MB % 97.46/14.19 % (3016459)Instructions burned: 3773 (million) % 97.46/14.19 % (3016470)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=2727141628:i=5211_2970 on theBenchmark for (2970ds/5211Mi) % 97.46/14.19 % (3016444)Instruction limit reached! % 97.46/14.19 % (3016444)------------------------------ % 97.46/14.19 % (3016444)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 126.27/18.20 % (3016444)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 126.27/18.20 % (3016444)CaDiCaL version: 2.1.3 % 126.27/18.20 % (3016444)Termination reason: Instruction limit % 126.27/18.20 % (3016444)Termination phase: Saturation % 126.27/18.20 % (3016444)Time elapsed: 2.702 s % 126.27/18.20 % (3016444)Peak memory usage: 40 MB % 126.27/18.20 % (3016444)Instructions burned: 5132 (million) % 126.27/18.20 % (3016472)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=2660060739:i=5497:nm=2_2969 on theBenchmark for (2969ds/5497Mi) % 126.27/18.20 % (3016472)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 126.27/18.20 % (3016472)Terminated due to inappropriate strategy. % 126.27/18.20 % (3016472)------------------------------ % 126.27/18.20 % (3016472)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 126.27/18.20 % (3016472)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 126.27/18.20 % (3016472)CaDiCaL version: 2.1.3 % 126.27/18.20 % (3016472)Termination reason: Inappropriate % 126.27/18.20 % (3016472)Time elapsed: 0.0000 s % 126.27/18.20 % (3016472)Peak memory usage: 10 MB % 126.27/18.20 % (3016472)------------------------------ % 126.27/18.20 % (3016472)------------------------------ % 126.27/18.20 % (3016474)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=4206815383:fmbsr=2:i=46332_2968 on theBenchmark for (2968ds/46332Mi) % 126.27/18.20 % (3016474)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 126.27/18.20 % (3016474)Terminated due to inappropriate strategy. % 126.27/18.20 % (3016474)------------------------------ % 126.27/18.20 % (3016474)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 126.27/18.20 % (3016474)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 126.27/18.20 % (3016474)CaDiCaL version: 2.1.3 % 126.27/18.20 % (3016474)Termination reason: Inappropriate % 126.27/18.20 % (3016474)Time elapsed: 0.0000 s % 126.27/18.20 % (3016474)Peak memory usage: 10 MB % 126.27/18.20 % (3016474)------------------------------ % 126.27/18.20 % (3016474)------------------------------ % 126.27/18.20 % (3016476)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=3394252946:i=14071_2968 on theBenchmark for (2968ds/14071Mi) % 126.27/18.20 % (3016476)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 126.27/18.20 % (3016476)Terminated due to inappropriate strategy. % 126.27/18.20 % (3016476)------------------------------ % 126.27/18.20 % (3016476)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 126.27/18.20 % (3016476)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 126.27/18.20 % (3016476)CaDiCaL version: 2.1.3 % 126.27/18.20 % (3016476)Termination reason: Inappropriate % 126.27/18.20 % (3016476)Time elapsed: 0.0000 s % 126.27/18.20 % (3016476)Peak memory usage: 10 MB % 126.27/18.20 % (3016476)------------------------------ % 126.27/18.20 % (3016476)------------------------------ % 126.27/18.20 % (3016478)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=4033363521:i=22565:add=on:rawr=on_2968 on theBenchmark for (2968ds/22565Mi) % 126.27/18.20 % (3016466)Instruction limit reached! % 126.27/18.20 % (3016466)------------------------------ % 126.27/18.20 % (3016466)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 126.27/18.20 % (3016466)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 126.27/18.20 % (3016466)CaDiCaL version: 2.1.3 % 126.27/18.20 % (3016466)Termination reason: Instruction limit % 126.27/18.20 % (3016466)Termination phase: Saturation % 126.27/18.20 % (3016466)Time elapsed: 1.386 s % 126.27/18.20 % (3016466)Peak memory usage: 39 MB % 126.27/18.20 % (3016466)Instructions burned: 4595 (million) % 126.27/18.20 % (3016480)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=4128119026:i=8173:av=off_2966 on theBenchmark for (2966ds/8173Mi) % 126.27/18.20 % (3016454)Instruction limit reached! % 126.27/18.20 % (3016454)------------------------------ % 126.27/18.20 % (3016454)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 126.27/18.20 % (3016454)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 126.27/18.20 % (3016454)CaDiCaL version: 2.1.3 % 126.27/18.20 % (3016454)Termination reason: Instruction limit % 126.27/18.20 % (3016454)Termination phase: Saturation % 126.27/18.20 % (3016454)Time elapsed: 3.207 s % 126.27/18.20 % (3016454)Peak memory usage: 31 MB % 126.27/18.20 % (3016454)Instructions burned: 5115 (million) % 126.27/18.20 % (3016483)dis+10_16:1_sil=16000:random_seed=2324730063:i=9155:fsr=off_2960 on theBenchmark for (2960ds/9155Mi) % 155.39/22.37 % (3016470)Instruction limit reached! % 155.39/22.37 % (3016470)------------------------------ % 155.39/22.37 % (3016470)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 155.39/22.37 % (3016470)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 155.39/22.37 % (3016470)CaDiCaL version: 2.1.3 % 155.39/22.37 % (3016470)Termination reason: Instruction limit % 155.39/22.37 % (3016470)Termination phase: Saturation % 155.39/22.37 % (3016470)Time elapsed: 2.773 s % 155.39/22.37 % (3016470)Peak memory usage: 44 MB % 155.39/22.37 % (3016470)Instructions burned: 5213 (million) % 155.39/22.37 % (3016485)ott-3_8_sil=64000:random_seed=1850338552:i=20139:bs=on_2942 on theBenchmark for (2942ds/20139Mi) % 155.39/22.37 % (3016480)Instruction limit reached! % 155.39/22.37 % (3016480)------------------------------ % 155.39/22.37 % (3016480)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 155.39/22.37 % (3016480)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 155.39/22.37 % (3016480)CaDiCaL version: 2.1.3 % 155.39/22.37 % (3016480)Termination reason: Instruction limit % 155.39/22.37 % (3016480)Termination phase: Saturation % 155.39/22.37 % (3016480)Time elapsed: 2.800 s % 155.39/22.37 % (3016480)Peak memory usage: 47 MB % 155.39/22.37 % (3016480)Instructions burned: 8174 (million) % 155.39/22.37 % (3016487)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=3218495537:fmbsr=2:i=32576_2938 on theBenchmark for (2938ds/32576Mi) % 155.39/22.37 % (3016487)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 155.39/22.37 % (3016487)Terminated due to inappropriate strategy. % 155.39/22.37 % (3016487)------------------------------ % 155.39/22.37 % (3016487)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 155.39/22.37 % (3016487)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 155.39/22.37 % (3016487)CaDiCaL version: 2.1.3 % 155.39/22.37 % (3016487)Termination reason: Inappropriate % 155.39/22.37 % (3016487)Time elapsed: 0.0000 s % 155.39/22.37 % (3016487)Peak memory usage: 10 MB % 155.39/22.37 % (3016487)------------------------------ % 155.39/22.37 % (3016487)------------------------------ % 155.39/22.37 % (3016489)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=1196376206:i=11404_2938 on theBenchmark for (2938ds/11404Mi) % 155.39/22.37 % (3016483)Instruction limit reached! % 155.39/22.37 % (3016483)------------------------------ % 155.39/22.37 % (3016483)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 155.39/22.37 % (3016483)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 155.39/22.37 % (3016483)CaDiCaL version: 2.1.3 % 155.39/22.37 % (3016483)Termination reason: Instruction limit % 155.39/22.37 % (3016483)Termination phase: Saturation % 155.39/22.37 % (3016483)Time elapsed: 4.766 s % 155.39/22.37 % (3016483)Peak memory usage: 49 MB % 155.39/22.37 % (3016483)Instructions burned: 9156 (million) % 155.39/22.37 % (3016491)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=3635932191:i=14134_2912 on theBenchmark for (2912ds/14134Mi) % 155.39/22.37 % (3016489)Instruction limit reached! % 155.39/22.37 % (3016489)------------------------------ % 155.39/22.37 % (3016489)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 155.39/22.37 % (3016489)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 155.39/22.37 % (3016489)CaDiCaL version: 2.1.3 % 155.39/22.37 % (3016489)Termination reason: Instruction limit % 155.39/22.37 % (3016489)Termination phase: Saturation % 155.39/22.37 % (3016489)Time elapsed: 4.021 s % 155.39/22.37 % (3016489)Peak memory usage: 43 MB % 155.39/22.37 % (3016489)Instructions burned: 11409 (million) % 155.39/22.37 % (3016493)dis+33_16_sil=32000:sac=on:random_seed=735804679:i=15851:nm=0_2897 on theBenchmark for (2897ds/15851Mi) % 155.39/22.37 % (3016478)Instruction limit reached! % 155.39/22.37 % (3016478)------------------------------ % 155.39/22.37 % (3016478)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 155.39/22.37 % (3016478)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 155.39/22.37 % (3016478)CaDiCaL version: 2.1.3 % 155.39/22.37 % (3016478)Termination reason: Instruction limit % 155.39/22.37 % (3016478)Termination phase: Saturation % 155.39/22.37 % (3016478)Time elapsed: 9.820 s % 155.39/22.37 % (3016478)Peak memory usage: 275 MB % 155.39/22.37 % (3016478)Instructions burned: 22566 (million) % 155.39/22.37 % (3016495)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=2621498206:avsq=on:i=17627:add=on:amm=off_2869 on theBenchmark for (2869ds/17627Mi) % 155.39/22.37 % (3016493)Instruction limit reached! % 155.39/22.37 % (3016493)------------------------------ % 162.35/23.36 % (3016493)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 162.35/23.36 % (3016493)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 162.35/23.36 % (3016493)CaDiCaL version: 2.1.3 % 162.35/23.36 % (3016493)Termination reason: Instruction limit % 162.35/23.36 % (3016493)Termination phase: Saturation % 162.35/23.36 % (3016493)Time elapsed: 3.576 s % 162.35/23.36 % (3016493)Peak memory usage: 25 MB % 162.35/23.36 % (3016493)Instructions burned: 15853 (million) % 162.35/23.36 % (3016497)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=3590240557:s2a=on:i=53295_2862 on theBenchmark for (2862ds/53295Mi) % 162.35/23.36 % (3016468)Instruction limit reached! % 162.35/23.36 % (3016468)------------------------------ % 162.35/23.36 % (3016468)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 162.35/23.36 % (3016468)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 162.35/23.36 % (3016468)CaDiCaL version: 2.1.3 % 162.35/23.36 % (3016468)Termination reason: Instruction limit % 162.35/23.36 % (3016468)Termination phase: Saturation % 162.35/23.36 % (3016468)Time elapsed: 13.379 s % 162.35/23.36 % (3016468)Peak memory usage: 325 MB % 162.35/23.36 % (3016468)Instructions burned: 29341 (million) % 162.35/23.36 % (3016499)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=3291738607:i=26857:ins=20_2841 on theBenchmark for (2841ds/26857Mi) % 162.35/23.36 % (3016499)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 162.35/23.36 % (3016499)Terminated due to inappropriate strategy. % 162.35/23.36 % (3016499)------------------------------ % 162.35/23.36 % (3016499)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 162.35/23.36 % (3016499)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 162.35/23.36 % (3016499)CaDiCaL version: 2.1.3 % 162.35/23.36 % (3016499)Termination reason: Inappropriate % 162.35/23.36 % (3016499)Time elapsed: 0.0000 s % 162.35/23.36 % (3016499)Peak memory usage: 10 MB % 162.35/23.36 % (3016499)------------------------------ % 162.35/23.36 % (3016499)------------------------------ % 162.35/23.36 % (3016501)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=869014269:i=28120:bs=on:fsr=off_2841 on theBenchmark for (2841ds/28120Mi) % 162.35/23.36 % (3016491)Instruction limit reached! % 162.35/23.36 % (3016491)------------------------------ % 162.35/23.36 % (3016491)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 162.35/23.36 % (3016491)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 162.35/23.36 % (3016491)CaDiCaL version: 2.1.3 % 162.35/23.36 % (3016491)Termination reason: Instruction limit % 162.35/23.36 % (3016491)Termination phase: Saturation % 162.35/23.36 % (3016491)Time elapsed: 8.969 s % 162.35/23.36 % (3016491)Peak memory usage: 55 MB % 162.35/23.36 % (3016491)Instructions burned: 14135 (million) % 162.35/23.36 % (3016503)fmb+10_1_sil=256000:fmbss=7:random_seed=3659895621:fmbsr=1.6:i=182295_2822 on theBenchmark for (2822ds/182295Mi) % 162.35/23.36 % (3016503)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 162.35/23.36 % (3016503)Terminated due to inappropriate strategy. % 162.35/23.36 % (3016503)------------------------------ % 162.35/23.36 % (3016503)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 162.35/23.36 % (3016503)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 162.35/23.36 % (3016503)CaDiCaL version: 2.1.3 % 162.35/23.36 % (3016503)Termination reason: Inappropriate % 162.35/23.36 % (3016503)Time elapsed: 0.0000 s % 162.35/23.36 % (3016503)Peak memory usage: 10 MB % 162.35/23.36 % (3016503)------------------------------ % 162.35/23.36 % (3016503)------------------------------ % 162.35/23.36 % (3016505)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=1121741176:i=44625:gsp=on_2822 on theBenchmark for (2822ds/44625Mi) % 162.35/23.36 % (3016505)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 162.35/23.36 % (3016505)Terminated due to inappropriate strategy. % 162.35/23.36 % (3016505)------------------------------ % 162.35/23.36 % (3016505)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 162.35/23.36 % (3016505)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 162.35/23.36 % (3016505)CaDiCaL version: 2.1.3 % 162.35/23.36 % (3016505)Termination reason: Inappropriate % 162.35/23.36 % (3016505)Time elapsed: 0.0000 s % 162.35/23.36 % (3016505)Peak memory usage: 10 MB % 162.35/23.36 % (3016505)------------------------------ % 162.35/23.36 % (3016505)------------------------------ % 162.35/23.36 % (3016507)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=1917590507:i=160505_2822 on theBenchmark for (2822ds/160505Mi) % 185.91/26.66 % (3016507)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 185.91/26.66 % (3016507)Terminated due to inappropriate strategy. % 185.91/26.66 % (3016507)------------------------------ % 185.91/26.66 % (3016507)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 185.91/26.66 % (3016507)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 185.91/26.66 % (3016507)CaDiCaL version: 2.1.3 % 185.91/26.66 % (3016507)Termination reason: Inappropriate % 185.91/26.66 % (3016507)Time elapsed: 0.0000 s % 185.91/26.66 % (3016507)Peak memory usage: 10 MB % 185.91/26.66 % (3016507)------------------------------ % 185.91/26.66 % (3016507)------------------------------ % 185.91/26.66 % (3016509)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=3999946276:fmbsr=1.3:i=225729_2822 on theBenchmark for (2822ds/225729Mi) % 185.91/26.66 % (3016509)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 185.91/26.66 % (3016509)Terminated due to inappropriate strategy. % 185.91/26.66 % (3016509)------------------------------ % 185.91/26.66 % (3016509)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 185.91/26.66 % (3016509)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 185.91/26.66 % (3016509)CaDiCaL version: 2.1.3 % 185.91/26.66 % (3016509)Termination reason: Inappropriate % 185.91/26.66 % (3016509)Time elapsed: 0.0000 s % 185.91/26.66 % (3016509)Peak memory usage: 10 MB % 185.91/26.66 % (3016509)------------------------------ % 185.91/26.66 % (3016509)------------------------------ % 185.91/26.66 % (3016511)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=4103834900:fmbsr=2:i=185024:ins=7_2821 on theBenchmark for (2821ds/185024Mi) % 185.91/26.66 % (3016511)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 185.91/26.66 % (3016511)Terminated due to inappropriate strategy. % 185.91/26.66 % (3016511)------------------------------ % 185.91/26.66 % (3016511)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 185.91/26.66 % (3016511)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 185.91/26.66 % (3016511)CaDiCaL version: 2.1.3 % 185.91/26.66 % (3016511)Termination reason: Inappropriate % 185.91/26.66 % (3016511)Time elapsed: 0.0000 s % 185.91/26.66 % (3016511)Peak memory usage: 10 MB % 185.91/26.66 % (3016511)------------------------------ % 185.91/26.66 % (3016511)------------------------------ % 185.91/26.66 % (3016513)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=3416736121:rtra=on_2821 on theBenchmark for (2821ds/0Mi) % 185.91/26.66 % (3016513)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 185.91/26.66 % (3016513)Terminated due to inappropriate strategy. % 185.91/26.66 % (3016513)------------------------------ % 185.91/26.66 % (3016513)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 185.91/26.66 % (3016513)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 185.91/26.66 % (3016513)CaDiCaL version: 2.1.3 % 185.91/26.66 % (3016513)Termination reason: Inappropriate % 185.91/26.66 % (3016513)Time elapsed: 0.0000 s % 185.91/26.66 % (3016513)Peak memory usage: 10 MB % 185.91/26.66 % (3016513)------------------------------ % 185.91/26.66 % (3016513)------------------------------ % 185.91/26.66 % (3016515)% WARNING: option uhcvi not known. % 185.91/26.66 % (3016515)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1423623682:i=271062:add=off:rtra=on:rawr=on_2821 on theBenchmark for (2821ds/271062Mi) % 185.91/26.66 % (3016485)Instruction limit reached! % 185.91/26.66 % (3016485)------------------------------ % 185.91/26.66 % (3016485)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 185.91/26.66 % (3016485)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 185.91/26.66 % (3016485)CaDiCaL version: 2.1.3 % 185.91/26.66 % (3016485)Termination reason: Instruction limit % 185.91/26.66 % (3016485)Termination phase: Saturation % 185.91/26.66 % (3016485)Time elapsed: 12.683 s % 185.91/26.66 % (3016485)Peak memory usage: 67 MB % 185.91/26.66 % (3016485)Instructions burned: 20140 (million) % 185.91/26.66 % (3016517)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1069879313:i=176048:add=on:rtra=on:rawr=on_2815 on theBenchmark for (2815ds/176048Mi) % 185.91/26.66 % (3016495)Instruction limit reached! % 185.91/26.66 % (3016495)------------------------------ % 185.91/26.66 % (3016495)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 192.04/27.56 % (3016495)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 192.04/27.56 % (3016495)CaDiCaL version: 2.1.3 % 192.04/27.56 % (3016495)Termination reason: Instruction limit % 192.04/27.56 % (3016495)Termination phase: Saturation % 192.04/27.56 % (3016495)Time elapsed: 8.935 s % 192.04/27.56 % (3016495)Peak memory usage: 185 MB % 192.04/27.56 % (3016495)Instructions burned: 17629 (million) % 192.04/27.56 % (3016519)dis+10_1_sil=32000:si=on:sp=arity:random_seed=322336553:i=206:fgj=on:rtra=on_2780 on theBenchmark for (2780ds/206Mi) % 192.04/27.56 % (3016519)Instruction limit reached! % 192.04/27.56 % (3016519)------------------------------ % 192.04/27.56 % (3016519)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 192.04/27.56 % (3016519)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 192.04/27.56 % (3016519)CaDiCaL version: 2.1.3 % 192.04/27.56 % (3016519)Termination reason: Instruction limit % 192.04/27.56 % (3016519)Termination phase: Saturation % 192.04/27.56 % (3016519)Time elapsed: 0.128 s % 192.04/27.56 % (3016519)Peak memory usage: 13 MB % 192.04/27.56 % (3016519)Instructions burned: 207 (million) % 192.04/27.56 % (3016521)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=2551009856:i=232:rtra=on_2778 on theBenchmark for (2778ds/232Mi) % 192.04/27.56 % (3016521)Instruction limit reached! % 192.04/27.56 % (3016521)------------------------------ % 192.04/27.56 % (3016521)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 192.04/27.56 % (3016521)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 192.04/27.56 % (3016521)CaDiCaL version: 2.1.3 % 192.04/27.56 % (3016521)Termination reason: Instruction limit % 192.04/27.56 % (3016521)Termination phase: Saturation % 192.04/27.56 % (3016521)Time elapsed: 0.145 s % 192.04/27.56 % (3016521)Peak memory usage: 13 MB % 192.04/27.56 % (3016521)Instructions burned: 233 (million) % 192.04/27.56 % (3016523)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=2668255512:i=262:rtra=on_2776 on theBenchmark for (2776ds/262Mi) % 192.04/27.56 % (3016523)Instruction limit reached! % 192.04/27.56 % (3016523)------------------------------ % 192.04/27.56 % (3016523)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 192.04/27.56 % (3016523)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 192.04/27.56 % (3016523)CaDiCaL version: 2.1.3 % 192.04/27.56 % (3016523)Termination reason: Instruction limit % 192.04/27.56 % (3016523)Termination phase: Saturation % 192.04/27.56 % (3016523)Time elapsed: 0.165 s % 192.04/27.56 % (3016523)Peak memory usage: 13 MB % 192.04/27.56 % (3016523)Instructions burned: 263 (million) % 192.04/27.56 % (3016525)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=2098855705:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2775 on theBenchmark for (2775ds/318Mi) % 192.04/27.56 % (3016525)Instruction limit reached! % 192.04/27.56 % (3016525)------------------------------ % 192.04/27.56 % (3016525)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 192.04/27.56 % (3016525)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 192.04/27.56 % (3016525)CaDiCaL version: 2.1.3 % 192.04/27.56 % (3016525)Termination reason: Instruction limit % 192.04/27.56 % (3016525)Termination phase: Saturation % 192.04/27.56 % (3016525)Time elapsed: 0.224 s % 192.04/27.56 % (3016525)Peak memory usage: 14 MB % 192.04/27.56 % (3016525)Instructions burned: 319 (million) % 192.04/27.56 % (3016527)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=2318180181:i=1428:nm=2:rtra=on_2772 on theBenchmark for (2772ds/1428Mi) % 192.04/27.56 % (3016527)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 192.04/27.56 % (3016527)Terminated due to inappropriate strategy. % 192.04/27.56 % (3016527)------------------------------ % 192.04/27.56 % (3016527)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 192.04/27.56 % (3016527)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 192.04/27.56 % (3016527)CaDiCaL version: 2.1.3 % 192.04/27.56 % (3016527)Termination reason: Inappropriate % 192.04/27.56 % (3016527)Time elapsed: 0.0000 s % 192.04/27.56 % (3016527)Peak memory usage: 10 MB % 192.04/27.56 % (3016527)------------------------------ % 192.04/27.56 % (3016527)------------------------------ % 192.04/27.56 % (3016529)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=988457452:i=262:bd=preordered:rtra=on:fsd=on_2772 on theBenchmark for (2772ds/262Mi) % 192.04/27.56 % (3016529)Instruction limit reached! % 192.04/27.56 % (3016529)------------------------------ % 192.04/27.56 % (3016529)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 203.19/29.05 % (3016529)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 203.19/29.05 % (3016529)CaDiCaL version: 2.1.3 % 203.19/29.05 % (3016529)Termination reason: Instruction limit % 203.19/29.05 % (3016529)Termination phase: Saturation % 203.19/29.05 % (3016529)Time elapsed: 0.178 s % 203.19/29.05 % (3016529)Peak memory usage: 13 MB % 203.19/29.05 % (3016529)Instructions burned: 263 (million) % 203.19/29.05 % (3016531)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=3162568744:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2770 on theBenchmark for (2770ds/1368Mi) % 203.19/29.05 % (3016531)Instruction limit reached! % 203.19/29.05 % (3016531)------------------------------ % 203.19/29.05 % (3016531)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 203.19/29.05 % (3016531)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 203.19/29.05 % (3016531)CaDiCaL version: 2.1.3 % 203.19/29.05 % (3016531)Termination reason: Instruction limit % 203.19/29.05 % (3016531)Termination phase: Saturation % 203.19/29.05 % (3016531)Time elapsed: 0.791 s % 203.19/29.05 % (3016531)Peak memory usage: 19 MB % 203.19/29.05 % (3016531)Instructions burned: 1368 (million) % 203.19/29.05 % (3016533)ott-21_1_sil=16000:si=on:fs=off:random_seed=4059312757:i=360:av=off:fsr=off:rtra=on_2762 on theBenchmark for (2762ds/360Mi) % 203.19/29.05 % (3016533)Instruction limit reached! % 203.19/29.05 % (3016533)------------------------------ % 203.19/29.05 % (3016533)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 203.19/29.05 % (3016533)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 203.19/29.05 % (3016533)CaDiCaL version: 2.1.3 % 203.19/29.05 % (3016533)Termination reason: Instruction limit % 203.19/29.05 % (3016533)Termination phase: Saturation % 203.19/29.05 % (3016533)Time elapsed: 0.156 s % 203.19/29.05 % (3016533)Peak memory usage: 12 MB % 203.19/29.05 % (3016533)Instructions burned: 361 (million) % 203.19/29.05 % (3016535)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=243851857:i=954:bd=all:rtra=on_2760 on theBenchmark for (2760ds/954Mi) % 203.19/29.05 % (3016535)Instruction limit reached! % 203.19/29.05 % (3016535)------------------------------ % 203.19/29.05 % (3016535)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 203.19/29.05 % (3016535)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 203.19/29.05 % (3016535)CaDiCaL version: 2.1.3 % 203.19/29.05 % (3016535)Termination reason: Instruction limit % 203.19/29.05 % (3016535)Termination phase: Saturation % 203.19/29.05 % (3016535)Time elapsed: 0.626 s % 203.19/29.05 % (3016535)Peak memory usage: 17 MB % 203.19/29.05 % (3016535)Instructions burned: 954 (million) % 203.19/29.05 % (3016537)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=3893692601:fmbsr=1.3:i=1730:ins=25:rtra=on_2754 on theBenchmark for (2754ds/1730Mi) % 203.19/29.05 % (3016537)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 203.19/29.05 % (3016537)Terminated due to inappropriate strategy. % 203.19/29.05 % (3016537)------------------------------ % 203.19/29.05 % (3016537)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 203.19/29.05 % (3016537)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 203.19/29.05 % (3016537)CaDiCaL version: 2.1.3 % 203.19/29.05 % (3016537)Termination reason: Inappropriate % 203.19/29.05 % (3016537)Time elapsed: 0.0000 s % 203.19/29.05 % (3016537)Peak memory usage: 10 MB % 203.19/29.05 % (3016537)------------------------------ % 203.19/29.05 % (3016537)------------------------------ % 203.19/29.05 % (3016539)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=2533610974:i=2358:rtra=on_2753 on theBenchmark for (2753ds/2358Mi) % 203.19/29.05 % (3016539)Instruction limit reached! % 203.19/29.05 % (3016539)------------------------------ % 203.19/29.05 % (3016539)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 203.19/29.05 % (3016539)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 203.19/29.05 % (3016539)CaDiCaL version: 2.1.3 % 203.19/29.05 % (3016539)Termination reason: Instruction limit % 203.19/29.05 % (3016539)Termination phase: Saturation % 203.19/29.05 % (3016539)Time elapsed: 1.609 s % 203.19/29.05 % (3016539)Peak memory usage: 22 MB % 203.19/29.05 % (3016539)Instructions burned: 2360 (million) % 203.19/29.05 % (3016541)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=3036208069:i=1778:ins=1:rtra=on_2737 on theBenchmark for (2737ds/1778Mi) % 203.19/29.05 % (3016541)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 233.88/33.47 % (3016541)Terminated due to inappropriate strategy. % 233.88/33.47 % (3016541)------------------------------ % 233.88/33.47 % (3016541)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 233.88/33.47 % (3016541)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 233.88/33.47 % (3016541)CaDiCaL version: 2.1.3 % 233.88/33.47 % (3016541)Termination reason: Inappropriate % 233.88/33.47 % (3016541)Time elapsed: 0.0000 s % 233.88/33.47 % (3016541)Peak memory usage: 10 MB % 233.88/33.47 % (3016541)------------------------------ % 233.88/33.47 % (3016541)------------------------------ % 233.88/33.47 % (3016543)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=553441812:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2737 on theBenchmark for (2737ds/1384Mi) % 233.88/33.47 % (3016497)Instruction limit reached! % 233.88/33.47 % (3016497)------------------------------ % 233.88/33.47 % (3016497)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 233.88/33.47 % (3016497)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 233.88/33.47 % (3016497)CaDiCaL version: 2.1.3 % 233.88/33.47 % (3016497)Termination reason: Instruction limit % 233.88/33.47 % (3016497)Termination phase: Saturation % 233.88/33.47 % (3016497)Time elapsed: 13.040 s % 233.88/33.47 % (3016497)Peak memory usage: 322 MB % 233.88/33.47 % (3016497)Instructions burned: 53295 (million) % 233.88/33.47 % (3016545)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=2244490605:i=1758:kws=inv_precedence:fsr=off:rtra=on_2731 on theBenchmark for (2731ds/1758Mi) % 233.88/33.47 % (3016543)Instruction limit reached! % 233.88/33.47 % (3016543)------------------------------ % 233.88/33.47 % (3016543)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 233.88/33.47 % (3016543)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 233.88/33.47 % (3016543)CaDiCaL version: 2.1.3 % 233.88/33.47 % (3016543)Termination reason: Instruction limit % 233.88/33.47 % (3016543)Termination phase: Saturation % 233.88/33.47 % (3016543)Time elapsed: 0.814 s % 233.88/33.47 % (3016543)Peak memory usage: 19 MB % 233.88/33.47 % (3016543)Instructions burned: 1387 (million) % 233.88/33.47 % (3016547)fmb+10_1_sil=64000:si=on:random_seed=3147502658:i=44122:nm=2:rtra=on:gsp=on_2729 on theBenchmark for (2729ds/44122Mi) % 233.88/33.47 % (3016547)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 233.88/33.47 % (3016547)Terminated due to inappropriate strategy. % 233.88/33.47 % (3016547)------------------------------ % 233.88/33.47 % (3016547)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 233.88/33.47 % (3016547)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 233.88/33.47 % (3016547)CaDiCaL version: 2.1.3 % 233.88/33.47 % (3016547)Termination reason: Inappropriate % 233.88/33.47 % (3016547)Time elapsed: 0.0000 s % 233.88/33.47 % (3016547)Peak memory usage: 10 MB % 233.88/33.47 % (3016547)------------------------------ % 233.88/33.47 % (3016547)------------------------------ % 233.88/33.47 % (3016549)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=1024004974:i=19030:nm=5:rtra=on_2728 on theBenchmark for (2728ds/19030Mi) % 233.88/33.47 % (3016549)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 233.88/33.47 % (3016549)Terminated due to inappropriate strategy. % 233.88/33.47 % (3016549)------------------------------ % 233.88/33.47 % (3016549)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 233.88/33.47 % (3016549)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 233.88/33.47 % (3016549)CaDiCaL version: 2.1.3 % 233.88/33.47 % (3016549)Termination reason: Inappropriate % 233.88/33.47 % (3016549)Time elapsed: 0.0000 s % 233.88/33.47 % (3016549)Peak memory usage: 10 MB % 233.88/33.47 % (3016549)------------------------------ % 233.88/33.47 % (3016549)------------------------------ % 233.88/33.47 % (3016551)fmb+10_1_sil=64000:sas=cadical:si=on:fmbss=8:random_seed=1182403398:fmbsr=1.7:i=1840:rtra=on_2728 on theBenchmark for (2728ds/1840Mi) % 233.88/33.47 % (3016551)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 233.88/33.47 % (3016551)Terminated due to inappropriate strategy. % 233.88/33.47 % (3016551)------------------------------ % 233.88/33.47 % (3016551)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 233.88/33.47 % (3016551)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 264.68/37.74 % (3016551)CaDiCaL version: 2.1.3 % 264.68/37.74 % (3016551)Termination reason: Inappropriate % 264.68/37.74 % (3016551)Time elapsed: 0.0000 s % 264.68/37.74 % (3016551)Peak memory usage: 10 MB % 264.68/37.74 % (3016551)------------------------------ % 264.68/37.74 % (3016551)------------------------------ % 264.68/37.74 % (3016553)dis-4_1_sil=16000:drc=ordering:si=on:sp=const_frequency:sac=on:newcnf=on:random_seed=3866130071:i=10262:rtra=on_2728 on theBenchmark for (2728ds/10262Mi) % 264.68/37.74 % (3016545)Instruction limit reached! % 264.68/37.74 % (3016545)------------------------------ % 264.68/37.74 % (3016545)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 264.68/37.74 % (3016545)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 264.68/37.74 % (3016545)CaDiCaL version: 2.1.3 % 264.68/37.74 % (3016545)Termination reason: Instruction limit % 264.68/37.74 % (3016545)Termination phase: Saturation % 264.68/37.74 % (3016545)Time elapsed: 0.536 s % 264.68/37.74 % (3016545)Peak memory usage: 29 MB % 264.68/37.74 % (3016545)Instructions burned: 1759 (million) % 264.68/37.74 % (3016555)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:si=on:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1670750628:i=2944:ins=7:rtra=on:fdi=8:gsp=on_2725 on theBenchmark for (2725ds/2944Mi) % 264.68/37.74 % (3016501)Instruction limit reached! % 264.68/37.74 % (3016501)------------------------------ % 264.68/37.74 % (3016501)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 264.68/37.74 % (3016501)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 264.68/37.74 % (3016501)CaDiCaL version: 2.1.3 % 264.68/37.74 % (3016501)Termination reason: Instruction limit % 264.68/37.74 % (3016501)Termination phase: Saturation % 264.68/37.74 % (3016501)Time elapsed: 11.546 s % 264.68/37.74 % (3016501)Peak memory usage: 26 MB % 264.68/37.74 % (3016501)Instructions burned: 28122 (million) % 264.68/37.74 % (3016557)fmb+10_1_sil=16000:sas=cadical:si=on:bce=on:fmbss=77:random_seed=259381881:i=12648:rtra=on_2725 on theBenchmark for (2725ds/12648Mi) % 264.68/37.74 % (3016557)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 264.68/37.74 % (3016557)Terminated due to inappropriate strategy. % 264.68/37.74 % (3016557)------------------------------ % 264.68/37.74 % (3016557)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 264.68/37.74 % (3016557)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 264.68/37.74 % (3016557)CaDiCaL version: 2.1.3 % 264.68/37.74 % (3016557)Termination reason: Inappropriate % 264.68/37.74 % (3016557)Time elapsed: 0.0000 s % 264.68/37.74 % (3016557)Peak memory usage: 10 MB % 264.68/37.74 % (3016557)------------------------------ % 264.68/37.74 % (3016557)------------------------------ % 264.68/37.74 % (3016559)fmb+10_1_fmbas=function:sil=32000:sas=cadical:si=on:fmbss=16:random_seed=916363663:fmbsr=2.30978:i=4348:rtra=on_2725 on theBenchmark for (2725ds/4348Mi) % 264.68/37.74 % (3016559)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 264.68/37.74 % (3016559)Terminated due to inappropriate strategy. % 264.68/37.74 % (3016559)------------------------------ % 264.68/37.74 % (3016559)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 264.68/37.74 % (3016559)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 264.68/37.74 % (3016559)CaDiCaL version: 2.1.3 % 264.68/37.74 % (3016559)Termination reason: Inappropriate % 264.68/37.74 % (3016559)Time elapsed: 0.0000 s % 264.68/37.74 % (3016559)Peak memory usage: 10 MB % 264.68/37.74 % (3016559)------------------------------ % 264.68/37.74 % (3016559)------------------------------ % 264.68/37.74 % (3016561)ott-2_1_sil=16000:si=on:newcnf=on:random_seed=2305004017:avsq=on:i=1738:avsqr=1,16:kws=inv_arity_squared:rtra=on_2725 on theBenchmark for (2725ds/1738Mi) % 264.68/37.74 % (3016555)Instruction limit reached! % 264.68/37.74 % (3016555)------------------------------ % 264.68/37.74 % (3016555)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 264.68/37.74 % (3016555)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 264.68/37.74 % (3016555)CaDiCaL version: 2.1.3 % 264.68/37.74 % (3016555)Termination reason: Instruction limit % 264.68/37.74 % (3016555)Termination phase: Saturation % 264.68/37.74 % (3016555)Time elapsed: 0.714 s % 264.68/37.74 % (3016555)Peak memory usage: 28 MB % 264.68/37.74 % (3016555)Instructions burned: 2945 (million) % 264.68/37.74 % (3016563)ott+10_1_sil=32000:tgt=ground:si=on:random_seed=1244883874:i=10228:av=off:rtra=on_2718 on theBenchmark for (2718ds/10228Mi) % 264.68/37.74 % (3016561)Terminated % 300.18/42.74 Terminated %------------------------------------------------------------------------------