%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWC470_1 : TPTP v9.3.1. Bugfixed v9.1.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % Computer : n017.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 29 01:06:02 PM UTC 2026 % Result : Timeout 300.00s 42.54s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWC470_1 : TPTP v9.3.1. Bugfixed v9.1.0. % 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.09/0.24 % Computer : n017.cluster.edu % 0.09/0.24 % Model : x86_64 x86_64 % 0.09/0.24 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.24 % Memory : 8046.5625MB % 0.09/0.24 % OS : Linux 6.8.0-71-generic % 0.09/0.24 % CPULimit : 300 % 0.09/0.24 % WCLimit : 300 % 0.09/0.24 % DateTime : Mon Sep 28 09:35:36 UTC 2026 % 0.09/0.24 % CPUTime : % 0.09/0.24 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.25/0.29 Running first-order model finding % 0.25/0.29 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 6.74/1.30 % (3432420)Will run a generic schedule for satisfiability detection. % 6.74/1.30 % (3432426)% WARNING: option uhcvi not known. % 6.74/1.30 % (3432426)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3223653661:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 6.74/1.30 % (3432431)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3172083642:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 6.74/1.30 % (3432425)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=940769127_2999 on theBenchmark for (2999ds/0Mi) % 6.74/1.30 % (3432425)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 6.74/1.30 % (3432425)Terminated due to inappropriate strategy. % 6.74/1.30 % (3432425)------------------------------ % 6.74/1.30 % (3432425)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.74/1.30 % (3432425)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.74/1.30 % (3432425)CaDiCaL version: 2.1.3 % 6.74/1.30 % (3432425)Termination reason: Inappropriate % 6.74/1.30 % (3432425)Time elapsed: 0.001 s % 6.74/1.30 % (3432425)Peak memory usage: 10 MB % 6.74/1.30 % (3432425)Instructions burned: 1 (million) % 6.74/1.30 % (3432428)dis+10_1_sil=32000:sp=arity:random_seed=3305922794:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 6.74/1.30 % (3432425)------------------------------ % 6.74/1.30 % (3432425)------------------------------ % 6.74/1.30 % (3432427)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=504127871:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 6.74/1.30 % (3432429)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=280293824:i=116_2999 on theBenchmark for (2999ds/116Mi) % 6.74/1.30 % (3432430)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1518930225:i=131_2999 on theBenchmark for (2999ds/131Mi) % 6.74/1.30 % (3432436)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3997902399:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 6.74/1.30 % (3432436)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 6.74/1.30 % (3432436)Terminated due to inappropriate strategy. % 6.74/1.30 % (3432436)------------------------------ % 6.74/1.30 % (3432436)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.74/1.30 % (3432436)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.74/1.30 % (3432436)CaDiCaL version: 2.1.3 % 6.74/1.30 % (3432436)Termination reason: Inappropriate % 6.74/1.30 % (3432436)Time elapsed: 0.002 s % 6.74/1.30 % (3432436)Peak memory usage: 10 MB % 6.74/1.30 % (3432436)Instructions burned: 1 (million) % 6.74/1.30 % (3432436)------------------------------ % 6.74/1.30 % (3432436)------------------------------ % 6.74/1.30 % (3432441)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=297570550:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 6.74/1.30 % (3432428)Instruction limit reached! % 6.74/1.30 % (3432428)------------------------------ % 6.74/1.30 % (3432428)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.74/1.30 % (3432428)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.74/1.30 % (3432428)CaDiCaL version: 2.1.3 % 6.74/1.30 % (3432428)Termination reason: Instruction limit % 6.74/1.30 % (3432428)Termination phase: Saturation % 6.74/1.30 % (3432428)Time elapsed: 0.102 s % 6.74/1.30 % (3432428)Peak memory usage: 12 MB % 6.74/1.30 % (3432428)Instructions burned: 103 (million) % 6.74/1.30 % (3432429)Instruction limit reached! % 6.74/1.30 % (3432429)------------------------------ % 6.74/1.30 % (3432429)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.74/1.30 % (3432429)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.74/1.30 % (3432429)CaDiCaL version: 2.1.3 % 6.74/1.30 % (3432429)Termination reason: Instruction limit % 6.74/1.30 % (3432429)Termination phase: Saturation % 6.74/1.30 % (3432429)Time elapsed: 0.110 s % 6.74/1.30 % (3432429)Peak memory usage: 12 MB % 6.74/1.30 % (3432429)Instructions burned: 116 (million) % 6.74/1.30 % (3432430)Instruction limit reached! % 6.74/1.30 % (3432430)------------------------------ % 6.74/1.30 % (3432430)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.74/1.30 % (3432430)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.74/1.30 % (3432430)CaDiCaL version: 2.1.3 % 6.74/1.30 % (3432430)Termination reason: Instruction limit % 8.23/1.76 % (3432430)Termination phase: Saturation % 8.23/1.76 % (3432430)Time elapsed: 0.131 s % 8.23/1.76 % (3432430)Peak memory usage: 12 MB % 8.23/1.76 % (3432430)Instructions burned: 131 (million) % 8.23/1.76 % (3432443)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=3595463531:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi) % 8.23/1.76 % (3432444)ott-21_1_sil=16000:fs=off:random_seed=3004172494:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 8.23/1.76 % (3432431)Instruction limit reached! % 8.23/1.76 % (3432431)------------------------------ % 8.23/1.76 % (3432431)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.23/1.76 % (3432431)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.23/1.76 % (3432431)CaDiCaL version: 2.1.3 % 8.23/1.76 % (3432431)Termination reason: Instruction limit % 8.23/1.76 % (3432431)Termination phase: Saturation % 8.23/1.76 % (3432431)Time elapsed: 0.157 s % 8.23/1.76 % (3432431)Peak memory usage: 13 MB % 8.23/1.76 % (3432431)Instructions burned: 159 (million) % 8.23/1.76 % (3432445)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3324823434:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 8.23/1.76 % (3432448)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=527544217:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 8.23/1.76 % (3432448)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 8.23/1.76 % (3432448)Terminated due to inappropriate strategy. % 8.23/1.76 % (3432448)------------------------------ % 8.23/1.76 % (3432448)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.23/1.76 % (3432448)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.23/1.76 % (3432448)CaDiCaL version: 2.1.3 % 8.23/1.76 % (3432448)Termination reason: Inappropriate % 8.23/1.76 % (3432448)Time elapsed: 0.001 s % 8.23/1.76 % (3432448)Peak memory usage: 11 MB % 8.23/1.76 % (3432448)Instructions burned: 1 (million) % 8.23/1.76 % (3432448)------------------------------ % 8.23/1.76 % (3432448)------------------------------ % 8.23/1.76 % (3432451)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2107155291:i=1179_2997 on theBenchmark for (2997ds/1179Mi) % 8.23/1.76 % (3432441)Instruction limit reached! % 8.23/1.76 % (3432441)------------------------------ % 8.23/1.76 % (3432441)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.23/1.76 % (3432441)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.23/1.76 % (3432441)CaDiCaL version: 2.1.3 % 8.23/1.76 % (3432441)Termination reason: Instruction limit % 8.23/1.76 % (3432441)Termination phase: Saturation % 8.23/1.76 % (3432441)Time elapsed: 0.144 s % 8.23/1.76 % (3432441)Peak memory usage: 13 MB % 8.23/1.76 % (3432441)Instructions burned: 131 (million) % 8.23/1.76 % (3432453)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=718493126:i=889:ins=1_2997 on theBenchmark for (2997ds/889Mi) % 8.23/1.76 % (3432453)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 8.23/1.76 % (3432453)Terminated due to inappropriate strategy. % 8.23/1.76 % (3432453)------------------------------ % 8.23/1.76 % (3432453)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.23/1.76 % (3432453)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.23/1.76 % (3432453)CaDiCaL version: 2.1.3 % 8.23/1.76 % (3432453)Termination reason: Inappropriate % 8.23/1.76 % (3432453)Time elapsed: 0.001 s % 8.23/1.76 % (3432453)Peak memory usage: 10 MB % 8.23/1.76 % (3432453)Instructions burned: 1 (million) % 8.23/1.76 % (3432453)------------------------------ % 8.23/1.76 % (3432453)------------------------------ % 8.23/1.76 % (3432455)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=125001665:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2997 on theBenchmark for (2997ds/692Mi) % 8.23/1.76 % (3432444)Instruction limit reached! % 8.23/1.76 % (3432444)------------------------------ % 8.23/1.76 % (3432444)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.23/1.76 % (3432444)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.23/1.76 % (3432444)CaDiCaL version: 2.1.3 % 8.23/1.76 % (3432444)Termination reason: Instruction limit % 8.23/1.76 % (3432444)Termination phase: Saturation % 36.98/5.53 % (3432444)Time elapsed: 0.143 s % 36.98/5.53 % (3432444)Peak memory usage: 12 MB % 36.98/5.53 % (3432444)Instructions burned: 180 (million) % 36.98/5.53 % (3432457)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2356285211:i=879:kws=inv_precedence:fsr=off_2996 on theBenchmark for (2996ds/879Mi) % 36.98/5.53 % (3432445)Instruction limit reached! % 36.98/5.53 % (3432445)------------------------------ % 36.98/5.53 % (3432445)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 36.98/5.53 % (3432445)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 36.98/5.53 % (3432445)CaDiCaL version: 2.1.3 % 36.98/5.53 % (3432445)Termination reason: Instruction limit % 36.98/5.53 % (3432445)Termination phase: Saturation % 36.98/5.53 % (3432445)Time elapsed: 0.477 s % 36.98/5.53 % (3432445)Peak memory usage: 14 MB % 36.98/5.53 % (3432445)Instructions burned: 477 (million) % 36.98/5.53 % (3432443)Instruction limit reached! % 36.98/5.53 % (3432443)------------------------------ % 36.98/5.53 % (3432443)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 36.98/5.53 % (3432443)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 36.98/5.53 % (3432443)CaDiCaL version: 2.1.3 % 36.98/5.53 % (3432443)Termination reason: Instruction limit % 36.98/5.53 % (3432443)Termination phase: Saturation % 36.98/5.53 % (3432443)Time elapsed: 0.532 s % 36.98/5.53 % (3432443)Peak memory usage: 17 MB % 36.98/5.53 % (3432443)Instructions burned: 684 (million) % 36.98/5.53 % (3432459)fmb+10_1_sil=64000:random_seed=1916304576:i=22061:nm=2:gsp=on_2993 on theBenchmark for (2993ds/22061Mi) % 36.98/5.53 % (3432459)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 36.98/5.53 % (3432459)Terminated due to inappropriate strategy. % 36.98/5.53 % (3432459)------------------------------ % 36.98/5.53 % (3432459)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 36.98/5.53 % (3432459)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 36.98/5.53 % (3432459)CaDiCaL version: 2.1.3 % 36.98/5.53 % (3432459)Termination reason: Inappropriate % 36.98/5.53 % (3432459)Time elapsed: 0.002 s % 36.98/5.53 % (3432459)Peak memory usage: 10 MB % 36.98/5.53 % (3432459)Instructions burned: 1 (million) % 36.98/5.53 % (3432459)------------------------------ % 36.98/5.53 % (3432459)------------------------------ % 36.98/5.53 % (3432460)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=952772631:i=9515:nm=5_2992 on theBenchmark for (2992ds/9515Mi) % 36.98/5.53 % (3432460)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 36.98/5.53 % (3432460)Terminated due to inappropriate strategy. % 36.98/5.53 % (3432460)------------------------------ % 36.98/5.53 % (3432460)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 36.98/5.53 % (3432460)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 36.98/5.53 % (3432460)CaDiCaL version: 2.1.3 % 36.98/5.53 % (3432460)Termination reason: Inappropriate % 36.98/5.53 % (3432460)Time elapsed: 0.002 s % 36.98/5.53 % (3432460)Peak memory usage: 10 MB % 36.98/5.53 % (3432460)Instructions burned: 1 (million) % 36.98/5.53 % (3432460)------------------------------ % 36.98/5.53 % (3432460)------------------------------ % 36.98/5.53 % (3432462)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3760065915:fmbsr=1.7:i=920_2992 on theBenchmark for (2992ds/920Mi) % 36.98/5.53 % (3432462)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 36.98/5.53 % (3432462)Terminated due to inappropriate strategy. % 36.98/5.53 % (3432462)------------------------------ % 36.98/5.53 % (3432462)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 36.98/5.53 % (3432462)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 36.98/5.53 % (3432462)CaDiCaL version: 2.1.3 % 36.98/5.53 % (3432462)Termination reason: Inappropriate % 36.98/5.53 % (3432462)Time elapsed: 0.001 s % 36.98/5.53 % (3432462)Peak memory usage: 10 MB % 36.98/5.53 % (3432462)Instructions burned: 1 (million) % 36.98/5.53 % (3432462)------------------------------ % 36.98/5.53 % (3432462)------------------------------ % 36.98/5.53 % (3432466)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3784025600:i=1472:ins=7:fdi=8:gsp=on_2992 on theBenchmark for (2992ds/1472Mi) % 36.98/5.53 % (3432464)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1119597855:i=5131_2992 on theBenchmark for (2992ds/5131Mi) % 36.98/5.53 % (3432455)Instruction limit reached! % 36.98/5.53 % (3432455)------------------------------ % 61.11/8.99 % (3432455)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 61.11/8.99 % (3432455)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 61.11/8.99 % (3432455)CaDiCaL version: 2.1.3 % 61.11/8.99 % (3432455)Termination reason: Instruction limit % 61.11/8.99 % (3432455)Termination phase: Saturation % 61.11/8.99 % (3432455)Time elapsed: 0.693 s % 61.11/8.99 % (3432455)Peak memory usage: 21 MB % 61.11/8.99 % (3432455)Instructions burned: 693 (million) % 61.11/8.99 % (3432469)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3426219815:i=6324_2989 on theBenchmark for (2989ds/6324Mi) % 61.11/8.99 % (3432469)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 61.11/8.99 % (3432469)Terminated due to inappropriate strategy. % 61.11/8.99 % (3432469)------------------------------ % 61.11/8.99 % (3432469)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 61.11/8.99 % (3432469)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 61.11/8.99 % (3432469)CaDiCaL version: 2.1.3 % 61.11/8.99 % (3432469)Termination reason: Inappropriate % 61.11/8.99 % (3432469)Time elapsed: 0.001 s % 61.11/8.99 % (3432469)Peak memory usage: 10 MB % 61.11/8.99 % (3432469)Instructions burned: 1 (million) % 61.11/8.99 % (3432469)------------------------------ % 61.11/8.99 % (3432469)------------------------------ % 61.11/8.99 % (3432471)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1061656399:fmbsr=2.30978:i=2174_2989 on theBenchmark for (2989ds/2174Mi) % 61.11/8.99 % (3432471)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 61.11/8.99 % (3432471)Terminated due to inappropriate strategy. % 61.11/8.99 % (3432471)------------------------------ % 61.11/8.99 % (3432471)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 61.11/8.99 % (3432471)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 61.11/8.99 % (3432471)CaDiCaL version: 2.1.3 % 61.11/8.99 % (3432471)Termination reason: Inappropriate % 61.11/8.99 % (3432471)Time elapsed: 0.001 s % 61.11/8.99 % (3432471)Peak memory usage: 10 MB % 61.11/8.99 % (3432471)Instructions burned: 1 (million) % 61.11/8.99 % (3432471)------------------------------ % 61.11/8.99 % (3432471)------------------------------ % 61.11/8.99 % (3432473)ott-2_1_sil=16000:newcnf=on:random_seed=885352261:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2989 on theBenchmark for (2989ds/869Mi) % 61.11/8.99 % (3432457)Instruction limit reached! % 61.11/8.99 % (3432457)------------------------------ % 61.11/8.99 % (3432457)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 61.11/8.99 % (3432457)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 61.11/8.99 % (3432457)CaDiCaL version: 2.1.3 % 61.11/8.99 % (3432457)Termination reason: Instruction limit % 61.11/8.99 % (3432457)Termination phase: Saturation % 61.11/8.99 % (3432457)Time elapsed: 0.821 s % 61.11/8.99 % (3432457)Peak memory usage: 18 MB % 61.11/8.99 % (3432457)Instructions burned: 879 (million) % 61.11/8.99 % (3432475)ott+10_1_sil=32000:tgt=ground:random_seed=2860497699:i=5114:av=off_2988 on theBenchmark for (2988ds/5114Mi) % 61.11/8.99 % (3432451)Instruction limit reached! % 61.11/8.99 % (3432451)------------------------------ % 61.11/8.99 % (3432451)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 61.11/8.99 % (3432451)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 61.11/8.99 % (3432451)CaDiCaL version: 2.1.3 % 61.11/8.99 % (3432451)Termination reason: Instruction limit % 61.11/8.99 % (3432451)Termination phase: Saturation % 61.11/8.99 % (3432451)Time elapsed: 1.185 s % 61.11/8.99 % (3432451)Peak memory usage: 21 MB % 61.11/8.99 % (3432451)Instructions burned: 1179 (million) % 61.11/8.99 % (3432477)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=3945798851:i=54282_2985 on theBenchmark for (2985ds/54282Mi) % 61.11/8.99 % (3432477)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 61.11/8.99 % (3432477)Terminated due to inappropriate strategy. % 61.11/8.99 % (3432477)------------------------------ % 61.11/8.99 % (3432477)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 61.11/8.99 % (3432477)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 61.11/8.99 % (3432477)CaDiCaL version: 2.1.3 % 61.11/8.99 % (3432477)Termination reason: Inappropriate % 61.11/8.99 % (3432477)Time elapsed: 0.002 s % 61.11/8.99 % (3432477)Peak memory usage: 10 MB % 61.11/8.99 % (3432477)Instructions burned: 1 (million) % 188.56/26.90 % (3432477)------------------------------ % 188.56/26.90 % (3432477)------------------------------ % 188.56/26.90 % (3432479)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=2205879382:i=3512:aac=none_2985 on theBenchmark for (2985ds/3512Mi) % 188.56/26.90 % (3432473)Instruction limit reached! % 188.56/26.90 % (3432473)------------------------------ % 188.56/26.90 % (3432473)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 188.56/26.90 % (3432473)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 188.56/26.90 % (3432473)CaDiCaL version: 2.1.3 % 188.56/26.90 % (3432473)Termination reason: Instruction limit % 188.56/26.90 % (3432473)Termination phase: Saturation % 188.56/26.90 % (3432473)Time elapsed: 0.833 s % 188.56/26.90 % (3432473)Peak memory usage: 15 MB % 188.56/26.90 % (3432473)Instructions burned: 870 (million) % 188.56/26.90 % (3432483)dis+21_1_sil=32000:sas=cadical:random_seed=395038890:i=3773:amm=off_2980 on theBenchmark for (2980ds/3773Mi) % 188.56/26.90 % (3432466)Instruction limit reached! % 188.56/26.90 % (3432466)------------------------------ % 188.56/26.90 % (3432466)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 188.56/26.90 % (3432466)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 188.56/26.90 % (3432466)CaDiCaL version: 2.1.3 % 188.56/26.90 % (3432466)Termination reason: Instruction limit % 188.56/26.90 % (3432466)Termination phase: Saturation % 188.56/26.90 % (3432466)Time elapsed: 1.351 s % 188.56/26.90 % (3432466)Peak memory usage: 23 MB % 188.56/26.90 % (3432466)Instructions burned: 1472 (million) % 188.56/26.90 % (3432485)ott+11_1_sil=16000:gs=on:random_seed=2484037836:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2978 on theBenchmark for (2978ds/2251Mi) % 188.56/26.90 % (3432485)Instruction limit reached! % 188.56/26.90 % (3432485)------------------------------ % 188.56/26.90 % (3432485)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 188.56/26.90 % (3432485)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 188.56/26.90 % (3432485)CaDiCaL version: 2.1.3 % 188.56/26.90 % (3432485)Termination reason: Instruction limit % 188.56/26.90 % (3432485)Termination phase: Saturation % 188.56/26.90 % (3432485)Time elapsed: 2.126 s % 188.56/26.90 % (3432485)Peak memory usage: 24 MB % 188.56/26.90 % (3432485)Instructions burned: 2251 (million) % 188.56/26.90 % (3432491)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=3351186012:fmbsr=1.6:i=67534_2957 on theBenchmark for (2957ds/67534Mi) % 188.56/26.90 % (3432491)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 188.56/26.90 % (3432491)Terminated due to inappropriate strategy. % 188.56/26.90 % (3432491)------------------------------ % 188.56/26.90 % (3432491)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 188.56/26.90 % (3432491)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 188.56/26.90 % (3432491)CaDiCaL version: 2.1.3 % 188.56/26.90 % (3432491)Termination reason: Inappropriate % 188.56/26.90 % (3432491)Time elapsed: 0.002 s % 188.56/26.90 % (3432491)Peak memory usage: 11 MB % 188.56/26.90 % (3432491)Instructions burned: 1 (million) % 188.56/26.90 % (3432491)------------------------------ % 188.56/26.90 % (3432491)------------------------------ % 188.56/26.90 % (3432493)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=2479485222:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2956 on theBenchmark for (2956ds/4591Mi) % 188.56/26.90 % (3432479)Instruction limit reached! % 188.56/26.90 % (3432479)------------------------------ % 188.56/26.90 % (3432479)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 188.56/26.90 % (3432479)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 188.56/26.90 % (3432479)CaDiCaL version: 2.1.3 % 188.56/26.90 % (3432479)Termination reason: Instruction limit % 188.56/26.90 % (3432479)Termination phase: Saturation % 188.56/26.90 % (3432479)Time elapsed: 3.119 s % 188.56/26.90 % (3432479)Peak memory usage: 34 MB % 188.56/26.90 % (3432479)Instructions burned: 3512 (million) % 188.56/26.90 % (3432495)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=713382041:i=29340_2953 on theBenchmark for (2953ds/29340Mi) % 188.56/26.90 % (3432483)Instruction limit reached! % 188.56/26.90 % (3432483)------------------------------ % 188.56/26.90 % (3432483)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 188.56/26.90 % (3432483)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 188.56/26.90 % (3432483)CaDiCaL version: 2.1.3 % 188.56/26.90 % (3432483)Termination reason: Instruction limit % 212.27/30.15 % (3432483)Termination phase: Saturation % 212.27/30.15 % (3432483)Time elapsed: 3.289 s % 212.27/30.15 % (3432483)Peak memory usage: 31 MB % 212.27/30.15 % (3432483)Instructions burned: 3774 (million) % 212.27/30.15 % (3432497)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=3097641595:i=5211_2947 on theBenchmark for (2947ds/5211Mi) % 212.27/30.15 % (3432464)Instruction limit reached! % 212.27/30.15 % (3432464)------------------------------ % 212.27/30.15 % (3432464)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 212.27/30.15 % (3432464)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 212.27/30.15 % (3432464)CaDiCaL version: 2.1.3 % 212.27/30.15 % (3432464)Termination reason: Instruction limit % 212.27/30.15 % (3432464)Termination phase: Saturation % 212.27/30.15 % (3432464)Time elapsed: 4.736 s % 212.27/30.15 % (3432464)Peak memory usage: 41 MB % 212.27/30.15 % (3432464)Instructions burned: 5131 (million) % 212.27/30.15 % (3432499)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=2639564861:i=5497:nm=2_2944 on theBenchmark for (2944ds/5497Mi) % 212.27/30.15 % (3432499)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 212.27/30.15 % (3432499)Terminated due to inappropriate strategy. % 212.27/30.15 % (3432499)------------------------------ % 212.27/30.15 % (3432499)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 212.27/30.15 % (3432499)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 212.27/30.15 % (3432499)CaDiCaL version: 2.1.3 % 212.27/30.15 % (3432499)Termination reason: Inappropriate % 212.27/30.15 % (3432499)Time elapsed: 0.001 s % 212.27/30.15 % (3432499)Peak memory usage: 10 MB % 212.27/30.15 % (3432499)Instructions burned: 1 (million) % 212.27/30.15 % (3432499)------------------------------ % 212.27/30.15 % (3432499)------------------------------ % 212.27/30.15 % (3432501)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=1222945633:fmbsr=2:i=46332_2944 on theBenchmark for (2944ds/46332Mi) % 212.27/30.15 % (3432501)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 212.27/30.15 % (3432501)Terminated due to inappropriate strategy. % 212.27/30.15 % (3432501)------------------------------ % 212.27/30.15 % (3432501)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 212.27/30.16 % (3432501)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 212.27/30.16 % (3432501)CaDiCaL version: 2.1.3 % 212.27/30.16 % (3432501)Termination reason: Inappropriate % 212.27/30.16 % (3432501)Time elapsed: 0.001 s % 212.27/30.16 % (3432501)Peak memory usage: 10 MB % 212.27/30.16 % (3432501)Instructions burned: 1 (million) % 212.27/30.16 % (3432501)------------------------------ % 212.27/30.16 % (3432501)------------------------------ % 212.27/30.16 % (3432503)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=58876929:i=14071_2944 on theBenchmark for (2944ds/14071Mi) % 212.27/30.16 % (3432503)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 212.27/30.16 % (3432503)Terminated due to inappropriate strategy. % 212.27/30.16 % (3432503)------------------------------ % 212.27/30.16 % (3432503)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 212.27/30.16 % (3432503)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 212.27/30.16 % (3432503)CaDiCaL version: 2.1.3 % 212.27/30.16 % (3432503)Termination reason: Inappropriate % 212.27/30.16 % (3432503)Time elapsed: 0.001 s % 212.27/30.16 % (3432503)Peak memory usage: 10 MB % 212.27/30.16 % (3432503)Instructions burned: 1 (million) % 212.27/30.16 % (3432503)------------------------------ % 212.27/30.16 % (3432503)------------------------------ % 212.27/30.16 % (3432505)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2539975249:i=22565:add=on:rawr=on_2944 on theBenchmark for (2944ds/22565Mi) % 212.27/30.16 % (3432475)Instruction limit reached! % 212.27/30.16 % (3432475)------------------------------ % 212.27/30.16 % (3432475)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 212.27/30.16 % (3432475)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 212.27/30.16 % (3432475)CaDiCaL version: 2.1.3 % 212.27/30.16 % (3432475)Termination reason: Instruction limit % 212.27/30.16 % (3432475)Termination phase: Saturation % 212.27/30.16 % (3432475)Time elapsed: 5.268 s % 212.27/30.16 % (3432475)Peak memory usage: 42 MB % 212.27/30.16 % (3432475)Instructions burned: 5115 (million) % 212.27/30.16 % (3432507)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=1097407233:i=8173:av=off_2935 on theBenchmark for (2935ds/8173Mi) % 212.27/30.16 % (3432493)Instruction limit reached! % 212.69/30.26 % (3432493)------------------------------ % 212.69/30.26 % (3432493)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 212.69/30.26 % (3432493)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 212.69/30.26 % (3432493)CaDiCaL version: 2.1.3 % 212.69/30.26 % (3432493)Termination reason: Instruction limit % 212.69/30.26 % (3432493)Termination phase: Saturation % 212.69/30.26 % (3432493)Time elapsed: 4.347 s % 212.69/30.26 % (3432493)Peak memory usage: 36 MB % 212.69/30.26 % (3432493)Instructions burned: 4592 (million) % 212.69/30.26 % (3432525)dis+10_16:1_sil=16000:random_seed=1645614637:i=9155:fsr=off_2913 on theBenchmark for (2913ds/9155Mi) % 212.69/30.26 % (3432497)Instruction limit reached! % 212.69/30.26 % (3432497)------------------------------ % 212.69/30.26 % (3432497)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 212.69/30.26 % (3432497)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 212.69/30.26 % (3432497)CaDiCaL version: 2.1.3 % 212.69/30.26 % (3432497)Termination reason: Instruction limit % 212.69/30.26 % (3432497)Termination phase: Saturation % 212.69/30.26 % (3432497)Time elapsed: 4.635 s % 212.69/30.26 % (3432497)Peak memory usage: 51 MB % 212.69/30.26 % (3432497)Instructions burned: 5211 (million) % 212.69/30.26 % (3432527)ott-3_8_sil=64000:random_seed=3831672606:i=20139:bs=on_2901 on theBenchmark for (2901ds/20139Mi) % 212.69/30.26 % (3432507)Instruction limit reached! % 212.69/30.26 % (3432507)------------------------------ % 212.69/30.26 % (3432507)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 212.69/30.26 % (3432507)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 212.69/30.26 % (3432507)CaDiCaL version: 2.1.3 % 212.69/30.26 % (3432507)Termination reason: Instruction limit % 212.69/30.26 % (3432507)Termination phase: Saturation % 212.69/30.26 % (3432507)Time elapsed: 8.341 s % 212.69/30.26 % (3432507)Peak memory usage: 52 MB % 212.69/30.26 % (3432507)Instructions burned: 8173 (million) % 212.69/30.26 % (3432529)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=2165677237:fmbsr=2:i=32576_2851 on theBenchmark for (2851ds/32576Mi) % 212.69/30.26 % (3432529)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 212.69/30.26 % (3432529)Terminated due to inappropriate strategy. % 212.69/30.26 % (3432529)------------------------------ % 212.69/30.26 % (3432529)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 212.69/30.26 % (3432529)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 212.69/30.26 % (3432529)CaDiCaL version: 2.1.3 % 212.69/30.26 % (3432529)Termination reason: Inappropriate % 212.69/30.26 % (3432529)Time elapsed: 0.002 s % 212.69/30.26 % (3432529)Peak memory usage: 10 MB % 212.69/30.26 % (3432529)Instructions burned: 1 (million) % 212.69/30.26 % (3432529)------------------------------ % 212.69/30.26 % (3432529)------------------------------ % 212.69/30.26 % (3432531)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=2605650077:i=11404_2850 on theBenchmark for (2850ds/11404Mi) % 212.69/30.26 % (3432525)Instruction limit reached! % 212.69/30.26 % (3432525)------------------------------ % 212.69/30.26 % (3432525)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 212.69/30.26 % (3432525)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 212.69/30.26 % (3432525)CaDiCaL version: 2.1.3 % 212.69/30.26 % (3432525)Termination reason: Instruction limit % 212.69/30.26 % (3432525)Termination phase: Saturation % 212.69/30.26 % (3432525)Time elapsed: 8.262 s % 212.69/30.26 % (3432525)Peak memory usage: 52 MB % 212.69/30.26 % (3432525)Instructions burned: 9156 (million) % 212.69/30.26 % (3432541)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=3187441964:i=14134_2829 on theBenchmark for (2829ds/14134Mi) % 212.69/30.26 % (3432505)Instruction limit reached! % 212.69/30.26 % (3432505)------------------------------ % 212.69/30.26 % (3432505)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 212.69/30.26 % (3432505)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 212.69/30.26 % (3432505)CaDiCaL version: 2.1.3 % 212.69/30.26 % (3432505)Termination reason: Instruction limit % 212.69/30.26 % (3432505)Termination phase: Saturation % 212.69/30.26 % (3432505)Time elapsed: 15.995 s % 212.69/30.26 % (3432505)Peak memory usage: 146 MB % 212.69/30.26 % (3432505)Instructions burned: 22565 (million) % 212.69/30.26 % (3432557)dis+33_16_sil=32000:sac=on:random_seed=2609400271:i=15851:nm=0_2783 on theBenchmark for (2783ds/15851Mi) % 212.69/30.26 % (3432531)Instruction limit reached! % 212.69/30.26 % (3432531)------------------------------ % 212.69/30.26 % (3432531)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 253.05/36.00 % (3432531)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 253.05/36.00 % (3432531)CaDiCaL version: 2.1.3 % 253.05/36.00 % (3432531)Termination reason: Instruction limit % 253.05/36.00 % (3432531)Termination phase: Saturation % 253.05/36.00 % (3432531)Time elapsed: 11.653 s % 253.05/36.00 % (3432531)Peak memory usage: 71 MB % 253.05/36.00 % (3432531)Instructions burned: 11405 (million) % 253.05/36.00 % (3432581)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=1683948374:avsq=on:i=17627:add=on:amm=off_2733 on theBenchmark for (2733ds/17627Mi) % 253.05/36.00 % (3432495)Instruction limit reached! % 253.05/36.00 % (3432495)------------------------------ % 253.05/36.00 % (3432495)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 253.05/36.00 % (3432495)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 253.05/36.00 % (3432495)CaDiCaL version: 2.1.3 % 253.05/36.00 % (3432495)Termination reason: Instruction limit % 253.05/36.00 % (3432495)Termination phase: Saturation % 253.05/36.00 % (3432495)Time elapsed: 22.763 s % 253.05/36.00 % (3432495)Peak memory usage: 171 MB % 253.05/36.01 % (3432495)Instructions burned: 29341 (million) % 253.05/36.01 % (3432624)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=1516644539:s2a=on:i=53295_2725 on theBenchmark for (2725ds/53295Mi) % 253.05/36.01 % (3432527)Instruction limit reached! % 253.05/36.01 % (3432527)------------------------------ % 253.05/36.01 % (3432527)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 253.05/36.01 % (3432527)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 253.05/36.01 % (3432527)CaDiCaL version: 2.1.3 % 253.05/36.01 % (3432527)Termination reason: Instruction limit % 253.05/36.01 % (3432527)Termination phase: Saturation % 253.05/36.01 % (3432527)Time elapsed: 17.953 s % 253.05/36.01 % (3432527)Peak memory usage: 55 MB % 253.05/36.01 % (3432527)Instructions burned: 20141 (million) % 253.05/36.01 % (3432626)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=1179087921:i=26857:ins=20_2721 on theBenchmark for (2721ds/26857Mi) % 253.05/36.01 % (3432626)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 253.05/36.01 % (3432626)Terminated due to inappropriate strategy. % 253.05/36.01 % (3432626)------------------------------ % 253.05/36.01 % (3432626)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 253.05/36.01 % (3432626)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 253.05/36.01 % (3432626)CaDiCaL version: 2.1.3 % 253.05/36.01 % (3432626)Termination reason: Inappropriate % 253.05/36.01 % (3432626)Time elapsed: 0.001 s % 253.05/36.01 % (3432626)Peak memory usage: 10 MB % 253.05/36.01 % (3432626)Instructions burned: 1 (million) % 253.05/36.01 % (3432626)------------------------------ % 253.05/36.01 % (3432626)------------------------------ % 253.05/36.01 % (3432628)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=2641495612:i=28120:bs=on:fsr=off_2720 on theBenchmark for (2720ds/28120Mi) % 253.05/36.01 % (3432541)Instruction limit reached! % 253.05/36.01 % (3432541)------------------------------ % 253.05/36.01 % (3432541)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 253.05/36.01 % (3432541)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 253.05/36.01 % (3432541)CaDiCaL version: 2.1.3 % 253.05/36.01 % (3432541)Termination reason: Instruction limit % 253.05/36.01 % (3432541)Termination phase: Saturation % 253.05/36.01 % (3432541)Time elapsed: 12.745 s % 253.05/36.01 % (3432541)Peak memory usage: 72 MB % 253.05/36.01 % (3432541)Instructions burned: 14135 (million) % 253.05/36.01 % (3432730)fmb+10_1_sil=256000:fmbss=7:random_seed=3651508565:fmbsr=1.6:i=182295_2701 on theBenchmark for (2701ds/182295Mi) % 253.05/36.01 % (3432730)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 253.05/36.01 % (3432730)Terminated due to inappropriate strategy. % 253.05/36.01 % (3432730)------------------------------ % 253.05/36.01 % (3432730)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 253.05/36.01 % (3432730)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 253.05/36.01 % (3432730)CaDiCaL version: 2.1.3 % 253.05/36.01 % (3432730)Termination reason: Inappropriate % 253.05/36.01 % (3432730)Time elapsed: 0.001 s % 253.05/36.01 % (3432730)Peak memory usage: 10 MB % 253.05/36.01 % (3432730)Instructions burned: 1 (million) % 253.05/36.01 % (3432730)------------------------------ % 253.05/36.01 % (3432730)------------------------------ % 253.05/36.01 % (3432742)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=1051800576:i=44625:gsp=on_2701 on theBenchmark for (2701ds/44625Mi) % 265.39/37.77 % (3432742)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 265.39/37.77 % (3432742)Terminated due to inappropriate strategy. % 265.39/37.77 % (3432742)------------------------------ % 265.39/37.77 % (3432742)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 265.39/37.77 % (3432742)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 265.39/37.77 % (3432742)CaDiCaL version: 2.1.3 % 265.39/37.77 % (3432742)Termination reason: Inappropriate % 265.39/37.77 % (3432742)Time elapsed: 0.001 s % 265.39/37.77 % (3432742)Peak memory usage: 10 MB % 265.39/37.77 % (3432742)Instructions burned: 1 (million) % 265.39/37.77 % (3432742)------------------------------ % 265.39/37.77 % (3432742)------------------------------ % 265.39/37.77 % (3432748)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=1918020147:i=160505_2701 on theBenchmark for (2701ds/160505Mi) % 265.39/37.77 % (3432748)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 265.39/37.77 % (3432748)Terminated due to inappropriate strategy. % 265.39/37.77 % (3432748)------------------------------ % 265.39/37.77 % (3432748)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 265.39/37.77 % (3432748)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 265.39/37.77 % (3432748)CaDiCaL version: 2.1.3 % 265.39/37.77 % (3432748)Termination reason: Inappropriate % 265.39/37.77 % (3432748)Time elapsed: 0.001 s % 265.39/37.77 % (3432748)Peak memory usage: 10 MB % 265.39/37.77 % (3432748)Instructions burned: 1 (million) % 265.39/37.77 % (3432748)------------------------------ % 265.39/37.77 % (3432748)------------------------------ % 265.39/37.77 % (3432750)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=812543050:fmbsr=1.3:i=225729_2701 on theBenchmark for (2701ds/225729Mi) % 265.39/37.77 % (3432750)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 265.39/37.77 % (3432750)Terminated due to inappropriate strategy. % 265.39/37.77 % (3432750)------------------------------ % 265.39/37.77 % (3432750)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 265.39/37.77 % (3432750)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 265.39/37.77 % (3432750)CaDiCaL version: 2.1.3 % 265.39/37.77 % (3432750)Termination reason: Inappropriate % 265.39/37.77 % (3432750)Time elapsed: 0.001 s % 265.39/37.77 % (3432750)Peak memory usage: 10 MB % 265.39/37.77 % (3432750)Instructions burned: 1 (million) % 265.39/37.77 % (3432750)------------------------------ % 265.39/37.77 % (3432750)------------------------------ % 265.39/37.77 % (3432752)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=3140628489:fmbsr=2:i=185024:ins=7_2701 on theBenchmark for (2701ds/185024Mi) % 265.39/37.77 % (3432752)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 265.39/37.77 % (3432752)Terminated due to inappropriate strategy. % 265.39/37.77 % (3432752)------------------------------ % 265.39/37.77 % (3432752)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 265.39/37.77 % (3432752)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 265.39/37.77 % (3432752)CaDiCaL version: 2.1.3 % 265.39/37.77 % (3432752)Termination reason: Inappropriate % 265.39/37.77 % (3432752)Time elapsed: 0.001 s % 265.39/37.77 % (3432752)Peak memory usage: 11 MB % 265.39/37.77 % (3432752)Instructions burned: 1 (million) % 265.39/37.77 % (3432752)------------------------------ % 265.39/37.77 % (3432752)------------------------------ % 265.39/37.77 % (3432754)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=2608973708:rtra=on_2700 on theBenchmark for (2700ds/0Mi) % 265.39/37.77 % (3432754)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 265.39/37.77 % (3432754)Terminated due to inappropriate strategy. % 265.39/37.77 % (3432754)------------------------------ % 265.39/37.77 % (3432754)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 265.39/37.77 % (3432754)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 265.39/37.77 % (3432754)CaDiCaL version: 2.1.3 % 265.39/37.77 % (3432754)Termination reason: Inappropriate % 265.39/37.77 % (3432754)Time elapsed: 0.001 s % 265.39/37.77 % (3432754)Peak memory usage: 10 MB % 265.39/37.77 % (3432754)Instructions burned: 1 (million) % 265.39/37.77 % (3432754)------------------------------ % 265.39/37.77 % (3432754)------------------------------ % 265.39/37.77 % (3432756)% WARNING: option uhcvi not known. % 265.39/37.77 % (3432756)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=4031262621:i=271062:add=off:rtra=on:rawr=on_2700 on theBenchmark for (2700ds/271062Mi) % 283.67/40.25 % (3432557)Instruction limit reached! % 283.67/40.25 % (3432557)------------------------------ % 283.67/40.25 % (3432557)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 283.67/40.25 % (3432557)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 283.67/40.25 % (3432557)CaDiCaL version: 2.1.3 % 283.67/40.25 % (3432557)Termination reason: Instruction limit % 283.67/40.25 % (3432557)Termination phase: Saturation % 283.67/40.25 % (3432557)Time elapsed: 9.500 s % 283.67/40.25 % (3432557)Peak memory usage: 203 MB % 283.67/40.25 % (3432557)Instructions burned: 15853 (million) % 283.67/40.25 % (3432758)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1265128899:i=176048:add=on:rtra=on:rawr=on_2687 on theBenchmark for (2687ds/176048Mi) % 283.67/40.25 % (3432581)Instruction limit reached! % 283.67/40.25 % (3432581)------------------------------ % 283.67/40.25 % (3432581)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 283.67/40.25 % (3432581)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 283.67/40.25 % (3432581)CaDiCaL version: 2.1.3 % 283.67/40.25 % (3432581)Termination reason: Instruction limit % 283.67/40.25 % (3432581)Termination phase: Saturation % 283.67/40.25 % (3432581)Time elapsed: 8.307 s % 283.67/40.25 % (3432581)Peak memory usage: 233 MB % 283.67/40.25 % (3432581)Instructions burned: 17628 (million) % 283.67/40.25 % (3432760)dis+10_1_sil=32000:si=on:sp=arity:random_seed=2157816373:i=206:fgj=on:rtra=on_2650 on theBenchmark for (2650ds/206Mi) % 283.67/40.25 % (3432760)Instruction limit reached! % 283.67/40.25 % (3432760)------------------------------ % 283.67/40.25 % (3432760)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 283.67/40.25 % (3432760)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 283.67/40.25 % (3432760)CaDiCaL version: 2.1.3 % 283.67/40.25 % (3432760)Termination reason: Instruction limit % 283.67/40.25 % (3432760)Termination phase: Saturation % 283.67/40.25 % (3432760)Time elapsed: 0.125 s % 283.67/40.25 % (3432760)Peak memory usage: 13 MB % 283.67/40.25 % (3432760)Instructions burned: 207 (million) % 283.67/40.25 % (3432762)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=2468937412:i=232:rtra=on_2648 on theBenchmark for (2648ds/232Mi) % 283.67/40.25 % (3432762)Instruction limit reached! % 283.67/40.25 % (3432762)------------------------------ % 283.67/40.25 % (3432762)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 283.67/40.25 % (3432762)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 283.67/40.25 % (3432762)CaDiCaL version: 2.1.3 % 283.67/40.25 % (3432762)Termination reason: Instruction limit % 283.67/40.25 % (3432762)Termination phase: Saturation % 283.67/40.25 % (3432762)Time elapsed: 0.149 s % 283.67/40.25 % (3432762)Peak memory usage: 13 MB % 283.67/40.25 % (3432762)Instructions burned: 232 (million) % 283.67/40.25 % (3432764)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=2502297280:i=262:rtra=on_2647 on theBenchmark for (2647ds/262Mi) % 283.67/40.25 % (3432764)Instruction limit reached! % 283.67/40.25 % (3432764)------------------------------ % 283.67/40.25 % (3432764)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 283.67/40.25 % (3432764)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 283.67/40.25 % (3432764)CaDiCaL version: 2.1.3 % 283.67/40.25 % (3432764)Termination reason: Instruction limit % 283.67/40.25 % (3432764)Termination phase: Saturation % 283.67/40.25 % (3432764)Time elapsed: 0.164 s % 283.67/40.25 % (3432764)Peak memory usage: 14 MB % 283.67/40.25 % (3432764)Instructions burned: 262 (million) % 283.67/40.25 % (3432766)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=890715062:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2645 on theBenchmark for (2645ds/318Mi) % 283.67/40.25 % (3432766)Instruction limit reached! % 283.67/40.25 % (3432766)------------------------------ % 283.67/40.25 % (3432766)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 283.67/40.25 % (3432766)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 283.67/40.25 % (3432766)CaDiCaL version: 2.1.3 % 283.67/40.25 % (3432766)Termination reason: Instruction limit % 283.67/40.25 % (3432766)Termination phase: Saturation % 283.67/40.25 % (3432766)Time elapsed: 0.187 s % 283.67/40.25 % (3432766)Peak memory usage: 14 MB % 283.67/40.25 % (3432766)Instructions burned: 319 (million) % 283.67/40.25 % (3432768)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=1499255779:i=1428:nm=2:rtra=on_2643Terminated % 300.00/42.54 % Vampire exiting %------------------------------------------------------------------------------