%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWX135_1 : TPTP v9.3.1. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % Computer : n005.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 29 01:46:32 PM UTC 2026 % Result : Timeout 291.39s 41.42s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWX135_1 : TPTP v9.3.1. Released v9.3.0. % 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.10/0.22 % Computer : n005.cluster.edu % 0.10/0.22 % Model : x86_64 x86_64 % 0.10/0.22 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.22 % Memory : 8046.5625MB % 0.10/0.22 % OS : Linux 6.8.0-71-generic % 0.10/0.22 % CPULimit : 300 % 0.10/0.22 % WCLimit : 300 % 0.10/0.22 % DateTime : Mon Sep 28 15:03:01 UTC 2026 % 0.10/0.23 % CPUTime : % 0.10/0.23 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.24/0.28 Running first-order model finding % 0.24/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 % 4.84/1.11 % (845614)Will run a generic schedule for satisfiability detection. % 4.84/1.11 % (845623)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2566970233_2998 on theBenchmark for (2998ds/0Mi) % 4.84/1.11 % (845624)% WARNING: option uhcvi not known. % 4.84/1.11 % (845626)dis+10_1_sil=32000:sp=arity:random_seed=3318241918:i=103:fgj=on_2998 on theBenchmark for (2998ds/103Mi) % 4.84/1.11 % (845624)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=415666846:i=135531:add=off:rawr=on_2998 on theBenchmark for (2998ds/135531Mi) % 4.84/1.11 % (845625)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=95454769:i=88024:add=on:rawr=on_2998 on theBenchmark for (2998ds/88024Mi) % 4.84/1.11 % (845627)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1143818848:i=116_2998 on theBenchmark for (2998ds/116Mi) % 4.84/1.11 % (845628)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=361313160:i=131_2998 on theBenchmark for (2998ds/131Mi) % 4.84/1.11 % (845629)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2520604748:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2998 on theBenchmark for (2998ds/159Mi) % 4.84/1.11 % (845623)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 4.84/1.11 % (845623)Terminated due to inappropriate strategy. % 4.84/1.11 % (845623)------------------------------ % 4.84/1.11 % (845623)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 4.84/1.11 % (845623)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.84/1.11 % (845623)CaDiCaL version: 2.1.3 % 4.84/1.11 % (845623)Termination reason: Inappropriate % 4.84/1.11 % (845623)Time elapsed: 0.050 s % 4.84/1.11 % (845623)Peak memory usage: 10 MB % 4.84/1.11 % (845623)Instructions burned: 118 (million) % 4.84/1.11 % (845623)------------------------------ % 4.84/1.11 % (845623)------------------------------ % 4.84/1.11 % (845637)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=420304305:i=714:nm=2_2998 on theBenchmark for (2998ds/714Mi) % 4.84/1.11 % (845626)Instruction limit reached! % 4.84/1.11 % (845626)------------------------------ % 4.84/1.11 % (845626)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 4.84/1.11 % (845626)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.84/1.11 % (845626)CaDiCaL version: 2.1.3 % 4.84/1.11 % (845626)Termination reason: Instruction limit % 4.84/1.11 % (845626)Termination phase: Property scanning % 4.84/1.11 % (845626)Time elapsed: 0.083 s % 4.84/1.11 % (845626)Peak memory usage: 10 MB % 4.84/1.11 % (845626)Instructions burned: 104 (million) % 4.84/1.11 % (845629)Instruction limit reached! % 4.84/1.11 % (845629)------------------------------ % 4.84/1.11 % (845629)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 4.84/1.11 % (845629)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.84/1.11 % (845629)CaDiCaL version: 2.1.3 % 4.84/1.11 % (845629)Termination reason: Instruction limit % 4.84/1.11 % (845629)Termination phase: Saturation % 4.84/1.11 % (845629)Time elapsed: 0.092 s % 4.84/1.11 % (845629)Peak memory usage: 12 MB % 4.84/1.11 % (845629)Instructions burned: 160 (million) % 4.84/1.11 % (845627)Instruction limit reached! % 4.84/1.11 % (845627)------------------------------ % 4.84/1.11 % (845627)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 4.84/1.11 % (845627)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.84/1.11 % (845627)CaDiCaL version: 2.1.3 % 4.84/1.11 % (845627)Termination reason: Instruction limit % 4.84/1.11 % (845627)Termination phase: Property scanning % 4.84/1.11 % (845627)Time elapsed: 0.095 s % 4.84/1.11 % (845627)Peak memory usage: 10 MB % 4.84/1.11 % (845627)Instructions burned: 117 (million) % 4.84/1.11 % (845628)Instruction limit reached! % 4.84/1.11 % (845628)------------------------------ % 4.84/1.11 % (845628)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 4.84/1.11 % (845628)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.84/1.11 % (845628)CaDiCaL version: 2.1.3 % 4.84/1.11 % (845628)Termination reason: Instruction limit % 4.84/1.11 % (845628)Termination phase: Saturation % 4.84/1.11 % (845628)Time elapsed: 0.104 s % 4.84/1.11 % (845628)Peak memory usage: 11 MB % 4.84/1.11 % (845628)Instructions burned: 132 (million) % 4.84/1.11 % (845637)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 4.84/1.11 % (845637)Terminated due to inappropriate strategy. % 4.84/1.11 % (845637)------------------------------ % 7.38/1.89 % (845637)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.38/1.89 % (845637)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.38/1.89 % (845637)CaDiCaL version: 2.1.3 % 7.38/1.89 % (845637)Termination reason: Inappropriate % 7.38/1.89 % (845637)Time elapsed: 0.050 s % 7.38/1.89 % (845637)Peak memory usage: 10 MB % 7.38/1.89 % (845637)Instructions burned: 118 (million) % 7.38/1.89 % (845637)------------------------------ % 7.38/1.89 % (845637)------------------------------ % 7.38/1.89 % (845641)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=826473818:i=131:bd=preordered:fsd=on_2997 on theBenchmark for (2997ds/131Mi) % 7.38/1.89 % (845643)ott-21_1_sil=16000:fs=off:random_seed=1596418579:i=180:av=off:fsr=off_2997 on theBenchmark for (2997ds/180Mi) % 7.38/1.89 % (845642)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=3051300687:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2997 on theBenchmark for (2997ds/684Mi) % 7.38/1.89 % (845645)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2198192982:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi) % 7.38/1.89 % (845644)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1981811703:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi) % 7.38/1.89 % (845645)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 7.38/1.89 % (845645)Terminated due to inappropriate strategy. % 7.38/1.89 % (845645)------------------------------ % 7.38/1.89 % (845645)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.38/1.89 % (845645)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.38/1.89 % (845645)CaDiCaL version: 2.1.3 % 7.38/1.89 % (845645)Termination reason: Inappropriate % 7.38/1.89 % (845645)Time elapsed: 0.037 s % 7.38/1.89 % (845645)Peak memory usage: 10 MB % 7.38/1.89 % (845645)Instructions burned: 90 (million) % 7.38/1.89 % (845645)------------------------------ % 7.38/1.89 % (845645)------------------------------ % 7.38/1.89 % (845652)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1496792198:i=1179_2996 on theBenchmark for (2996ds/1179Mi) % 7.38/1.89 % (845641)Instruction limit reached! % 7.38/1.89 % (845641)------------------------------ % 7.38/1.89 % (845641)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.38/1.89 % (845641)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.38/1.89 % (845641)CaDiCaL version: 2.1.3 % 7.38/1.89 % (845641)Termination reason: Instruction limit % 7.38/1.89 % (845641)Termination phase: Saturation % 7.38/1.89 % (845641)Time elapsed: 0.105 s % 7.38/1.89 % (845641)Peak memory usage: 12 MB % 7.38/1.89 % (845641)Instructions burned: 132 (million) % 7.38/1.89 % (845655)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=4169959216:i=889:ins=1_2996 on theBenchmark for (2996ds/889Mi) % 7.38/1.89 % (845643)Instruction limit reached! % 7.38/1.89 % (845643)------------------------------ % 7.38/1.89 % (845643)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.38/1.89 % (845643)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.38/1.89 % (845643)CaDiCaL version: 2.1.3 % 7.38/1.89 % (845643)Termination reason: Instruction limit % 7.38/1.89 % (845643)Termination phase: Saturation % 7.38/1.89 % (845643)Time elapsed: 0.142 s % 7.38/1.89 % (845643)Peak memory usage: 11 MB % 7.38/1.89 % (845643)Instructions burned: 181 (million) % 7.38/1.89 % (845657)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=2464726878:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2995 on theBenchmark for (2995ds/692Mi) % 7.38/1.89 % (845655)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 7.38/1.89 % (845655)Terminated due to inappropriate strategy. % 7.38/1.89 % (845655)------------------------------ % 7.38/1.89 % (845655)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.38/1.89 % (845655)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.38/1.89 % (845655)CaDiCaL version: 2.1.3 % 7.38/1.89 % (845655)Termination reason: Inappropriate % 7.38/1.89 % (845655)Time elapsed: 0.062 s % 7.38/1.89 % (845655)Peak memory usage: 10 MB % 7.38/1.89 % (845655)Instructions burned: 90 (million) % 7.38/1.89 % (845655)------------------------------ % 7.38/1.89 % (845655)------------------------------ % 23.58/3.87 % (845660)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=196391971:i=879:kws=inv_precedence:fsr=off_2995 on theBenchmark for (2995ds/879Mi) % 23.58/3.87 % (845644)Instruction limit reached! % 23.58/3.87 % (845644)------------------------------ % 23.58/3.87 % (845644)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 23.58/3.87 % (845644)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.58/3.87 % (845644)CaDiCaL version: 2.1.3 % 23.58/3.87 % (845644)Termination reason: Instruction limit % 23.58/3.87 % (845644)Termination phase: Saturation % 23.58/3.87 % (845644)Time elapsed: 0.295 s % 23.58/3.87 % (845644)Peak memory usage: 13 MB % 23.58/3.87 % (845644)Instructions burned: 478 (million) % 23.58/3.87 % (845665)fmb+10_1_sil=64000:random_seed=3832935103:i=22061:nm=2:gsp=on_2994 on theBenchmark for (2994ds/22061Mi) % 23.58/3.87 % (845665)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 23.58/3.87 % (845665)Terminated due to inappropriate strategy. % 23.58/3.87 % (845665)------------------------------ % 23.58/3.87 % (845665)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 23.58/3.87 % (845665)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.58/3.87 % (845665)CaDiCaL version: 2.1.3 % 23.58/3.87 % (845665)Termination reason: Inappropriate % 23.58/3.87 % (845665)Time elapsed: 0.070 s % 23.58/3.87 % (845665)Peak memory usage: 11 MB % 23.58/3.87 % (845665)Instructions burned: 118 (million) % 23.58/3.87 % (845665)------------------------------ % 23.58/3.87 % (845665)------------------------------ % 23.58/3.87 % (845667)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=659677413:i=9515:nm=5_2993 on theBenchmark for (2993ds/9515Mi) % 23.58/3.87 % (845652)Instruction limit reached! % 23.58/3.87 % (845652)------------------------------ % 23.58/3.87 % (845652)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 23.58/3.87 % (845652)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.58/3.87 % (845652)CaDiCaL version: 2.1.3 % 23.58/3.87 % (845652)Termination reason: Instruction limit % 23.58/3.87 % (845652)Termination phase: Saturation % 23.58/3.87 % (845652)Time elapsed: 0.404 s % 23.58/3.87 % (845652)Peak memory usage: 17 MB % 23.58/3.87 % (845652)Instructions burned: 1179 (million) % 23.58/3.87 % (845670)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=73170258:fmbsr=1.7:i=920_2992 on theBenchmark for (2992ds/920Mi) % 23.58/3.87 % (845667)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 23.58/3.87 % (845667)Terminated due to inappropriate strategy. % 23.58/3.87 % (845667)------------------------------ % 23.58/3.87 % (845667)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 23.58/3.87 % (845667)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.58/3.87 % (845667)CaDiCaL version: 2.1.3 % 23.58/3.87 % (845667)Termination reason: Inappropriate % 23.58/3.87 % (845667)Time elapsed: 0.096 s % 23.58/3.87 % (845667)Peak memory usage: 10 MB % 23.58/3.87 % (845667)Instructions burned: 118 (million) % 23.58/3.87 % (845667)------------------------------ % 23.58/3.87 % (845667)------------------------------ % 23.58/3.87 % (845670)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 23.58/3.87 % (845670)Terminated due to inappropriate strategy. % 23.58/3.87 % (845670)------------------------------ % 23.58/3.87 % (845670)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 23.58/3.87 % (845670)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.58/3.87 % (845670)CaDiCaL version: 2.1.3 % 23.58/3.87 % (845670)Termination reason: Inappropriate % 23.58/3.87 % (845670)Time elapsed: 0.052 s % 23.58/3.87 % (845670)Peak memory usage: 10 MB % 23.58/3.87 % (845670)Instructions burned: 118 (million) % 23.58/3.87 % (845670)------------------------------ % 23.58/3.87 % (845670)------------------------------ % 23.58/3.87 % (845642)Instruction limit reached! % 23.58/3.87 % (845642)------------------------------ % 23.58/3.87 % (845642)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 23.58/3.87 % (845642)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.58/3.87 % (845642)CaDiCaL version: 2.1.3 % 23.58/3.87 % (845642)Termination reason: Instruction limit % 23.58/3.87 % (845642)Termination phase: Saturation % 23.58/3.87 % (845642)Time elapsed: 0.551 s % 23.58/3.87 % (845642)Peak memory usage: 15 MB % 23.58/3.87 % (845642)Instructions burned: 684 (million) % 23.58/3.87 % (845673)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1809640115:i=5131_2992 on theBenchmark for (2992ds/5131Mi) % 34.73/5.35 % (845674)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2493759338:i=1472:ins=7:fdi=8:gsp=on_2991 on theBenchmark for (2991ds/1472Mi) % 34.73/5.35 % (845657)Instruction limit reached! % 34.73/5.35 % (845657)------------------------------ % 34.73/5.35 % (845657)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 34.73/5.35 % (845657)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.73/5.35 % (845657)CaDiCaL version: 2.1.3 % 34.73/5.35 % (845657)Termination reason: Instruction limit % 34.73/5.35 % (845657)Termination phase: Saturation % 34.73/5.35 % (845657)Time elapsed: 0.421 s % 34.73/5.35 % (845657)Peak memory usage: 17 MB % 34.73/5.35 % (845657)Instructions burned: 693 (million) % 34.73/5.35 % (845675)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3386268305:i=6324_2991 on theBenchmark for (2991ds/6324Mi) % 34.73/5.35 % (845679)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=4118073421:fmbsr=2.30978:i=2174_2991 on theBenchmark for (2991ds/2174Mi) % 34.73/5.35 % (845675)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 34.73/5.35 % (845675)Terminated due to inappropriate strategy. % 34.73/5.35 % (845675)------------------------------ % 34.73/5.35 % (845675)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 34.73/5.35 % (845675)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.73/5.35 % (845675)CaDiCaL version: 2.1.3 % 34.73/5.35 % (845675)Termination reason: Inappropriate % 34.73/5.35 % (845675)Time elapsed: 0.096 s % 34.73/5.35 % (845675)Peak memory usage: 11 MB % 34.73/5.35 % (845675)Instructions burned: 118 (million) % 34.73/5.35 % (845675)------------------------------ % 34.73/5.35 % (845675)------------------------------ % 34.73/5.35 % (845679)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 34.73/5.35 % (845679)Terminated due to inappropriate strategy. % 34.73/5.35 % (845679)------------------------------ % 34.73/5.35 % (845679)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 34.73/5.35 % (845679)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.73/5.35 % (845679)CaDiCaL version: 2.1.3 % 34.73/5.35 % (845679)Termination reason: Inappropriate % 34.73/5.35 % (845679)Time elapsed: 0.096 s % 34.73/5.35 % (845679)Peak memory usage: 10 MB % 34.73/5.35 % (845679)Instructions burned: 118 (million) % 34.73/5.35 % (845679)------------------------------ % 34.73/5.35 % (845679)------------------------------ % 34.73/5.35 % (845681)ott-2_1_sil=16000:newcnf=on:random_seed=902928270:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2990 on theBenchmark for (2990ds/869Mi) % 34.73/5.35 % (845682)ott+10_1_sil=32000:tgt=ground:random_seed=2475827188:i=5114:av=off_2990 on theBenchmark for (2990ds/5114Mi) % 34.73/5.35 % (845660)Instruction limit reached! % 34.73/5.35 % (845660)------------------------------ % 34.73/5.35 % (845660)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 34.73/5.35 % (845660)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.73/5.35 % (845660)CaDiCaL version: 2.1.3 % 34.73/5.35 % (845660)Termination reason: Instruction limit % 34.73/5.35 % (845660)Termination phase: Saturation % 34.73/5.35 % (845660)Time elapsed: 0.650 s % 34.73/5.35 % (845660)Peak memory usage: 13 MB % 34.73/5.35 % (845660)Instructions burned: 879 (million) % 34.73/5.35 % (845685)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=3518952528:i=54282_2988 on theBenchmark for (2988ds/54282Mi) % 34.73/5.35 % (845685)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 34.73/5.35 % (845685)Terminated due to inappropriate strategy. % 34.73/5.35 % (845685)------------------------------ % 34.73/5.35 % (845685)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 34.73/5.35 % (845685)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.73/5.35 % (845685)CaDiCaL version: 2.1.3 % 34.73/5.35 % (845685)Termination reason: Inappropriate % 34.73/5.35 % (845685)Time elapsed: 0.058 s % 34.73/5.35 % (845685)Peak memory usage: 11 MB % 34.73/5.35 % (845685)Instructions burned: 118 (million) % 34.73/5.35 % (845685)------------------------------ % 34.73/5.35 % (845685)------------------------------ % 34.73/5.35 % (845687)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=903047183:i=3512:aac=none_2987 on theBenchmark for (2987ds/3512Mi) % 34.73/5.35 % (845681)Instruction limit reached! % 132.68/19.05 % (845681)------------------------------ % 132.68/19.05 % (845681)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 132.68/19.05 % (845681)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 132.68/19.05 % (845681)CaDiCaL version: 2.1.3 % 132.68/19.05 % (845681)Termination reason: Instruction limit % 132.68/19.05 % (845681)Termination phase: Saturation % 132.68/19.05 % (845681)Time elapsed: 0.621 s % 132.68/19.05 % (845681)Peak memory usage: 16 MB % 132.68/19.05 % (845681)Instructions burned: 869 (million) % 132.68/19.05 % (845689)dis+21_1_sil=32000:sas=cadical:random_seed=1354396477:i=3773:amm=off_2983 on theBenchmark for (2983ds/3773Mi) % 132.68/19.05 % (845674)Instruction limit reached! % 132.68/19.05 % (845674)------------------------------ % 132.68/19.05 % (845674)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 132.68/19.05 % (845674)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 132.68/19.05 % (845674)CaDiCaL version: 2.1.3 % 132.68/19.05 % (845674)Termination reason: Instruction limit % 132.68/19.05 % (845674)Termination phase: Saturation % 132.68/19.05 % (845674)Time elapsed: 1.061 s % 132.68/19.05 % (845674)Peak memory usage: 15 MB % 132.68/19.05 % (845674)Instructions burned: 1473 (million) % 132.68/19.05 % (845693)ott+11_1_sil=16000:gs=on:random_seed=542848973:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2981 on theBenchmark for (2981ds/2251Mi) % 132.68/19.05 % (845673)Instruction limit reached! % 132.68/19.05 % (845673)------------------------------ % 132.68/19.05 % (845673)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 132.68/19.05 % (845673)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 132.68/19.05 % (845673)CaDiCaL version: 2.1.3 % 132.68/19.05 % (845673)Termination reason: Instruction limit % 132.68/19.05 % (845673)Termination phase: Saturation % 132.68/19.05 % (845673)Time elapsed: 1.942 s % 132.68/19.05 % (845673)Peak memory usage: 15 MB % 132.68/19.05 % (845673)Instructions burned: 5132 (million) % 132.68/19.05 % (845698)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=1326794745:fmbsr=1.6:i=67534_2972 on theBenchmark for (2972ds/67534Mi) % 132.68/19.05 % (845698)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 132.68/19.05 % (845698)Terminated due to inappropriate strategy. % 132.68/19.05 % (845698)------------------------------ % 132.68/19.05 % (845698)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 132.68/19.05 % (845698)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 132.68/19.05 % (845698)CaDiCaL version: 2.1.3 % 132.68/19.05 % (845698)Termination reason: Inappropriate % 132.68/19.05 % (845698)Time elapsed: 0.050 s % 132.68/19.05 % (845698)Peak memory usage: 10 MB % 132.68/19.05 % (845698)Instructions burned: 118 (million) % 132.68/19.05 % (845698)------------------------------ % 132.68/19.05 % (845698)------------------------------ % 132.68/19.05 % (845700)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=1604557792:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2971 on theBenchmark for (2971ds/4591Mi) % 132.68/19.05 % (845693)Instruction limit reached! % 132.68/19.05 % (845693)------------------------------ % 132.68/19.05 % (845693)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 132.68/19.05 % (845693)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 132.68/19.05 % (845693)CaDiCaL version: 2.1.3 % 132.68/19.05 % (845693)Termination reason: Instruction limit % 132.68/19.05 % (845693)Termination phase: Saturation % 132.68/19.05 % (845693)Time elapsed: 1.504 s % 132.68/19.05 % (845693)Peak memory usage: 15 MB % 132.68/19.05 % (845693)Instructions burned: 2251 (million) % 132.68/19.05 % (845706)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=2046014014:i=29340_2965 on theBenchmark for (2965ds/29340Mi) % 132.68/19.05 % (845687)Instruction limit reached! % 132.68/19.05 % (845687)------------------------------ % 132.68/19.05 % (845687)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 132.68/19.05 % (845687)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 132.68/19.05 % (845687)CaDiCaL version: 2.1.3 % 132.68/19.05 % (845687)Termination reason: Instruction limit % 132.68/19.05 % (845687)Termination phase: Saturation % 132.68/19.05 % (845687)Time elapsed: 2.299 s % 132.68/19.05 % (845687)Peak memory usage: 15 MB % 132.68/19.05 % (845687)Instructions burned: 3512 (million) % 132.68/19.05 % (845708)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=3826056686:i=5211_2964 on theBenchmark for (2964ds/5211Mi) % 154.05/22.12 % (845689)Instruction limit reached! % 154.05/22.12 % (845689)------------------------------ % 154.05/22.12 % (845689)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 154.05/22.12 % (845689)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 154.05/22.12 % (845689)CaDiCaL version: 2.1.3 % 154.05/22.12 % (845689)Termination reason: Instruction limit % 154.05/22.12 % (845689)Termination phase: Saturation % 154.05/22.12 % (845689)Time elapsed: 2.765 s % 154.05/22.12 % (845689)Peak memory usage: 15 MB % 154.05/22.12 % (845689)Instructions burned: 3774 (million) % 154.05/22.12 % (845710)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=4276014325:i=5497:nm=2_2955 on theBenchmark for (2955ds/5497Mi) % 154.05/22.12 % (845710)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 154.05/22.12 % (845710)Terminated due to inappropriate strategy. % 154.05/22.12 % (845710)------------------------------ % 154.05/22.12 % (845710)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 154.05/22.12 % (845710)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 154.05/22.12 % (845710)CaDiCaL version: 2.1.3 % 154.05/22.12 % (845710)Termination reason: Inappropriate % 154.05/22.12 % (845710)Time elapsed: 0.058 s % 154.05/22.12 % (845710)Peak memory usage: 11 MB % 154.05/22.12 % (845710)Instructions burned: 118 (million) % 154.05/22.12 % (845710)------------------------------ % 154.05/22.12 % (845710)------------------------------ % 154.05/22.12 % (845712)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=3098481633:fmbsr=2:i=46332_2955 on theBenchmark for (2955ds/46332Mi) % 154.05/22.12 % (845712)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 154.05/22.12 % (845712)Terminated due to inappropriate strategy. % 154.05/22.12 % (845712)------------------------------ % 154.05/22.12 % (845712)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 154.05/22.12 % (845712)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 154.05/22.12 % (845712)CaDiCaL version: 2.1.3 % 154.05/22.12 % (845712)Termination reason: Inappropriate % 154.05/22.12 % (845712)Time elapsed: 0.096 s % 154.05/22.12 % (845712)Peak memory usage: 10 MB % 154.05/22.12 % (845712)Instructions burned: 118 (million) % 154.05/22.12 % (845712)------------------------------ % 154.05/22.12 % (845712)------------------------------ % 154.05/22.12 % (845682)Instruction limit reached! % 154.05/22.12 % (845682)------------------------------ % 154.05/22.12 % (845682)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 154.05/22.12 % (845682)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 154.05/22.12 % (845682)CaDiCaL version: 2.1.3 % 154.05/22.12 % (845682)Termination reason: Instruction limit % 154.05/22.12 % (845682)Termination phase: Saturation % 154.05/22.12 % (845682)Time elapsed: 3.633 s % 154.05/22.12 % (845682)Peak memory usage: 15 MB % 154.05/22.12 % (845682)Instructions burned: 5115 (million) % 154.05/22.12 % (845718)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=1005839837:i=14071_2953 on theBenchmark for (2953ds/14071Mi) % 154.05/22.12 % (845719)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1746883786:i=22565:add=on:rawr=on_2953 on theBenchmark for (2953ds/22565Mi) % 154.05/22.12 % (845718)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 154.05/22.12 % (845718)Terminated due to inappropriate strategy. % 154.05/22.12 % (845718)------------------------------ % 154.05/22.12 % (845718)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 154.05/22.12 % (845718)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 154.05/22.12 % (845718)CaDiCaL version: 2.1.3 % 154.05/22.12 % (845718)Termination reason: Inappropriate % 154.05/22.12 % (845718)Time elapsed: 0.096 s % 154.05/22.12 % (845718)Peak memory usage: 10 MB % 154.05/22.12 % (845718)Instructions burned: 118 (million) % 154.05/22.12 % (845718)------------------------------ % 154.05/22.12 % (845718)------------------------------ % 154.05/22.12 % (845722)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=2122703641:i=8173:av=off_2952 on theBenchmark for (2952ds/8173Mi) % 154.05/22.12 % (845700)Instruction limit reached! % 154.05/22.12 % (845700)------------------------------ % 154.05/22.12 % (845700)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 154.05/22.12 % (845700)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 154.05/22.12 % (845700)CaDiCaL version: 2.1.3 % 154.05/22.12 % (845700)Termination reason: Instruction limit % 154.05/22.12 % (845700)Termination phase: Saturation % 165.06/23.68 % (845700)Time elapsed: 2.201 s % 165.06/23.68 % (845700)Peak memory usage: 44 MB % 165.06/23.68 % (845700)Instructions burned: 4594 (million) % 165.06/23.68 % (845724)dis+10_16:1_sil=16000:random_seed=160455034:i=9155:fsr=off_2949 on theBenchmark for (2949ds/9155Mi) % 165.06/23.68 % (845708)Instruction limit reached! % 165.06/23.68 % (845708)------------------------------ % 165.06/23.68 % (845708)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 165.06/23.68 % (845708)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 165.06/23.68 % (845708)CaDiCaL version: 2.1.3 % 165.06/23.68 % (845708)Termination reason: Instruction limit % 165.06/23.68 % (845708)Termination phase: Saturation % 165.06/23.68 % (845708)Time elapsed: 3.804 s % 165.06/23.68 % (845708)Peak memory usage: 17 MB % 165.06/23.68 % (845708)Instructions burned: 5211 (million) % 165.06/23.68 % (845736)ott-3_8_sil=64000:random_seed=1641270586:i=20139:bs=on_2926 on theBenchmark for (2926ds/20139Mi) % 165.06/23.68 % (845724)Instruction limit reached! % 165.06/23.68 % (845724)------------------------------ % 165.06/23.68 % (845724)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 165.06/23.68 % (845724)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 165.06/23.68 % (845724)CaDiCaL version: 2.1.3 % 165.06/23.68 % (845724)Termination reason: Instruction limit % 165.06/23.68 % (845724)Termination phase: Saturation % 165.06/23.68 % (845724)Time elapsed: 3.417 s % 165.06/23.68 % (845724)Peak memory usage: 16 MB % 165.06/23.68 % (845724)Instructions burned: 9157 (million) % 165.06/23.68 % (845738)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=23829933:fmbsr=2:i=32576_2914 on theBenchmark for (2914ds/32576Mi) % 165.06/23.68 % (845738)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 165.06/23.68 % (845738)Terminated due to inappropriate strategy. % 165.06/23.68 % (845738)------------------------------ % 165.06/23.68 % (845738)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 165.06/23.68 % (845738)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 165.06/23.68 % (845738)CaDiCaL version: 2.1.3 % 165.06/23.68 % (845738)Termination reason: Inappropriate % 165.06/23.68 % (845738)Time elapsed: 0.054 s % 165.06/23.68 % (845738)Peak memory usage: 11 MB % 165.06/23.68 % (845738)Instructions burned: 118 (million) % 165.06/23.68 % (845738)------------------------------ % 165.06/23.68 % (845738)------------------------------ % 165.06/23.68 % (845740)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=2070946209:i=11404_2914 on theBenchmark for (2914ds/11404Mi) % 165.06/23.68 % (845722)Instruction limit reached! % 165.06/23.68 % (845722)------------------------------ % 165.06/23.68 % (845722)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 165.06/23.68 % (845722)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 165.06/23.68 % (845722)CaDiCaL version: 2.1.3 % 165.06/23.68 % (845722)Termination reason: Instruction limit % 165.06/23.68 % (845722)Termination phase: Saturation % 165.06/23.68 % (845722)Time elapsed: 5.802 s % 165.06/23.68 % (845722)Peak memory usage: 16 MB % 165.06/23.68 % (845722)Instructions burned: 8174 (million) % 165.06/23.68 % (845742)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=31837526:i=14134_2894 on theBenchmark for (2894ds/14134Mi) % 165.06/23.68 % (845740)Instruction limit reached! % 165.06/23.68 % (845740)------------------------------ % 165.06/23.68 % (845740)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 165.06/23.68 % (845740)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 165.06/23.68 % (845740)CaDiCaL version: 2.1.3 % 165.06/23.68 % (845740)Termination reason: Instruction limit % 165.06/23.68 % (845740)Termination phase: Saturation % 165.06/23.68 % (845740)Time elapsed: 4.197 s % 165.06/23.68 % (845740)Peak memory usage: 16 MB % 165.06/23.68 % (845740)Instructions burned: 11405 (million) % 165.06/23.68 % (845744)dis+33_16_sil=32000:sac=on:random_seed=3191235196:i=15851:nm=0_2871 on theBenchmark for (2871ds/15851Mi) % 165.06/23.68 % (845744)Instruction limit reached! % 165.06/23.68 % (845744)------------------------------ % 165.06/23.68 % (845744)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 165.06/23.68 % (845744)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 165.06/23.68 % (845744)CaDiCaL version: 2.1.3 % 165.06/23.68 % (845744)Termination reason: Instruction limit % 165.06/23.68 % (845744)Termination phase: Saturation % 165.06/23.68 % (845744)Time elapsed: 5.919 s % 165.06/23.68 % (845744)Peak memory usage: 20 MB % 165.06/23.68 % (845744)Instructions burned: 15853 (million) % 165.06/23.68 % (845760)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=2408583583:avsq=on:i=17627:add=on:amm=off_2812 on theBenchmark for (2812ds/17627Mi) % 188.38/26.98 % (845719)Instruction limit reached! % 188.38/26.98 % (845719)------------------------------ % 188.38/26.98 % (845719)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 188.38/26.98 % (845719)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 188.38/26.98 % (845719)CaDiCaL version: 2.1.3 % 188.38/26.98 % (845719)Termination reason: Instruction limit % 188.38/26.98 % (845719)Termination phase: Saturation % 188.38/26.98 % (845719)Time elapsed: 15.291 s % 188.38/26.98 % (845719)Peak memory usage: 17 MB % 188.38/26.98 % (845719)Instructions burned: 22566 (million) % 188.38/26.98 % (845762)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=4012235988:s2a=on:i=53295_2800 on theBenchmark for (2800ds/53295Mi) % 188.38/26.98 % (845742)Instruction limit reached! % 188.38/26.98 % (845742)------------------------------ % 188.38/26.98 % (845742)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 188.38/26.98 % (845742)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 188.38/26.98 % (845742)CaDiCaL version: 2.1.3 % 188.38/26.98 % (845742)Termination reason: Instruction limit % 188.38/26.98 % (845742)Termination phase: Saturation % 188.38/26.98 % (845742)Time elapsed: 10.006 s % 188.38/26.98 % (845742)Peak memory usage: 16 MB % 188.38/26.98 % (845742)Instructions burned: 14135 (million) % 188.38/26.98 % (845764)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=2262684294:i=26857:ins=20_2793 on theBenchmark for (2793ds/26857Mi) % 188.38/26.98 % (845764)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 188.38/26.98 % (845764)Terminated due to inappropriate strategy. % 188.38/26.98 % (845764)------------------------------ % 188.38/26.98 % (845764)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 188.38/26.98 % (845764)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 188.38/26.98 % (845764)CaDiCaL version: 2.1.3 % 188.38/26.98 % (845764)Termination reason: Inappropriate % 188.38/26.98 % (845764)Time elapsed: 0.057 s % 188.38/26.98 % (845764)Peak memory usage: 11 MB % 188.38/26.98 % (845764)Instructions burned: 118 (million) % 188.38/26.98 % (845764)------------------------------ % 188.38/26.98 % (845764)------------------------------ % 188.38/26.98 % (845766)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=2955159402:i=28120:bs=on:fsr=off_2792 on theBenchmark for (2792ds/28120Mi) % 188.38/26.98 % (845736)Instruction limit reached! % 188.38/26.98 % (845736)------------------------------ % 188.38/26.98 % (845736)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 188.38/26.98 % (845736)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 188.38/26.98 % (845736)CaDiCaL version: 2.1.3 % 188.38/26.98 % (845736)Termination reason: Instruction limit % 188.38/26.98 % (845736)Termination phase: Saturation % 188.38/26.98 % (845736)Time elapsed: 14.152 s % 188.38/26.98 % (845736)Peak memory usage: 18 MB % 188.38/26.98 % (845736)Instructions burned: 20140 (million) % 188.38/26.98 % (845768)fmb+10_1_sil=256000:fmbss=7:random_seed=1730250100:fmbsr=1.6:i=182295_2784 on theBenchmark for (2784ds/182295Mi) % 188.38/26.98 % (845768)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 188.38/26.98 % (845768)Terminated due to inappropriate strategy. % 188.38/26.98 % (845768)------------------------------ % 188.38/26.98 % (845768)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 188.38/26.98 % (845768)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 188.38/26.98 % (845768)CaDiCaL version: 2.1.3 % 188.38/26.98 % (845768)Termination reason: Inappropriate % 188.38/26.98 % (845768)Time elapsed: 0.096 s % 188.38/26.98 % (845768)Peak memory usage: 10 MB % 188.38/26.98 % (845768)Instructions burned: 118 (million) % 188.38/26.98 % (845768)------------------------------ % 188.38/26.98 % (845768)------------------------------ % 188.38/26.98 % (845770)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=2204836533:i=44625:gsp=on_2783 on theBenchmark for (2783ds/44625Mi) % 188.38/26.98 % (845770)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 188.38/26.98 % (845770)Terminated due to inappropriate strategy. % 188.38/26.98 % (845770)------------------------------ % 188.38/26.98 % (845770)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 188.38/26.98 % (845770)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 188.38/26.98 % (845770)CaDiCaL version: 2.1.3 % 188.38/26.98 % (845770)Termination reason: Inappropriate % 200.91/28.79 % (845770)Time elapsed: 0.100 s % 200.91/28.79 % (845770)Peak memory usage: 11 MB % 200.91/28.79 % (845770)Instructions burned: 118 (million) % 200.91/28.79 % (845770)------------------------------ % 200.91/28.79 % (845770)------------------------------ % 200.91/28.79 % (845772)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=28437441:i=160505_2781 on theBenchmark for (2781ds/160505Mi) % 200.91/28.79 % (845772)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 200.91/28.79 % (845772)Terminated due to inappropriate strategy. % 200.91/28.79 % (845772)------------------------------ % 200.91/28.79 % (845772)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 200.91/28.79 % (845772)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 200.91/28.79 % (845772)CaDiCaL version: 2.1.3 % 200.91/28.79 % (845772)Termination reason: Inappropriate % 200.91/28.79 % (845772)Time elapsed: 0.053 s % 200.91/28.79 % (845772)Peak memory usage: 11 MB % 200.91/28.79 % (845772)Instructions burned: 118 (million) % 200.91/28.79 % (845772)------------------------------ % 200.91/28.79 % (845772)------------------------------ % 200.91/28.79 % (845774)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=1398513494:fmbsr=1.3:i=225729_2780 on theBenchmark for (2780ds/225729Mi) % 200.91/28.79 % (845774)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 200.91/28.79 % (845774)Terminated due to inappropriate strategy. % 200.91/28.79 % (845774)------------------------------ % 200.91/28.79 % (845774)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 200.91/28.79 % (845774)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 200.91/28.79 % (845774)CaDiCaL version: 2.1.3 % 200.91/28.79 % (845774)Termination reason: Inappropriate % 200.91/28.79 % (845774)Time elapsed: 0.106 s % 200.91/28.79 % (845774)Peak memory usage: 10 MB % 200.91/28.79 % (845774)Instructions burned: 118 (million) % 200.91/28.79 % (845774)------------------------------ % 200.91/28.79 % (845774)------------------------------ % 200.91/28.79 % (845776)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=264140574:fmbsr=2:i=185024:ins=7_2779 on theBenchmark for (2779ds/185024Mi) % 200.91/28.79 % (845776)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 200.91/28.79 % (845776)Terminated due to inappropriate strategy. % 200.91/28.79 % (845776)------------------------------ % 200.91/28.79 % (845776)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 200.91/28.79 % (845776)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 200.91/28.79 % (845776)CaDiCaL version: 2.1.3 % 200.91/28.79 % (845776)Termination reason: Inappropriate % 200.91/28.79 % (845776)Time elapsed: 0.057 s % 200.91/28.79 % (845776)Peak memory usage: 10 MB % 200.91/28.79 % (845776)Instructions burned: 118 (million) % 200.91/28.79 % (845776)------------------------------ % 200.91/28.79 % (845776)------------------------------ % 200.91/28.79 % (845778)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=2311373310:rtra=on_2778 on theBenchmark for (2778ds/0Mi) % 200.91/28.79 % (845778)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 200.91/28.79 % (845778)Terminated due to inappropriate strategy. % 200.91/28.79 % (845778)------------------------------ % 200.91/28.79 % (845778)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 200.91/28.79 % (845778)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 200.91/28.79 % (845778)CaDiCaL version: 2.1.3 % 200.91/28.79 % (845778)Termination reason: Inappropriate % 200.91/28.79 % (845778)Time elapsed: 0.096 s % 200.91/28.79 % (845778)Peak memory usage: 10 MB % 200.91/28.79 % (845778)Instructions burned: 118 (million) % 200.91/28.79 % (845778)------------------------------ % 200.91/28.79 % (845778)------------------------------ % 200.91/28.79 % (845782)% WARNING: option uhcvi not known. % 200.91/28.79 % (845782)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2620804576:i=271062:add=off:rtra=on:rawr=on_2777 on theBenchmark for (2777ds/271062Mi) % 200.91/28.79 % (845706)Instruction limit reached! % 200.91/28.79 % (845706)------------------------------ % 200.91/28.79 % (845706)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 200.91/28.79 % (845706)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 200.91/28.79 % (845706)CaDiCaL version: 2.1.3 % 200.91/28.79 % (845706)Termination reason: Instruction limit % 200.91/28.79 % (845706)Termination phase: Saturation % 200.91/28.79 % (845706)Time elapsed: 19.951 s % 200.91/28.79 % (845706)Peak memory usage: 16 MB % 200.91/28.79 % (845706)Instructions burned: 29340 (million) % 206.92/29.56 % (845786)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3806846905:i=176048:add=on:rtra=on:rawr=on_2766 on theBenchmark for (2766ds/176048Mi) % 206.92/29.56 % (845760)Instruction limit reached! % 206.92/29.56 % (845760)------------------------------ % 206.92/29.56 % (845760)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 206.92/29.56 % (845760)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 206.92/29.56 % (845760)CaDiCaL version: 2.1.3 % 206.92/29.56 % (845760)Termination reason: Instruction limit % 206.92/29.56 % (845760)Termination phase: Saturation % 206.92/29.56 % (845760)Time elapsed: 7.254 s % 206.92/29.56 % (845760)Peak memory usage: 115 MB % 206.92/29.56 % (845760)Instructions burned: 17627 (million) % 206.92/29.56 % (845788)dis+10_1_sil=32000:si=on:sp=arity:random_seed=882543642:i=206:fgj=on:rtra=on_2739 on theBenchmark for (2739ds/206Mi) % 206.92/29.56 % (845788)Instruction limit reached! % 206.92/29.56 % (845788)------------------------------ % 206.92/29.56 % (845788)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 206.92/29.56 % (845788)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 206.92/29.56 % (845788)CaDiCaL version: 2.1.3 % 206.92/29.56 % (845788)Termination reason: Instruction limit % 206.92/29.56 % (845788)Termination phase: Saturation % 206.92/29.56 % (845788)Time elapsed: 0.109 s % 206.92/29.56 % (845788)Peak memory usage: 13 MB % 206.92/29.56 % (845788)Instructions burned: 206 (million) % 206.92/29.56 % (845790)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=1359845737:i=232:rtra=on_2738 on theBenchmark for (2738ds/232Mi) % 206.92/29.56 % (845790)Instruction limit reached! % 206.92/29.56 % (845790)------------------------------ % 206.92/29.56 % (845790)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 206.92/29.56 % (845790)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 206.92/29.56 % (845790)CaDiCaL version: 2.1.3 % 206.92/29.56 % (845790)Termination reason: Instruction limit % 206.92/29.56 % (845790)Termination phase: Saturation % 206.92/29.56 % (845790)Time elapsed: 0.099 s % 206.92/29.56 % (845790)Peak memory usage: 13 MB % 206.92/29.56 % (845790)Instructions burned: 234 (million) % 206.92/29.56 % (845792)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=2051703825:i=262:rtra=on_2737 on theBenchmark for (2737ds/262Mi) % 206.92/29.56 % (845792)Instruction limit reached! % 206.92/29.56 % (845792)------------------------------ % 206.92/29.56 % (845792)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 206.92/29.56 % (845792)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 206.92/29.56 % (845792)CaDiCaL version: 2.1.3 % 206.92/29.56 % (845792)Termination reason: Instruction limit % 206.92/29.56 % (845792)Termination phase: Saturation % 206.92/29.56 % (845792)Time elapsed: 0.148 s % 206.92/29.56 % (845792)Peak memory usage: 12 MB % 206.92/29.56 % (845792)Instructions burned: 264 (million) % 206.92/29.56 % (845798)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=1910956309:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2735 on theBenchmark for (2735ds/318Mi) % 206.92/29.56 % (845798)Instruction limit reached! % 206.92/29.56 % (845798)------------------------------ % 206.92/29.56 % (845798)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 206.92/29.56 % (845798)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 206.92/29.56 % (845798)CaDiCaL version: 2.1.3 % 206.92/29.56 % (845798)Termination reason: Instruction limit % 206.92/29.56 % (845798)Termination phase: Saturation % 206.92/29.56 % (845798)Time elapsed: 0.135 s % 206.92/29.56 % (845798)Peak memory usage: 14 MB % 206.92/29.56 % (845798)Instructions burned: 318 (million) % 206.92/29.56 % (845800)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=2225234759:i=1428:nm=2:rtra=on_2733 on theBenchmark for (2733ds/1428Mi) % 206.92/29.56 % (845800)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 206.92/29.56 % (845800)Terminated due to inappropriate strategy. % 206.92/29.56 % (845800)------------------------------ % 206.92/29.56 % (845800)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 206.92/29.56 % (845800)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 206.92/29.56 % (845800)CaDiCaL version: 2.1.3 % 206.92/29.56 % (845800)Termination reason: Inappropriate % 206.92/29.56 % (845800)Time elapsed: 0.050 s % 206.92/29.56 % (845800)Peak memory usage: 10 MB % 206.92/29.56 % (845800)Instructions burned: 118 (million) % 229.31/32.72 % (845800)------------------------------ % 229.31/32.72 % (845800)------------------------------ % 229.31/32.72 % (845802)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=3218772177:i=262:bd=preordered:rtra=on:fsd=on_2733 on theBenchmark for (2733ds/262Mi) % 229.31/32.72 % (845802)Instruction limit reached! % 229.31/32.72 % (845802)------------------------------ % 229.31/32.72 % (845802)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 229.31/32.72 % (845802)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 229.31/32.72 % (845802)CaDiCaL version: 2.1.3 % 229.31/32.72 % (845802)Termination reason: Instruction limit % 229.31/32.72 % (845802)Termination phase: Saturation % 229.31/32.72 % (845802)Time elapsed: 0.118 s % 229.31/32.72 % (845802)Peak memory usage: 13 MB % 229.31/32.72 % (845802)Instructions burned: 263 (million) % 229.31/32.72 % (845804)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=967037935:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2731 on theBenchmark for (2731ds/1368Mi) % 229.31/32.72 % (845804)Instruction limit reached! % 229.31/32.72 % (845804)------------------------------ % 229.31/32.72 % (845804)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 229.31/32.72 % (845804)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 229.31/32.72 % (845804)CaDiCaL version: 2.1.3 % 229.31/32.72 % (845804)Termination reason: Instruction limit % 229.31/32.72 % (845804)Termination phase: Saturation % 229.31/32.72 % (845804)Time elapsed: 0.543 s % 229.31/32.72 % (845804)Peak memory usage: 16 MB % 229.31/32.72 % (845804)Instructions burned: 1369 (million) % 229.31/32.72 % (845806)ott-21_1_sil=16000:si=on:fs=off:random_seed=971155668:i=360:av=off:fsr=off:rtra=on_2726 on theBenchmark for (2726ds/360Mi) % 229.31/32.72 % (845806)Instruction limit reached! % 229.31/32.72 % (845806)------------------------------ % 229.31/32.72 % (845806)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 229.31/32.72 % (845806)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 229.31/32.72 % (845806)CaDiCaL version: 2.1.3 % 229.31/32.72 % (845806)Termination reason: Instruction limit % 229.31/32.72 % (845806)Termination phase: Saturation % 229.31/32.72 % (845806)Time elapsed: 0.140 s % 229.31/32.72 % (845806)Peak memory usage: 12 MB % 229.31/32.72 % (845806)Instructions burned: 362 (million) % 229.31/32.72 % (845808)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=694444810:i=954:bd=all:rtra=on_2724 on theBenchmark for (2724ds/954Mi) % 229.31/32.72 % (845808)Instruction limit reached! % 229.31/32.72 % (845808)------------------------------ % 229.31/32.72 % (845808)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 229.31/32.72 % (845808)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 229.31/32.72 % (845808)CaDiCaL version: 2.1.3 % 229.31/32.72 % (845808)Termination reason: Instruction limit % 229.31/32.72 % (845808)Termination phase: Saturation % 229.31/32.72 % (845808)Time elapsed: 0.362 s % 229.31/32.72 % (845808)Peak memory usage: 14 MB % 229.31/32.72 % (845808)Instructions burned: 956 (million) % 229.31/32.72 % (845817)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=3991119725:fmbsr=1.3:i=1730:ins=25:rtra=on_2720 on theBenchmark for (2720ds/1730Mi) % 229.31/32.72 % (845817)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 229.31/32.72 % (845817)Terminated due to inappropriate strategy. % 229.31/32.72 % (845817)------------------------------ % 229.31/32.72 % (845817)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 229.31/32.72 % (845817)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 229.31/32.72 % (845817)CaDiCaL version: 2.1.3 % 229.31/32.72 % (845817)Termination reason: Inappropriate % 229.31/32.72 % (845817)Time elapsed: 0.055 s % 229.31/32.72 % (845817)Peak memory usage: 10 MB % 229.31/32.72 % (845817)Instructions burned: 90 (million) % 229.31/32.72 % (845817)------------------------------ % 229.31/32.72 % (845817)------------------------------ % 229.31/32.72 % (845819)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=2141246836:i=2358:rtra=on_2719 on theBenchmark for (2719ds/2358Mi) % 229.31/32.72 % (845819)Instruction limit reached! % 229.31/32.72 % (845819)------------------------------ % 229.31/32.72 % (845819)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 229.31/32.72 % (845819)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 229.31/32.72 % (845819)CaDiCaL version: 2.1.3 % 229.31/32.72 % (845819)Termination reason: Instruction limit % 261.56/37.21 % (845819)Termination phase: Saturation % 261.56/37.21 % (845819)Time elapsed: 0.471 s % 261.56/37.21 % (845819)Peak memory usage: 12 MB % 261.56/37.21 % (845819)Instructions burned: 2360 (million) % 261.56/37.21 % (845860)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=476276598:i=1778:ins=1:rtra=on_2714 on theBenchmark for (2714ds/1778Mi) % 261.56/37.21 % (845860)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 261.56/37.21 % (845860)Terminated due to inappropriate strategy. % 261.56/37.21 % (845860)------------------------------ % 261.56/37.21 % (845860)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 261.56/37.21 % (845860)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 261.56/37.21 % (845860)CaDiCaL version: 2.1.3 % 261.56/37.21 % (845860)Termination reason: Inappropriate % 261.56/37.21 % (845860)Time elapsed: 0.018 s % 261.56/37.21 % (845860)Peak memory usage: 10 MB % 261.56/37.21 % (845860)Instructions burned: 90 (million) % 261.56/37.21 % (845860)------------------------------ % 261.56/37.21 % (845860)------------------------------ % 261.56/37.21 % (845862)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=574391440:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2714 on theBenchmark for (2714ds/1384Mi) % 261.56/37.21 % (845862)Instruction limit reached! % 261.56/37.21 % (845862)------------------------------ % 261.56/37.21 % (845862)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 261.56/37.21 % (845862)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 261.56/37.21 % (845862)CaDiCaL version: 2.1.3 % 261.56/37.21 % (845862)Termination reason: Instruction limit % 261.56/37.21 % (845862)Termination phase: Saturation % 261.56/37.21 % (845862)Time elapsed: 0.278 s % 261.56/37.21 % (845862)Peak memory usage: 14 MB % 261.56/37.21 % (845862)Instructions burned: 1386 (million) % 261.56/37.21 % (845864)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=116134464:i=1758:kws=inv_precedence:fsr=off:rtra=on_2711 on theBenchmark for (2711ds/1758Mi) % 261.56/37.21 % (845864)Instruction limit reached! % 261.56/37.21 % (845864)------------------------------ % 261.56/37.21 % (845864)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 261.56/37.21 % (845864)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 261.56/37.21 % (845864)CaDiCaL version: 2.1.3 % 261.56/37.21 % (845864)Termination reason: Instruction limit % 261.56/37.21 % (845864)Termination phase: Saturation % 261.56/37.21 % (845864)Time elapsed: 0.354 s % 261.56/37.21 % (845864)Peak memory usage: 14 MB % 261.56/37.21 % (845864)Instructions burned: 1760 (million) % 261.56/37.21 % (845866)fmb+10_1_sil=64000:si=on:random_seed=3973427229:i=44122:nm=2:rtra=on:gsp=on_2708 on theBenchmark for (2708ds/44122Mi) % 261.56/37.21 % (845866)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 261.56/37.21 % (845866)Terminated due to inappropriate strategy. % 261.56/37.21 % (845866)------------------------------ % 261.56/37.21 % (845866)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 261.56/37.21 % (845866)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 261.56/37.21 % (845866)CaDiCaL version: 2.1.3 % 261.56/37.21 % (845866)Termination reason: Inappropriate % 261.56/37.21 % (845866)Time elapsed: 0.024 s % 261.56/37.21 % (845866)Peak memory usage: 10 MB % 261.56/37.21 % (845866)Instructions burned: 118 (million) % 261.56/37.21 % (845866)------------------------------ % 261.56/37.21 % (845866)------------------------------ % 261.56/37.21 % (845868)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=1907630489:i=19030:nm=5:rtra=on_2707 on theBenchmark for (2707ds/19030Mi) % 261.56/37.21 % (845868)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 261.56/37.21 % (845868)Terminated due to inappropriate strategy. % 261.56/37.21 % (845868)------------------------------ % 261.56/37.21 % (845868)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 261.56/37.21 % (845868)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 261.56/37.21 % (845868)CaDiCaL version: 2.1.3 % 261.56/37.21 % (845868)Termination reason: Inappropriate % 261.56/37.21 % (845868)Time elapsed: 0.024 s % 261.56/37.21 % (845868)Peak memory usage: 10 MB % 261.56/37.21 % (845868)Instructions burned: 118 (million) % 261.56/37.21 % (845868)------------------------------ % 261.56/37.21 % (845868)------------------------------ % 261.56/37.21 % (845870)fmb+10_1_sil=64000:sas=cadical:si=on:fmbss=8:random_seed=2339303749:fmbsr=1.7:i=1840:rtra=on_2707 on theBenchmark for (2707ds/1840Mi) % 291.39/41.42 % (845870)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 291.39/41.42 % (845870)Terminated due to inappropriate strategy. % 291.39/41.42 % (845870)------------------------------ % 291.39/41.42 % (845870)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 291.39/41.42 % (845870)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 291.39/41.42 % (845870)CaDiCaL version: 2.1.3 % 291.39/41.42 % (845870)Termination reason: Inappropriate % 291.39/41.42 % (845870)Time elapsed: 0.024 s % 291.39/41.42 % (845870)Peak memory usage: 10 MB % 291.39/41.42 % (845870)Instructions burned: 118 (million) % 291.39/41.42 % (845870)------------------------------ % 291.39/41.42 % (845870)------------------------------ % 291.39/41.42 % (845872)dis-4_1_sil=16000:drc=ordering:si=on:sp=const_frequency:sac=on:newcnf=on:random_seed=3441679684:i=10262:rtra=on_2706 on theBenchmark for (2706ds/10262Mi) % 291.39/41.42 % (845872)Instruction limit reached! % 291.39/41.42 % (845872)------------------------------ % 291.39/41.42 % (845872)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 291.39/41.42 % (845872)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 291.39/41.42 % (845872)CaDiCaL version: 2.1.3 % 291.39/41.42 % (845872)Termination reason: Instruction limit % 291.39/41.42 % (845872)Termination phase: Saturation % 291.39/41.42 % (845872)Time elapsed: 2.085 s % 291.39/41.42 % (845872)Peak memory usage: 18 MB % 291.39/41.42 % (845872)Instructions burned: 10267 (million) % 291.39/41.42 % (845874)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:si=on:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2558038142:i=2944:ins=7:rtra=on:fdi=8:gsp=on_2686 on theBenchmark for (2686ds/2944Mi) % 291.39/41.42 % (845874)Instruction limit reached! % 291.39/41.42 % (845874)------------------------------ % 291.39/41.42 % (845874)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 291.39/41.42 % (845874)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 291.39/41.42 % (845874)CaDiCaL version: 2.1.3 % 291.39/41.42 % (845874)Termination reason: Instruction limit % 291.39/41.42 % (845874)Termination phase: Saturation % 291.39/41.42 % (845874)Time elapsed: 0.596 s % 291.39/41.42 % (845874)Peak memory usage: 15 MB % 291.39/41.42 % (845874)Instructions burned: 2947 (million) % 291.39/41.42 % (845876)fmb+10_1_sil=16000:sas=cadical:si=on:bce=on:fmbss=77:random_seed=1406468902:i=12648:rtra=on_2679 on theBenchmark for (2679ds/12648Mi) % 291.39/41.42 % (845876)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 291.39/41.42 % (845876)Terminated due to inappropriate strategy. % 291.39/41.42 % (845876)------------------------------ % 291.39/41.42 % (845876)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 291.39/41.42 % (845876)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 291.39/41.42 % (845876)CaDiCaL version: 2.1.3 % 291.39/41.42 % (845876)Termination reason: Inappropriate % 291.39/41.42 % (845876)Time elapsed: 0.024 s % 291.39/41.42 % (845876)Peak memory usage: 10 MB % 291.39/41.42 % (845876)Instructions burned: 118 (million) % 291.39/41.42 % (845876)------------------------------ % 291.39/41.42 % (845876)------------------------------ % 291.39/41.42 % (845878)fmb+10_1_fmbas=function:sil=32000:sas=cadical:si=on:fmbss=16:random_seed=234228798:fmbsr=2.30978:i=4348:rtra=on_2679 on theBenchmark for (2679ds/4348Mi) % 291.39/41.42 % (845878)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 291.39/41.42 % (845878)Terminated due to inappropriate strategy. % 291.39/41.42 % (845878)------------------------------ % 291.39/41.42 % (845878)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 291.39/41.42 % (845878)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 291.39/41.42 % (845878)CaDiCaL version: 2.1.3 % 291.39/41.42 % (845878)Termination reason: Inappropriate % 291.39/41.42 % (845878)Time elapsed: 0.024 s % 291.39/41.42 % (845878)Peak memory usage: 10 MB % 291.39/41.42 % (845878)Instructions burned: 118 (million) % 291.39/41.42 % (845878)------------------------------ % 291.39/41.42 % (845878)------------------------------ % 291.39/41.42 % (845880)ott-2_1_sil=16000:si=on:newcnf=on:random_seed=379938965:avsq=on:i=1738:avsqr=1,16:kws=inv_arity_squared:rtra=on_2679 on theBenchmark for (2679ds/1738Mi) % 291.39/41.42 % (845880)Instruction limit reached! % 291.39/41.42 % (845880)------------------------------ % 291.39/41.42 % (845880)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 291.39/41.42 % (845880)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.59/42.74 % (845880)CaDiCaL version: 2.1.3 % 300.59/42.74 % (845880)Termination reason: Instruction limit % 300.59/42.74 % (845880)Termination phase: Saturation % 300.59/42.74 % (845880)Time elapsed: 0.347 s % 300.59/42.74 % (845880)Peak memory usage: 13 MB % 300.59/42.74 % (845880)Instructions burned: 1740 (million) % 300.59/42.74 % (845882)ott+10_1_sil=32000:tgt=ground:si=on:random_seed=1666850911:i=10228:av=off:rtra=on_2675 on theBenchmark for (2675ds/10228Mi) % 300.59/42.74 % (845882)Instruction limit reached! % 300.59/42.74 % (845882)------------------------------ % 300.59/42.74 % (845882)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.59/42.74 % (845882)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.59/42.74 % (845882)CaDiCaL version: 2.1.3 % 300.59/42.74 % (845882)Termination reason: Instruction limit % 300.59/42.74 % (845882)Termination phase: Saturation % 300.59/42.74 % (845882)Time elapsed: 2.036 s % 300.59/42.74 % (845882)Peak memory usage: 18 MB % 300.59/42.74 % (845882)Instructions burned: 10231 (million) % 300.59/42.74 % (845884)fmb+10_1_sil=64000:sas=cadical:si=on:bce=on:rp=on:random_seed=4219819737:i=108564:rtra=on_2655 on theBenchmark for (2655ds/108564Mi) % 300.59/42.74 % (845884)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 300.59/42.74 % (845884)Terminated due to inappropriate strategy. % 300.59/42.74 % (845884)------------------------------ % 300.59/42.74 % (845884)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.59/42.74 % (845884)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.59/42.74 % (845884)CaDiCaL version: 2.1.3 % 300.59/42.74 % (845884)Termination reason: Inappropriate % 300.59/42.74 % (845884)Time elapsed: 0.024 s % 300.59/42.74 % (845884)Peak memory usage: 10 MB % 300.59/42.74 % (845884)Instructions burned: 118 (million) % 300.59/42.74 % (845884)------------------------------ % 300.59/42.74 % (845884)------------------------------ % 300.59/42.74 % (845886)dis-11_1_sil=16000:si=on:sp=reverse_frequency:alpa=true:random_seed=1934352810:i=7024:aac=none:rtra=on_2654 on theBenchmark for (2654ds/7024Mi) % 300.59/42.74 % (845766)Instruction limit reached! % 300.59/42.74 % (845766)------------------------------ % 300.59/42.74 % (845766)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.59/42.74 % (845766)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.59/42.74 % (845766)CaDiCaL version: 2.1.3 % 300.59/42.74 % (845766)Termination reason: Instruction limit % 300.59/42.74 % (845766)Termination phase: Saturation % 300.59/42.74 % (845766)Time elapsed: 13.907 s % 300.59/42.74 % (845766)Peak memory usage: 16 MB % 300.59/42.74 % (845766)Instructions burned: 28121 (million) % 300.59/42.74 % (845888)dis+21_1_sil=32000:sas=cadical:si=on:random_seed=1084203147:i=7546:rtra=on:amm=off_2653 on theBenchmark for (2653ds/7546Mi) % 300.59/42.74 % (845886)Instruction limit reached! % 300.59/42.74 % (845886)------------------------------ % 300.59/42.74 % (845886)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.59/42.74 % (845886)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.59/42.74 % (845886)CaDiCaL version: 2.1.3 % 300.59/42.74 % (845886)Termination reason: Instruction limit % 300.59/42.74 % (845886)Termination phase: Saturation % 300.59/42.74 % (845886)Time elapsed: 1.445 s % 300.59/42.74 % (845886)Peak memory usage: 18 MB % 300.59/42.74 % (845886)Instructions burned: 7026 (million) % 300.59/42.74 % (845890)ott+11_1_sil=16000:si=on:gs=on:random_seed=1118159634:s2a=on:i=4502:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:rtra=on:fsd=on_2640 on theBenchmark for (2640ds/4502Mi) % 300.59/42.74 % (845890)Instruction limit reached! % 300.59/42.74 % (845890)------------------------------ % 300.59/42.74 % (845890)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.59/42.74 % (845890)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.59/42.74 % (845890)CaDiCaL version: 2.1.3 % 300.59/42.74 % (845890)Termination reason: Instruction limit % 300.59/42.74 % (845890)Termination phase: Saturation % 300.59/42.74 % (845890)Time elapsed: 0.900 s % 300.59/42.74 % (845890)Peak memory usage: 17 MB % 300.59/42.74 % (845890)Instructions burned: 4507 (million) % 300.59/42.74 % (845892)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:si=on:fmbss=7:random_seed=1226283211:fmbsr=1.6:i=135068:rtra=on_2631 on theBenchmark for (2631ds/135068Mi) % 300.59/42.74 % (845892)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 300.59/42.74 % (845892)Terminated due to inappropriate strategy. % 300.59/42.74 % (845892)--------- % 300.59/42.74 Terminated % 300.59/42.74 % Vampire exiting %------------------------------------------------------------------------------