%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWW740_1 : TPTP v9.3.1. Released v7.0.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/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:40:41 PM UTC 2026 % Result : Timeout 289.10s 41.03s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWW740_1 : TPTP v9.3.1. Released v7.0.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.09/0.20 % Computer : n015.cluster.edu % 0.09/0.20 % Model : x86_64 x86_64 % 0.09/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.20 % Memory : 8046.5625MB % 0.09/0.20 % OS : Linux 6.8.0-71-generic % 0.09/0.20 % CPULimit : 300 % 0.09/0.20 % WCLimit : 300 % 0.09/0.20 % DateTime : Mon Sep 28 14:32:02 UTC 2026 % 0.09/0.20 % CPUTime : % 0.09/0.20 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.09/0.22 Running first-order model finding % 0.09/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 % 3.91/0.89 % (2671452)Will run a generic schedule for satisfiability detection. % 3.91/0.89 % (2671458)% WARNING: option uhcvi not known. % 3.91/0.89 % (2671458)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3020307569:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 3.91/0.89 % (2671457)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3086265271_2999 on theBenchmark for (2999ds/0Mi) % 3.91/0.89 % (2671459)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1376105691:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 3.91/0.89 % (2671460)dis+10_1_sil=32000:sp=arity:random_seed=2595755645:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 3.91/0.89 % (2671461)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1510258703:i=116_2999 on theBenchmark for (2999ds/116Mi) % 3.91/0.89 % (2671462)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=878436149:i=131_2999 on theBenchmark for (2999ds/131Mi) % 3.91/0.89 % (2671463)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2577885582:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 3.91/0.89 % (2671457)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.91/0.89 % (2671457)Terminated due to inappropriate strategy. % 3.91/0.89 % (2671457)------------------------------ % 3.91/0.89 % (2671457)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.91/0.89 % (2671457)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.91/0.89 % (2671457)CaDiCaL version: 2.1.3 % 3.91/0.89 % (2671457)Termination reason: Inappropriate % 3.91/0.89 % (2671457)Time elapsed: 0.009 s % 3.91/0.89 % (2671457)Peak memory usage: 11 MB % 3.91/0.89 % (2671457)Instructions burned: 19 (million) % 3.91/0.89 % (2671457)------------------------------ % 3.91/0.89 % (2671457)------------------------------ % 3.91/0.89 % (2671471)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=413142553:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 3.91/0.89 % (2671471)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.91/0.89 % (2671471)Terminated due to inappropriate strategy. % 3.91/0.89 % (2671471)------------------------------ % 3.91/0.89 % (2671471)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.91/0.89 % (2671471)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.91/0.89 % (2671471)CaDiCaL version: 2.1.3 % 3.91/0.89 % (2671471)Termination reason: Inappropriate % 3.91/0.89 % (2671471)Time elapsed: 0.006 s % 3.91/0.89 % (2671471)Peak memory usage: 10 MB % 3.91/0.89 % (2671471)Instructions burned: 14 (million) % 3.91/0.89 % (2671471)------------------------------ % 3.91/0.89 % (2671471)------------------------------ % 3.91/0.89 % (2671473)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2209320927:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 3.91/0.89 % (2671460)Instruction limit reached! % 3.91/0.89 % (2671460)------------------------------ % 3.91/0.89 % (2671460)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.91/0.89 % (2671460)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.91/0.89 % (2671460)CaDiCaL version: 2.1.3 % 3.91/0.89 % (2671460)Termination reason: Instruction limit % 3.91/0.89 % (2671460)Termination phase: Saturation % 3.91/0.89 % (2671460)Time elapsed: 0.062 s % 3.91/0.89 % (2671460)Peak memory usage: 13 MB % 3.91/0.89 % (2671460)Instructions burned: 104 (million) % 3.91/0.89 % (2671461)Instruction limit reached! % 3.91/0.89 % (2671461)------------------------------ % 3.91/0.89 % (2671461)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.91/0.89 % (2671461)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.91/0.89 % (2671461)CaDiCaL version: 2.1.3 % 3.91/0.89 % (2671461)Termination reason: Instruction limit % 3.91/0.89 % (2671461)Termination phase: Saturation % 3.91/0.89 % (2671461)Time elapsed: 0.065 s % 3.91/0.89 % (2671461)Peak memory usage: 13 MB % 3.91/0.89 % (2671461)Instructions burned: 116 (million) % 3.91/0.89 % (2671462)Instruction limit reached! % 3.91/0.89 % (2671462)------------------------------ % 3.91/0.89 % (2671462)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.91/0.89 % (2671462)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.91/0.89 % (2671462)CaDiCaL version: 2.1.3 % 3.91/0.89 % (2671462)Termination reason: Instruction limit % 6.41/1.17 % (2671462)Termination phase: Saturation % 6.41/1.17 % (2671462)Time elapsed: 0.080 s % 6.41/1.17 % (2671462)Peak memory usage: 13 MB % 6.41/1.17 % (2671462)Instructions burned: 132 (million) % 6.41/1.17 % (2671475)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=4161845279:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi) % 6.41/1.17 % (2671476)ott-21_1_sil=16000:fs=off:random_seed=1653611722:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 6.41/1.17 % (2671480)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2823093239:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 6.41/1.17 % (2671463)Instruction limit reached! % 6.41/1.17 % (2671463)------------------------------ % 6.41/1.17 % (2671463)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.41/1.17 % (2671463)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.41/1.17 % (2671463)CaDiCaL version: 2.1.3 % 6.41/1.17 % (2671463)Termination reason: Instruction limit % 6.41/1.17 % (2671463)Termination phase: Saturation % 6.41/1.17 % (2671463)Time elapsed: 0.100 s % 6.41/1.17 % (2671463)Peak memory usage: 14 MB % 6.41/1.17 % (2671463)Instructions burned: 159 (million) % 6.41/1.17 % (2671489)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1634250488:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 6.41/1.17 % (2671489)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 6.41/1.17 % (2671489)Terminated due to inappropriate strategy. % 6.41/1.17 % (2671489)------------------------------ % 6.41/1.17 % (2671489)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.41/1.17 % (2671489)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.41/1.17 % (2671489)CaDiCaL version: 2.1.3 % 6.41/1.17 % (2671489)Termination reason: Inappropriate % 6.41/1.17 % (2671489)Time elapsed: 0.012 s % 6.41/1.17 % (2671489)Peak memory usage: 11 MB % 6.41/1.17 % (2671489)Instructions burned: 27 (million) % 6.41/1.17 % (2671489)------------------------------ % 6.41/1.17 % (2671489)------------------------------ % 6.41/1.17 % (2671473)Instruction limit reached! % 6.41/1.17 % (2671473)------------------------------ % 6.41/1.17 % (2671473)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.41/1.17 % (2671473)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.41/1.17 % (2671473)CaDiCaL version: 2.1.3 % 6.41/1.17 % (2671473)Termination reason: Instruction limit % 6.41/1.17 % (2671473)Termination phase: Saturation % 6.41/1.17 % (2671473)Time elapsed: 0.084 s % 6.41/1.17 % (2671473)Peak memory usage: 14 MB % 6.41/1.17 % (2671473)Instructions burned: 131 (million) % 6.41/1.17 % (2671499)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2831841753:i=1179_2998 on theBenchmark for (2998ds/1179Mi) % 6.41/1.17 % (2671502)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=44906916:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi) % 6.41/1.17 % (2671502)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 6.41/1.17 % (2671502)Terminated due to inappropriate strategy. % 6.41/1.17 % (2671502)------------------------------ % 6.41/1.17 % (2671502)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.41/1.17 % (2671502)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.41/1.17 % (2671502)CaDiCaL version: 2.1.3 % 6.41/1.17 % (2671502)Termination reason: Inappropriate % 6.41/1.17 % (2671502)Time elapsed: 0.007 s % 6.41/1.17 % (2671502)Peak memory usage: 10 MB % 6.41/1.17 % (2671502)Instructions burned: 16 (million) % 6.41/1.17 % (2671502)------------------------------ % 6.41/1.17 % (2671502)------------------------------ % 6.41/1.17 % (2671476)Instruction limit reached! % 6.41/1.17 % (2671476)------------------------------ % 6.41/1.17 % (2671476)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.41/1.17 % (2671476)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.41/1.17 % (2671476)CaDiCaL version: 2.1.3 % 6.41/1.17 % (2671476)Termination reason: Instruction limit % 6.41/1.17 % (2671476)Termination phase: Saturation % 6.41/1.17 % (2671476)Time elapsed: 0.085 s % 6.41/1.17 % (2671476)Peak memory usage: 13 MB % 6.41/1.17 % (2671476)Instructions burned: 183 (million) % 6.41/1.17 % (2671511)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=3705884211: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) % 22.19/3.46 % (2671512)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2815987425:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi) % 22.19/3.46 % (2671480)Instruction limit reached! % 22.19/3.46 % (2671480)------------------------------ % 22.19/3.46 % (2671480)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.19/3.46 % (2671480)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.19/3.46 % (2671480)CaDiCaL version: 2.1.3 % 22.19/3.46 % (2671480)Termination reason: Instruction limit % 22.19/3.46 % (2671480)Termination phase: Saturation % 22.19/3.46 % (2671480)Time elapsed: 0.282 s % 22.19/3.46 % (2671480)Peak memory usage: 15 MB % 22.19/3.46 % (2671480)Instructions burned: 477 (million) % 22.19/3.46 % (2671563)fmb+10_1_sil=64000:random_seed=4008455119:i=22061:nm=2:gsp=on_2995 on theBenchmark for (2995ds/22061Mi) % 22.19/3.46 % (2671563)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 22.19/3.46 % (2671563)Terminated due to inappropriate strategy. % 22.19/3.46 % (2671563)------------------------------ % 22.19/3.46 % (2671563)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.19/3.46 % (2671563)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.19/3.46 % (2671563)CaDiCaL version: 2.1.3 % 22.19/3.46 % (2671563)Termination reason: Inappropriate % 22.19/3.46 % (2671563)Time elapsed: 0.007 s % 22.19/3.46 % (2671563)Peak memory usage: 10 MB % 22.19/3.46 % (2671563)Instructions burned: 15 (million) % 22.19/3.46 % (2671563)------------------------------ % 22.19/3.46 % (2671563)------------------------------ % 22.19/3.46 % (2671568)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2224362065:i=9515:nm=5_2995 on theBenchmark for (2995ds/9515Mi) % 22.19/3.46 % (2671568)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 22.19/3.46 % (2671568)Terminated due to inappropriate strategy. % 22.19/3.46 % (2671568)------------------------------ % 22.19/3.46 % (2671568)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.19/3.46 % (2671568)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.19/3.46 % (2671568)CaDiCaL version: 2.1.3 % 22.19/3.46 % (2671568)Termination reason: Inappropriate % 22.19/3.46 % (2671568)Time elapsed: 0.007 s % 22.19/3.46 % (2671568)Peak memory usage: 10 MB % 22.19/3.46 % (2671568)Instructions burned: 14 (million) % 22.19/3.46 % (2671568)------------------------------ % 22.19/3.46 % (2671568)------------------------------ % 22.19/3.46 % (2671475)Instruction limit reached! % 22.19/3.46 % (2671475)------------------------------ % 22.19/3.46 % (2671475)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.19/3.46 % (2671475)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.19/3.46 % (2671475)CaDiCaL version: 2.1.3 % 22.19/3.46 % (2671475)Termination reason: Instruction limit % 22.19/3.46 % (2671475)Termination phase: Saturation % 22.19/3.46 % (2671475)Time elapsed: 0.370 s % 22.19/3.46 % (2671475)Peak memory usage: 18 MB % 22.19/3.46 % (2671475)Instructions burned: 686 (million) % 22.19/3.46 % (2671574)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3488319443:fmbsr=1.7:i=920_2995 on theBenchmark for (2995ds/920Mi) % 22.19/3.46 % (2671574)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 22.19/3.46 % (2671574)Terminated due to inappropriate strategy. % 22.19/3.46 % (2671574)------------------------------ % 22.19/3.46 % (2671574)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.19/3.46 % (2671574)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.19/3.46 % (2671574)CaDiCaL version: 2.1.3 % 22.19/3.46 % (2671574)Termination reason: Inappropriate % 22.19/3.46 % (2671574)Time elapsed: 0.006 s % 22.19/3.46 % (2671574)Peak memory usage: 10 MB % 22.19/3.46 % (2671574)Instructions burned: 14 (million) % 22.19/3.46 % (2671574)------------------------------ % 22.19/3.46 % (2671574)------------------------------ % 22.19/3.46 % (2671580)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=899003951:i=5131_2995 on theBenchmark for (2995ds/5131Mi) % 22.19/3.46 % (2671584)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3878237804:i=1472:ins=7:fdi=8:gsp=on_2994 on theBenchmark for (2994ds/1472Mi) % 22.19/3.46 % (2671511)Instruction limit reached! % 22.19/3.46 % (2671511)------------------------------ % 38.79/5.75 % (2671511)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 38.79/5.75 % (2671511)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 38.79/5.75 % (2671511)CaDiCaL version: 2.1.3 % 38.79/5.75 % (2671511)Termination reason: Instruction limit % 38.79/5.75 % (2671511)Termination phase: Saturation % 38.79/5.75 % (2671511)Time elapsed: 0.433 s % 38.79/5.75 % (2671511)Peak memory usage: 19 MB % 38.79/5.75 % (2671511)Instructions burned: 693 (million) % 38.79/5.75 % (2671606)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=662659527:i=6324_2993 on theBenchmark for (2993ds/6324Mi) % 38.79/5.75 % (2671606)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 38.79/5.75 % (2671606)Terminated due to inappropriate strategy. % 38.79/5.75 % (2671606)------------------------------ % 38.79/5.75 % (2671606)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 38.79/5.75 % (2671606)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 38.79/5.75 % (2671606)CaDiCaL version: 2.1.3 % 38.79/5.75 % (2671606)Termination reason: Inappropriate % 38.79/5.75 % (2671606)Time elapsed: 0.009 s % 38.79/5.75 % (2671606)Peak memory usage: 11 MB % 38.79/5.75 % (2671606)Instructions burned: 19 (million) % 38.79/5.75 % (2671606)------------------------------ % 38.79/5.75 % (2671606)------------------------------ % 38.79/5.75 % (2671608)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=607113311:fmbsr=2.30978:i=2174_2993 on theBenchmark for (2993ds/2174Mi) % 38.79/5.75 % (2671512)Instruction limit reached! % 38.79/5.75 % (2671512)------------------------------ % 38.79/5.75 % (2671512)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 38.79/5.75 % (2671512)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 38.79/5.75 % (2671512)CaDiCaL version: 2.1.3 % 38.79/5.75 % (2671512)Termination reason: Instruction limit % 38.79/5.75 % (2671512)Termination phase: Saturation % 38.79/5.75 % (2671512)Time elapsed: 0.481 s % 38.79/5.75 % (2671512)Peak memory usage: 21 MB % 38.79/5.75 % (2671512)Instructions burned: 880 (million) % 38.79/5.75 % (2671608)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 38.79/5.75 % (2671608)Terminated due to inappropriate strategy. % 38.79/5.75 % (2671608)------------------------------ % 38.79/5.75 % (2671608)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 38.79/5.75 % (2671608)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 38.79/5.75 % (2671608)CaDiCaL version: 2.1.3 % 38.79/5.75 % (2671608)Termination reason: Inappropriate % 38.79/5.75 % (2671608)Time elapsed: 0.006 s % 38.79/5.75 % (2671608)Peak memory usage: 10 MB % 38.79/5.75 % (2671608)Instructions burned: 14 (million) % 38.79/5.75 % (2671608)------------------------------ % 38.79/5.75 % (2671608)------------------------------ % 38.79/5.75 % (2671610)ott-2_1_sil=16000:newcnf=on:random_seed=2510100791:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2992 on theBenchmark for (2992ds/869Mi) % 38.79/5.75 % (2671611)ott+10_1_sil=32000:tgt=ground:random_seed=1981380907:i=5114:av=off_2992 on theBenchmark for (2992ds/5114Mi) % 38.79/5.75 % (2671499)Instruction limit reached! % 38.79/5.75 % (2671499)------------------------------ % 38.79/5.75 % (2671499)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 38.79/5.75 % (2671499)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 38.79/5.75 % (2671499)CaDiCaL version: 2.1.3 % 38.79/5.75 % (2671499)Termination reason: Instruction limit % 38.79/5.75 % (2671499)Termination phase: Saturation % 38.79/5.75 % (2671499)Time elapsed: 0.720 s % 38.79/5.75 % (2671499)Peak memory usage: 18 MB % 38.79/5.75 % (2671499)Instructions burned: 1180 (million) % 38.79/5.75 % (2671622)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=3800776816:i=54282_2990 on theBenchmark for (2990ds/54282Mi) % 38.79/5.75 % (2671622)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 38.79/5.75 % (2671622)Terminated due to inappropriate strategy. % 38.79/5.75 % (2671622)------------------------------ % 38.79/5.75 % (2671622)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 38.79/5.75 % (2671622)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 38.79/5.75 % (2671622)CaDiCaL version: 2.1.3 % 38.79/5.75 % (2671622)Termination reason: Inappropriate % 38.79/5.75 % (2671622)Time elapsed: 0.009 s % 38.79/5.75 % (2671622)Peak memory usage: 11 MB % 38.79/5.75 % (2671622)Instructions burned: 19 (million) % 113.40/16.26 % (2671622)------------------------------ % 113.40/16.26 % (2671622)------------------------------ % 113.40/16.26 % (2671630)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=1648615429:i=3512:aac=none_2990 on theBenchmark for (2990ds/3512Mi) % 113.40/16.26 % (2671610)Instruction limit reached! % 113.40/16.26 % (2671610)------------------------------ % 113.40/16.26 % (2671610)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 113.40/16.26 % (2671610)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 113.40/16.26 % (2671610)CaDiCaL version: 2.1.3 % 113.40/16.26 % (2671610)Termination reason: Instruction limit % 113.40/16.26 % (2671610)Termination phase: Saturation % 113.40/16.26 % (2671610)Time elapsed: 0.535 s % 113.40/16.26 % (2671610)Peak memory usage: 18 MB % 113.40/16.26 % (2671610)Instructions burned: 870 (million) % 113.40/16.26 % (2671665)dis+21_1_sil=32000:sas=cadical:random_seed=231017248:i=3773:amm=off_2987 on theBenchmark for (2987ds/3773Mi) % 113.40/16.26 % (2671584)Instruction limit reached! % 113.40/16.26 % (2671584)------------------------------ % 113.40/16.26 % (2671584)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 113.40/16.26 % (2671584)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 113.40/16.26 % (2671584)CaDiCaL version: 2.1.3 % 113.40/16.26 % (2671584)Termination reason: Instruction limit % 113.40/16.26 % (2671584)Termination phase: Saturation % 113.40/16.26 % (2671584)Time elapsed: 0.780 s % 113.40/16.26 % (2671584)Peak memory usage: 30 MB % 113.40/16.26 % (2671584)Instructions burned: 1472 (million) % 113.40/16.26 % (2671667)ott+11_1_sil=16000:gs=on:random_seed=2410448982:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2986 on theBenchmark for (2986ds/2251Mi) % 113.40/16.26 % (2671667)Instruction limit reached! % 113.40/16.26 % (2671667)------------------------------ % 113.40/16.26 % (2671667)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 113.40/16.26 % (2671667)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 113.40/16.26 % (2671667)CaDiCaL version: 2.1.3 % 113.40/16.26 % (2671667)Termination reason: Instruction limit % 113.40/16.26 % (2671667)Termination phase: Saturation % 113.40/16.26 % (2671667)Time elapsed: 1.247 s % 113.40/16.26 % (2671667)Peak memory usage: 23 MB % 113.40/16.26 % (2671667)Instructions burned: 2251 (million) % 113.40/16.26 % (2671669)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=3461261729:fmbsr=1.6:i=67534_2974 on theBenchmark for (2974ds/67534Mi) % 113.40/16.26 % (2671669)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 113.40/16.26 % (2671669)Terminated due to inappropriate strategy. % 113.40/16.26 % (2671669)------------------------------ % 113.40/16.26 % (2671669)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 113.40/16.26 % (2671669)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 113.40/16.26 % (2671669)CaDiCaL version: 2.1.3 % 113.40/16.26 % (2671669)Termination reason: Inappropriate % 113.40/16.26 % (2671669)Time elapsed: 0.007 s % 113.40/16.26 % (2671669)Peak memory usage: 10 MB % 113.40/16.26 % (2671669)Instructions burned: 14 (million) % 113.40/16.26 % (2671669)------------------------------ % 113.40/16.26 % (2671669)------------------------------ % 113.40/16.26 % (2671671)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=2898605184:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2974 on theBenchmark for (2974ds/4591Mi) % 113.40/16.26 % (2671630)Instruction limit reached! % 113.40/16.26 % (2671630)------------------------------ % 113.40/16.26 % (2671630)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 113.40/16.26 % (2671630)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 113.40/16.26 % (2671630)CaDiCaL version: 2.1.3 % 113.40/16.26 % (2671630)Termination reason: Instruction limit % 113.40/16.26 % (2671630)Termination phase: Saturation % 113.40/16.26 % (2671630)Time elapsed: 1.887 s % 113.40/16.26 % (2671630)Peak memory usage: 29 MB % 113.40/16.26 % (2671630)Instructions burned: 3512 (million) % 113.40/16.26 % (2671673)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=3644215382:i=29340_2971 on theBenchmark for (2971ds/29340Mi) % 113.40/16.26 % (2671580)Instruction limit reached! % 113.40/16.26 % (2671580)------------------------------ % 113.40/16.26 % (2671580)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 113.40/16.26 % (2671580)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 113.40/16.26 % (2671580)CaDiCaL version: 2.1.3 % 113.40/16.26 % (2671580)Termination reason: Instruction limit % 156.07/22.27 % (2671580)Termination phase: Saturation % 156.07/22.27 % (2671580)Time elapsed: 2.722 s % 156.07/22.27 % (2671580)Peak memory usage: 40 MB % 156.07/22.27 % (2671580)Instructions burned: 5132 (million) % 156.07/22.27 % (2671675)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=713538442:i=5211_2967 on theBenchmark for (2967ds/5211Mi) % 156.07/22.27 % (2671665)Instruction limit reached! % 156.07/22.27 % (2671665)------------------------------ % 156.07/22.27 % (2671665)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 156.07/22.27 % (2671665)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 156.07/22.27 % (2671665)CaDiCaL version: 2.1.3 % 156.07/22.27 % (2671665)Termination reason: Instruction limit % 156.07/22.27 % (2671665)Termination phase: Saturation % 156.07/22.27 % (2671665)Time elapsed: 2.058 s % 156.07/22.27 % (2671665)Peak memory usage: 31 MB % 156.07/22.27 % (2671665)Instructions burned: 3774 (million) % 156.07/22.27 % (2671677)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=477586411:i=5497:nm=2_2966 on theBenchmark for (2966ds/5497Mi) % 156.07/22.27 % (2671677)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 156.07/22.27 % (2671677)Terminated due to inappropriate strategy. % 156.07/22.27 % (2671677)------------------------------ % 156.07/22.27 % (2671677)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 156.07/22.27 % (2671677)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 156.07/22.27 % (2671677)CaDiCaL version: 2.1.3 % 156.07/22.27 % (2671677)Termination reason: Inappropriate % 156.07/22.27 % (2671677)Time elapsed: 0.009 s % 156.07/22.27 % (2671677)Peak memory usage: 11 MB % 156.07/22.27 % (2671677)Instructions burned: 18 (million) % 156.07/22.27 % (2671677)------------------------------ % 156.07/22.27 % (2671677)------------------------------ % 156.07/22.27 % (2671679)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=4018109903:fmbsr=2:i=46332_2966 on theBenchmark for (2966ds/46332Mi) % 156.07/22.27 % (2671679)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 156.07/22.27 % (2671679)Terminated due to inappropriate strategy. % 156.07/22.27 % (2671679)------------------------------ % 156.07/22.27 % (2671679)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 156.07/22.27 % (2671679)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 156.07/22.27 % (2671679)CaDiCaL version: 2.1.3 % 156.07/22.27 % (2671679)Termination reason: Inappropriate % 156.07/22.27 % (2671679)Time elapsed: 0.007 s % 156.07/22.27 % (2671679)Peak memory usage: 10 MB % 156.07/22.27 % (2671679)Instructions burned: 14 (million) % 156.07/22.27 % (2671679)------------------------------ % 156.07/22.27 % (2671679)------------------------------ % 156.07/22.27 % (2671681)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=2606140753:i=14071_2965 on theBenchmark for (2965ds/14071Mi) % 156.07/22.27 % (2671681)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 156.07/22.27 % (2671681)Terminated due to inappropriate strategy. % 156.07/22.27 % (2671681)------------------------------ % 156.07/22.27 % (2671681)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 156.07/22.27 % (2671681)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 156.07/22.27 % (2671681)CaDiCaL version: 2.1.3 % 156.07/22.27 % (2671681)Termination reason: Inappropriate % 156.07/22.27 % (2671681)Time elapsed: 0.007 s % 156.07/22.27 % (2671681)Peak memory usage: 10 MB % 156.07/22.27 % (2671681)Instructions burned: 14 (million) % 156.07/22.27 % (2671681)------------------------------ % 156.07/22.27 % (2671681)------------------------------ % 156.07/22.27 % (2671683)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=899835279:i=22565:add=on:rawr=on_2965 on theBenchmark for (2965ds/22565Mi) % 156.07/22.27 % (2671611)Instruction limit reached! % 156.07/22.27 % (2671611)------------------------------ % 156.07/22.27 % (2671611)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 156.07/22.27 % (2671611)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 156.07/22.27 % (2671611)CaDiCaL version: 2.1.3 % 156.07/22.27 % (2671611)Termination reason: Instruction limit % 156.07/22.27 % (2671611)Termination phase: Saturation % 156.07/22.27 % (2671611)Time elapsed: 3.166 s % 156.07/22.27 % (2671611)Peak memory usage: 30 MB % 156.07/22.27 % (2671611)Instructions burned: 5115 (million) % 156.07/22.27 % (2671687)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=244110059:i=8173:av=off_2960 on theBenchmark for (2960ds/8173Mi) % 156.07/22.27 % (2671671)Instruction limit reached! % 158.18/22.56 % (2671671)------------------------------ % 158.18/22.56 % (2671671)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 158.18/22.56 % (2671671)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 158.18/22.56 % (2671671)CaDiCaL version: 2.1.3 % 158.18/22.56 % (2671671)Termination reason: Instruction limit % 158.18/22.56 % (2671671)Termination phase: Saturation % 158.18/22.56 % (2671671)Time elapsed: 2.900 s % 158.18/22.56 % (2671671)Peak memory usage: 44 MB % 158.18/22.56 % (2671671)Instructions burned: 4592 (million) % 158.18/22.56 % (2671689)dis+10_16:1_sil=16000:random_seed=2945207361:i=9155:fsr=off_2944 on theBenchmark for (2944ds/9155Mi) % 158.18/22.56 % (2671675)Instruction limit reached! % 158.18/22.56 % (2671675)------------------------------ % 158.18/22.56 % (2671675)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 158.18/22.56 % (2671675)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 158.18/22.56 % (2671675)CaDiCaL version: 2.1.3 % 158.18/22.56 % (2671675)Termination reason: Instruction limit % 158.18/22.56 % (2671675)Termination phase: Saturation % 158.18/22.56 % (2671675)Time elapsed: 2.746 s % 158.18/22.56 % (2671675)Peak memory usage: 48 MB % 158.18/22.56 % (2671675)Instructions burned: 5211 (million) % 158.18/22.56 % (2671691)ott-3_8_sil=64000:random_seed=786822399:i=20139:bs=on_2939 on theBenchmark for (2939ds/20139Mi) % 158.18/22.56 % (2671687)Instruction limit reached! % 158.18/22.56 % (2671687)------------------------------ % 158.18/22.56 % (2671687)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 158.18/22.56 % (2671687)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 158.18/22.56 % (2671687)CaDiCaL version: 2.1.3 % 158.18/22.56 % (2671687)Termination reason: Instruction limit % 158.18/22.56 % (2671687)Termination phase: Saturation % 158.18/22.56 % (2671687)Time elapsed: 5.232 s % 158.18/22.56 % (2671687)Peak memory usage: 44 MB % 158.18/22.56 % (2671687)Instructions burned: 8174 (million) % 158.18/22.56 % (2671693)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=1636759115:fmbsr=2:i=32576_2908 on theBenchmark for (2908ds/32576Mi) % 158.18/22.56 % (2671693)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 158.18/22.56 % (2671693)Terminated due to inappropriate strategy. % 158.18/22.56 % (2671693)------------------------------ % 158.18/22.56 % (2671693)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 158.18/22.56 % (2671693)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 158.18/22.56 % (2671693)CaDiCaL version: 2.1.3 % 158.18/22.56 % (2671693)Termination reason: Inappropriate % 158.18/22.56 % (2671693)Time elapsed: 0.009 s % 158.18/22.56 % (2671693)Peak memory usage: 11 MB % 158.18/22.56 % (2671693)Instructions burned: 19 (million) % 158.18/22.56 % (2671693)------------------------------ % 158.18/22.56 % (2671693)------------------------------ % 158.18/22.56 % (2671695)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=1810028054:i=11404_2908 on theBenchmark for (2908ds/11404Mi) % 158.18/22.56 % (2671689)Instruction limit reached! % 158.18/22.56 % (2671689)------------------------------ % 158.18/22.56 % (2671689)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 158.18/22.56 % (2671689)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 158.18/22.56 % (2671689)CaDiCaL version: 2.1.3 % 158.18/22.56 % (2671689)Termination reason: Instruction limit % 158.18/22.56 % (2671689)Termination phase: Saturation % 158.18/22.56 % (2671689)Time elapsed: 4.845 s % 158.18/22.56 % (2671689)Peak memory usage: 50 MB % 158.18/22.56 % (2671689)Instructions burned: 9155 (million) % 158.18/22.56 % (2671697)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=2137668879:i=14134_2896 on theBenchmark for (2896ds/14134Mi) % 158.18/22.56 % (2671683)Instruction limit reached! % 158.18/22.56 % (2671683)------------------------------ % 158.18/22.56 % (2671683)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 158.18/22.56 % (2671683)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 158.18/22.56 % (2671683)CaDiCaL version: 2.1.3 % 158.18/22.56 % (2671683)Termination reason: Instruction limit % 158.18/22.56 % (2671683)Termination phase: Saturation % 158.18/22.56 % (2671683)Time elapsed: 9.107 s % 158.18/22.56 % (2671683)Peak memory usage: 23 MB % 158.18/22.56 % (2671683)Instructions burned: 22565 (million) % 158.18/22.56 % (2671699)dis+33_16_sil=32000:sac=on:random_seed=2818974449:i=15851:nm=0_2874 on theBenchmark for (2874ds/15851Mi) % 158.18/22.56 % (2671691)Instruction limit reached! % 158.18/22.56 % (2671691)------------------------------ % 158.18/22.56 % (2671691)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 228.61/32.43 % (2671691)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 228.61/32.43 % (2671691)CaDiCaL version: 2.1.3 % 228.61/32.43 % (2671691)Termination reason: Instruction limit % 228.61/32.43 % (2671691)Termination phase: Saturation % 228.61/32.43 % (2671691)Time elapsed: 9.998 s % 228.61/32.43 % (2671691)Peak memory usage: 50 MB % 228.61/32.43 % (2671691)Instructions burned: 20139 (million) % 228.61/32.43 % (2671979)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=2393598656:avsq=on:i=17627:add=on:amm=off_2839 on theBenchmark for (2839ds/17627Mi) % 228.61/32.43 % (2671695)Instruction limit reached! % 228.61/32.43 % (2671695)------------------------------ % 228.61/32.43 % (2671695)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 228.61/32.43 % (2671695)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 228.61/32.43 % (2671695)CaDiCaL version: 2.1.3 % 228.61/32.43 % (2671695)Termination reason: Instruction limit % 228.61/32.43 % (2671695)Termination phase: Saturation % 228.61/32.43 % (2671695)Time elapsed: 7.964 s % 228.61/32.43 % (2671695)Peak memory usage: 44 MB % 228.61/32.43 % (2671695)Instructions burned: 11405 (million) % 228.61/32.43 % (2672031)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=2720258608:s2a=on:i=53295_2828 on theBenchmark for (2828ds/53295Mi) % 228.61/32.43 % (2671673)Instruction limit reached! % 228.61/32.43 % (2671673)------------------------------ % 228.61/32.43 % (2671673)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 228.61/32.43 % (2671673)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 228.61/32.43 % (2671673)CaDiCaL version: 2.1.3 % 228.61/32.43 % (2671673)Termination reason: Instruction limit % 228.61/32.43 % (2671673)Termination phase: Saturation % 228.61/32.43 % (2671673)Time elapsed: 16.558 s % 228.61/32.43 % (2671673)Peak memory usage: 73 MB % 228.61/32.43 % (2671673)Instructions burned: 29340 (million) % 228.61/32.43 % (2672092)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=309061491:i=26857:ins=20_2805 on theBenchmark for (2805ds/26857Mi) % 228.61/32.43 % (2672092)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 228.61/32.43 % (2672092)Terminated due to inappropriate strategy. % 228.61/32.43 % (2672092)------------------------------ % 228.61/32.43 % (2672092)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 228.61/32.43 % (2672092)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 228.61/32.43 % (2672092)CaDiCaL version: 2.1.3 % 228.61/32.43 % (2672092)Termination reason: Inappropriate % 228.61/32.43 % (2672092)Time elapsed: 0.013 s % 228.61/32.43 % (2672092)Peak memory usage: 11 MB % 228.61/32.43 % (2672092)Instructions burned: 14 (million) % 228.61/32.43 % (2672092)------------------------------ % 228.61/32.43 % (2672092)------------------------------ % 228.61/32.43 % (2672096)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=3148668685:i=28120:bs=on:fsr=off_2804 on theBenchmark for (2804ds/28120Mi) % 228.61/32.43 % (2671697)Instruction limit reached! % 228.61/32.43 % (2671697)------------------------------ % 228.61/32.43 % (2671697)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 228.61/32.43 % (2671697)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 228.61/32.43 % (2671697)CaDiCaL version: 2.1.3 % 228.61/32.43 % (2671697)Termination reason: Instruction limit % 228.61/32.43 % (2671697)Termination phase: Saturation % 228.61/32.43 % (2671697)Time elapsed: 11.515 s % 228.61/32.43 % (2671697)Peak memory usage: 53 MB % 228.61/32.43 % (2671697)Instructions burned: 14134 (million) % 228.61/32.43 % (2672145)fmb+10_1_sil=256000:fmbss=7:random_seed=4152828998:fmbsr=1.6:i=182295_2780 on theBenchmark for (2780ds/182295Mi) % 228.61/32.43 % (2672145)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 228.61/32.43 % (2672145)Terminated due to inappropriate strategy. % 228.61/32.43 % (2672145)------------------------------ % 228.61/32.43 % (2672145)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 228.61/32.43 % (2672145)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 228.61/32.43 % (2672145)CaDiCaL version: 2.1.3 % 228.61/32.43 % (2672145)Termination reason: Inappropriate % 228.61/32.43 % (2672145)Time elapsed: 0.012 s % 228.61/32.43 % (2672145)Peak memory usage: 11 MB % 228.61/32.43 % (2672145)Instructions burned: 14 (million) % 228.61/32.43 % (2672145)------------------------------ % 228.61/32.43 % (2672145)------------------------------ % 228.61/32.43 % (2672147)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=126953719:i=44625:gsp=on_2780 on theBenchmark for (2780ds/44625Mi) % 249.92/35.45 % (2672147)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 249.92/35.45 % (2672147)Terminated due to inappropriate strategy. % 249.92/35.45 % (2672147)------------------------------ % 249.92/35.45 % (2672147)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 249.92/35.45 % (2672147)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 249.92/35.45 % (2672147)CaDiCaL version: 2.1.3 % 249.92/35.45 % (2672147)Termination reason: Inappropriate % 249.92/35.45 % (2672147)Time elapsed: 0.016 s % 249.92/35.45 % (2672147)Peak memory usage: 11 MB % 249.92/35.45 % (2672147)Instructions burned: 18 (million) % 249.92/35.45 % (2672147)------------------------------ % 249.92/35.45 % (2672147)------------------------------ % 249.92/35.45 % (2672149)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=1783109256:i=160505_2779 on theBenchmark for (2779ds/160505Mi) % 249.92/35.45 % (2672149)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 249.92/35.45 % (2672149)Terminated due to inappropriate strategy. % 249.92/35.45 % (2672149)------------------------------ % 249.92/35.45 % (2672149)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 249.92/35.45 % (2672149)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 249.92/35.45 % (2672149)CaDiCaL version: 2.1.3 % 249.92/35.45 % (2672149)Termination reason: Inappropriate % 249.92/35.45 % (2672149)Time elapsed: 0.015 s % 249.92/35.45 % (2672149)Peak memory usage: 11 MB % 249.92/35.45 % (2672149)Instructions burned: 14 (million) % 249.92/35.45 % (2672149)------------------------------ % 249.92/35.45 % (2672149)------------------------------ % 249.92/35.45 % (2672153)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=664415604:fmbsr=1.3:i=225729_2778 on theBenchmark for (2778ds/225729Mi) % 249.92/35.45 % (2672153)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 249.92/35.45 % (2672153)Terminated due to inappropriate strategy. % 249.92/35.45 % (2672153)------------------------------ % 249.92/35.45 % (2672153)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 249.92/35.45 % (2672153)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 249.92/35.45 % (2672153)CaDiCaL version: 2.1.3 % 249.92/35.45 % (2672153)Termination reason: Inappropriate % 249.92/35.45 % (2672153)Time elapsed: 0.018 s % 249.92/35.45 % (2672153)Peak memory usage: 11 MB % 249.92/35.45 % (2672153)Instructions burned: 14 (million) % 249.92/35.45 % (2672153)------------------------------ % 249.92/35.45 % (2672153)------------------------------ % 249.92/35.45 % (2672156)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=2961907408:fmbsr=2:i=185024:ins=7_2778 on theBenchmark for (2778ds/185024Mi) % 249.92/35.45 % (2672156)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 249.92/35.45 % (2672156)Terminated due to inappropriate strategy. % 249.92/35.45 % (2672156)------------------------------ % 249.92/35.45 % (2672156)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 249.92/35.45 % (2672156)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 249.92/35.45 % (2672156)CaDiCaL version: 2.1.3 % 249.92/35.45 % (2672156)Termination reason: Inappropriate % 249.92/35.45 % (2672156)Time elapsed: 0.013 s % 249.92/35.45 % (2672156)Peak memory usage: 10 MB % 249.92/35.45 % (2672156)Instructions burned: 14 (million) % 249.92/35.45 % (2672156)------------------------------ % 249.92/35.45 % (2672156)------------------------------ % 249.92/35.45 % (2672159)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=329635435:rtra=on_2777 on theBenchmark for (2777ds/0Mi) % 249.92/35.45 % (2672159)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 249.92/35.45 % (2672159)Terminated due to inappropriate strategy. % 249.92/35.45 % (2672159)------------------------------ % 249.92/35.45 % (2672159)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 249.92/35.45 % (2672159)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 249.92/35.45 % (2672159)CaDiCaL version: 2.1.3 % 249.92/35.45 % (2672159)Termination reason: Inappropriate % 249.92/35.45 % (2672159)Time elapsed: 0.018 s % 249.92/35.45 % (2672159)Peak memory usage: 11 MB % 249.92/35.45 % (2672159)Instructions burned: 20 (million) % 249.92/35.45 % (2672159)------------------------------ % 249.92/35.45 % (2672159)------------------------------ % 249.92/35.45 % (2672161)% WARNING: option uhcvi not known. % 249.92/35.45 % (2672161)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3389584277:i=271062:add=off:rtra=on:rawr=on_2777 on theBenchmark for (2777ds/271062Mi) % 289.10/41.03 % (2671699)Instruction limit reached! % 289.10/41.03 % (2671699)------------------------------ % 289.10/41.03 % (2671699)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 289.10/41.03 % (2671699)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 289.10/41.03 % (2671699)CaDiCaL version: 2.1.3 % 289.10/41.03 % (2671699)Termination reason: Instruction limit % 289.10/41.03 % (2671699)Termination phase: Saturation % 289.10/41.03 % (2671699)Time elapsed: 13.309 s % 289.10/41.03 % (2671699)Peak memory usage: 71 MB % 289.10/41.03 % (2671699)Instructions burned: 15851 (million) % 289.10/41.03 % (2672198)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1379334157:i=176048:add=on:rtra=on:rawr=on_2740 on theBenchmark for (2740ds/176048Mi) % 289.10/41.03 % (2671979)Instruction limit reached! % 289.10/41.03 % (2671979)------------------------------ % 289.10/41.03 % (2671979)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 289.10/41.03 % (2671979)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 289.10/41.03 % (2671979)CaDiCaL version: 2.1.3 % 289.10/41.03 % (2671979)Termination reason: Instruction limit % 289.10/41.03 % (2671979)Termination phase: Saturation % 289.10/41.03 % (2671979)Time elapsed: 14.845 s % 289.10/41.03 % (2671979)Peak memory usage: 154 MB % 289.10/41.03 % (2671979)Instructions burned: 17627 (million) % 289.10/41.03 % (2672226)dis+10_1_sil=32000:si=on:sp=arity:random_seed=1123997561:i=206:fgj=on:rtra=on_2690 on theBenchmark for (2690ds/206Mi) % 289.10/41.03 % (2672226)Instruction limit reached! % 289.10/41.03 % (2672226)------------------------------ % 289.10/41.03 % (2672226)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 289.10/41.03 % (2672226)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 289.10/41.03 % (2672226)CaDiCaL version: 2.1.3 % 289.10/41.03 % (2672226)Termination reason: Instruction limit % 289.10/41.03 % (2672226)Termination phase: Saturation % 289.10/41.03 % (2672226)Time elapsed: 0.227 s % 289.10/41.03 % (2672226)Peak memory usage: 14 MB % 289.10/41.03 % (2672226)Instructions burned: 206 (million) % 289.10/41.03 % (2672228)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=1039755777:i=232:rtra=on_2687 on theBenchmark for (2687ds/232Mi) % 289.10/41.03 % (2672228)Instruction limit reached! % 289.10/41.03 % (2672228)------------------------------ % 289.10/41.03 % (2672228)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 289.10/41.03 % (2672228)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 289.10/41.03 % (2672228)CaDiCaL version: 2.1.3 % 289.10/41.03 % (2672228)Termination reason: Instruction limit % 289.10/41.03 % (2672228)Termination phase: Saturation % 289.10/41.03 % (2672228)Time elapsed: 0.197 s % 289.10/41.03 % (2672228)Peak memory usage: 14 MB % 289.10/41.03 % (2672228)Instructions burned: 232 (million) % 289.10/41.03 % (2672230)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=364361145:i=262:rtra=on_2685 on theBenchmark for (2685ds/262Mi) % 289.10/41.03 % (2672230)Instruction limit reached! % 289.10/41.03 % (2672230)------------------------------ % 289.10/41.03 % (2672230)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 289.10/41.03 % (2672230)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 289.10/41.03 % (2672230)CaDiCaL version: 2.1.3 % 289.10/41.03 % (2672230)Termination reason: Instruction limit % 289.10/41.03 % (2672230)Termination phase: Saturation % 289.10/41.03 % (2672230)Time elapsed: 0.278 s % 289.10/41.03 % (2672230)Peak memory usage: 15 MB % 289.10/41.03 % (2672230)Instructions burned: 262 (million) % 289.10/41.03 % (2672232)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=3502559344:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2682 on theBenchmark for (2682ds/318Mi) % 289.10/41.03 % (2672232)Instruction limit reached! % 289.10/41.03 % (2672232)------------------------------ % 289.10/41.03 % (2672232)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 289.10/41.03 % (2672232)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 289.10/41.03 % (2672232)CaDiCaL version: 2.1.3 % 289.10/41.03 % (2672232)Termination reason: Instruction limit % 289.10/41.03 % (2672232)Termination phase: Saturation % 289.10/41.03 % (2672232)Time elapsed: 0.377 s % 289.10/41.03 % (2672232)Peak memory usage: 16 MB % 289.10/41.03 % (2672232)Instructions burned: 318 (million) % 289.10/41.03 % (2672235)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=3439539801:i=1428:nmTerminated % 300.45/42.54 % Vampire exiting % 300.45/42.54 Terminated %------------------------------------------------------------------------------