%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWX131_1 : TPTP v9.3.1. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % Computer : n001.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:32 PM UTC 2026 % Result : Timeout 300.48s 42.63s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWX131_1 : TPTP v9.3.1. Released v9.3.0. % 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.10/0.19 % Computer : n001.cluster.edu % 0.10/0.19 % Model : x86_64 x86_64 % 0.10/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.19 % Memory : 8046.5625MB % 0.10/0.19 % OS : Linux 6.8.0-71-generic % 0.10/0.19 % CPULimit : 300 % 0.10/0.19 % WCLimit : 300 % 0.10/0.19 % DateTime : Mon Sep 28 15:09:03 UTC 2026 % 0.10/0.19 % CPUTime : % 0.10/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.10/0.22 Running first-order model finding % 0.10/0.22 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 2.64/0.67 % (414875)Will run a generic schedule for satisfiability detection. % 2.64/0.67 % (414885)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2989803342:i=131_2999 on theBenchmark for (2999ds/131Mi) % 2.64/0.67 % (414881)% WARNING: option uhcvi not known. % 2.64/0.67 % (414880)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2538533047_2999 on theBenchmark for (2999ds/0Mi) % 2.64/0.67 % (414881)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2161325366:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 2.64/0.67 % (414882)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1788786144:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 2.64/0.67 % (414883)dis+10_1_sil=32000:sp=arity:random_seed=801968235:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 2.64/0.67 % (414884)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3373637449:i=116_2999 on theBenchmark for (2999ds/116Mi) % 2.64/0.67 % (414886)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3697375639:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 2.64/0.67 % (414880)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 2.64/0.67 % (414880)Terminated due to inappropriate strategy. % 2.64/0.67 % (414880)------------------------------ % 2.64/0.67 % (414880)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 2.64/0.67 % (414880)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 2.64/0.67 % (414880)CaDiCaL version: 2.1.3 % 2.64/0.67 % (414880)Termination reason: Inappropriate % 2.64/0.67 % (414880)Time elapsed: 0.013 s % 2.64/0.67 % (414880)Peak memory usage: 10 MB % 2.64/0.67 % (414880)Instructions burned: 31 (million) % 2.64/0.67 % (414880)------------------------------ % 2.64/0.67 % (414880)------------------------------ % 2.64/0.67 % (414885)Instruction limit reached! % 2.64/0.67 % (414885)------------------------------ % 2.64/0.67 % (414885)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 2.64/0.67 % (414885)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 2.64/0.67 % (414885)CaDiCaL version: 2.1.3 % 2.64/0.67 % (414885)Termination reason: Instruction limit % 2.64/0.67 % (414885)Termination phase: Saturation % 2.64/0.67 % (414885)Time elapsed: 0.032 s % 2.64/0.67 % (414885)Peak memory usage: 13 MB % 2.64/0.67 % (414885)Instructions burned: 136 (million) % 2.64/0.67 % (414894)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2200919585:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 2.64/0.67 % (414895)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3617004320:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 2.64/0.67 % (414883)Instruction limit reached! % 2.64/0.67 % (414883)------------------------------ % 2.64/0.67 % (414883)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 2.64/0.67 % (414883)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 2.64/0.67 % (414883)CaDiCaL version: 2.1.3 % 2.64/0.67 % (414883)Termination reason: Instruction limit % 2.64/0.67 % (414883)Termination phase: Saturation % 2.64/0.67 % (414883)Time elapsed: 0.045 s % 2.64/0.67 % (414883)Peak memory usage: 12 MB % 2.64/0.67 % (414883)Instructions burned: 105 (million) % 2.64/0.67 % (414894)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 2.64/0.67 % (414894)Terminated due to inappropriate strategy. % 2.64/0.67 % (414894)------------------------------ % 2.64/0.67 % (414894)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 2.64/0.67 % (414894)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 2.64/0.67 % (414894)CaDiCaL version: 2.1.3 % 2.64/0.67 % (414894)Termination reason: Inappropriate % 2.64/0.67 % (414894)Time elapsed: 0.013 s % 2.64/0.67 % (414894)Peak memory usage: 10 MB % 2.64/0.67 % (414894)Instructions burned: 31 (million) % 2.64/0.67 % (414894)------------------------------ % 2.64/0.67 % (414894)------------------------------ % 2.64/0.67 % (414884)Instruction limit reached! % 2.64/0.67 % (414884)------------------------------ % 2.64/0.67 % (414884)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 2.64/0.67 % (414884)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 2.64/0.67 % (414884)CaDiCaL version: 2.1.3 % 2.64/0.67 % (414884)Termination reason: Instruction limit % 2.64/0.67 % (414884)Termination phase: Saturation % 5.48/1.11 % (414884)Time elapsed: 0.052 s % 5.48/1.11 % (414884)Peak memory usage: 13 MB % 5.48/1.11 % (414884)Instructions burned: 117 (million) % 5.48/1.11 % (414895)Instruction limit reached! % 5.48/1.11 % (414895)------------------------------ % 5.48/1.11 % (414895)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.48/1.11 % (414895)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.48/1.11 % (414895)CaDiCaL version: 2.1.3 % 5.48/1.11 % (414895)Termination reason: Instruction limit % 5.48/1.11 % (414895)Termination phase: Saturation % 5.48/1.11 % (414895)Time elapsed: 0.031 s % 5.48/1.11 % (414895)Peak memory usage: 14 MB % 5.48/1.11 % (414895)Instructions burned: 136 (million) % 5.48/1.11 % (414898)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=1775053236:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi) % 5.48/1.11 % (414899)ott-21_1_sil=16000:fs=off:random_seed=3507566298:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 5.48/1.11 % (414900)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2016252446:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 5.48/1.11 % (414902)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1847856710:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 5.48/1.11 % (414886)Instruction limit reached! % 5.48/1.11 % (414886)------------------------------ % 5.48/1.11 % (414886)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.48/1.11 % (414886)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.48/1.11 % (414886)CaDiCaL version: 2.1.3 % 5.48/1.11 % (414886)Termination reason: Instruction limit % 5.48/1.11 % (414886)Termination phase: Saturation % 5.48/1.11 % (414886)Time elapsed: 0.079 s % 5.48/1.11 % (414886)Peak memory usage: 14 MB % 5.48/1.11 % (414886)Instructions burned: 160 (million) % 5.48/1.11 % (414902)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 5.48/1.11 % (414902)Terminated due to inappropriate strategy. % 5.48/1.11 % (414902)------------------------------ % 5.48/1.11 % (414902)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.48/1.11 % (414902)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.48/1.11 % (414902)CaDiCaL version: 2.1.3 % 5.48/1.11 % (414902)Termination reason: Inappropriate % 5.48/1.11 % (414902)Time elapsed: 0.005 s % 5.48/1.11 % (414902)Peak memory usage: 10 MB % 5.48/1.11 % (414902)Instructions burned: 23 (million) % 5.48/1.11 % (414902)------------------------------ % 5.48/1.11 % (414902)------------------------------ % 5.48/1.11 % (414907)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3451987551:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi) % 5.48/1.11 % (414907)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 5.48/1.11 % (414907)Terminated due to inappropriate strategy. % 5.48/1.11 % (414907)------------------------------ % 5.48/1.11 % (414907)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.48/1.11 % (414907)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.48/1.11 % (414907)CaDiCaL version: 2.1.3 % 5.48/1.11 % (414907)Termination reason: Inappropriate % 5.48/1.11 % (414907)Time elapsed: 0.005 s % 5.48/1.11 % (414907)Peak memory usage: 10 MB % 5.48/1.11 % (414907)Instructions burned: 23 (million) % 5.48/1.11 % (414907)------------------------------ % 5.48/1.11 % (414907)------------------------------ % 5.48/1.11 % (414906)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3325114750:i=1179_2998 on theBenchmark for (2998ds/1179Mi) % 5.48/1.11 % (414910)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=2711091626:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2998 on theBenchmark for (2998ds/692Mi) % 5.48/1.11 % (414899)Instruction limit reached! % 5.48/1.11 % (414899)------------------------------ % 5.48/1.11 % (414899)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.48/1.11 % (414899)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.48/1.11 % (414899)CaDiCaL version: 2.1.3 % 5.48/1.11 % (414899)Termination reason: Instruction limit % 5.48/1.11 % (414899)Termination phase: Saturation % 5.48/1.11 % (414899)Time elapsed: 0.078 s % 5.48/1.11 % (414899)Peak memory usage: 13 MB % 5.48/1.11 % (414899)Instructions burned: 182 (million) % 15.45/2.56 % (414912)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2325312234:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi) % 15.45/2.56 % (414900)Instruction limit reached! % 15.45/2.56 % (414900)------------------------------ % 15.45/2.56 % (414900)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 15.45/2.56 % (414900)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.45/2.56 % (414900)CaDiCaL version: 2.1.3 % 15.45/2.56 % (414900)Termination reason: Instruction limit % 15.45/2.56 % (414900)Termination phase: Saturation % 15.45/2.56 % (414900)Time elapsed: 0.187 s % 15.45/2.56 % (414900)Peak memory usage: 13 MB % 15.45/2.56 % (414900)Instructions burned: 477 (million) % 15.45/2.56 % (414910)Instruction limit reached! % 15.45/2.56 % (414910)------------------------------ % 15.45/2.56 % (414910)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 15.45/2.56 % (414910)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.45/2.56 % (414910)CaDiCaL version: 2.1.3 % 15.45/2.56 % (414910)Termination reason: Instruction limit % 15.45/2.56 % (414910)Termination phase: Saturation % 15.45/2.56 % (414910)Time elapsed: 0.159 s % 15.45/2.56 % (414910)Peak memory usage: 15 MB % 15.45/2.56 % (414910)Instructions burned: 696 (million) % 15.45/2.56 % (414914)fmb+10_1_sil=64000:random_seed=2974827794:i=22061:nm=2:gsp=on_2996 on theBenchmark for (2996ds/22061Mi) % 15.45/2.56 % (414915)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2128059500:i=9515:nm=5_2996 on theBenchmark for (2996ds/9515Mi) % 15.45/2.56 % (414914)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 15.45/2.56 % (414914)Terminated due to inappropriate strategy. % 15.45/2.56 % (414914)------------------------------ % 15.45/2.56 % (414914)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 15.45/2.56 % (414914)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.45/2.56 % (414914)CaDiCaL version: 2.1.3 % 15.45/2.56 % (414914)Termination reason: Inappropriate % 15.45/2.56 % (414914)Time elapsed: 0.013 s % 15.45/2.56 % (414914)Peak memory usage: 11 MB % 15.45/2.56 % (414914)Instructions burned: 31 (million) % 15.45/2.56 % (414914)------------------------------ % 15.45/2.56 % (414914)------------------------------ % 15.45/2.56 % (414915)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 15.45/2.56 % (414915)Terminated due to inappropriate strategy. % 15.45/2.56 % (414915)------------------------------ % 15.45/2.56 % (414915)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 15.45/2.56 % (414915)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.45/2.56 % (414915)CaDiCaL version: 2.1.3 % 15.45/2.56 % (414915)Termination reason: Inappropriate % 15.45/2.56 % (414915)Time elapsed: 0.006 s % 15.45/2.56 % (414915)Peak memory usage: 10 MB % 15.45/2.56 % (414915)Instructions burned: 31 (million) % 15.45/2.56 % (414915)------------------------------ % 15.45/2.56 % (414915)------------------------------ % 15.45/2.56 % (414919)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2686977399:i=5131_2996 on theBenchmark for (2996ds/5131Mi) % 15.45/2.56 % (414918)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=4009574732:fmbsr=1.7:i=920_2996 on theBenchmark for (2996ds/920Mi) % 15.45/2.56 % (414918)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 15.45/2.56 % (414918)Terminated due to inappropriate strategy. % 15.45/2.56 % (414918)------------------------------ % 15.45/2.56 % (414918)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 15.45/2.56 % (414918)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.45/2.56 % (414918)CaDiCaL version: 2.1.3 % 15.45/2.56 % (414918)Termination reason: Inappropriate % 15.45/2.56 % (414918)Time elapsed: 0.012 s % 15.45/2.56 % (414918)Peak memory usage: 11 MB % 15.45/2.56 % (414918)Instructions burned: 31 (million) % 15.45/2.56 % (414918)------------------------------ % 15.45/2.56 % (414918)------------------------------ % 15.45/2.56 % (414922)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3761190978:i=1472:ins=7:fdi=8:gsp=on_2996 on theBenchmark for (2996ds/1472Mi) % 15.45/2.56 % (414898)Instruction limit reached! % 15.45/2.56 % (414898)------------------------------ % 15.45/2.56 % (414898)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 15.45/2.56 % (414898)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.66/3.11 % (414898)CaDiCaL version: 2.1.3 % 19.66/3.11 % (414898)Termination reason: Instruction limit % 19.66/3.11 % (414898)Termination phase: Saturation % 19.66/3.11 % (414898)Time elapsed: 0.312 s % 19.66/3.11 % (414898)Peak memory usage: 17 MB % 19.66/3.11 % (414898)Instructions burned: 685 (million) % 19.66/3.11 % (414924)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=1319848634:i=6324_2995 on theBenchmark for (2995ds/6324Mi) % 19.66/3.11 % (414924)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 19.66/3.11 % (414924)Terminated due to inappropriate strategy. % 19.66/3.11 % (414924)------------------------------ % 19.66/3.11 % (414924)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 19.66/3.11 % (414924)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.66/3.11 % (414924)CaDiCaL version: 2.1.3 % 19.66/3.11 % (414924)Termination reason: Inappropriate % 19.66/3.11 % (414924)Time elapsed: 0.013 s % 19.66/3.11 % (414924)Peak memory usage: 10 MB % 19.66/3.11 % (414924)Instructions burned: 31 (million) % 19.66/3.11 % (414924)------------------------------ % 19.66/3.11 % (414924)------------------------------ % 19.66/3.11 % (414926)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=2764245233:fmbsr=2.30978:i=2174_2995 on theBenchmark for (2995ds/2174Mi) % 19.66/3.11 % (414926)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 19.66/3.11 % (414926)Terminated due to inappropriate strategy. % 19.66/3.11 % (414926)------------------------------ % 19.66/3.11 % (414926)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 19.66/3.11 % (414926)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.66/3.11 % (414926)CaDiCaL version: 2.1.3 % 19.66/3.11 % (414926)Termination reason: Inappropriate % 19.66/3.11 % (414926)Time elapsed: 0.012 s % 19.66/3.11 % (414926)Peak memory usage: 10 MB % 19.66/3.11 % (414926)Instructions burned: 31 (million) % 19.66/3.11 % (414926)------------------------------ % 19.66/3.11 % (414926)------------------------------ % 19.66/3.11 % (414928)ott-2_1_sil=16000:newcnf=on:random_seed=2460785554:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2994 on theBenchmark for (2994ds/869Mi) % 19.66/3.11 % (414912)Instruction limit reached! % 19.66/3.11 % (414912)------------------------------ % 19.66/3.11 % (414912)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 19.66/3.11 % (414912)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.66/3.11 % (414912)CaDiCaL version: 2.1.3 % 19.66/3.11 % (414912)Termination reason: Instruction limit % 19.66/3.11 % (414912)Termination phase: Saturation % 19.66/3.11 % (414912)Time elapsed: 0.340 s % 19.66/3.11 % (414912)Peak memory usage: 14 MB % 19.66/3.11 % (414912)Instructions burned: 879 (million) % 19.66/3.11 % (414930)ott+10_1_sil=32000:tgt=ground:random_seed=1979104713:i=5114:av=off_2994 on theBenchmark for (2994ds/5114Mi) % 19.66/3.11 % (414906)Instruction limit reached! % 19.66/3.11 % (414906)------------------------------ % 19.66/3.11 % (414906)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 19.66/3.11 % (414906)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.66/3.11 % (414906)CaDiCaL version: 2.1.3 % 19.66/3.11 % (414906)Termination reason: Instruction limit % 19.66/3.11 % (414906)Termination phase: Saturation % 19.66/3.11 % (414906)Time elapsed: 0.455 s % 19.66/3.11 % (414906)Peak memory usage: 14 MB % 19.66/3.11 % (414906)Instructions burned: 1179 (million) % 19.66/3.11 % (414932)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=108829721:i=54282_2993 on theBenchmark for (2993ds/54282Mi) % 19.66/3.11 % (414932)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 19.66/3.11 % (414932)Terminated due to inappropriate strategy. % 19.66/3.11 % (414932)------------------------------ % 19.66/3.11 % (414932)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 19.66/3.11 % (414932)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.66/3.11 % (414932)CaDiCaL version: 2.1.3 % 19.66/3.11 % (414932)Termination reason: Inappropriate % 19.66/3.11 % (414932)Time elapsed: 0.013 s % 19.66/3.11 % (414932)Peak memory usage: 10 MB % 19.66/3.11 % (414932)Instructions burned: 31 (million) % 19.66/3.11 % (414932)------------------------------ % 19.66/3.11 % (414932)------------------------------ % 19.66/3.11 % (414934)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=1020734446:i=3512:aac=none_2993 on theBenchmark for (2993ds/3512Mi) % 19.66/3.11 % (414928)Instruction limit reached! % 74.09/10.79 % (414928)------------------------------ % 74.09/10.79 % (414928)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 74.09/10.79 % (414928)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 74.09/10.79 % (414928)CaDiCaL version: 2.1.3 % 74.09/10.79 % (414928)Termination reason: Instruction limit % 74.09/10.79 % (414928)Termination phase: Saturation % 74.09/10.79 % (414928)Time elapsed: 0.354 s % 74.09/10.79 % (414928)Peak memory usage: 15 MB % 74.09/10.79 % (414928)Instructions burned: 871 (million) % 74.09/10.79 % (414936)dis+21_1_sil=32000:sas=cadical:random_seed=897023023:i=3773:amm=off_2991 on theBenchmark for (2991ds/3773Mi) % 74.09/10.79 % (414922)Instruction limit reached! % 74.09/10.79 % (414922)------------------------------ % 74.09/10.79 % (414922)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 74.09/10.79 % (414922)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 74.09/10.79 % (414922)CaDiCaL version: 2.1.3 % 74.09/10.79 % (414922)Termination reason: Instruction limit % 74.09/10.79 % (414922)Termination phase: Saturation % 74.09/10.79 % (414922)Time elapsed: 0.751 s % 74.09/10.79 % (414922)Peak memory usage: 23 MB % 74.09/10.79 % (414922)Instructions burned: 1473 (million) % 74.09/10.79 % (414938)ott+11_1_sil=16000:gs=on:random_seed=1710330721:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2988 on theBenchmark for (2988ds/2251Mi) % 74.09/10.79 % (414919)Instruction limit reached! % 74.09/10.79 % (414919)------------------------------ % 74.09/10.79 % (414919)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 74.09/10.79 % (414919)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 74.09/10.79 % (414919)CaDiCaL version: 2.1.3 % 74.09/10.79 % (414919)Termination reason: Instruction limit % 74.09/10.79 % (414919)Termination phase: Saturation % 74.09/10.79 % (414919)Time elapsed: 1.071 s % 74.09/10.79 % (414919)Peak memory usage: 20 MB % 74.09/10.79 % (414919)Instructions burned: 5136 (million) % 74.09/10.79 % (414940)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=1910220354:fmbsr=1.6:i=67534_2985 on theBenchmark for (2985ds/67534Mi) % 74.09/10.79 % (414940)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 74.09/10.79 % (414940)Terminated due to inappropriate strategy. % 74.09/10.79 % (414940)------------------------------ % 74.09/10.79 % (414940)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 74.09/10.79 % (414940)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 74.09/10.79 % (414940)CaDiCaL version: 2.1.3 % 74.09/10.79 % (414940)Termination reason: Inappropriate % 74.09/10.79 % (414940)Time elapsed: 0.007 s % 74.09/10.79 % (414940)Peak memory usage: 10 MB % 74.09/10.79 % (414940)Instructions burned: 31 (million) % 74.09/10.79 % (414940)------------------------------ % 74.09/10.79 % (414940)------------------------------ % 74.09/10.79 % (414942)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=1644921837:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2985 on theBenchmark for (2985ds/4591Mi) % 74.09/10.79 % (414934)Instruction limit reached! % 74.09/10.79 % (414934)------------------------------ % 74.09/10.79 % (414934)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 74.09/10.79 % (414934)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 74.09/10.79 % (414934)CaDiCaL version: 2.1.3 % 74.09/10.79 % (414934)Termination reason: Instruction limit % 74.09/10.79 % (414934)Termination phase: Saturation % 74.09/10.79 % (414934)Time elapsed: 1.359 s % 74.09/10.79 % (414934)Peak memory usage: 17 MB % 74.09/10.79 % (414934)Instructions burned: 3515 (million) % 74.09/10.79 % (414938)Instruction limit reached! % 74.09/10.79 % (414938)------------------------------ % 74.09/10.79 % (414938)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 74.09/10.79 % (414938)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 74.09/10.79 % (414938)CaDiCaL version: 2.1.3 % 74.09/10.79 % (414938)Termination reason: Instruction limit % 74.09/10.79 % (414938)Termination phase: Saturation % 74.09/10.79 % (414938)Time elapsed: 0.861 s % 74.09/10.79 % (414938)Peak memory usage: 14 MB % 74.09/10.79 % (414938)Instructions burned: 2252 (million) % 74.09/10.79 % (414944)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=1013434791:i=29340_2979 on theBenchmark for (2979ds/29340Mi) % 74.09/10.79 % (414945)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=459398176:i=5211_2979 on theBenchmark for (2979ds/5211Mi) % 74.09/10.79 % (414936)Instruction limit reached! % 83.49/12.06 % (414936)------------------------------ % 83.49/12.06 % (414936)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 83.49/12.06 % (414936)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 83.49/12.06 % (414936)CaDiCaL version: 2.1.3 % 83.49/12.06 % (414936)Termination reason: Instruction limit % 83.49/12.06 % (414936)Termination phase: Saturation % 83.49/12.06 % (414936)Time elapsed: 1.430 s % 83.49/12.06 % (414936)Peak memory usage: 16 MB % 83.49/12.06 % (414936)Instructions burned: 3775 (million) % 83.49/12.06 % (414948)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=2991978152:i=5497:nm=2_2976 on theBenchmark for (2976ds/5497Mi) % 83.49/12.06 % (414948)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 83.49/12.06 % (414948)Terminated due to inappropriate strategy. % 83.49/12.06 % (414948)------------------------------ % 83.49/12.06 % (414948)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 83.49/12.06 % (414948)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 83.49/12.06 % (414948)CaDiCaL version: 2.1.3 % 83.49/12.06 % (414948)Termination reason: Inappropriate % 83.49/12.06 % (414948)Time elapsed: 0.013 s % 83.49/12.06 % (414948)Peak memory usage: 10 MB % 83.49/12.06 % (414948)Instructions burned: 31 (million) % 83.49/12.06 % (414948)------------------------------ % 83.49/12.06 % (414948)------------------------------ % 83.49/12.06 % (414950)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=3233868666:fmbsr=2:i=46332_2976 on theBenchmark for (2976ds/46332Mi) % 83.49/12.06 % (414950)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 83.49/12.06 % (414950)Terminated due to inappropriate strategy. % 83.49/12.06 % (414950)------------------------------ % 83.49/12.06 % (414950)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 83.49/12.06 % (414950)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 83.49/12.06 % (414950)CaDiCaL version: 2.1.3 % 83.49/12.06 % (414950)Termination reason: Inappropriate % 83.49/12.06 % (414950)Time elapsed: 0.013 s % 83.49/12.06 % (414950)Peak memory usage: 10 MB % 83.49/12.06 % (414950)Instructions burned: 31 (million) % 83.49/12.06 % (414950)------------------------------ % 83.49/12.06 % (414950)------------------------------ % 83.49/12.06 % (414952)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=1859522983:i=14071_2975 on theBenchmark for (2975ds/14071Mi) % 83.49/12.06 % (414952)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 83.49/12.06 % (414952)Terminated due to inappropriate strategy. % 83.49/12.06 % (414952)------------------------------ % 83.49/12.06 % (414952)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 83.49/12.06 % (414952)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 83.49/12.06 % (414952)CaDiCaL version: 2.1.3 % 83.49/12.06 % (414952)Termination reason: Inappropriate % 83.49/12.06 % (414952)Time elapsed: 0.013 s % 83.49/12.06 % (414952)Peak memory usage: 10 MB % 83.49/12.06 % (414952)Instructions burned: 31 (million) % 83.49/12.06 % (414952)------------------------------ % 83.49/12.06 % (414952)------------------------------ % 83.49/12.06 % (414954)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1066696690:i=22565:add=on:rawr=on_2975 on theBenchmark for (2975ds/22565Mi) % 83.49/12.06 % (414930)Instruction limit reached! % 83.49/12.06 % (414930)------------------------------ % 83.49/12.06 % (414930)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 83.49/12.06 % (414930)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 83.49/12.06 % (414930)CaDiCaL version: 2.1.3 % 83.49/12.06 % (414930)Termination reason: Instruction limit % 83.49/12.06 % (414930)Termination phase: Saturation % 83.49/12.06 % (414930)Time elapsed: 1.980 s % 83.49/12.06 % (414930)Peak memory usage: 14 MB % 83.49/12.06 % (414930)Instructions burned: 5116 (million) % 83.49/12.06 % (414956)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=2497080183:i=8173:av=off_2974 on theBenchmark for (2974ds/8173Mi) % 83.49/12.06 % (414942)Instruction limit reached! % 83.49/12.06 % (414942)------------------------------ % 83.49/12.06 % (414942)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 83.49/12.06 % (414942)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 83.49/12.06 % (414942)CaDiCaL version: 2.1.3 % 83.49/12.06 % (414942)Termination reason: Instruction limit % 83.49/12.06 % (414942)Termination phase: Saturation % 93.26/13.44 % (414942)Time elapsed: 1.399 s % 93.26/13.44 % (414942)Peak memory usage: 41 MB % 93.26/13.44 % (414942)Instructions burned: 4594 (million) % 93.26/13.44 % (414958)dis+10_16:1_sil=16000:random_seed=2867912451:i=9155:fsr=off_2971 on theBenchmark for (2971ds/9155Mi) % 93.26/13.44 % (414945)Instruction limit reached! % 93.26/13.44 % (414945)------------------------------ % 93.26/13.44 % (414945)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 93.26/13.44 % (414945)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 93.26/13.44 % (414945)CaDiCaL version: 2.1.3 % 93.26/13.44 % (414945)Termination reason: Instruction limit % 93.26/13.44 % (414945)Termination phase: Saturation % 93.26/13.44 % (414945)Time elapsed: 2.018 s % 93.26/13.44 % (414945)Peak memory usage: 22 MB % 93.26/13.44 % (414945)Instructions burned: 5213 (million) % 93.26/13.44 % (414960)ott-3_8_sil=64000:random_seed=4132882137:i=20139:bs=on_2959 on theBenchmark for (2959ds/20139Mi) % 93.26/13.44 % (414958)Instruction limit reached! % 93.26/13.44 % (414958)------------------------------ % 93.26/13.44 % (414958)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 93.26/13.44 % (414958)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 93.26/13.44 % (414958)CaDiCaL version: 2.1.3 % 93.26/13.44 % (414958)Termination reason: Instruction limit % 93.26/13.44 % (414958)Termination phase: Saturation % 93.26/13.44 % (414958)Time elapsed: 1.905 s % 93.26/13.44 % (414958)Peak memory usage: 18 MB % 93.26/13.44 % (414958)Instructions burned: 9159 (million) % 93.26/13.44 % (414962)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=1117865969:fmbsr=2:i=32576_2951 on theBenchmark for (2951ds/32576Mi) % 93.26/13.44 % (414962)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 93.26/13.44 % (414962)Terminated due to inappropriate strategy. % 93.26/13.44 % (414962)------------------------------ % 93.26/13.44 % (414962)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 93.26/13.44 % (414962)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 93.26/13.44 % (414962)CaDiCaL version: 2.1.3 % 93.26/13.44 % (414962)Termination reason: Inappropriate % 93.26/13.44 % (414962)Time elapsed: 0.007 s % 93.26/13.44 % (414962)Peak memory usage: 10 MB % 93.26/13.44 % (414962)Instructions burned: 31 (million) % 93.26/13.44 % (414962)------------------------------ % 93.26/13.44 % (414962)------------------------------ % 93.26/13.44 % (414964)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=1380612970:i=11404_2951 on theBenchmark for (2951ds/11404Mi) % 93.26/13.44 % (414956)Instruction limit reached! % 93.26/13.44 % (414956)------------------------------ % 93.26/13.44 % (414956)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 93.26/13.44 % (414956)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 93.26/13.44 % (414956)CaDiCaL version: 2.1.3 % 93.26/13.44 % (414956)Termination reason: Instruction limit % 93.26/13.44 % (414956)Termination phase: Saturation % 93.26/13.44 % (414956)Time elapsed: 3.170 s % 93.26/13.44 % (414956)Peak memory usage: 15 MB % 93.26/13.44 % (414956)Instructions burned: 8175 (million) % 93.26/13.44 % (414966)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=1399989871:i=14134_2942 on theBenchmark for (2942ds/14134Mi) % 93.26/13.44 % (414964)Instruction limit reached! % 93.26/13.44 % (414964)------------------------------ % 93.26/13.44 % (414964)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 93.26/13.44 % (414964)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 93.26/13.44 % (414964)CaDiCaL version: 2.1.3 % 93.26/13.44 % (414964)Termination reason: Instruction limit % 93.26/13.44 % (414964)Termination phase: Saturation % 93.26/13.44 % (414964)Time elapsed: 2.383 s % 93.26/13.44 % (414964)Peak memory usage: 15 MB % 93.26/13.44 % (414964)Instructions burned: 11409 (million) % 93.26/13.44 % (414968)dis+33_16_sil=32000:sac=on:random_seed=720187638:i=15851:nm=0_2927 on theBenchmark for (2927ds/15851Mi) % 93.26/13.44 % (414968)Instruction limit reached! % 93.26/13.44 % (414968)------------------------------ % 93.26/13.44 % (414968)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 93.26/13.44 % (414968)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 93.26/13.44 % (414968)CaDiCaL version: 2.1.3 % 93.26/13.44 % (414968)Termination reason: Instruction limit % 93.26/13.44 % (414968)Termination phase: Saturation % 93.26/13.44 % (414968)Time elapsed: 3.315 s % 93.26/13.44 % (414968)Peak memory usage: 22 MB % 93.26/13.44 % (414968)Instructions burned: 15854 (million) % 93.26/13.44 % (414970)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=945851306:avsq=on:i=17627:add=on:amm=off_2894 on theBenchmark for (2894ds/17627Mi) % 105.48/15.16 % (414966)Instruction limit reached! % 105.48/15.16 % (414966)------------------------------ % 105.48/15.16 % (414966)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 105.48/15.16 % (414966)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 105.48/15.16 % (414966)CaDiCaL version: 2.1.3 % 105.48/15.16 % (414966)Termination reason: Instruction limit % 105.48/15.16 % (414966)Termination phase: Saturation % 105.48/15.16 % (414966)Time elapsed: 5.498 s % 105.48/15.16 % (414966)Peak memory usage: 16 MB % 105.48/15.16 % (414966)Instructions burned: 14135 (million) % 105.48/15.16 % (414972)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=3910360022:s2a=on:i=53295_2887 on theBenchmark for (2887ds/53295Mi) % 105.48/15.16 % (414954)Instruction limit reached! % 105.48/15.16 % (414954)------------------------------ % 105.48/15.16 % (414954)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 105.48/15.16 % (414954)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 105.48/15.16 % (414954)CaDiCaL version: 2.1.3 % 105.48/15.16 % (414954)Termination reason: Instruction limit % 105.48/15.16 % (414954)Termination phase: Saturation % 105.48/15.16 % (414954)Time elapsed: 9.156 s % 105.48/15.16 % (414954)Peak memory usage: 17 MB % 105.48/15.16 % (414954)Instructions burned: 22567 (million) % 105.48/15.16 % (414974)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=4021871555:i=26857:ins=20_2883 on theBenchmark for (2883ds/26857Mi) % 105.48/15.16 % (414974)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 105.48/15.16 % (414974)Terminated due to inappropriate strategy. % 105.48/15.16 % (414974)------------------------------ % 105.48/15.16 % (414974)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 105.48/15.16 % (414974)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 105.48/15.16 % (414974)CaDiCaL version: 2.1.3 % 105.48/15.16 % (414974)Termination reason: Inappropriate % 105.48/15.16 % (414974)Time elapsed: 0.013 s % 105.48/15.16 % (414974)Peak memory usage: 11 MB % 105.48/15.16 % (414974)Instructions burned: 31 (million) % 105.48/15.16 % (414974)------------------------------ % 105.48/15.16 % (414974)------------------------------ % 105.48/15.16 % (414976)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=3223504618:i=28120:bs=on:fsr=off_2883 on theBenchmark for (2883ds/28120Mi) % 105.48/15.16 % (414960)Instruction limit reached! % 105.48/15.16 % (414960)------------------------------ % 105.48/15.16 % (414960)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 105.48/15.16 % (414960)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 105.48/15.16 % (414960)CaDiCaL version: 2.1.3 % 105.48/15.16 % (414960)Termination reason: Instruction limit % 105.48/15.16 % (414960)Termination phase: Saturation % 105.48/15.16 % (414960)Time elapsed: 7.661 s % 105.48/15.16 % (414960)Peak memory usage: 19 MB % 105.48/15.16 % (414960)Instructions burned: 20142 (million) % 105.48/15.16 % (414978)fmb+10_1_sil=256000:fmbss=7:random_seed=2327438817:fmbsr=1.6:i=182295_2882 on theBenchmark for (2882ds/182295Mi) % 105.48/15.16 % (414978)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 105.48/15.16 % (414978)Terminated due to inappropriate strategy. % 105.48/15.16 % (414978)------------------------------ % 105.48/15.16 % (414978)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 105.48/15.16 % (414978)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 105.48/15.16 % (414978)CaDiCaL version: 2.1.3 % 105.48/15.16 % (414978)Termination reason: Inappropriate % 105.48/15.16 % (414978)Time elapsed: 0.013 s % 105.48/15.16 % (414978)Peak memory usage: 10 MB % 105.48/15.16 % (414978)Instructions burned: 31 (million) % 105.48/15.16 % (414978)------------------------------ % 105.48/15.16 % (414978)------------------------------ % 105.48/15.16 % (414980)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=534174366:i=44625:gsp=on_2882 on theBenchmark for (2882ds/44625Mi) % 105.48/15.16 % (414980)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 105.48/15.16 % (414980)Terminated due to inappropriate strategy. % 105.48/15.16 % (414980)------------------------------ % 105.48/15.16 % (414980)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 105.48/15.16 % (414980)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 105.48/15.16 % (414980)CaDiCaL version: 2.1.3 % 105.48/15.16 % (414980)Termination reason: Inappropriate % 113.84/16.36 % (414980)Time elapsed: 0.013 s % 113.84/16.36 % (414980)Peak memory usage: 11 MB % 113.84/16.36 % (414980)Instructions burned: 31 (million) % 113.84/16.36 % (414980)------------------------------ % 113.84/16.36 % (414980)------------------------------ % 113.84/16.36 % (414982)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=840332608:i=160505_2881 on theBenchmark for (2881ds/160505Mi) % 113.84/16.36 % (414982)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 113.84/16.36 % (414982)Terminated due to inappropriate strategy. % 113.84/16.36 % (414982)------------------------------ % 113.84/16.36 % (414982)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 113.84/16.36 % (414982)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 113.84/16.36 % (414982)CaDiCaL version: 2.1.3 % 113.84/16.36 % (414982)Termination reason: Inappropriate % 113.84/16.36 % (414982)Time elapsed: 0.013 s % 113.84/16.36 % (414982)Peak memory usage: 10 MB % 113.84/16.36 % (414982)Instructions burned: 31 (million) % 113.84/16.36 % (414982)------------------------------ % 113.84/16.36 % (414982)------------------------------ % 113.84/16.36 % (414984)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=800207583:fmbsr=1.3:i=225729_2881 on theBenchmark for (2881ds/225729Mi) % 113.84/16.36 % (414984)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 113.84/16.36 % (414984)Terminated due to inappropriate strategy. % 113.84/16.36 % (414984)------------------------------ % 113.84/16.36 % (414984)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 113.84/16.36 % (414984)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 113.84/16.36 % (414984)CaDiCaL version: 2.1.3 % 113.84/16.36 % (414984)Termination reason: Inappropriate % 113.84/16.36 % (414984)Time elapsed: 0.013 s % 113.84/16.36 % (414984)Peak memory usage: 10 MB % 113.84/16.36 % (414984)Instructions burned: 31 (million) % 113.84/16.36 % (414984)------------------------------ % 113.84/16.36 % (414984)------------------------------ % 113.84/16.36 % (414986)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=624127730:fmbsr=2:i=185024:ins=7_2880 on theBenchmark for (2880ds/185024Mi) % 113.84/16.36 % (414986)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 113.84/16.36 % (414986)Terminated due to inappropriate strategy. % 113.84/16.36 % (414986)------------------------------ % 113.84/16.36 % (414986)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 113.84/16.36 % (414986)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 113.84/16.36 % (414986)CaDiCaL version: 2.1.3 % 113.84/16.36 % (414986)Termination reason: Inappropriate % 113.84/16.36 % (414986)Time elapsed: 0.013 s % 113.84/16.36 % (414986)Peak memory usage: 10 MB % 113.84/16.36 % (414986)Instructions burned: 31 (million) % 113.84/16.36 % (414986)------------------------------ % 113.84/16.36 % (414986)------------------------------ % 113.84/16.36 % (414988)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=1397154961:rtra=on_2880 on theBenchmark for (2880ds/0Mi) % 113.84/16.36 % (414988)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 113.84/16.36 % (414988)Terminated due to inappropriate strategy. % 113.84/16.36 % (414988)------------------------------ % 113.84/16.36 % (414988)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 113.84/16.36 % (414988)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 113.84/16.36 % (414988)CaDiCaL version: 2.1.3 % 113.84/16.36 % (414988)Termination reason: Inappropriate % 113.84/16.36 % (414988)Time elapsed: 0.013 s % 113.84/16.36 % (414988)Peak memory usage: 11 MB % 113.84/16.36 % (414988)Instructions burned: 32 (million) % 113.84/16.36 % (414988)------------------------------ % 113.84/16.36 % (414988)------------------------------ % 113.84/16.36 % (414990)% WARNING: option uhcvi not known. % 113.84/16.36 % (414990)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1599145696:i=271062:add=off:rtra=on:rawr=on_2880 on theBenchmark for (2880ds/271062Mi) % 113.84/16.36 % (414944)Instruction limit reached! % 113.84/16.36 % (414944)------------------------------ % 113.84/16.36 % (414944)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 113.84/16.36 % (414944)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 113.84/16.36 % (414944)CaDiCaL version: 2.1.3 % 113.84/16.36 % (414944)Termination reason: Instruction limit % 113.84/16.36 % (414944)Termination phase: Saturation % 113.84/16.36 % (414944)Time elapsed: 11.155 s % 113.84/16.36 % (414944)Peak memory usage: 21 MB % 113.84/16.36 % (414944)Instructions burned: 29341 (million) % 119.78/17.14 % (414992)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1801414923:i=176048:add=on:rtra=on:rawr=on_2867 on theBenchmark for (2867ds/176048Mi) % 119.78/17.14 % (414970)Instruction limit reached! % 119.78/17.14 % (414970)------------------------------ % 119.78/17.14 % (414970)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 119.78/17.14 % (414970)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 119.78/17.14 % (414970)CaDiCaL version: 2.1.3 % 119.78/17.14 % (414970)Termination reason: Instruction limit % 119.78/17.14 % (414970)Termination phase: Saturation % 119.78/17.14 % (414970)Time elapsed: 4.063 s % 119.78/17.14 % (414970)Peak memory usage: 98 MB % 119.78/17.14 % (414970)Instructions burned: 17630 (million) % 119.78/17.14 % (414994)dis+10_1_sil=32000:si=on:sp=arity:random_seed=1399867082:i=206:fgj=on:rtra=on_2853 on theBenchmark for (2853ds/206Mi) % 119.78/17.14 % (414994)Instruction limit reached! % 119.78/17.14 % (414994)------------------------------ % 119.78/17.14 % (414994)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 119.78/17.14 % (414994)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 119.78/17.14 % (414994)CaDiCaL version: 2.1.3 % 119.78/17.14 % (414994)Termination reason: Instruction limit % 119.78/17.14 % (414994)Termination phase: Saturation % 119.78/17.14 % (414994)Time elapsed: 0.045 s % 119.78/17.14 % (414994)Peak memory usage: 13 MB % 119.78/17.14 % (414994)Instructions burned: 210 (million) % 119.78/17.14 % (414996)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=4140604377:i=232:rtra=on_2853 on theBenchmark for (2853ds/232Mi) % 119.78/17.14 % (414996)Instruction limit reached! % 119.78/17.14 % (414996)------------------------------ % 119.78/17.14 % (414996)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 119.78/17.14 % (414996)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 119.78/17.14 % (414996)CaDiCaL version: 2.1.3 % 119.78/17.14 % (414996)Termination reason: Instruction limit % 119.78/17.14 % (414996)Termination phase: Saturation % 119.78/17.14 % (414996)Time elapsed: 0.049 s % 119.78/17.14 % (414996)Peak memory usage: 12 MB % 119.78/17.14 % (414996)Instructions burned: 234 (million) % 119.78/17.14 % (414998)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=1406949743:i=262:rtra=on_2852 on theBenchmark for (2852ds/262Mi) % 119.78/17.14 % (414998)Instruction limit reached! % 119.78/17.14 % (414998)------------------------------ % 119.78/17.14 % (414998)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 119.78/17.14 % (414998)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 119.78/17.14 % (414998)CaDiCaL version: 2.1.3 % 119.78/17.14 % (414998)Termination reason: Instruction limit % 119.78/17.14 % (414998)Termination phase: Saturation % 119.78/17.14 % (414998)Time elapsed: 0.055 s % 119.78/17.14 % (414998)Peak memory usage: 12 MB % 119.78/17.14 % (414998)Instructions burned: 267 (million) % 119.78/17.14 % (415000)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=1211454432:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2851 on theBenchmark for (2851ds/318Mi) % 119.78/17.14 % (415000)Instruction limit reached! % 119.78/17.14 % (415000)------------------------------ % 119.78/17.14 % (415000)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 119.78/17.14 % (415000)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 119.78/17.14 % (415000)CaDiCaL version: 2.1.3 % 119.78/17.14 % (415000)Termination reason: Instruction limit % 119.78/17.14 % (415000)Termination phase: Saturation % 119.78/17.14 % (415000)Time elapsed: 0.078 s % 119.78/17.14 % (415000)Peak memory usage: 14 MB % 119.78/17.14 % (415000)Instructions burned: 320 (million) % 119.78/17.14 % (415002)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=3144364260:i=1428:nm=2:rtra=on_2850 on theBenchmark for (2850ds/1428Mi) % 119.78/17.14 % (415002)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 119.78/17.14 % (415002)Terminated due to inappropriate strategy. % 119.78/17.14 % (415002)------------------------------ % 119.78/17.14 % (415002)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 119.78/17.14 % (415002)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 119.78/17.14 % (415002)CaDiCaL version: 2.1.3 % 119.78/17.14 % (415002)Termination reason: Inappropriate % 119.78/17.14 % (415002)Time elapsed: 0.007 s % 119.78/17.14 % (415002)Peak memory usage: 11 MB % 119.78/17.14 % (415002)Instructions burned: 31 (million) % 119.78/17.14 % (415002)------------------------------ % 141.94/20.37 % (415002)------------------------------ % 141.94/20.37 % (415004)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=93661499:i=262:bd=preordered:rtra=on:fsd=on_2850 on theBenchmark for (2850ds/262Mi) % 141.94/20.37 % (415004)Instruction limit reached! % 141.94/20.37 % (415004)------------------------------ % 141.94/20.37 % (415004)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 141.94/20.37 % (415004)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 141.94/20.37 % (415004)CaDiCaL version: 2.1.3 % 141.94/20.37 % (415004)Termination reason: Instruction limit % 141.94/20.37 % (415004)Termination phase: Saturation % 141.94/20.37 % (415004)Time elapsed: 0.056 s % 141.94/20.37 % (415004)Peak memory usage: 13 MB % 141.94/20.37 % (415004)Instructions burned: 267 (million) % 141.94/20.37 % (415006)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=2613938824:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2850 on theBenchmark for (2850ds/1368Mi) % 141.94/20.37 % (415006)Instruction limit reached! % 141.94/20.37 % (415006)------------------------------ % 141.94/20.37 % (415006)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 141.94/20.37 % (415006)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 141.94/20.37 % (415006)CaDiCaL version: 2.1.3 % 141.94/20.37 % (415006)Termination reason: Instruction limit % 141.94/20.37 % (415006)Termination phase: Saturation % 141.94/20.37 % (415006)Time elapsed: 0.312 s % 141.94/20.37 % (415006)Peak memory usage: 17 MB % 141.94/20.37 % (415006)Instructions burned: 1372 (million) % 141.94/20.37 % (415008)ott-21_1_sil=16000:si=on:fs=off:random_seed=3116829359:i=360:av=off:fsr=off:rtra=on_2846 on theBenchmark for (2846ds/360Mi) % 141.94/20.37 % (415008)Instruction limit reached! % 141.94/20.37 % (415008)------------------------------ % 141.94/20.37 % (415008)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 141.94/20.37 % (415008)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 141.94/20.37 % (415008)CaDiCaL version: 2.1.3 % 141.94/20.37 % (415008)Termination reason: Instruction limit % 141.94/20.37 % (415008)Termination phase: Saturation % 141.94/20.37 % (415008)Time elapsed: 0.074 s % 141.94/20.37 % (415008)Peak memory usage: 12 MB % 141.94/20.37 % (415008)Instructions burned: 366 (million) % 141.94/20.37 % (415010)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=4214986970:i=954:bd=all:rtra=on_2845 on theBenchmark for (2845ds/954Mi) % 141.94/20.37 % (415010)Instruction limit reached! % 141.94/20.37 % (415010)------------------------------ % 141.94/20.37 % (415010)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 141.94/20.37 % (415010)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 141.94/20.37 % (415010)CaDiCaL version: 2.1.3 % 141.94/20.37 % (415010)Termination reason: Instruction limit % 141.94/20.37 % (415010)Termination phase: Saturation % 141.94/20.37 % (415010)Time elapsed: 0.203 s % 141.94/20.37 % (415010)Peak memory usage: 13 MB % 141.94/20.37 % (415010)Instructions burned: 954 (million) % 141.94/20.37 % (415012)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=2898579912:fmbsr=1.3:i=1730:ins=25:rtra=on_2843 on theBenchmark for (2843ds/1730Mi) % 141.94/20.37 % (415012)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 141.94/20.37 % (415012)Terminated due to inappropriate strategy. % 141.94/20.37 % (415012)------------------------------ % 141.94/20.37 % (415012)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 141.94/20.37 % (415012)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 141.94/20.37 % (415012)CaDiCaL version: 2.1.3 % 141.94/20.37 % (415012)Termination reason: Inappropriate % 141.94/20.37 % (415012)Time elapsed: 0.005 s % 141.94/20.37 % (415012)Peak memory usage: 10 MB % 141.94/20.37 % (415012)Instructions burned: 24 (million) % 141.94/20.37 % (415012)------------------------------ % 141.94/20.37 % (415012)------------------------------ % 141.94/20.37 % (415014)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=4206763177:i=2358:rtra=on_2843 on theBenchmark for (2843ds/2358Mi) % 141.94/20.37 % (415014)Instruction limit reached! % 141.94/20.37 % (415014)------------------------------ % 141.94/20.37 % (415014)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 141.94/20.37 % (415014)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 141.94/20.37 % (415014)CaDiCaL version: 2.1.3 % 141.94/20.37 % (415014)Termination reason: Instruction limit % 173.99/24.96 % (415014)Termination phase: Saturation % 173.99/24.96 % (415014)Time elapsed: 0.489 s % 173.99/24.96 % (415014)Peak memory usage: 13 MB % 173.99/24.96 % (415014)Instructions burned: 2362 (million) % 173.99/24.96 % (415016)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=3689520265:i=1778:ins=1:rtra=on_2838 on theBenchmark for (2838ds/1778Mi) % 173.99/24.96 % (415016)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 173.99/24.96 % (415016)Terminated due to inappropriate strategy. % 173.99/24.96 % (415016)------------------------------ % 173.99/24.96 % (415016)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 173.99/24.96 % (415016)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 173.99/24.96 % (415016)CaDiCaL version: 2.1.3 % 173.99/24.96 % (415016)Termination reason: Inappropriate % 173.99/24.96 % (415016)Time elapsed: 0.005 s % 173.99/24.96 % (415016)Peak memory usage: 10 MB % 173.99/24.96 % (415016)Instructions burned: 24 (million) % 173.99/24.96 % (415016)------------------------------ % 173.99/24.96 % (415016)------------------------------ % 173.99/24.96 % (415018)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=2788937627:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2838 on theBenchmark for (2838ds/1384Mi) % 173.99/24.96 % (415018)Instruction limit reached! % 173.99/24.96 % (415018)------------------------------ % 173.99/24.96 % (415018)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 173.99/24.96 % (415018)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 173.99/24.96 % (415018)CaDiCaL version: 2.1.3 % 173.99/24.96 % (415018)Termination reason: Instruction limit % 173.99/24.96 % (415018)Termination phase: Saturation % 173.99/24.96 % (415018)Time elapsed: 0.294 s % 173.99/24.96 % (415018)Peak memory usage: 15 MB % 173.99/24.96 % (415018)Instructions burned: 1387 (million) % 173.99/24.96 % (415020)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=2881889377:i=1758:kws=inv_precedence:fsr=off:rtra=on_2835 on theBenchmark for (2835ds/1758Mi) % 173.99/24.96 % (415020)Instruction limit reached! % 173.99/24.96 % (415020)------------------------------ % 173.99/24.96 % (415020)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 173.99/24.96 % (415020)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 173.99/24.96 % (415020)CaDiCaL version: 2.1.3 % 173.99/24.96 % (415020)Termination reason: Instruction limit % 173.99/24.96 % (415020)Termination phase: Saturation % 173.99/24.96 % (415020)Time elapsed: 0.361 s % 173.99/24.96 % (415020)Peak memory usage: 14 MB % 173.99/24.96 % (415020)Instructions burned: 1761 (million) % 173.99/24.96 % (415022)fmb+10_1_sil=64000:si=on:random_seed=2902694515:i=44122:nm=2:rtra=on:gsp=on_2831 on theBenchmark for (2831ds/44122Mi) % 173.99/24.96 % (415022)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 173.99/24.96 % (415022)Terminated due to inappropriate strategy. % 173.99/24.96 % (415022)------------------------------ % 173.99/24.96 % (415022)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 173.99/24.96 % (415022)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 173.99/24.96 % (415022)CaDiCaL version: 2.1.3 % 173.99/24.96 % (415022)Termination reason: Inappropriate % 173.99/24.96 % (415022)Time elapsed: 0.013 s % 173.99/24.96 % (415022)Peak memory usage: 11 MB % 173.99/24.96 % (415022)Instructions burned: 32 (million) % 173.99/24.96 % (415022)------------------------------ % 173.99/24.96 % (415022)------------------------------ % 173.99/24.96 % (415024)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=1347913209:i=19030:nm=5:rtra=on_2831 on theBenchmark for (2831ds/19030Mi) % 173.99/24.96 % (415024)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 173.99/24.96 % (415024)Terminated due to inappropriate strategy. % 173.99/24.96 % (415024)------------------------------ % 173.99/24.96 % (415024)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 173.99/24.96 % (415024)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 173.99/24.96 % (415024)CaDiCaL version: 2.1.3 % 173.99/24.96 % (415024)Termination reason: Inappropriate % 173.99/24.96 % (415024)Time elapsed: 0.013 s % 173.99/24.96 % (415024)Peak memory usage: 11 MB % 173.99/24.96 % (415024)Instructions burned: 32 (million) % 173.99/24.96 % (415024)------------------------------ % 173.99/24.96 % (415024)------------------------------ % 173.99/24.96 % (415026)fmb+10_1_sil=64000:sas=cadical:si=on:fmbss=8:random_seed=3396071681:fmbsr=1.7:i=1840:rtra=on_2831 on theBenchmark for (2831ds/1840Mi) % 208.92/29.72 % (415026)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 208.92/29.72 % (415026)Terminated due to inappropriate strategy. % 208.92/29.72 % (415026)------------------------------ % 208.92/29.72 % (415026)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 208.92/29.72 % (415026)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 208.92/29.72 % (415026)CaDiCaL version: 2.1.3 % 208.92/29.72 % (415026)Termination reason: Inappropriate % 208.92/29.72 % (415026)Time elapsed: 0.007 s % 208.92/29.72 % (415026)Peak memory usage: 11 MB % 208.92/29.72 % (415026)Instructions burned: 31 (million) % 208.92/29.72 % (415026)------------------------------ % 208.92/29.72 % (415026)------------------------------ % 208.92/29.72 % (415028)dis-4_1_sil=16000:drc=ordering:si=on:sp=const_frequency:sac=on:newcnf=on:random_seed=3219748544:i=10262:rtra=on_2830 on theBenchmark for (2830ds/10262Mi) % 208.92/29.72 % (415028)Instruction limit reached! % 208.92/29.72 % (415028)------------------------------ % 208.92/29.72 % (415028)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 208.92/29.72 % (415028)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 208.92/29.72 % (415028)CaDiCaL version: 2.1.3 % 208.92/29.72 % (415028)Termination reason: Instruction limit % 208.92/29.72 % (415028)Termination phase: Saturation % 208.92/29.72 % (415028)Time elapsed: 2.167 s % 208.92/29.72 % (415028)Peak memory usage: 22 MB % 208.92/29.72 % (415028)Instructions burned: 10263 (million) % 208.92/29.72 % (415031)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:si=on:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2339378360:i=2944:ins=7:rtra=on:fdi=8:gsp=on_2808 on theBenchmark for (2808ds/2944Mi) % 208.92/29.72 % (415031)Instruction limit reached! % 208.92/29.72 % (415031)------------------------------ % 208.92/29.72 % (415031)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 208.92/29.72 % (415031)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 208.92/29.72 % (415031)CaDiCaL version: 2.1.3 % 208.92/29.72 % (415031)Termination reason: Instruction limit % 208.92/29.72 % (415031)Termination phase: Saturation % 208.92/29.72 % (415031)Time elapsed: 0.621 s % 208.92/29.72 % (415031)Peak memory usage: 16 MB % 208.92/29.72 % (415031)Instructions burned: 2948 (million) % 208.92/29.72 % (415033)fmb+10_1_sil=16000:sas=cadical:si=on:bce=on:fmbss=77:random_seed=1358685297:i=12648:rtra=on_2802 on theBenchmark for (2802ds/12648Mi) % 208.92/29.72 % (415033)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 208.92/29.72 % (415033)Terminated due to inappropriate strategy. % 208.92/29.72 % (415033)------------------------------ % 208.92/29.72 % (415033)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 208.92/29.72 % (415033)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 208.92/29.72 % (415033)CaDiCaL version: 2.1.3 % 208.92/29.72 % (415033)Termination reason: Inappropriate % 208.92/29.72 % (415033)Time elapsed: 0.007 s % 208.92/29.72 % (415033)Peak memory usage: 11 MB % 208.92/29.72 % (415033)Instructions burned: 31 (million) % 208.92/29.72 % (415033)------------------------------ % 208.92/29.72 % (415033)------------------------------ % 208.92/29.72 % (415035)fmb+10_1_fmbas=function:sil=32000:sas=cadical:si=on:fmbss=16:random_seed=2417097744:fmbsr=2.30978:i=4348:rtra=on_2802 on theBenchmark for (2802ds/4348Mi) % 208.92/29.72 % (415035)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 208.92/29.72 % (415035)Terminated due to inappropriate strategy. % 208.92/29.72 % (415035)------------------------------ % 208.92/29.72 % (415035)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 208.92/29.72 % (415035)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 208.92/29.72 % (415035)CaDiCaL version: 2.1.3 % 208.92/29.72 % (415035)Termination reason: Inappropriate % 208.92/29.72 % (415035)Time elapsed: 0.007 s % 208.92/29.72 % (415035)Peak memory usage: 11 MB % 208.92/29.72 % (415035)Instructions burned: 31 (million) % 208.92/29.72 % (415035)------------------------------ % 208.92/29.72 % (415035)------------------------------ % 208.92/29.72 % (415037)ott-2_1_sil=16000:si=on:newcnf=on:random_seed=3478716522:avsq=on:i=1738:avsqr=1,16:kws=inv_arity_squared:rtra=on_2802 on theBenchmark for (2802ds/1738Mi) % 208.92/29.72 % (415037)Instruction limit reached! % 208.92/29.72 % (415037)------------------------------ % 208.92/29.72 % (415037)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 208.92/29.72 % (415037)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 279.41/39.72 % (415037)CaDiCaL version: 2.1.3 % 279.41/39.72 % (415037)Termination reason: Instruction limit % 279.41/39.72 % (415037)Termination phase: Saturation % 279.41/39.72 % (415037)Time elapsed: 0.354 s % 279.41/39.72 % (415037)Peak memory usage: 14 MB % 279.41/39.72 % (415037)Instructions burned: 1744 (million) % 279.41/39.72 % (415039)ott+10_1_sil=32000:tgt=ground:si=on:random_seed=2841994492:i=10228:av=off:rtra=on_2798 on theBenchmark for (2798ds/10228Mi) % 279.41/39.72 % (415039)Instruction limit reached! % 279.41/39.72 % (415039)------------------------------ % 279.41/39.72 % (415039)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 279.41/39.72 % (415039)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 279.41/39.72 % (415039)CaDiCaL version: 2.1.3 % 279.41/39.72 % (415039)Termination reason: Instruction limit % 279.41/39.72 % (415039)Termination phase: Saturation % 279.41/39.72 % (415039)Time elapsed: 2.124 s % 279.41/39.72 % (415039)Peak memory usage: 16 MB % 279.41/39.72 % (415039)Instructions burned: 10234 (million) % 279.41/39.72 % (415041)fmb+10_1_sil=64000:sas=cadical:si=on:bce=on:rp=on:random_seed=2802688363:i=108564:rtra=on_2777 on theBenchmark for (2777ds/108564Mi) % 279.41/39.72 % (415041)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 279.41/39.72 % (415041)Terminated due to inappropriate strategy. % 279.41/39.72 % (415041)------------------------------ % 279.41/39.72 % (415041)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 279.41/39.72 % (415041)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 279.41/39.72 % (415041)CaDiCaL version: 2.1.3 % 279.41/39.72 % (415041)Termination reason: Inappropriate % 279.41/39.72 % (415041)Time elapsed: 0.007 s % 279.41/39.72 % (415041)Peak memory usage: 11 MB % 279.41/39.72 % (415041)Instructions burned: 31 (million) % 279.41/39.72 % (415041)------------------------------ % 279.41/39.72 % (415041)------------------------------ % 279.41/39.72 % (415043)dis-11_1_sil=16000:si=on:sp=reverse_frequency:alpa=true:random_seed=2049284375:i=7024:aac=none:rtra=on_2776 on theBenchmark for (2776ds/7024Mi) % 279.41/39.72 % (414976)Instruction limit reached! % 279.41/39.72 % (414976)------------------------------ % 279.41/39.72 % (414976)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 279.41/39.72 % (414976)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 279.41/39.72 % (414976)CaDiCaL version: 2.1.3 % 279.41/39.72 % (414976)Termination reason: Instruction limit % 279.41/39.72 % (414976)Termination phase: Saturation % 279.41/39.72 % (414976)Time elapsed: 10.895 s % 279.41/39.72 % (414976)Peak memory usage: 18 MB % 279.41/39.72 % (414976)Instructions burned: 28120 (million) % 279.41/39.72 % (415045)dis+21_1_sil=32000:sas=cadical:si=on:random_seed=1671752270:i=7546:rtra=on:amm=off_2774 on theBenchmark for (2774ds/7546Mi) % 279.41/39.72 % (415043)Instruction limit reached! % 279.41/39.72 % (415043)------------------------------ % 279.41/39.72 % (415043)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 279.41/39.72 % (415043)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 279.41/39.72 % (415043)CaDiCaL version: 2.1.3 % 279.41/39.72 % (415043)Termination reason: Instruction limit % 279.41/39.72 % (415043)Termination phase: Saturation % 279.41/39.72 % (415043)Time elapsed: 1.473 s % 279.41/39.72 % (415043)Peak memory usage: 20 MB % 279.41/39.72 % (415043)Instructions burned: 7029 (million) % 279.41/39.72 % (415047)ott+11_1_sil=16000:si=on:gs=on:random_seed=1507572371:s2a=on:i=4502:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:rtra=on:fsd=on_2762 on theBenchmark for (2762ds/4502Mi) % 279.41/39.72 % (415047)Instruction limit reached! % 279.41/39.72 % (415047)------------------------------ % 279.41/39.72 % (415047)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 279.41/39.72 % (415047)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 279.41/39.72 % (415047)CaDiCaL version: 2.1.3 % 279.41/39.72 % (415047)Termination reason: Instruction limit % 279.41/39.72 % (415047)Termination phase: Saturation % 279.41/39.72 % (415047)Time elapsed: 0.917 s % 279.41/39.72 % (415047)Peak memory usage: 16 MB % 279.41/39.72 % (415047)Instructions burned: 4503 (million) % 279.41/39.72 % (415049)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:si=on:fmbss=7:random_seed=3270083279:fmbsr=1.6:i=135068:rtra=on_2752 on theBenchmark for (2752ds/135068Mi) % 279.41/39.72 % (415049)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 279.41/39.72 % (415049)Terminated due to inappropriate strategy. % 279.41/39.72 % (415049)------------------------------ % 279.41/39.72 % (415049)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.48/42.63 % (415049)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.48/42.63 % (415049)CaDiCaL version: 2.1.3 % 300.48/42.63 % (415049)Termination reason: Inappropriate % 300.48/42.63 % (415049)Time elapsed: 0.007 s % 300.48/42.63 % (415049)Peak memory usage: 11 MB % 300.48/42.63 % (415049)Instructions burned: 31 (million) % 300.48/42.63 % (415049)------------------------------ % 300.48/42.63 % (415049)------------------------------ % 300.48/42.63 % (415051)ott-22_32_sil=16000:tgt=full:si=on:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=990379813:avsq=on:i=9182:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:rtra=on:fdi=4_2752 on theBenchmark for (2752ds/9182Mi) % 300.48/42.63 % (415045)Instruction limit reached! % 300.48/42.63 % (415045)------------------------------ % 300.48/42.63 % (415045)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.48/42.63 % (415045)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.48/42.63 % (415045)CaDiCaL version: 2.1.3 % 300.48/42.63 % (415045)Termination reason: Instruction limit % 300.48/42.63 % (415045)Termination phase: Saturation % 300.48/42.63 % (415045)Time elapsed: 2.895 s % 300.48/42.63 % (415045)Peak memory usage: 19 MB % 300.48/42.63 % (415045)Instructions burned: 7547 (million) % 300.48/42.63 % (415053)dis+10_64_to=lpo:sil=32000:si=on:spb=intro:urr=on:sac=on:random_seed=4018146092:i=58680:rtra=on_2745 on theBenchmark for (2745ds/58680Mi) % 300.48/42.63 % (415051)Instruction limit reached! % 300.48/42.63 % (415051)------------------------------ % 300.48/42.63 % (415051)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.48/42.63 % (415051)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.48/42.63 % (415051)CaDiCaL version: 2.1.3 % 300.48/42.63 % (415051)Termination reason: Instruction limit % 300.48/42.63 % (415051)Termination phase: Saturation % 300.48/42.63 % (415051)Time elapsed: 2.536 s % 300.48/42.63 % (415051)Peak memory usage: 54 MB % 300.48/42.63 % (415051)Instructions burned: 9182 (million) % 300.48/42.63 % (415055)dis-10_1_sil=64000:sas=cadical:si=on:cn=on:random_seed=2960133649:i=10422:rtra=on_2727 on theBenchmark for (2727ds/10422Mi) % 300.48/42.63 % (415055)Instruction limit reached! % 300.48/42.63 % (415055)------------------------------ % 300.48/42.63 % (415055)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.48/42.63 % (415055)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.48/42.63 % (415055)CaDiCaL version: 2.1.3 % 300.48/42.63 % (415055)Termination reason: Instruction limit % 300.48/42.63 % (415055)Termination phase: Saturation % 300.48/42.63 % (415055)Time elapsed: 2.150 s % 300.48/42.63 % (415055)Peak memory usage: 27 MB % 300.48/42.63 % (415055)Instructions burned: 10426 (million) % 300.48/42.63 % (415057)fmb+10_1_sil=32000:sas=cadical:si=on:bce=on:fmbss=17:random_seed=3307091353:i=10994:nm=2:rtra=on_2705 on theBenchmark for (2705ds/10994Mi) % 300.48/42.63 % (415057)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 300.48/42.63 % (415057)Terminated due to inappropriate strategy. % 300.48/42.63 % (415057)------------------------------ % 300.48/42.63 % (415057)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.48/42.63 % (415057)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.48/42.63 % (415057)CaDiCaL version: 2.1.3 % 300.48/42.63 % (415057)Termination reason: Inappropriate % 300.48/42.63 % (415057)Time elapsed: 0.007 s % 300.48/42.63 % (415057)Peak memory usage: 11 MB % 300.48/42.63 % (415057)Instructions burned: 31 (million) % 300.48/42.63 % (415057)------------------------------ % 300.48/42.63 % (415057)------------------------------ % 300.48/42.63 % (415059)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:si=on:fmbss=15:random_seed=2013694205:fmbsr=2:i=92664:rtra=on_2705 on theBenchmark for (2705ds/92664Mi) % 300.48/42.63 % (415059)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 300.48/42.63 % (415059)Terminated due to inappropriate strategy. % 300.48/42.63 % (415059)------------------------------ % 300.48/42.63 % (415059)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.48/42.63 % (415059)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.48/42.63 % (415059)CaDiCaL version: 2.1.3 % 300.48/42.63 % (415059)Termination reason: Inappropriate % 300.48/42.63 % (415059)Time elapsed: 0.007 s % 300.48/42.63 % (415059)Peak memory usage: 11 MB % 300.48/42.63 % (415059)Instructions burned: 31 (million) % 300.48/42.63 % (415059)----------------------------- % 300.48/42.64 Terminated % 300.48/42.64 % Vampire exiting %------------------------------------------------------------------------------