%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWW045_1 : TPTP v9.3.1. Released v5.0.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % Computer : n019.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:38:40 PM UTC 2026 % Result : Timeout 300.62s 42.64s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : SWW045_1 : TPTP v9.3.1. Released v5.0.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.09/0.17 % Computer : n019.cluster.edu % 0.09/0.17 % Model : x86_64 x86_64 % 0.09/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.17 % Memory : 8046.5625MB % 0.09/0.17 % OS : Linux 6.8.0-71-generic % 0.09/0.17 % CPULimit : 300 % 0.09/0.17 % WCLimit : 300 % 0.09/0.17 % DateTime : Mon Sep 28 13:10:18 UTC 2026 % 0.09/0.17 % CPUTime : % 0.09/0.17 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.09/0.20 Running first-order model finding % 0.09/0.20 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.23/0.70 % (3992114)Will run a generic schedule for satisfiability detection. % 3.23/0.70 % (3992119)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1909366128_2999 on theBenchmark for (2999ds/0Mi) % 3.23/0.70 % (3992120)% WARNING: option uhcvi not known. % 3.23/0.70 % (3992120)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2152622906:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 3.23/0.70 % (3992121)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1456145211:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 3.23/0.70 % (3992122)dis+10_1_sil=32000:sp=arity:random_seed=591196237:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 3.23/0.70 % (3992124)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1398936445:i=131_2999 on theBenchmark for (2999ds/131Mi) % 3.23/0.70 % (3992123)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1497286737:i=116_2999 on theBenchmark for (2999ds/116Mi) % 3.23/0.70 % (3992125)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=958389922:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 3.23/0.70 % (3992119)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.23/0.70 % (3992119)Terminated due to inappropriate strategy. % 3.23/0.70 % (3992119)------------------------------ % 3.23/0.70 % (3992119)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.23/0.70 % (3992119)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.23/0.70 % (3992119)CaDiCaL version: 2.1.3 % 3.23/0.70 % (3992119)Termination reason: Inappropriate % 3.23/0.70 % (3992119)Time elapsed: 0.019 s % 3.23/0.70 % (3992119)Peak memory usage: 13 MB % 3.23/0.70 % (3992119)Instructions burned: 83 (million) % 3.23/0.70 % (3992119)------------------------------ % 3.23/0.70 % (3992119)------------------------------ % 3.23/0.70 % (3992133)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3525814175:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 3.23/0.70 % (3992133)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.23/0.70 % (3992133)Terminated due to inappropriate strategy. % 3.23/0.70 % (3992133)------------------------------ % 3.23/0.70 % (3992133)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.23/0.70 % (3992133)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.23/0.70 % (3992133)CaDiCaL version: 2.1.3 % 3.23/0.70 % (3992133)Termination reason: Inappropriate % 3.23/0.70 % (3992133)Time elapsed: 0.019 s % 3.23/0.70 % (3992133)Peak memory usage: 13 MB % 3.23/0.70 % (3992133)Instructions burned: 83 (million) % 3.23/0.70 % (3992133)------------------------------ % 3.23/0.70 % (3992133)------------------------------ % 3.23/0.70 % (3992122)Instruction limit reached! % 3.23/0.70 % (3992122)------------------------------ % 3.23/0.70 % (3992122)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.23/0.70 % (3992122)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.23/0.70 % (3992122)CaDiCaL version: 2.1.3 % 3.23/0.70 % (3992122)Termination reason: Instruction limit % 3.23/0.70 % (3992122)Termination phase: Saturation % 3.23/0.70 % (3992122)Time elapsed: 0.045 s % 3.23/0.70 % (3992122)Peak memory usage: 14 MB % 3.23/0.70 % (3992122)Instructions burned: 103 (million) % 3.23/0.70 % (3992123)Instruction limit reached! % 3.23/0.70 % (3992123)------------------------------ % 3.23/0.70 % (3992123)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.23/0.70 % (3992124)Instruction limit reached! % 3.23/0.70 % (3992124)------------------------------ % 3.23/0.70 % (3992124)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.23/0.70 % (3992124)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.23/0.70 % (3992124)CaDiCaL version: 2.1.3 % 3.23/0.70 % (3992124)Termination reason: Instruction limit % 3.23/0.70 % (3992124)Termination phase: Saturation % 3.23/0.70 % (3992124)Time elapsed: 0.053 s % 3.23/0.70 % (3992124)Peak memory usage: 14 MB % 3.23/0.70 % (3992124)Instructions burned: 131 (million) % 3.23/0.70 % (3992123)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.23/0.70 % (3992123)CaDiCaL version: 2.1.3 % 3.23/0.70 % (3992123)Termination reason: Instruction limit % 3.23/0.70 % (3992123)Termination phase: Saturation % 3.23/0.70 % (3992123)Time elapsed: 0.053 s % 3.23/0.70 % (3992123)Peak memory usage: 15 MB % 3.23/0.70 % (3992123)Instructions burned: 117 (million) % 4.18/0.99 % (3992135)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1241915772:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi) % 4.18/0.99 % (3992136)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=761620051:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi) % 4.18/0.99 % (3992125)Instruction limit reached! % 4.18/0.99 % (3992125)------------------------------ % 4.18/0.99 % (3992125)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 4.18/0.99 % (3992125)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.18/0.99 % (3992125)CaDiCaL version: 2.1.3 % 4.18/0.99 % (3992125)Termination reason: Instruction limit % 4.18/0.99 % (3992125)Termination phase: Saturation % 4.18/0.99 % (3992125)Time elapsed: 0.068 s % 4.18/0.99 % (3992125)Peak memory usage: 15 MB % 4.18/0.99 % (3992125)Instructions burned: 168 (million) % 4.18/0.99 % (3992137)ott-21_1_sil=16000:fs=off:random_seed=898932430:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 4.18/0.99 % (3992138)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3779833885:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 4.18/0.99 % (3992135)Instruction limit reached! % 4.18/0.99 % (3992135)------------------------------ % 4.18/0.99 % (3992135)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 4.18/0.99 % (3992135)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.18/0.99 % (3992135)CaDiCaL version: 2.1.3 % 4.18/0.99 % (3992135)Termination reason: Instruction limit % 4.18/0.99 % (3992135)Termination phase: Saturation % 4.18/0.99 % (3992135)Time elapsed: 0.029 s % 4.18/0.99 % (3992135)Peak memory usage: 15 MB % 4.18/0.99 % (3992135)Instructions burned: 132 (million) % 4.18/0.99 % (3992141)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3799998142:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 4.18/0.99 % (3992144)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1401604838:i=1179_2998 on theBenchmark for (2998ds/1179Mi) % 4.18/0.99 % (3992141)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 4.18/0.99 % (3992141)Terminated due to inappropriate strategy. % 4.18/0.99 % (3992141)------------------------------ % 4.18/0.99 % (3992141)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 4.18/0.99 % (3992141)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.18/0.99 % (3992141)CaDiCaL version: 2.1.3 % 4.18/0.99 % (3992141)Termination reason: Inappropriate % 4.18/0.99 % (3992141)Time elapsed: 0.036 s % 4.18/0.99 % (3992141)Peak memory usage: 13 MB % 4.18/0.99 % (3992141)Instructions burned: 82 (million) % 4.18/0.99 % (3992141)------------------------------ % 4.18/0.99 % (3992141)------------------------------ % 4.18/0.99 % (3992147)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1008517709:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi) % 4.18/0.99 % (3992137)Instruction limit reached! % 4.18/0.99 % (3992137)------------------------------ % 4.18/0.99 % (3992137)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 4.18/0.99 % (3992137)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.18/0.99 % (3992137)CaDiCaL version: 2.1.3 % 4.18/0.99 % (3992137)Termination reason: Instruction limit % 4.18/0.99 % (3992137)Termination phase: Saturation % 4.18/0.99 % (3992137)Time elapsed: 0.084 s % 4.18/0.99 % (3992137)Peak memory usage: 15 MB % 4.18/0.99 % (3992137)Instructions burned: 180 (million) % 4.18/0.99 % (3992149)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=3500846137: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) % 4.18/0.99 % (3992147)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 4.18/0.99 % (3992147)Terminated due to inappropriate strategy. % 4.18/0.99 % (3992147)------------------------------ % 4.18/0.99 % (3992147)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 4.18/0.99 % (3992147)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.18/0.99 % (3992147)CaDiCaL version: 2.1.3 % 4.18/0.99 % (3992147)Termination reason: Inappropriate % 4.18/0.99 % (3992147)Time elapsed: 0.050 s % 4.18/0.99 % (3992147)Peak memory usage: 15 MB % 16.92/2.74 % (3992147)Instructions burned: 114 (million) % 16.92/2.74 % (3992147)------------------------------ % 16.92/2.74 % (3992147)------------------------------ % 16.92/2.74 % (3992151)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1387763721:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi) % 16.92/2.74 % (3992138)Instruction limit reached! % 16.92/2.74 % (3992138)------------------------------ % 16.92/2.74 % (3992138)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 16.92/2.74 % (3992138)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.92/2.74 % (3992138)CaDiCaL version: 2.1.3 % 16.92/2.74 % (3992138)Termination reason: Instruction limit % 16.92/2.74 % (3992138)Termination phase: Saturation % 16.92/2.74 % (3992138)Time elapsed: 0.238 s % 16.92/2.74 % (3992138)Peak memory usage: 16 MB % 16.92/2.74 % (3992138)Instructions burned: 478 (million) % 16.92/2.74 % (3992153)fmb+10_1_sil=64000:random_seed=3827384416:i=22061:nm=2:gsp=on_2996 on theBenchmark for (2996ds/22061Mi) % 16.92/2.74 % (3992153)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 16.92/2.74 % (3992153)Terminated due to inappropriate strategy. % 16.92/2.74 % (3992153)------------------------------ % 16.92/2.74 % (3992153)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 16.92/2.74 % (3992153)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.92/2.74 % (3992153)CaDiCaL version: 2.1.3 % 16.92/2.74 % (3992153)Termination reason: Inappropriate % 16.92/2.74 % (3992153)Time elapsed: 0.040 s % 16.92/2.74 % (3992153)Peak memory usage: 13 MB % 16.92/2.74 % (3992153)Instructions burned: 91 (million) % 16.92/2.74 % (3992153)------------------------------ % 16.92/2.74 % (3992153)------------------------------ % 16.92/2.74 % (3992144)Instruction limit reached! % 16.92/2.74 % (3992144)------------------------------ % 16.92/2.74 % (3992144)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 16.92/2.74 % (3992144)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.92/2.74 % (3992144)CaDiCaL version: 2.1.3 % 16.92/2.74 % (3992144)Termination reason: Instruction limit % 16.92/2.74 % (3992144)Termination phase: Saturation % 16.92/2.74 % (3992144)Time elapsed: 0.286 s % 16.92/2.74 % (3992144)Peak memory usage: 19 MB % 16.92/2.74 % (3992144)Instructions burned: 1181 (million) % 16.92/2.74 % (3992156)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1868486590:fmbsr=1.7:i=920_2995 on theBenchmark for (2995ds/920Mi) % 16.92/2.74 % (3992155)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=16004665:i=9515:nm=5_2995 on theBenchmark for (2995ds/9515Mi) % 16.92/2.74 % (3992136)Instruction limit reached! % 16.92/2.74 % (3992136)------------------------------ % 16.92/2.74 % (3992136)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 16.92/2.74 % (3992136)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.92/2.74 % (3992136)CaDiCaL version: 2.1.3 % 16.92/2.74 % (3992136)Termination reason: Instruction limit % 16.92/2.74 % (3992136)Termination phase: Saturation % 16.92/2.74 % (3992136)Time elapsed: 0.334 s % 16.92/2.74 % (3992136)Peak memory usage: 20 MB % 16.92/2.74 % (3992136)Instructions burned: 686 (million) % 16.92/2.74 % (3992156)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 16.92/2.74 % (3992156)Terminated due to inappropriate strategy. % 16.92/2.74 % (3992156)------------------------------ % 16.92/2.74 % (3992156)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 16.92/2.74 % (3992156)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.92/2.74 % (3992156)CaDiCaL version: 2.1.3 % 16.92/2.74 % (3992156)Termination reason: Inappropriate % 16.92/2.74 % (3992156)Time elapsed: 0.019 s % 16.92/2.74 % (3992156)Peak memory usage: 13 MB % 16.92/2.74 % (3992156)Instructions burned: 83 (million) % 16.92/2.74 % (3992156)------------------------------ % 16.92/2.74 % (3992156)------------------------------ % 16.92/2.74 % (3992159)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1811791754:i=5131_2995 on theBenchmark for (2995ds/5131Mi) % 16.92/2.74 % (3992155)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 16.92/2.74 % (3992155)Terminated due to inappropriate strategy. % 16.92/2.74 % (3992155)------------------------------ % 16.92/2.74 % (3992155)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 16.92/2.74 % (3992155)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.44/3.80 % (3992155)CaDiCaL version: 2.1.3 % 24.44/3.80 % (3992155)Termination reason: Inappropriate % 24.44/3.80 % (3992155)Time elapsed: 0.036 s % 24.44/3.80 % (3992155)Peak memory usage: 13 MB % 24.44/3.80 % (3992155)Instructions burned: 83 (million) % 24.44/3.80 % (3992160)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1821512099:i=1472:ins=7:fdi=8:gsp=on_2995 on theBenchmark for (2995ds/1472Mi) % 24.44/3.80 % (3992155)------------------------------ % 24.44/3.80 % (3992155)------------------------------ % 24.44/3.80 % (3992163)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3580879549:i=6324_2995 on theBenchmark for (2995ds/6324Mi) % 24.44/3.80 % (3992163)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 24.44/3.80 % (3992163)Terminated due to inappropriate strategy. % 24.44/3.80 % (3992163)------------------------------ % 24.44/3.80 % (3992163)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 24.44/3.80 % (3992163)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.44/3.80 % (3992163)CaDiCaL version: 2.1.3 % 24.44/3.80 % (3992163)Termination reason: Inappropriate % 24.44/3.80 % (3992163)Time elapsed: 0.036 s % 24.44/3.80 % (3992163)Peak memory usage: 13 MB % 24.44/3.80 % (3992163)Instructions burned: 83 (million) % 24.44/3.80 % (3992163)------------------------------ % 24.44/3.80 % (3992163)------------------------------ % 24.44/3.80 % (3992165)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=390527108:fmbsr=2.30978:i=2174_2994 on theBenchmark for (2994ds/2174Mi) % 24.44/3.80 % (3992165)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 24.44/3.80 % (3992165)Terminated due to inappropriate strategy. % 24.44/3.80 % (3992165)------------------------------ % 24.44/3.80 % (3992165)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 24.44/3.80 % (3992165)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.44/3.80 % (3992165)CaDiCaL version: 2.1.3 % 24.44/3.80 % (3992165)Termination reason: Inappropriate % 24.44/3.80 % (3992165)Time elapsed: 0.036 s % 24.44/3.80 % (3992165)Peak memory usage: 13 MB % 24.44/3.80 % (3992165)Instructions burned: 83 (million) % 24.44/3.80 % (3992165)------------------------------ % 24.44/3.80 % (3992165)------------------------------ % 24.44/3.80 % (3992167)ott-2_1_sil=16000:newcnf=on:random_seed=1600253563:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2993 on theBenchmark for (2993ds/869Mi) % 24.44/3.80 % (3992149)Instruction limit reached! % 24.44/3.80 % (3992149)------------------------------ % 24.44/3.80 % (3992149)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 24.44/3.80 % (3992149)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.44/3.80 % (3992149)CaDiCaL version: 2.1.3 % 24.44/3.80 % (3992149)Termination reason: Instruction limit % 24.44/3.80 % (3992149)Termination phase: Saturation % 24.44/3.80 % (3992149)Time elapsed: 0.413 s % 24.44/3.80 % (3992149)Peak memory usage: 22 MB % 24.44/3.80 % (3992149)Instructions burned: 692 (million) % 24.44/3.80 % (3992169)ott+10_1_sil=32000:tgt=ground:random_seed=933032713:i=5114:av=off_2993 on theBenchmark for (2993ds/5114Mi) % 24.44/3.80 % (3992151)Instruction limit reached! % 24.44/3.80 % (3992151)------------------------------ % 24.44/3.80 % (3992151)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 24.44/3.80 % (3992151)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.44/3.80 % (3992151)CaDiCaL version: 2.1.3 % 24.44/3.80 % (3992151)Termination reason: Instruction limit % 24.44/3.80 % (3992151)Termination phase: Saturation % 24.44/3.80 % (3992151)Time elapsed: 0.474 s % 24.44/3.80 % (3992151)Peak memory usage: 21 MB % 24.44/3.80 % (3992151)Instructions burned: 880 (million) % 24.44/3.80 % (3992160)Instruction limit reached! % 24.44/3.80 % (3992160)------------------------------ % 24.44/3.80 % (3992160)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 24.44/3.80 % (3992160)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.44/3.80 % (3992160)CaDiCaL version: 2.1.3 % 24.44/3.80 % (3992160)Termination reason: Instruction limit % 24.44/3.80 % (3992160)Termination phase: Saturation % 24.44/3.80 % (3992160)Time elapsed: 0.272 s % 24.44/3.80 % (3992160)Peak memory usage: 17 MB % 24.44/3.80 % (3992160)Instructions burned: 1478 (million) % 24.44/3.80 % (3992172)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=4222559519:i=3512:aac=none_2992 on theBenchmark for (2992ds/3512Mi) % 24.44/3.80 % (3992171)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=435720579:i=54282_2992 on theBenchmark for (2992ds/54282Mi) % 99.79/14.32 % (3992171)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 99.79/14.32 % (3992171)Terminated due to inappropriate strategy. % 99.79/14.32 % (3992171)------------------------------ % 99.79/14.32 % (3992171)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 99.79/14.32 % (3992171)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 99.79/14.32 % (3992171)CaDiCaL version: 2.1.3 % 99.79/14.32 % (3992171)Termination reason: Inappropriate % 99.79/14.32 % (3992171)Time elapsed: 0.035 s % 99.79/14.32 % (3992171)Peak memory usage: 13 MB % 99.79/14.32 % (3992171)Instructions burned: 83 (million) % 99.79/14.32 % (3992171)------------------------------ % 99.79/14.32 % (3992171)------------------------------ % 99.79/14.32 % (3992175)dis+21_1_sil=32000:sas=cadical:random_seed=4168785080:i=3773:amm=off_2991 on theBenchmark for (2991ds/3773Mi) % 99.79/14.32 % (3992167)Instruction limit reached! % 99.79/14.32 % (3992167)------------------------------ % 99.79/14.32 % (3992167)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 99.79/14.32 % (3992167)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 99.79/14.32 % (3992167)CaDiCaL version: 2.1.3 % 99.79/14.32 % (3992167)Termination reason: Instruction limit % 99.79/14.32 % (3992167)Termination phase: Saturation % 99.79/14.32 % (3992167)Time elapsed: 0.410 s % 99.79/14.32 % (3992167)Peak memory usage: 19 MB % 99.79/14.32 % (3992167)Instructions burned: 870 (million) % 99.79/14.32 % (3992177)ott+11_1_sil=16000:gs=on:random_seed=1043763000:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2989 on theBenchmark for (2989ds/2251Mi) % 99.79/14.32 % (3992172)Instruction limit reached! % 99.79/14.32 % (3992172)------------------------------ % 99.79/14.32 % (3992172)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 99.79/14.32 % (3992172)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 99.79/14.32 % (3992172)CaDiCaL version: 2.1.3 % 99.79/14.32 % (3992172)Termination reason: Instruction limit % 99.79/14.32 % (3992172)Termination phase: Saturation % 99.79/14.32 % (3992172)Time elapsed: 0.948 s % 99.79/14.32 % (3992172)Peak memory usage: 31 MB % 99.79/14.32 % (3992172)Instructions burned: 3514 (million) % 99.79/14.32 % (3992179)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=2878091782:fmbsr=1.6:i=67534_2982 on theBenchmark for (2982ds/67534Mi) % 99.79/14.32 % (3992179)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 99.79/14.32 % (3992179)Terminated due to inappropriate strategy. % 99.79/14.32 % (3992179)------------------------------ % 99.79/14.32 % (3992179)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 99.79/14.32 % (3992179)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 99.79/14.32 % (3992179)CaDiCaL version: 2.1.3 % 99.79/14.32 % (3992179)Termination reason: Inappropriate % 99.79/14.32 % (3992179)Time elapsed: 0.025 s % 99.79/14.32 % (3992179)Peak memory usage: 14 MB % 99.79/14.32 % (3992179)Instructions burned: 112 (million) % 99.79/14.32 % (3992179)------------------------------ % 99.79/14.32 % (3992179)------------------------------ % 99.79/14.32 % (3992181)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=260259148:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2982 on theBenchmark for (2982ds/4591Mi) % 99.79/14.32 % (3992177)Instruction limit reached! % 99.79/14.32 % (3992177)------------------------------ % 99.79/14.32 % (3992177)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 99.79/14.32 % (3992177)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 99.79/14.32 % (3992177)CaDiCaL version: 2.1.3 % 99.79/14.32 % (3992177)Termination reason: Instruction limit % 99.79/14.32 % (3992177)Termination phase: Saturation % 99.79/14.32 % (3992177)Time elapsed: 0.904 s % 99.79/14.32 % (3992177)Peak memory usage: 20 MB % 99.79/14.32 % (3992177)Instructions burned: 2253 (million) % 99.79/14.32 % (3992183)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=193871383:i=29340_2980 on theBenchmark for (2980ds/29340Mi) % 99.79/14.32 % (3992175)Instruction limit reached! % 99.79/14.32 % (3992175)------------------------------ % 99.79/14.32 % (3992175)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 99.79/14.32 % (3992175)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 99.79/14.32 % (3992175)CaDiCaL version: 2.1.3 % 99.79/14.32 % (3992175)Termination reason: Instruction limit % 112.11/16.10 % (3992175)Termination phase: Saturation % 112.11/16.10 % (3992175)Time elapsed: 1.694 s % 112.11/16.10 % (3992175)Peak memory usage: 25 MB % 112.11/16.10 % (3992175)Instructions burned: 3775 (million) % 112.11/16.10 % (3992185)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=3907994896:i=5211_2974 on theBenchmark for (2974ds/5211Mi) % 112.11/16.10 % (3992181)Instruction limit reached! % 112.11/16.10 % (3992181)------------------------------ % 112.11/16.10 % (3992181)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 112.11/16.10 % (3992181)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 112.11/16.10 % (3992181)CaDiCaL version: 2.1.3 % 112.11/16.10 % (3992181)Termination reason: Instruction limit % 112.11/16.10 % (3992181)Termination phase: Saturation % 112.11/16.10 % (3992181)Time elapsed: 1.259 s % 112.11/16.10 % (3992181)Peak memory usage: 40 MB % 112.11/16.10 % (3992181)Instructions burned: 4593 (million) % 112.11/16.10 % (3992187)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=360058175:i=5497:nm=2_2969 on theBenchmark for (2969ds/5497Mi) % 112.11/16.10 % (3992187)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 112.11/16.10 % (3992187)Terminated due to inappropriate strategy. % 112.11/16.10 % (3992187)------------------------------ % 112.11/16.10 % (3992187)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 112.11/16.10 % (3992187)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 112.11/16.10 % (3992187)CaDiCaL version: 2.1.3 % 112.11/16.10 % (3992187)Termination reason: Inappropriate % 112.11/16.10 % (3992187)Time elapsed: 0.020 s % 112.11/16.10 % (3992187)Peak memory usage: 13 MB % 112.11/16.10 % (3992187)Instructions burned: 83 (million) % 112.11/16.10 % (3992187)------------------------------ % 112.11/16.10 % (3992187)------------------------------ % 112.11/16.10 % (3992189)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=3651502697:fmbsr=2:i=46332_2969 on theBenchmark for (2969ds/46332Mi) % 112.11/16.10 % (3992189)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 112.11/16.10 % (3992189)Terminated due to inappropriate strategy. % 112.11/16.10 % (3992189)------------------------------ % 112.11/16.10 % (3992189)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 112.11/16.10 % (3992189)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 112.11/16.10 % (3992189)CaDiCaL version: 2.1.3 % 112.11/16.10 % (3992189)Termination reason: Inappropriate % 112.11/16.10 % (3992189)Time elapsed: 0.026 s % 112.11/16.10 % (3992189)Peak memory usage: 14 MB % 112.11/16.10 % (3992189)Instructions burned: 116 (million) % 112.11/16.10 % (3992189)------------------------------ % 112.11/16.10 % (3992189)------------------------------ % 112.11/16.10 % (3992191)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=508681647:i=14071_2968 on theBenchmark for (2968ds/14071Mi) % 112.11/16.10 % (3992191)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 112.11/16.10 % (3992191)Terminated due to inappropriate strategy. % 112.11/16.10 % (3992191)------------------------------ % 112.11/16.10 % (3992191)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 112.11/16.10 % (3992191)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 112.11/16.10 % (3992191)CaDiCaL version: 2.1.3 % 112.11/16.10 % (3992191)Termination reason: Inappropriate % 112.11/16.10 % (3992191)Time elapsed: 0.048 s % 112.11/16.11 % (3992191)Peak memory usage: 14 MB % 112.11/16.11 % (3992191)Instructions burned: 116 (million) % 112.11/16.11 % (3992191)------------------------------ % 112.11/16.11 % (3992191)------------------------------ % 112.11/16.11 % (3992159)Instruction limit reached! % 112.11/16.11 % (3992159)------------------------------ % 112.11/16.11 % (3992159)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 112.11/16.11 % (3992159)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 112.11/16.11 % (3992159)CaDiCaL version: 2.1.3 % 112.11/16.11 % (3992159)Termination reason: Instruction limit % 112.11/16.11 % (3992159)Termination phase: Saturation % 112.11/16.11 % (3992159)Time elapsed: 2.694 s % 112.11/16.11 % (3992159)Peak memory usage: 43 MB % 112.11/16.11 % (3992159)Instructions burned: 5131 (million) % 112.11/16.11 % (3992193)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3012923387:i=22565:add=on:rawr=on_2968 on theBenchmark for (2968ds/22565Mi) % 112.11/16.11 % (3992194)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=200418276:i=8173:av=off_2968 on theBenchmark for (2968ds/8173Mi) % 114.67/16.43 % (3992169)Instruction limit reached! % 114.67/16.43 % (3992169)------------------------------ % 114.67/16.43 % (3992169)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 114.67/16.43 % (3992169)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 114.67/16.43 % (3992169)CaDiCaL version: 2.1.3 % 114.67/16.43 % (3992169)Termination reason: Instruction limit % 114.67/16.43 % (3992169)Termination phase: Saturation % 114.67/16.43 % (3992169)Time elapsed: 2.916 s % 114.67/16.43 % (3992169)Peak memory usage: 32 MB % 114.67/16.43 % (3992169)Instructions burned: 5114 (million) % 114.67/16.43 % (3992197)dis+10_16:1_sil=16000:random_seed=3332327434:i=9155:fsr=off_2964 on theBenchmark for (2964ds/9155Mi) % 114.67/16.43 % (3992185)Instruction limit reached! % 114.67/16.43 % (3992185)------------------------------ % 114.67/16.43 % (3992185)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 114.67/16.43 % (3992185)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 114.67/16.43 % (3992185)CaDiCaL version: 2.1.3 % 114.67/16.43 % (3992185)Termination reason: Instruction limit % 114.67/16.43 % (3992185)Termination phase: Saturation % 114.67/16.43 % (3992185)Time elapsed: 2.739 s % 114.67/16.43 % (3992185)Peak memory usage: 47 MB % 114.67/16.43 % (3992185)Instructions burned: 5211 (million) % 114.67/16.43 % (3992199)ott-3_8_sil=64000:random_seed=2528946898:i=20139:bs=on_2947 on theBenchmark for (2947ds/20139Mi) % 114.67/16.43 % (3992194)Instruction limit reached! % 114.67/16.43 % (3992194)------------------------------ % 114.67/16.43 % (3992194)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 114.67/16.43 % (3992194)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 114.67/16.43 % (3992194)CaDiCaL version: 2.1.3 % 114.67/16.43 % (3992194)Termination reason: Instruction limit % 114.67/16.43 % (3992194)Termination phase: Saturation % 114.67/16.43 % (3992194)Time elapsed: 3.478 s % 114.67/16.43 % (3992194)Peak memory usage: 34 MB % 114.67/16.43 % (3992194)Instructions burned: 8174 (million) % 114.67/16.43 % (3992201)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=2098723823:fmbsr=2:i=32576_2933 on theBenchmark for (2933ds/32576Mi) % 114.67/16.43 % (3992201)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 114.67/16.43 % (3992201)Terminated due to inappropriate strategy. % 114.67/16.43 % (3992201)------------------------------ % 114.67/16.43 % (3992201)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 114.67/16.43 % (3992201)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 114.67/16.43 % (3992201)CaDiCaL version: 2.1.3 % 114.67/16.43 % (3992201)Termination reason: Inappropriate % 114.67/16.43 % (3992201)Time elapsed: 0.046 s % 114.67/16.43 % (3992201)Peak memory usage: 14 MB % 114.67/16.43 % (3992201)Instructions burned: 112 (million) % 114.67/16.43 % (3992201)------------------------------ % 114.67/16.43 % (3992201)------------------------------ % 114.67/16.43 % (3992203)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=735829087:i=11404_2932 on theBenchmark for (2932ds/11404Mi) % 114.67/16.43 % (3992197)Instruction limit reached! % 114.67/16.43 % (3992197)------------------------------ % 114.67/16.43 % (3992197)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 114.67/16.43 % (3992197)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 114.67/16.43 % (3992197)CaDiCaL version: 2.1.3 % 114.67/16.43 % (3992197)Termination reason: Instruction limit % 114.67/16.43 % (3992197)Termination phase: Saturation % 114.67/16.43 % (3992197)Time elapsed: 4.663 s % 114.67/16.43 % (3992197)Peak memory usage: 55 MB % 114.67/16.43 % (3992197)Instructions burned: 9156 (million) % 114.67/16.43 % (3992205)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=2943474387:i=14134_2917 on theBenchmark for (2917ds/14134Mi) % 114.67/16.43 % (3992193)Instruction limit reached! % 114.67/16.43 % (3992193)------------------------------ % 114.67/16.43 % (3992193)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 114.67/16.43 % (3992193)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 114.67/16.43 % (3992193)CaDiCaL version: 2.1.3 % 114.67/16.43 % (3992193)Termination reason: Instruction limit % 114.67/16.43 % (3992193)Termination phase: Saturation % 114.67/16.43 % (3992193)Time elapsed: 7.491 s % 114.67/16.43 % (3992193)Peak memory usage: 121 MB % 114.67/16.43 % (3992193)Instructions burned: 22567 (million) % 114.67/16.43 % (3992207)dis+33_16_sil=32000:sac=on:random_seed=1379226746:i=15851:nm=0_2893 on theBenchmark for (2893ds/15851Mi) % 114.67/16.43 % (3992203)Instruction limit reached! % 114.67/16.43 % (3992203)------------------------------ % 114.67/16.43 % (3992203)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 167.20/23.80 % (3992203)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 167.20/23.80 % (3992203)CaDiCaL version: 2.1.3 % 167.20/23.80 % (3992203)Termination reason: Instruction limit % 167.20/23.80 % (3992203)Termination phase: Saturation % 167.20/23.80 % (3992203)Time elapsed: 7.343 s % 167.20/23.80 % (3992203)Peak memory usage: 48 MB % 167.20/23.80 % (3992203)Instructions burned: 11404 (million) % 167.20/23.80 % (3992214)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=1889155118:avsq=on:i=17627:add=on:amm=off_2858 on theBenchmark for (2858ds/17627Mi) % 167.20/23.80 % (3992207)Instruction limit reached! % 167.20/23.80 % (3992207)------------------------------ % 167.20/23.80 % (3992207)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 167.20/23.80 % (3992207)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 167.20/23.80 % (3992207)CaDiCaL version: 2.1.3 % 167.20/23.80 % (3992207)Termination reason: Instruction limit % 167.20/23.80 % (3992207)Termination phase: Saturation % 167.20/23.80 % (3992207)Time elapsed: 3.592 s % 167.20/23.80 % (3992207)Peak memory usage: 33 MB % 167.20/23.80 % (3992207)Instructions burned: 15855 (million) % 167.20/23.80 % (3992289)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=2874145327:s2a=on:i=53295_2857 on theBenchmark for (2857ds/53295Mi) % 167.20/23.80 % (3992183)Instruction limit reached! % 167.20/23.80 % (3992183)------------------------------ % 167.20/23.80 % (3992183)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 167.20/23.80 % (3992183)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 167.20/23.80 % (3992183)CaDiCaL version: 2.1.3 % 167.20/23.80 % (3992183)Termination reason: Instruction limit % 167.20/23.80 % (3992183)Termination phase: Saturation % 167.20/23.80 % (3992183)Time elapsed: 13.675 s % 167.20/23.80 % (3992183)Peak memory usage: 43 MB % 167.20/23.80 % (3992183)Instructions burned: 29341 (million) % 167.20/23.80 % (3992365)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=2479244305:i=26857:ins=20_2843 on theBenchmark for (2843ds/26857Mi) % 167.20/23.80 % (3992365)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 167.20/23.80 % (3992365)Terminated due to inappropriate strategy. % 167.20/23.80 % (3992365)------------------------------ % 167.20/23.80 % (3992365)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 167.20/23.80 % (3992365)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 167.20/23.80 % (3992365)CaDiCaL version: 2.1.3 % 167.20/23.80 % (3992365)Termination reason: Inappropriate % 167.20/23.80 % (3992365)Time elapsed: 0.036 s % 167.20/23.80 % (3992365)Peak memory usage: 13 MB % 167.20/23.80 % (3992365)Instructions burned: 83 (million) % 167.20/23.80 % (3992365)------------------------------ % 167.20/23.80 % (3992365)------------------------------ % 167.20/23.80 % (3992367)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=253045552:i=28120:bs=on:fsr=off_2842 on theBenchmark for (2842ds/28120Mi) % 167.20/23.80 % (3992199)Instruction limit reached! % 167.20/23.80 % (3992199)------------------------------ % 167.20/23.80 % (3992199)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 167.20/23.80 % (3992199)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 167.20/23.80 % (3992199)CaDiCaL version: 2.1.3 % 167.20/23.80 % (3992199)Termination reason: Instruction limit % 167.20/23.80 % (3992199)Termination phase: Saturation % 167.20/23.80 % (3992199)Time elapsed: 10.502 s % 167.20/23.80 % (3992199)Peak memory usage: 55 MB % 167.20/23.80 % (3992199)Instructions burned: 20140 (million) % 167.20/23.80 % (3992369)fmb+10_1_sil=256000:fmbss=7:random_seed=3092147561:fmbsr=1.6:i=182295_2841 on theBenchmark for (2841ds/182295Mi) % 167.20/23.80 % (3992369)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 167.20/23.80 % (3992369)Terminated due to inappropriate strategy. % 167.20/23.80 % (3992369)------------------------------ % 167.20/23.80 % (3992369)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 167.20/23.80 % (3992369)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 167.20/23.80 % (3992369)CaDiCaL version: 2.1.3 % 167.20/23.80 % (3992369)Termination reason: Inappropriate % 167.20/23.80 % (3992369)Time elapsed: 0.035 s % 167.20/23.80 % (3992369)Peak memory usage: 13 MB % 167.20/23.80 % (3992369)Instructions burned: 83 (million) % 167.20/23.80 % (3992369)------------------------------ % 167.20/23.80 % (3992369)------------------------------ % 167.20/23.80 % (3992371)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=663450460:i=44625:gsp=on_2841 on theBenchmark for (2841ds/44625Mi) % 179.26/25.54 % (3992371)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 179.26/25.54 % (3992371)Terminated due to inappropriate strategy. % 179.26/25.54 % (3992371)------------------------------ % 179.26/25.54 % (3992371)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 179.26/25.54 % (3992371)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 179.26/25.54 % (3992371)CaDiCaL version: 2.1.3 % 179.26/25.54 % (3992371)Termination reason: Inappropriate % 179.26/25.54 % (3992371)Time elapsed: 0.040 s % 179.26/25.54 % (3992371)Peak memory usage: 14 MB % 179.26/25.54 % (3992371)Instructions burned: 88 (million) % 179.26/25.54 % (3992371)------------------------------ % 179.26/25.54 % (3992371)------------------------------ % 179.26/25.54 % (3992373)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=2434962962:i=160505_2840 on theBenchmark for (2840ds/160505Mi) % 179.26/25.54 % (3992373)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 179.26/25.54 % (3992373)Terminated due to inappropriate strategy. % 179.26/25.54 % (3992373)------------------------------ % 179.26/25.54 % (3992373)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 179.26/25.54 % (3992373)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 179.26/25.54 % (3992373)CaDiCaL version: 2.1.3 % 179.26/25.54 % (3992373)Termination reason: Inappropriate % 179.26/25.54 % (3992373)Time elapsed: 0.035 s % 179.26/25.54 % (3992373)Peak memory usage: 13 MB % 179.26/25.54 % (3992373)Instructions burned: 83 (million) % 179.26/25.54 % (3992373)------------------------------ % 179.26/25.54 % (3992373)------------------------------ % 179.26/25.54 % (3992375)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=1462207493:fmbsr=1.3:i=225729_2840 on theBenchmark for (2840ds/225729Mi) % 179.26/25.54 % (3992375)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 179.26/25.54 % (3992375)Terminated due to inappropriate strategy. % 179.26/25.54 % (3992375)------------------------------ % 179.26/25.54 % (3992375)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 179.26/25.54 % (3992375)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 179.26/25.54 % (3992375)CaDiCaL version: 2.1.3 % 179.26/25.54 % (3992375)Termination reason: Inappropriate % 179.26/25.54 % (3992375)Time elapsed: 0.048 s % 179.26/25.54 % (3992375)Peak memory usage: 14 MB % 179.26/25.54 % (3992375)Instructions burned: 116 (million) % 179.26/25.54 % (3992375)------------------------------ % 179.26/25.54 % (3992375)------------------------------ % 179.26/25.54 % (3992377)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=1330123204:fmbsr=2:i=185024:ins=7_2839 on theBenchmark for (2839ds/185024Mi) % 179.26/25.54 % (3992377)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 179.26/25.54 % (3992377)Terminated due to inappropriate strategy. % 179.26/25.54 % (3992377)------------------------------ % 179.26/25.54 % (3992377)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 179.26/25.54 % (3992377)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 179.26/25.54 % (3992377)CaDiCaL version: 2.1.3 % 179.26/25.54 % (3992377)Termination reason: Inappropriate % 179.26/25.54 % (3992377)Time elapsed: 0.048 s % 179.26/25.54 % (3992377)Peak memory usage: 14 MB % 179.26/25.54 % (3992377)Instructions burned: 116 (million) % 179.26/25.54 % (3992377)------------------------------ % 179.26/25.54 % (3992377)------------------------------ % 179.26/25.54 % (3992379)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=2483705947:rtra=on_2838 on theBenchmark for (2838ds/0Mi) % 179.26/25.54 % (3992379)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 179.26/25.54 % (3992379)Terminated due to inappropriate strategy. % 179.26/25.54 % (3992379)------------------------------ % 179.26/25.54 % (3992379)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 179.26/25.54 % (3992379)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 179.26/25.54 % (3992379)CaDiCaL version: 2.1.3 % 179.26/25.54 % (3992379)Termination reason: Inappropriate % 179.26/25.54 % (3992379)Time elapsed: 0.046 s % 179.26/25.54 % (3992379)Peak memory usage: 15 MB % 179.26/25.54 % (3992379)Instructions burned: 97 (million) % 179.26/25.54 % (3992379)------------------------------ % 179.26/25.54 % (3992379)------------------------------ % 179.26/25.54 % (3992381)% WARNING: option uhcvi not known. % 179.26/25.54 % (3992381)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3742255567:i=271062:add=off:rtra=on:rawr=on_2838 on theBenchmark for (2838ds/271062Mi) % 191.93/27.31 % (3992205)Instruction limit reached! % 191.93/27.31 % (3992205)------------------------------ % 191.93/27.31 % (3992205)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 191.93/27.31 % (3992205)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 191.93/27.31 % (3992205)CaDiCaL version: 2.1.3 % 191.93/27.31 % (3992205)Termination reason: Instruction limit % 191.93/27.31 % (3992205)Termination phase: Saturation % 191.93/27.31 % (3992205)Time elapsed: 8.821 s % 191.93/27.31 % (3992205)Peak memory usage: 53 MB % 191.93/27.31 % (3992205)Instructions burned: 14136 (million) % 191.93/27.31 % (3992383)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=715470986:i=176048:add=on:rtra=on:rawr=on_2828 on theBenchmark for (2828ds/176048Mi) % 191.93/27.31 % (3992214)Instruction limit reached! % 191.93/27.31 % (3992214)------------------------------ % 191.93/27.31 % (3992214)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 191.93/27.31 % (3992214)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 191.93/27.31 % (3992214)CaDiCaL version: 2.1.3 % 191.93/27.31 % (3992214)Termination reason: Instruction limit % 191.93/27.31 % (3992214)Termination phase: Saturation % 191.93/27.31 % (3992214)Time elapsed: 8.848 s % 191.93/27.31 % (3992214)Peak memory usage: 100 MB % 191.93/27.31 % (3992214)Instructions burned: 17628 (million) % 191.93/27.31 % (3992386)dis+10_1_sil=32000:si=on:sp=arity:random_seed=2182736390:i=206:fgj=on:rtra=on_2770 on theBenchmark for (2770ds/206Mi) % 191.93/27.31 % (3992386)Instruction limit reached! % 191.93/27.31 % (3992386)------------------------------ % 191.93/27.31 % (3992386)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 191.93/27.31 % (3992386)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 191.93/27.31 % (3992386)CaDiCaL version: 2.1.3 % 191.93/27.31 % (3992386)Termination reason: Instruction limit % 191.93/27.31 % (3992386)Termination phase: Saturation % 191.93/27.31 % (3992386)Time elapsed: 0.105 s % 191.93/27.31 % (3992386)Peak memory usage: 17 MB % 191.93/27.31 % (3992386)Instructions burned: 208 (million) % 191.93/27.31 % (3992388)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=4054337753:i=232:rtra=on_2768 on theBenchmark for (2768ds/232Mi) % 191.93/27.31 % (3992388)Instruction limit reached! % 191.93/27.31 % (3992388)------------------------------ % 191.93/27.31 % (3992388)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 191.93/27.31 % (3992388)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 191.93/27.31 % (3992388)CaDiCaL version: 2.1.3 % 191.93/27.31 % (3992388)Termination reason: Instruction limit % 191.93/27.31 % (3992388)Termination phase: Saturation % 191.93/27.31 % (3992388)Time elapsed: 0.105 s % 191.93/27.31 % (3992388)Peak memory usage: 16 MB % 191.93/27.31 % (3992388)Instructions burned: 232 (million) % 191.93/27.31 % (3992390)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=3464180515:i=262:rtra=on_2767 on theBenchmark for (2767ds/262Mi) % 191.93/27.31 % (3992390)Instruction limit reached! % 191.93/27.31 % (3992390)------------------------------ % 191.93/27.31 % (3992390)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 191.93/27.31 % (3992390)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 191.93/27.31 % (3992390)CaDiCaL version: 2.1.3 % 191.93/27.31 % (3992390)Termination reason: Instruction limit % 191.93/27.31 % (3992390)Termination phase: Saturation % 191.93/27.31 % (3992390)Time elapsed: 0.122 s % 191.93/27.31 % (3992390)Peak memory usage: 17 MB % 191.93/27.31 % (3992390)Instructions burned: 265 (million) % 191.93/27.31 % (3992392)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=3127501845:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2766 on theBenchmark for (2766ds/318Mi) % 191.93/27.31 % (3992392)Instruction limit reached! % 191.93/27.31 % (3992392)------------------------------ % 191.93/27.31 % (3992392)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 191.93/27.31 % (3992392)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 191.93/27.31 % (3992392)CaDiCaL version: 2.1.3 % 191.93/27.31 % (3992392)Termination reason: Instruction limit % 191.93/27.31 % (3992392)Termination phase: Saturation % 191.93/27.31 % (3992392)Time elapsed: 0.161 s % 191.93/27.31 % (3992392)Peak memory usage: 18 MB % 191.93/27.31 % (3992392)Instructions burned: 318 (million) % 191.93/27.31 % (3992394)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=1799401144:i=1428:nm=2:rtra=on_2764 on theBenchmark for (2764ds/1428Mi) % 199.16/28.35 % (3992394)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 199.16/28.35 % (3992394)Terminated due to inappropriate strategy. % 199.16/28.35 % (3992394)------------------------------ % 199.16/28.35 % (3992394)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 199.16/28.35 % (3992394)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 199.16/28.35 % (3992394)CaDiCaL version: 2.1.3 % 199.16/28.35 % (3992394)Termination reason: Inappropriate % 199.16/28.35 % (3992394)Time elapsed: 0.046 s % 199.16/28.35 % (3992394)Peak memory usage: 15 MB % 199.16/28.35 % (3992394)Instructions burned: 97 (million) % 199.16/28.35 % (3992394)------------------------------ % 199.16/28.35 % (3992394)------------------------------ % 199.16/28.35 % (3992396)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=664849863:i=262:bd=preordered:rtra=on:fsd=on_2763 on theBenchmark for (2763ds/262Mi) % 199.16/28.35 % (3992396)Instruction limit reached! % 199.16/28.35 % (3992396)------------------------------ % 199.16/28.35 % (3992396)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 199.16/28.35 % (3992396)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 199.16/28.35 % (3992396)CaDiCaL version: 2.1.3 % 199.16/28.35 % (3992396)Termination reason: Instruction limit % 199.16/28.35 % (3992396)Termination phase: Saturation % 199.16/28.35 % (3992396)Time elapsed: 0.121 s % 199.16/28.35 % (3992396)Peak memory usage: 17 MB % 199.16/28.35 % (3992396)Instructions burned: 262 (million) % 199.16/28.35 % (3992398)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=1746507300:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2762 on theBenchmark for (2762ds/1368Mi) % 199.16/28.35 % (3992398)Instruction limit reached! % 199.16/28.35 % (3992398)------------------------------ % 199.16/28.35 % (3992398)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 199.16/28.35 % (3992398)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 199.16/28.35 % (3992398)CaDiCaL version: 2.1.3 % 199.16/28.35 % (3992398)Termination reason: Instruction limit % 199.16/28.35 % (3992398)Termination phase: Saturation % 199.16/28.35 % (3992398)Time elapsed: 0.705 s % 199.16/28.35 % (3992398)Peak memory usage: 22 MB % 199.16/28.35 % (3992398)Instructions burned: 1369 (million) % 199.16/28.35 % (3992400)ott-21_1_sil=16000:si=on:fs=off:random_seed=3901535993:i=360:av=off:fsr=off:rtra=on_2754 on theBenchmark for (2754ds/360Mi) % 199.16/28.35 % (3992400)Instruction limit reached! % 199.16/28.35 % (3992400)------------------------------ % 199.16/28.35 % (3992400)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 199.16/28.35 % (3992400)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 199.16/28.35 % (3992400)CaDiCaL version: 2.1.3 % 199.16/28.35 % (3992400)Termination reason: Instruction limit % 199.16/28.35 % (3992400)Termination phase: Saturation % 199.16/28.35 % (3992400)Time elapsed: 0.177 s % 199.16/28.35 % (3992400)Peak memory usage: 17 MB % 199.16/28.35 % (3992400)Instructions burned: 362 (million) % 199.16/28.35 % (3992402)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2369416046:i=954:bd=all:rtra=on_2752 on theBenchmark for (2752ds/954Mi) % 199.16/28.35 % (3992402)Instruction limit reached! % 199.16/28.35 % (3992402)------------------------------ % 199.16/28.35 % (3992402)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 199.16/28.35 % (3992402)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 199.16/28.35 % (3992402)CaDiCaL version: 2.1.3 % 199.16/28.35 % (3992402)Termination reason: Instruction limit % 199.16/28.35 % (3992402)Termination phase: Saturation % 199.16/28.35 % (3992402)Time elapsed: 0.532 s % 199.16/28.35 % (3992402)Peak memory usage: 20 MB % 199.16/28.35 % (3992402)Instructions burned: 954 (million) % 199.16/28.35 % (3992404)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=2612746061:fmbsr=1.3:i=1730:ins=25:rtra=on_2747 on theBenchmark for (2747ds/1730Mi) % 199.16/28.35 % (3992404)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 199.16/28.35 % (3992404)Terminated due to inappropriate strategy. % 199.16/28.35 % (3992404)------------------------------ % 199.16/28.35 % (3992404)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 199.16/28.35 % (3992404)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 199.16/28.35 % (3992404)CaDiCaL version: 2.1.3 % 199.16/28.35 % (3992404)Termination reason: Inappropriate % 231.08/32.84 % (3992404)Time elapsed: 0.045 s % 231.08/32.84 % (3992404)Peak memory usage: 15 MB % 231.08/32.84 % (3992404)Instructions burned: 96 (million) % 231.08/32.84 % (3992404)------------------------------ % 231.08/32.84 % (3992404)------------------------------ % 231.08/32.84 % (3992406)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=1472793595:i=2358:rtra=on_2746 on theBenchmark for (2746ds/2358Mi) % 231.08/32.84 % (3992406)Instruction limit reached! % 231.08/32.84 % (3992406)------------------------------ % 231.08/32.84 % (3992406)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 231.08/32.84 % (3992406)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 231.08/32.84 % (3992406)CaDiCaL version: 2.1.3 % 231.08/32.84 % (3992406)Termination reason: Instruction limit % 231.08/32.84 % (3992406)Termination phase: Saturation % 231.08/32.84 % (3992406)Time elapsed: 1.315 s % 231.08/32.84 % (3992406)Peak memory usage: 26 MB % 231.08/32.84 % (3992406)Instructions burned: 2359 (million) % 231.08/32.84 % (3992408)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=3152231058:i=1778:ins=1:rtra=on_2733 on theBenchmark for (2733ds/1778Mi) % 231.08/32.84 % (3992408)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 231.08/32.84 % (3992408)Terminated due to inappropriate strategy. % 231.08/32.84 % (3992408)------------------------------ % 231.08/32.84 % (3992408)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 231.08/32.84 % (3992408)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 231.08/32.84 % (3992408)CaDiCaL version: 2.1.3 % 231.08/32.84 % (3992408)Termination reason: Inappropriate % 231.08/32.84 % (3992408)Time elapsed: 0.061 s % 231.08/32.84 % (3992408)Peak memory usage: 16 MB % 231.08/32.84 % (3992408)Instructions burned: 129 (million) % 231.08/32.84 % (3992408)------------------------------ % 231.08/32.84 % (3992408)------------------------------ % 231.08/32.84 % (3992410)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=1915742404:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2732 on theBenchmark for (2732ds/1384Mi) % 231.08/32.84 % (3992367)Instruction limit reached! % 231.08/32.84 % (3992367)------------------------------ % 231.08/32.84 % (3992367)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 231.08/32.84 % (3992367)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 231.08/32.84 % (3992367)CaDiCaL version: 2.1.3 % 231.08/32.84 % (3992367)Termination reason: Instruction limit % 231.08/32.84 % (3992367)Termination phase: Saturation % 231.08/32.84 % (3992367)Time elapsed: 11.256 s % 231.08/32.84 % (3992367)Peak memory usage: 28 MB % 231.08/32.84 % (3992367)Instructions burned: 28120 (million) % 231.08/32.84 % (3992412)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=2766378248:i=1758:kws=inv_precedence:fsr=off:rtra=on_2730 on theBenchmark for (2730ds/1758Mi) % 231.08/32.84 % (3992289)Instruction limit reached! % 231.08/32.84 % (3992289)------------------------------ % 231.08/32.84 % (3992289)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 231.08/32.84 % (3992289)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 231.08/32.84 % (3992289)CaDiCaL version: 2.1.3 % 231.08/32.84 % (3992289)Termination reason: Instruction limit % 231.08/32.84 % (3992289)Termination phase: Saturation % 231.08/32.84 % (3992289)Time elapsed: 12.732 s % 231.08/32.84 % (3992289)Peak memory usage: 147 MB % 231.08/32.84 % (3992289)Instructions burned: 53299 (million) % 231.08/32.84 % (3992414)fmb+10_1_sil=64000:si=on:random_seed=4019092550:i=44122:nm=2:rtra=on:gsp=on_2729 on theBenchmark for (2729ds/44122Mi) % 231.08/32.84 % (3992414)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 231.08/32.84 % (3992414)Terminated due to inappropriate strategy. % 231.08/32.84 % (3992414)------------------------------ % 231.08/32.84 % (3992414)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 231.08/32.84 % (3992414)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 231.08/32.84 % (3992414)CaDiCaL version: 2.1.3 % 231.08/32.84 % (3992414)Termination reason: Inappropriate % 231.08/32.84 % (3992414)Time elapsed: 0.027 s % 231.08/32.84 % (3992414)Peak memory usage: 15 MB % 231.08/32.84 % (3992414)Instructions burned: 105 (million) % 231.08/32.84 % (3992414)------------------------------ % 231.08/32.84 % (3992414)------------------------------ % 231.08/32.84 % (3992416)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=892809692:i=19030:nm=5:rtra=on_2729 on theBenchmark for (2729ds/19030Mi) % 251.83/36.86 % (3992416)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 251.83/36.86 % (3992416)Terminated due to inappropriate strategy. % 251.83/36.86 % (3992416)------------------------------ % 251.83/36.86 % (3992416)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 251.83/36.86 % (3992416)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 251.83/36.86 % (3992416)CaDiCaL version: 2.1.3 % 251.83/36.86 % (3992416)Termination reason: Inappropriate % 251.83/36.86 % (3992416)Time elapsed: 0.024 s % 251.83/36.86 % (3992416)Peak memory usage: 15 MB % 251.83/36.86 % (3992416)Instructions burned: 97 (million) % 251.83/36.86 % (3992416)------------------------------ % 251.83/36.86 % (3992416)------------------------------ % 251.83/36.86 % (3992418)fmb+10_1_sil=64000:sas=cadical:si=on:fmbss=8:random_seed=2469185787:fmbsr=1.7:i=1840:rtra=on_2728 on theBenchmark for (2728ds/1840Mi) % 251.83/36.86 % (3992418)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 251.83/36.86 % (3992418)Terminated due to inappropriate strategy. % 251.83/36.86 % (3992418)------------------------------ % 251.83/36.87 % (3992418)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 251.83/36.87 % (3992418)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 251.83/36.87 % (3992418)CaDiCaL version: 2.1.3 % 251.83/36.87 % (3992418)Termination reason: Inappropriate % 251.83/36.87 % (3992418)Time elapsed: 0.024 s % 251.83/36.87 % (3992418)Peak memory usage: 15 MB % 251.83/36.87 % (3992418)Instructions burned: 97 (million) % 251.83/36.87 % (3992418)------------------------------ % 251.83/36.87 % (3992418)------------------------------ % 251.83/36.87 % (3992420)dis-4_1_sil=16000:drc=ordering:si=on:sp=const_frequency:sac=on:newcnf=on:random_seed=1682508343:i=10262:rtra=on_2728 on theBenchmark for (2728ds/10262Mi) % 251.83/36.87 % (3992410)Instruction limit reached! % 251.83/36.87 % (3992410)------------------------------ % 251.83/36.87 % (3992410)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 251.83/36.87 % (3992410)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 251.83/36.87 % (3992410)CaDiCaL version: 2.1.3 % 251.83/36.87 % (3992410)Termination reason: Instruction limit % 251.83/36.87 % (3992410)Termination phase: Saturation % 251.83/36.87 % (3992410)Time elapsed: 0.682 s % 251.83/36.87 % (3992410)Peak memory usage: 21 MB % 251.83/36.87 % (3992410)Instructions burned: 1384 (million) % 251.83/36.87 % (3992422)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:si=on:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1906688233:i=2944:ins=7:rtra=on:fdi=8:gsp=on_2725 on theBenchmark for (2725ds/2944Mi) % 251.83/36.87 % (3992412)Instruction limit reached! % 251.83/36.87 % (3992412)------------------------------ % 251.83/36.87 % (3992412)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 251.83/36.87 % (3992412)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 251.83/36.87 % (3992412)CaDiCaL version: 2.1.3 % 251.83/36.87 % (3992412)Termination reason: Instruction limit % 251.83/36.87 % (3992412)Termination phase: Saturation % 251.83/36.87 % (3992412)Time elapsed: 0.985 s % 251.83/36.87 % (3992412)Peak memory usage: 27 MB % 251.83/36.87 % (3992412)Instructions burned: 1759 (million) % 251.83/36.87 % (3992424)fmb+10_1_sil=16000:sas=cadical:si=on:bce=on:fmbss=77:random_seed=1507186970:i=12648:rtra=on_2719 on theBenchmark for (2719ds/12648Mi) % 251.83/36.87 % (3992424)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 251.83/36.87 % (3992424)Terminated due to inappropriate strategy. % 251.83/36.87 % (3992424)------------------------------ % 251.83/36.87 % (3992424)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 251.83/36.87 % (3992424)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 251.83/36.87 % (3992424)CaDiCaL version: 2.1.3 % 251.83/36.87 % (3992424)Termination reason: Inappropriate % 251.83/36.87 % (3992424)Time elapsed: 0.046 s % 251.83/36.87 % (3992424)Peak memory usage: 15 MB % 251.83/36.87 % (3992424)Instructions burned: 97 (million) % 251.83/36.87 % (3992424)------------------------------ % 251.83/36.87 % (3992424)------------------------------ % 251.83/36.87 % (3992426)fmb+10_1_fmbas=function:sil=32000:sas=cadical:si=on:fmbss=16:random_seed=1577576393:fmbsr=2.30978:i=4348:rtra=on_2719 on theBenchmark for (2719ds/4348Mi) % 251.83/36.87 % (3992426)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 251.83/36.87 % (3992426)Terminated due to inappropriate strategy. % 251.83/36.87 % (3992426)------------Terminated % 300.62/42.64 % Vampire exiting %------------------------------------------------------------------------------