%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWW658_2 : TPTP v9.3.1. Released v6.1.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % Computer : n015.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 29 01:40:36 PM UTC 2026 % Result : Timeout 300.05s 42.53s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWW658_2 : TPTP v9.3.1. Released v6.1.0. % 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.09/0.18 % Computer : n015.cluster.edu % 0.09/0.18 % Model : x86_64 x86_64 % 0.09/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.18 % Memory : 8046.5625MB % 0.09/0.18 % OS : Linux 6.8.0-71-generic % 0.09/0.19 % CPULimit : 300 % 0.09/0.19 % WCLimit : 300 % 0.09/0.19 % DateTime : Mon Sep 28 14:27:17 UTC 2026 % 0.09/0.19 % CPUTime : % 0.09/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.09/0.22 Running first-order model finding % 0.09/0.22 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 3.65/0.83 % (2665602)Will run a generic schedule for satisfiability detection. % 3.65/0.83 % (2665614)dis+10_1_sil=32000:sp=arity:random_seed=1812048556:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 3.65/0.83 % (2665612)% WARNING: option uhcvi not known. % 3.65/0.83 % (2665611)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1616868764_2999 on theBenchmark for (2999ds/0Mi) % 3.65/0.83 % (2665615)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2816756683:i=116_2999 on theBenchmark for (2999ds/116Mi) % 3.65/0.83 % (2665613)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=521991804:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 3.65/0.83 % (2665612)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=4219110832:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 3.65/0.83 % (2665616)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=97693299:i=131_2999 on theBenchmark for (2999ds/131Mi) % 3.65/0.83 % (2665617)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3880400544:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 3.65/0.83 % (2665611)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.65/0.83 % (2665611)Terminated due to inappropriate strategy. % 3.65/0.83 % (2665611)------------------------------ % 3.65/0.83 % (2665611)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.65/0.83 % (2665611)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.65/0.83 % (2665611)CaDiCaL version: 2.1.3 % 3.65/0.83 % (2665611)Termination reason: Inappropriate % 3.65/0.83 % (2665611)Time elapsed: 0.003 s % 3.65/0.83 % (2665611)Peak memory usage: 10 MB % 3.65/0.83 % (2665611)Instructions burned: 4 (million) % 3.65/0.83 % (2665611)------------------------------ % 3.65/0.83 % (2665611)------------------------------ % 3.65/0.83 % (2665625)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3467751523:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 3.65/0.83 % (2665625)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.65/0.83 % (2665625)Terminated due to inappropriate strategy. % 3.65/0.83 % (2665625)------------------------------ % 3.65/0.83 % (2665625)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.65/0.83 % (2665625)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.65/0.83 % (2665625)CaDiCaL version: 2.1.3 % 3.65/0.83 % (2665625)Termination reason: Inappropriate % 3.65/0.83 % (2665625)Time elapsed: 0.002 s % 3.65/0.83 % (2665625)Peak memory usage: 10 MB % 3.65/0.83 % (2665625)Instructions burned: 4 (million) % 3.65/0.83 % (2665625)------------------------------ % 3.65/0.83 % (2665625)------------------------------ % 3.65/0.83 % (2665614)Instruction limit reached! % 3.65/0.83 % (2665614)------------------------------ % 3.65/0.83 % (2665614)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.65/0.83 % (2665614)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.65/0.83 % (2665614)CaDiCaL version: 2.1.3 % 3.65/0.83 % (2665614)Termination reason: Instruction limit % 3.65/0.83 % (2665614)Termination phase: Saturation % 3.65/0.83 % (2665614)Time elapsed: 0.036 s % 3.65/0.83 % (2665614)Peak memory usage: 12 MB % 3.65/0.83 % (2665614)Instructions burned: 106 (million) % 3.65/0.83 % (2665628)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=563824311:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi) % 3.65/0.83 % (2665627)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1342406388:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 3.65/0.83 % (2665615)Instruction limit reached! % 3.65/0.83 % (2665615)------------------------------ % 3.65/0.83 % (2665615)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.65/0.83 % (2665615)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.65/0.83 % (2665615)CaDiCaL version: 2.1.3 % 3.65/0.83 % (2665615)Termination reason: Instruction limit % 3.65/0.83 % (2665615)Termination phase: Saturation % 3.65/0.83 % (2665615)Time elapsed: 0.073 s % 3.65/0.83 % (2665615)Peak memory usage: 13 MB % 3.65/0.83 % (2665615)Instructions burned: 116 (million) % 3.65/0.83 % (2665616)Instruction limit reached! % 3.65/0.83 % (2665616)------------------------------ % 3.65/0.83 % (2665616)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.36/1.19 % (2665616)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.36/1.19 % (2665616)CaDiCaL version: 2.1.3 % 6.36/1.19 % (2665616)Termination reason: Instruction limit % 6.36/1.19 % (2665616)Termination phase: Saturation % 6.36/1.19 % (2665616)Time elapsed: 0.085 s % 6.36/1.19 % (2665616)Peak memory usage: 13 MB % 6.36/1.19 % (2665616)Instructions burned: 133 (million) % 6.36/1.19 % (2665631)ott-21_1_sil=16000:fs=off:random_seed=1958019429:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 6.36/1.19 % (2665632)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=775306181:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 6.36/1.19 % (2665617)Instruction limit reached! % 6.36/1.19 % (2665617)------------------------------ % 6.36/1.19 % (2665617)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.36/1.19 % (2665617)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.36/1.19 % (2665617)CaDiCaL version: 2.1.3 % 6.36/1.19 % (2665617)Termination reason: Instruction limit % 6.36/1.19 % (2665617)Termination phase: Saturation % 6.36/1.19 % (2665617)Time elapsed: 0.113 s % 6.36/1.19 % (2665617)Peak memory usage: 13 MB % 6.36/1.19 % (2665617)Instructions burned: 160 (million) % 6.36/1.19 % (2665635)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1172042592:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 6.36/1.19 % (2665627)Instruction limit reached! % 6.36/1.19 % (2665627)------------------------------ % 6.36/1.19 % (2665627)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.36/1.19 % (2665627)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.36/1.19 % (2665627)CaDiCaL version: 2.1.3 % 6.36/1.19 % (2665627)Termination reason: Instruction limit % 6.36/1.19 % (2665627)Termination phase: Saturation % 6.36/1.19 % (2665627)Time elapsed: 0.090 s % 6.36/1.19 % (2665627)Peak memory usage: 13 MB % 6.36/1.19 % (2665627)Instructions burned: 131 (million) % 6.36/1.19 % (2665635)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 6.36/1.19 % (2665635)Terminated due to inappropriate strategy. % 6.36/1.19 % (2665635)------------------------------ % 6.36/1.19 % (2665635)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.36/1.19 % (2665635)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.36/1.19 % (2665635)CaDiCaL version: 2.1.3 % 6.36/1.19 % (2665635)Termination reason: Inappropriate % 6.36/1.19 % (2665635)Time elapsed: 0.002 s % 6.36/1.19 % (2665635)Peak memory usage: 10 MB % 6.36/1.19 % (2665635)Instructions burned: 4 (million) % 6.36/1.19 % (2665635)------------------------------ % 6.36/1.19 % (2665635)------------------------------ % 6.36/1.19 % (2665637)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=484957077:i=1179_2998 on theBenchmark for (2998ds/1179Mi) % 6.36/1.19 % (2665638)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=4724837:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi) % 6.36/1.19 % (2665638)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 6.36/1.19 % (2665638)Terminated due to inappropriate strategy. % 6.36/1.19 % (2665638)------------------------------ % 6.36/1.19 % (2665638)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.36/1.19 % (2665638)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.36/1.19 % (2665638)CaDiCaL version: 2.1.3 % 6.36/1.19 % (2665638)Termination reason: Inappropriate % 6.36/1.19 % (2665638)Time elapsed: 0.002 s % 6.36/1.19 % (2665638)Peak memory usage: 10 MB % 6.36/1.19 % (2665638)Instructions burned: 4 (million) % 6.36/1.19 % (2665638)------------------------------ % 6.36/1.19 % (2665638)------------------------------ % 6.36/1.19 % (2665641)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=963928768:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2998 on theBenchmark for (2998ds/692Mi) % 6.36/1.19 % (2665631)Instruction limit reached! % 6.36/1.19 % (2665631)------------------------------ % 6.36/1.19 % (2665631)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.36/1.19 % (2665631)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.36/1.19 % (2665631)CaDiCaL version: 2.1.3 % 6.36/1.19 % (2665631)Termination reason: Instruction limit % 6.36/1.19 % (2665631)Termination phase: Saturation % 21.06/3.23 % (2665631)Time elapsed: 0.086 s % 21.06/3.23 % (2665631)Peak memory usage: 13 MB % 21.06/3.23 % (2665631)Instructions burned: 180 (million) % 21.06/3.23 % (2665643)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3547338777:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi) % 21.06/3.23 % (2665628)Instruction limit reached! % 21.06/3.23 % (2665628)------------------------------ % 21.06/3.23 % (2665628)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 21.06/3.23 % (2665628)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.06/3.23 % (2665628)CaDiCaL version: 2.1.3 % 21.06/3.23 % (2665628)Termination reason: Instruction limit % 21.06/3.23 % (2665628)Termination phase: Saturation % 21.06/3.23 % (2665628)Time elapsed: 0.190 s % 21.06/3.23 % (2665628)Peak memory usage: 16 MB % 21.06/3.23 % (2665628)Instructions burned: 688 (million) % 21.06/3.23 % (2665645)fmb+10_1_sil=64000:random_seed=2439687554:i=22061:nm=2:gsp=on_2997 on theBenchmark for (2997ds/22061Mi) % 21.06/3.23 % (2665645)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 21.06/3.23 % (2665645)Terminated due to inappropriate strategy. % 21.06/3.23 % (2665645)------------------------------ % 21.06/3.23 % (2665645)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 21.06/3.23 % (2665645)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.06/3.23 % (2665645)CaDiCaL version: 2.1.3 % 21.06/3.23 % (2665645)Termination reason: Inappropriate % 21.06/3.23 % (2665645)Time elapsed: 0.001 s % 21.06/3.23 % (2665645)Peak memory usage: 10 MB % 21.06/3.23 % (2665645)Instructions burned: 4 (million) % 21.06/3.23 % (2665645)------------------------------ % 21.06/3.23 % (2665645)------------------------------ % 21.06/3.23 % (2665647)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=292580599:i=9515:nm=5_2997 on theBenchmark for (2997ds/9515Mi) % 21.06/3.23 % (2665647)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 21.06/3.23 % (2665647)Terminated due to inappropriate strategy. % 21.06/3.23 % (2665647)------------------------------ % 21.06/3.23 % (2665647)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 21.06/3.23 % (2665647)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.06/3.23 % (2665647)CaDiCaL version: 2.1.3 % 21.06/3.23 % (2665647)Termination reason: Inappropriate % 21.06/3.23 % (2665647)Time elapsed: 0.001 s % 21.06/3.23 % (2665647)Peak memory usage: 10 MB % 21.06/3.23 % (2665647)Instructions burned: 4 (million) % 21.06/3.23 % (2665647)------------------------------ % 21.06/3.23 % (2665647)------------------------------ % 21.06/3.23 % (2665649)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2782036711:fmbsr=1.7:i=920_2997 on theBenchmark for (2997ds/920Mi) % 21.06/3.23 % (2665649)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 21.06/3.23 % (2665649)Terminated due to inappropriate strategy. % 21.06/3.23 % (2665649)------------------------------ % 21.06/3.23 % (2665649)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 21.06/3.23 % (2665649)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.06/3.23 % (2665649)CaDiCaL version: 2.1.3 % 21.06/3.23 % (2665649)Termination reason: Inappropriate % 21.06/3.23 % (2665649)Time elapsed: 0.001 s % 21.06/3.23 % (2665649)Peak memory usage: 10 MB % 21.06/3.23 % (2665649)Instructions burned: 4 (million) % 21.06/3.23 % (2665649)------------------------------ % 21.06/3.23 % (2665649)------------------------------ % 21.06/3.23 % (2665651)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1892540295:i=5131_2996 on theBenchmark for (2996ds/5131Mi) % 21.06/3.23 % (2665632)Instruction limit reached! % 21.06/3.23 % (2665632)------------------------------ % 21.06/3.23 % (2665632)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 21.06/3.23 % (2665632)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.06/3.23 % (2665632)CaDiCaL version: 2.1.3 % 21.06/3.23 % (2665632)Termination reason: Instruction limit % 21.06/3.23 % (2665632)Termination phase: Saturation % 21.06/3.23 % (2665632)Time elapsed: 0.315 s % 21.06/3.23 % (2665632)Peak memory usage: 14 MB % 21.06/3.23 % (2665632)Instructions burned: 477 (million) % 21.06/3.23 % (2665653)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2073537503:i=1472:ins=7:fdi=8:gsp=on_2995 on theBenchmark for (2995ds/1472Mi) % 21.06/3.23 % (2665641)Instruction limit reached! % 21.06/3.23 % (2665641)------------------------------ % 28.15/4.25 % (2665641)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 28.15/4.25 % (2665641)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.15/4.25 % (2665641)CaDiCaL version: 2.1.3 % 28.15/4.25 % (2665641)Termination reason: Instruction limit % 28.15/4.25 % (2665641)Termination phase: Saturation % 28.15/4.25 % (2665641)Time elapsed: 0.387 s % 28.15/4.25 % (2665641)Peak memory usage: 18 MB % 28.15/4.25 % (2665641)Instructions burned: 693 (million) % 28.15/4.25 % (2665655)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=2226410944:i=6324_2993 on theBenchmark for (2993ds/6324Mi) % 28.15/4.25 % (2665655)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 28.15/4.25 % (2665655)Terminated due to inappropriate strategy. % 28.15/4.25 % (2665655)------------------------------ % 28.15/4.25 % (2665655)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 28.15/4.25 % (2665655)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.15/4.25 % (2665655)CaDiCaL version: 2.1.3 % 28.15/4.25 % (2665655)Termination reason: Inappropriate % 28.15/4.25 % (2665655)Time elapsed: 0.003 s % 28.15/4.25 % (2665655)Peak memory usage: 10 MB % 28.15/4.25 % (2665655)Instructions burned: 4 (million) % 28.15/4.25 % (2665655)------------------------------ % 28.15/4.25 % (2665655)------------------------------ % 28.15/4.25 % (2665657)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=2619329698:fmbsr=2.30978:i=2174_2993 on theBenchmark for (2993ds/2174Mi) % 28.15/4.25 % (2665657)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 28.15/4.25 % (2665657)Terminated due to inappropriate strategy. % 28.15/4.25 % (2665657)------------------------------ % 28.15/4.25 % (2665657)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 28.15/4.25 % (2665657)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.15/4.25 % (2665657)CaDiCaL version: 2.1.3 % 28.15/4.25 % (2665657)Termination reason: Inappropriate % 28.15/4.25 % (2665657)Time elapsed: 0.002 s % 28.15/4.25 % (2665657)Peak memory usage: 10 MB % 28.15/4.25 % (2665657)Instructions burned: 4 (million) % 28.15/4.25 % (2665657)------------------------------ % 28.15/4.25 % (2665657)------------------------------ % 28.15/4.25 % (2665659)ott-2_1_sil=16000:newcnf=on:random_seed=605388288:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2993 on theBenchmark for (2993ds/869Mi) % 28.15/4.25 % (2665643)Instruction limit reached! % 28.15/4.25 % (2665643)------------------------------ % 28.15/4.25 % (2665643)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 28.15/4.25 % (2665643)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.15/4.25 % (2665643)CaDiCaL version: 2.1.3 % 28.15/4.25 % (2665643)Termination reason: Instruction limit % 28.15/4.25 % (2665643)Termination phase: Saturation % 28.15/4.25 % (2665643)Time elapsed: 0.504 s % 28.15/4.25 % (2665643)Peak memory usage: 18 MB % 28.15/4.25 % (2665643)Instructions burned: 879 (million) % 28.15/4.25 % (2665661)ott+10_1_sil=32000:tgt=ground:random_seed=3483199203:i=5114:av=off_2992 on theBenchmark for (2992ds/5114Mi) % 28.15/4.25 % (2665637)Instruction limit reached! % 28.15/4.25 % (2665637)------------------------------ % 28.15/4.25 % (2665637)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 28.15/4.25 % (2665637)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.15/4.25 % (2665637)CaDiCaL version: 2.1.3 % 28.15/4.25 % (2665637)Termination reason: Instruction limit % 28.15/4.25 % (2665637)Termination phase: Saturation % 28.15/4.25 % (2665637)Time elapsed: 0.739 s % 28.15/4.25 % (2665637)Peak memory usage: 18 MB % 28.15/4.25 % (2665637)Instructions burned: 1179 (million) % 28.15/4.25 % (2665663)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=4027084624:i=54282_2990 on theBenchmark for (2990ds/54282Mi) % 28.15/4.25 % (2665663)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 28.15/4.25 % (2665663)Terminated due to inappropriate strategy. % 28.15/4.25 % (2665663)------------------------------ % 28.15/4.25 % (2665663)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 28.15/4.25 % (2665663)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.15/4.25 % (2665663)CaDiCaL version: 2.1.3 % 28.15/4.25 % (2665663)Termination reason: Inappropriate % 28.15/4.25 % (2665663)Time elapsed: 0.003 s % 28.15/4.25 % (2665663)Peak memory usage: 10 MB % 28.15/4.25 % (2665663)Instructions burned: 4 (million) % 88.49/12.74 % (2665663)------------------------------ % 88.49/12.74 % (2665663)------------------------------ % 88.49/12.74 % (2665665)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=462102422:i=3512:aac=none_2990 on theBenchmark for (2990ds/3512Mi) % 88.49/12.74 % (2665659)Instruction limit reached! % 88.49/12.74 % (2665659)------------------------------ % 88.49/12.74 % (2665659)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 88.49/12.74 % (2665659)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 88.49/12.74 % (2665659)CaDiCaL version: 2.1.3 % 88.49/12.74 % (2665659)Termination reason: Instruction limit % 88.49/12.74 % (2665659)Termination phase: Saturation % 88.49/12.74 % (2665659)Time elapsed: 0.495 s % 88.49/12.74 % (2665659)Peak memory usage: 15 MB % 88.49/12.74 % (2665659)Instructions burned: 870 (million) % 88.49/12.74 % (2665667)dis+21_1_sil=32000:sas=cadical:random_seed=52815839:i=3773:amm=off_2988 on theBenchmark for (2988ds/3773Mi) % 88.49/12.74 % (2665653)Instruction limit reached! % 88.49/12.74 % (2665653)------------------------------ % 88.49/12.74 % (2665653)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 88.49/12.74 % (2665653)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 88.49/12.74 % (2665653)CaDiCaL version: 2.1.3 % 88.49/12.74 % (2665653)Termination reason: Instruction limit % 88.49/12.74 % (2665653)Termination phase: Saturation % 88.49/12.74 % (2665653)Time elapsed: 0.870 s % 88.49/12.74 % (2665653)Peak memory usage: 22 MB % 88.49/12.74 % (2665653)Instructions burned: 1474 (million) % 88.49/12.74 % (2665669)ott+11_1_sil=16000:gs=on:random_seed=3022222595:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2986 on theBenchmark for (2986ds/2251Mi) % 88.49/12.74 % (2665651)Instruction limit reached! % 88.49/12.74 % (2665651)------------------------------ % 88.49/12.74 % (2665651)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 88.49/12.74 % (2665651)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 88.49/12.74 % (2665651)CaDiCaL version: 2.1.3 % 88.49/12.74 % (2665651)Termination reason: Instruction limit % 88.49/12.74 % (2665651)Termination phase: Saturation % 88.49/12.74 % (2665651)Time elapsed: 1.536 s % 88.49/12.74 % (2665651)Peak memory usage: 41 MB % 88.49/12.74 % (2665651)Instructions burned: 5133 (million) % 88.49/12.74 % (2665671)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=2539073028:fmbsr=1.6:i=67534_2981 on theBenchmark for (2981ds/67534Mi) % 88.49/12.74 % (2665671)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 88.49/12.74 % (2665671)Terminated due to inappropriate strategy. % 88.49/12.74 % (2665671)------------------------------ % 88.49/12.74 % (2665671)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 88.49/12.74 % (2665671)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 88.49/12.74 % (2665671)CaDiCaL version: 2.1.3 % 88.49/12.74 % (2665671)Termination reason: Inappropriate % 88.49/12.74 % (2665671)Time elapsed: 0.001 s % 88.49/12.74 % (2665671)Peak memory usage: 10 MB % 88.49/12.74 % (2665671)Instructions burned: 4 (million) % 88.49/12.74 % (2665671)------------------------------ % 88.49/12.74 % (2665671)------------------------------ % 88.49/12.74 % (2665673)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=2515564560:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2981 on theBenchmark for (2981ds/4591Mi) % 88.49/12.74 % (2665669)Instruction limit reached! % 88.49/12.74 % (2665669)------------------------------ % 88.49/12.74 % (2665669)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 88.49/12.74 % (2665669)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 88.49/12.74 % (2665669)CaDiCaL version: 2.1.3 % 88.49/12.74 % (2665669)Termination reason: Instruction limit % 88.49/12.74 % (2665669)Termination phase: Saturation % 88.49/12.74 % (2665669)Time elapsed: 1.311 s % 88.49/12.74 % (2665669)Peak memory usage: 25 MB % 88.49/12.74 % (2665669)Instructions burned: 2251 (million) % 88.49/12.74 % (2665675)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=2543176550:i=29340_2973 on theBenchmark for (2973ds/29340Mi) % 88.49/12.74 % (2665665)Instruction limit reached! % 88.49/12.74 % (2665665)------------------------------ % 88.49/12.74 % (2665665)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 88.49/12.74 % (2665665)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 88.49/12.74 % (2665665)CaDiCaL version: 2.1.3 % 88.49/12.74 % (2665665)Termination reason: Instruction limit % 124.78/17.92 % (2665665)Termination phase: Saturation % 124.78/17.92 % (2665665)Time elapsed: 2.028 s % 124.78/17.92 % (2665665)Peak memory usage: 31 MB % 124.78/17.92 % (2665665)Instructions burned: 3514 (million) % 124.78/17.92 % (2665677)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=288943908:i=5211_2969 on theBenchmark for (2969ds/5211Mi) % 124.78/17.92 % (2665673)Instruction limit reached! % 124.78/17.92 % (2665673)------------------------------ % 124.78/17.92 % (2665673)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 124.78/17.92 % (2665673)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 124.78/17.92 % (2665673)CaDiCaL version: 2.1.3 % 124.78/17.92 % (2665673)Termination reason: Instruction limit % 124.78/17.92 % (2665673)Termination phase: Saturation % 124.78/17.92 % (2665673)Time elapsed: 1.266 s % 124.78/17.92 % (2665673)Peak memory usage: 47 MB % 124.78/17.92 % (2665673)Instructions burned: 4594 (million) % 124.78/17.92 % (2665679)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=705807276:i=5497:nm=2_2968 on theBenchmark for (2968ds/5497Mi) % 124.78/17.92 % (2665679)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 124.78/17.92 % (2665679)Terminated due to inappropriate strategy. % 124.78/17.92 % (2665679)------------------------------ % 124.78/17.92 % (2665679)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 124.78/17.92 % (2665679)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 124.78/17.92 % (2665679)CaDiCaL version: 2.1.3 % 124.78/17.92 % (2665679)Termination reason: Inappropriate % 124.78/17.92 % (2665679)Time elapsed: 0.001 s % 124.78/17.92 % (2665679)Peak memory usage: 10 MB % 124.78/17.92 % (2665679)Instructions burned: 4 (million) % 124.78/17.92 % (2665679)------------------------------ % 124.78/17.92 % (2665679)------------------------------ % 124.78/17.92 % (2665681)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=985306984:fmbsr=2:i=46332_2968 on theBenchmark for (2968ds/46332Mi) % 124.78/17.92 % (2665681)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 124.78/17.92 % (2665681)Terminated due to inappropriate strategy. % 124.78/17.92 % (2665681)------------------------------ % 124.78/17.92 % (2665681)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 124.78/17.92 % (2665681)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 124.78/17.92 % (2665681)CaDiCaL version: 2.1.3 % 124.78/17.92 % (2665681)Termination reason: Inappropriate % 124.78/17.92 % (2665681)Time elapsed: 0.001 s % 124.78/17.92 % (2665681)Peak memory usage: 10 MB % 124.78/17.92 % (2665681)Instructions burned: 4 (million) % 124.78/17.92 % (2665681)------------------------------ % 124.78/17.92 % (2665681)------------------------------ % 124.78/17.92 % (2665683)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=576898005:i=14071_2968 on theBenchmark for (2968ds/14071Mi) % 124.78/17.92 % (2665683)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 124.78/17.92 % (2665683)Terminated due to inappropriate strategy. % 124.78/17.92 % (2665683)------------------------------ % 124.78/17.92 % (2665683)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 124.78/17.92 % (2665683)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 124.78/17.92 % (2665683)CaDiCaL version: 2.1.3 % 124.78/17.92 % (2665683)Termination reason: Inappropriate % 124.78/17.92 % (2665683)Time elapsed: 0.001 s % 124.78/17.92 % (2665683)Peak memory usage: 10 MB % 124.78/17.92 % (2665683)Instructions burned: 4 (million) % 124.78/17.92 % (2665683)------------------------------ % 124.78/17.92 % (2665683)------------------------------ % 124.78/17.92 % (2665685)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=683060277:i=22565:add=on:rawr=on_2968 on theBenchmark for (2968ds/22565Mi) % 124.78/17.92 % (2665667)Instruction limit reached! % 124.78/17.92 % (2665667)------------------------------ % 124.78/17.92 % (2665667)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 124.78/17.92 % (2665667)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 124.78/17.92 % (2665667)CaDiCaL version: 2.1.3 % 124.78/17.92 % (2665667)Termination reason: Instruction limit % 124.78/17.92 % (2665667)Termination phase: Saturation % 124.78/17.92 % (2665667)Time elapsed: 2.147 s % 124.78/17.92 % (2665667)Peak memory usage: 33 MB % 124.78/17.92 % (2665667)Instructions burned: 3774 (million) % 124.78/17.92 % (2665687)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=4123450238:i=8173:av=off_2966 on theBenchmark for (2966ds/8173Mi) % 124.78/17.92 % (2665661)Instruction limit reached! % 124.78/18.03 % (2665661)------------------------------ % 124.78/18.03 % (2665661)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 124.78/18.03 % (2665661)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 124.78/18.03 % (2665661)CaDiCaL version: 2.1.3 % 124.78/18.03 % (2665661)Termination reason: Instruction limit % 124.78/18.03 % (2665661)Termination phase: Saturation % 124.78/18.03 % (2665661)Time elapsed: 3.261 s % 124.78/18.03 % (2665661)Peak memory usage: 36 MB % 124.78/18.03 % (2665661)Instructions burned: 5114 (million) % 124.78/18.03 % (2665689)dis+10_16:1_sil=16000:random_seed=3428619683:i=9155:fsr=off_2959 on theBenchmark for (2959ds/9155Mi) % 124.78/18.03 % (2665677)Instruction limit reached! % 124.78/18.03 % (2665677)------------------------------ % 124.78/18.03 % (2665677)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 124.78/18.03 % (2665677)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 124.78/18.03 % (2665677)CaDiCaL version: 2.1.3 % 124.78/18.03 % (2665677)Termination reason: Instruction limit % 124.78/18.03 % (2665677)Termination phase: Saturation % 124.78/18.03 % (2665677)Time elapsed: 2.868 s % 124.78/18.03 % (2665677)Peak memory usage: 55 MB % 124.78/18.03 % (2665677)Instructions burned: 5212 (million) % 124.78/18.03 % (2665691)ott-3_8_sil=64000:random_seed=750658499:i=20139:bs=on_2940 on theBenchmark for (2940ds/20139Mi) % 124.78/18.03 % (2665685)Instruction limit reached! % 124.78/18.03 % (2665685)------------------------------ % 124.78/18.03 % (2665685)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 124.78/18.03 % (2665685)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 124.78/18.03 % (2665685)CaDiCaL version: 2.1.3 % 124.78/18.03 % (2665685)Termination reason: Instruction limit % 124.78/18.03 % (2665685)Termination phase: Saturation % 124.78/18.03 % (2665685)Time elapsed: 5.067 s % 124.78/18.03 % (2665685)Peak memory usage: 61 MB % 124.78/18.03 % (2665685)Instructions burned: 22569 (million) % 124.78/18.03 % (2665693)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=169162035:fmbsr=2:i=32576_2917 on theBenchmark for (2917ds/32576Mi) % 124.78/18.03 % (2665693)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 124.78/18.03 % (2665693)Terminated due to inappropriate strategy. % 124.78/18.03 % (2665693)------------------------------ % 124.78/18.03 % (2665693)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 124.78/18.03 % (2665693)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 124.78/18.03 % (2665693)CaDiCaL version: 2.1.3 % 124.78/18.03 % (2665693)Termination reason: Inappropriate % 124.78/18.03 % (2665693)Time elapsed: 0.001 s % 124.78/18.03 % (2665693)Peak memory usage: 10 MB % 124.78/18.03 % (2665693)Instructions burned: 4 (million) % 124.78/18.03 % (2665693)------------------------------ % 124.78/18.03 % (2665693)------------------------------ % 124.78/18.03 % (2665695)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=2957130234:i=11404_2917 on theBenchmark for (2917ds/11404Mi) % 124.78/18.03 % (2665687)Instruction limit reached! % 124.78/18.03 % (2665687)------------------------------ % 124.78/18.03 % (2665687)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 124.78/18.03 % (2665687)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 124.78/18.03 % (2665687)CaDiCaL version: 2.1.3 % 124.78/18.03 % (2665687)Termination reason: Instruction limit % 124.78/18.03 % (2665687)Termination phase: Saturation % 124.78/18.03 % (2665687)Time elapsed: 5.576 s % 124.78/18.03 % (2665687)Peak memory usage: 57 MB % 124.78/18.03 % (2665687)Instructions burned: 8173 (million) % 124.78/18.03 % (2665697)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=3968718835:i=14134_2910 on theBenchmark for (2910ds/14134Mi) % 124.78/18.03 % (2665689)Instruction limit reached! % 124.78/18.03 % (2665689)------------------------------ % 124.78/18.03 % (2665689)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 124.78/18.03 % (2665689)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 124.78/18.03 % (2665689)CaDiCaL version: 2.1.3 % 124.78/18.03 % (2665689)Termination reason: Instruction limit % 124.78/18.03 % (2665689)Termination phase: Saturation % 124.78/18.03 % (2665689)Time elapsed: 4.995 s % 124.78/18.03 % (2665689)Peak memory usage: 50 MB % 124.78/18.03 % (2665689)Instructions burned: 9157 (million) % 124.78/18.03 % (2665699)dis+33_16_sil=32000:sac=on:random_seed=368089166:i=15851:nm=0_2909 on theBenchmark for (2909ds/15851Mi) % 124.78/18.03 % (2665695)Instruction limit reached! % 124.78/18.03 % (2665695)------------------------------ % 124.78/18.03 % (2665695)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 146.48/20.94 % (2665695)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 146.48/20.94 % (2665695)CaDiCaL version: 2.1.3 % 146.48/20.94 % (2665695)Termination reason: Instruction limit % 146.48/20.94 % (2665695)Termination phase: Saturation % 146.48/20.94 % (2665695)Time elapsed: 4.214 s % 146.48/20.94 % (2665695)Peak memory usage: 63 MB % 146.48/20.94 % (2665695)Instructions burned: 11407 (million) % 146.48/20.94 % (2665701)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=1736208118:avsq=on:i=17627:add=on:amm=off_2874 on theBenchmark for (2874ds/17627Mi) % 146.48/20.94 % (2665699)Instruction limit reached! % 146.48/20.94 % (2665699)------------------------------ % 146.48/20.94 % (2665699)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 146.48/20.94 % (2665699)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 146.48/20.94 % (2665699)CaDiCaL version: 2.1.3 % 146.48/20.94 % (2665699)Termination reason: Instruction limit % 146.48/20.94 % (2665699)Termination phase: Saturation % 146.48/20.94 % (2665699)Time elapsed: 8.077 s % 146.48/20.94 % (2665699)Peak memory usage: 189 MB % 146.48/20.94 % (2665699)Instructions burned: 15852 (million) % 146.48/20.94 % (2666035)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=3001862851:s2a=on:i=53295_2828 on theBenchmark for (2828ds/53295Mi) % 146.48/20.94 % (2665701)Instruction limit reached! % 146.48/20.94 % (2665701)------------------------------ % 146.48/20.94 % (2665701)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 146.48/20.94 % (2665701)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 146.48/20.94 % (2665701)CaDiCaL version: 2.1.3 % 146.48/20.94 % (2665701)Termination reason: Instruction limit % 146.48/20.94 % (2665701)Termination phase: Saturation % 146.48/20.94 % (2665701)Time elapsed: 4.966 s % 146.48/20.94 % (2665701)Peak memory usage: 229 MB % 146.48/20.94 % (2665701)Instructions burned: 17631 (million) % 146.48/20.94 % (2666038)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=4162138033:i=26857:ins=20_2824 on theBenchmark for (2824ds/26857Mi) % 146.48/20.94 % (2666038)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 146.48/20.94 % (2666038)Terminated due to inappropriate strategy. % 146.48/20.94 % (2666038)------------------------------ % 146.48/20.94 % (2666038)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 146.48/20.94 % (2666038)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 146.48/20.94 % (2666038)CaDiCaL version: 2.1.3 % 146.48/20.94 % (2666038)Termination reason: Inappropriate % 146.48/20.94 % (2666038)Time elapsed: 0.001 s % 146.48/20.94 % (2666038)Peak memory usage: 10 MB % 146.48/20.94 % (2666038)Instructions burned: 4 (million) % 146.48/20.94 % (2666038)------------------------------ % 146.48/20.94 % (2666038)------------------------------ % 146.48/20.94 % (2666040)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=626045935:i=28120:bs=on:fsr=off_2824 on theBenchmark for (2824ds/28120Mi) % 146.48/20.94 % (2665675)Instruction limit reached! % 146.48/20.94 % (2665675)------------------------------ % 146.48/20.94 % (2665675)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 146.48/20.94 % (2665675)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 146.48/20.94 % (2665675)CaDiCaL version: 2.1.3 % 146.48/20.94 % (2665675)Termination reason: Instruction limit % 146.48/20.94 % (2665675)Termination phase: Saturation % 146.48/20.94 % (2665675)Time elapsed: 14.931 s % 146.48/20.94 % (2665675)Peak memory usage: 93 MB % 146.48/20.94 % (2665675)Instructions burned: 29341 (million) % 146.48/20.94 % (2666052)fmb+10_1_sil=256000:fmbss=7:random_seed=3461922904:fmbsr=1.6:i=182295_2823 on theBenchmark for (2823ds/182295Mi) % 146.48/20.94 % (2666052)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 146.48/20.94 % (2666052)Terminated due to inappropriate strategy. % 146.48/20.94 % (2666052)------------------------------ % 146.48/20.94 % (2666052)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 146.48/20.94 % (2666052)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 146.48/20.94 % (2666052)CaDiCaL version: 2.1.3 % 146.48/20.94 % (2666052)Termination reason: Inappropriate % 146.48/20.94 % (2666052)Time elapsed: 0.002 s % 146.48/20.94 % (2666052)Peak memory usage: 10 MB % 146.48/20.94 % (2666052)Instructions burned: 4 (million) % 146.48/20.94 % (2666052)------------------------------ % 146.48/20.94 % (2666052)------------------------------ % 146.48/20.94 % (2666059)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=2656061658:i=44625:gsp=on_2823 on theBenchmark for (2823ds/44625Mi) % 159.47/22.71 % (2666059)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 159.47/22.71 % (2666059)Terminated due to inappropriate strategy. % 159.47/22.71 % (2666059)------------------------------ % 159.47/22.71 % (2666059)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 159.47/22.71 % (2666059)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 159.47/22.71 % (2666059)CaDiCaL version: 2.1.3 % 159.47/22.71 % (2666059)Termination reason: Inappropriate % 159.47/22.71 % (2666059)Time elapsed: 0.002 s % 159.47/22.71 % (2666059)Peak memory usage: 10 MB % 159.47/22.71 % (2666059)Instructions burned: 4 (million) % 159.47/22.71 % (2666059)------------------------------ % 159.47/22.71 % (2666059)------------------------------ % 159.47/22.71 % (2666067)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=4137982985:i=160505_2823 on theBenchmark for (2823ds/160505Mi) % 159.47/22.71 % (2666067)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 159.47/22.71 % (2666067)Terminated due to inappropriate strategy. % 159.47/22.71 % (2666067)------------------------------ % 159.47/22.71 % (2666067)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 159.47/22.71 % (2666067)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 159.47/22.71 % (2666067)CaDiCaL version: 2.1.3 % 159.47/22.71 % (2666067)Termination reason: Inappropriate % 159.47/22.71 % (2666067)Time elapsed: 0.002 s % 159.47/22.71 % (2666067)Peak memory usage: 10 MB % 159.47/22.71 % (2666067)Instructions burned: 4 (million) % 159.47/22.71 % (2666067)------------------------------ % 159.47/22.71 % (2666067)------------------------------ % 159.47/22.71 % (2666073)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=1182132993:fmbsr=1.3:i=225729_2822 on theBenchmark for (2822ds/225729Mi) % 159.47/22.71 % (2666073)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 159.47/22.71 % (2666073)Terminated due to inappropriate strategy. % 159.47/22.71 % (2666073)------------------------------ % 159.47/22.71 % (2666073)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 159.47/22.71 % (2666073)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 159.47/22.71 % (2666073)CaDiCaL version: 2.1.3 % 159.47/22.71 % (2666073)Termination reason: Inappropriate % 159.47/22.71 % (2666073)Time elapsed: 0.002 s % 159.47/22.71 % (2666073)Peak memory usage: 10 MB % 159.47/22.71 % (2666073)Instructions burned: 4 (million) % 159.47/22.71 % (2666073)------------------------------ % 159.47/22.71 % (2666073)------------------------------ % 159.47/22.71 % (2666080)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=3349434633:fmbsr=2:i=185024:ins=7_2822 on theBenchmark for (2822ds/185024Mi) % 159.47/22.71 % (2666080)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 159.47/22.71 % (2666080)Terminated due to inappropriate strategy. % 159.47/22.71 % (2666080)------------------------------ % 159.47/22.71 % (2666080)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 159.47/22.71 % (2666080)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 159.47/22.71 % (2666080)CaDiCaL version: 2.1.3 % 159.47/22.71 % (2666080)Termination reason: Inappropriate % 159.47/22.71 % (2666080)Time elapsed: 0.002 s % 159.47/22.71 % (2666080)Peak memory usage: 10 MB % 159.47/22.71 % (2666080)Instructions burned: 4 (million) % 159.47/22.71 % (2666080)------------------------------ % 159.47/22.71 % (2666080)------------------------------ % 159.47/22.71 % (2666090)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=2539008816:rtra=on_2822 on theBenchmark for (2822ds/0Mi) % 159.47/22.71 % (2666090)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 159.47/22.71 % (2666090)Terminated due to inappropriate strategy. % 159.47/22.71 % (2666090)------------------------------ % 159.47/22.71 % (2666090)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 159.47/22.71 % (2666090)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 159.47/22.71 % (2666090)CaDiCaL version: 2.1.3 % 159.47/22.71 % (2666090)Termination reason: Inappropriate % 159.47/22.71 % (2666090)Time elapsed: 0.003 s % 159.47/22.71 % (2666090)Peak memory usage: 10 MB % 159.47/22.71 % (2666090)Instructions burned: 5 (million) % 159.47/22.71 % (2666090)------------------------------ % 159.47/22.71 % (2666090)------------------------------ % 159.47/22.71 % (2666095)% WARNING: option uhcvi not known. % 159.47/22.71 % (2666095)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1017454857:i=271062:add=off:rtra=on:rawr=on_2822 on theBenchmark for (2822ds/271062Mi) % 184.32/26.25 % (2665697)Instruction limit reached! % 184.32/26.25 % (2665697)------------------------------ % 184.32/26.25 % (2665697)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 184.32/26.25 % (2665697)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 184.32/26.25 % (2665697)CaDiCaL version: 2.1.3 % 184.32/26.25 % (2665697)Termination reason: Instruction limit % 184.32/26.25 % (2665697)Termination phase: Saturation % 184.32/26.25 % (2665697)Time elapsed: 9.635 s % 184.32/26.25 % (2665697)Peak memory usage: 78 MB % 184.32/26.25 % (2665697)Instructions burned: 14134 (million) % 184.32/26.25 % (2666208)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3329903409:i=176048:add=on:rtra=on:rawr=on_2814 on theBenchmark for (2814ds/176048Mi) % 184.32/26.25 % (2665691)Instruction limit reached! % 184.32/26.25 % (2665691)------------------------------ % 184.32/26.25 % (2665691)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 184.32/26.25 % (2665691)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 184.32/26.25 % (2665691)CaDiCaL version: 2.1.3 % 184.32/26.25 % (2665691)Termination reason: Instruction limit % 184.32/26.25 % (2665691)Termination phase: Saturation % 184.32/26.25 % (2665691)Time elapsed: 14.006 s % 184.32/26.25 % (2665691)Peak memory usage: 87 MB % 184.32/26.25 % (2665691)Instructions burned: 20140 (million) % 184.32/26.25 % (2666210)dis+10_1_sil=32000:si=on:sp=arity:random_seed=38638982:i=206:fgj=on:rtra=on_2800 on theBenchmark for (2800ds/206Mi) % 184.32/26.25 % (2666210)Instruction limit reached! % 184.32/26.25 % (2666210)------------------------------ % 184.32/26.25 % (2666210)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 184.32/26.25 % (2666210)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 184.32/26.25 % (2666210)CaDiCaL version: 2.1.3 % 184.32/26.25 % (2666210)Termination reason: Instruction limit % 184.32/26.25 % (2666210)Termination phase: Saturation % 184.32/26.25 % (2666210)Time elapsed: 0.133 s % 184.32/26.25 % (2666210)Peak memory usage: 14 MB % 184.32/26.25 % (2666210)Instructions burned: 206 (million) % 184.32/26.25 % (2666212)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=238255001:i=232:rtra=on_2799 on theBenchmark for (2799ds/232Mi) % 184.32/26.25 % (2666212)Instruction limit reached! % 184.32/26.25 % (2666212)------------------------------ % 184.32/26.25 % (2666212)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 184.32/26.25 % (2666212)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 184.32/26.25 % (2666212)CaDiCaL version: 2.1.3 % 184.32/26.25 % (2666212)Termination reason: Instruction limit % 184.32/26.25 % (2666212)Termination phase: Saturation % 184.32/26.25 % (2666212)Time elapsed: 0.147 s % 184.32/26.25 % (2666212)Peak memory usage: 13 MB % 184.32/26.25 % (2666212)Instructions burned: 232 (million) % 184.32/26.25 % (2666214)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=1168972796:i=262:rtra=on_2797 on theBenchmark for (2797ds/262Mi) % 184.32/26.25 % (2666214)Instruction limit reached! % 184.32/26.25 % (2666214)------------------------------ % 184.32/26.25 % (2666214)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 184.32/26.25 % (2666214)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 184.32/26.25 % (2666214)CaDiCaL version: 2.1.3 % 184.32/26.25 % (2666214)Termination reason: Instruction limit % 184.32/26.25 % (2666214)Termination phase: Saturation % 184.32/26.25 % (2666214)Time elapsed: 0.169 s % 184.32/26.25 % (2666214)Peak memory usage: 14 MB % 184.32/26.25 % (2666214)Instructions burned: 262 (million) % 184.32/26.25 % (2666216)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=1664859350:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2795 on theBenchmark for (2795ds/318Mi) % 184.32/26.25 % (2666216)Instruction limit reached! % 184.32/26.25 % (2666216)------------------------------ % 184.32/26.25 % (2666216)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 184.32/26.25 % (2666216)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 184.32/26.25 % (2666216)CaDiCaL version: 2.1.3 % 184.32/26.25 % (2666216)Termination reason: Instruction limit % 184.32/26.25 % (2666216)Termination phase: Saturation % 184.32/26.25 % (2666216)Time elapsed: 0.219 s % 184.32/26.25 % (2666216)Peak memory usage: 15 MB % 184.32/26.25 % (2666216)Instructions burned: 319 (million) % 184.32/26.25 % (2666218)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=819977306:i=1428:nm=2:rtra=on_2793 on theBenchmark for (2793ds/1428Mi) % 194.91/27.89 % (2666218)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 194.91/27.89 % (2666218)Terminated due to inappropriate strategy. % 194.91/27.89 % (2666218)------------------------------ % 194.91/27.89 % (2666218)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 194.91/27.89 % (2666218)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 194.91/27.89 % (2666218)CaDiCaL version: 2.1.3 % 194.91/27.89 % (2666218)Termination reason: Inappropriate % 194.91/27.89 % (2666218)Time elapsed: 0.003 s % 194.91/27.89 % (2666218)Peak memory usage: 10 MB % 194.91/27.89 % (2666218)Instructions burned: 4 (million) % 194.91/27.89 % (2666218)------------------------------ % 194.91/27.89 % (2666218)------------------------------ % 194.91/27.89 % (2666220)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=97325813:i=262:bd=preordered:rtra=on:fsd=on_2792 on theBenchmark for (2792ds/262Mi) % 194.91/27.89 % (2666220)Instruction limit reached! % 194.91/27.89 % (2666220)------------------------------ % 194.91/27.89 % (2666220)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 194.91/27.89 % (2666220)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 194.91/27.89 % (2666220)CaDiCaL version: 2.1.3 % 194.91/27.89 % (2666220)Termination reason: Instruction limit % 194.91/27.89 % (2666220)Termination phase: Saturation % 194.91/27.89 % (2666220)Time elapsed: 0.184 s % 194.91/27.89 % (2666220)Peak memory usage: 15 MB % 194.91/27.89 % (2666220)Instructions burned: 262 (million) % 194.91/27.89 % (2666222)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:si=on:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=759199977:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2790 on theBenchmark for (2790ds/1368Mi) % 194.91/27.89 % (2666222)Instruction limit reached! % 194.91/27.89 % (2666222)------------------------------ % 194.91/27.89 % (2666222)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 194.91/27.89 % (2666222)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 194.91/27.89 % (2666222)CaDiCaL version: 2.1.3 % 194.91/27.89 % (2666222)Termination reason: Instruction limit % 194.91/27.89 % (2666222)Termination phase: Saturation % 194.91/27.89 % (2666222)Time elapsed: 0.684 s % 194.91/27.89 % (2666222)Peak memory usage: 18 MB % 194.91/27.89 % (2666222)Instructions burned: 1370 (million) % 194.91/27.89 % (2666224)ott-21_1_sil=16000:si=on:fs=off:random_seed=1656263570:i=360:av=off:fsr=off:rtra=on_2783 on theBenchmark for (2783ds/360Mi) % 194.91/27.89 % (2666224)Instruction limit reached! % 194.91/27.89 % (2666224)------------------------------ % 194.91/27.89 % (2666224)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 194.91/27.89 % (2666224)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 194.91/27.89 % (2666224)CaDiCaL version: 2.1.3 % 194.91/27.89 % (2666224)Termination reason: Instruction limit % 194.91/27.89 % (2666224)Termination phase: Saturation % 194.91/27.89 % (2666224)Time elapsed: 0.168 s % 194.91/27.89 % (2666224)Peak memory usage: 13 MB % 194.91/27.89 % (2666224)Instructions burned: 361 (million) % 194.91/27.89 % (2666226)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=4158725458:i=954:bd=all:rtra=on_2781 on theBenchmark for (2781ds/954Mi) % 194.91/27.89 % (2666226)Instruction limit reached! % 194.91/27.89 % (2666226)------------------------------ % 194.91/27.89 % (2666226)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 194.91/27.89 % (2666226)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 194.91/27.89 % (2666226)CaDiCaL version: 2.1.3 % 194.91/27.89 % (2666226)Termination reason: Instruction limit % 194.91/27.89 % (2666226)Termination phase: Saturation % 194.91/27.89 % (2666226)Time elapsed: 0.633 s % 194.91/27.89 % (2666226)Peak memory usage: 15 MB % 194.91/27.89 % (2666226)Instructions burned: 954 (million) % 194.91/27.89 % (2666228)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=2544201990:fmbsr=1.3:i=1730:ins=25:rtra=on_2775 on theBenchmark for (2775ds/1730Mi) % 194.91/27.89 % (2666228)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 194.91/27.89 % (2666228)Terminated due to inappropriate strategy. % 194.91/27.89 % (2666228)------------------------------ % 194.91/27.89 % (2666228)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 194.91/27.89 % (2666228)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 194.91/27.89 % (2666228)CaDiCaL version: 2.1.3 % 194.91/27.89 % (2666228)Termination reason: Inappropriate % 194.91/27.89 % (2666228)Time elapsed: 0.003 s % 258.15/36.67 % (2666228)Peak memory usage: 10 MB % 258.15/36.67 % (2666228)Instructions burned: 5 (million) % 258.15/36.67 % (2666228)------------------------------ % 258.15/36.67 % (2666228)------------------------------ % 258.15/36.67 % (2666230)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=4249695200:i=2358:rtra=on_2775 on theBenchmark for (2775ds/2358Mi) % 258.15/36.67 % (2666230)Instruction limit reached! % 258.15/36.67 % (2666230)------------------------------ % 258.15/36.67 % (2666230)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 258.15/36.67 % (2666230)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 258.15/36.67 % (2666230)CaDiCaL version: 2.1.3 % 258.15/36.67 % (2666230)Termination reason: Instruction limit % 258.15/36.67 % (2666230)Termination phase: Saturation % 258.15/36.67 % (2666230)Time elapsed: 1.557 s % 258.15/36.67 % (2666230)Peak memory usage: 25 MB % 258.15/36.67 % (2666230)Instructions burned: 2359 (million) % 258.15/36.67 % (2666232)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=2862697345:i=1778:ins=1:rtra=on_2759 on theBenchmark for (2759ds/1778Mi) % 258.15/36.67 % (2666232)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 258.15/36.67 % (2666232)Terminated due to inappropriate strategy. % 258.15/36.67 % (2666232)------------------------------ % 258.15/36.67 % (2666232)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 258.15/36.67 % (2666232)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 258.15/36.67 % (2666232)CaDiCaL version: 2.1.3 % 258.15/36.67 % (2666232)Termination reason: Inappropriate % 258.15/36.67 % (2666232)Time elapsed: 0.003 s % 258.15/36.67 % (2666232)Peak memory usage: 10 MB % 258.15/36.67 % (2666232)Instructions burned: 4 (million) % 258.15/36.67 % (2666232)------------------------------ % 258.15/36.67 % (2666232)------------------------------ % 258.15/36.67 % (2666234)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:si=on:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=1335954412:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2759 on theBenchmark for (2759ds/1384Mi) % 258.15/36.67 % (2666234)Instruction limit reached! % 258.15/36.67 % (2666234)------------------------------ % 258.15/36.67 % (2666234)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 258.15/36.67 % (2666234)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 258.15/36.67 % (2666234)CaDiCaL version: 2.1.3 % 258.15/36.67 % (2666234)Termination reason: Instruction limit % 258.15/36.67 % (2666234)Termination phase: Saturation % 258.15/36.67 % (2666234)Time elapsed: 0.826 s % 258.15/36.67 % (2666234)Peak memory usage: 22 MB % 258.15/36.67 % (2666234)Instructions burned: 1385 (million) % 258.15/36.67 % (2666236)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=2527519593:i=1758:kws=inv_precedence:fsr=off:rtra=on_2750 on theBenchmark for (2750ds/1758Mi) % 258.15/36.67 % (2666236)Instruction limit reached! % 258.15/36.67 % (2666236)------------------------------ % 258.15/36.67 % (2666236)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 258.15/36.67 % (2666236)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 258.15/36.67 % (2666236)CaDiCaL version: 2.1.3 % 258.15/36.67 % (2666236)Termination reason: Instruction limit % 258.15/36.67 % (2666236)Termination phase: Saturation % 258.15/36.67 % (2666236)Time elapsed: 1.021 s % 258.15/36.67 % (2666236)Peak memory usage: 29 MB % 258.15/36.67 % (2666236)Instructions burned: 1758 (million) % 258.15/36.67 % (2666238)fmb+10_1_sil=64000:si=on:random_seed=1874727581:i=44122:nm=2:rtra=on:gsp=on_2740 on theBenchmark for (2740ds/44122Mi) % 258.15/36.67 % (2666238)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 258.15/36.67 % (2666238)Terminated due to inappropriate strategy. % 258.15/36.67 % (2666238)------------------------------ % 258.15/36.67 % (2666238)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 258.15/36.67 % (2666238)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 258.15/36.67 % (2666238)CaDiCaL version: 2.1.3 % 258.15/36.67 % (2666238)Termination reason: Inappropriate % 258.15/36.67 % (2666238)Time elapsed: 0.003 s % 258.15/36.67 % (2666238)Peak memory usage: 10 MB % 258.15/36.67 % (2666238)Instructions burned: 4 (million) % 258.15/36.67 % (2666238)------------------------------ % 258.15/36.67 % (2666238)------------------------------ % 258.15/36.67 % (2666240)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=2616485093:i=19030:nm=5:rtra=on_2739 on theBenchmark for (2739ds/19030Mi) % 277.14/39.33 % (2666240)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 277.14/39.33 % (2666240)Terminated due to inappropriate strategy. % 277.14/39.33 % (2666240)------------------------------ % 277.14/39.33 % (2666240)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 277.14/39.33 % (2666240)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 277.14/39.33 % (2666240)CaDiCaL version: 2.1.3 % 277.14/39.33 % (2666240)Termination reason: Inappropriate % 277.14/39.33 % (2666240)Time elapsed: 0.003 s % 277.14/39.33 % (2666240)Peak memory usage: 10 MB % 277.14/39.33 % (2666240)Instructions burned: 4 (million) % 277.14/39.33 % (2666240)------------------------------ % 277.14/39.33 % (2666240)------------------------------ % 277.14/39.33 % (2666242)fmb+10_1_sil=64000:sas=cadical:si=on:fmbss=8:random_seed=4100371810:fmbsr=1.7:i=1840:rtra=on_2739 on theBenchmark for (2739ds/1840Mi) % 277.14/39.33 % (2666242)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 277.14/39.33 % (2666242)Terminated due to inappropriate strategy. % 277.14/39.33 % (2666242)------------------------------ % 277.14/39.33 % (2666242)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 277.14/39.33 % (2666242)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 277.14/39.33 % (2666242)CaDiCaL version: 2.1.3 % 277.14/39.33 % (2666242)Termination reason: Inappropriate % 277.14/39.33 % (2666242)Time elapsed: 0.003 s % 277.14/39.33 % (2666242)Peak memory usage: 10 MB % 277.14/39.33 % (2666242)Instructions burned: 4 (million) % 277.14/39.33 % (2666242)------------------------------ % 277.14/39.33 % (2666242)------------------------------ % 277.14/39.33 % (2666244)dis-4_1_sil=16000:drc=ordering:si=on:sp=const_frequency:sac=on:newcnf=on:random_seed=2264287840:i=10262:rtra=on_2739 on theBenchmark for (2739ds/10262Mi) % 277.14/39.33 % (2666040)Instruction limit reached! % 277.14/39.33 % (2666040)------------------------------ % 277.14/39.33 % (2666040)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 277.14/39.33 % (2666040)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 277.14/39.33 % (2666040)CaDiCaL version: 2.1.3 % 277.14/39.33 % (2666040)Termination reason: Instruction limit % 277.14/39.33 % (2666040)Termination phase: Saturation % 277.14/39.33 % (2666040)Time elapsed: 9.247 s % 277.14/39.33 % (2666040)Peak memory usage: 89 MB % 277.14/39.33 % (2666040)Instructions burned: 28122 (million) % 277.14/39.33 % (2666246)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:si=on:sp=arity:spb=units:lsd=10:nwc=3:random_seed=4288932320:i=2944:ins=7:rtra=on:fdi=8:gsp=on_2732 on theBenchmark for (2732ds/2944Mi) % 277.14/39.33 % (2666246)Instruction limit reached! % 277.14/39.33 % (2666246)------------------------------ % 277.14/39.33 % (2666246)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 277.14/39.33 % (2666246)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 277.14/39.33 % (2666246)CaDiCaL version: 2.1.3 % 277.14/39.33 % (2666246)Termination reason: Instruction limit % 277.14/39.33 % (2666246)Termination phase: Saturation % 277.14/39.33 % (2666246)Time elapsed: 0.813 s % 277.14/39.33 % (2666246)Peak memory usage: 44 MB % 277.14/39.33 % (2666246)Instructions burned: 2949 (million) % 277.14/39.33 % (2666248)fmb+10_1_sil=16000:sas=cadical:si=on:bce=on:fmbss=77:random_seed=485248812:i=12648:rtra=on_2723 on theBenchmark for (2723ds/12648Mi) % 277.14/39.33 % (2666248)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 277.14/39.33 % (2666248)Terminated due to inappropriate strategy. % 277.14/39.33 % (2666248)------------------------------ % 277.14/39.33 % (2666248)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 277.14/39.33 % (2666248)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 277.14/39.33 % (2666248)CaDiCaL version: 2.1.3 % 277.14/39.33 % (2666248)Termination reason: Inappropriate % 277.14/39.33 % (2666248)Time elapsed: 0.003 s % 277.14/39.33 % (2666248)Peak memory usage: 10 MB % 277.14/39.33 % (2666248)Instructions burned: 5 (million) % 277.14/39.33 % (2666248)------------------------------ % 277.14/39.33 % (2666248)------------------------------ % 277.14/39.33 % (2666250)fmb+10_1_fmbas=function:sil=32000:sas=cadical:si=on:fmbss=16:random_seed=2671009938:fmbsr=2.30978:i=4348:rtra=on_2723 on theBenchmark for (2723ds/4348Mi) % 277.14/39.33 % (2666250)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 277.14/39.33 % (2666250)Terminated due to inappropriate strategy. % 277.14/39.33 % (2666250)------------------------------ % 277.14/39.33 % (2666250)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.05/42.53 % (2666250)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.05/42.53 % (2666250)CaDiCaL version: 2.1.3 % 300.05/42.53 % (2666250)Termination reason: Inappropriate % 300.05/42.53 % (2666250)Time elapsed: 0.003 s % 300.05/42.53 % (2666250)Peak memory usage: 10 MB % 300.05/42.53 % (2666250)Instructions burned: 4 (million) % 300.05/42.53 % (2666250)------------------------------ % 300.05/42.53 % (2666250)------------------------------ % 300.05/42.53 % (2666252)ott-2_1_sil=16000:si=on:newcnf=on:random_seed=243818294:avsq=on:i=1738:avsqr=1,16:kws=inv_arity_squared:rtra=on_2723 on theBenchmark for (2723ds/1738Mi) % 300.05/42.53 % (2666252)Instruction limit reached! % 300.05/42.53 % (2666252)------------------------------ % 300.05/42.53 % (2666252)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.05/42.53 % (2666252)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.05/42.53 % (2666252)CaDiCaL version: 2.1.3 % 300.05/42.53 % (2666252)Termination reason: Instruction limit % 300.05/42.53 % (2666252)Termination phase: Saturation % 300.05/42.53 % (2666252)Time elapsed: 0.597 s % 300.05/42.53 % (2666252)Peak memory usage: 20 MB % 300.05/42.53 % (2666252)Instructions burned: 1740 (million) % 300.05/42.53 % (2666280)ott+10_1_sil=32000:tgt=ground:si=on:random_seed=2881906845:i=10228:av=off:rtra=on_2717 on theBenchmark for (2717ds/10228Mi) % 300.05/42.53 % (2666280)Instruction limit reached! % 300.05/42.53 % (2666280)------------------------------ % 300.05/42.53 % (2666280)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.05/42.53 % (2666280)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.05/42.53 % (2666280)CaDiCaL version: 2.1.3 % 300.05/42.53 % (2666280)Termination reason: Instruction limit % 300.05/42.53 % (2666280)Termination phase: Saturation % 300.05/42.53 % (2666280)Time elapsed: 4.483 s % 300.05/42.53 % (2666280)Peak memory usage: 55 MB % 300.05/42.53 % (2666280)Instructions burned: 10230 (million) % 300.05/42.53 % (2666601)fmb+10_1_sil=64000:sas=cadical:si=on:bce=on:rp=on:random_seed=3876822305:i=108564:rtra=on_2672 on theBenchmark for (2672ds/108564Mi) % 300.05/42.53 % (2666601)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 300.05/42.53 % (2666601)Terminated due to inappropriate strategy. % 300.05/42.53 % (2666601)------------------------------ % 300.05/42.53 % (2666601)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.05/42.53 % (2666601)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.05/42.53 % (2666601)CaDiCaL version: 2.1.3 % 300.05/42.53 % (2666601)Termination reason: Inappropriate % 300.05/42.53 % (2666601)Time elapsed: 0.001 s % 300.05/42.53 % (2666601)Peak memory usage: 10 MB % 300.05/42.53 % (2666601)Instructions burned: 5 (million) % 300.05/42.53 % (2666601)------------------------------ % 300.05/42.53 % (2666601)------------------------------ % 300.05/42.53 % (2666603)dis-11_1_sil=16000:si=on:sp=reverse_frequency:alpa=true:random_seed=3406184992:i=7024:aac=none:rtra=on_2672 on theBenchmark for (2672ds/7024Mi) % 300.05/42.53 % (2666244)Instruction limit reached! % 300.05/42.53 % (2666244)------------------------------ % 300.05/42.53 % (2666244)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.05/42.53 % (2666244)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.05/42.53 % (2666244)CaDiCaL version: 2.1.3 % 300.05/42.53 % (2666244)Termination reason: Instruction limit % 300.05/42.53 % (2666244)Termination phase: Saturation % 300.05/42.53 % (2666244)Time elapsed: 6.928 s % 300.05/42.53 % (2666244)Peak memory usage: 68 MB % 300.05/42.53 % (2666244)Instructions burned: 10263 (million) % 300.05/42.53 % (2666606)dis+21_1_sil=32000:sas=cadical:si=on:random_seed=1884804602:i=7546:rtra=on:amm=off_2669 on theBenchmark for (2669ds/7546Mi) % 300.05/42.53 % (2666603)Instruction limit reached! % 300.05/42.53 % (2666603)------------------------------ % 300.05/42.53 % (2666603)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.05/42.53 % (2666603)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.05/42.53 % (2666603)CaDiCaL version: 2.1.3 % 300.05/42.53 % (2666603)Termination reason: Instruction limit % 300.05/42.53 % (2666603)Termination phase: Saturation % 300.05/42.53 % (2666603)Time elapsed: 2.237 s % 300.05/42.53 % (2666603)Peak memory usage: 46 MB % 300.05/42.53 % (2666603)Instructions burned: 7026 (million) % 300.05/42.53 % (2666763)ott+11_1_sil=16000:si=on:gs=on:random_seed=2770379577:s2a=on:i=4502:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:rtra=on:fsd=on_2649 on theBenchmark for (2649ds/4502Mi) % 300.05/42.54 Terminated % 300.05/42.54 % Vampire exiting % 300.05/42.54 Terminated %------------------------------------------------------------------------------