%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWX119_1 : TPTP v9.3.1. Released v9.1.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % Computer : n002.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 29 01:46:31 PM UTC 2026 % Result : Timeout 297.72s 42.16s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWX119_1 : TPTP v9.3.1. Released v9.1.0. % 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.10/0.21 % Computer : n002.cluster.edu % 0.10/0.21 % Model : x86_64 x86_64 % 0.10/0.21 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.21 % Memory : 8046.5625MB % 0.10/0.21 % OS : Linux 6.8.0-71-generic % 0.10/0.21 % CPULimit : 300 % 0.10/0.22 % WCLimit : 300 % 0.10/0.22 % DateTime : Mon Sep 28 15:04:37 UTC 2026 % 0.10/0.22 % CPUTime : % 0.10/0.22 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.10/0.27 Running first-order model finding % 0.10/0.27 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 % 7.04/1.30 % (422654)Will run a generic schedule for satisfiability detection. % 7.04/1.30 % (422660)% WARNING: option uhcvi not known. % 7.04/1.30 % (422660)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3434131588:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 7.04/1.30 % (422659)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=4155345970_2999 on theBenchmark for (2999ds/0Mi) % 7.04/1.30 % (422659)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 7.04/1.30 % (422659)Terminated due to inappropriate strategy. % 7.04/1.30 % (422659)------------------------------ % 7.04/1.30 % (422659)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.04/1.30 % (422659)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.04/1.30 % (422659)CaDiCaL version: 2.1.3 % 7.04/1.30 % (422659)Termination reason: Inappropriate % 7.04/1.30 % (422659)Time elapsed: 0.002 s % 7.04/1.30 % (422659)Peak memory usage: 11 MB % 7.04/1.30 % (422659)Instructions burned: 2 (million) % 7.04/1.30 % (422659)------------------------------ % 7.04/1.30 % (422659)------------------------------ % 7.04/1.30 % (422663)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1836769726:i=116_2999 on theBenchmark for (2999ds/116Mi) % 7.04/1.30 % (422661)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3238668072:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 7.04/1.30 % (422664)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1381004678:i=131_2999 on theBenchmark for (2999ds/131Mi) % 7.04/1.30 % (422662)dis+10_1_sil=32000:sp=arity:random_seed=334981259:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 7.04/1.30 % (422665)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1925511304:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 7.04/1.30 % (422668)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1159079708:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 7.04/1.30 % (422668)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 7.04/1.30 % (422668)Terminated due to inappropriate strategy. % 7.04/1.30 % (422668)------------------------------ % 7.04/1.30 % (422668)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.04/1.30 % (422668)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.04/1.30 % (422668)CaDiCaL version: 2.1.3 % 7.04/1.30 % (422668)Termination reason: Inappropriate % 7.04/1.30 % (422668)Time elapsed: 0.001 s % 7.04/1.30 % (422668)Peak memory usage: 11 MB % 7.04/1.30 % (422668)Instructions burned: 2 (million) % 7.04/1.30 % (422668)------------------------------ % 7.04/1.30 % (422668)------------------------------ % 7.04/1.30 % (422675)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2514349390:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 7.04/1.30 % (422662)Instruction limit reached! % 7.04/1.30 % (422662)------------------------------ % 7.04/1.30 % (422662)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.04/1.30 % (422662)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.04/1.30 % (422662)CaDiCaL version: 2.1.3 % 7.04/1.30 % (422662)Termination reason: Instruction limit % 7.04/1.30 % (422662)Termination phase: Saturation % 7.04/1.30 % (422662)Time elapsed: 0.109 s % 7.04/1.30 % (422662)Peak memory usage: 13 MB % 7.04/1.30 % (422662)Instructions burned: 104 (million) % 7.04/1.30 % (422663)Instruction limit reached! % 7.04/1.30 % (422663)------------------------------ % 7.04/1.30 % (422663)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.04/1.30 % (422663)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.04/1.30 % (422663)CaDiCaL version: 2.1.3 % 7.04/1.30 % (422663)Termination reason: Instruction limit % 7.04/1.30 % (422663)Termination phase: Saturation % 7.04/1.30 % (422663)Time elapsed: 0.116 s % 7.04/1.30 % (422663)Peak memory usage: 13 MB % 7.04/1.30 % (422663)Instructions burned: 116 (million) % 7.04/1.30 % (422677)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=882777385:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi) % 7.04/1.30 % (422664)Instruction limit reached! % 7.04/1.30 % (422664)------------------------------ % 7.04/1.30 % (422664)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 13.81/2.27 % (422664)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.81/2.27 % (422664)CaDiCaL version: 2.1.3 % 13.81/2.27 % (422664)Termination reason: Instruction limit % 13.81/2.27 % (422664)Termination phase: Saturation % 13.81/2.27 % (422664)Time elapsed: 0.137 s % 13.81/2.27 % (422664)Peak memory usage: 13 MB % 13.81/2.27 % (422664)Instructions burned: 132 (million) % 13.81/2.27 % (422678)ott-21_1_sil=16000:fs=off:random_seed=3651638058:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 13.81/2.27 % (422680)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=4000344740:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 13.81/2.27 % (422665)Instruction limit reached! % 13.81/2.27 % (422665)------------------------------ % 13.81/2.27 % (422665)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 13.81/2.27 % (422665)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.81/2.27 % (422665)CaDiCaL version: 2.1.3 % 13.81/2.27 % (422665)Termination reason: Instruction limit % 13.81/2.27 % (422665)Termination phase: Saturation % 13.81/2.27 % (422665)Time elapsed: 0.184 s % 13.81/2.27 % (422665)Peak memory usage: 14 MB % 13.81/2.27 % (422665)Instructions burned: 159 (million) % 13.81/2.27 % (422675)Instruction limit reached! % 13.81/2.27 % (422675)------------------------------ % 13.81/2.27 % (422675)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 13.81/2.27 % (422675)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.81/2.27 % (422675)CaDiCaL version: 2.1.3 % 13.81/2.27 % (422675)Termination reason: Instruction limit % 13.81/2.27 % (422675)Termination phase: Saturation % 13.81/2.27 % (422675)Time elapsed: 0.151 s % 13.81/2.27 % (422675)Peak memory usage: 13 MB % 13.81/2.27 % (422675)Instructions burned: 132 (million) % 13.81/2.27 % (422683)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3682147710:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi) % 13.81/2.27 % (422683)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 13.81/2.27 % (422683)Terminated due to inappropriate strategy. % 13.81/2.27 % (422683)------------------------------ % 13.81/2.27 % (422683)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 13.81/2.27 % (422683)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.81/2.27 % (422683)CaDiCaL version: 2.1.3 % 13.81/2.27 % (422683)Termination reason: Inappropriate % 13.81/2.27 % (422683)Time elapsed: 0.002 s % 13.81/2.27 % (422683)Peak memory usage: 10 MB % 13.81/2.27 % (422683)Instructions burned: 1 (million) % 13.81/2.27 % (422683)------------------------------ % 13.81/2.27 % (422683)------------------------------ % 13.81/2.27 % (422684)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1384355211:i=1179_2997 on theBenchmark for (2997ds/1179Mi) % 13.81/2.27 % (422686)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1893222875:i=889:ins=1_2997 on theBenchmark for (2997ds/889Mi) % 13.81/2.27 % (422686)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 13.81/2.27 % (422686)Terminated due to inappropriate strategy. % 13.81/2.27 % (422686)------------------------------ % 13.81/2.27 % (422686)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 13.81/2.27 % (422686)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.81/2.27 % (422686)CaDiCaL version: 2.1.3 % 13.81/2.27 % (422686)Termination reason: Inappropriate % 13.81/2.27 % (422686)Time elapsed: 0.003 s % 13.81/2.27 % (422686)Peak memory usage: 10 MB % 13.81/2.27 % (422686)Instructions burned: 2 (million) % 13.81/2.27 % (422686)------------------------------ % 13.81/2.27 % (422686)------------------------------ % 13.81/2.27 % (422689)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=2996442384: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) % 13.81/2.27 % (422678)Instruction limit reached! % 13.81/2.27 % (422678)------------------------------ % 13.81/2.27 % (422678)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 13.81/2.27 % (422678)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.81/2.27 % (422678)CaDiCaL version: 2.1.3 % 13.81/2.27 % (422678)Termination reason: Instruction limit % 13.81/2.27 % (422678)Termination phase: Saturation % 13.81/2.27 % (422678)Time elapsed: 0.155 s % 13.81/2.27 % (422678)Peak memory usage: 12 MB % 13.81/2.27 % (422678)Instructions burned: 181 (million) % 38.23/6.00 % (422691)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3731702405:i=879:kws=inv_precedence:fsr=off_2996 on theBenchmark for (2996ds/879Mi) % 38.23/6.00 % (422680)Instruction limit reached! % 38.23/6.00 % (422680)------------------------------ % 38.23/6.00 % (422680)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 38.23/6.00 % (422680)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 38.23/6.00 % (422680)CaDiCaL version: 2.1.3 % 38.23/6.00 % (422680)Termination reason: Instruction limit % 38.23/6.00 % (422680)Termination phase: Saturation % 38.23/6.00 % (422680)Time elapsed: 0.527 s % 38.23/6.00 % (422680)Peak memory usage: 14 MB % 38.23/6.00 % (422680)Instructions burned: 477 (million) % 38.23/6.00 % (422693)fmb+10_1_sil=64000:random_seed=1456014788:i=22061:nm=2:gsp=on_2992 on theBenchmark for (2992ds/22061Mi) % 38.23/6.00 % (422693)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 38.23/6.00 % (422693)Terminated due to inappropriate strategy. % 38.23/6.00 % (422693)------------------------------ % 38.23/6.00 % (422693)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 38.23/6.00 % (422693)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 38.23/6.00 % (422693)CaDiCaL version: 2.1.3 % 38.23/6.00 % (422693)Termination reason: Inappropriate % 38.23/6.00 % (422693)Time elapsed: 0.003 s % 38.23/6.00 % (422693)Peak memory usage: 10 MB % 38.23/6.00 % (422693)Instructions burned: 2 (million) % 38.23/6.00 % (422693)------------------------------ % 38.23/6.00 % (422693)------------------------------ % 38.23/6.00 % (422695)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=715219398:i=9515:nm=5_2992 on theBenchmark for (2992ds/9515Mi) % 38.23/6.00 % (422695)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 38.23/6.00 % (422695)Terminated due to inappropriate strategy. % 38.23/6.00 % (422695)------------------------------ % 38.23/6.00 % (422695)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 38.23/6.00 % (422695)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 38.23/6.00 % (422695)CaDiCaL version: 2.1.3 % 38.23/6.00 % (422695)Termination reason: Inappropriate % 38.23/6.00 % (422695)Time elapsed: 0.002 s % 38.23/6.00 % (422695)Peak memory usage: 11 MB % 38.23/6.00 % (422695)Instructions burned: 2 (million) % 38.23/6.00 % (422695)------------------------------ % 38.23/6.00 % (422695)------------------------------ % 38.23/6.00 % (422677)Instruction limit reached! % 38.23/6.00 % (422677)------------------------------ % 38.23/6.00 % (422677)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 38.23/6.00 % (422677)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 38.23/6.00 % (422677)CaDiCaL version: 2.1.3 % 38.23/6.00 % (422677)Termination reason: Instruction limit % 38.23/6.00 % (422677)Termination phase: Saturation % 38.23/6.00 % (422677)Time elapsed: 0.646 s % 38.23/6.00 % (422677)Peak memory usage: 16 MB % 38.23/6.00 % (422677)Instructions burned: 684 (million) % 38.23/6.00 % (422697)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2902719000:fmbsr=1.7:i=920_2992 on theBenchmark for (2992ds/920Mi) % 38.23/6.00 % (422697)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 38.23/6.00 % (422697)Terminated due to inappropriate strategy. % 38.23/6.00 % (422697)------------------------------ % 38.23/6.00 % (422697)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 38.23/6.00 % (422697)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 38.23/6.00 % (422697)CaDiCaL version: 2.1.3 % 38.23/6.00 % (422697)Termination reason: Inappropriate % 38.23/6.00 % (422697)Time elapsed: 0.002 s % 38.23/6.00 % (422697)Peak memory usage: 11 MB % 38.23/6.00 % (422697)Instructions burned: 2 (million) % 38.23/6.00 % (422697)------------------------------ % 38.23/6.00 % (422697)------------------------------ % 38.23/6.00 % (422700)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=4014528746:i=1472:ins=7:fdi=8:gsp=on_2991 on theBenchmark for (2991ds/1472Mi) % 38.23/6.00 % (422698)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=4198929032:i=5131_2991 on theBenchmark for (2991ds/5131Mi) % 38.23/6.00 % (422689)Instruction limit reached! % 38.23/6.00 % (422689)------------------------------ % 38.23/6.00 % (422689)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 38.23/6.00 % (422689)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 65.05/9.42 % (422689)CaDiCaL version: 2.1.3 % 65.05/9.42 % (422689)Termination reason: Instruction limit % 65.05/9.42 % (422689)Termination phase: Saturation % 65.05/9.42 % (422689)Time elapsed: 0.703 s % 65.05/9.42 % (422689)Peak memory usage: 17 MB % 65.05/9.42 % (422689)Instructions burned: 693 (million) % 65.05/9.42 % (422704)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=2873753093:i=6324_2989 on theBenchmark for (2989ds/6324Mi) % 65.05/9.42 % (422704)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 65.05/9.42 % (422704)Terminated due to inappropriate strategy. % 65.05/9.42 % (422704)------------------------------ % 65.05/9.42 % (422704)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 65.05/9.42 % (422704)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 65.05/9.42 % (422704)CaDiCaL version: 2.1.3 % 65.05/9.42 % (422704)Termination reason: Inappropriate % 65.05/9.42 % (422704)Time elapsed: 0.002 s % 65.05/9.42 % (422704)Peak memory usage: 11 MB % 65.05/9.42 % (422704)Instructions burned: 2 (million) % 65.05/9.42 % (422704)------------------------------ % 65.05/9.42 % (422704)------------------------------ % 65.05/9.42 % (422707)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=3343024871:fmbsr=2.30978:i=2174_2989 on theBenchmark for (2989ds/2174Mi) % 65.05/9.42 % (422707)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 65.05/9.42 % (422707)Terminated due to inappropriate strategy. % 65.05/9.42 % (422707)------------------------------ % 65.05/9.42 % (422707)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 65.05/9.42 % (422707)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 65.05/9.42 % (422707)CaDiCaL version: 2.1.3 % 65.05/9.42 % (422707)Termination reason: Inappropriate % 65.05/9.42 % (422707)Time elapsed: 0.002 s % 65.05/9.42 % (422707)Peak memory usage: 11 MB % 65.05/9.42 % (422707)Instructions burned: 2 (million) % 65.05/9.42 % (422707)------------------------------ % 65.05/9.42 % (422707)------------------------------ % 65.05/9.42 % (422709)ott-2_1_sil=16000:newcnf=on:random_seed=1533621348:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2989 on theBenchmark for (2989ds/869Mi) % 65.05/9.42 % (422691)Instruction limit reached! % 65.05/9.42 % (422691)------------------------------ % 65.05/9.42 % (422691)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 65.05/9.42 % (422691)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 65.05/9.42 % (422691)CaDiCaL version: 2.1.3 % 65.05/9.42 % (422691)Termination reason: Instruction limit % 65.05/9.42 % (422691)Termination phase: Saturation % 65.05/9.42 % (422691)Time elapsed: 0.861 s % 65.05/9.42 % (422691)Peak memory usage: 18 MB % 65.05/9.42 % (422691)Instructions burned: 879 (million) % 65.05/9.42 % (422711)ott+10_1_sil=32000:tgt=ground:random_seed=521284782:i=5114:av=off_2987 on theBenchmark for (2987ds/5114Mi) % 65.05/9.42 % (422684)Instruction limit reached! % 65.05/9.42 % (422684)------------------------------ % 65.05/9.42 % (422684)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 65.05/9.42 % (422684)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 65.05/9.42 % (422684)CaDiCaL version: 2.1.3 % 65.05/9.42 % (422684)Termination reason: Instruction limit % 65.05/9.42 % (422684)Termination phase: Saturation % 65.05/9.42 % (422684)Time elapsed: 1.167 s % 65.05/9.42 % (422684)Peak memory usage: 20 MB % 65.05/9.42 % (422684)Instructions burned: 1180 (million) % 65.05/9.42 % (422713)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2489994948:i=54282_2985 on theBenchmark for (2985ds/54282Mi) % 65.05/9.42 % (422713)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 65.05/9.42 % (422713)Terminated due to inappropriate strategy. % 65.05/9.42 % (422713)------------------------------ % 65.05/9.42 % (422713)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 65.05/9.42 % (422713)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 65.05/9.42 % (422713)CaDiCaL version: 2.1.3 % 65.05/9.42 % (422713)Termination reason: Inappropriate % 65.05/9.42 % (422713)Time elapsed: 0.002 s % 65.05/9.42 % (422713)Peak memory usage: 11 MB % 65.05/9.42 % (422713)Instructions burned: 2 (million) % 65.05/9.42 % (422713)------------------------------ % 65.05/9.42 % (422713)------------------------------ % 65.05/9.42 % (422715)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3995610669:i=3512:aac=none_2985 on theBenchmark for (2985ds/3512Mi) % 65.05/9.42 % (422709)Instruction limit reached! % 178.90/25.48 % (422709)------------------------------ % 178.90/25.48 % (422709)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 178.90/25.48 % (422709)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 178.90/25.48 % (422709)CaDiCaL version: 2.1.3 % 178.90/25.48 % (422709)Termination reason: Instruction limit % 178.90/25.48 % (422709)Termination phase: Saturation % 178.90/25.48 % (422709)Time elapsed: 0.872 s % 178.90/25.48 % (422709)Peak memory usage: 18 MB % 178.90/25.48 % (422709)Instructions burned: 869 (million) % 178.90/25.48 % (422717)dis+21_1_sil=32000:sas=cadical:random_seed=3249100257:i=3773:amm=off_2980 on theBenchmark for (2980ds/3773Mi) % 178.90/25.48 % (422700)Instruction limit reached! % 178.90/25.48 % (422700)------------------------------ % 178.90/25.48 % (422700)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 178.90/25.48 % (422700)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 178.90/25.48 % (422700)CaDiCaL version: 2.1.3 % 178.90/25.48 % (422700)Termination reason: Instruction limit % 178.90/25.48 % (422700)Termination phase: Saturation % 178.90/25.48 % (422700)Time elapsed: 1.578 s % 178.90/25.48 % (422700)Peak memory usage: 22 MB % 178.90/25.48 % (422700)Instructions burned: 1473 (million) % 178.90/25.48 % (422719)ott+11_1_sil=16000:gs=on:random_seed=3175834899:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2975 on theBenchmark for (2975ds/2251Mi) % 178.90/25.48 % (422715)Instruction limit reached! % 178.90/25.48 % (422715)------------------------------ % 178.90/25.48 % (422715)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 178.90/25.48 % (422715)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 178.90/25.48 % (422715)CaDiCaL version: 2.1.3 % 178.90/25.48 % (422715)Termination reason: Instruction limit % 178.90/25.48 % (422715)Termination phase: Saturation % 178.90/25.48 % (422715)Time elapsed: 3.200 s % 178.90/25.48 % (422715)Peak memory usage: 32 MB % 178.90/25.48 % (422715)Instructions burned: 3512 (million) % 178.90/25.48 % (422739)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=348712515:fmbsr=1.6:i=67534_2953 on theBenchmark for (2953ds/67534Mi) % 178.90/25.48 % (422719)Instruction limit reached! % 178.90/25.48 % (422719)------------------------------ % 178.90/25.48 % (422719)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 178.90/25.48 % (422719)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 178.90/25.48 % (422719)CaDiCaL version: 2.1.3 % 178.90/25.48 % (422719)Termination reason: Instruction limit % 178.90/25.48 % (422719)Termination phase: Saturation % 178.90/25.48 % (422719)Time elapsed: 2.271 s % 178.90/25.48 % (422719)Peak memory usage: 26 MB % 178.90/25.48 % (422719)Instructions burned: 2251 (million) % 178.90/25.48 % (422739)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 178.90/25.48 % (422739)Terminated due to inappropriate strategy. % 178.90/25.48 % (422739)------------------------------ % 178.90/25.48 % (422739)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 178.90/25.48 % (422739)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 178.90/25.48 % (422739)CaDiCaL version: 2.1.3 % 178.90/25.48 % (422739)Termination reason: Inappropriate % 178.90/25.48 % (422739)Time elapsed: 0.003 s % 178.90/25.48 % (422739)Peak memory usage: 10 MB % 178.90/25.48 % (422739)Instructions burned: 2 (million) % 178.90/25.48 % (422739)------------------------------ % 178.90/25.48 % (422739)------------------------------ % 178.90/25.48 % (422742)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=3493140475:i=29340_2952 on theBenchmark for (2952ds/29340Mi) % 178.90/25.48 % (422741)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=1968318603:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2952 on theBenchmark for (2952ds/4591Mi) % 178.90/25.48 % (422711)Instruction limit reached! % 178.90/25.48 % (422711)------------------------------ % 178.90/25.48 % (422711)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 178.90/25.48 % (422711)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 178.90/25.48 % (422711)CaDiCaL version: 2.1.3 % 178.90/25.48 % (422711)Termination reason: Instruction limit % 178.90/25.48 % (422711)Termination phase: Saturation % 178.90/25.48 % (422711)Time elapsed: 4.244 s % 178.90/25.48 % (422711)Peak memory usage: 24 MB % 178.90/25.48 % (422711)Instructions burned: 5114 (million) % 178.90/25.48 % (422745)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=3904226476:i=5211_2944 on theBenchmark for (2944ds/5211Mi) % 178.90/25.48 % (422717)Instruction limit reached! % 218.92/31.11 % (422717)------------------------------ % 218.92/31.11 % (422717)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 218.92/31.11 % (422717)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 218.92/31.11 % (422717)CaDiCaL version: 2.1.3 % 218.92/31.11 % (422717)Termination reason: Instruction limit % 218.92/31.11 % (422717)Termination phase: Saturation % 218.92/31.11 % (422717)Time elapsed: 3.703 s % 218.92/31.11 % (422717)Peak memory usage: 34 MB % 218.92/31.11 % (422717)Instructions burned: 3773 (million) % 218.92/31.11 % (422698)Instruction limit reached! % 218.92/31.11 % (422698)------------------------------ % 218.92/31.11 % (422698)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 218.92/31.11 % (422698)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 218.92/31.11 % (422698)CaDiCaL version: 2.1.3 % 218.92/31.11 % (422698)Termination reason: Instruction limit % 218.92/31.11 % (422698)Termination phase: Saturation % 218.92/31.11 % (422698)Time elapsed: 4.890 s % 218.92/31.11 % (422698)Peak memory usage: 43 MB % 218.92/31.11 % (422698)Instructions burned: 5131 (million) % 218.92/31.11 % (422747)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=1586705946:i=5497:nm=2_2942 on theBenchmark for (2942ds/5497Mi) % 218.92/31.11 % (422747)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 218.92/31.11 % (422747)Terminated due to inappropriate strategy. % 218.92/31.11 % (422747)------------------------------ % 218.92/31.11 % (422747)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 218.92/31.11 % (422747)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 218.92/31.11 % (422747)CaDiCaL version: 2.1.3 % 218.92/31.11 % (422747)Termination reason: Inappropriate % 218.92/31.11 % (422747)Time elapsed: 0.004 s % 218.92/31.11 % (422747)Peak memory usage: 11 MB % 218.92/31.11 % (422747)Instructions burned: 2 (million) % 218.92/31.11 % (422747)------------------------------ % 218.92/31.11 % (422747)------------------------------ % 218.92/31.11 % (422748)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=3833308723:fmbsr=2:i=46332_2942 on theBenchmark for (2942ds/46332Mi) % 218.92/31.11 % (422748)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 218.92/31.11 % (422748)Terminated due to inappropriate strategy. % 218.92/31.11 % (422748)------------------------------ % 218.92/31.11 % (422748)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 218.92/31.11 % (422748)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 218.92/31.11 % (422748)CaDiCaL version: 2.1.3 % 218.92/31.11 % (422748)Termination reason: Inappropriate % 218.92/31.11 % (422748)Time elapsed: 0.003 s % 218.92/31.11 % (422748)Peak memory usage: 10 MB % 218.92/31.11 % (422748)Instructions burned: 2 (million) % 218.92/31.11 % (422748)------------------------------ % 218.92/31.11 % (422748)------------------------------ % 218.92/31.11 % (422750)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=2100986576:i=14071_2942 on theBenchmark for (2942ds/14071Mi) % 218.92/31.11 % (422750)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 218.92/31.11 % (422750)Terminated due to inappropriate strategy. % 218.92/31.11 % (422750)------------------------------ % 218.92/31.11 % (422750)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 218.92/31.11 % (422750)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 218.92/31.11 % (422750)CaDiCaL version: 2.1.3 % 218.92/31.11 % (422750)Termination reason: Inappropriate % 218.92/31.11 % (422750)Time elapsed: 0.002 s % 218.92/31.11 % (422750)Peak memory usage: 11 MB % 218.92/31.11 % (422750)Instructions burned: 2 (million) % 218.92/31.11 % (422750)------------------------------ % 218.92/31.11 % (422750)------------------------------ % 218.92/31.11 % (422752)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3372557434:i=22565:add=on:rawr=on_2942 on theBenchmark for (2942ds/22565Mi) % 218.92/31.11 % (422754)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=2362179860:i=8173:av=off_2942 on theBenchmark for (2942ds/8173Mi) % 218.92/31.11 % (422741)Instruction limit reached! % 218.92/31.11 % (422741)------------------------------ % 218.92/31.11 % (422741)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 218.92/31.11 % (422741)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 218.92/31.11 % (422741)CaDiCaL version: 2.1.3 % 218.92/31.11 % (422741)Termination reason: Instruction limit % 218.92/31.11 % (422741)Termination phase: Saturation % 218.92/31.11 % (422741)Time elapsed: 4.378 s % 235.74/33.42 % (422741)Peak memory usage: 44 MB % 235.74/33.42 % (422741)Instructions burned: 4593 (million) % 235.74/33.42 % (422773)dis+10_16:1_sil=16000:random_seed=2151856407:i=9155:fsr=off_2908 on theBenchmark for (2908ds/9155Mi) % 235.74/33.42 % (422745)Instruction limit reached! % 235.74/33.42 % (422745)------------------------------ % 235.74/33.42 % (422745)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 235.74/33.42 % (422745)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 235.74/33.42 % (422745)CaDiCaL version: 2.1.3 % 235.74/33.42 % (422745)Termination reason: Instruction limit % 235.74/33.42 % (422745)Termination phase: Saturation % 235.74/33.42 % (422745)Time elapsed: 4.618 s % 235.74/33.42 % (422745)Peak memory usage: 50 MB % 235.74/33.42 % (422745)Instructions burned: 5212 (million) % 235.74/33.42 % (422779)ott-3_8_sil=64000:random_seed=2089719164:i=20139:bs=on_2898 on theBenchmark for (2898ds/20139Mi) % 235.74/33.42 % (422754)Instruction limit reached! % 235.74/33.42 % (422754)------------------------------ % 235.74/33.42 % (422754)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 235.74/33.42 % (422754)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 235.74/33.42 % (422754)CaDiCaL version: 2.1.3 % 235.74/33.42 % (422754)Termination reason: Instruction limit % 235.74/33.42 % (422754)Termination phase: Saturation % 235.74/33.42 % (422754)Time elapsed: 7.244 s % 235.74/33.42 % (422754)Peak memory usage: 45 MB % 235.74/33.42 % (422754)Instructions burned: 8173 (million) % 235.74/33.42 % (422785)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=630890425:fmbsr=2:i=32576_2869 on theBenchmark for (2869ds/32576Mi) % 235.74/33.42 % (422785)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 235.74/33.42 % (422785)Terminated due to inappropriate strategy. % 235.74/33.42 % (422785)------------------------------ % 235.74/33.42 % (422785)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 235.74/33.42 % (422785)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 235.74/33.42 % (422785)CaDiCaL version: 2.1.3 % 235.74/33.42 % (422785)Termination reason: Inappropriate % 235.74/33.42 % (422785)Time elapsed: 0.002 s % 235.74/33.42 % (422785)Peak memory usage: 11 MB % 235.74/33.42 % (422785)Instructions burned: 2 (million) % 235.74/33.42 % (422785)------------------------------ % 235.74/33.42 % (422785)------------------------------ % 235.74/33.42 % (422787)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=3720509308:i=11404_2869 on theBenchmark for (2869ds/11404Mi) % 235.74/33.42 % (422773)Instruction limit reached! % 235.74/33.42 % (422773)------------------------------ % 235.74/33.42 % (422773)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 235.74/33.42 % (422773)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 235.74/33.42 % (422773)CaDiCaL version: 2.1.3 % 235.74/33.42 % (422773)Termination reason: Instruction limit % 235.74/33.42 % (422773)Termination phase: Saturation % 235.74/33.42 % (422773)Time elapsed: 8.384 s % 235.74/33.42 % (422773)Peak memory usage: 53 MB % 235.74/33.42 % (422773)Instructions burned: 9156 (million) % 235.74/33.42 % (422803)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=2674700069:i=14134_2824 on theBenchmark for (2824ds/14134Mi) % 235.74/33.42 % (422752)Instruction limit reached! % 235.74/33.42 % (422752)------------------------------ % 235.74/33.42 % (422752)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 235.74/33.42 % (422752)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 235.74/33.42 % (422752)CaDiCaL version: 2.1.3 % 235.74/33.42 % (422752)Termination reason: Instruction limit % 235.74/33.42 % (422752)Termination phase: Saturation % 235.74/33.42 % (422752)Time elapsed: 16.339 s % 235.74/33.42 % (422752)Peak memory usage: 78 MB % 235.74/33.42 % (422752)Instructions burned: 22566 (million) % 235.74/33.42 % (422805)dis+33_16_sil=32000:sac=on:random_seed=2577456944:i=15851:nm=0_2778 on theBenchmark for (2778ds/15851Mi) % 235.74/33.42 % (422787)Instruction limit reached! % 235.74/33.42 % (422787)------------------------------ % 235.74/33.42 % (422787)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 235.74/33.42 % (422787)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 235.74/33.42 % (422787)CaDiCaL version: 2.1.3 % 235.74/33.42 % (422787)Termination reason: Instruction limit % 235.74/33.42 % (422787)Termination phase: Saturation % 235.74/33.42 % (422787)Time elapsed: 12.038 s % 235.74/33.42 % (422787)Peak memory usage: 62 MB % 235.74/33.42 % (422787)Instructions burned: 11404 (million) % 235.74/33.42 % (422807)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=3373607237:avsq=on:i=17627:add=on:amm=off_2748 on theBenchmark for (2748ds/17627Mi) % 261.51/37.05 % (422742)Instruction limit reached! % 261.51/37.05 % (422742)------------------------------ % 261.51/37.05 % (422742)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 261.51/37.05 % (422742)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 261.51/37.05 % (422742)CaDiCaL version: 2.1.3 % 261.51/37.05 % (422742)Termination reason: Instruction limit % 261.51/37.05 % (422742)Termination phase: Saturation % 261.51/37.05 % (422742)Time elapsed: 24.037 s % 261.51/37.05 % (422742)Peak memory usage: 104 MB % 261.51/37.05 % (422742)Instructions burned: 29341 (million) % 261.51/37.05 % (422971)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=2370605505:s2a=on:i=53295_2711 on theBenchmark for (2711ds/53295Mi) % 261.51/37.05 % (422779)Instruction limit reached! % 261.51/37.05 % (422779)------------------------------ % 261.51/37.05 % (422779)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 261.51/37.05 % (422779)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 261.51/37.05 % (422779)CaDiCaL version: 2.1.3 % 261.51/37.05 % (422779)Termination reason: Instruction limit % 261.51/37.05 % (422779)Termination phase: Saturation % 261.51/37.05 % (422779)Time elapsed: 19.948 s % 261.51/37.05 % (422779)Peak memory usage: 89 MB % 261.51/37.05 % (422779)Instructions burned: 20139 (million) % 261.51/37.05 % (422973)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=2729084040:i=26857:ins=20_2698 on theBenchmark for (2698ds/26857Mi) % 261.51/37.05 % (422973)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 261.51/37.05 % (422973)Terminated due to inappropriate strategy. % 261.51/37.05 % (422973)------------------------------ % 261.51/37.05 % (422973)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 261.51/37.05 % (422973)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 261.51/37.05 % (422973)CaDiCaL version: 2.1.3 % 261.51/37.05 % (422973)Termination reason: Inappropriate % 261.51/37.05 % (422973)Time elapsed: 0.001 s % 261.51/37.05 % (422973)Peak memory usage: 10 MB % 261.51/37.05 % (422973)Instructions burned: 2 (million) % 261.51/37.05 % (422973)------------------------------ % 261.51/37.05 % (422973)------------------------------ % 261.51/37.05 % (422975)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=3002690913:i=28120:bs=on:fsr=off_2698 on theBenchmark for (2698ds/28120Mi) % 261.51/37.05 % (422803)Instruction limit reached! % 261.51/37.05 % (422803)------------------------------ % 261.51/37.05 % (422803)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 261.51/37.05 % (422803)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 261.51/37.05 % (422803)CaDiCaL version: 2.1.3 % 261.51/37.05 % (422803)Termination reason: Instruction limit % 261.51/37.05 % (422803)Termination phase: Saturation % 261.51/37.05 % (422803)Time elapsed: 13.184 s % 261.51/37.05 % (422803)Peak memory usage: 71 MB % 261.51/37.05 % (422803)Instructions burned: 14135 (million) % 261.51/37.05 % (422977)fmb+10_1_sil=256000:fmbss=7:random_seed=4201645038:fmbsr=1.6:i=182295_2692 on theBenchmark for (2692ds/182295Mi) % 261.51/37.05 % (422977)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 261.51/37.05 % (422977)Terminated due to inappropriate strategy. % 261.51/37.05 % (422977)------------------------------ % 261.51/37.05 % (422977)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 261.51/37.05 % (422977)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 261.51/37.05 % (422977)CaDiCaL version: 2.1.3 % 261.51/37.05 % (422977)Termination reason: Inappropriate % 261.51/37.05 % (422977)Time elapsed: 0.001 s % 261.51/37.05 % (422977)Peak memory usage: 10 MB % 261.51/37.05 % (422977)Instructions burned: 2 (million) % 261.51/37.05 % (422977)------------------------------ % 261.51/37.05 % (422977)------------------------------ % 261.51/37.05 % (422979)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=99956881:i=44625:gsp=on_2691 on theBenchmark for (2691ds/44625Mi) % 261.51/37.05 % (422979)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 261.51/37.05 % (422979)Terminated due to inappropriate strategy. % 261.51/37.05 % (422979)------------------------------ % 261.51/37.05 % (422979)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 261.51/37.05 % (422979)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 261.51/37.05 % (422979)CaDiCaL version: 2.1.3 % 261.51/37.05 % (422979)Termination reason: Inappropriate % 283.98/40.24 % (422979)Time elapsed: 0.001 s % 283.98/40.24 % (422979)Peak memory usage: 11 MB % 283.98/40.24 % (422979)Instructions burned: 2 (million) % 283.98/40.24 % (422979)------------------------------ % 283.98/40.24 % (422979)------------------------------ % 283.98/40.24 % (422981)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=492820629:i=160505_2691 on theBenchmark for (2691ds/160505Mi) % 283.98/40.24 % (422981)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 283.98/40.24 % (422981)Terminated due to inappropriate strategy. % 283.98/40.24 % (422981)------------------------------ % 283.98/40.24 % (422981)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 283.98/40.24 % (422981)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 283.98/40.24 % (422981)CaDiCaL version: 2.1.3 % 283.98/40.24 % (422981)Termination reason: Inappropriate % 283.98/40.24 % (422981)Time elapsed: 0.001 s % 283.98/40.24 % (422981)Peak memory usage: 10 MB % 283.98/40.24 % (422981)Instructions burned: 2 (million) % 283.98/40.24 % (422981)------------------------------ % 283.98/40.24 % (422981)------------------------------ % 283.98/40.24 % (422983)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=1503116019:fmbsr=1.3:i=225729_2691 on theBenchmark for (2691ds/225729Mi) % 283.98/40.24 % (422983)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 283.98/40.24 % (422983)Terminated due to inappropriate strategy. % 283.98/40.24 % (422983)------------------------------ % 283.98/40.24 % (422983)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 283.98/40.24 % (422983)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 283.98/40.24 % (422983)CaDiCaL version: 2.1.3 % 283.98/40.24 % (422983)Termination reason: Inappropriate % 283.98/40.24 % (422983)Time elapsed: 0.002 s % 283.98/40.24 % (422983)Peak memory usage: 11 MB % 283.98/40.24 % (422983)Instructions burned: 2 (million) % 283.98/40.24 % (422983)------------------------------ % 283.98/40.24 % (422983)------------------------------ % 283.98/40.24 % (422985)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=149593374:fmbsr=2:i=185024:ins=7_2691 on theBenchmark for (2691ds/185024Mi) % 283.98/40.24 % (422985)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 283.98/40.24 % (422985)Terminated due to inappropriate strategy. % 283.98/40.24 % (422985)------------------------------ % 283.98/40.24 % (422985)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 283.98/40.24 % (422985)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 283.98/40.24 % (422985)CaDiCaL version: 2.1.3 % 283.98/40.24 % (422985)Termination reason: Inappropriate % 283.98/40.24 % (422985)Time elapsed: 0.002 s % 283.98/40.24 % (422985)Peak memory usage: 11 MB % 283.98/40.24 % (422985)Instructions burned: 2 (million) % 283.98/40.24 % (422985)------------------------------ % 283.98/40.24 % (422985)------------------------------ % 283.98/40.24 % (422987)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=3182629142:rtra=on_2690 on theBenchmark for (2690ds/0Mi) % 283.98/40.24 % (422987)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 283.98/40.24 % (422987)Terminated due to inappropriate strategy. % 283.98/40.24 % (422987)------------------------------ % 283.98/40.24 % (422987)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 283.98/40.24 % (422987)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 283.98/40.24 % (422987)CaDiCaL version: 2.1.3 % 283.98/40.24 % (422987)Termination reason: Inappropriate % 283.98/40.24 % (422987)Time elapsed: 0.002 s % 283.98/40.24 % (422987)Peak memory usage: 10 MB % 283.98/40.24 % (422987)Instructions burned: 2 (million) % 283.98/40.24 % (422987)------------------------------ % 283.98/40.24 % (422987)------------------------------ % 283.98/40.24 % (422989)% WARNING: option uhcvi not known. % 283.98/40.24 % (422989)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1549761288:i=271062:add=off:rtra=on:rawr=on_2690 on theBenchmark for (2690ds/271062Mi) % 283.98/40.24 % (422805)Instruction limit reached! % 283.98/40.24 % (422805)------------------------------ % 283.98/40.24 % (422805)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 283.98/40.24 % (422805)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 283.98/40.24 % (422805)CaDiCaL version: 2.1.3 % 283.98/40.24 % (422805)Termination reason: Instruction limit % 283.98/40.24 % (422805)Termination phase: Saturation % 283.98/40.24 % (422805)Time elapsed: 10.912 s % 283.98/40.24 % (422805)Peak memory usage: 128 MB % 283.98/40.24 % (422805)Instructions burned: 15852 (million) % 283.98/40.24 % (422993)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2004927427:i=176048:add=on:rtra=on:rawr=on_2668 on theBenchmark for (2668ds/176048Mi) % 297.72/42.16 % (422807)Instruction limit reached! % 297.72/42.16 % (422807)------------------------------ % 297.72/42.16 % (422807)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 297.72/42.16 % (422807)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 297.72/42.16 % (422807)CaDiCaL version: 2.1.3 % 297.72/42.16 % (422807)Termination reason: Instruction limit % 297.72/42.16 % (422807)Termination phase: Saturation % 297.72/42.16 % (422807)Time elapsed: 10.772 s % 297.72/42.16 % (422807)Peak memory usage: 192 MB % 297.72/42.16 % (422807)Instructions burned: 17628 (million) % 297.72/42.16 % (422995)dis+10_1_sil=32000:si=on:sp=arity:random_seed=1903728238:i=206:fgj=on:rtra=on_2640 on theBenchmark for (2640ds/206Mi) % 297.72/42.16 % (422995)Instruction limit reached! % 297.72/42.16 % (422995)------------------------------ % 297.72/42.16 % (422995)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 297.72/42.16 % (422995)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 297.72/42.16 % (422995)CaDiCaL version: 2.1.3 % 297.72/42.16 % (422995)Termination reason: Instruction limit % 297.72/42.16 % (422995)Termination phase: Saturation % 297.72/42.16 % (422995)Time elapsed: 0.136 s % 297.72/42.16 % (422995)Peak memory usage: 14 MB % 297.72/42.16 % (422995)Instructions burned: 206 (million) % 297.72/42.16 % (422997)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=3121821846:i=232:rtra=on_2638 on theBenchmark for (2638ds/232Mi) % 297.72/42.16 % (422997)Instruction limit reached! % 297.72/42.16 % (422997)------------------------------ % 297.72/42.16 % (422997)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 297.72/42.16 % (422997)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 297.72/42.16 % (422997)CaDiCaL version: 2.1.3 % 297.72/42.16 % (422997)Termination reason: Instruction limit % 297.72/42.16 % (422997)Termination phase: Saturation % 297.72/42.16 % (422997)Time elapsed: 0.147 s % 297.72/42.16 % (422997)Peak memory usage: 14 MB % 297.72/42.16 % (422997)Instructions burned: 232 (million) % 297.72/42.16 % (422999)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=3586872162:i=262:rtra=on_2636 on theBenchmark for (2636ds/262Mi) % 297.72/42.16 % (422999)Instruction limit reached! % 297.72/42.16 % (422999)------------------------------ % 297.72/42.16 % (422999)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 297.72/42.16 % (422999)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 297.72/42.16 % (422999)CaDiCaL version: 2.1.3 % 297.72/42.16 % (422999)Termination reason: Instruction limit % 297.72/42.16 % (422999)Termination phase: Saturation % 297.72/42.16 % (422999)Time elapsed: 0.160 s % 297.72/42.16 % (422999)Peak memory usage: 13 MB % 297.72/42.16 % (422999)Instructions burned: 262 (million) % 297.72/42.16 % (423001)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=3038389448:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2634 on theBenchmark for (2634ds/318Mi) % 297.72/42.16 % (423001)Instruction limit reached! % 297.72/42.16 % (423001)------------------------------ % 297.72/42.16 % (423001)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 297.72/42.16 % (423001)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 297.72/42.16 % (423001)CaDiCaL version: 2.1.3 % 297.72/42.16 % (423001)Termination reason: Instruction limit % 297.72/42.16 % (423001)Termination phase: Saturation % 297.72/42.16 % (423001)Time elapsed: 0.230 s % 297.72/42.16 % (423001)Peak memory usage: 15 MB % 297.72/42.16 % (423001)Instructions burned: 318 (million) % 297.72/42.16 % (423003)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=4234267563:i=1428:nm=2:rtra=on_2632 on theBenchmark for (2632ds/1428Mi) % 297.72/42.16 % (423003)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 297.72/42.16 % (423003)Terminated due to inappropriate strategy. % 297.72/42.16 % (423003)------------------------------ % 297.72/42.16 % (423003)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 297.72/42.16 % (423003)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 297.72/42.16 % (423003)CaDiCaL version: 2.1.3 % 297.72/42.16 % (423003)Termination reason: Inappropriate % 297.72/42.16 % (423003)Time elapsed: 0.002 s % 297.72/42.16 % (423003)Peak memory usage: 11 MB % 297.72/42.16 % (423003)Instructions burned: 2 (million) % 297.72/42.16 % (423003)------------------------------ % 300.59/42.64 Terminated % 300.59/42.64 % Vampire exiting % 300.59/42.64 Terminated %------------------------------------------------------------------------------