%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWC439_1 : TPTP v9.3.1. Released v9.0.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % Computer : n008.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 29 01:06:00 PM UTC 2026 % Result : Timeout 300.11s 42.54s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWC439_1 : TPTP v9.3.1. Released v9.0.0. % 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.10/0.21 % Computer : n008.cluster.edu % 0.10/0.21 % Model : x86_64 x86_64 % 0.10/0.21 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.21 % Memory : 8046.5625MB % 0.10/0.21 % OS : Linux 6.8.0-71-generic % 0.10/0.21 % CPULimit : 300 % 0.10/0.21 % WCLimit : 300 % 0.10/0.21 % DateTime : Mon Sep 28 09:38:25 UTC 2026 % 0.10/0.22 % CPUTime : % 0.10/0.22 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.10/0.25 Running first-order model finding % 0.10/0.25 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 3.57/0.88 % (2127399)Will run a generic schedule for satisfiability detection. % 3.57/0.88 % (2127409)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2787549488:i=131_2999 on theBenchmark for (2999ds/131Mi) % 3.57/0.88 % (2127405)% WARNING: option uhcvi not known. % 3.57/0.88 % (2127407)dis+10_1_sil=32000:sp=arity:random_seed=3698086027:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 3.57/0.88 % (2127404)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1757161177_2999 on theBenchmark for (2999ds/0Mi) % 3.57/0.88 % (2127405)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=662340491:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 3.57/0.88 % (2127406)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2155110473:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 3.57/0.88 % (2127408)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=734600810:i=116_2999 on theBenchmark for (2999ds/116Mi) % 3.57/0.88 % (2127410)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1394566818:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 3.57/0.88 % (2127404)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.57/0.88 % (2127404)Terminated due to inappropriate strategy. % 3.57/0.88 % (2127404)------------------------------ % 3.57/0.88 % (2127404)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.57/0.88 % (2127404)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.57/0.88 % (2127404)CaDiCaL version: 2.1.3 % 3.57/0.88 % (2127404)Termination reason: Inappropriate % 3.57/0.88 % (2127404)Time elapsed: 0.001 s % 3.57/0.88 % (2127404)Peak memory usage: 10 MB % 3.57/0.88 % (2127404)Instructions burned: 2 (million) % 3.57/0.88 % (2127404)------------------------------ % 3.57/0.88 % (2127404)------------------------------ % 3.57/0.88 % (2127418)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=952579700:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 3.57/0.88 % (2127418)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.57/0.88 % (2127418)Terminated due to inappropriate strategy. % 3.57/0.88 % (2127418)------------------------------ % 3.57/0.88 % (2127418)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.57/0.88 % (2127418)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.57/0.88 % (2127418)CaDiCaL version: 2.1.3 % 3.57/0.88 % (2127418)Termination reason: Inappropriate % 3.57/0.88 % (2127418)Time elapsed: 0.001 s % 3.57/0.88 % (2127418)Peak memory usage: 10 MB % 3.57/0.88 % (2127418)Instructions burned: 2 (million) % 3.57/0.88 % (2127418)------------------------------ % 3.57/0.88 % (2127418)------------------------------ % 3.57/0.88 % (2127409)Instruction limit reached! % 3.57/0.88 % (2127409)------------------------------ % 3.57/0.88 % (2127409)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.57/0.88 % (2127409)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.57/0.88 % (2127409)CaDiCaL version: 2.1.3 % 3.57/0.88 % (2127409)Termination reason: Instruction limit % 3.57/0.88 % (2127409)Termination phase: Saturation % 3.57/0.88 % (2127409)Time elapsed: 0.044 s % 3.57/0.88 % (2127409)Peak memory usage: 13 MB % 3.57/0.88 % (2127409)Instructions burned: 132 (million) % 3.57/0.88 % (2127420)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1606502541:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 3.57/0.88 % (2127421)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=3719415961:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi) % 3.57/0.88 % (2127407)Instruction limit reached! % 3.57/0.88 % (2127407)------------------------------ % 3.57/0.88 % (2127407)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.57/0.88 % (2127407)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.57/0.88 % (2127407)CaDiCaL version: 2.1.3 % 3.57/0.88 % (2127407)Termination reason: Instruction limit % 3.57/0.88 % (2127407)Termination phase: Saturation % 3.57/0.88 % (2127407)Time elapsed: 0.065 s % 3.57/0.88 % (2127407)Peak memory usage: 13 MB % 3.57/0.88 % (2127407)Instructions burned: 104 (million) % 3.57/0.88 % (2127408)Instruction limit reached! % 3.57/0.88 % (2127408)------------------------------ % 3.57/0.88 % (2127408)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.54/1.12 % (2127408)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.54/1.12 % (2127408)CaDiCaL version: 2.1.3 % 5.54/1.12 % (2127408)Termination reason: Instruction limit % 5.54/1.12 % (2127408)Termination phase: Saturation % 5.54/1.12 % (2127408)Time elapsed: 0.072 s % 5.54/1.12 % (2127408)Peak memory usage: 12 MB % 5.54/1.12 % (2127408)Instructions burned: 117 (million) % 5.54/1.12 % (2127424)ott-21_1_sil=16000:fs=off:random_seed=177336451:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi) % 5.54/1.12 % (2127425)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3332234221:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 5.54/1.12 % (2127410)Instruction limit reached! % 5.54/1.12 % (2127410)------------------------------ % 5.54/1.12 % (2127410)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.54/1.12 % (2127410)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.54/1.12 % (2127410)CaDiCaL version: 2.1.3 % 5.54/1.12 % (2127410)Termination reason: Instruction limit % 5.54/1.12 % (2127410)Termination phase: Saturation % 5.54/1.12 % (2127410)Time elapsed: 0.103 s % 5.54/1.12 % (2127410)Peak memory usage: 13 MB % 5.54/1.12 % (2127410)Instructions burned: 160 (million) % 5.54/1.12 % (2127420)Instruction limit reached! % 5.54/1.12 % (2127420)------------------------------ % 5.54/1.12 % (2127420)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.54/1.12 % (2127420)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.54/1.12 % (2127420)CaDiCaL version: 2.1.3 % 5.54/1.12 % (2127420)Termination reason: Instruction limit % 5.54/1.12 % (2127420)Termination phase: Saturation % 5.54/1.12 % (2127420)Time elapsed: 0.079 s % 5.54/1.12 % (2127420)Peak memory usage: 12 MB % 5.54/1.12 % (2127420)Instructions burned: 132 (million) % 5.54/1.12 % (2127428)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=858125597:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 5.54/1.12 % (2127428)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 5.54/1.12 % (2127428)Terminated due to inappropriate strategy. % 5.54/1.12 % (2127428)------------------------------ % 5.54/1.12 % (2127428)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.54/1.12 % (2127428)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.54/1.12 % (2127428)CaDiCaL version: 2.1.3 % 5.54/1.12 % (2127428)Termination reason: Inappropriate % 5.54/1.12 % (2127428)Time elapsed: 0.001 s % 5.54/1.12 % (2127428)Peak memory usage: 10 MB % 5.54/1.12 % (2127428)Instructions burned: 2 (million) % 5.54/1.12 % (2127428)------------------------------ % 5.54/1.12 % (2127428)------------------------------ % 5.54/1.12 % (2127430)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3297493997:i=1179_2998 on theBenchmark for (2998ds/1179Mi) % 5.54/1.12 % (2127431)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=25717238:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi) % 5.54/1.12 % (2127431)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 5.54/1.12 % (2127431)Terminated due to inappropriate strategy. % 5.54/1.12 % (2127431)------------------------------ % 5.54/1.12 % (2127431)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.54/1.12 % (2127431)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.54/1.12 % (2127431)CaDiCaL version: 2.1.3 % 5.54/1.12 % (2127431)Termination reason: Inappropriate % 5.54/1.12 % (2127431)Time elapsed: 0.001 s % 5.54/1.12 % (2127431)Peak memory usage: 10 MB % 5.54/1.12 % (2127431)Instructions burned: 2 (million) % 5.54/1.12 % (2127431)------------------------------ % 5.54/1.12 % (2127431)------------------------------ % 5.54/1.12 % (2127424)Instruction limit reached! % 5.54/1.12 % (2127424)------------------------------ % 5.54/1.12 % (2127424)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.54/1.12 % (2127424)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.54/1.12 % (2127424)CaDiCaL version: 2.1.3 % 5.54/1.12 % (2127424)Termination reason: Instruction limit % 5.54/1.12 % (2127424)Termination phase: Saturation % 5.54/1.12 % (2127424)Time elapsed: 0.083 s % 5.54/1.12 % (2127424)Peak memory usage: 12 MB % 5.54/1.12 % (2127424)Instructions burned: 180 (million) % 5.54/1.12 % (2127434)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=804482660: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) % 17.37/2.81 % (2127436)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2490251584:i=879:kws=inv_precedence:fsr=off_2998 on theBenchmark for (2998ds/879Mi) % 17.37/2.81 % (2127421)Instruction limit reached! % 17.37/2.81 % (2127421)------------------------------ % 17.37/2.81 % (2127421)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 17.37/2.81 % (2127421)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.37/2.81 % (2127421)CaDiCaL version: 2.1.3 % 17.37/2.81 % (2127421)Termination reason: Instruction limit % 17.37/2.81 % (2127421)Termination phase: Saturation % 17.37/2.81 % (2127421)Time elapsed: 0.204 s % 17.37/2.81 % (2127421)Peak memory usage: 16 MB % 17.37/2.81 % (2127421)Instructions burned: 685 (million) % 17.37/2.81 % (2127438)fmb+10_1_sil=64000:random_seed=1707724622:i=22061:nm=2:gsp=on_2997 on theBenchmark for (2997ds/22061Mi) % 17.37/2.81 % (2127438)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 17.37/2.81 % (2127438)Terminated due to inappropriate strategy. % 17.37/2.81 % (2127438)------------------------------ % 17.37/2.81 % (2127438)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 17.37/2.81 % (2127438)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.37/2.81 % (2127438)CaDiCaL version: 2.1.3 % 17.37/2.81 % (2127438)Termination reason: Inappropriate % 17.37/2.81 % (2127438)Time elapsed: 0.0000 s % 17.37/2.81 % (2127438)Peak memory usage: 11 MB % 17.37/2.81 % (2127438)Instructions burned: 2 (million) % 17.37/2.81 % (2127438)------------------------------ % 17.37/2.81 % (2127438)------------------------------ % 17.37/2.81 % (2127440)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3317565713:i=9515:nm=5_2997 on theBenchmark for (2997ds/9515Mi) % 17.37/2.81 % (2127440)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 17.37/2.81 % (2127440)Terminated due to inappropriate strategy. % 17.37/2.81 % (2127440)------------------------------ % 17.37/2.81 % (2127440)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 17.37/2.81 % (2127440)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.37/2.81 % (2127440)CaDiCaL version: 2.1.3 % 17.37/2.81 % (2127440)Termination reason: Inappropriate % 17.37/2.81 % (2127440)Time elapsed: 0.0000 s % 17.37/2.81 % (2127440)Peak memory usage: 11 MB % 17.37/2.81 % (2127440)Instructions burned: 2 (million) % 17.37/2.81 % (2127440)------------------------------ % 17.37/2.81 % (2127440)------------------------------ % 17.37/2.81 % (2127442)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=4102348583:fmbsr=1.7:i=920_2996 on theBenchmark for (2996ds/920Mi) % 17.37/2.81 % (2127442)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 17.37/2.81 % (2127442)Terminated due to inappropriate strategy. % 17.37/2.81 % (2127442)------------------------------ % 17.37/2.81 % (2127442)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 17.37/2.81 % (2127442)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.37/2.81 % (2127442)CaDiCaL version: 2.1.3 % 17.37/2.81 % (2127442)Termination reason: Inappropriate % 17.37/2.81 % (2127442)Time elapsed: 0.001 s % 17.37/2.81 % (2127442)Peak memory usage: 10 MB % 17.37/2.81 % (2127442)Instructions burned: 2 (million) % 17.37/2.81 % (2127442)------------------------------ % 17.37/2.81 % (2127442)------------------------------ % 17.37/2.81 % (2127444)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1208796266:i=5131_2996 on theBenchmark for (2996ds/5131Mi) % 17.37/2.81 % (2127425)Instruction limit reached! % 17.37/2.81 % (2127425)------------------------------ % 17.37/2.81 % (2127425)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 17.37/2.81 % (2127425)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.37/2.81 % (2127425)CaDiCaL version: 2.1.3 % 17.37/2.81 % (2127425)Termination reason: Instruction limit % 17.37/2.81 % (2127425)Termination phase: Saturation % 17.37/2.81 % (2127425)Time elapsed: 0.313 s % 17.37/2.81 % (2127425)Peak memory usage: 14 MB % 17.37/2.81 % (2127425)Instructions burned: 478 (million) % 17.37/2.81 % (2127446)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3001206607:i=1472:ins=7:fdi=8:gsp=on_2995 on theBenchmark for (2995ds/1472Mi) % 17.37/2.81 % (2127434)Instruction limit reached! % 17.37/2.81 % (2127434)------------------------------ % 27.55/4.17 % (2127434)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 27.55/4.17 % (2127434)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.55/4.17 % (2127434)CaDiCaL version: 2.1.3 % 27.55/4.17 % (2127434)Termination reason: Instruction limit % 27.55/4.17 % (2127434)Termination phase: Saturation % 27.55/4.17 % (2127434)Time elapsed: 0.424 s % 27.55/4.17 % (2127434)Peak memory usage: 17 MB % 27.55/4.17 % (2127434)Instructions burned: 693 (million) % 27.55/4.17 % (2127448)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=4289959873:i=6324_2993 on theBenchmark for (2993ds/6324Mi) % 27.55/4.17 % (2127448)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 27.55/4.17 % (2127448)Terminated due to inappropriate strategy. % 27.55/4.17 % (2127448)------------------------------ % 27.55/4.17 % (2127448)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 27.55/4.17 % (2127448)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.55/4.17 % (2127448)CaDiCaL version: 2.1.3 % 27.55/4.17 % (2127448)Termination reason: Inappropriate % 27.55/4.17 % (2127448)Time elapsed: 0.001 s % 27.55/4.17 % (2127448)Peak memory usage: 10 MB % 27.55/4.17 % (2127448)Instructions burned: 2 (million) % 27.55/4.17 % (2127448)------------------------------ % 27.55/4.17 % (2127448)------------------------------ % 27.55/4.17 % (2127450)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=3565571523:fmbsr=2.30978:i=2174_2993 on theBenchmark for (2993ds/2174Mi) % 27.55/4.17 % (2127450)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 27.55/4.17 % (2127450)Terminated due to inappropriate strategy. % 27.55/4.17 % (2127450)------------------------------ % 27.55/4.17 % (2127450)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 27.55/4.17 % (2127450)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.55/4.17 % (2127450)CaDiCaL version: 2.1.3 % 27.55/4.17 % (2127450)Termination reason: Inappropriate % 27.55/4.17 % (2127450)Time elapsed: 0.001 s % 27.55/4.17 % (2127450)Peak memory usage: 10 MB % 27.55/4.17 % (2127450)Instructions burned: 2 (million) % 27.55/4.17 % (2127450)------------------------------ % 27.55/4.17 % (2127450)------------------------------ % 27.55/4.17 % (2127452)ott-2_1_sil=16000:newcnf=on:random_seed=3030256459:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2993 on theBenchmark for (2993ds/869Mi) % 27.55/4.17 % (2127436)Instruction limit reached! % 27.55/4.17 % (2127436)------------------------------ % 27.55/4.17 % (2127436)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 27.55/4.17 % (2127436)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.55/4.17 % (2127436)CaDiCaL version: 2.1.3 % 27.55/4.17 % (2127436)Termination reason: Instruction limit % 27.55/4.17 % (2127436)Termination phase: Saturation % 27.55/4.17 % (2127436)Time elapsed: 0.497 s % 27.55/4.17 % (2127436)Peak memory usage: 18 MB % 27.55/4.17 % (2127436)Instructions burned: 880 (million) % 27.55/4.17 % (2127454)ott+10_1_sil=32000:tgt=ground:random_seed=199648169:i=5114:av=off_2992 on theBenchmark for (2992ds/5114Mi) % 27.55/4.17 % (2127430)Instruction limit reached! % 27.55/4.17 % (2127430)------------------------------ % 27.55/4.17 % (2127430)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 27.55/4.17 % (2127430)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.55/4.17 % (2127430)CaDiCaL version: 2.1.3 % 27.55/4.17 % (2127430)Termination reason: Instruction limit % 27.55/4.17 % (2127430)Termination phase: Saturation % 27.55/4.17 % (2127430)Time elapsed: 0.671 s % 27.55/4.17 % (2127430)Peak memory usage: 20 MB % 27.55/4.17 % (2127430)Instructions burned: 1180 (million) % 27.55/4.17 % (2127456)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=1377406284:i=54282_2991 on theBenchmark for (2991ds/54282Mi) % 27.55/4.17 % (2127456)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 27.55/4.17 % (2127456)Terminated due to inappropriate strategy. % 27.55/4.17 % (2127456)------------------------------ % 27.55/4.17 % (2127456)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 27.55/4.17 % (2127456)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.55/4.17 % (2127456)CaDiCaL version: 2.1.3 % 27.55/4.17 % (2127456)Termination reason: Inappropriate % 27.55/4.17 % (2127456)Time elapsed: 0.001 s % 27.55/4.17 % (2127456)Peak memory usage: 10 MB % 27.55/4.17 % (2127456)Instructions burned: 2 (million) % 84.77/12.23 % (2127456)------------------------------ % 84.77/12.23 % (2127456)------------------------------ % 84.77/12.23 % (2127458)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3301950594:i=3512:aac=none_2991 on theBenchmark for (2991ds/3512Mi) % 84.77/12.23 % (2127452)Instruction limit reached! % 84.77/12.23 % (2127452)------------------------------ % 84.77/12.23 % (2127452)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 84.77/12.23 % (2127452)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 84.77/12.23 % (2127452)CaDiCaL version: 2.1.3 % 84.77/12.23 % (2127452)Termination reason: Instruction limit % 84.77/12.23 % (2127452)Termination phase: Saturation % 84.77/12.23 % (2127452)Time elapsed: 0.501 s % 84.77/12.23 % (2127452)Peak memory usage: 16 MB % 84.77/12.23 % (2127452)Instructions burned: 869 (million) % 84.77/12.23 % (2127460)dis+21_1_sil=32000:sas=cadical:random_seed=1598374425:i=3773:amm=off_2988 on theBenchmark for (2988ds/3773Mi) % 84.77/12.23 % (2127446)Instruction limit reached! % 84.77/12.23 % (2127446)------------------------------ % 84.77/12.23 % (2127446)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 84.77/12.23 % (2127446)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 84.77/12.23 % (2127446)CaDiCaL version: 2.1.3 % 84.77/12.23 % (2127446)Termination reason: Instruction limit % 84.77/12.23 % (2127446)Termination phase: Saturation % 84.77/12.23 % (2127446)Time elapsed: 0.853 s % 84.77/12.23 % (2127446)Peak memory usage: 27 MB % 84.77/12.23 % (2127446)Instructions burned: 1473 (million) % 84.77/12.23 % (2127462)ott+11_1_sil=16000:gs=on:random_seed=632700440:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2986 on theBenchmark for (2986ds/2251Mi) % 84.77/12.23 % (2127444)Instruction limit reached! % 84.77/12.23 % (2127444)------------------------------ % 84.77/12.23 % (2127444)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 84.77/12.23 % (2127444)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 84.77/12.23 % (2127444)CaDiCaL version: 2.1.3 % 84.77/12.23 % (2127444)Termination reason: Instruction limit % 84.77/12.23 % (2127444)Termination phase: Saturation % 84.77/12.23 % (2127444)Time elapsed: 1.480 s % 84.77/12.23 % (2127444)Peak memory usage: 41 MB % 84.77/12.23 % (2127444)Instructions burned: 5134 (million) % 84.77/12.23 % (2127464)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=1930024603:fmbsr=1.6:i=67534_2981 on theBenchmark for (2981ds/67534Mi) % 84.77/12.23 % (2127464)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 84.77/12.23 % (2127464)Terminated due to inappropriate strategy. % 84.77/12.23 % (2127464)------------------------------ % 84.77/12.23 % (2127464)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 84.77/12.23 % (2127464)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 84.77/12.23 % (2127464)CaDiCaL version: 2.1.3 % 84.77/12.23 % (2127464)Termination reason: Inappropriate % 84.77/12.23 % (2127464)Time elapsed: 0.001 s % 84.77/12.23 % (2127464)Peak memory usage: 10 MB % 84.77/12.23 % (2127464)Instructions burned: 2 (million) % 84.77/12.23 % (2127464)------------------------------ % 84.77/12.23 % (2127464)------------------------------ % 84.77/12.23 % (2127466)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=3560005778:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2981 on theBenchmark for (2981ds/4591Mi) % 84.77/12.23 % (2127458)Instruction limit reached! % 84.77/12.23 % (2127458)------------------------------ % 84.77/12.23 % (2127458)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 84.77/12.23 % (2127458)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 84.77/12.23 % (2127458)CaDiCaL version: 2.1.3 % 84.77/12.23 % (2127458)Termination reason: Instruction limit % 84.77/12.23 % (2127458)Termination phase: Saturation % 84.77/12.23 % (2127458)Time elapsed: 1.642 s % 84.77/12.23 % (2127458)Peak memory usage: 27 MB % 84.77/12.23 % (2127458)Instructions burned: 3514 (million) % 84.77/12.23 % (2127462)Instruction limit reached! % 84.77/12.23 % (2127462)------------------------------ % 84.77/12.23 % (2127462)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 84.77/12.23 % (2127462)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 84.77/12.23 % (2127462)CaDiCaL version: 2.1.3 % 84.77/12.23 % (2127462)Termination reason: Instruction limit % 84.77/12.23 % (2127462)Termination phase: Saturation % 84.77/12.23 % (2127462)Time elapsed: 1.219 s % 84.77/12.23 % (2127462)Peak memory usage: 24 MB % 119.10/17.10 % (2127462)Instructions burned: 2253 (million) % 119.10/17.10 % (2127468)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=3745255265:i=29340_2974 on theBenchmark for (2974ds/29340Mi) % 119.10/17.10 % (2127470)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=1386659009:i=5211_2974 on theBenchmark for (2974ds/5211Mi) % 119.10/17.10 % (2127466)Instruction limit reached! % 119.10/17.10 % (2127466)------------------------------ % 119.10/17.10 % (2127466)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 119.10/17.10 % (2127466)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 119.10/17.10 % (2127466)CaDiCaL version: 2.1.3 % 119.10/17.10 % (2127466)Termination reason: Instruction limit % 119.10/17.10 % (2127466)Termination phase: Saturation % 119.10/17.10 % (2127466)Time elapsed: 1.190 s % 119.10/17.10 % (2127466)Peak memory usage: 38 MB % 119.10/17.10 % (2127466)Instructions burned: 4594 (million) % 119.10/17.10 % (2127472)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=3156072488:i=5497:nm=2_2969 on theBenchmark for (2969ds/5497Mi) % 119.10/17.10 % (2127472)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 119.10/17.10 % (2127472)Terminated due to inappropriate strategy. % 119.10/17.10 % (2127472)------------------------------ % 119.10/17.10 % (2127472)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 119.10/17.10 % (2127472)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 119.10/17.10 % (2127472)CaDiCaL version: 2.1.3 % 119.10/17.10 % (2127472)Termination reason: Inappropriate % 119.10/17.10 % (2127472)Time elapsed: 0.0000 s % 119.10/17.10 % (2127472)Peak memory usage: 10 MB % 119.10/17.10 % (2127472)Instructions burned: 2 (million) % 119.10/17.10 % (2127472)------------------------------ % 119.10/17.10 % (2127472)------------------------------ % 119.10/17.10 % (2127474)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=1691465124:fmbsr=2:i=46332_2969 on theBenchmark for (2969ds/46332Mi) % 119.10/17.10 % (2127474)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 119.10/17.10 % (2127474)Terminated due to inappropriate strategy. % 119.10/17.10 % (2127474)------------------------------ % 119.10/17.10 % (2127474)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 119.10/17.10 % (2127474)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 119.10/17.10 % (2127474)CaDiCaL version: 2.1.3 % 119.10/17.10 % (2127474)Termination reason: Inappropriate % 119.10/17.10 % (2127474)Time elapsed: 0.0000 s % 119.10/17.10 % (2127474)Peak memory usage: 10 MB % 119.10/17.10 % (2127474)Instructions burned: 2 (million) % 119.10/17.10 % (2127474)------------------------------ % 119.10/17.10 % (2127474)------------------------------ % 119.10/17.10 % (2127476)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=944126583:i=14071_2969 on theBenchmark for (2969ds/14071Mi) % 119.10/17.10 % (2127476)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 119.10/17.10 % (2127476)Terminated due to inappropriate strategy. % 119.10/17.10 % (2127476)------------------------------ % 119.10/17.10 % (2127476)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 119.10/17.10 % (2127476)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 119.10/17.10 % (2127476)CaDiCaL version: 2.1.3 % 119.10/17.10 % (2127476)Termination reason: Inappropriate % 119.10/17.10 % (2127476)Time elapsed: 0.0000 s % 119.10/17.10 % (2127476)Peak memory usage: 10 MB % 119.10/17.10 % (2127476)Instructions burned: 2 (million) % 119.10/17.10 % (2127476)------------------------------ % 119.10/17.10 % (2127476)------------------------------ % 119.10/17.10 % (2127478)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3850785959:i=22565:add=on:rawr=on_2969 on theBenchmark for (2969ds/22565Mi) % 119.10/17.10 % (2127460)Instruction limit reached! % 119.10/17.10 % (2127460)------------------------------ % 119.10/17.10 % (2127460)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 119.10/17.10 % (2127460)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 119.10/17.10 % (2127460)CaDiCaL version: 2.1.3 % 119.10/17.10 % (2127460)Termination reason: Instruction limit % 119.10/17.10 % (2127460)Termination phase: Saturation % 119.10/17.10 % (2127460)Time elapsed: 2.051 s % 119.10/17.10 % (2127460)Peak memory usage: 32 MB % 119.10/17.10 % (2127460)Instructions burned: 3773 (million) % 119.10/17.10 % (2127480)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=2049518284:i=8173:av=off_2967 on theBenchmark for (2967ds/8173Mi) % 119.10/17.10 % (2127454)Instruction limit reached! % 120.26/17.21 % (2127454)------------------------------ % 120.26/17.21 % (2127454)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 120.26/17.21 % (2127454)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 120.26/17.21 % (2127454)CaDiCaL version: 2.1.3 % 120.26/17.21 % (2127454)Termination reason: Instruction limit % 120.26/17.21 % (2127454)Termination phase: Saturation % 120.26/17.21 % (2127454)Time elapsed: 3.180 s % 120.26/17.21 % (2127454)Peak memory usage: 38 MB % 120.26/17.21 % (2127454)Instructions burned: 5115 (million) % 120.26/17.21 % (2127482)dis+10_16:1_sil=16000:random_seed=416448691:i=9155:fsr=off_2960 on theBenchmark for (2960ds/9155Mi) % 120.26/17.21 % (2127470)Instruction limit reached! % 120.26/17.21 % (2127470)------------------------------ % 120.26/17.21 % (2127470)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 120.26/17.21 % (2127470)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 120.26/17.21 % (2127470)CaDiCaL version: 2.1.3 % 120.26/17.21 % (2127470)Termination reason: Instruction limit % 120.26/17.21 % (2127470)Termination phase: Saturation % 120.26/17.21 % (2127470)Time elapsed: 2.627 s % 120.26/17.21 % (2127470)Peak memory usage: 44 MB % 120.26/17.21 % (2127470)Instructions burned: 5213 (million) % 120.26/17.21 % (2127484)ott-3_8_sil=64000:random_seed=1630498835:i=20139:bs=on_2947 on theBenchmark for (2947ds/20139Mi) % 120.26/17.21 % (2127478)Instruction limit reached! % 120.26/17.21 % (2127478)------------------------------ % 120.26/17.21 % (2127478)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 120.26/17.21 % (2127478)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 120.26/17.21 % (2127478)CaDiCaL version: 2.1.3 % 120.26/17.21 % (2127478)Termination reason: Instruction limit % 120.26/17.21 % (2127478)Termination phase: Saturation % 120.26/17.21 % (2127478)Time elapsed: 5.021 s % 120.26/17.21 % (2127478)Peak memory usage: 64 MB % 120.26/17.21 % (2127478)Instructions burned: 22570 (million) % 120.26/17.21 % (2127486)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=2201510415:fmbsr=2:i=32576_2918 on theBenchmark for (2918ds/32576Mi) % 120.26/17.21 % (2127486)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 120.26/17.21 % (2127486)Terminated due to inappropriate strategy. % 120.26/17.21 % (2127486)------------------------------ % 120.26/17.21 % (2127486)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 120.26/17.21 % (2127486)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 120.26/17.21 % (2127486)CaDiCaL version: 2.1.3 % 120.26/17.21 % (2127486)Termination reason: Inappropriate % 120.26/17.21 % (2127486)Time elapsed: 0.001 s % 120.26/17.21 % (2127486)Peak memory usage: 10 MB % 120.26/17.21 % (2127486)Instructions burned: 2 (million) % 120.26/17.21 % (2127486)------------------------------ % 120.26/17.21 % (2127486)------------------------------ % 120.26/17.21 % (2127488)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=4199218242:i=11404_2918 on theBenchmark for (2918ds/11404Mi) % 120.26/17.21 % (2127480)Instruction limit reached! % 120.26/17.21 % (2127480)------------------------------ % 120.26/17.21 % (2127480)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 120.26/17.21 % (2127480)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 120.26/17.21 % (2127480)CaDiCaL version: 2.1.3 % 120.26/17.21 % (2127480)Termination reason: Instruction limit % 120.26/17.21 % (2127480)Termination phase: Saturation % 120.26/17.21 % (2127480)Time elapsed: 5.038 s % 120.26/17.21 % (2127480)Peak memory usage: 56 MB % 120.26/17.21 % (2127480)Instructions burned: 8174 (million) % 120.26/17.21 % (2127490)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=3447467367:i=14134_2916 on theBenchmark for (2916ds/14134Mi) % 120.26/17.21 % (2127482)Instruction limit reached! % 120.26/17.21 % (2127482)------------------------------ % 120.26/17.21 % (2127482)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 120.26/17.21 % (2127482)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 120.26/17.21 % (2127482)CaDiCaL version: 2.1.3 % 120.26/17.21 % (2127482)Termination reason: Instruction limit % 120.26/17.21 % (2127482)Termination phase: Saturation % 120.26/17.21 % (2127482)Time elapsed: 4.620 s % 120.26/17.21 % (2127482)Peak memory usage: 52 MB % 120.26/17.21 % (2127482)Instructions burned: 9157 (million) % 120.26/17.21 % (2127492)dis+33_16_sil=32000:sac=on:random_seed=781186349:i=15851:nm=0_2914 on theBenchmark for (2914ds/15851Mi) % 120.26/17.21 % (2127488)Instruction limit reached! % 120.26/17.21 % (2127488)------------------------------ % 120.26/17.21 % (2127488)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 123.84/17.91 % (2127488)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 123.84/17.91 % (2127488)CaDiCaL version: 2.1.3 % 123.84/17.91 % (2127488)Termination reason: Instruction limit % 123.84/17.91 % (2127488)Termination phase: Saturation % 123.84/17.91 % (2127488)Time elapsed: 3.833 s % 123.84/17.91 % (2127488)Peak memory usage: 62 MB % 123.84/17.91 % (2127488)Instructions burned: 11405 (million) % 123.84/17.91 % (2127494)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=3306872931:avsq=on:i=17627:add=on:amm=off_2880 on theBenchmark for (2880ds/17627Mi) % 123.84/17.91 % (2127468)Instruction limit reached! % 123.84/17.91 % (2127468)------------------------------ % 123.84/17.91 % (2127468)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 123.84/17.91 % (2127468)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 123.84/17.91 % (2127468)CaDiCaL version: 2.1.3 % 123.84/17.91 % (2127468)Termination reason: Instruction limit % 123.84/17.91 % (2127468)Termination phase: Saturation % 123.84/17.91 % (2127468)Time elapsed: 12.133 s % 123.84/17.91 % (2127468)Peak memory usage: 161 MB % 123.84/17.91 % (2127468)Instructions burned: 29342 (million) % 123.84/17.91 % (2127496)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=3598662321:s2a=on:i=53295_2852 on theBenchmark for (2852ds/53295Mi) % 123.84/17.91 % (2127492)Instruction limit reached! % 123.84/17.91 % (2127492)------------------------------ % 123.84/17.91 % (2127492)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 123.84/17.91 % (2127492)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 123.84/17.91 % (2127492)CaDiCaL version: 2.1.3 % 123.84/17.91 % (2127492)Termination reason: Instruction limit % 123.84/17.91 % (2127492)Termination phase: Saturation % 123.84/17.91 % (2127492)Time elapsed: 7.557 s % 123.84/17.91 % (2127492)Peak memory usage: 160 MB % 123.84/17.91 % (2127492)Instructions burned: 15853 (million) % 123.84/17.91 % (2127498)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=2424433561:i=26857:ins=20_2838 on theBenchmark for (2838ds/26857Mi) % 123.84/17.91 % (2127498)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 123.84/17.91 % (2127498)Terminated due to inappropriate strategy. % 123.84/17.91 % (2127498)------------------------------ % 123.84/17.91 % (2127498)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 123.84/17.91 % (2127498)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 123.84/17.91 % (2127498)CaDiCaL version: 2.1.3 % 123.84/17.91 % (2127498)Termination reason: Inappropriate % 123.84/17.91 % (2127498)Time elapsed: 0.001 s % 123.84/17.91 % (2127498)Peak memory usage: 10 MB % 123.84/17.91 % (2127498)Instructions burned: 2 (million) % 123.84/17.91 % (2127498)------------------------------ % 123.84/17.91 % (2127498)------------------------------ % 123.84/17.91 % (2127500)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=3883255036:i=28120:bs=on:fsr=off_2838 on theBenchmark for (2838ds/28120Mi) % 123.84/17.91 % (2127484)Instruction limit reached! % 123.84/17.91 % (2127484)------------------------------ % 123.84/17.91 % (2127484)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 123.84/17.91 % (2127484)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 123.84/17.91 % (2127484)CaDiCaL version: 2.1.3 % 123.84/17.91 % (2127484)Termination reason: Instruction limit % 123.84/17.91 % (2127484)Termination phase: Saturation % 123.84/17.91 % (2127484)Time elapsed: 11.571 s % 123.84/17.91 % (2127484)Peak memory usage: 75 MB % 123.84/17.91 % (2127484)Instructions burned: 20141 (million) % 123.84/17.91 % (2127502)fmb+10_1_sil=256000:fmbss=7:random_seed=359393289:fmbsr=1.6:i=182295_2831 on theBenchmark for (2831ds/182295Mi) % 123.84/17.91 % (2127502)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 123.84/17.91 % (2127502)Terminated due to inappropriate strategy. % 123.84/17.91 % (2127502)------------------------------ % 123.84/17.91 % (2127502)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 123.84/17.91 % (2127502)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 123.84/17.91 % (2127502)CaDiCaL version: 2.1.3 % 123.84/17.91 % (2127502)Termination reason: Inappropriate % 123.84/17.91 % (2127502)Time elapsed: 0.001 s % 123.84/17.91 % (2127502)Peak memory usage: 10 MB % 123.84/17.91 % (2127502)Instructions burned: 2 (million) % 123.84/17.91 % (2127502)------------------------------ % 123.84/17.91 % (2127502)------------------------------ % 123.84/17.91 % (2127504)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=88114642:i=44625:gsp=on_2831 on theBenchmark for (2831ds/44625Mi) % 132.34/18.90 % (2127504)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 132.34/18.90 % (2127504)Terminated due to inappropriate strategy. % 132.34/18.90 % (2127504)------------------------------ % 132.34/18.90 % (2127504)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 132.34/18.90 % (2127504)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 132.34/18.90 % (2127504)CaDiCaL version: 2.1.3 % 132.34/18.90 % (2127504)Termination reason: Inappropriate % 132.34/18.90 % (2127504)Time elapsed: 0.001 s % 132.34/18.90 % (2127504)Peak memory usage: 11 MB % 132.34/18.90 % (2127504)Instructions burned: 2 (million) % 132.34/18.90 % (2127504)------------------------------ % 132.34/18.90 % (2127504)------------------------------ % 132.34/18.90 % (2127506)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=1383329579:i=160505_2831 on theBenchmark for (2831ds/160505Mi) % 132.34/18.90 % (2127506)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 132.34/18.90 % (2127506)Terminated due to inappropriate strategy. % 132.34/18.90 % (2127506)------------------------------ % 132.34/18.90 % (2127506)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 132.34/18.90 % (2127506)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 132.34/18.90 % (2127506)CaDiCaL version: 2.1.3 % 132.34/18.90 % (2127506)Termination reason: Inappropriate % 132.34/18.90 % (2127506)Time elapsed: 0.001 s % 132.34/18.90 % (2127506)Peak memory usage: 10 MB % 132.34/18.90 % (2127506)Instructions burned: 2 (million) % 132.34/18.90 % (2127506)------------------------------ % 132.34/18.90 % (2127506)------------------------------ % 132.34/18.90 % (2127508)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=3099313757:fmbsr=1.3:i=225729_2831 on theBenchmark for (2831ds/225729Mi) % 132.34/18.90 % (2127508)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 132.34/18.90 % (2127508)Terminated due to inappropriate strategy. % 132.34/18.90 % (2127508)------------------------------ % 132.34/18.90 % (2127508)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 132.34/18.90 % (2127508)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 132.34/18.90 % (2127508)CaDiCaL version: 2.1.3 % 132.34/18.90 % (2127508)Termination reason: Inappropriate % 132.34/18.90 % (2127508)Time elapsed: 0.001 s % 132.34/18.90 % (2127508)Peak memory usage: 11 MB % 132.34/18.90 % (2127508)Instructions burned: 2 (million) % 132.34/18.90 % (2127508)------------------------------ % 132.34/18.90 % (2127508)------------------------------ % 132.34/18.90 % (2127510)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=839635374:fmbsr=2:i=185024:ins=7_2831 on theBenchmark for (2831ds/185024Mi) % 132.34/18.90 % (2127510)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 132.34/18.90 % (2127510)Terminated due to inappropriate strategy. % 132.34/18.90 % (2127510)------------------------------ % 132.34/18.90 % (2127510)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 132.34/18.90 % (2127510)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 132.34/18.90 % (2127510)CaDiCaL version: 2.1.3 % 132.34/18.90 % (2127510)Termination reason: Inappropriate % 132.34/18.90 % (2127510)Time elapsed: 0.001 s % 132.34/18.90 % (2127510)Peak memory usage: 11 MB % 132.34/18.90 % (2127510)Instructions burned: 2 (million) % 132.34/18.90 % (2127510)------------------------------ % 132.34/18.90 % (2127510)------------------------------ % 132.34/18.90 % (2127512)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=3502103630:rtra=on_2830 on theBenchmark for (2830ds/0Mi) % 132.34/18.90 % (2127512)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 132.34/18.90 % (2127512)Terminated due to inappropriate strategy. % 132.34/18.90 % (2127512)------------------------------ % 132.34/18.90 % (2127512)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 132.34/18.90 % (2127512)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 132.34/18.90 % (2127512)CaDiCaL version: 2.1.3 % 132.34/18.90 % (2127512)Termination reason: Inappropriate % 132.34/18.90 % (2127512)Time elapsed: 0.001 s % 132.34/18.90 % (2127512)Peak memory usage: 10 MB % 132.34/18.90 % (2127512)Instructions burned: 2 (million) % 132.34/18.90 % (2127512)------------------------------ % 132.34/18.90 % (2127512)------------------------------ % 132.34/18.90 % (2127514)% WARNING: option uhcvi not known. % 132.34/18.90 % (2127514)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3592762147:i=271062:add=off:rtra=on:rawr=on_2830 on theBenchmark for (2830ds/271062Mi) % 143.67/20.55 % (2127490)Instruction limit reached! % 143.67/20.55 % (2127490)------------------------------ % 143.67/20.55 % (2127490)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 143.67/20.55 % (2127490)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 143.67/20.55 % (2127490)CaDiCaL version: 2.1.3 % 143.67/20.55 % (2127490)Termination reason: Instruction limit % 143.67/20.55 % (2127490)Termination phase: Saturation % 143.67/20.55 % (2127490)Time elapsed: 8.720 s % 143.67/20.55 % (2127490)Peak memory usage: 78 MB % 143.67/20.55 % (2127490)Instructions burned: 14135 (million) % 143.67/20.55 % (2127516)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=423380813:i=176048:add=on:rtra=on:rawr=on_2829 on theBenchmark for (2829ds/176048Mi) % 143.67/20.55 % (2127494)Instruction limit reached! % 143.67/20.55 % (2127494)------------------------------ % 143.67/20.55 % (2127494)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 143.67/20.55 % (2127494)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 143.67/20.55 % (2127494)CaDiCaL version: 2.1.3 % 143.67/20.55 % (2127494)Termination reason: Instruction limit % 143.67/20.55 % (2127494)Termination phase: Saturation % 143.67/20.55 % (2127494)Time elapsed: 5.268 s % 143.67/20.55 % (2127494)Peak memory usage: 93 MB % 143.67/20.55 % (2127494)Instructions burned: 17629 (million) % 143.67/20.55 % (2127518)dis+10_1_sil=32000:si=on:sp=arity:random_seed=2369917797:i=206:fgj=on:rtra=on_2827 on theBenchmark for (2827ds/206Mi) % 143.67/20.55 % (2127518)Instruction limit reached! % 143.67/20.55 % (2127518)------------------------------ % 143.67/20.55 % (2127518)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 143.67/20.55 % (2127518)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 143.67/20.55 % (2127518)CaDiCaL version: 2.1.3 % 143.67/20.55 % (2127518)Termination reason: Instruction limit % 143.67/20.55 % (2127518)Termination phase: Saturation % 143.67/20.55 % (2127518)Time elapsed: 0.066 s % 143.67/20.55 % (2127518)Peak memory usage: 13 MB % 143.67/20.55 % (2127518)Instructions burned: 207 (million) % 143.67/20.55 % (2127520)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=633626244:i=232:rtra=on_2826 on theBenchmark for (2826ds/232Mi) % 143.67/20.55 % (2127520)Instruction limit reached! % 143.67/20.55 % (2127520)------------------------------ % 143.67/20.55 % (2127520)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 143.67/20.55 % (2127520)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 143.67/20.55 % (2127520)CaDiCaL version: 2.1.3 % 143.67/20.55 % (2127520)Termination reason: Instruction limit % 143.67/20.55 % (2127520)Termination phase: Saturation % 143.67/20.55 % (2127520)Time elapsed: 0.078 s % 143.67/20.55 % (2127520)Peak memory usage: 13 MB % 143.67/20.55 % (2127520)Instructions burned: 234 (million) % 143.67/20.55 % (2127522)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=2809368890:i=262:rtra=on_2825 on theBenchmark for (2825ds/262Mi) % 143.67/20.55 % (2127522)Instruction limit reached! % 143.67/20.55 % (2127522)------------------------------ % 143.67/20.55 % (2127522)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 143.67/20.55 % (2127522)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 143.67/20.55 % (2127522)CaDiCaL version: 2.1.3 % 143.67/20.55 % (2127522)Termination reason: Instruction limit % 143.67/20.55 % (2127522)Termination phase: Saturation % 143.67/20.55 % (2127522)Time elapsed: 0.072 s % 143.67/20.55 % (2127522)Peak memory usage: 14 MB % 143.67/20.55 % (2127522)Instructions burned: 263 (million) % 143.67/20.55 % (2127524)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=1329099833:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2824 on theBenchmark for (2824ds/318Mi) % 143.67/20.55 % (2127524)Instruction limit reached! % 143.67/20.55 % (2127524)------------------------------ % 143.67/20.55 % (2127524)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 143.67/20.55 % (2127524)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 143.67/20.55 % (2127524)CaDiCaL version: 2.1.3 % 143.67/20.55 % (2127524)Termination reason: Instruction limit % 143.67/20.55 % (2127524)Termination phase: Saturation % 143.67/20.55 % (2127524)Time elapsed: 0.115 s % 143.67/20.55 % (2127524)Peak memory usage: 15 MB % 143.67/20.55 % (2127524)Instructions burned: 320 (million) % 143.67/20.55 % (2127526)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=3157119541:i=1428:nm=2:rtra=on_2823 on theBenchmark for (2823ds/1428Mi) % 174.20/24.85 % (2127526)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 174.20/24.85 % (2127526)Terminated due to inappropriate strategy. % 174.20/24.85 % (2127526)------------------------------ % 174.20/24.85 % (2127526)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 174.20/24.85 % (2127526)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 174.20/24.85 % (2127526)CaDiCaL version: 2.1.3 % 174.20/24.85 % (2127526)Termination reason: Inappropriate % 174.20/24.85 % (2127526)Time elapsed: 0.001 s % 174.20/24.85 % (2127526)Peak memory usage: 10 MB % 174.20/24.85 % (2127526)Instructions burned: 2 (million) % 174.20/24.85 % (2127526)------------------------------ % 174.20/24.85 % (2127526)------------------------------ % 174.20/24.85 % (2127528)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=3665053873:i=262:bd=preordered:rtra=on:fsd=on_2823 on theBenchmark for (2823ds/262Mi) % 174.20/24.85 % (2127528)Instruction limit reached! % 174.20/24.85 % (2127528)------------------------------ % 174.20/24.85 % (2127528)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 174.20/24.85 % (2127528)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 174.20/24.85 % (2127528)CaDiCaL version: 2.1.3 % 174.20/24.85 % (2127528)Termination reason: Instruction limit % 174.20/24.85 % (2127528)Termination phase: Saturation % 174.20/24.85 % (2127528)Time elapsed: 0.084 s % 174.20/24.85 % (2127528)Peak memory usage: 13 MB % 174.20/24.85 % (2127528)Instructions burned: 262 (million) % 174.20/24.85 % (2127531)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=3009497946:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2822 on theBenchmark for (2822ds/1368Mi) % 174.20/24.85 % (2127531)Instruction limit reached! % 174.20/24.85 % (2127531)------------------------------ % 174.20/24.85 % (2127531)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 174.20/24.85 % (2127531)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 174.20/24.85 % (2127531)CaDiCaL version: 2.1.3 % 174.20/24.85 % (2127531)Termination reason: Instruction limit % 174.20/24.85 % (2127531)Termination phase: Saturation % 174.20/24.85 % (2127531)Time elapsed: 0.443 s % 174.20/24.85 % (2127531)Peak memory usage: 20 MB % 174.20/24.85 % (2127531)Instructions burned: 1369 (million) % 174.20/24.85 % (2127610)ott-21_1_sil=16000:si=on:fs=off:random_seed=4285736763:i=360:av=off:fsr=off:rtra=on_2817 on theBenchmark for (2817ds/360Mi) % 174.20/24.85 % (2127610)Instruction limit reached! % 174.20/24.85 % (2127610)------------------------------ % 174.20/24.85 % (2127610)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 174.20/24.85 % (2127610)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 174.20/24.85 % (2127610)CaDiCaL version: 2.1.3 % 174.20/24.85 % (2127610)Termination reason: Instruction limit % 174.20/24.85 % (2127610)Termination phase: Saturation % 174.20/24.85 % (2127610)Time elapsed: 0.087 s % 174.20/24.85 % (2127610)Peak memory usage: 13 MB % 174.20/24.85 % (2127610)Instructions burned: 362 (million) % 174.20/24.85 % (2127650)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2845458328:i=954:bd=all:rtra=on_2816 on theBenchmark for (2816ds/954Mi) % 174.20/24.85 % (2127650)Instruction limit reached! % 174.20/24.85 % (2127650)------------------------------ % 174.20/24.85 % (2127650)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 174.20/24.85 % (2127650)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 174.20/24.85 % (2127650)CaDiCaL version: 2.1.3 % 174.20/24.85 % (2127650)Termination reason: Instruction limit % 174.20/24.85 % (2127650)Termination phase: Saturation % 174.20/24.85 % (2127650)Time elapsed: 0.319 s % 174.20/24.85 % (2127650)Peak memory usage: 15 MB % 174.20/24.85 % (2127650)Instructions burned: 956 (million) % 174.20/24.85 % (2127656)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=4277580890:fmbsr=1.3:i=1730:ins=25:rtra=on_2813 on theBenchmark for (2813ds/1730Mi) % 174.20/24.85 % (2127656)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 174.20/24.85 % (2127656)Terminated due to inappropriate strategy. % 174.20/24.85 % (2127656)------------------------------ % 174.20/24.85 % (2127656)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 174.20/24.85 % (2127656)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 174.20/24.85 % (2127656)CaDiCaL version: 2.1.3 % 174.20/24.85 % (2127656)Termination reason: Inappropriate % 174.20/24.85 % (2127656)Time elapsed: 0.001 s % 232.03/33.52 % (2127656)Peak memory usage: 10 MB % 232.03/33.52 % (2127656)Instructions burned: 2 (million) % 232.03/33.52 % (2127656)------------------------------ % 232.03/33.52 % (2127656)------------------------------ % 232.03/33.52 % (2127658)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=16780774:i=2358:rtra=on_2813 on theBenchmark for (2813ds/2358Mi) % 232.03/33.52 % (2127658)Instruction limit reached! % 232.03/33.52 % (2127658)------------------------------ % 232.03/33.52 % (2127658)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 232.03/33.52 % (2127658)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 232.03/33.52 % (2127658)CaDiCaL version: 2.1.3 % 232.03/33.52 % (2127658)Termination reason: Instruction limit % 232.03/33.52 % (2127658)Termination phase: Saturation % 232.03/33.52 % (2127658)Time elapsed: 0.637 s % 232.03/33.52 % (2127658)Peak memory usage: 21 MB % 232.03/33.52 % (2127658)Instructions burned: 2361 (million) % 232.03/33.52 % (2127660)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=1425678717:i=1778:ins=1:rtra=on_2807 on theBenchmark for (2807ds/1778Mi) % 232.03/33.52 % (2127660)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 232.03/33.52 % (2127660)Terminated due to inappropriate strategy. % 232.03/33.52 % (2127660)------------------------------ % 232.03/33.52 % (2127660)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 232.03/33.52 % (2127660)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 232.03/33.52 % (2127660)CaDiCaL version: 2.1.3 % 232.03/33.52 % (2127660)Termination reason: Inappropriate % 232.03/33.52 % (2127660)Time elapsed: 0.001 s % 232.03/33.52 % (2127660)Peak memory usage: 10 MB % 232.03/33.52 % (2127660)Instructions burned: 2 (million) % 232.03/33.52 % (2127660)------------------------------ % 232.03/33.52 % (2127660)------------------------------ % 232.03/33.52 % (2127662)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=2353522007:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2806 on theBenchmark for (2806ds/1384Mi) % 232.03/33.52 % (2127662)Instruction limit reached! % 232.03/33.52 % (2127662)------------------------------ % 232.03/33.52 % (2127662)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 232.03/33.52 % (2127662)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 232.03/33.52 % (2127662)CaDiCaL version: 2.1.3 % 232.03/33.52 % (2127662)Termination reason: Instruction limit % 232.03/33.52 % (2127662)Termination phase: Saturation % 232.03/33.52 % (2127662)Time elapsed: 0.403 s % 232.03/33.52 % (2127662)Peak memory usage: 22 MB % 232.03/33.52 % (2127662)Instructions burned: 1384 (million) % 232.03/33.52 % (2127664)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=1308049681:i=1758:kws=inv_precedence:fsr=off:rtra=on_2802 on theBenchmark for (2802ds/1758Mi) % 232.03/33.52 % (2127664)Instruction limit reached! % 232.03/33.52 % (2127664)------------------------------ % 232.03/33.52 % (2127664)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 232.03/33.52 % (2127664)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 232.03/33.52 % (2127664)CaDiCaL version: 2.1.3 % 232.03/33.52 % (2127664)Termination reason: Instruction limit % 232.03/33.52 % (2127664)Termination phase: Saturation % 232.03/33.52 % (2127664)Time elapsed: 0.536 s % 232.03/33.52 % (2127664)Peak memory usage: 24 MB % 232.03/33.52 % (2127664)Instructions burned: 1760 (million) % 232.03/33.52 % (2127666)fmb+10_1_sil=64000:si=on:random_seed=1377218150:i=44122:nm=2:rtra=on:gsp=on_2797 on theBenchmark for (2797ds/44122Mi) % 232.03/33.52 % (2127666)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 232.03/33.52 % (2127666)Terminated due to inappropriate strategy. % 232.03/33.52 % (2127666)------------------------------ % 232.03/33.52 % (2127666)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 232.03/33.52 % (2127666)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 232.03/33.52 % (2127666)CaDiCaL version: 2.1.3 % 232.03/33.52 % (2127666)Termination reason: Inappropriate % 232.03/33.52 % (2127666)Time elapsed: 0.001 s % 232.03/33.52 % (2127666)Peak memory usage: 10 MB % 232.03/33.52 % (2127666)Instructions burned: 2 (million) % 232.03/33.52 % (2127666)------------------------------ % 232.03/33.52 % (2127666)------------------------------ % 232.03/33.52 % (2127668)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=1425162964:i=19030:nm=5:rtra=on_2797 on theBenchmark for (2797ds/19030Mi) % 300.11/42.54 % (2127668)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 300.11/42.54 % (2127668)Terminated due to inappropriate strategy. % 300.11/42.54 % (2127668)------------------------------ % 300.11/42.54 % (2127668)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.11/42.54 % (2127668)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.11/42.54 % (2127668)CaDiCaL version: 2.1.3 % 300.11/42.54 % (2127668)Termination reason: Inappropriate % 300.11/42.54 % (2127668)Time elapsed: 0.0000 s % 300.11/42.54 % (2127668)Peak memory usage: 10 MB % 300.11/42.54 % (2127668)Instructions burned: 2 (million) % 300.11/42.54 % (2127668)------------------------------ % 300.11/42.54 % (2127668)------------------------------ % 300.11/42.54 % (2127670)fmb+10_1_sil=64000:sas=cadical:si=on:fmbss=8:random_seed=3941564733:fmbsr=1.7:i=1840:rtra=on_2797 on theBenchmark for (2797ds/1840Mi) % 300.11/42.54 % (2127670)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 300.11/42.54 % (2127670)Terminated due to inappropriate strategy. % 300.11/42.54 % (2127670)------------------------------ % 300.11/42.54 % (2127670)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.11/42.54 % (2127670)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.11/42.54 % (2127670)CaDiCaL version: 2.1.3 % 300.11/42.54 % (2127670)Termination reason: Inappropriate % 300.11/42.54 % (2127670)Time elapsed: 0.001 s % 300.11/42.54 % (2127670)Peak memory usage: 10 MB % 300.11/42.54 % (2127670)Instructions burned: 2 (million) % 300.11/42.54 % (2127670)------------------------------ % 300.11/42.54 % (2127670)------------------------------ % 300.11/42.54 % (2127672)dis-4_1_sil=16000:drc=ordering:si=on:sp=const_frequency:sac=on:newcnf=on:random_seed=1687798597:i=10262:rtra=on_2796 on theBenchmark for (2796ds/10262Mi) % 300.11/42.54 % (2127672)Instruction limit reached! % 300.11/42.54 % (2127672)------------------------------ % 300.11/42.54 % (2127672)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.11/42.54 % (2127672)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.11/42.54 % (2127672)CaDiCaL version: 2.1.3 % 300.11/42.54 % (2127672)Termination reason: Instruction limit % 300.11/42.54 % (2127672)Termination phase: Saturation % 300.11/42.54 % (2127672)Time elapsed: 3.196 s % 300.11/42.54 % (2127672)Peak memory usage: 67 MB % 300.11/42.54 % (2127672)Instructions burned: 10263 (million) % 300.11/42.54 % (2127675)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:si=on:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3683602131:i=2944:ins=7:rtra=on:fdi=8:gsp=on_2764 on theBenchmark for (2764ds/2944Mi) % 300.11/42.54 % (2127675)Instruction limit reached! % 300.11/42.54 % (2127675)------------------------------ % 300.11/42.54 % (2127675)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.11/42.54 % (2127675)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.11/42.54 % (2127675)CaDiCaL version: 2.1.3 % 300.11/42.54 % (2127675)Termination reason: Instruction limit % 300.11/42.54 % (2127675)Termination phase: Saturation % 300.11/42.54 % (2127675)Time elapsed: 1.026 s % 300.11/42.54 % (2127675)Peak memory usage: 31 MB % 300.11/42.54 % (2127675)Instructions burned: 2945 (million) % 300.11/42.54 % (2127677)fmb+10_1_sil=16000:sas=cadical:si=on:bce=on:fmbss=77:random_seed=1989698730:i=12648:rtra=on_2754 on theBenchmark for (2754ds/12648Mi) % 300.11/42.54 % (2127677)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 300.11/42.54 % (2127677)Terminated due to inappropriate strategy. % 300.11/42.54 % (2127677)------------------------------ % 300.11/42.54 % (2127677)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.11/42.54 % (2127677)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.11/42.54 % (2127677)CaDiCaL version: 2.1.3 % 300.11/42.54 % (2127677)Termination reason: Inappropriate % 300.11/42.54 % (2127677)Time elapsed: 0.001 s % 300.11/42.54 % (2127677)Peak memory usage: 10 MB % 300.11/42.54 % (2127677)Instructions burned: 2 (million) % 300.11/42.54 % (2127677)------------------------------ % 300.11/42.54 % (2127677)------------------------------ % 300.11/42.54 % (2127679)fmb+10_1_fmbas=function:sil=32000:sas=cadical:si=on:fmbss=16:random_seed=3857091610:fmbsr=2.30978:i=4348:rtra=on_2754 on theBenchmark for (2754ds/4348Mi) % 300.11/42.54 % (2127679)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 300.11/42.54 % (2127679)Terminated due to inappropriate strategy. % 300.11/42.54 % (2127679)------------------------------ % 300.11/42.54 % (2127679)Version % 300.11/42.54 Terminated % 300.11/42.54 % Vampire exiting % 300.11/42.54 Terminated %------------------------------------------------------------------------------