%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWW669_2 : TPTP v9.3.1. Released v6.1.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % Computer : n007.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:37 PM UTC 2026 % Result : Timeout 290.98s 41.29s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWW669_2 : TPTP v9.3.1. Released v6.1.0. % 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.10/0.23 % Computer : n007.cluster.edu % 0.10/0.23 % Model : x86_64 x86_64 % 0.10/0.23 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.23 % Memory : 8046.5625MB % 0.10/0.23 % OS : Linux 6.8.0-71-generic % 0.10/0.23 % CPULimit : 300 % 0.10/0.23 % WCLimit : 300 % 0.10/0.23 % DateTime : Mon Sep 28 14:22:26 UTC 2026 % 0.10/0.23 % CPUTime : % 0.10/0.23 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.26/0.28 Running first-order model finding % 0.26/0.28 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 5.97/1.19 % (2418576)Will run a generic schedule for satisfiability detection. % 5.97/1.19 % (2418582)% WARNING: option uhcvi not known. % 5.97/1.19 % (2418586)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2521411910:i=131_2999 on theBenchmark for (2999ds/131Mi) % 5.97/1.19 % (2418582)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=583295436:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 5.97/1.19 % (2418581)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2436147303_2999 on theBenchmark for (2999ds/0Mi) % 5.97/1.19 % (2418584)dis+10_1_sil=32000:sp=arity:random_seed=3323063596:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 5.97/1.19 % (2418585)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3548523671:i=116_2999 on theBenchmark for (2999ds/116Mi) % 5.97/1.19 % (2418583)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=199341336:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 5.97/1.19 % (2418587)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1946528373:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 5.97/1.19 % (2418581)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 5.97/1.19 % (2418581)Terminated due to inappropriate strategy. % 5.97/1.19 % (2418581)------------------------------ % 5.97/1.19 % (2418581)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.97/1.19 % (2418581)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.97/1.19 % (2418581)CaDiCaL version: 2.1.3 % 5.97/1.19 % (2418581)Termination reason: Inappropriate % 5.97/1.19 % (2418581)Time elapsed: 0.013 s % 5.97/1.19 % (2418581)Peak memory usage: 11 MB % 5.97/1.19 % (2418581)Instructions burned: 15 (million) % 5.97/1.19 % (2418581)------------------------------ % 5.97/1.19 % (2418581)------------------------------ % 5.97/1.19 % (2418597)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3950346319:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 5.97/1.19 % (2418586)Instruction limit reached! % 5.97/1.19 % (2418586)------------------------------ % 5.97/1.19 % (2418586)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.97/1.19 % (2418586)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.97/1.19 % (2418586)CaDiCaL version: 2.1.3 % 5.97/1.19 % (2418586)Termination reason: Instruction limit % 5.97/1.19 % (2418586)Termination phase: Saturation % 5.97/1.19 % (2418586)Time elapsed: 0.074 s % 5.97/1.19 % (2418586)Peak memory usage: 13 MB % 5.97/1.19 % (2418586)Instructions burned: 131 (million) % 5.97/1.19 % (2418597)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 5.97/1.19 % (2418597)Terminated due to inappropriate strategy. % 5.97/1.19 % (2418597)------------------------------ % 5.97/1.19 % (2418597)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.97/1.19 % (2418597)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.97/1.19 % (2418597)CaDiCaL version: 2.1.3 % 5.97/1.19 % (2418597)Termination reason: Inappropriate % 5.97/1.19 % (2418597)Time elapsed: 0.012 s % 5.97/1.19 % (2418597)Peak memory usage: 10 MB % 5.97/1.19 % (2418597)Instructions burned: 10 (million) % 5.97/1.19 % (2418597)------------------------------ % 5.97/1.19 % (2418597)------------------------------ % 5.97/1.19 % (2418600)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3784430514:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 5.97/1.19 % (2418601)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=3524920141:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi) % 5.97/1.19 % (2418585)Instruction limit reached! % 5.97/1.19 % (2418585)------------------------------ % 5.97/1.19 % (2418585)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.97/1.19 % (2418585)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.97/1.19 % (2418585)CaDiCaL version: 2.1.3 % 5.97/1.19 % (2418585)Termination reason: Instruction limit % 5.97/1.19 % (2418585)Termination phase: Saturation % 5.97/1.19 % (2418585)Time elapsed: 0.108 s % 5.97/1.19 % (2418585)Peak memory usage: 12 MB % 5.97/1.19 % (2418585)Instructions burned: 116 (million) % 5.97/1.19 % (2418584)Instruction limit reached! % 5.97/1.19 % (2418584)------------------------------ % 5.97/1.19 % (2418584)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.78/1.55 % (2418584)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.78/1.55 % (2418584)CaDiCaL version: 2.1.3 % 7.78/1.55 % (2418584)Termination reason: Instruction limit % 7.78/1.55 % (2418584)Termination phase: Saturation % 7.78/1.55 % (2418584)Time elapsed: 0.108 s % 7.78/1.55 % (2418584)Peak memory usage: 12 MB % 7.78/1.55 % (2418584)Instructions burned: 103 (million) % 7.78/1.55 % (2418605)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2157644798:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 7.78/1.55 % (2418604)ott-21_1_sil=16000:fs=off:random_seed=3387145881:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 7.78/1.55 % (2418600)Instruction limit reached! % 7.78/1.55 % (2418600)------------------------------ % 7.78/1.55 % (2418600)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.78/1.55 % (2418600)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.78/1.55 % (2418600)CaDiCaL version: 2.1.3 % 7.78/1.55 % (2418600)Termination reason: Instruction limit % 7.78/1.55 % (2418600)Termination phase: Saturation % 7.78/1.55 % (2418600)Time elapsed: 0.077 s % 7.78/1.55 % (2418600)Peak memory usage: 14 MB % 7.78/1.55 % (2418600)Instructions burned: 131 (million) % 7.78/1.55 % (2418609)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1453947138:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 7.78/1.55 % (2418609)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 7.78/1.55 % (2418609)Terminated due to inappropriate strategy. % 7.78/1.55 % (2418609)------------------------------ % 7.78/1.55 % (2418609)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.78/1.55 % (2418609)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.78/1.55 % (2418609)CaDiCaL version: 2.1.3 % 7.78/1.55 % (2418609)Termination reason: Inappropriate % 7.78/1.55 % (2418609)Time elapsed: 0.006 s % 7.78/1.55 % (2418609)Peak memory usage: 10 MB % 7.78/1.55 % (2418609)Instructions burned: 11 (million) % 7.78/1.55 % (2418587)Instruction limit reached! % 7.78/1.55 % (2418587)------------------------------ % 7.78/1.55 % (2418587)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.78/1.55 % (2418587)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.78/1.55 % (2418587)CaDiCaL version: 2.1.3 % 7.78/1.55 % (2418587)Termination reason: Instruction limit % 7.78/1.55 % (2418587)Termination phase: Saturation % 7.78/1.55 % (2418587)Time elapsed: 0.175 s % 7.78/1.55 % (2418587)Peak memory usage: 13 MB % 7.78/1.55 % (2418587)Instructions burned: 159 (million) % 7.78/1.55 % (2418609)------------------------------ % 7.78/1.55 % (2418609)------------------------------ % 7.78/1.55 % (2418611)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=704582671:i=1179_2997 on theBenchmark for (2997ds/1179Mi) % 7.78/1.55 % (2418612)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2531056035:i=889:ins=1_2997 on theBenchmark for (2997ds/889Mi) % 7.78/1.55 % (2418612)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 7.78/1.55 % (2418612)Terminated due to inappropriate strategy. % 7.78/1.55 % (2418612)------------------------------ % 7.78/1.55 % (2418612)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.78/1.55 % (2418612)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.78/1.55 % (2418612)CaDiCaL version: 2.1.3 % 7.78/1.55 % (2418612)Termination reason: Inappropriate % 7.78/1.55 % (2418612)Time elapsed: 0.011 s % 7.78/1.55 % (2418612)Peak memory usage: 10 MB % 7.78/1.55 % (2418612)Instructions burned: 11 (million) % 7.78/1.55 % (2418612)------------------------------ % 7.78/1.55 % (2418612)------------------------------ % 7.78/1.55 % (2418616)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=1867344349: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) % 7.78/1.55 % (2418604)Instruction limit reached! % 7.78/1.55 % (2418604)------------------------------ % 7.78/1.55 % (2418604)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.78/1.55 % (2418604)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.78/1.55 % (2418604)CaDiCaL version: 2.1.3 % 7.78/1.55 % (2418604)Termination reason: Instruction limit % 7.78/1.55 % (2418604)Termination phase: Saturation % 31.77/4.86 % (2418604)Time elapsed: 0.160 s % 31.77/4.86 % (2418604)Peak memory usage: 13 MB % 31.77/4.86 % (2418604)Instructions burned: 180 (million) % 31.77/4.86 % (2418618)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2079923603:i=879:kws=inv_precedence:fsr=off_2996 on theBenchmark for (2996ds/879Mi) % 31.77/4.86 % (2418605)Instruction limit reached! % 31.77/4.86 % (2418605)------------------------------ % 31.77/4.86 % (2418605)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 31.77/4.86 % (2418605)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.77/4.86 % (2418605)CaDiCaL version: 2.1.3 % 31.77/4.86 % (2418605)Termination reason: Instruction limit % 31.77/4.86 % (2418605)Termination phase: Saturation % 31.77/4.86 % (2418605)Time elapsed: 0.427 s % 31.77/4.86 % (2418605)Peak memory usage: 14 MB % 31.77/4.86 % (2418605)Instructions burned: 477 (million) % 31.77/4.86 % (2418624)fmb+10_1_sil=64000:random_seed=1544940408:i=22061:nm=2:gsp=on_2994 on theBenchmark for (2994ds/22061Mi) % 31.77/4.86 % (2418624)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 31.77/4.86 % (2418624)Terminated due to inappropriate strategy. % 31.77/4.86 % (2418624)------------------------------ % 31.77/4.86 % (2418624)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 31.77/4.86 % (2418624)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.77/4.86 % (2418624)CaDiCaL version: 2.1.3 % 31.77/4.86 % (2418624)Termination reason: Inappropriate % 31.77/4.86 % (2418624)Time elapsed: 0.008 s % 31.77/4.86 % (2418624)Peak memory usage: 10 MB % 31.77/4.86 % (2418624)Instructions burned: 11 (million) % 31.77/4.86 % (2418624)------------------------------ % 31.77/4.86 % (2418624)------------------------------ % 31.77/4.86 % (2418626)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1748654389:i=9515:nm=5_2993 on theBenchmark for (2993ds/9515Mi) % 31.77/4.86 % (2418626)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 31.77/4.86 % (2418626)Terminated due to inappropriate strategy. % 31.77/4.86 % (2418626)------------------------------ % 31.77/4.86 % (2418626)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 31.77/4.86 % (2418626)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.77/4.86 % (2418626)CaDiCaL version: 2.1.3 % 31.77/4.86 % (2418626)Termination reason: Inappropriate % 31.77/4.86 % (2418626)Time elapsed: 0.007 s % 31.77/4.86 % (2418626)Peak memory usage: 10 MB % 31.77/4.86 % (2418626)Instructions burned: 11 (million) % 31.77/4.86 % (2418626)------------------------------ % 31.77/4.86 % (2418626)------------------------------ % 31.77/4.86 % (2418628)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1848725150:fmbsr=1.7:i=920_2993 on theBenchmark for (2993ds/920Mi) % 31.77/4.86 % (2418628)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 31.77/4.86 % (2418628)Terminated due to inappropriate strategy. % 31.77/4.86 % (2418628)------------------------------ % 31.77/4.86 % (2418628)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 31.77/4.86 % (2418628)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.77/4.86 % (2418628)CaDiCaL version: 2.1.3 % 31.77/4.86 % (2418628)Termination reason: Inappropriate % 31.77/4.86 % (2418628)Time elapsed: 0.006 s % 31.77/4.86 % (2418628)Peak memory usage: 10 MB % 31.77/4.86 % (2418628)Instructions burned: 11 (million) % 31.77/4.86 % (2418628)------------------------------ % 31.77/4.86 % (2418628)------------------------------ % 31.77/4.86 % (2418630)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1415814316:i=5131_2993 on theBenchmark for (2993ds/5131Mi) % 31.77/4.86 % (2418601)Instruction limit reached! % 31.77/4.86 % (2418601)------------------------------ % 31.77/4.86 % (2418601)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 31.77/4.86 % (2418601)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.77/4.86 % (2418601)CaDiCaL version: 2.1.3 % 31.77/4.86 % (2418601)Termination reason: Instruction limit % 31.77/4.86 % (2418601)Termination phase: Saturation % 31.77/4.86 % (2418601)Time elapsed: 0.598 s % 31.77/4.86 % (2418601)Peak memory usage: 16 MB % 31.77/4.86 % (2418601)Instructions burned: 684 (million) % 31.77/4.86 % (2418632)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1484950009:i=1472:ins=7:fdi=8:gsp=on_2992 on theBenchmark for (2992ds/1472Mi) % 31.77/4.86 % (2418611)Instruction limit reached! % 31.77/4.86 % (2418611)------------------------------ % 39.04/5.86 % (2418611)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 39.04/5.86 % (2418611)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.04/5.86 % (2418611)CaDiCaL version: 2.1.3 % 39.04/5.86 % (2418611)Termination reason: Instruction limit % 39.04/5.86 % (2418611)Termination phase: Saturation % 39.04/5.86 % (2418611)Time elapsed: 0.661 s % 39.04/5.86 % (2418611)Peak memory usage: 21 MB % 39.04/5.86 % (2418611)Instructions burned: 1182 (million) % 39.04/5.86 % (2418635)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3707122454:i=6324_2990 on theBenchmark for (2990ds/6324Mi) % 39.04/5.86 % (2418635)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 39.04/5.86 % (2418635)Terminated due to inappropriate strategy. % 39.04/5.86 % (2418635)------------------------------ % 39.04/5.86 % (2418635)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 39.04/5.86 % (2418635)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.04/5.86 % (2418635)CaDiCaL version: 2.1.3 % 39.04/5.86 % (2418635)Termination reason: Inappropriate % 39.04/5.86 % (2418635)Time elapsed: 0.009 s % 39.04/5.86 % (2418635)Peak memory usage: 11 MB % 39.04/5.86 % (2418635)Instructions burned: 15 (million) % 39.04/5.86 % (2418635)------------------------------ % 39.04/5.86 % (2418635)------------------------------ % 39.04/5.86 % (2418638)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=3380576027:fmbsr=2.30978:i=2174_2990 on theBenchmark for (2990ds/2174Mi) % 39.04/5.86 % (2418638)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 39.04/5.86 % (2418638)Terminated due to inappropriate strategy. % 39.04/5.86 % (2418638)------------------------------ % 39.04/5.86 % (2418638)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 39.04/5.86 % (2418638)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.04/5.86 % (2418638)CaDiCaL version: 2.1.3 % 39.04/5.86 % (2418638)Termination reason: Inappropriate % 39.04/5.86 % (2418638)Time elapsed: 0.006 s % 39.04/5.86 % (2418638)Peak memory usage: 10 MB % 39.04/5.86 % (2418638)Instructions burned: 11 (million) % 39.04/5.86 % (2418638)------------------------------ % 39.04/5.87 % (2418638)------------------------------ % 39.04/5.87 % (2418640)ott-2_1_sil=16000:newcnf=on:random_seed=3386239631:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2990 on theBenchmark for (2990ds/869Mi) % 39.04/5.87 % (2418616)Instruction limit reached! % 39.04/5.87 % (2418616)------------------------------ % 39.04/5.87 % (2418616)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 39.04/5.87 % (2418616)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.04/5.87 % (2418616)CaDiCaL version: 2.1.3 % 39.04/5.87 % (2418616)Termination reason: Instruction limit % 39.04/5.87 % (2418616)Termination phase: Saturation % 39.04/5.87 % (2418616)Time elapsed: 0.698 s % 39.04/5.87 % (2418616)Peak memory usage: 18 MB % 39.04/5.87 % (2418616)Instructions burned: 692 (million) % 39.04/5.87 % (2418644)ott+10_1_sil=32000:tgt=ground:random_seed=4293316789:i=5114:av=off_2990 on theBenchmark for (2990ds/5114Mi) % 39.04/5.87 % (2418618)Instruction limit reached! % 39.04/5.87 % (2418618)------------------------------ % 39.04/5.87 % (2418618)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 39.04/5.87 % (2418618)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.04/5.87 % (2418618)CaDiCaL version: 2.1.3 % 39.04/5.87 % (2418618)Termination reason: Instruction limit % 39.04/5.87 % (2418618)Termination phase: Saturation % 39.04/5.87 % (2418618)Time elapsed: 0.851 s % 39.04/5.87 % (2418618)Peak memory usage: 18 MB % 39.04/5.87 % (2418618)Instructions burned: 879 (million) % 39.04/5.87 % (2418646)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=3946262013:i=54282_2987 on theBenchmark for (2987ds/54282Mi) % 39.04/5.87 % (2418646)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 39.04/5.87 % (2418646)Terminated due to inappropriate strategy. % 39.04/5.87 % (2418646)------------------------------ % 39.04/5.87 % (2418646)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 39.04/5.87 % (2418646)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.04/5.87 % (2418646)CaDiCaL version: 2.1.3 % 39.04/5.87 % (2418646)Termination reason: Inappropriate % 39.04/5.87 % (2418646)Time elapsed: 0.009 s % 39.04/5.87 % (2418646)Peak memory usage: 11 MB % 39.04/5.87 % (2418646)Instructions burned: 15 (million) % 152.87/21.85 % (2418646)------------------------------ % 152.87/21.85 % (2418646)------------------------------ % 152.87/21.85 % (2418648)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=2060697244:i=3512:aac=none_2987 on theBenchmark for (2987ds/3512Mi) % 152.87/21.85 % (2418640)Instruction limit reached! % 152.87/21.85 % (2418640)------------------------------ % 152.87/21.85 % (2418640)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 152.87/21.85 % (2418640)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 152.87/21.85 % (2418640)CaDiCaL version: 2.1.3 % 152.87/21.85 % (2418640)Termination reason: Instruction limit % 152.87/21.85 % (2418640)Termination phase: Saturation % 152.87/21.85 % (2418640)Time elapsed: 0.523 s % 152.87/21.85 % (2418640)Peak memory usage: 15 MB % 152.87/21.85 % (2418640)Instructions burned: 871 (million) % 152.87/21.85 % (2418650)dis+21_1_sil=32000:sas=cadical:random_seed=2190464174:i=3773:amm=off_2984 on theBenchmark for (2984ds/3773Mi) % 152.87/21.85 % (2418632)Instruction limit reached! % 152.87/21.85 % (2418632)------------------------------ % 152.87/21.85 % (2418632)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 152.87/21.85 % (2418632)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 152.87/21.85 % (2418632)CaDiCaL version: 2.1.3 % 152.87/21.85 % (2418632)Termination reason: Instruction limit % 152.87/21.85 % (2418632)Termination phase: Saturation % 152.87/21.85 % (2418632)Time elapsed: 1.393 s % 152.87/21.85 % (2418632)Peak memory usage: 27 MB % 152.87/21.85 % (2418632)Instructions burned: 1472 (million) % 152.87/21.85 % (2418656)ott+11_1_sil=16000:gs=on:random_seed=3516903330:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2978 on theBenchmark for (2978ds/2251Mi) % 152.87/21.85 % (2418650)Instruction limit reached! % 152.87/21.85 % (2418650)------------------------------ % 152.87/21.85 % (2418650)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 152.87/21.85 % (2418650)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 152.87/21.85 % (2418650)CaDiCaL version: 2.1.3 % 152.87/21.85 % (2418650)Termination reason: Instruction limit % 152.87/21.85 % (2418650)Termination phase: Saturation % 152.87/21.85 % (2418650)Time elapsed: 1.948 s % 152.87/21.85 % (2418650)Peak memory usage: 31 MB % 152.87/21.85 % (2418650)Instructions burned: 3774 (million) % 152.87/21.85 % (2418661)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=3867982782:fmbsr=1.6:i=67534_2965 on theBenchmark for (2965ds/67534Mi) % 152.87/21.85 % (2418661)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 152.87/21.85 % (2418661)Terminated due to inappropriate strategy. % 152.87/21.85 % (2418661)------------------------------ % 152.87/21.85 % (2418661)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 152.87/21.85 % (2418661)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 152.87/21.85 % (2418661)CaDiCaL version: 2.1.3 % 152.87/21.85 % (2418661)Termination reason: Inappropriate % 152.87/21.85 % (2418661)Time elapsed: 0.008 s % 152.87/21.85 % (2418661)Peak memory usage: 11 MB % 152.87/21.85 % (2418661)Instructions burned: 11 (million) % 152.87/21.85 % (2418661)------------------------------ % 152.87/21.85 % (2418661)------------------------------ % 152.87/21.85 % (2418663)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=1618494825:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2964 on theBenchmark for (2964ds/4591Mi) % 152.87/21.85 % (2418656)Instruction limit reached! % 152.87/21.85 % (2418656)------------------------------ % 152.87/21.85 % (2418656)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 152.87/21.85 % (2418656)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 152.87/21.85 % (2418656)CaDiCaL version: 2.1.3 % 152.87/21.85 % (2418656)Termination reason: Instruction limit % 152.87/21.85 % (2418656)Termination phase: Saturation % 152.87/21.85 % (2418656)Time elapsed: 2.011 s % 152.87/21.85 % (2418656)Peak memory usage: 26 MB % 152.87/21.85 % (2418656)Instructions burned: 2252 (million) % 152.87/21.85 % (2418675)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=3463063479:i=29340_2957 on theBenchmark for (2957ds/29340Mi) % 152.87/21.85 % (2418648)Instruction limit reached! % 152.87/21.85 % (2418648)------------------------------ % 152.87/21.85 % (2418648)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 152.87/21.85 % (2418648)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 152.87/21.85 % (2418648)CaDiCaL version: 2.1.3 % 152.87/21.85 % (2418648)Termination reason: Instruction limit % 205.59/29.30 % (2418648)Termination phase: Saturation % 205.59/29.30 % (2418648)Time elapsed: 3.288 s % 205.59/29.30 % (2418648)Peak memory usage: 32 MB % 205.59/29.30 % (2418648)Instructions burned: 3512 (million) % 205.59/29.30 % (2418679)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=3663555188:i=5211_2954 on theBenchmark for (2954ds/5211Mi) % 205.59/29.30 % (2418630)Instruction limit reached! % 205.59/29.30 % (2418630)------------------------------ % 205.59/29.30 % (2418630)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 205.59/29.30 % (2418630)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 205.59/29.30 % (2418630)CaDiCaL version: 2.1.3 % 205.59/29.30 % (2418630)Termination reason: Instruction limit % 205.59/29.30 % (2418630)Termination phase: Saturation % 205.59/29.30 % (2418630)Time elapsed: 4.646 s % 205.59/29.30 % (2418630)Peak memory usage: 30 MB % 205.59/29.30 % (2418630)Instructions burned: 5131 (million) % 205.59/29.30 % (2418683)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=1795184536:i=5497:nm=2_2946 on theBenchmark for (2946ds/5497Mi) % 205.59/29.30 % (2418683)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 205.59/29.30 % (2418683)Terminated due to inappropriate strategy. % 205.59/29.30 % (2418683)------------------------------ % 205.59/29.30 % (2418683)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 205.59/29.30 % (2418683)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 205.59/29.30 % (2418683)CaDiCaL version: 2.1.3 % 205.59/29.30 % (2418683)Termination reason: Inappropriate % 205.59/29.30 % (2418683)Time elapsed: 0.009 s % 205.59/29.30 % (2418683)Peak memory usage: 11 MB % 205.59/29.30 % (2418683)Instructions burned: 13 (million) % 205.59/29.30 % (2418683)------------------------------ % 205.59/29.30 % (2418683)------------------------------ % 205.59/29.30 % (2418685)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=679692164:fmbsr=2:i=46332_2945 on theBenchmark for (2945ds/46332Mi) % 205.59/29.30 % (2418685)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 205.59/29.30 % (2418685)Terminated due to inappropriate strategy. % 205.59/29.30 % (2418685)------------------------------ % 205.59/29.30 % (2418685)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 205.59/29.30 % (2418685)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 205.59/29.30 % (2418685)CaDiCaL version: 2.1.3 % 205.59/29.30 % (2418685)Termination reason: Inappropriate % 205.59/29.30 % (2418685)Time elapsed: 0.006 s % 205.59/29.30 % (2418685)Peak memory usage: 11 MB % 205.59/29.30 % (2418685)Instructions burned: 11 (million) % 205.59/29.30 % (2418685)------------------------------ % 205.59/29.30 % (2418685)------------------------------ % 205.59/29.30 % (2418687)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=760857528:i=14071_2945 on theBenchmark for (2945ds/14071Mi) % 205.59/29.30 % (2418687)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 205.59/29.30 % (2418687)Terminated due to inappropriate strategy. % 205.59/29.30 % (2418687)------------------------------ % 205.59/29.30 % (2418687)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 205.59/29.30 % (2418687)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 205.59/29.30 % (2418687)CaDiCaL version: 2.1.3 % 205.59/29.30 % (2418687)Termination reason: Inappropriate % 205.59/29.30 % (2418687)Time elapsed: 0.006 s % 205.59/29.30 % (2418687)Peak memory usage: 11 MB % 205.59/29.30 % (2418687)Instructions burned: 11 (million) % 205.59/29.30 % (2418687)------------------------------ % 205.59/29.30 % (2418687)------------------------------ % 205.59/29.30 % (2418689)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1127618749:i=22565:add=on:rawr=on_2945 on theBenchmark for (2945ds/22565Mi) % 205.59/29.30 % (2418663)Instruction limit reached! % 205.59/29.30 % (2418663)------------------------------ % 205.59/29.30 % (2418663)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 205.59/29.30 % (2418663)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 205.59/29.30 % (2418663)CaDiCaL version: 2.1.3 % 205.59/29.30 % (2418663)Termination reason: Instruction limit % 205.59/29.30 % (2418663)Termination phase: Saturation % 205.59/29.30 % (2418663)Time elapsed: 1.997 s % 205.59/29.30 % (2418663)Peak memory usage: 34 MB % 205.59/29.30 % (2418663)Instructions burned: 4591 (million) % 205.59/29.30 % (2418691)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=1706707387:i=8173:av=off_2944 on theBenchmark for (2944ds/8173Mi) % 207.66/29.53 % (2418644)Instruction limit reached! % 207.66/29.53 % (2418644)------------------------------ % 207.66/29.53 % (2418644)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 207.66/29.53 % (2418644)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 207.66/29.53 % (2418644)CaDiCaL version: 2.1.3 % 207.66/29.53 % (2418644)Termination reason: Instruction limit % 207.66/29.53 % (2418644)Termination phase: Saturation % 207.66/29.53 % (2418644)Time elapsed: 5.245 s % 207.66/29.53 % (2418644)Peak memory usage: 32 MB % 207.66/29.53 % (2418644)Instructions burned: 5114 (million) % 207.66/29.53 % (2418693)dis+10_16:1_sil=16000:random_seed=4162048577:i=9155:fsr=off_2937 on theBenchmark for (2937ds/9155Mi) % 207.66/29.53 % (2418679)Instruction limit reached! % 207.66/29.53 % (2418679)------------------------------ % 207.66/29.53 % (2418679)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 207.66/29.53 % (2418679)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 207.66/29.53 % (2418679)CaDiCaL version: 2.1.3 % 207.66/29.53 % (2418679)Termination reason: Instruction limit % 207.66/29.53 % (2418679)Termination phase: Saturation % 207.66/29.53 % (2418679)Time elapsed: 4.421 s % 207.66/29.53 % (2418679)Peak memory usage: 42 MB % 207.66/29.53 % (2418679)Instructions burned: 5212 (million) % 207.66/29.53 % (2418697)ott-3_8_sil=64000:random_seed=3928872370:i=20139:bs=on_2909 on theBenchmark for (2909ds/20139Mi) % 207.66/29.53 % (2418691)Instruction limit reached! % 207.66/29.53 % (2418691)------------------------------ % 207.66/29.53 % (2418691)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 207.66/29.53 % (2418691)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 207.66/29.53 % (2418691)CaDiCaL version: 2.1.3 % 207.66/29.53 % (2418691)Termination reason: Instruction limit % 207.66/29.53 % (2418691)Termination phase: Saturation % 207.66/29.53 % (2418691)Time elapsed: 4.359 s % 207.66/29.53 % (2418691)Peak memory usage: 57 MB % 207.66/29.53 % (2418691)Instructions burned: 8174 (million) % 207.66/29.53 % (2418699)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=1411666761:fmbsr=2:i=32576_2900 on theBenchmark for (2900ds/32576Mi) % 207.66/29.53 % (2418699)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 207.66/29.53 % (2418699)Terminated due to inappropriate strategy. % 207.66/29.53 % (2418699)------------------------------ % 207.66/29.53 % (2418699)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 207.66/29.53 % (2418699)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 207.66/29.53 % (2418699)CaDiCaL version: 2.1.3 % 207.66/29.53 % (2418699)Termination reason: Inappropriate % 207.66/29.53 % (2418699)Time elapsed: 0.011 s % 207.66/29.53 % (2418699)Peak memory usage: 11 MB % 207.66/29.53 % (2418699)Instructions burned: 15 (million) % 207.66/29.53 % (2418699)------------------------------ % 207.66/29.53 % (2418699)------------------------------ % 207.66/29.53 % (2418701)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=397775697:i=11404_2900 on theBenchmark for (2900ds/11404Mi) % 207.66/29.53 % (2418693)Instruction limit reached! % 207.66/29.53 % (2418693)------------------------------ % 207.66/29.53 % (2418693)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 207.66/29.53 % (2418693)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 207.66/29.53 % (2418693)CaDiCaL version: 2.1.3 % 207.66/29.53 % (2418693)Termination reason: Instruction limit % 207.66/29.53 % (2418693)Termination phase: Saturation % 207.66/29.53 % (2418693)Time elapsed: 8.148 s % 207.66/29.53 % (2418693)Peak memory usage: 52 MB % 207.66/29.53 % (2418693)Instructions burned: 9156 (million) % 207.66/29.53 % (2418711)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=277824639:i=14134_2855 on theBenchmark for (2855ds/14134Mi) % 207.66/29.53 % (2418701)Instruction limit reached! % 207.66/29.53 % (2418701)------------------------------ % 207.66/29.53 % (2418701)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 207.66/29.53 % (2418701)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 207.66/29.53 % (2418701)CaDiCaL version: 2.1.3 % 207.66/29.53 % (2418701)Termination reason: Instruction limit % 207.66/29.53 % (2418701)Termination phase: Saturation % 207.66/29.53 % (2418701)Time elapsed: 6.392 s % 207.66/29.53 % (2418701)Peak memory usage: 63 MB % 207.66/29.53 % (2418701)Instructions burned: 11405 (million) % 207.66/29.53 % (2418713)dis+33_16_sil=32000:sac=on:random_seed=2133562563:i=15851:nm=0_2836 on theBenchmark for (2836ds/15851Mi) % 207.66/29.53 % (2418689)Instruction limit reached! % 207.66/29.53 % (2418689)------------------------------ % 207.66/29.53 % (2418689)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 269.63/38.27 % (2418689)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 269.63/38.27 % (2418689)CaDiCaL version: 2.1.3 % 269.63/38.27 % (2418689)Termination reason: Instruction limit % 269.63/38.27 % (2418689)Termination phase: Saturation % 269.63/38.27 % (2418689)Time elapsed: 16.064 s % 269.63/38.27 % (2418689)Peak memory usage: 21 MB % 269.63/38.27 % (2418689)Instructions burned: 22566 (million) % 269.63/38.27 % (2418717)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=2650978935:avsq=on:i=17627:add=on:amm=off_2784 on theBenchmark for (2784ds/17627Mi) % 269.63/38.27 % (2418713)Instruction limit reached! % 269.63/38.27 % (2418713)------------------------------ % 269.63/38.27 % (2418713)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 269.63/38.27 % (2418713)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 269.63/38.27 % (2418713)CaDiCaL version: 2.1.3 % 269.63/38.27 % (2418713)Termination reason: Instruction limit % 269.63/38.27 % (2418713)Termination phase: Function definition elimination % 269.63/38.27 % (2418713)Time elapsed: 6.705 s % 269.63/38.27 % (2418713)Peak memory usage: 42 MB % 269.63/38.27 % (2418713)Instructions burned: 15852 (million) % 269.63/38.27 % (2418719)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=1674711444:s2a=on:i=53295_2768 on theBenchmark for (2768ds/53295Mi) % 269.63/38.27 % (2418675)Instruction limit reached! % 269.63/38.27 % (2418675)------------------------------ % 269.63/38.27 % (2418675)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 269.63/38.27 % (2418675)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 269.63/38.27 % (2418675)CaDiCaL version: 2.1.3 % 269.63/38.27 % (2418675)Termination reason: Instruction limit % 269.63/38.27 % (2418675)Termination phase: Saturation % 269.63/38.27 % (2418675)Time elapsed: 22.100 s % 269.63/38.27 % (2418675)Peak memory usage: 97 MB % 269.63/38.27 % (2418675)Instructions burned: 29340 (million) % 269.63/38.27 % (2418721)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=3772841439:i=26857:ins=20_2736 on theBenchmark for (2736ds/26857Mi) % 269.63/38.27 % (2418721)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 269.63/38.27 % (2418721)Terminated due to inappropriate strategy. % 269.63/38.27 % (2418721)------------------------------ % 269.63/38.27 % (2418721)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 269.63/38.27 % (2418721)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 269.63/38.27 % (2418721)CaDiCaL version: 2.1.3 % 269.63/38.27 % (2418721)Termination reason: Inappropriate % 269.63/38.27 % (2418721)Time elapsed: 0.010 s % 269.63/38.27 % (2418721)Peak memory usage: 11 MB % 269.63/38.27 % (2418721)Instructions burned: 11 (million) % 269.63/38.27 % (2418721)------------------------------ % 269.63/38.27 % (2418721)------------------------------ % 269.63/38.27 % (2418724)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=4059594175:i=28120:bs=on:fsr=off_2736 on theBenchmark for (2736ds/28120Mi) % 269.63/38.27 % (2418711)Instruction limit reached! % 269.63/38.27 % (2418711)------------------------------ % 269.63/38.27 % (2418711)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 269.63/38.27 % (2418711)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 269.63/38.27 % (2418711)CaDiCaL version: 2.1.3 % 269.63/38.27 % (2418711)Termination reason: Instruction limit % 269.63/38.27 % (2418711)Termination phase: Saturation % 269.63/38.27 % (2418711)Time elapsed: 14.456 s % 269.63/38.27 % (2418711)Peak memory usage: 69 MB % 269.63/38.27 % (2418711)Instructions burned: 14135 (million) % 269.63/38.27 % (2418761)fmb+10_1_sil=256000:fmbss=7:random_seed=3857815123:fmbsr=1.6:i=182295_2710 on theBenchmark for (2710ds/182295Mi) % 269.63/38.27 % (2418761)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 269.63/38.27 % (2418761)Terminated due to inappropriate strategy. % 269.63/38.27 % (2418761)------------------------------ % 269.63/38.27 % (2418761)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 269.63/38.27 % (2418761)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 269.63/38.27 % (2418761)CaDiCaL version: 2.1.3 % 269.63/38.27 % (2418761)Termination reason: Inappropriate % 269.63/38.27 % (2418761)Time elapsed: 0.009 s % 269.63/38.27 % (2418761)Peak memory usage: 11 MB % 269.63/38.27 % (2418761)Instructions burned: 11 (million) % 269.63/38.27 % (2418761)------------------------------ % 269.63/38.27 % (2418761)------------------------------ % 269.63/38.27 % (2418763)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=2130262490:i=44625:gsp=on_2710 on theBenchmark for (2710ds/44625Mi) % 290.98/41.29 % (2418763)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 290.98/41.29 % (2418763)Terminated due to inappropriate strategy. % 290.98/41.29 % (2418763)------------------------------ % 290.98/41.29 % (2418763)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 290.98/41.29 % (2418763)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 290.98/41.29 % (2418763)CaDiCaL version: 2.1.3 % 290.98/41.29 % (2418763)Termination reason: Inappropriate % 290.98/41.29 % (2418763)Time elapsed: 0.018 s % 290.98/41.29 % (2418763)Peak memory usage: 11 MB % 290.98/41.29 % (2418763)Instructions burned: 18 (million) % 290.98/41.29 % (2418763)------------------------------ % 290.98/41.29 % (2418763)------------------------------ % 290.98/41.29 % (2418765)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=754929868:i=160505_2709 on theBenchmark for (2709ds/160505Mi) % 290.98/41.29 % (2418765)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 290.98/41.29 % (2418765)Terminated due to inappropriate strategy. % 290.98/41.29 % (2418765)------------------------------ % 290.98/41.29 % (2418765)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 290.98/41.29 % (2418765)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 290.98/41.29 % (2418765)CaDiCaL version: 2.1.3 % 290.98/41.29 % (2418765)Termination reason: Inappropriate % 290.98/41.29 % (2418765)Time elapsed: 0.006 s % 290.98/41.29 % (2418765)Peak memory usage: 11 MB % 290.98/41.29 % (2418765)Instructions burned: 11 (million) % 290.98/41.29 % (2418765)------------------------------ % 290.98/41.29 % (2418765)------------------------------ % 290.98/41.29 % (2418767)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=3769977313:fmbsr=1.3:i=225729_2709 on theBenchmark for (2709ds/225729Mi) % 290.98/41.29 % (2418767)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 290.98/41.29 % (2418767)Terminated due to inappropriate strategy. % 290.98/41.29 % (2418767)------------------------------ % 290.98/41.29 % (2418767)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 290.98/41.29 % (2418767)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 290.98/41.29 % (2418767)CaDiCaL version: 2.1.3 % 290.98/41.29 % (2418767)Termination reason: Inappropriate % 290.98/41.29 % (2418767)Time elapsed: 0.011 s % 290.98/41.29 % (2418767)Peak memory usage: 11 MB % 290.98/41.29 % (2418767)Instructions burned: 11 (million) % 290.98/41.29 % (2418767)------------------------------ % 290.98/41.29 % (2418767)------------------------------ % 290.98/41.29 % (2418769)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=751936231:fmbsr=2:i=185024:ins=7_2709 on theBenchmark for (2709ds/185024Mi) % 290.98/41.29 % (2418769)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 290.98/41.29 % (2418769)Terminated due to inappropriate strategy. % 290.98/41.29 % (2418769)------------------------------ % 290.98/41.29 % (2418769)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 290.98/41.29 % (2418769)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 290.98/41.29 % (2418769)CaDiCaL version: 2.1.3 % 290.98/41.29 % (2418769)Termination reason: Inappropriate % 290.98/41.29 % (2418769)Time elapsed: 0.011 s % 290.98/41.29 % (2418769)Peak memory usage: 11 MB % 290.98/41.29 % (2418769)Instructions burned: 11 (million) % 290.98/41.29 % (2418769)------------------------------ % 290.98/41.29 % (2418769)------------------------------ % 290.98/41.29 % (2418771)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=3736616244:rtra=on_2708 on theBenchmark for (2708ds/0Mi) % 290.98/41.29 % (2418771)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 290.98/41.29 % (2418771)Terminated due to inappropriate strategy. % 290.98/41.29 % (2418771)------------------------------ % 290.98/41.29 % (2418771)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 290.98/41.29 % (2418771)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 290.98/41.29 % (2418771)CaDiCaL version: 2.1.3 % 290.98/41.29 % (2418771)Termination reason: Inappropriate % 290.98/41.29 % (2418771)Time elapsed: 0.019 s % 290.98/41.29 % (2418771)Peak memory usage: 11 MB % 290.98/41.29 % (2418771)Instructions burned: 15 (million) % 290.98/41.29 % (2418771)------------------------------ % 290.98/41.29 % (2418771)------------------------------ % 290.98/41.29 % (2418773)% WARNING: option uhcvi not known. % 290.98/41.29 % (2418773)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:Terminated % 300.22/42.54 % Vampire exiting %------------------------------------------------------------------------------