%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWW612_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 : n013.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:31 PM UTC 2026 % Result : Timeout 290.43s 41.14s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : SWW612_2 : TPTP v9.3.1. Released v6.1.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.09/0.18 % Computer : n013.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.18 % CPULimit : 300 % 0.09/0.18 % WCLimit : 300 % 0.09/0.18 % DateTime : Mon Sep 28 14:22:06 UTC 2026 % 0.09/0.18 % CPUTime : % 0.09/0.18 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.68/0.89 % (1213243)Will run a generic schedule for satisfiability detection. % 3.68/0.89 % (1213253)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3963128613:i=131_2999 on theBenchmark for (2999ds/131Mi) % 3.68/0.89 % (1213249)% WARNING: option uhcvi not known. % 3.68/0.89 % (1213248)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=655056565_2999 on theBenchmark for (2999ds/0Mi) % 3.68/0.89 % (1213249)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1464245596:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 3.68/0.89 % (1213250)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2596116254:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 3.68/0.89 % (1213251)dis+10_1_sil=32000:sp=arity:random_seed=1111732274:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 3.68/0.89 % (1213252)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=937120877:i=116_2999 on theBenchmark for (2999ds/116Mi) % 3.68/0.89 % (1213254)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1682526979:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 3.68/0.89 % (1213248)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.68/0.89 % (1213248)Terminated due to inappropriate strategy. % 3.68/0.89 % (1213248)------------------------------ % 3.68/0.89 % (1213248)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.68/0.89 % (1213248)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.68/0.89 % (1213248)CaDiCaL version: 2.1.3 % 3.68/0.89 % (1213248)Termination reason: Inappropriate % 3.68/0.89 % (1213248)Time elapsed: 0.006 s % 3.68/0.89 % (1213248)Peak memory usage: 11 MB % 3.68/0.89 % (1213248)Instructions burned: 12 (million) % 3.68/0.89 % (1213248)------------------------------ % 3.68/0.89 % (1213248)------------------------------ % 3.68/0.89 % (1213262)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2520259743:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 3.68/0.89 % (1213262)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.68/0.89 % (1213262)Terminated due to inappropriate strategy. % 3.68/0.89 % (1213262)------------------------------ % 3.68/0.89 % (1213262)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.68/0.89 % (1213262)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.68/0.89 % (1213262)CaDiCaL version: 2.1.3 % 3.68/0.89 % (1213262)Termination reason: Inappropriate % 3.68/0.89 % (1213262)Time elapsed: 0.005 s % 3.68/0.89 % (1213262)Peak memory usage: 11 MB % 3.68/0.89 % (1213262)Instructions burned: 10 (million) % 3.68/0.89 % (1213262)------------------------------ % 3.68/0.89 % (1213262)------------------------------ % 3.68/0.89 % (1213253)Instruction limit reached! % 3.68/0.89 % (1213253)------------------------------ % 3.68/0.89 % (1213253)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.68/0.89 % (1213253)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.68/0.89 % (1213253)CaDiCaL version: 2.1.3 % 3.68/0.89 % (1213253)Termination reason: Instruction limit % 3.68/0.89 % (1213253)Termination phase: Saturation % 3.68/0.89 % (1213253)Time elapsed: 0.049 s % 3.68/0.89 % (1213253)Peak memory usage: 14 MB % 3.68/0.89 % (1213253)Instructions burned: 133 (million) % 3.68/0.89 % (1213265)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=1103535854:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi) % 3.68/0.89 % (1213264)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2120371948:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 3.68/0.89 % (1213251)Instruction limit reached! % 3.68/0.89 % (1213251)------------------------------ % 3.68/0.89 % (1213251)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.68/0.89 % (1213251)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.68/0.89 % (1213251)CaDiCaL version: 2.1.3 % 3.68/0.89 % (1213251)Termination reason: Instruction limit % 3.68/0.89 % (1213251)Termination phase: Saturation % 3.68/0.89 % (1213251)Time elapsed: 0.069 s % 3.68/0.89 % (1213251)Peak memory usage: 13 MB % 3.68/0.89 % (1213251)Instructions burned: 104 (million) % 3.68/0.89 % (1213252)Instruction limit reached! % 3.68/0.89 % (1213252)------------------------------ % 3.68/0.89 % (1213252)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 4.18/1.03 % (1213252)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.18/1.03 % (1213252)CaDiCaL version: 2.1.3 % 4.18/1.03 % (1213252)Termination reason: Instruction limit % 4.18/1.03 % (1213252)Termination phase: Saturation % 4.18/1.03 % (1213252)Time elapsed: 0.076 s % 4.18/1.03 % (1213252)Peak memory usage: 13 MB % 4.18/1.03 % (1213252)Instructions burned: 117 (million) % 4.18/1.03 % (1213268)ott-21_1_sil=16000:fs=off:random_seed=613666620:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 4.18/1.03 % (1213269)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3646653330:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 4.18/1.03 % (1213254)Instruction limit reached! % 4.18/1.03 % (1213254)------------------------------ % 4.18/1.03 % (1213254)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 4.18/1.03 % (1213254)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.18/1.03 % (1213254)CaDiCaL version: 2.1.3 % 4.18/1.03 % (1213254)Termination reason: Instruction limit % 4.18/1.03 % (1213254)Termination phase: Saturation % 4.18/1.03 % (1213254)Time elapsed: 0.098 s % 4.18/1.03 % (1213254)Peak memory usage: 14 MB % 4.18/1.03 % (1213254)Instructions burned: 160 (million) % 4.18/1.03 % (1213272)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1940457336:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 4.18/1.03 % (1213272)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 4.18/1.03 % (1213272)Terminated due to inappropriate strategy. % 4.18/1.03 % (1213272)------------------------------ % 4.18/1.03 % (1213272)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 4.18/1.03 % (1213272)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.18/1.03 % (1213272)CaDiCaL version: 2.1.3 % 4.18/1.03 % (1213272)Termination reason: Inappropriate % 4.18/1.03 % (1213272)Time elapsed: 0.005 s % 4.18/1.03 % (1213272)Peak memory usage: 11 MB % 4.18/1.03 % (1213272)Instructions burned: 10 (million) % 4.18/1.03 % (1213272)------------------------------ % 4.18/1.03 % (1213272)------------------------------ % 4.18/1.03 % (1213264)Instruction limit reached! % 4.18/1.03 % (1213264)------------------------------ % 4.18/1.03 % (1213264)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 4.18/1.03 % (1213264)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.18/1.03 % (1213264)CaDiCaL version: 2.1.3 % 4.18/1.03 % (1213264)Termination reason: Instruction limit % 4.18/1.03 % (1213264)Termination phase: Saturation % 4.18/1.03 % (1213264)Time elapsed: 0.088 s % 4.18/1.03 % (1213264)Peak memory usage: 13 MB % 4.18/1.03 % (1213264)Instructions burned: 132 (million) % 4.18/1.03 % (1213274)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1012168334:i=1179_2998 on theBenchmark for (2998ds/1179Mi) % 4.18/1.03 % (1213275)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=972118130:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi) % 4.18/1.03 % (1213275)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 4.18/1.03 % (1213275)Terminated due to inappropriate strategy. % 4.18/1.03 % (1213275)------------------------------ % 4.18/1.03 % (1213275)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 4.18/1.03 % (1213275)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.18/1.03 % (1213275)CaDiCaL version: 2.1.3 % 4.18/1.03 % (1213275)Termination reason: Inappropriate % 4.18/1.03 % (1213275)Time elapsed: 0.005 s % 4.18/1.03 % (1213275)Peak memory usage: 10 MB % 4.18/1.03 % (1213275)Instructions burned: 10 (million) % 4.18/1.03 % (1213275)------------------------------ % 4.18/1.03 % (1213275)------------------------------ % 4.18/1.03 % (1213268)Instruction limit reached! % 4.18/1.03 % (1213268)------------------------------ % 4.18/1.03 % (1213268)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 4.18/1.03 % (1213268)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.18/1.03 % (1213268)CaDiCaL version: 2.1.3 % 4.18/1.03 % (1213268)Termination reason: Instruction limit % 4.18/1.03 % (1213268)Termination phase: Saturation % 4.18/1.03 % (1213268)Time elapsed: 0.095 s % 4.18/1.03 % (1213268)Peak memory usage: 13 MB % 4.18/1.03 % (1213268)Instructions burned: 180 (million) % 4.18/1.03 % (1213278)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=3131289069: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) % 20.65/3.17 % (1213279)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=809222483:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi) % 20.65/3.17 % (1213265)Instruction limit reached! % 20.65/3.17 % (1213265)------------------------------ % 20.65/3.17 % (1213265)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 20.65/3.17 % (1213265)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.65/3.17 % (1213265)CaDiCaL version: 2.1.3 % 20.65/3.17 % (1213265)Termination reason: Instruction limit % 20.65/3.17 % (1213265)Termination phase: Saturation % 20.65/3.17 % (1213265)Time elapsed: 0.217 s % 20.65/3.17 % (1213265)Peak memory usage: 19 MB % 20.65/3.17 % (1213265)Instructions burned: 685 (million) % 20.65/3.17 % (1213282)fmb+10_1_sil=64000:random_seed=1642187828:i=22061:nm=2:gsp=on_2996 on theBenchmark for (2996ds/22061Mi) % 20.65/3.17 % (1213282)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 20.65/3.17 % (1213282)Terminated due to inappropriate strategy. % 20.65/3.17 % (1213282)------------------------------ % 20.65/3.17 % (1213282)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 20.65/3.17 % (1213282)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.65/3.17 % (1213282)CaDiCaL version: 2.1.3 % 20.65/3.17 % (1213282)Termination reason: Inappropriate % 20.65/3.17 % (1213282)Time elapsed: 0.003 s % 20.65/3.17 % (1213282)Peak memory usage: 11 MB % 20.65/3.17 % (1213282)Instructions burned: 11 (million) % 20.65/3.17 % (1213282)------------------------------ % 20.65/3.17 % (1213282)------------------------------ % 20.65/3.17 % (1213284)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=4195817902:i=9515:nm=5_2996 on theBenchmark for (2996ds/9515Mi) % 20.65/3.17 % (1213284)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 20.65/3.17 % (1213284)Terminated due to inappropriate strategy. % 20.65/3.17 % (1213284)------------------------------ % 20.65/3.17 % (1213284)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 20.65/3.17 % (1213284)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.65/3.17 % (1213284)CaDiCaL version: 2.1.3 % 20.65/3.17 % (1213284)Termination reason: Inappropriate % 20.65/3.17 % (1213284)Time elapsed: 0.003 s % 20.65/3.17 % (1213284)Peak memory usage: 11 MB % 20.65/3.17 % (1213284)Instructions burned: 10 (million) % 20.65/3.17 % (1213284)------------------------------ % 20.65/3.17 % (1213284)------------------------------ % 20.65/3.17 % (1213286)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=737635324:fmbsr=1.7:i=920_2996 on theBenchmark for (2996ds/920Mi) % 20.65/3.17 % (1213286)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 20.65/3.17 % (1213286)Terminated due to inappropriate strategy. % 20.65/3.17 % (1213286)------------------------------ % 20.65/3.17 % (1213286)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 20.65/3.17 % (1213286)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.65/3.17 % (1213286)CaDiCaL version: 2.1.3 % 20.65/3.17 % (1213286)Termination reason: Inappropriate % 20.65/3.17 % (1213286)Time elapsed: 0.003 s % 20.65/3.17 % (1213286)Peak memory usage: 11 MB % 20.65/3.17 % (1213286)Instructions burned: 10 (million) % 20.65/3.17 % (1213286)------------------------------ % 20.65/3.17 % (1213286)------------------------------ % 20.65/3.17 % (1213288)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=3107361937:i=5131_2996 on theBenchmark for (2996ds/5131Mi) % 20.65/3.17 % (1213269)Instruction limit reached! % 20.65/3.17 % (1213269)------------------------------ % 20.65/3.17 % (1213269)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 20.65/3.17 % (1213269)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.65/3.17 % (1213269)CaDiCaL version: 2.1.3 % 20.65/3.17 % (1213269)Termination reason: Instruction limit % 20.65/3.17 % (1213269)Termination phase: Saturation % 20.65/3.17 % (1213269)Time elapsed: 0.271 s % 20.65/3.17 % (1213269)Peak memory usage: 14 MB % 20.65/3.17 % (1213269)Instructions burned: 479 (million) % 20.65/3.17 % (1213290)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=381020194:i=1472:ins=7:fdi=8:gsp=on_2995 on theBenchmark for (2995ds/1472Mi) % 20.65/3.17 % (1213278)Instruction limit reached! % 20.65/3.17 % (1213278)------------------------------ % 28.17/4.24 % (1213278)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 28.17/4.24 % (1213278)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.17/4.24 % (1213278)CaDiCaL version: 2.1.3 % 28.17/4.24 % (1213278)Termination reason: Instruction limit % 28.17/4.24 % (1213278)Termination phase: Saturation % 28.17/4.24 % (1213278)Time elapsed: 0.433 s % 28.17/4.24 % (1213278)Peak memory usage: 18 MB % 28.17/4.24 % (1213278)Instructions burned: 692 (million) % 28.17/4.24 % (1213292)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3886201910:i=6324_2993 on theBenchmark for (2993ds/6324Mi) % 28.17/4.24 % (1213292)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 28.17/4.24 % (1213292)Terminated due to inappropriate strategy. % 28.17/4.24 % (1213292)------------------------------ % 28.17/4.24 % (1213292)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 28.17/4.24 % (1213292)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.17/4.24 % (1213292)CaDiCaL version: 2.1.3 % 28.17/4.24 % (1213292)Termination reason: Inappropriate % 28.17/4.24 % (1213292)Time elapsed: 0.007 s % 28.17/4.24 % (1213292)Peak memory usage: 11 MB % 28.17/4.24 % (1213292)Instructions burned: 12 (million) % 28.17/4.24 % (1213292)------------------------------ % 28.17/4.24 % (1213292)------------------------------ % 28.17/4.24 % (1213294)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1197098705:fmbsr=2.30978:i=2174_2993 on theBenchmark for (2993ds/2174Mi) % 28.17/4.24 % (1213294)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 28.17/4.24 % (1213294)Terminated due to inappropriate strategy. % 28.17/4.24 % (1213294)------------------------------ % 28.17/4.24 % (1213294)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 28.17/4.24 % (1213294)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.17/4.24 % (1213294)CaDiCaL version: 2.1.3 % 28.17/4.24 % (1213294)Termination reason: Inappropriate % 28.17/4.24 % (1213294)Time elapsed: 0.005 s % 28.17/4.24 % (1213294)Peak memory usage: 11 MB % 28.17/4.24 % (1213294)Instructions burned: 10 (million) % 28.17/4.24 % (1213294)------------------------------ % 28.17/4.24 % (1213294)------------------------------ % 28.17/4.24 % (1213296)ott-2_1_sil=16000:newcnf=on:random_seed=627807027:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2992 on theBenchmark for (2992ds/869Mi) % 28.17/4.24 % (1213279)Instruction limit reached! % 28.17/4.24 % (1213279)------------------------------ % 28.17/4.24 % (1213279)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 28.17/4.24 % (1213279)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.17/4.24 % (1213279)CaDiCaL version: 2.1.3 % 28.17/4.24 % (1213279)Termination reason: Instruction limit % 28.17/4.24 % (1213279)Termination phase: Saturation % 28.17/4.24 % (1213279)Time elapsed: 0.510 s % 28.17/4.24 % (1213279)Peak memory usage: 20 MB % 28.17/4.24 % (1213279)Instructions burned: 880 (million) % 28.17/4.24 % (1213274)Instruction limit reached! % 28.17/4.24 % (1213274)------------------------------ % 28.17/4.24 % (1213274)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 28.17/4.24 % (1213274)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.17/4.24 % (1213274)CaDiCaL version: 2.1.3 % 28.17/4.24 % (1213274)Termination reason: Instruction limit % 28.17/4.24 % (1213274)Termination phase: Saturation % 28.17/4.24 % (1213274)Time elapsed: 0.588 s % 28.17/4.24 % (1213274)Peak memory usage: 23 MB % 28.17/4.24 % (1213274)Instructions burned: 1187 (million) % 28.17/4.24 % (1213298)ott+10_1_sil=32000:tgt=ground:random_seed=4031189991:i=5114:av=off_2992 on theBenchmark for (2992ds/5114Mi) % 28.17/4.24 % (1213299)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=3472278822:i=54282_2992 on theBenchmark for (2992ds/54282Mi) % 28.17/4.24 % (1213299)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 28.17/4.24 % (1213299)Terminated due to inappropriate strategy. % 28.17/4.24 % (1213299)------------------------------ % 28.17/4.24 % (1213299)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 28.17/4.24 % (1213299)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.17/4.24 % (1213299)CaDiCaL version: 2.1.3 % 28.17/4.24 % (1213299)Termination reason: Inappropriate % 28.17/4.24 % (1213299)Time elapsed: 0.007 s % 28.17/4.24 % (1213299)Peak memory usage: 11 MB % 28.17/4.24 % (1213299)Instructions burned: 12 (million) % 112.95/16.17 % (1213299)------------------------------ % 112.95/16.17 % (1213299)------------------------------ % 112.95/16.17 % (1213302)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=1056361242:i=3512:aac=none_2991 on theBenchmark for (2991ds/3512Mi) % 112.95/16.17 % (1213296)Instruction limit reached! % 112.95/16.17 % (1213296)------------------------------ % 112.95/16.17 % (1213296)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 112.95/16.17 % (1213296)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 112.95/16.17 % (1213296)CaDiCaL version: 2.1.3 % 112.95/16.17 % (1213296)Termination reason: Instruction limit % 112.95/16.17 % (1213296)Termination phase: Saturation % 112.95/16.17 % (1213296)Time elapsed: 0.558 s % 112.95/16.17 % (1213296)Peak memory usage: 19 MB % 112.95/16.17 % (1213296)Instructions burned: 870 (million) % 112.95/16.17 % (1213304)dis+21_1_sil=32000:sas=cadical:random_seed=599030100:i=3773:amm=off_2987 on theBenchmark for (2987ds/3773Mi) % 112.95/16.17 % (1213290)Instruction limit reached! % 112.95/16.17 % (1213290)------------------------------ % 112.95/16.17 % (1213290)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 112.95/16.17 % (1213290)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 112.95/16.17 % (1213290)CaDiCaL version: 2.1.3 % 112.95/16.17 % (1213290)Termination reason: Instruction limit % 112.95/16.17 % (1213290)Termination phase: Saturation % 112.95/16.17 % (1213290)Time elapsed: 0.892 s % 112.95/16.17 % (1213290)Peak memory usage: 34 MB % 112.95/16.17 % (1213290)Instructions burned: 1472 (million) % 112.95/16.17 % (1213308)ott+11_1_sil=16000:gs=on:random_seed=1585927076:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2986 on theBenchmark for (2986ds/2251Mi) % 112.95/16.17 % (1213288)Instruction limit reached! % 112.95/16.17 % (1213288)------------------------------ % 112.95/16.17 % (1213288)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 112.95/16.17 % (1213288)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 112.95/16.17 % (1213288)CaDiCaL version: 2.1.3 % 112.95/16.17 % (1213288)Termination reason: Instruction limit % 112.95/16.17 % (1213288)Termination phase: Saturation % 112.95/16.17 % (1213288)Time elapsed: 1.527 s % 112.95/16.17 % (1213288)Peak memory usage: 43 MB % 112.95/16.17 % (1213288)Instructions burned: 5132 (million) % 112.95/16.17 % (1213392)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=1800378974:fmbsr=1.6:i=67534_2981 on theBenchmark for (2981ds/67534Mi) % 112.95/16.17 % (1213392)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 112.95/16.17 % (1213392)Terminated due to inappropriate strategy. % 112.95/16.17 % (1213392)------------------------------ % 112.95/16.17 % (1213392)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 112.95/16.17 % (1213392)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 112.95/16.17 % (1213392)CaDiCaL version: 2.1.3 % 112.95/16.17 % (1213392)Termination reason: Inappropriate % 112.95/16.17 % (1213392)Time elapsed: 0.003 s % 112.95/16.17 % (1213392)Peak memory usage: 11 MB % 112.95/16.17 % (1213392)Instructions burned: 11 (million) % 112.95/16.17 % (1213392)------------------------------ % 112.95/16.17 % (1213392)------------------------------ % 112.95/16.17 % (1213397)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=97705473:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2980 on theBenchmark for (2980ds/4591Mi) % 112.95/16.17 % (1213308)Instruction limit reached! % 112.95/16.17 % (1213308)------------------------------ % 112.95/16.17 % (1213308)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 112.95/16.17 % (1213308)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 112.95/16.17 % (1213308)CaDiCaL version: 2.1.3 % 112.95/16.17 % (1213308)Termination reason: Instruction limit % 112.95/16.17 % (1213308)Termination phase: Saturation % 112.95/16.17 % (1213308)Time elapsed: 1.354 s % 112.95/16.17 % (1213308)Peak memory usage: 27 MB % 112.95/16.17 % (1213308)Instructions burned: 2253 (million) % 112.95/16.17 % (1213576)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=1938495098:i=29340_2972 on theBenchmark for (2972ds/29340Mi) % 112.95/16.17 % (1213302)Instruction limit reached! % 112.95/16.17 % (1213302)------------------------------ % 112.95/16.17 % (1213302)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 112.95/16.17 % (1213302)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 112.95/16.17 % (1213302)CaDiCaL version: 2.1.3 % 112.95/16.17 % (1213302)Termination reason: Instruction limit % 129.69/18.52 % (1213302)Termination phase: Saturation % 129.69/18.52 % (1213302)Time elapsed: 2.119 s % 129.69/18.52 % (1213302)Peak memory usage: 36 MB % 129.69/18.52 % (1213302)Instructions burned: 3513 (million) % 129.69/18.52 % (1213630)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=3658973277:i=5211_2970 on theBenchmark for (2970ds/5211Mi) % 129.69/18.52 % (1213397)Instruction limit reached! % 129.69/18.52 % (1213397)------------------------------ % 129.69/18.52 % (1213397)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 129.69/18.52 % (1213397)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 129.69/18.52 % (1213397)CaDiCaL version: 2.1.3 % 129.69/18.52 % (1213397)Termination reason: Instruction limit % 129.69/18.52 % (1213397)Termination phase: Saturation % 129.69/18.52 % (1213397)Time elapsed: 1.245 s % 129.69/18.52 % (1213397)Peak memory usage: 40 MB % 129.69/18.52 % (1213397)Instructions burned: 4594 (million) % 129.69/18.52 % (1213681)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=699238354:i=5497:nm=2_2968 on theBenchmark for (2968ds/5497Mi) % 129.69/18.52 % (1213681)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 129.69/18.52 % (1213681)Terminated due to inappropriate strategy. % 129.69/18.52 % (1213681)------------------------------ % 129.69/18.52 % (1213681)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 129.69/18.52 % (1213681)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 129.69/18.52 % (1213681)CaDiCaL version: 2.1.3 % 129.69/18.52 % (1213681)Termination reason: Inappropriate % 129.69/18.52 % (1213681)Time elapsed: 0.003 s % 129.69/18.52 % (1213681)Peak memory usage: 11 MB % 129.69/18.52 % (1213681)Instructions burned: 11 (million) % 129.69/18.52 % (1213681)------------------------------ % 129.69/18.52 % (1213681)------------------------------ % 129.69/18.52 % (1213685)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=3552533868:fmbsr=2:i=46332_2968 on theBenchmark for (2968ds/46332Mi) % 129.69/18.52 % (1213685)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 129.69/18.52 % (1213685)Terminated due to inappropriate strategy. % 129.69/18.52 % (1213685)------------------------------ % 129.69/18.52 % (1213685)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 129.69/18.52 % (1213685)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 129.69/18.52 % (1213685)CaDiCaL version: 2.1.3 % 129.69/18.52 % (1213685)Termination reason: Inappropriate % 129.69/18.52 % (1213685)Time elapsed: 0.006 s % 129.69/18.52 % (1213685)Peak memory usage: 11 MB % 129.69/18.52 % (1213685)Instructions burned: 11 (million) % 129.69/18.52 % (1213685)------------------------------ % 129.69/18.52 % (1213685)------------------------------ % 129.69/18.52 % (1213691)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=958727082:i=14071_2967 on theBenchmark for (2967ds/14071Mi) % 129.69/18.52 % (1213691)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 129.69/18.52 % (1213691)Terminated due to inappropriate strategy. % 129.69/18.52 % (1213691)------------------------------ % 129.69/18.52 % (1213691)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 129.69/18.52 % (1213691)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 129.69/18.52 % (1213691)CaDiCaL version: 2.1.3 % 129.69/18.52 % (1213691)Termination reason: Inappropriate % 129.69/18.52 % (1213691)Time elapsed: 0.006 s % 129.69/18.52 % (1213691)Peak memory usage: 11 MB % 129.69/18.52 % (1213691)Instructions burned: 11 (million) % 129.69/18.52 % (1213691)------------------------------ % 129.69/18.52 % (1213691)------------------------------ % 129.69/18.52 % (1213693)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2244470138:i=22565:add=on:rawr=on_2967 on theBenchmark for (2967ds/22565Mi) % 129.69/18.52 % (1213304)Instruction limit reached! % 129.69/18.52 % (1213304)------------------------------ % 129.69/18.52 % (1213304)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 129.69/18.52 % (1213304)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 129.69/18.52 % (1213304)CaDiCaL version: 2.1.3 % 129.69/18.52 % (1213304)Termination reason: Instruction limit % 129.69/18.52 % (1213304)Termination phase: Saturation % 129.69/18.52 % (1213304)Time elapsed: 2.291 s % 129.69/18.52 % (1213304)Peak memory usage: 36 MB % 129.69/18.52 % (1213304)Instructions burned: 3773 (million) % 129.69/18.52 % (1213695)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=1712049007:i=8173:av=off_2963 on theBenchmark for (2963ds/8173Mi) % 129.69/18.52 % (1213298)Instruction limit reached! % 130.42/18.66 % (1213298)------------------------------ % 130.42/18.66 % (1213298)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 130.42/18.66 % (1213298)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 130.42/18.66 % (1213298)CaDiCaL version: 2.1.3 % 130.42/18.66 % (1213298)Termination reason: Instruction limit % 130.42/18.66 % (1213298)Termination phase: Saturation % 130.42/18.66 % (1213298)Time elapsed: 3.233 s % 130.42/18.66 % (1213298)Peak memory usage: 44 MB % 130.42/18.66 % (1213298)Instructions burned: 5115 (million) % 130.42/18.66 % (1213697)dis+10_16:1_sil=16000:random_seed=662294252:i=9155:fsr=off_2959 on theBenchmark for (2959ds/9155Mi) % 130.42/18.66 % (1213630)Instruction limit reached! % 130.42/18.66 % (1213630)------------------------------ % 130.42/18.66 % (1213630)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 130.42/18.66 % (1213630)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 130.42/18.66 % (1213630)CaDiCaL version: 2.1.3 % 130.42/18.66 % (1213630)Termination reason: Instruction limit % 130.42/18.66 % (1213630)Termination phase: Saturation % 130.42/18.66 % (1213630)Time elapsed: 2.624 s % 130.42/18.66 % (1213630)Peak memory usage: 43 MB % 130.42/18.66 % (1213630)Instructions burned: 5213 (million) % 130.42/18.66 % (1213699)ott-3_8_sil=64000:random_seed=3303027439:i=20139:bs=on_2944 on theBenchmark for (2944ds/20139Mi) % 130.42/18.66 % (1213695)Instruction limit reached! % 130.42/18.66 % (1213695)------------------------------ % 130.42/18.66 % (1213695)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 130.42/18.66 % (1213695)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 130.42/18.66 % (1213695)CaDiCaL version: 2.1.3 % 130.42/18.66 % (1213695)Termination reason: Instruction limit % 130.42/18.66 % (1213695)Termination phase: Saturation % 130.42/18.66 % (1213695)Time elapsed: 5.158 s % 130.42/18.66 % (1213695)Peak memory usage: 95 MB % 130.42/18.66 % (1213695)Instructions burned: 8174 (million) % 130.42/18.66 % (1213701)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=678843645:fmbsr=2:i=32576_2911 on theBenchmark for (2911ds/32576Mi) % 130.42/18.66 % (1213701)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 130.42/18.66 % (1213701)Terminated due to inappropriate strategy. % 130.42/18.66 % (1213701)------------------------------ % 130.42/18.66 % (1213701)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 130.42/18.66 % (1213701)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 130.42/18.66 % (1213701)CaDiCaL version: 2.1.3 % 130.42/18.66 % (1213701)Termination reason: Inappropriate % 130.42/18.66 % (1213701)Time elapsed: 0.007 s % 130.42/18.66 % (1213701)Peak memory usage: 11 MB % 130.42/18.66 % (1213701)Instructions burned: 12 (million) % 130.42/18.66 % (1213701)------------------------------ % 130.42/18.66 % (1213701)------------------------------ % 130.42/18.66 % (1213703)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=774178618:i=11404_2911 on theBenchmark for (2911ds/11404Mi) % 130.42/18.66 % (1213697)Instruction limit reached! % 130.42/18.66 % (1213697)------------------------------ % 130.42/18.66 % (1213697)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 130.42/18.66 % (1213697)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 130.42/18.66 % (1213697)CaDiCaL version: 2.1.3 % 130.42/18.66 % (1213697)Termination reason: Instruction limit % 130.42/18.66 % (1213697)Termination phase: Saturation % 130.42/18.66 % (1213697)Time elapsed: 4.987 s % 130.42/18.66 % (1213697)Peak memory usage: 62 MB % 130.42/18.66 % (1213697)Instructions burned: 9156 (million) % 130.42/18.66 % (1213705)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=17342087:i=14134_2909 on theBenchmark for (2909ds/14134Mi) % 130.42/18.66 % (1213693)Instruction limit reached! % 130.42/18.66 % (1213693)------------------------------ % 130.42/18.66 % (1213693)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 130.42/18.66 % (1213693)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 130.42/18.66 % (1213693)CaDiCaL version: 2.1.3 % 130.42/18.66 % (1213693)Termination reason: Instruction limit % 130.42/18.66 % (1213693)Termination phase: Saturation % 130.42/18.66 % (1213693)Time elapsed: 7.796 s % 130.42/18.66 % (1213693)Peak memory usage: 220 MB % 130.42/18.66 % (1213693)Instructions burned: 22567 (million) % 130.42/18.66 % (1213707)dis+33_16_sil=32000:sac=on:random_seed=2241557075:i=15851:nm=0_2889 on theBenchmark for (2889ds/15851Mi) % 130.42/18.66 % (1213707)Instruction limit reached! % 130.42/18.66 % (1213707)------------------------------ % 130.42/18.66 % (1213707)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 160.97/22.91 % (1213707)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 160.97/22.91 % (1213707)CaDiCaL version: 2.1.3 % 160.97/22.91 % (1213707)Termination reason: Instruction limit % 160.97/22.91 % (1213707)Termination phase: Saturation % 160.97/22.91 % (1213707)Time elapsed: 4.848 s % 160.97/22.91 % (1213707)Peak memory usage: 134 MB % 160.97/22.91 % (1213707)Instructions burned: 15852 (million) % 160.97/22.91 % (1214068)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=4172282954:avsq=on:i=17627:add=on:amm=off_2840 on theBenchmark for (2840ds/17627Mi) % 160.97/22.91 % (1213703)Instruction limit reached! % 160.97/22.91 % (1213703)------------------------------ % 160.97/22.91 % (1213703)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 160.97/22.91 % (1213703)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 160.97/22.91 % (1213703)CaDiCaL version: 2.1.3 % 160.97/22.91 % (1213703)Termination reason: Instruction limit % 160.97/22.91 % (1213703)Termination phase: Saturation % 160.97/22.91 % (1213703)Time elapsed: 7.593 s % 160.97/22.91 % (1213703)Peak memory usage: 85 MB % 160.97/22.91 % (1213703)Instructions burned: 11406 (million) % 160.97/22.91 % (1214070)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=1543422393:s2a=on:i=53295_2835 on theBenchmark for (2835ds/53295Mi) % 160.97/22.91 % (1213576)Instruction limit reached! % 160.97/22.91 % (1213576)------------------------------ % 160.97/22.91 % (1213576)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 160.97/22.91 % (1213576)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 160.97/22.91 % (1213576)CaDiCaL version: 2.1.3 % 160.97/22.91 % (1213576)Termination reason: Instruction limit % 160.97/22.91 % (1213576)Termination phase: Saturation % 160.97/22.91 % (1213576)Time elapsed: 13.845 s % 160.97/22.91 % (1213576)Peak memory usage: 243 MB % 160.97/22.91 % (1213576)Instructions burned: 29340 (million) % 160.97/22.91 % (1214072)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=741929720:i=26857:ins=20_2833 on theBenchmark for (2833ds/26857Mi) % 160.97/22.91 % (1214072)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 160.97/22.91 % (1214072)Terminated due to inappropriate strategy. % 160.97/22.91 % (1214072)------------------------------ % 160.97/22.91 % (1214072)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 160.97/22.91 % (1214072)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 160.97/22.91 % (1214072)CaDiCaL version: 2.1.3 % 160.97/22.91 % (1214072)Termination reason: Inappropriate % 160.97/22.91 % (1214072)Time elapsed: 0.006 s % 160.97/22.91 % (1214072)Peak memory usage: 11 MB % 160.97/22.91 % (1214072)Instructions burned: 10 (million) % 160.97/22.91 % (1214072)------------------------------ % 160.97/22.91 % (1214072)------------------------------ % 160.97/22.91 % (1214074)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=498574840:i=28120:bs=on:fsr=off_2833 on theBenchmark for (2833ds/28120Mi) % 160.97/22.91 % (1213705)Instruction limit reached! % 160.97/22.91 % (1213705)------------------------------ % 160.97/22.91 % (1213705)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 160.97/22.91 % (1213705)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 160.97/22.91 % (1213705)CaDiCaL version: 2.1.3 % 160.97/22.91 % (1213705)Termination reason: Instruction limit % 160.97/22.91 % (1213705)Termination phase: Saturation % 160.97/22.91 % (1213705)Time elapsed: 9.182 s % 160.97/22.91 % (1213705)Peak memory usage: 102 MB % 160.97/22.91 % (1213705)Instructions burned: 14135 (million) % 160.97/22.91 % (1214076)fmb+10_1_sil=256000:fmbss=7:random_seed=2523770940:fmbsr=1.6:i=182295_2817 on theBenchmark for (2817ds/182295Mi) % 160.97/22.91 % (1214076)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 160.97/22.91 % (1214076)Terminated due to inappropriate strategy. % 160.97/22.91 % (1214076)------------------------------ % 160.97/22.91 % (1214076)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 160.97/22.91 % (1214076)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 160.97/22.91 % (1214076)CaDiCaL version: 2.1.3 % 160.97/22.91 % (1214076)Termination reason: Inappropriate % 160.97/22.91 % (1214076)Time elapsed: 0.006 s % 160.97/22.91 % (1214076)Peak memory usage: 11 MB % 160.97/22.91 % (1214076)Instructions burned: 10 (million) % 160.97/22.91 % (1214076)------------------------------ % 160.97/22.91 % (1214076)------------------------------ % 160.97/22.91 % (1214078)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=855373081:i=44625:gsp=on_2817 on theBenchmark for (2817ds/44625Mi) % 167.81/24.02 % (1214078)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 167.81/24.02 % (1214078)Terminated due to inappropriate strategy. % 167.81/24.02 % (1214078)------------------------------ % 167.81/24.02 % (1214078)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 167.81/24.02 % (1214078)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 167.81/24.02 % (1214078)CaDiCaL version: 2.1.3 % 167.81/24.02 % (1214078)Termination reason: Inappropriate % 167.81/24.02 % (1214078)Time elapsed: 0.006 s % 167.81/24.02 % (1214078)Peak memory usage: 11 MB % 167.81/24.02 % (1214078)Instructions burned: 11 (million) % 167.81/24.02 % (1214078)------------------------------ % 167.81/24.02 % (1214078)------------------------------ % 167.81/24.02 % (1214080)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=4069001573:i=160505_2816 on theBenchmark for (2816ds/160505Mi) % 167.81/24.02 % (1214080)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 167.81/24.02 % (1214080)Terminated due to inappropriate strategy. % 167.81/24.02 % (1214080)------------------------------ % 167.81/24.02 % (1214080)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 167.81/24.02 % (1214080)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 167.81/24.02 % (1214080)CaDiCaL version: 2.1.3 % 167.81/24.02 % (1214080)Termination reason: Inappropriate % 167.81/24.02 % (1214080)Time elapsed: 0.006 s % 167.81/24.02 % (1214080)Peak memory usage: 11 MB % 167.81/24.02 % (1214080)Instructions burned: 10 (million) % 167.81/24.02 % (1214080)------------------------------ % 167.81/24.02 % (1214080)------------------------------ % 167.81/24.02 % (1214082)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=1619260301:fmbsr=1.3:i=225729_2816 on theBenchmark for (2816ds/225729Mi) % 167.81/24.02 % (1214082)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 167.81/24.02 % (1214082)Terminated due to inappropriate strategy. % 167.81/24.02 % (1214082)------------------------------ % 167.81/24.02 % (1214082)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 167.81/24.02 % (1214082)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 167.81/24.02 % (1214082)CaDiCaL version: 2.1.3 % 167.81/24.02 % (1214082)Termination reason: Inappropriate % 167.81/24.02 % (1214082)Time elapsed: 0.006 s % 167.81/24.02 % (1214082)Peak memory usage: 11 MB % 167.81/24.02 % (1214082)Instructions burned: 11 (million) % 167.81/24.02 % (1214082)------------------------------ % 167.81/24.02 % (1214082)------------------------------ % 167.81/24.02 % (1214084)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=3074452260:fmbsr=2:i=185024:ins=7_2816 on theBenchmark for (2816ds/185024Mi) % 167.81/24.02 % (1214084)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 167.81/24.02 % (1214084)Terminated due to inappropriate strategy. % 167.81/24.02 % (1214084)------------------------------ % 167.81/24.02 % (1214084)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 167.81/24.02 % (1214084)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 167.81/24.02 % (1214084)CaDiCaL version: 2.1.3 % 167.81/24.02 % (1214084)Termination reason: Inappropriate % 167.81/24.02 % (1214084)Time elapsed: 0.006 s % 167.81/24.02 % (1214084)Peak memory usage: 11 MB % 167.81/24.02 % (1214084)Instructions burned: 11 (million) % 167.81/24.02 % (1214084)------------------------------ % 167.81/24.02 % (1214084)------------------------------ % 167.81/24.02 % (1214086)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=1903965485:rtra=on_2816 on theBenchmark for (2816ds/0Mi) % 167.81/24.02 % (1214086)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 167.81/24.02 % (1214086)Terminated due to inappropriate strategy. % 167.81/24.02 % (1214086)------------------------------ % 167.81/24.02 % (1214086)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 167.81/24.02 % (1214086)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 167.81/24.02 % (1214086)CaDiCaL version: 2.1.3 % 167.81/24.02 % (1214086)Termination reason: Inappropriate % 167.81/24.02 % (1214086)Time elapsed: 0.008 s % 167.81/24.02 % (1214086)Peak memory usage: 11 MB % 167.81/24.02 % (1214086)Instructions burned: 13 (million) % 167.81/24.02 % (1214086)------------------------------ % 167.81/24.02 % (1214086)------------------------------ % 167.81/24.02 % (1214088)% WARNING: option uhcvi not known. % 167.81/24.02 % (1214088)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=794451019:i=271062:add=off:rtra=on:rawr=on_2815 on theBenchmark for (2815ds/271062Mi) % 181.75/25.99 % (1213699)Instruction limit reached! % 181.75/25.99 % (1213699)------------------------------ % 181.75/25.99 % (1213699)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 181.75/25.99 % (1213699)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 181.75/25.99 % (1213699)CaDiCaL version: 2.1.3 % 181.75/25.99 % (1213699)Termination reason: Instruction limit % 181.75/25.99 % (1213699)Termination phase: Saturation % 181.75/25.99 % (1213699)Time elapsed: 13.621 s % 181.75/25.99 % (1213699)Peak memory usage: 89 MB % 181.75/25.99 % (1213699)Instructions burned: 20139 (million) % 181.75/25.99 % (1214090)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1288153971:i=176048:add=on:rtra=on:rawr=on_2807 on theBenchmark for (2807ds/176048Mi) % 181.75/25.99 % (1214068)Instruction limit reached! % 181.75/25.99 % (1214068)------------------------------ % 181.75/25.99 % (1214068)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 181.75/25.99 % (1214068)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 181.75/25.99 % (1214068)CaDiCaL version: 2.1.3 % 181.75/25.99 % (1214068)Termination reason: Instruction limit % 181.75/25.99 % (1214068)Termination phase: Saturation % 181.75/25.99 % (1214068)Time elapsed: 6.286 s % 181.75/25.99 % (1214068)Peak memory usage: 129 MB % 181.75/25.99 % (1214068)Instructions burned: 17627 (million) % 181.75/25.99 % (1214092)dis+10_1_sil=32000:si=on:sp=arity:random_seed=1965978612:i=206:fgj=on:rtra=on_2777 on theBenchmark for (2777ds/206Mi) % 181.75/25.99 % (1214092)Instruction limit reached! % 181.75/25.99 % (1214092)------------------------------ % 181.75/25.99 % (1214092)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 181.75/25.99 % (1214092)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 181.75/25.99 % (1214092)CaDiCaL version: 2.1.3 % 181.75/25.99 % (1214092)Termination reason: Instruction limit % 181.75/25.99 % (1214092)Termination phase: Saturation % 181.75/25.99 % (1214092)Time elapsed: 0.074 s % 181.75/25.99 % (1214092)Peak memory usage: 14 MB % 181.75/25.99 % (1214092)Instructions burned: 207 (million) % 181.75/25.99 % (1214094)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=2849555355:i=232:rtra=on_2776 on theBenchmark for (2776ds/232Mi) % 181.75/25.99 % (1214094)Instruction limit reached! % 181.75/25.99 % (1214094)------------------------------ % 181.75/25.99 % (1214094)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 181.75/25.99 % (1214094)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 181.75/25.99 % (1214094)CaDiCaL version: 2.1.3 % 181.75/25.99 % (1214094)Termination reason: Instruction limit % 181.75/25.99 % (1214094)Termination phase: Saturation % 181.75/25.99 % (1214094)Time elapsed: 0.083 s % 181.75/25.99 % (1214094)Peak memory usage: 14 MB % 181.75/25.99 % (1214094)Instructions burned: 234 (million) % 181.75/25.99 % (1214096)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=4053470600:i=262:rtra=on_2775 on theBenchmark for (2775ds/262Mi) % 181.75/25.99 % (1214096)Instruction limit reached! % 181.75/25.99 % (1214096)------------------------------ % 181.75/25.99 % (1214096)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 181.75/25.99 % (1214096)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 181.75/25.99 % (1214096)CaDiCaL version: 2.1.3 % 181.75/25.99 % (1214096)Termination reason: Instruction limit % 181.75/25.99 % (1214096)Termination phase: Saturation % 181.75/25.99 % (1214096)Time elapsed: 0.092 s % 181.75/25.99 % (1214096)Peak memory usage: 15 MB % 181.75/25.99 % (1214096)Instructions burned: 263 (million) % 181.75/25.99 % (1214098)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=3693508196:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2774 on theBenchmark for (2774ds/318Mi) % 181.75/25.99 % (1214098)Instruction limit reached! % 181.75/25.99 % (1214098)------------------------------ % 181.75/25.99 % (1214098)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 181.75/25.99 % (1214098)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 181.75/25.99 % (1214098)CaDiCaL version: 2.1.3 % 181.75/25.99 % (1214098)Termination reason: Instruction limit % 181.75/25.99 % (1214098)Termination phase: Saturation % 181.75/25.99 % (1214098)Time elapsed: 0.106 s % 181.75/25.99 % (1214098)Peak memory usage: 15 MB % 181.75/25.99 % (1214098)Instructions burned: 318 (million) % 181.75/25.99 % (1214100)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=2349959891:i=1428:nm=2:rtra=on_2773 on theBenchmark for (2773ds/1428Mi) % 212.33/30.19 % (1214100)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 212.33/30.19 % (1214100)Terminated due to inappropriate strategy. % 212.33/30.19 % (1214100)------------------------------ % 212.33/30.19 % (1214100)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 212.33/30.19 % (1214100)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 212.33/30.19 % (1214100)CaDiCaL version: 2.1.3 % 212.33/30.19 % (1214100)Termination reason: Inappropriate % 212.33/30.19 % (1214100)Time elapsed: 0.003 s % 212.33/30.19 % (1214100)Peak memory usage: 11 MB % 212.33/30.19 % (1214100)Instructions burned: 11 (million) % 212.33/30.19 % (1214100)------------------------------ % 212.33/30.19 % (1214100)------------------------------ % 212.33/30.19 % (1214102)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=4214500857:i=262:bd=preordered:rtra=on:fsd=on_2773 on theBenchmark for (2773ds/262Mi) % 212.33/30.19 % (1214102)Instruction limit reached! % 212.33/30.19 % (1214102)------------------------------ % 212.33/30.19 % (1214102)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 212.33/30.19 % (1214102)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 212.33/30.19 % (1214102)CaDiCaL version: 2.1.3 % 212.33/30.19 % (1214102)Termination reason: Instruction limit % 212.33/30.19 % (1214102)Termination phase: Saturation % 212.33/30.19 % (1214102)Time elapsed: 0.128 s % 212.33/30.19 % (1214102)Peak memory usage: 14 MB % 212.33/30.19 % (1214102)Instructions burned: 262 (million) % 212.33/30.19 % (1214104)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=855386011:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2771 on theBenchmark for (2771ds/1368Mi) % 212.33/30.19 % (1214104)Instruction limit reached! % 212.33/30.19 % (1214104)------------------------------ % 212.33/30.19 % (1214104)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 212.33/30.19 % (1214104)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 212.33/30.19 % (1214104)CaDiCaL version: 2.1.3 % 212.33/30.19 % (1214104)Termination reason: Instruction limit % 212.33/30.19 % (1214104)Termination phase: Saturation % 212.33/30.19 % (1214104)Time elapsed: 0.469 s % 212.33/30.19 % (1214104)Peak memory usage: 25 MB % 212.33/30.19 % (1214104)Instructions burned: 1368 (million) % 212.33/30.19 % (1214106)ott-21_1_sil=16000:si=on:fs=off:random_seed=2152586195:i=360:av=off:fsr=off:rtra=on_2766 on theBenchmark for (2766ds/360Mi) % 212.33/30.19 % (1214106)Instruction limit reached! % 212.33/30.19 % (1214106)------------------------------ % 212.33/30.19 % (1214106)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 212.33/30.19 % (1214106)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 212.33/30.19 % (1214106)CaDiCaL version: 2.1.3 % 212.33/30.19 % (1214106)Termination reason: Instruction limit % 212.33/30.19 % (1214106)Termination phase: Saturation % 212.33/30.19 % (1214106)Time elapsed: 0.103 s % 212.33/30.19 % (1214106)Peak memory usage: 14 MB % 212.33/30.19 % (1214106)Instructions burned: 362 (million) % 212.33/30.19 % (1214108)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1291143924:i=954:bd=all:rtra=on_2765 on theBenchmark for (2765ds/954Mi) % 212.33/30.19 % (1214108)Instruction limit reached! % 212.33/30.19 % (1214108)------------------------------ % 212.33/30.19 % (1214108)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 212.33/30.19 % (1214108)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 212.33/30.19 % (1214108)CaDiCaL version: 2.1.3 % 212.33/30.19 % (1214108)Termination reason: Instruction limit % 212.33/30.19 % (1214108)Termination phase: Saturation % 212.33/30.19 % (1214108)Time elapsed: 0.315 s % 212.33/30.19 % (1214108)Peak memory usage: 16 MB % 212.33/30.19 % (1214108)Instructions burned: 956 (million) % 212.33/30.19 % (1214110)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=3018633869:fmbsr=1.3:i=1730:ins=25:rtra=on_2762 on theBenchmark for (2762ds/1730Mi) % 212.33/30.19 % (1214110)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 212.33/30.19 % (1214110)Terminated due to inappropriate strategy. % 212.33/30.19 % (1214110)------------------------------ % 212.33/30.19 % (1214110)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 212.33/30.19 % (1214110)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 212.33/30.19 % (1214110)CaDiCaL version: 2.1.3 % 212.33/30.19 % (1214110)Termination reason: Inappropriate % 258.22/36.69 % (1214110)Time elapsed: 0.003 s % 258.22/36.69 % (1214110)Peak memory usage: 11 MB % 258.22/36.69 % (1214110)Instructions burned: 11 (million) % 258.22/36.69 % (1214110)------------------------------ % 258.22/36.69 % (1214110)------------------------------ % 258.22/36.69 % (1214112)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=4257812597:i=2358:rtra=on_2762 on theBenchmark for (2762ds/2358Mi) % 258.22/36.69 % (1214112)Instruction limit reached! % 258.22/36.69 % (1214112)------------------------------ % 258.22/36.69 % (1214112)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 258.22/36.69 % (1214112)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 258.22/36.69 % (1214112)CaDiCaL version: 2.1.3 % 258.22/36.69 % (1214112)Termination reason: Instruction limit % 258.22/36.69 % (1214112)Termination phase: Saturation % 258.22/36.69 % (1214112)Time elapsed: 0.864 s % 258.22/36.69 % (1214112)Peak memory usage: 32 MB % 258.22/36.69 % (1214112)Instructions burned: 2358 (million) % 258.22/36.69 % (1214114)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=1707471786:i=1778:ins=1:rtra=on_2753 on theBenchmark for (2753ds/1778Mi) % 258.22/36.69 % (1214114)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 258.22/36.69 % (1214114)Terminated due to inappropriate strategy. % 258.22/36.69 % (1214114)------------------------------ % 258.22/36.69 % (1214114)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 258.22/36.69 % (1214114)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 258.22/36.69 % (1214114)CaDiCaL version: 2.1.3 % 258.22/36.69 % (1214114)Termination reason: Inappropriate % 258.22/36.69 % (1214114)Time elapsed: 0.003 s % 258.22/36.69 % (1214114)Peak memory usage: 10 MB % 258.22/36.69 % (1214114)Instructions burned: 11 (million) % 258.22/36.69 % (1214114)------------------------------ % 258.22/36.69 % (1214114)------------------------------ % 258.22/36.69 % (1214116)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=3162619887:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2753 on theBenchmark for (2753ds/1384Mi) % 258.22/36.69 % (1214116)Instruction limit reached! % 258.22/36.69 % (1214116)------------------------------ % 258.22/36.69 % (1214116)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 258.22/36.69 % (1214116)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 258.22/36.69 % (1214116)CaDiCaL version: 2.1.3 % 258.22/36.69 % (1214116)Termination reason: Instruction limit % 258.22/36.69 % (1214116)Termination phase: Saturation % 258.22/36.69 % (1214116)Time elapsed: 0.478 s % 258.22/36.69 % (1214116)Peak memory usage: 24 MB % 258.22/36.69 % (1214116)Instructions burned: 1384 (million) % 258.22/36.69 % (1214118)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=195380103:i=1758:kws=inv_precedence:fsr=off:rtra=on_2748 on theBenchmark for (2748ds/1758Mi) % 258.22/36.69 % (1214118)Instruction limit reached! % 258.22/36.69 % (1214118)------------------------------ % 258.22/36.69 % (1214118)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 258.22/36.69 % (1214118)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 258.22/36.69 % (1214118)CaDiCaL version: 2.1.3 % 258.22/36.69 % (1214118)Termination reason: Instruction limit % 258.22/36.69 % (1214118)Termination phase: Saturation % 258.22/36.69 % (1214118)Time elapsed: 0.547 s % 258.22/36.69 % (1214118)Peak memory usage: 26 MB % 258.22/36.69 % (1214118)Instructions burned: 1760 (million) % 258.22/36.69 % (1214120)fmb+10_1_sil=64000:si=on:random_seed=1986523279:i=44122:nm=2:rtra=on:gsp=on_2742 on theBenchmark for (2742ds/44122Mi) % 258.22/36.69 % (1214120)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 258.22/36.69 % (1214120)Terminated due to inappropriate strategy. % 258.22/36.69 % (1214120)------------------------------ % 258.22/36.69 % (1214120)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 258.22/36.69 % (1214120)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 258.22/36.69 % (1214120)CaDiCaL version: 2.1.3 % 258.22/36.69 % (1214120)Termination reason: Inappropriate % 258.22/36.69 % (1214120)Time elapsed: 0.003 s % 258.22/36.69 % (1214120)Peak memory usage: 11 MB % 258.22/36.69 % (1214120)Instructions burned: 12 (million) % 258.22/36.69 % (1214120)------------------------------ % 258.22/36.69 % (1214120)------------------------------ % 258.22/36.69 % (1214122)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=2383302285:i=19030:nm=5:rtra=on_2742 on theBenchmark for (2742ds/19030Mi) % 290.43/41.14 % (1214122)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 290.43/41.14 % (1214122)Terminated due to inappropriate strategy. % 290.43/41.14 % (1214122)------------------------------ % 290.43/41.14 % (1214122)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 290.43/41.14 % (1214122)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 290.43/41.14 % (1214122)CaDiCaL version: 2.1.3 % 290.43/41.14 % (1214122)Termination reason: Inappropriate % 290.43/41.14 % (1214122)Time elapsed: 0.003 s % 290.43/41.14 % (1214122)Peak memory usage: 11 MB % 290.43/41.14 % (1214122)Instructions burned: 11 (million) % 290.43/41.14 % (1214122)------------------------------ % 290.43/41.14 % (1214122)------------------------------ % 290.43/41.14 % (1214124)fmb+10_1_sil=64000:sas=cadical:si=on:fmbss=8:random_seed=3485853341:fmbsr=1.7:i=1840:rtra=on_2742 on theBenchmark for (2742ds/1840Mi) % 290.43/41.14 % (1214124)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 290.43/41.14 % (1214124)Terminated due to inappropriate strategy. % 290.43/41.14 % (1214124)------------------------------ % 290.43/41.14 % (1214124)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 290.43/41.14 % (1214124)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 290.43/41.14 % (1214124)CaDiCaL version: 2.1.3 % 290.43/41.14 % (1214124)Termination reason: Inappropriate % 290.43/41.14 % (1214124)Time elapsed: 0.003 s % 290.43/41.14 % (1214124)Peak memory usage: 11 MB % 290.43/41.14 % (1214124)Instructions burned: 11 (million) % 290.43/41.14 % (1214124)------------------------------ % 290.43/41.14 % (1214124)------------------------------ % 290.43/41.14 % (1214126)dis-4_1_sil=16000:drc=ordering:si=on:sp=const_frequency:sac=on:newcnf=on:random_seed=3145910335:i=10262:rtra=on_2742 on theBenchmark for (2742ds/10262Mi) % 290.43/41.14 % (1214126)Instruction limit reached! % 290.43/41.14 % (1214126)------------------------------ % 290.43/41.14 % (1214126)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 290.43/41.14 % (1214126)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 290.43/41.14 % (1214126)CaDiCaL version: 2.1.3 % 290.43/41.14 % (1214126)Termination reason: Instruction limit % 290.43/41.14 % (1214126)Termination phase: Saturation % 290.43/41.14 % (1214126)Time elapsed: 3.269 s % 290.43/41.14 % (1214126)Peak memory usage: 57 MB % 290.43/41.14 % (1214126)Instructions burned: 10265 (million) % 290.43/41.14 % (1214325)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:si=on:sp=arity:spb=units:lsd=10:nwc=3:random_seed=182989777:i=2944:ins=7:rtra=on:fdi=8:gsp=on_2709 on theBenchmark for (2709ds/2944Mi) % 290.43/41.14 % (1214325)Instruction limit reached! % 290.43/41.14 % (1214325)------------------------------ % 290.43/41.14 % (1214325)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 290.43/41.14 % (1214325)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 290.43/41.14 % (1214325)CaDiCaL version: 2.1.3 % 290.43/41.14 % (1214325)Termination reason: Instruction limit % 290.43/41.14 % (1214325)Termination phase: Saturation % 290.43/41.14 % (1214325)Time elapsed: 0.850 s % 290.43/41.14 % (1214325)Peak memory usage: 52 MB % 290.43/41.14 % (1214325)Instructions burned: 2946 (million) % 290.43/41.14 % (1214489)fmb+10_1_sil=16000:sas=cadical:si=on:bce=on:fmbss=77:random_seed=1626368731:i=12648:rtra=on_2700 on theBenchmark for (2700ds/12648Mi) % 290.43/41.14 % (1214489)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 290.43/41.14 % (1214489)Terminated due to inappropriate strategy. % 290.43/41.14 % (1214489)------------------------------ % 290.43/41.14 % (1214489)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 290.43/41.14 % (1214489)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 290.43/41.14 % (1214489)CaDiCaL version: 2.1.3 % 290.43/41.14 % (1214489)Termination reason: Inappropriate % 290.43/41.14 % (1214489)Time elapsed: 0.004 s % 290.43/41.14 % (1214489)Peak memory usage: 11 MB % 290.43/41.14 % (1214489)Instructions burned: 12 (million) % 290.43/41.14 % (1214489)------------------------------ % 290.43/41.14 % (1214489)------------------------------ % 290.43/41.14 % (1214491)fmb+10_1_fmbas=function:sil=32000:sas=cadical:si=on:fmbss=16:random_seed=2182502143:fmbsr=2.30978:i=4348:rtra=on_2700 on theBenchmark for (2700ds/4348Mi) % 290.43/41.14 % (1214491)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 290.43/41.14 % (1214491)Terminated due to inappropriate strategy. % 290.43/41.14 % (1214491)---------------------------Terminated % 300.36/42.63 % Vampire exiting %------------------------------------------------------------------------------