%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWX116_1 : TPTP v9.3.1. Released v9.1.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % Computer : n015.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:46:31 PM UTC 2026 % Result : Timeout 296.58s 42.10s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.04 % Problem : SWX116_1 : TPTP v9.3.1. Released v9.1.0. % 0.00/0.07 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.10/0.24 % Computer : n015.cluster.edu % 0.10/0.24 % Model : x86_64 x86_64 % 0.10/0.24 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.24 % Memory : 8046.5625MB % 0.10/0.24 % OS : Linux 6.8.0-71-generic % 0.10/0.24 % CPULimit : 300 % 0.10/0.24 % WCLimit : 300 % 0.10/0.24 % DateTime : Mon Sep 28 15:05:32 UTC 2026 % 0.10/0.25 % CPUTime : % 0.10/0.25 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.22/0.30 Running first-order model finding % 0.22/0.30 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 % 6.96/1.33 % (2697959)Will run a generic schedule for satisfiability detection. % 6.96/1.33 % (2697966)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3338788577:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 6.96/1.33 % (2697965)% WARNING: option uhcvi not known. % 6.96/1.33 % (2697964)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=48555820_2999 on theBenchmark for (2999ds/0Mi) % 6.96/1.33 % (2697965)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=998065631:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 6.96/1.33 % (2697967)dis+10_1_sil=32000:sp=arity:random_seed=4134301927:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 6.96/1.33 % (2697968)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=551565443:i=116_2999 on theBenchmark for (2999ds/116Mi) % 6.96/1.33 % (2697969)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1320361627:i=131_2999 on theBenchmark for (2999ds/131Mi) % 6.96/1.33 % (2697970)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3606775398:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 6.96/1.33 % (2697964)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 6.96/1.33 % (2697964)Terminated due to inappropriate strategy. % 6.96/1.33 % (2697964)------------------------------ % 6.96/1.33 % (2697964)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.96/1.33 % (2697964)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.96/1.33 % (2697964)CaDiCaL version: 2.1.3 % 6.96/1.33 % (2697964)Termination reason: Inappropriate % 6.96/1.33 % (2697964)Time elapsed: 0.006 s % 6.96/1.33 % (2697964)Peak memory usage: 11 MB % 6.96/1.33 % (2697964)Instructions burned: 6 (million) % 6.96/1.33 % (2697964)------------------------------ % 6.96/1.33 % (2697964)------------------------------ % 6.96/1.33 % (2697978)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=452736053:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 6.96/1.33 % (2697978)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 6.96/1.33 % (2697978)Terminated due to inappropriate strategy. % 6.96/1.33 % (2697978)------------------------------ % 6.96/1.33 % (2697978)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.96/1.33 % (2697978)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.96/1.33 % (2697978)CaDiCaL version: 2.1.3 % 6.96/1.33 % (2697978)Termination reason: Inappropriate % 6.96/1.33 % (2697978)Time elapsed: 0.005 s % 6.96/1.33 % (2697978)Peak memory usage: 10 MB % 6.96/1.33 % (2697978)Instructions burned: 4 (million) % 6.96/1.33 % (2697978)------------------------------ % 6.96/1.33 % (2697978)------------------------------ % 6.96/1.33 % (2697980)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1732634746:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 6.96/1.33 % (2697967)Instruction limit reached! % 6.96/1.33 % (2697967)------------------------------ % 6.96/1.33 % (2697967)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.96/1.33 % (2697967)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.96/1.33 % (2697967)CaDiCaL version: 2.1.3 % 6.96/1.33 % (2697967)Termination reason: Instruction limit % 6.96/1.33 % (2697967)Termination phase: Saturation % 6.96/1.33 % (2697967)Time elapsed: 0.112 s % 6.96/1.33 % (2697967)Peak memory usage: 13 MB % 6.96/1.33 % (2697967)Instructions burned: 103 (million) % 6.96/1.33 % (2697968)Instruction limit reached! % 6.96/1.33 % (2697968)------------------------------ % 6.96/1.33 % (2697968)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.96/1.33 % (2697968)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.96/1.33 % (2697968)CaDiCaL version: 2.1.3 % 6.96/1.33 % (2697968)Termination reason: Instruction limit % 6.96/1.33 % (2697968)Termination phase: Saturation % 6.96/1.33 % (2697968)Time elapsed: 0.115 s % 6.96/1.33 % (2697968)Peak memory usage: 13 MB % 6.96/1.33 % (2697968)Instructions burned: 117 (million) % 6.96/1.33 % (2697969)Instruction limit reached! % 6.96/1.33 % (2697969)------------------------------ % 6.96/1.33 % (2697969)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.96/1.33 % (2697969)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.96/1.33 % (2697969)CaDiCaL version: 2.1.3 % 6.96/1.33 % (2697969)Termination reason: Instruction limit % 8.53/1.74 % (2697969)Termination phase: Saturation % 8.53/1.74 % (2697969)Time elapsed: 0.128 s % 8.53/1.74 % (2697969)Peak memory usage: 13 MB % 8.53/1.74 % (2697969)Instructions burned: 131 (million) % 8.53/1.74 % (2697982)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=1935357354:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi) % 8.53/1.74 % (2697983)ott-21_1_sil=16000:fs=off:random_seed=1659453050:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 8.53/1.74 % (2697984)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2598311975:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 8.53/1.74 % (2697970)Instruction limit reached! % 8.53/1.74 % (2697970)------------------------------ % 8.53/1.74 % (2697970)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.53/1.74 % (2697970)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.53/1.74 % (2697970)CaDiCaL version: 2.1.3 % 8.53/1.74 % (2697970)Termination reason: Instruction limit % 8.53/1.74 % (2697970)Termination phase: Saturation % 8.53/1.74 % (2697970)Time elapsed: 0.179 s % 8.53/1.74 % (2697970)Peak memory usage: 14 MB % 8.53/1.74 % (2697970)Instructions burned: 159 (million) % 8.53/1.74 % (2697988)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3816418448:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi) % 8.53/1.74 % (2697980)Instruction limit reached! % 8.53/1.74 % (2697980)------------------------------ % 8.53/1.74 % (2697980)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.53/1.74 % (2697980)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.53/1.74 % (2697980)CaDiCaL version: 2.1.3 % 8.53/1.74 % (2697980)Termination reason: Instruction limit % 8.53/1.74 % (2697980)Termination phase: Saturation % 8.53/1.74 % (2697980)Time elapsed: 0.134 s % 8.53/1.74 % (2697980)Peak memory usage: 12 MB % 8.53/1.74 % (2697980)Instructions burned: 131 (million) % 8.53/1.74 % (2697988)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 8.53/1.74 % (2697988)Terminated due to inappropriate strategy. % 8.53/1.74 % (2697988)------------------------------ % 8.53/1.74 % (2697988)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.53/1.74 % (2697988)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.53/1.74 % (2697988)CaDiCaL version: 2.1.3 % 8.53/1.74 % (2697988)Termination reason: Inappropriate % 8.53/1.74 % (2697988)Time elapsed: 0.007 s % 8.53/1.74 % (2697988)Peak memory usage: 10 MB % 8.53/1.74 % (2697988)Instructions burned: 3 (million) % 8.53/1.74 % (2697988)------------------------------ % 8.53/1.74 % (2697988)------------------------------ % 8.53/1.74 % (2697990)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=271803258:i=1179_2997 on theBenchmark for (2997ds/1179Mi) % 8.53/1.74 % (2697991)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2781921322:i=889:ins=1_2997 on theBenchmark for (2997ds/889Mi) % 8.53/1.74 % (2697991)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 8.53/1.74 % (2697991)Terminated due to inappropriate strategy. % 8.53/1.74 % (2697991)------------------------------ % 8.53/1.74 % (2697991)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.53/1.74 % (2697991)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.53/1.74 % (2697991)CaDiCaL version: 2.1.3 % 8.53/1.74 % (2697991)Termination reason: Inappropriate % 8.53/1.74 % (2697991)Time elapsed: 0.005 s % 8.53/1.74 % (2697991)Peak memory usage: 10 MB % 8.53/1.74 % (2697991)Instructions burned: 4 (million) % 8.53/1.74 % (2697991)------------------------------ % 8.53/1.74 % (2697991)------------------------------ % 8.53/1.74 % (2697994)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=2673141268:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2997 on theBenchmark for (2997ds/692Mi) % 8.53/1.74 % (2697983)Instruction limit reached! % 8.53/1.74 % (2697983)------------------------------ % 8.53/1.74 % (2697983)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.53/1.74 % (2697983)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.53/1.74 % (2697983)CaDiCaL version: 2.1.3 % 8.53/1.74 % (2697983)Termination reason: Instruction limit % 8.53/1.74 % (2697983)Termination phase: Saturation % 38.44/5.84 % (2697983)Time elapsed: 0.153 s % 38.44/5.84 % (2697983)Peak memory usage: 12 MB % 38.44/5.84 % (2697983)Instructions burned: 181 (million) % 38.44/5.84 % (2697996)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3913403782:i=879:kws=inv_precedence:fsr=off_2996 on theBenchmark for (2996ds/879Mi) % 38.44/5.84 % (2697984)Instruction limit reached! % 38.44/5.84 % (2697984)------------------------------ % 38.44/5.84 % (2697984)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 38.44/5.84 % (2697984)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 38.44/5.84 % (2697984)CaDiCaL version: 2.1.3 % 38.44/5.84 % (2697984)Termination reason: Instruction limit % 38.44/5.84 % (2697984)Termination phase: Saturation % 38.44/5.84 % (2697984)Time elapsed: 0.545 s % 38.44/5.84 % (2697984)Peak memory usage: 14 MB % 38.44/5.84 % (2697984)Instructions burned: 477 (million) % 38.44/5.84 % (2697998)fmb+10_1_sil=64000:random_seed=3744271538:i=22061:nm=2:gsp=on_2992 on theBenchmark for (2992ds/22061Mi) % 38.44/5.84 % (2697998)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 38.44/5.84 % (2697998)Terminated due to inappropriate strategy. % 38.44/5.84 % (2697998)------------------------------ % 38.44/5.84 % (2697998)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 38.44/5.84 % (2697998)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 38.44/5.84 % (2697998)CaDiCaL version: 2.1.3 % 38.44/5.84 % (2697998)Termination reason: Inappropriate % 38.44/5.84 % (2697998)Time elapsed: 0.005 s % 38.44/5.84 % (2697998)Peak memory usage: 10 MB % 38.44/5.84 % (2697998)Instructions burned: 5 (million) % 38.44/5.84 % (2697998)------------------------------ % 38.44/5.84 % (2697998)------------------------------ % 38.44/5.84 % (2698000)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1416628328:i=9515:nm=5_2992 on theBenchmark for (2992ds/9515Mi) % 38.44/5.84 % (2698000)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 38.44/5.84 % (2698000)Terminated due to inappropriate strategy. % 38.44/5.84 % (2698000)------------------------------ % 38.44/5.84 % (2698000)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 38.44/5.84 % (2698000)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 38.44/5.84 % (2698000)CaDiCaL version: 2.1.3 % 38.44/5.84 % (2698000)Termination reason: Inappropriate % 38.44/5.84 % (2698000)Time elapsed: 0.005 s % 38.44/5.84 % (2698000)Peak memory usage: 10 MB % 38.44/5.84 % (2698000)Instructions burned: 4 (million) % 38.44/5.84 % (2698000)------------------------------ % 38.44/5.84 % (2698000)------------------------------ % 38.44/5.84 % (2698002)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=825510935:fmbsr=1.7:i=920_2991 on theBenchmark for (2991ds/920Mi) % 38.44/5.84 % (2698002)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 38.44/5.84 % (2698002)Terminated due to inappropriate strategy. % 38.44/5.84 % (2698002)------------------------------ % 38.44/5.84 % (2698002)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 38.44/5.84 % (2698002)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 38.44/5.84 % (2698002)CaDiCaL version: 2.1.3 % 38.44/5.84 % (2698002)Termination reason: Inappropriate % 38.44/5.84 % (2698002)Time elapsed: 0.005 s % 38.44/5.84 % (2698002)Peak memory usage: 10 MB % 38.44/5.84 % (2698002)Instructions burned: 4 (million) % 38.44/5.84 % (2698002)------------------------------ % 38.44/5.84 % (2698002)------------------------------ % 38.44/5.84 % (2698004)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=230884868:i=5131_2991 on theBenchmark for (2991ds/5131Mi) % 38.44/5.84 % (2697982)Instruction limit reached! % 38.44/5.84 % (2697982)------------------------------ % 38.44/5.84 % (2697982)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 38.44/5.84 % (2697982)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 38.44/5.84 % (2697982)CaDiCaL version: 2.1.3 % 38.44/5.84 % (2697982)Termination reason: Instruction limit % 38.44/5.84 % (2697982)Termination phase: Saturation % 38.44/5.84 % (2697982)Time elapsed: 0.706 s % 38.44/5.84 % (2697982)Peak memory usage: 27 MB % 38.44/5.84 % (2697982)Instructions burned: 684 (million) % 38.44/5.84 % (2698006)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1231934819:i=1472:ins=7:fdi=8:gsp=on_2991 on theBenchmark for (2991ds/1472Mi) % 38.44/5.84 % (2697994)Instruction limit reached! % 38.44/5.84 % (2697994)------------------------------ % 58.98/8.60 % (2697994)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 58.98/8.60 % (2697994)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 58.98/8.60 % (2697994)CaDiCaL version: 2.1.3 % 58.98/8.60 % (2697994)Termination reason: Instruction limit % 58.98/8.60 % (2697994)Termination phase: Saturation % 58.98/8.60 % (2697994)Time elapsed: 0.702 s % 58.98/8.60 % (2697994)Peak memory usage: 18 MB % 58.98/8.60 % (2697994)Instructions burned: 692 (million) % 58.98/8.60 % (2698008)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=227489960:i=6324_2989 on theBenchmark for (2989ds/6324Mi) % 58.98/8.60 % (2698008)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 58.98/8.60 % (2698008)Terminated due to inappropriate strategy. % 58.98/8.60 % (2698008)------------------------------ % 58.98/8.60 % (2698008)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 58.98/8.60 % (2698008)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 58.98/8.60 % (2698008)CaDiCaL version: 2.1.3 % 58.98/8.60 % (2698008)Termination reason: Inappropriate % 58.98/8.60 % (2698008)Time elapsed: 0.006 s % 58.98/8.60 % (2698008)Peak memory usage: 11 MB % 58.98/8.60 % (2698008)Instructions burned: 6 (million) % 58.98/8.60 % (2698008)------------------------------ % 58.98/8.60 % (2698008)------------------------------ % 58.98/8.60 % (2698010)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1603121456:fmbsr=2.30978:i=2174_2989 on theBenchmark for (2989ds/2174Mi) % 58.98/8.60 % (2698010)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 58.98/8.60 % (2698010)Terminated due to inappropriate strategy. % 58.98/8.60 % (2698010)------------------------------ % 58.98/8.60 % (2698010)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 58.98/8.60 % (2698010)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 58.98/8.60 % (2698010)CaDiCaL version: 2.1.3 % 58.98/8.60 % (2698010)Termination reason: Inappropriate % 58.98/8.60 % (2698010)Time elapsed: 0.003 s % 58.98/8.60 % (2698010)Peak memory usage: 11 MB % 58.98/8.60 % (2698010)Instructions burned: 4 (million) % 58.98/8.60 % (2698010)------------------------------ % 58.98/8.60 % (2698010)------------------------------ % 58.98/8.60 % (2698012)ott-2_1_sil=16000:newcnf=on:random_seed=2839610482:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2989 on theBenchmark for (2989ds/869Mi) % 58.98/8.60 % (2697996)Instruction limit reached! % 58.98/8.60 % (2697996)------------------------------ % 58.98/8.60 % (2697996)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 58.98/8.60 % (2697996)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 58.98/8.60 % (2697996)CaDiCaL version: 2.1.3 % 58.98/8.60 % (2697996)Termination reason: Instruction limit % 58.98/8.60 % (2697996)Termination phase: Saturation % 58.98/8.60 % (2697996)Time elapsed: 0.828 s % 58.98/8.60 % (2697996)Peak memory usage: 19 MB % 58.98/8.60 % (2697996)Instructions burned: 879 (million) % 58.98/8.60 % (2698014)ott+10_1_sil=32000:tgt=ground:random_seed=3531494479:i=5114:av=off_2987 on theBenchmark for (2987ds/5114Mi) % 58.98/8.60 % (2697990)Instruction limit reached! % 58.98/8.60 % (2697990)------------------------------ % 58.98/8.60 % (2697990)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 58.98/8.60 % (2697990)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 58.98/8.60 % (2697990)CaDiCaL version: 2.1.3 % 58.98/8.60 % (2697990)Termination reason: Instruction limit % 58.98/8.60 % (2697990)Termination phase: Saturation % 58.98/8.60 % (2697990)Time elapsed: 1.133 s % 58.98/8.60 % (2697990)Peak memory usage: 21 MB % 58.98/8.60 % (2697990)Instructions burned: 1179 (million) % 58.98/8.60 % (2698016)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=803329812:i=54282_2985 on theBenchmark for (2985ds/54282Mi) % 58.98/8.60 % (2698016)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 58.98/8.60 % (2698016)Terminated due to inappropriate strategy. % 58.98/8.60 % (2698016)------------------------------ % 58.98/8.60 % (2698016)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 58.98/8.60 % (2698016)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 58.98/8.60 % (2698016)CaDiCaL version: 2.1.3 % 58.98/8.60 % (2698016)Termination reason: Inappropriate % 58.98/8.60 % (2698016)Time elapsed: 0.005 s % 58.98/8.60 % (2698016)Peak memory usage: 11 MB % 58.98/8.60 % (2698016)Instructions burned: 6 (million) % 157.81/22.59 % (2698016)------------------------------ % 157.81/22.59 % (2698016)------------------------------ % 157.81/22.59 % (2698018)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=198904178:i=3512:aac=none_2985 on theBenchmark for (2985ds/3512Mi) % 157.81/22.59 % (2698012)Instruction limit reached! % 157.81/22.59 % (2698012)------------------------------ % 157.81/22.59 % (2698012)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 157.81/22.59 % (2698012)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 157.81/22.59 % (2698012)CaDiCaL version: 2.1.3 % 157.81/22.59 % (2698012)Termination reason: Instruction limit % 157.81/22.59 % (2698012)Termination phase: Saturation % 157.81/22.59 % (2698012)Time elapsed: 0.840 s % 157.81/22.59 % (2698012)Peak memory usage: 18 MB % 157.81/22.59 % (2698012)Instructions burned: 869 (million) % 157.81/22.59 % (2698022)dis+21_1_sil=32000:sas=cadical:random_seed=3319353698:i=3773:amm=off_2980 on theBenchmark for (2980ds/3773Mi) % 157.81/22.59 % (2698006)Instruction limit reached! % 157.81/22.59 % (2698006)------------------------------ % 157.81/22.59 % (2698006)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 157.81/22.59 % (2698006)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 157.81/22.59 % (2698006)CaDiCaL version: 2.1.3 % 157.81/22.59 % (2698006)Termination reason: Instruction limit % 157.81/22.59 % (2698006)Termination phase: Saturation % 157.81/22.59 % (2698006)Time elapsed: 1.468 s % 157.81/22.59 % (2698006)Peak memory usage: 27 MB % 157.81/22.59 % (2698006)Instructions burned: 1472 (million) % 157.81/22.59 % (2698026)ott+11_1_sil=16000:gs=on:random_seed=2526357474:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2976 on theBenchmark for (2976ds/2251Mi) % 157.81/22.59 % (2698026)Instruction limit reached! % 157.81/22.59 % (2698026)------------------------------ % 157.81/22.59 % (2698026)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 157.81/22.59 % (2698026)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 157.81/22.59 % (2698026)CaDiCaL version: 2.1.3 % 157.81/22.59 % (2698026)Termination reason: Instruction limit % 157.81/22.59 % (2698026)Termination phase: Saturation % 157.81/22.59 % (2698026)Time elapsed: 2.166 s % 157.81/22.59 % (2698026)Peak memory usage: 24 MB % 157.81/22.59 % (2698026)Instructions burned: 2252 (million) % 157.81/22.59 % (2698035)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=253507435:fmbsr=1.6:i=67534_2954 on theBenchmark for (2954ds/67534Mi) % 157.81/22.59 % (2698035)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 157.81/22.59 % (2698035)Terminated due to inappropriate strategy. % 157.81/22.59 % (2698035)------------------------------ % 157.81/22.59 % (2698035)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 157.81/22.59 % (2698035)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 157.81/22.59 % (2698035)CaDiCaL version: 2.1.3 % 157.81/22.59 % (2698035)Termination reason: Inappropriate % 157.81/22.59 % (2698035)Time elapsed: 0.004 s % 157.81/22.59 % (2698035)Peak memory usage: 11 MB % 157.81/22.59 % (2698035)Instructions burned: 4 (million) % 157.81/22.59 % (2698035)------------------------------ % 157.81/22.59 % (2698035)------------------------------ % 157.81/22.59 % (2698037)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=1547783328:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2953 on theBenchmark for (2953ds/4591Mi) % 157.81/22.59 % (2698018)Instruction limit reached! % 157.81/22.59 % (2698018)------------------------------ % 157.81/22.59 % (2698018)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 157.81/22.59 % (2698018)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 157.81/22.59 % (2698018)CaDiCaL version: 2.1.3 % 157.81/22.59 % (2698018)Termination reason: Instruction limit % 157.81/22.59 % (2698018)Termination phase: Saturation % 157.81/22.59 % (2698018)Time elapsed: 3.309 s % 157.81/22.59 % (2698018)Peak memory usage: 35 MB % 157.81/22.59 % (2698018)Instructions burned: 3512 (million) % 157.81/22.59 % (2698039)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=2317691467:i=29340_2952 on theBenchmark for (2952ds/29340Mi) % 157.81/22.59 % (2698022)Instruction limit reached! % 157.81/22.59 % (2698022)------------------------------ % 157.81/22.59 % (2698022)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 157.81/22.59 % (2698022)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 157.81/22.59 % (2698022)CaDiCaL version: 2.1.3 % 157.81/22.59 % (2698022)Termination reason: Instruction limit % 176.86/27.78 % (2698022)Termination phase: Saturation % 176.86/27.78 % (2698022)Time elapsed: 3.534 s % 176.86/27.78 % (2698022)Peak memory usage: 34 MB % 176.86/27.78 % (2698022)Instructions burned: 3773 (million) % 176.86/27.78 % (2698043)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=3394688677:i=5211_2944 on theBenchmark for (2944ds/5211Mi) % 176.86/27.78 % (2698004)Instruction limit reached! % 176.86/27.78 % (2698004)------------------------------ % 176.86/27.78 % (2698004)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 176.86/27.78 % (2698004)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 176.86/27.78 % (2698004)CaDiCaL version: 2.1.3 % 176.86/27.78 % (2698004)Termination reason: Instruction limit % 176.86/27.78 % (2698004)Termination phase: Saturation % 176.86/27.78 % (2698004)Time elapsed: 4.715 s % 176.86/27.78 % (2698004)Peak memory usage: 41 MB % 176.86/27.78 % (2698004)Instructions burned: 5131 (million) % 176.86/27.78 % (2698045)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=2844810864:i=5497:nm=2_2943 on theBenchmark for (2943ds/5497Mi) % 176.86/27.78 % (2698045)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 176.86/27.78 % (2698045)Terminated due to inappropriate strategy. % 176.86/27.78 % (2698045)------------------------------ % 176.86/27.78 % (2698045)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 176.86/27.78 % (2698045)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 176.86/27.78 % (2698045)CaDiCaL version: 2.1.3 % 176.86/27.78 % (2698045)Termination reason: Inappropriate % 176.86/27.78 % (2698045)Time elapsed: 0.005 s % 176.86/27.78 % (2698045)Peak memory usage: 11 MB % 176.86/27.78 % (2698045)Instructions burned: 6 (million) % 176.86/27.78 % (2698045)------------------------------ % 176.86/27.78 % (2698045)------------------------------ % 176.86/27.78 % (2698047)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=1952651826:fmbsr=2:i=46332_2943 on theBenchmark for (2943ds/46332Mi) % 176.86/27.78 % (2698047)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 176.86/27.78 % (2698047)Terminated due to inappropriate strategy. % 176.86/27.78 % (2698047)------------------------------ % 176.86/27.78 % (2698047)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 176.86/27.78 % (2698047)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 176.86/27.78 % (2698047)CaDiCaL version: 2.1.3 % 176.86/27.78 % (2698047)Termination reason: Inappropriate % 176.86/27.78 % (2698047)Time elapsed: 0.005 s % 176.86/27.78 % (2698047)Peak memory usage: 11 MB % 176.86/27.78 % (2698047)Instructions burned: 4 (million) % 176.86/27.78 % (2698047)------------------------------ % 176.86/27.78 % (2698047)------------------------------ % 176.86/27.78 % (2698049)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=254115856:i=14071_2943 on theBenchmark for (2943ds/14071Mi) % 176.86/27.78 % (2698049)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 176.86/27.78 % (2698049)Terminated due to inappropriate strategy. % 176.86/27.78 % (2698049)------------------------------ % 176.86/27.78 % (2698049)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 176.86/27.78 % (2698049)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 176.86/27.78 % (2698049)CaDiCaL version: 2.1.3 % 176.86/27.78 % (2698049)Termination reason: Inappropriate % 176.86/27.78 % (2698049)Time elapsed: 0.007 s % 176.86/27.78 % (2698049)Peak memory usage: 11 MB % 176.86/27.78 % (2698049)Instructions burned: 4 (million) % 176.86/27.78 % (2698049)------------------------------ % 176.86/27.78 % (2698049)------------------------------ % 176.86/27.78 % (2698051)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=829808438:i=22565:add=on:rawr=on_2942 on theBenchmark for (2942ds/22565Mi) % 176.86/27.78 % (2698014)Instruction limit reached! % 176.86/27.78 % (2698014)------------------------------ % 176.86/27.78 % (2698014)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 176.86/27.78 % (2698014)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 176.86/27.78 % (2698014)CaDiCaL version: 2.1.3 % 176.86/27.78 % (2698014)Termination reason: Instruction limit % 176.86/27.78 % (2698014)Termination phase: Saturation % 176.86/27.78 % (2698014)Time elapsed: 4.769 s % 176.86/27.78 % (2698014)Peak memory usage: 31 MB % 176.86/27.78 % (2698014)Instructions burned: 5114 (million) % 176.86/27.78 % (2698053)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=21993409:i=8173:av=off_2939 on theBenchmark for (2939ds/8173Mi) % 176.86/27.78 % (2698037)Instruction limit reached! % 195.36/27.88 % (2698037)------------------------------ % 195.36/27.88 % (2698037)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 195.36/27.88 % (2698037)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 195.36/27.88 % (2698037)CaDiCaL version: 2.1.3 % 195.36/27.88 % (2698037)Termination reason: Instruction limit % 195.36/27.88 % (2698037)Termination phase: Saturation % 195.36/27.88 % (2698037)Time elapsed: 3.637 s % 195.36/27.88 % (2698037)Peak memory usage: 37 MB % 195.36/27.88 % (2698037)Instructions burned: 4591 (million) % 195.36/27.88 % (2698057)dis+10_16:1_sil=16000:random_seed=2793780433:i=9155:fsr=off_2916 on theBenchmark for (2916ds/9155Mi) % 195.36/27.88 % (2698043)Instruction limit reached! % 195.36/27.88 % (2698043)------------------------------ % 195.36/27.88 % (2698043)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 195.36/27.88 % (2698043)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 195.36/27.88 % (2698043)CaDiCaL version: 2.1.3 % 195.36/27.88 % (2698043)Termination reason: Instruction limit % 195.36/27.88 % (2698043)Termination phase: Saturation % 195.36/27.88 % (2698043)Time elapsed: 4.183 s % 195.36/27.88 % (2698043)Peak memory usage: 30 MB % 195.36/27.88 % (2698043)Instructions burned: 5211 (million) % 195.36/27.88 % (2698060)ott-3_8_sil=64000:random_seed=2333830948:i=20139:bs=on_2902 on theBenchmark for (2902ds/20139Mi) % 195.36/27.88 % (2698053)Instruction limit reached! % 195.36/27.88 % (2698053)------------------------------ % 195.36/27.88 % (2698053)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 195.36/27.88 % (2698053)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 195.36/27.88 % (2698053)CaDiCaL version: 2.1.3 % 195.36/27.88 % (2698053)Termination reason: Instruction limit % 195.36/27.88 % (2698053)Termination phase: Saturation % 195.36/27.88 % (2698053)Time elapsed: 8.029 s % 195.36/27.88 % (2698053)Peak memory usage: 52 MB % 195.36/27.88 % (2698053)Instructions burned: 8173 (million) % 195.36/27.88 % (2698065)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=1817224285:fmbsr=2:i=32576_2859 on theBenchmark for (2859ds/32576Mi) % 195.36/27.88 % (2698065)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 195.36/27.88 % (2698065)Terminated due to inappropriate strategy. % 195.36/27.88 % (2698065)------------------------------ % 195.36/27.88 % (2698065)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 195.36/27.88 % (2698065)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 195.36/27.88 % (2698065)CaDiCaL version: 2.1.3 % 195.36/27.88 % (2698065)Termination reason: Inappropriate % 195.36/27.88 % (2698065)Time elapsed: 0.007 s % 195.36/27.88 % (2698065)Peak memory usage: 11 MB % 195.36/27.88 % (2698065)Instructions burned: 6 (million) % 195.36/27.88 % (2698065)------------------------------ % 195.36/27.88 % (2698065)------------------------------ % 195.36/27.88 % (2698067)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=2777350607:i=11404_2858 on theBenchmark for (2858ds/11404Mi) % 195.36/27.88 % (2698057)Instruction limit reached! % 195.36/27.88 % (2698057)------------------------------ % 195.36/27.88 % (2698057)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 195.36/27.88 % (2698057)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 195.36/27.88 % (2698057)CaDiCaL version: 2.1.3 % 195.36/27.88 % (2698057)Termination reason: Instruction limit % 195.36/27.88 % (2698057)Termination phase: Saturation % 195.36/27.88 % (2698057)Time elapsed: 8.176 s % 195.36/27.88 % (2698057)Peak memory usage: 56 MB % 195.36/27.88 % (2698057)Instructions burned: 9155 (million) % 195.36/27.88 % (2698071)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=1803959972:i=14134_2834 on theBenchmark for (2834ds/14134Mi) % 195.36/27.88 % (2698039)Instruction limit reached! % 195.36/27.88 % (2698039)------------------------------ % 195.36/27.88 % (2698039)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 195.36/27.88 % (2698039)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 195.36/27.88 % (2698039)CaDiCaL version: 2.1.3 % 195.36/27.88 % (2698039)Termination reason: Instruction limit % 195.36/27.88 % (2698039)Termination phase: Saturation % 195.36/27.88 % (2698039)Time elapsed: 14.269 s % 195.36/27.88 % (2698039)Peak memory usage: 165 MB % 195.36/27.88 % (2698039)Instructions burned: 29341 (million) % 195.36/27.88 % (2698075)dis+33_16_sil=32000:sac=on:random_seed=1374873193:i=15851:nm=0_2809 on theBenchmark for (2809ds/15851Mi) % 195.36/27.88 % (2698051)Instruction limit reached! % 195.36/27.88 % (2698051)------------------------------ % 195.36/27.88 % (2698051)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 245.80/35.02 % (2698051)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 245.80/35.02 % (2698051)CaDiCaL version: 2.1.3 % 245.80/35.02 % (2698051)Termination reason: Instruction limit % 245.80/35.02 % (2698051)Termination phase: Saturation % 245.80/35.02 % (2698051)Time elapsed: 16.518 s % 245.80/35.02 % (2698051)Peak memory usage: 72 MB % 245.80/35.02 % (2698051)Instructions burned: 22566 (million) % 245.80/35.02 % (2698079)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=2856222514:avsq=on:i=17627:add=on:amm=off_2776 on theBenchmark for (2776ds/17627Mi) % 245.80/35.02 % (2698067)Instruction limit reached! % 245.80/35.02 % (2698067)------------------------------ % 245.80/35.02 % (2698067)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 245.80/35.02 % (2698067)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 245.80/35.02 % (2698067)CaDiCaL version: 2.1.3 % 245.80/35.02 % (2698067)Termination reason: Instruction limit % 245.80/35.02 % (2698067)Termination phase: Saturation % 245.80/35.02 % (2698067)Time elapsed: 11.620 s % 245.80/35.02 % (2698067)Peak memory usage: 63 MB % 245.80/35.02 % (2698067)Instructions burned: 11404 (million) % 245.80/35.02 % (2698087)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=1927341634:s2a=on:i=53295_2742 on theBenchmark for (2742ds/53295Mi) % 245.80/35.02 % (2698075)Instruction limit reached! % 245.80/35.02 % (2698075)------------------------------ % 245.80/35.02 % (2698075)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 245.80/35.02 % (2698075)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 245.80/35.02 % (2698075)CaDiCaL version: 2.1.3 % 245.80/35.02 % (2698075)Termination reason: Instruction limit % 245.80/35.02 % (2698075)Termination phase: Saturation % 245.80/35.02 % (2698075)Time elapsed: 8.143 s % 245.80/35.02 % (2698075)Peak memory usage: 121 MB % 245.80/35.02 % (2698075)Instructions burned: 15852 (million) % 245.80/35.02 % (2698091)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=1015334259:i=26857:ins=20_2727 on theBenchmark for (2727ds/26857Mi) % 245.80/35.02 % (2698091)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 245.80/35.02 % (2698091)Terminated due to inappropriate strategy. % 245.80/35.02 % (2698091)------------------------------ % 245.80/35.02 % (2698091)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 245.80/35.02 % (2698091)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 245.80/35.02 % (2698091)CaDiCaL version: 2.1.3 % 245.80/35.02 % (2698091)Termination reason: Inappropriate % 245.80/35.02 % (2698091)Time elapsed: 0.003 s % 245.80/35.02 % (2698091)Peak memory usage: 10 MB % 245.80/35.02 % (2698091)Instructions burned: 4 (million) % 245.80/35.02 % (2698091)------------------------------ % 245.80/35.02 % (2698091)------------------------------ % 245.80/35.02 % (2698093)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=2878660763:i=28120:bs=on:fsr=off_2726 on theBenchmark for (2726ds/28120Mi) % 245.80/35.02 % (2698060)Instruction limit reached! % 245.80/35.02 % (2698060)------------------------------ % 245.80/35.02 % (2698060)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 245.80/35.02 % (2698060)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 245.80/35.02 % (2698060)CaDiCaL version: 2.1.3 % 245.80/35.02 % (2698060)Termination reason: Instruction limit % 245.80/35.02 % (2698060)Termination phase: Saturation % 245.80/35.02 % (2698060)Time elapsed: 17.606 s % 245.80/35.02 % (2698060)Peak memory usage: 67 MB % 245.80/35.02 % (2698060)Instructions burned: 20139 (million) % 245.80/35.02 % (2698095)fmb+10_1_sil=256000:fmbss=7:random_seed=4058716914:fmbsr=1.6:i=182295_2725 on theBenchmark for (2725ds/182295Mi) % 245.80/35.02 % (2698095)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 245.80/35.02 % (2698095)Terminated due to inappropriate strategy. % 245.80/35.02 % (2698095)------------------------------ % 245.80/35.02 % (2698095)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 245.80/35.02 % (2698095)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 245.80/35.02 % (2698095)CaDiCaL version: 2.1.3 % 245.80/35.02 % (2698095)Termination reason: Inappropriate % 245.80/35.02 % (2698095)Time elapsed: 0.005 s % 245.80/35.02 % (2698095)Peak memory usage: 10 MB % 245.80/35.02 % (2698095)Instructions burned: 4 (million) % 245.80/35.02 % (2698095)------------------------------ % 245.80/35.02 % (2698095)------------------------------ % 245.80/35.02 % (2698099)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=820160718:i=44625:gsp=on_2725 on theBenchmark for (2725ds/44625Mi) % 259.52/36.98 % (2698099)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 259.52/36.98 % (2698099)Terminated due to inappropriate strategy. % 259.52/36.98 % (2698099)------------------------------ % 259.52/36.98 % (2698099)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 259.52/36.98 % (2698099)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 259.52/36.98 % (2698099)CaDiCaL version: 2.1.3 % 259.52/36.98 % (2698099)Termination reason: Inappropriate % 259.52/36.98 % (2698099)Time elapsed: 0.003 s % 259.52/36.98 % (2698099)Peak memory usage: 11 MB % 259.52/36.98 % (2698099)Instructions burned: 5 (million) % 259.52/36.98 % (2698099)------------------------------ % 259.52/36.98 % (2698099)------------------------------ % 259.52/36.98 % (2698101)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=823735243:i=160505_2725 on theBenchmark for (2725ds/160505Mi) % 259.52/36.98 % (2698101)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 259.52/36.98 % (2698101)Terminated due to inappropriate strategy. % 259.52/36.98 % (2698101)------------------------------ % 259.52/36.98 % (2698101)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 259.52/36.98 % (2698101)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 259.52/36.98 % (2698101)CaDiCaL version: 2.1.3 % 259.52/36.98 % (2698101)Termination reason: Inappropriate % 259.52/36.98 % (2698101)Time elapsed: 0.004 s % 259.52/36.98 % (2698101)Peak memory usage: 10 MB % 259.52/36.98 % (2698101)Instructions burned: 4 (million) % 259.52/36.98 % (2698101)------------------------------ % 259.52/36.98 % (2698101)------------------------------ % 259.52/36.98 % (2698103)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=3068891635:fmbsr=1.3:i=225729_2724 on theBenchmark for (2724ds/225729Mi) % 259.52/36.98 % (2698103)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 259.52/36.98 % (2698103)Terminated due to inappropriate strategy. % 259.52/36.98 % (2698103)------------------------------ % 259.52/36.98 % (2698103)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 259.52/36.98 % (2698103)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 259.52/36.98 % (2698103)CaDiCaL version: 2.1.3 % 259.52/36.98 % (2698103)Termination reason: Inappropriate % 259.52/36.98 % (2698103)Time elapsed: 0.003 s % 259.52/36.98 % (2698103)Peak memory usage: 11 MB % 259.52/36.98 % (2698103)Instructions burned: 4 (million) % 259.52/36.98 % (2698103)------------------------------ % 259.52/36.98 % (2698103)------------------------------ % 259.52/36.98 % (2698105)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=552435154:fmbsr=2:i=185024:ins=7_2724 on theBenchmark for (2724ds/185024Mi) % 259.52/36.98 % (2698105)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 259.52/36.98 % (2698105)Terminated due to inappropriate strategy. % 259.52/36.98 % (2698105)------------------------------ % 259.52/36.98 % (2698105)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 259.52/36.98 % (2698105)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 259.52/36.98 % (2698105)CaDiCaL version: 2.1.3 % 259.52/36.98 % (2698105)Termination reason: Inappropriate % 259.52/36.98 % (2698105)Time elapsed: 0.001 s % 259.52/36.98 % (2698105)Peak memory usage: 11 MB % 259.52/36.98 % (2698105)Instructions burned: 4 (million) % 259.52/36.98 % (2698105)------------------------------ % 259.52/36.98 % (2698105)------------------------------ % 259.52/36.98 % (2698107)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=2403965784:rtra=on_2724 on theBenchmark for (2724ds/0Mi) % 259.52/36.98 % (2698107)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 259.52/36.98 % (2698107)Terminated due to inappropriate strategy. % 259.52/36.98 % (2698107)------------------------------ % 259.52/36.98 % (2698107)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 259.52/36.98 % (2698107)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 259.52/36.98 % (2698107)CaDiCaL version: 2.1.3 % 259.52/36.98 % (2698107)Termination reason: Inappropriate % 259.52/36.98 % (2698107)Time elapsed: 0.002 s % 259.52/36.98 % (2698107)Peak memory usage: 11 MB % 259.52/36.98 % (2698107)Instructions burned: 6 (million) % 259.52/36.98 % (2698107)------------------------------ % 259.52/36.98 % (2698107)------------------------------ % 259.52/36.98 % (2698109)% WARNING: option uhcvi not known. % 259.52/36.98 % (2698109)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=93283717:i=271062:add=off:rtra=on:rawr=on_2724 on theBenchmark for (2724ds/271062Mi) % 284.26/40.35 % (2698071)Instruction limit reached! % 284.26/40.35 % (2698071)------------------------------ % 284.26/40.35 % (2698071)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 284.26/40.35 % (2698071)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 284.26/40.35 % (2698071)CaDiCaL version: 2.1.3 % 284.26/40.35 % (2698071)Termination reason: Instruction limit % 284.26/40.35 % (2698071)Termination phase: Saturation % 284.26/40.35 % (2698071)Time elapsed: 13.183 s % 284.26/40.35 % (2698071)Peak memory usage: 72 MB % 284.26/40.35 % (2698071)Instructions burned: 14135 (million) % 284.26/40.35 % (2698264)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3470321050:i=176048:add=on:rtra=on:rawr=on_2702 on theBenchmark for (2702ds/176048Mi) % 284.26/40.35 % (2698079)Instruction limit reached! % 284.26/40.35 % (2698079)------------------------------ % 284.26/40.35 % (2698079)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 284.26/40.35 % (2698079)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 284.26/40.35 % (2698079)CaDiCaL version: 2.1.3 % 284.26/40.35 % (2698079)Termination reason: Instruction limit % 284.26/40.35 % (2698079)Termination phase: Saturation % 284.26/40.35 % (2698079)Time elapsed: 11.611 s % 284.26/40.35 % (2698079)Peak memory usage: 166 MB % 284.26/40.35 % (2698079)Instructions burned: 17628 (million) % 284.26/40.35 % (2698267)dis+10_1_sil=32000:si=on:sp=arity:random_seed=1534725003:i=206:fgj=on:rtra=on_2660 on theBenchmark for (2660ds/206Mi) % 284.26/40.35 % (2698267)Instruction limit reached! % 284.26/40.35 % (2698267)------------------------------ % 284.26/40.35 % (2698267)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 284.26/40.35 % (2698267)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 284.26/40.35 % (2698267)CaDiCaL version: 2.1.3 % 284.26/40.35 % (2698267)Termination reason: Instruction limit % 284.26/40.35 % (2698267)Termination phase: Saturation % 284.26/40.35 % (2698267)Time elapsed: 0.133 s % 284.26/40.35 % (2698267)Peak memory usage: 14 MB % 284.26/40.35 % (2698267)Instructions burned: 208 (million) % 284.26/40.35 % (2698269)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=3897416260:i=232:rtra=on_2658 on theBenchmark for (2658ds/232Mi) % 284.26/40.35 % (2698269)Instruction limit reached! % 284.26/40.35 % (2698269)------------------------------ % 284.26/40.35 % (2698269)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 284.26/40.35 % (2698269)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 284.26/40.35 % (2698269)CaDiCaL version: 2.1.3 % 284.26/40.35 % (2698269)Termination reason: Instruction limit % 284.26/40.35 % (2698269)Termination phase: Saturation % 284.26/40.35 % (2698269)Time elapsed: 0.141 s % 284.26/40.35 % (2698269)Peak memory usage: 14 MB % 284.26/40.35 % (2698269)Instructions burned: 232 (million) % 284.26/40.35 % (2698271)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=3380761171:i=262:rtra=on_2657 on theBenchmark for (2657ds/262Mi) % 284.26/40.35 % (2698271)Instruction limit reached! % 284.26/40.35 % (2698271)------------------------------ % 284.26/40.35 % (2698271)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 284.26/40.35 % (2698271)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 284.26/40.35 % (2698271)CaDiCaL version: 2.1.3 % 284.26/40.35 % (2698271)Termination reason: Instruction limit % 284.26/40.35 % (2698271)Termination phase: Saturation % 284.26/40.35 % (2698271)Time elapsed: 0.156 s % 284.26/40.35 % (2698271)Peak memory usage: 14 MB % 284.26/40.35 % (2698271)Instructions burned: 264 (million) % 284.26/40.35 % (2698273)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=1364089870:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2655 on theBenchmark for (2655ds/318Mi) % 284.26/40.35 % (2698273)Instruction limit reached! % 284.26/40.35 % (2698273)------------------------------ % 284.26/40.35 % (2698273)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 284.26/40.35 % (2698273)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 284.26/40.35 % (2698273)CaDiCaL version: 2.1.3 % 284.26/40.35 % (2698273)Termination reason: Instruction limit % 284.26/40.35 % (2698273)Termination phase: Saturation % 284.26/40.35 % (2698273)Time elapsed: 0.219 s % 284.26/40.35 % (2698273)Peak memory usage: 16 MB % 284.26/40.35 % (2698273)Instructions burned: 318 (million) % 284.26/40.35 % (2698275)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=1023303037:i=1428:nm=2:rtra=on_2653 on theBenchmark for (2653ds/1428Mi) % 296.58/42.10 % (2698275)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 296.58/42.10 % (2698275)Terminated due to inappropriate strategy. % 296.58/42.10 % (2698275)------------------------------ % 296.58/42.10 % (2698275)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 296.58/42.10 % (2698275)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 296.58/42.10 % (2698275)CaDiCaL version: 2.1.3 % 296.58/42.10 % (2698275)Termination reason: Inappropriate % 296.58/42.10 % (2698275)Time elapsed: 0.003 s % 296.58/42.10 % (2698275)Peak memory usage: 10 MB % 296.58/42.10 % (2698275)Instructions burned: 5 (million) % 296.58/42.10 % (2698275)------------------------------ % 296.58/42.10 % (2698275)------------------------------ % 296.58/42.10 % (2698277)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=3009527789:i=262:bd=preordered:rtra=on:fsd=on_2652 on theBenchmark for (2652ds/262Mi) % 296.58/42.10 % (2698277)Instruction limit reached! % 296.58/42.10 % (2698277)------------------------------ % 296.58/42.10 % (2698277)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 296.58/42.10 % (2698277)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 296.58/42.10 % (2698277)CaDiCaL version: 2.1.3 % 296.58/42.10 % (2698277)Termination reason: Instruction limit % 296.58/42.10 % (2698277)Termination phase: Saturation % 296.58/42.10 % (2698277)Time elapsed: 0.150 s % 296.58/42.10 % (2698277)Peak memory usage: 13 MB % 296.58/42.10 % (2698277)Instructions burned: 262 (million) % 296.58/42.10 % (2698279)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=2581289417:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2651 on theBenchmark for (2651ds/1368Mi) % 296.58/42.10 % (2698279)Instruction limit reached! % 296.58/42.10 % (2698279)------------------------------ % 296.58/42.10 % (2698279)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 296.58/42.10 % (2698279)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 296.58/42.10 % (2698279)CaDiCaL version: 2.1.3 % 296.58/42.10 % (2698279)Termination reason: Instruction limit % 296.58/42.10 % (2698279)Termination phase: Saturation % 296.58/42.10 % (2698279)Time elapsed: 0.882 s % 296.58/42.10 % (2698279)Peak memory usage: 24 MB % 296.58/42.10 % (2698279)Instructions burned: 1368 (million) % 296.58/42.10 % (2698281)ott-21_1_sil=16000:si=on:fs=off:random_seed=116558256:i=360:av=off:fsr=off:rtra=on_2642 on theBenchmark for (2642ds/360Mi) % 296.58/42.10 % (2698281)Instruction limit reached! % 296.58/42.10 % (2698281)------------------------------ % 296.58/42.10 % (2698281)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 296.58/42.10 % (2698281)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 296.58/42.10 % (2698281)CaDiCaL version: 2.1.3 % 296.58/42.10 % (2698281)Termination reason: Instruction limit % 296.58/42.10 % (2698281)Termination phase: Saturation % 296.58/42.10 % (2698281)Time elapsed: 0.162 s % 296.58/42.10 % (2698281)Peak memory usage: 13 MB % 296.58/42.10 % (2698281)Instructions burned: 360 (million) % 296.58/42.10 % (2698283)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2207050622:i=954:bd=all:rtra=on_2640 on theBenchmark for (2640ds/954Mi) % 296.58/42.10 % (2698283)Instruction limit reached! % 296.58/42.10 % (2698283)------------------------------ % 296.58/42.10 % (2698283)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 296.58/42.10 % (2698283)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 296.58/42.10 % (2698283)CaDiCaL version: 2.1.3 % 296.58/42.10 % (2698283)Termination reason: Instruction limit % 296.58/42.10 % (2698283)Termination phase: Saturation % 296.58/42.10 % (2698283)Time elapsed: 0.651 s % 296.58/42.10 % (2698283)Peak memory usage: 17 MB % 296.58/42.10 % (2698283)Instructions burned: 954 (million) % 296.58/42.10 % (2698285)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=2618448116:fmbsr=1.3:i=1730:ins=25:rtra=on_2633 on theBenchmark for (2633ds/1730Mi) % 296.58/42.10 % (2698285)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 296.58/42.10 % (2698285)Terminated due to inappropriate strategy. % 296.58/42.10 % (2698285)------------------------------ % 296.58/42.10 % (2698285)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 296.58/42.10 % (2698285)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 296.58/42.10 % (2698285)CaDiCaL version: 2.1.3 % 296.58/42.10 % (2698285)Termination reason: Inappropriate % 296.58/42.10 % (2698285)Time elapsed: 0.002 s % 300.11/42.63 % (2698285)Peak memory usage: 10 MB % 300.11/42.63 % (2698285)Instructions burned: 4 (million) % 300.11/42.63 % (2698285)------------------------------ % 300.11/42.63 % (2698285)------------------------------ % 300.11/42.63 % (2698287)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=944798266:i=2358:rtra=on_2633 on theBenchmark for (2633ds/2358Mi) % 300.11/42.63 % (2698287)Instruction limit reached! % 300.11/42.63 % (2698287)------------------------------ % 300.11/42.63 % (2698287)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.11/42.63 % (2698287)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.11/42.63 % (2698287)CaDiCaL version: 2.1.3 % 300.11/42.63 % (2698287)Termination reason: Instruction limit % 300.11/42.63 % (2698287)Termination phase: Saturation % 300.11/42.63 % (2698287)Time elapsed: 1.375 s % 300.11/42.63 % (2698287)Peak memory usage: 23 MB % 300.11/42.63 % (2698287)Instructions burned: 2361 (million) % 300.11/42.63 % (2698289)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=1716202906:i=1778:ins=1:rtra=on_2619 on theBenchmark for (2619ds/1778Mi) % 300.11/42.63 % (2698289)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 300.11/42.63 % (2698289)Terminated due to inappropriate strategy. % 300.11/42.63 % (2698289)------------------------------ % 300.11/42.63 % (2698289)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.11/42.63 % (2698289)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.11/42.63 % (2698289)CaDiCaL version: 2.1.3 % 300.11/42.63 % (2698289)Termination reason: Inappropriate % 300.11/42.63 % (2698289)Time elapsed: 0.003 s % 300.11/42.63 % (2698289)Peak memory usage: 10 MB % 300.11/42.63 % (2698289)Instructions burned: 4 (million) % 300.11/42.63 % (2698289)------------------------------ % 300.11/42.63 % (2698289)------------------------------ % 300.11/42.63 % (2698291)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=152441098:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2618 on theBenchmark for (2618ds/1384Mi) % 300.11/42.63 % (2698291)Instruction limit reached! % 300.11/42.63 % (2698291)------------------------------ % 300.11/42.63 % (2698291)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.11/42.63 % (2698291)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.11/42.63 % (2698291)CaDiCaL version: 2.1.3 % 300.11/42.63 % (2698291)Termination reason: Instruction limit % 300.11/42.63 % (2698291)Termination phase: Saturation % 300.11/42.63 % (2698291)Time elapsed: 0.856 s % 300.11/42.63 % (2698291)Peak memory usage: 22 MB % 300.11/42.63 % (2698291)Instructions burned: 1384 (million) % 300.11/42.63 % (2698293)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=2937164156:i=1758:kws=inv_precedence:fsr=off:rtra=on_2610 on theBenchmark for (2610ds/1758Mi) % 300.11/42.63 % (2698293)Instruction limit reached! % 300.11/42.63 % (2698293)------------------------------ % 300.11/42.63 % (2698293)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.11/42.63 % (2698293)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.11/42.63 % (2698293)CaDiCaL version: 2.1.3 % 300.11/42.63 % (2698293)Termination reason: Instruction limit % 300.11/42.63 % (2698293)Termination phase: Saturation % 300.11/42.63 % (2698293)Time elapsed: 0.992 s % 300.11/42.63 % (2698293)Peak memory usage: 25 MB % 300.11/42.63 % (2698293)Instructions burned: 1761 (million) % 300.11/42.63 % (2698295)fmb+10_1_sil=64000:si=on:random_seed=4083244174:i=44122:nm=2:rtra=on:gsp=on_2600 on theBenchmark for (2600ds/44122Mi) % 300.11/42.63 % (2698295)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 300.11/42.63 % (2698295)Terminated due to inappropriate strategy. % 300.11/42.63 % (2698295)------------------------------ % 300.11/42.63 % (2698295)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.11/42.63 % (2698295)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.11/42.63 % (2698295)CaDiCaL version: 2.1.3 % 300.11/42.63 % (2698295)Termination reason: Inappropriate % 300.11/42.63 % (2698295)Time elapsed: 0.003 s % 300.11/42.63 % (2698295)Peak memory usage: 10 MB % 300.11/42.63 % (2698295)Instructions burned: 5 (million) % 300.11/42.63 % (2698295)------------------------------ % 300.11/42.63 % (2698295)------------------------------ % 300.11/42.63 % (2698297)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=2291875870:i=19030:nm=5:rtra=on_2599 on theBenchmark for ( % 300.11/42.63 Terminated % 300.11/42.63 % Vampire exiting %------------------------------------------------------------------------------