%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : PRO033_1 : TPTP v9.3.1. Released v9.0.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % Computer : n019.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 29 12:30:43 PM UTC 2026 % Result : Timeout 300.44s 42.74s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : PRO033_1 : TPTP v9.3.1. Released v9.0.0. % 0.00/0.04 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.08/0.35 % Computer : n019.cluster.edu % 0.08/0.35 % Model : x86_64 x86_64 % 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.08/0.35 % Memory : 8046.5625MB % 0.08/0.35 % OS : Linux 6.8.0-71-generic % 0.08/0.35 % CPULimit : 300 % 0.08/0.35 % WCLimit : 300 % 0.08/0.35 % DateTime : Sun Sep 27 22:27:18 UTC 2026 % 0.08/0.36 % CPUTime : % 0.08/0.36 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.14/0.41 Running first-order model finding % 0.14/0.41 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 5.55/1.25 % (3474634)Will run a generic schedule for satisfiability detection. % 5.55/1.25 % (3474645)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3513461379:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_3000 on theBenchmark for (3000ds/159Mi) % 5.55/1.25 % (3474639)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2214607119_3000 on theBenchmark for (3000ds/0Mi) % 5.55/1.25 % (3474639)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 5.55/1.25 % (3474639)Terminated due to inappropriate strategy. % 5.55/1.25 % (3474639)------------------------------ % 5.55/1.25 % (3474639)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.55/1.25 % (3474639)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.55/1.25 % (3474639)CaDiCaL version: 2.1.3 % 5.55/1.25 % (3474639)Termination reason: Inappropriate % 5.55/1.25 % (3474639)Time elapsed: 0.0000 s % 5.55/1.25 % (3474639)Peak memory usage: 10 MB % 5.55/1.25 % (3474639)------------------------------ % 5.55/1.25 % (3474639)------------------------------ % 5.55/1.25 % (3474640)% WARNING: option uhcvi not known. % 5.55/1.25 % (3474640)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=485597988:i=135531:add=off:rawr=on_3000 on theBenchmark for (3000ds/135531Mi) % 5.55/1.25 % (3474642)dis+10_1_sil=32000:sp=arity:random_seed=2681844968:i=103:fgj=on_3000 on theBenchmark for (3000ds/103Mi) % 5.55/1.25 % (3474643)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=601435908:i=116_3000 on theBenchmark for (3000ds/116Mi) % 5.55/1.25 % (3474641)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=727265754:i=88024:add=on:rawr=on_3000 on theBenchmark for (3000ds/88024Mi) % 5.55/1.25 % (3474644)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2773595017:i=131_3000 on theBenchmark for (3000ds/131Mi) % 5.55/1.25 % (3474648)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=872586420:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 5.55/1.25 % (3474648)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 5.55/1.25 % (3474648)Terminated due to inappropriate strategy. % 5.55/1.25 % (3474648)------------------------------ % 5.55/1.25 % (3474648)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.55/1.25 % (3474648)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.55/1.25 % (3474648)CaDiCaL version: 2.1.3 % 5.55/1.25 % (3474648)Termination reason: Inappropriate % 5.55/1.25 % (3474648)Time elapsed: 0.001 s % 5.55/1.25 % (3474648)Peak memory usage: 10 MB % 5.55/1.25 % (3474648)------------------------------ % 5.55/1.25 % (3474648)------------------------------ % 5.55/1.25 % (3474655)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=213658731:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 5.55/1.25 % (3474645)Instruction limit reached! % 5.55/1.25 % (3474645)------------------------------ % 5.55/1.25 % (3474645)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.55/1.25 % (3474645)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.55/1.25 % (3474645)CaDiCaL version: 2.1.3 % 5.55/1.25 % (3474645)Termination reason: Instruction limit % 5.55/1.25 % (3474645)Termination phase: Saturation % 5.55/1.25 % (3474645)Time elapsed: 0.083 s % 5.55/1.25 % (3474645)Peak memory usage: 12 MB % 5.55/1.25 % (3474645)Instructions burned: 160 (million) % 5.55/1.25 % (3474657)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=2574338094:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi) % 5.55/1.25 % (3474643)Instruction limit reached! % 5.55/1.25 % (3474643)------------------------------ % 5.55/1.25 % (3474643)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.55/1.25 % (3474643)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.55/1.25 % (3474643)CaDiCaL version: 2.1.3 % 5.55/1.25 % (3474643)Termination reason: Instruction limit % 5.55/1.25 % (3474643)Termination phase: Saturation % 5.55/1.25 % (3474643)Time elapsed: 0.111 s % 5.55/1.25 % (3474643)Peak memory usage: 12 MB % 5.55/1.25 % (3474643)Instructions burned: 116 (million) % 5.55/1.25 % (3474642)Instruction limit reached! % 5.55/1.25 % (3474642)------------------------------ % 5.55/1.25 % (3474642)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.55/1.25 % (3474642)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.23/2.15 % (3474642)CaDiCaL version: 2.1.3 % 12.23/2.15 % (3474642)Termination reason: Instruction limit % 12.23/2.15 % (3474642)Termination phase: Saturation % 12.23/2.15 % (3474642)Time elapsed: 0.112 s % 12.23/2.15 % (3474642)Peak memory usage: 12 MB % 12.23/2.15 % (3474642)Instructions burned: 103 (million) % 12.23/2.15 % (3474644)Instruction limit reached! % 12.23/2.15 % (3474644)------------------------------ % 12.23/2.15 % (3474644)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 12.23/2.15 % (3474644)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.23/2.15 % (3474644)CaDiCaL version: 2.1.3 % 12.23/2.15 % (3474644)Termination reason: Instruction limit % 12.23/2.15 % (3474644)Termination phase: Saturation % 12.23/2.15 % (3474644)Time elapsed: 0.131 s % 12.23/2.15 % (3474644)Peak memory usage: 12 MB % 12.23/2.15 % (3474644)Instructions burned: 131 (million) % 12.23/2.15 % (3474659)ott-21_1_sil=16000:fs=off:random_seed=3716989943:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 12.23/2.15 % (3474660)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=363966826:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 12.23/2.15 % (3474655)Instruction limit reached! % 12.23/2.15 % (3474655)------------------------------ % 12.23/2.15 % (3474655)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 12.23/2.15 % (3474655)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.23/2.15 % (3474655)CaDiCaL version: 2.1.3 % 12.23/2.15 % (3474655)Termination reason: Instruction limit % 12.23/2.15 % (3474655)Termination phase: Saturation % 12.23/2.15 % (3474655)Time elapsed: 0.106 s % 12.23/2.15 % (3474655)Peak memory usage: 12 MB % 12.23/2.15 % (3474655)Instructions burned: 131 (million) % 12.23/2.15 % (3474661)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=963915600:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 12.23/2.15 % (3474661)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 12.23/2.15 % (3474661)Terminated due to inappropriate strategy. % 12.23/2.15 % (3474661)------------------------------ % 12.23/2.15 % (3474661)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 12.23/2.15 % (3474661)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.23/2.15 % (3474661)CaDiCaL version: 2.1.3 % 12.23/2.15 % (3474661)Termination reason: Inappropriate % 12.23/2.15 % (3474661)Time elapsed: 0.0000 s % 12.23/2.15 % (3474661)Peak memory usage: 10 MB % 12.23/2.15 % (3474661)------------------------------ % 12.23/2.15 % (3474661)------------------------------ % 12.23/2.15 % (3474664)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=253310696:i=1179_2998 on theBenchmark for (2998ds/1179Mi) % 12.23/2.15 % (3474666)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3700198067:i=889:ins=1_2997 on theBenchmark for (2997ds/889Mi) % 12.23/2.15 % (3474666)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 12.23/2.15 % (3474666)Terminated due to inappropriate strategy. % 12.23/2.15 % (3474666)------------------------------ % 12.23/2.15 % (3474666)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 12.23/2.15 % (3474666)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.23/2.15 % (3474666)CaDiCaL version: 2.1.3 % 12.23/2.15 % (3474666)Termination reason: Inappropriate % 12.23/2.15 % (3474666)Time elapsed: 0.001 s % 12.23/2.15 % (3474666)Peak memory usage: 10 MB % 12.23/2.15 % (3474666)------------------------------ % 12.23/2.15 % (3474666)------------------------------ % 12.23/2.15 % (3474669)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=2841977324: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) % 12.23/2.15 % (3474659)Instruction limit reached! % 12.23/2.15 % (3474659)------------------------------ % 12.23/2.15 % (3474659)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 12.23/2.15 % (3474659)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.23/2.15 % (3474659)CaDiCaL version: 2.1.3 % 12.23/2.15 % (3474659)Termination reason: Instruction limit % 12.23/2.15 % (3474659)Termination phase: Saturation % 12.23/2.15 % (3474659)Time elapsed: 0.114 s % 12.23/2.15 % (3474659)Peak memory usage: 11 MB % 12.23/2.15 % (3474659)Instructions burned: 180 (million) % 12.23/2.15 % (3474671)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3436060321:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi) % 35.40/5.47 % (3474660)Instruction limit reached! % 35.40/5.47 % (3474660)------------------------------ % 35.40/5.47 % (3474660)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 35.40/5.47 % (3474660)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 35.40/5.47 % (3474660)CaDiCaL version: 2.1.3 % 35.40/5.47 % (3474660)Termination reason: Instruction limit % 35.40/5.47 % (3474660)Termination phase: Saturation % 35.40/5.47 % (3474660)Time elapsed: 0.498 s % 35.40/5.47 % (3474660)Peak memory usage: 14 MB % 35.40/5.47 % (3474660)Instructions burned: 477 (million) % 35.40/5.47 % (3474673)fmb+10_1_sil=64000:random_seed=1849645380:i=22061:nm=2:gsp=on_2993 on theBenchmark for (2993ds/22061Mi) % 35.40/5.47 % (3474673)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 35.40/5.47 % (3474673)Terminated due to inappropriate strategy. % 35.40/5.47 % (3474673)------------------------------ % 35.40/5.47 % (3474673)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 35.40/5.47 % (3474673)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 35.40/5.47 % (3474673)CaDiCaL version: 2.1.3 % 35.40/5.47 % (3474673)Termination reason: Inappropriate % 35.40/5.47 % (3474673)Time elapsed: 0.004 s % 35.40/5.47 % (3474673)Peak memory usage: 10 MB % 35.40/5.47 % (3474673)------------------------------ % 35.40/5.47 % (3474673)------------------------------ % 35.40/5.47 % (3474675)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1284902931:i=9515:nm=5_2992 on theBenchmark for (2992ds/9515Mi) % 35.40/5.47 % (3474675)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 35.40/5.47 % (3474675)Terminated due to inappropriate strategy. % 35.40/5.47 % (3474675)------------------------------ % 35.40/5.47 % (3474675)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 35.40/5.47 % (3474675)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 35.40/5.47 % (3474675)CaDiCaL version: 2.1.3 % 35.40/5.47 % (3474675)Termination reason: Inappropriate % 35.40/5.47 % (3474675)Time elapsed: 0.001 s % 35.40/5.47 % (3474675)Peak memory usage: 10 MB % 35.40/5.47 % (3474675)------------------------------ % 35.40/5.47 % (3474675)------------------------------ % 35.40/5.47 % (3474677)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1862150299:fmbsr=1.7:i=920_2992 on theBenchmark for (2992ds/920Mi) % 35.40/5.47 % (3474677)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 35.40/5.47 % (3474677)Terminated due to inappropriate strategy. % 35.40/5.47 % (3474677)------------------------------ % 35.40/5.47 % (3474677)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 35.40/5.47 % (3474677)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 35.40/5.47 % (3474677)CaDiCaL version: 2.1.3 % 35.40/5.47 % (3474677)Termination reason: Inappropriate % 35.40/5.47 % (3474677)Time elapsed: 0.001 s % 35.40/5.47 % (3474677)Peak memory usage: 10 MB % 35.40/5.47 % (3474677)------------------------------ % 35.40/5.47 % (3474677)------------------------------ % 35.40/5.47 % (3474664)Instruction limit reached! % 35.40/5.47 % (3474664)------------------------------ % 35.40/5.47 % (3474664)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 35.40/5.47 % (3474664)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 35.40/5.47 % (3474664)CaDiCaL version: 2.1.3 % 35.40/5.47 % (3474664)Termination reason: Instruction limit % 35.40/5.47 % (3474664)Termination phase: Saturation % 35.40/5.47 % (3474664)Time elapsed: 0.589 s % 35.40/5.47 % (3474664)Peak memory usage: 17 MB % 35.40/5.47 % (3474664)Instructions burned: 1180 (million) % 35.40/5.47 % (3474657)Instruction limit reached! % 35.40/5.47 % (3474657)------------------------------ % 35.40/5.47 % (3474657)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 35.40/5.47 % (3474657)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 35.40/5.47 % (3474657)CaDiCaL version: 2.1.3 % 35.40/5.47 % (3474657)Termination reason: Instruction limit % 35.40/5.47 % (3474657)Termination phase: Saturation % 35.40/5.47 % (3474657)Time elapsed: 0.678 s % 35.40/5.47 % (3474657)Peak memory usage: 16 MB % 35.40/5.47 % (3474657)Instructions burned: 684 (million) % 35.40/5.47 % (3474679)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=479177694:i=5131_2992 on theBenchmark for (2992ds/5131Mi) % 35.40/5.47 % (3474680)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=777685550:i=1472:ins=7:fdi=8:gsp=on_2991 on theBenchmark for (2991ds/1472Mi) % 65.29/9.61 % (3474669)Instruction limit reached! % 65.29/9.61 % (3474669)------------------------------ % 65.29/9.61 % (3474669)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 65.29/9.61 % (3474669)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 65.29/9.61 % (3474669)CaDiCaL version: 2.1.3 % 65.29/9.61 % (3474669)Termination reason: Instruction limit % 65.29/9.61 % (3474669)Termination phase: Saturation % 65.29/9.61 % (3474669)Time elapsed: 0.564 s % 65.29/9.61 % (3474669)Peak memory usage: 16 MB % 65.29/9.61 % (3474669)Instructions burned: 692 (million) % 65.29/9.61 % (3474681)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=99385561:i=6324_2991 on theBenchmark for (2991ds/6324Mi) % 65.29/9.61 % (3474681)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 65.29/9.61 % (3474681)Terminated due to inappropriate strategy. % 65.29/9.61 % (3474681)------------------------------ % 65.29/9.61 % (3474681)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 65.29/9.61 % (3474681)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 65.29/9.61 % (3474681)CaDiCaL version: 2.1.3 % 65.29/9.61 % (3474681)Termination reason: Inappropriate % 65.29/9.61 % (3474681)Time elapsed: 0.0000 s % 65.29/9.61 % (3474681)Peak memory usage: 10 MB % 65.29/9.61 % (3474681)------------------------------ % 65.29/9.61 % (3474681)------------------------------ % 65.29/9.61 % (3474686)ott-2_1_sil=16000:newcnf=on:random_seed=2863470077:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2991 on theBenchmark for (2991ds/869Mi) % 65.29/9.61 % (3474684)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=509739155:fmbsr=2.30978:i=2174_2991 on theBenchmark for (2991ds/2174Mi) % 65.29/9.61 % (3474684)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 65.29/9.61 % (3474684)Terminated due to inappropriate strategy. % 65.29/9.61 % (3474684)------------------------------ % 65.29/9.61 % (3474684)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 65.29/9.61 % (3474684)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 65.29/9.61 % (3474684)CaDiCaL version: 2.1.3 % 65.29/9.61 % (3474684)Termination reason: Inappropriate % 65.29/9.61 % (3474684)Time elapsed: 0.001 s % 65.29/9.61 % (3474684)Peak memory usage: 10 MB % 65.29/9.61 % (3474684)------------------------------ % 65.29/9.61 % (3474684)------------------------------ % 65.29/9.61 % (3474689)ott+10_1_sil=32000:tgt=ground:random_seed=1227948779:i=5114:av=off_2991 on theBenchmark for (2991ds/5114Mi) % 65.29/9.61 % (3474671)Instruction limit reached! % 65.29/9.61 % (3474671)------------------------------ % 65.29/9.61 % (3474671)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 65.29/9.61 % (3474671)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 65.29/9.61 % (3474671)CaDiCaL version: 2.1.3 % 65.29/9.61 % (3474671)Termination reason: Instruction limit % 65.29/9.61 % (3474671)Termination phase: Saturation % 65.29/9.61 % (3474671)Time elapsed: 0.775 s % 65.29/9.61 % (3474671)Peak memory usage: 19 MB % 65.29/9.61 % (3474671)Instructions burned: 881 (million) % 65.29/9.61 % (3474692)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=472935207:i=54282_2989 on theBenchmark for (2989ds/54282Mi) % 65.29/9.61 % (3474692)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 65.29/9.61 % (3474692)Terminated due to inappropriate strategy. % 65.29/9.61 % (3474692)------------------------------ % 65.29/9.61 % (3474692)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 65.29/9.61 % (3474692)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 65.29/9.61 % (3474692)CaDiCaL version: 2.1.3 % 65.29/9.61 % (3474692)Termination reason: Inappropriate % 65.29/9.61 % (3474692)Time elapsed: 0.001 s % 65.29/9.61 % (3474692)Peak memory usage: 10 MB % 65.29/9.61 % (3474692)------------------------------ % 65.29/9.61 % (3474692)------------------------------ % 65.29/9.61 % (3474694)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=913382383:i=3512:aac=none_2988 on theBenchmark for (2988ds/3512Mi) % 65.29/9.61 % (3474686)Instruction limit reached! % 65.29/9.61 % (3474686)------------------------------ % 65.29/9.61 % (3474686)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 65.29/9.61 % (3474686)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 160.97/23.12 % (3474686)CaDiCaL version: 2.1.3 % 160.97/23.12 % (3474686)Termination reason: Instruction limit % 160.97/23.12 % (3474686)Termination phase: Saturation % 160.97/23.12 % (3474686)Time elapsed: 0.865 s % 160.97/23.12 % (3474686)Peak memory usage: 16 MB % 160.97/23.12 % (3474686)Instructions burned: 870 (million) % 160.97/23.12 % (3474697)dis+21_1_sil=32000:sas=cadical:random_seed=1974577514:i=3773:amm=off_2982 on theBenchmark for (2982ds/3773Mi) % 160.97/23.12 % (3474680)Instruction limit reached! % 160.97/23.12 % (3474680)------------------------------ % 160.97/23.12 % (3474680)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 160.97/23.12 % (3474680)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 160.97/23.12 % (3474680)CaDiCaL version: 2.1.3 % 160.97/23.12 % (3474680)Termination reason: Instruction limit % 160.97/23.12 % (3474680)Termination phase: Saturation % 160.97/23.12 % (3474680)Time elapsed: 1.343 s % 160.97/23.12 % (3474680)Peak memory usage: 22 MB % 160.97/23.12 % (3474680)Instructions burned: 1472 (million) % 160.97/23.12 % (3474701)ott+11_1_sil=16000:gs=on:random_seed=3023891082:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2978 on theBenchmark for (2978ds/2251Mi) % 160.97/23.12 % (3474679)Instruction limit reached! % 160.97/23.12 % (3474679)------------------------------ % 160.97/23.12 % (3474679)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 160.97/23.12 % (3474679)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 160.97/23.12 % (3474679)CaDiCaL version: 2.1.3 % 160.97/23.12 % (3474679)Termination reason: Instruction limit % 160.97/23.12 % (3474679)Termination phase: Saturation % 160.97/23.12 % (3474679)Time elapsed: 2.401 s % 160.97/23.12 % (3474679)Peak memory usage: 40 MB % 160.97/23.12 % (3474679)Instructions burned: 5133 (million) % 160.97/23.12 % (3474707)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=830906284:fmbsr=1.6:i=67534_2967 on theBenchmark for (2967ds/67534Mi) % 160.97/23.12 % (3474707)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 160.97/23.12 % (3474707)Terminated due to inappropriate strategy. % 160.97/23.12 % (3474707)------------------------------ % 160.97/23.12 % (3474707)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 160.97/23.12 % (3474707)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 160.97/23.12 % (3474707)CaDiCaL version: 2.1.3 % 160.97/23.12 % (3474707)Termination reason: Inappropriate % 160.97/23.12 % (3474707)Time elapsed: 0.0000 s % 160.97/23.12 % (3474707)Peak memory usage: 10 MB % 160.97/23.12 % (3474707)------------------------------ % 160.97/23.12 % (3474707)------------------------------ % 160.97/23.12 % (3474710)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=1120536968:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2967 on theBenchmark for (2967ds/4591Mi) % 160.97/23.12 % (3474694)Instruction limit reached! % 160.97/23.12 % (3474694)------------------------------ % 160.97/23.12 % (3474694)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 160.97/23.12 % (3474694)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 160.97/23.12 % (3474694)CaDiCaL version: 2.1.3 % 160.97/23.12 % (3474694)Termination reason: Instruction limit % 160.97/23.12 % (3474694)Termination phase: Saturation % 160.97/23.12 % (3474694)Time elapsed: 3.143 s % 160.97/23.12 % (3474694)Peak memory usage: 28 MB % 160.97/23.12 % (3474694)Instructions burned: 3512 (million) % 160.97/23.12 % (3474715)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=702458883:i=29340_2957 on theBenchmark for (2957ds/29340Mi) % 160.97/23.12 % (3474701)Instruction limit reached! % 160.97/23.12 % (3474701)------------------------------ % 160.97/23.12 % (3474701)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 160.97/23.12 % (3474701)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 160.97/23.12 % (3474701)CaDiCaL version: 2.1.3 % 160.97/23.12 % (3474701)Termination reason: Instruction limit % 160.97/23.12 % (3474701)Termination phase: Saturation % 160.97/23.12 % (3474701)Time elapsed: 2.190 s % 160.97/23.12 % (3474701)Peak memory usage: 22 MB % 160.97/23.12 % (3474701)Instructions burned: 2251 (million) % 160.97/23.12 % (3474717)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=1561873098:i=5211_2956 on theBenchmark for (2956ds/5211Mi) % 160.97/23.12 % (3474697)Instruction limit reached! % 160.97/23.12 % (3474697)------------------------------ % 160.97/23.12 % (3474697)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 160.97/23.12 % (3474697)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 172.77/28.14 % (3474697)CaDiCaL version: 2.1.3 % 172.77/28.14 % (3474697)Termination reason: Instruction limit % 172.77/28.14 % (3474697)Termination phase: Saturation % 172.77/28.14 % (3474697)Time elapsed: 3.298 s % 172.77/28.14 % (3474697)Peak memory usage: 29 MB % 172.77/28.14 % (3474697)Instructions burned: 3774 (million) % 172.77/28.14 % (3474721)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=3162961197:i=5497:nm=2_2949 on theBenchmark for (2949ds/5497Mi) % 172.77/28.14 % (3474721)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 172.77/28.14 % (3474721)Terminated due to inappropriate strategy. % 172.77/28.14 % (3474721)------------------------------ % 172.77/28.14 % (3474721)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 172.77/28.14 % (3474721)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 172.77/28.14 % (3474721)CaDiCaL version: 2.1.3 % 172.77/28.14 % (3474721)Termination reason: Inappropriate % 172.77/28.14 % (3474721)Time elapsed: 0.0000 s % 172.77/28.14 % (3474721)Peak memory usage: 10 MB % 172.77/28.14 % (3474721)------------------------------ % 172.77/28.14 % (3474721)------------------------------ % 172.77/28.14 % (3474723)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=4124739526:fmbsr=2:i=46332_2949 on theBenchmark for (2949ds/46332Mi) % 172.77/28.14 % (3474723)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 172.77/28.14 % (3474723)Terminated due to inappropriate strategy. % 172.77/28.14 % (3474723)------------------------------ % 172.77/28.14 % (3474723)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 172.77/28.14 % (3474723)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 172.77/28.14 % (3474723)CaDiCaL version: 2.1.3 % 172.77/28.14 % (3474723)Termination reason: Inappropriate % 172.77/28.14 % (3474723)Time elapsed: 0.001 s % 172.77/28.14 % (3474723)Peak memory usage: 10 MB % 172.77/28.14 % (3474723)------------------------------ % 172.77/28.14 % (3474723)------------------------------ % 172.77/28.14 % (3474725)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=2562024870:i=14071_2948 on theBenchmark for (2948ds/14071Mi) % 172.77/28.14 % (3474725)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 172.77/28.14 % (3474725)Terminated due to inappropriate strategy. % 172.77/28.14 % (3474725)------------------------------ % 172.77/28.14 % (3474725)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 172.77/28.14 % (3474725)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 172.77/28.14 % (3474725)CaDiCaL version: 2.1.3 % 172.77/28.14 % (3474725)Termination reason: Inappropriate % 172.77/28.14 % (3474725)Time elapsed: 0.0000 s % 172.77/28.14 % (3474725)Peak memory usage: 10 MB % 172.77/28.14 % (3474725)------------------------------ % 172.77/28.14 % (3474725)------------------------------ % 172.77/28.14 % (3474728)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1405976850:i=22565:add=on:rawr=on_2948 on theBenchmark for (2948ds/22565Mi) % 172.77/28.14 % (3474710)Instruction limit reached! % 172.77/28.14 % (3474710)------------------------------ % 172.77/28.14 % (3474710)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 172.77/28.14 % (3474710)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 172.77/28.14 % (3474710)CaDiCaL version: 2.1.3 % 172.77/28.14 % (3474710)Termination reason: Instruction limit % 172.77/28.14 % (3474710)Termination phase: Saturation % 172.77/28.14 % (3474710)Time elapsed: 2.335 s % 172.77/28.14 % (3474710)Peak memory usage: 44 MB % 172.77/28.14 % (3474710)Instructions burned: 4592 (million) % 172.77/28.14 % (3474731)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=2753872971:i=8173:av=off_2943 on theBenchmark for (2943ds/8173Mi) % 172.77/28.14 % (3474689)Instruction limit reached! % 172.77/28.14 % (3474689)------------------------------ % 172.77/28.14 % (3474689)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 172.77/28.14 % (3474689)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 172.77/28.14 % (3474689)CaDiCaL version: 2.1.3 % 172.77/28.14 % (3474689)Termination reason: Instruction limit % 172.77/28.14 % (3474689)Termination phase: Saturation % 172.77/28.14 % (3474689)Time elapsed: 5.124 s % 172.77/28.14 % (3474689)Peak memory usage: 29 MB % 172.77/28.14 % (3474689)Instructions burned: 5114 (million) % 172.77/28.14 % (3474734)dis+10_16:1_sil=16000:random_seed=1290377346:i=9155:fsr=off_2939 on theBenchmark for (2939ds/9155Mi) % 230.91/32.93 % (3474717)Instruction limit reached! % 230.91/32.93 % (3474717)------------------------------ % 230.91/32.93 % (3474717)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 230.91/32.93 % (3474717)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 230.91/32.93 % (3474717)CaDiCaL version: 2.1.3 % 230.91/32.93 % (3474717)Termination reason: Instruction limit % 230.91/32.93 % (3474717)Termination phase: Saturation % 230.91/32.93 % (3474717)Time elapsed: 4.766 s % 230.91/32.93 % (3474717)Peak memory usage: 49 MB % 230.91/32.93 % (3474717)Instructions burned: 5212 (million) % 230.91/32.93 % (3474763)ott-3_8_sil=64000:random_seed=3502863662:i=20139:bs=on_2908 on theBenchmark for (2908ds/20139Mi) % 230.91/32.93 % (3474731)Instruction limit reached! % 230.91/32.93 % (3474731)------------------------------ % 230.91/32.93 % (3474731)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 230.91/32.93 % (3474731)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 230.91/32.93 % (3474731)CaDiCaL version: 2.1.3 % 230.91/32.93 % (3474731)Termination reason: Instruction limit % 230.91/32.93 % (3474731)Termination phase: Saturation % 230.91/32.93 % (3474731)Time elapsed: 4.342 s % 230.91/32.93 % (3474731)Peak memory usage: 45 MB % 230.91/32.93 % (3474731)Instructions burned: 8173 (million) % 230.91/32.93 % (3474776)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=3128535416:fmbsr=2:i=32576_2900 on theBenchmark for (2900ds/32576Mi) % 230.91/32.93 % (3474776)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 230.91/32.93 % (3474776)Terminated due to inappropriate strategy. % 230.91/32.93 % (3474776)------------------------------ % 230.91/32.93 % (3474776)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 230.91/32.93 % (3474776)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 230.91/32.93 % (3474776)CaDiCaL version: 2.1.3 % 230.91/32.93 % (3474776)Termination reason: Inappropriate % 230.91/32.93 % (3474776)Time elapsed: 0.001 s % 230.91/32.93 % (3474776)Peak memory usage: 10 MB % 230.91/32.93 % (3474776)------------------------------ % 230.91/32.93 % (3474776)------------------------------ % 230.91/32.93 % (3474778)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=984388775:i=11404_2899 on theBenchmark for (2899ds/11404Mi) % 230.91/32.93 % (3474734)Instruction limit reached! % 230.91/32.93 % (3474734)------------------------------ % 230.91/32.93 % (3474734)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 230.91/32.93 % (3474734)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 230.91/32.93 % (3474734)CaDiCaL version: 2.1.3 % 230.91/32.93 % (3474734)Termination reason: Instruction limit % 230.91/32.93 % (3474734)Termination phase: Saturation % 230.91/32.93 % (3474734)Time elapsed: 8.231 s % 230.91/32.93 % (3474734)Peak memory usage: 50 MB % 230.91/32.93 % (3474734)Instructions burned: 9155 (million) % 230.91/32.93 % (3474825)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=2057262841:i=14134_2856 on theBenchmark for (2856ds/14134Mi) % 230.91/32.93 % (3474778)Instruction limit reached! % 230.91/32.93 % (3474778)------------------------------ % 230.91/32.93 % (3474778)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 230.91/32.93 % (3474778)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 230.91/32.93 % (3474778)CaDiCaL version: 2.1.3 % 230.91/32.93 % (3474778)Termination reason: Instruction limit % 230.91/32.93 % (3474778)Termination phase: Saturation % 230.91/32.93 % (3474778)Time elapsed: 6.240 s % 230.91/32.93 % (3474778)Peak memory usage: 44 MB % 230.91/32.93 % (3474778)Instructions burned: 11405 (million) % 230.91/32.93 % (3474843)dis+33_16_sil=32000:sac=on:random_seed=386115026:i=15851:nm=0_2837 on theBenchmark for (2837ds/15851Mi) % 230.91/32.93 % (3474728)Instruction limit reached! % 230.91/32.93 % (3474728)------------------------------ % 230.91/32.93 % (3474728)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 230.91/32.93 % (3474728)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 230.91/32.93 % (3474728)CaDiCaL version: 2.1.3 % 230.91/32.93 % (3474728)Termination reason: Instruction limit % 230.91/32.93 % (3474728)Termination phase: Saturation % 230.91/32.93 % (3474728)Time elapsed: 15.224 s % 230.91/32.93 % (3474728)Peak memory usage: 202 MB % 230.91/32.93 % (3474728)Instructions burned: 22565 (million) % 230.91/32.93 % (3474879)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=1287766580:avsq=on:i=17627:add=on:amm=off_2795 on theBenchmark for (2795ds/17627Mi) % 230.91/32.93 % (3474843)Instruction limit reached! % 230.91/32.93 % (3474843)------------------------------ % 230.91/32.93 % (3474843)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 237.22/33.90 % (3474843)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 237.22/33.90 % (3474843)CaDiCaL version: 2.1.3 % 237.22/33.90 % (3474843)Termination reason: Instruction limit % 237.22/33.90 % (3474843)Termination phase: Saturation % 237.22/33.90 % (3474843)Time elapsed: 6.404 s % 237.22/33.90 % (3474843)Peak memory usage: 25 MB % 237.22/33.90 % (3474843)Instructions burned: 15853 (million) % 237.22/33.90 % (3474903)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=180868157:s2a=on:i=53295_2772 on theBenchmark for (2772ds/53295Mi) % 237.22/33.90 % (3474763)Instruction limit reached! % 237.22/33.90 % (3474763)------------------------------ % 237.22/33.90 % (3474763)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 237.22/33.90 % (3474763)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 237.22/33.90 % (3474763)CaDiCaL version: 2.1.3 % 237.22/33.90 % (3474763)Termination reason: Instruction limit % 237.22/33.90 % (3474763)Termination phase: Saturation % 237.22/33.90 % (3474763)Time elapsed: 17.019 s % 237.22/33.90 % (3474763)Peak memory usage: 42 MB % 237.22/33.90 % (3474763)Instructions burned: 20139 (million) % 237.22/33.90 % (3474931)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=3953366926:i=26857:ins=20_2737 on theBenchmark for (2737ds/26857Mi) % 237.22/33.90 % (3474931)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 237.22/33.90 % (3474931)Terminated due to inappropriate strategy. % 237.22/33.90 % (3474931)------------------------------ % 237.22/33.90 % (3474931)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 237.22/33.90 % (3474931)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 237.22/33.90 % (3474931)CaDiCaL version: 2.1.3 % 237.22/33.90 % (3474931)Termination reason: Inappropriate % 237.22/33.90 % (3474931)Time elapsed: 0.0000 s % 237.22/33.90 % (3474931)Peak memory usage: 10 MB % 237.22/33.90 % (3474931)------------------------------ % 237.22/33.90 % (3474931)------------------------------ % 237.22/33.90 % (3474933)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=1958258513:i=28120:bs=on:fsr=off_2737 on theBenchmark for (2737ds/28120Mi) % 237.22/33.90 % (3474715)Instruction limit reached! % 237.22/33.90 % (3474715)------------------------------ % 237.22/33.90 % (3474715)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 237.22/33.90 % (3474715)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 237.22/33.90 % (3474715)CaDiCaL version: 2.1.3 % 237.22/33.90 % (3474715)Termination reason: Instruction limit % 237.22/33.90 % (3474715)Termination phase: Saturation % 237.22/33.90 % (3474715)Time elapsed: 23.297 s % 237.22/33.90 % (3474715)Peak memory usage: 134 MB % 237.22/33.90 % (3474715)Instructions burned: 29341 (million) % 237.22/33.90 % (3474941)fmb+10_1_sil=256000:fmbss=7:random_seed=747935111:fmbsr=1.6:i=182295_2723 on theBenchmark for (2723ds/182295Mi) % 237.22/33.90 % (3474941)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 237.22/33.90 % (3474941)Terminated due to inappropriate strategy. % 237.22/33.90 % (3474941)------------------------------ % 237.22/33.90 % (3474941)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 237.22/33.90 % (3474941)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 237.22/33.90 % (3474941)CaDiCaL version: 2.1.3 % 237.22/33.90 % (3474941)Termination reason: Inappropriate % 237.22/33.90 % (3474941)Time elapsed: 0.001 s % 237.22/33.90 % (3474941)Peak memory usage: 10 MB % 237.22/33.90 % (3474941)------------------------------ % 237.22/33.90 % (3474941)------------------------------ % 237.22/33.90 % (3474943)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=3825907432:i=44625:gsp=on_2723 on theBenchmark for (2723ds/44625Mi) % 237.22/33.90 % (3474943)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 237.22/33.90 % (3474943)Terminated due to inappropriate strategy. % 237.22/33.90 % (3474943)------------------------------ % 237.22/33.90 % (3474943)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 237.22/33.90 % (3474943)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 237.22/33.90 % (3474943)CaDiCaL version: 2.1.3 % 237.22/33.90 % (3474943)Termination reason: Inappropriate % 237.22/33.90 % (3474943)Time elapsed: 0.001 s % 237.22/33.90 % (3474943)Peak memory usage: 10 MB % 237.22/33.90 % (3474943)------------------------------ % 237.22/33.90 % (3474943)------------------------------ % 237.22/33.90 % (3474945)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=4152047649:i=160505_2723 on theBenchmark for (2723ds/160505Mi) % 259.30/37.03 % (3474945)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 259.30/37.03 % (3474945)Terminated due to inappropriate strategy. % 259.30/37.03 % (3474945)------------------------------ % 259.30/37.03 % (3474945)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 259.30/37.03 % (3474945)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 259.30/37.03 % (3474945)CaDiCaL version: 2.1.3 % 259.30/37.03 % (3474945)Termination reason: Inappropriate % 259.30/37.03 % (3474945)Time elapsed: 0.0000 s % 259.30/37.03 % (3474945)Peak memory usage: 10 MB % 259.30/37.03 % (3474945)------------------------------ % 259.30/37.03 % (3474945)------------------------------ % 259.30/37.03 % (3474947)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=1245519011:fmbsr=1.3:i=225729_2722 on theBenchmark for (2722ds/225729Mi) % 259.30/37.03 % (3474947)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 259.30/37.03 % (3474947)Terminated due to inappropriate strategy. % 259.30/37.03 % (3474947)------------------------------ % 259.30/37.03 % (3474947)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 259.30/37.03 % (3474947)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 259.30/37.03 % (3474947)CaDiCaL version: 2.1.3 % 259.30/37.03 % (3474947)Termination reason: Inappropriate % 259.30/37.03 % (3474947)Time elapsed: 0.001 s % 259.30/37.03 % (3474947)Peak memory usage: 10 MB % 259.30/37.03 % (3474947)------------------------------ % 259.30/37.03 % (3474947)------------------------------ % 259.30/37.03 % (3474949)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=3949636150:fmbsr=2:i=185024:ins=7_2722 on theBenchmark for (2722ds/185024Mi) % 259.30/37.03 % (3474949)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 259.30/37.03 % (3474949)Terminated due to inappropriate strategy. % 259.30/37.03 % (3474949)------------------------------ % 259.30/37.03 % (3474949)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 259.30/37.03 % (3474949)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 259.30/37.03 % (3474949)CaDiCaL version: 2.1.3 % 259.30/37.03 % (3474949)Termination reason: Inappropriate % 259.30/37.03 % (3474949)Time elapsed: 0.001 s % 259.30/37.03 % (3474949)Peak memory usage: 10 MB % 259.30/37.03 % (3474949)------------------------------ % 259.30/37.03 % (3474949)------------------------------ % 259.30/37.03 % (3474951)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=3550977082:rtra=on_2722 on theBenchmark for (2722ds/0Mi) % 259.30/37.03 % (3474951)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 259.30/37.03 % (3474951)Terminated due to inappropriate strategy. % 259.30/37.03 % (3474951)------------------------------ % 259.30/37.03 % (3474951)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 259.30/37.03 % (3474951)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 259.30/37.03 % (3474951)CaDiCaL version: 2.1.3 % 259.30/37.03 % (3474951)Termination reason: Inappropriate % 259.30/37.03 % (3474951)Time elapsed: 0.001 s % 259.30/37.03 % (3474951)Peak memory usage: 10 MB % 259.30/37.03 % (3474951)------------------------------ % 259.30/37.03 % (3474951)------------------------------ % 259.30/37.03 % (3474953)% WARNING: option uhcvi not known. % 259.30/37.03 % (3474953)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3902595888:i=271062:add=off:rtra=on:rawr=on_2721 on theBenchmark for (2721ds/271062Mi) % 259.30/37.03 % (3474825)Instruction limit reached! % 259.30/37.03 % (3474825)------------------------------ % 259.30/37.03 % (3474825)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 259.30/37.03 % (3474825)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 259.30/37.03 % (3474825)CaDiCaL version: 2.1.3 % 259.30/37.03 % (3474825)Termination reason: Instruction limit % 259.30/37.03 % (3474825)Termination phase: Saturation % 259.30/37.03 % (3474825)Time elapsed: 14.353 s % 259.30/37.03 % (3474825)Peak memory usage: 64 MB % 259.30/37.03 % (3474825)Instructions burned: 14134 (million) % 259.30/37.03 % (3474973)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2143708847:i=176048:add=on:rtra=on:rawr=on_2713 on theBenchmark for (2713ds/176048Mi) % 259.30/37.03 % (3474879)Instruction limit reached! % 259.30/37.03 % (3474879)------------------------------ % 259.30/37.03 % (3474879)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 265.52/37.97 % (3474879)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 265.52/37.97 % (3474879)CaDiCaL version: 2.1.3 % 265.52/37.97 % (3474879)Termination reason: Instruction limit % 265.52/37.97 % (3474879)Termination phase: Saturation % 265.52/37.97 % (3474879)Time elapsed: 12.042 s % 265.52/37.97 % (3474879)Peak memory usage: 194 MB % 265.52/37.97 % (3474879)Instructions burned: 17628 (million) % 265.52/37.97 % (3475001)dis+10_1_sil=32000:si=on:sp=arity:random_seed=3445026193:i=206:fgj=on:rtra=on_2674 on theBenchmark for (2674ds/206Mi) % 265.52/37.97 % (3475001)Instruction limit reached! % 265.52/37.97 % (3475001)------------------------------ % 265.52/37.97 % (3475001)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 265.52/37.97 % (3475001)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 265.52/37.97 % (3475001)CaDiCaL version: 2.1.3 % 265.52/37.97 % (3475001)Termination reason: Instruction limit % 265.52/37.97 % (3475001)Termination phase: Saturation % 265.52/37.97 % (3475001)Time elapsed: 0.127 s % 265.52/37.97 % (3475001)Peak memory usage: 13 MB % 265.52/37.97 % (3475001)Instructions burned: 206 (million) % 265.52/37.97 % (3475003)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=2272373694:i=232:rtra=on_2673 on theBenchmark for (2673ds/232Mi) % 265.52/37.97 % (3475003)Instruction limit reached! % 265.52/37.97 % (3475003)------------------------------ % 265.52/37.97 % (3475003)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 265.52/37.97 % (3475003)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 265.52/37.97 % (3475003)CaDiCaL version: 2.1.3 % 265.52/37.97 % (3475003)Termination reason: Instruction limit % 265.52/37.97 % (3475003)Termination phase: Saturation % 265.52/37.97 % (3475003)Time elapsed: 0.148 s % 265.52/37.97 % (3475003)Peak memory usage: 13 MB % 265.52/37.97 % (3475003)Instructions burned: 233 (million) % 265.52/37.97 % (3475005)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=177968233:i=262:rtra=on_2671 on theBenchmark for (2671ds/262Mi) % 265.52/37.97 % (3475005)Instruction limit reached! % 265.52/37.97 % (3475005)------------------------------ % 265.52/37.97 % (3475005)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 265.52/37.97 % (3475005)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 265.52/37.97 % (3475005)CaDiCaL version: 2.1.3 % 265.52/37.97 % (3475005)Termination reason: Instruction limit % 265.52/37.97 % (3475005)Termination phase: Saturation % 265.52/37.97 % (3475005)Time elapsed: 0.164 s % 265.52/37.97 % (3475005)Peak memory usage: 13 MB % 265.52/37.97 % (3475005)Instructions burned: 262 (million) % 265.52/37.97 % (3475007)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=1614557798:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2669 on theBenchmark for (2669ds/318Mi) % 265.52/37.97 % (3475007)Instruction limit reached! % 265.52/37.97 % (3475007)------------------------------ % 265.52/37.97 % (3475007)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 265.52/37.97 % (3475007)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 265.52/37.97 % (3475007)CaDiCaL version: 2.1.3 % 265.52/37.97 % (3475007)Termination reason: Instruction limit % 265.52/37.97 % (3475007)Termination phase: Saturation % 265.52/37.97 % (3475007)Time elapsed: 0.199 s % 265.52/37.97 % (3475007)Peak memory usage: 14 MB % 265.52/37.97 % (3475007)Instructions burned: 319 (million) % 265.52/37.97 % (3475009)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=631275209:i=1428:nm=2:rtra=on_2667 on theBenchmark for (2667ds/1428Mi) % 265.52/37.97 % (3475009)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 265.52/37.97 % (3475009)Terminated due to inappropriate strategy. % 265.52/37.97 % (3475009)------------------------------ % 265.52/37.97 % (3475009)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 265.52/37.97 % (3475009)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 265.52/37.97 % (3475009)CaDiCaL version: 2.1.3 % 265.52/37.97 % (3475009)Termination reason: Inappropriate % 265.52/37.97 % (3475009)Time elapsed: 0.0000 s % 265.52/37.97 % (3475009)Peak memory usage: 10 MB % 265.52/37.97 % (3475009)------------------------------ % 265.52/37.97 % (3475009)------------------------------ % 265.52/37.97 % (3475011)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=1751363801:i=262:bd=preordered:rtra=on:fsd=on_2667 on theBenchmark for (2667ds/262Mi) % 265.52/37.97 % (3475011)Instruction limit reached! % 265.52/37.97 % (3475011)------------------------------ % 265.52/37.97 % (3475011)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 282.25/40.16 % (3475011)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 282.25/40.16 % (3475011)CaDiCaL version: 2.1.3 % 282.25/40.16 % (3475011)Termination reason: Instruction limit % 282.25/40.16 % (3475011)Termination phase: Saturation % 282.25/40.16 % (3475011)Time elapsed: 0.175 s % 282.25/40.16 % (3475011)Peak memory usage: 13 MB % 282.25/40.16 % (3475011)Instructions burned: 262 (million) % 282.25/40.16 % (3475013)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=3807693806:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2665 on theBenchmark for (2665ds/1368Mi) % 282.25/40.16 % (3475013)Instruction limit reached! % 282.25/40.16 % (3475013)------------------------------ % 282.25/40.16 % (3475013)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 282.25/40.16 % (3475013)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 282.25/40.16 % (3475013)CaDiCaL version: 2.1.3 % 282.25/40.16 % (3475013)Termination reason: Instruction limit % 282.25/40.16 % (3475013)Termination phase: Saturation % 282.25/40.16 % (3475013)Time elapsed: 0.677 s % 282.25/40.16 % (3475013)Peak memory usage: 17 MB % 282.25/40.16 % (3475013)Instructions burned: 1370 (million) % 282.25/40.16 % (3475015)ott-21_1_sil=16000:si=on:fs=off:random_seed=3205678255:i=360:av=off:fsr=off:rtra=on_2658 on theBenchmark for (2658ds/360Mi) % 282.25/40.16 % (3475015)Instruction limit reached! % 282.25/40.16 % (3475015)------------------------------ % 282.25/40.16 % (3475015)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 282.25/40.16 % (3475015)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 282.25/40.16 % (3475015)CaDiCaL version: 2.1.3 % 282.25/40.16 % (3475015)Termination reason: Instruction limit % 282.25/40.16 % (3475015)Termination phase: Saturation % 282.25/40.16 % (3475015)Time elapsed: 0.156 s % 282.25/40.16 % (3475015)Peak memory usage: 13 MB % 282.25/40.16 % (3475015)Instructions burned: 361 (million) % 282.25/40.16 % (3475017)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=4185094856:i=954:bd=all:rtra=on_2656 on theBenchmark for (2656ds/954Mi) % 282.25/40.16 % (3475017)Instruction limit reached! % 282.25/40.16 % (3475017)------------------------------ % 282.25/40.16 % (3475017)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 282.25/40.16 % (3475017)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 282.25/40.16 % (3475017)CaDiCaL version: 2.1.3 % 282.25/40.16 % (3475017)Termination reason: Instruction limit % 282.25/40.16 % (3475017)Termination phase: Saturation % 282.25/40.16 % (3475017)Time elapsed: 0.582 s % 282.25/40.16 % (3475017)Peak memory usage: 17 MB % 282.25/40.16 % (3475017)Instructions burned: 954 (million) % 282.25/40.16 % (3475019)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=1226744299:fmbsr=1.3:i=1730:ins=25:rtra=on_2650 on theBenchmark for (2650ds/1730Mi) % 282.25/40.16 % (3475019)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 282.25/40.16 % (3475019)Terminated due to inappropriate strategy. % 282.25/40.16 % (3475019)------------------------------ % 282.25/40.16 % (3475019)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 282.25/40.16 % (3475019)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 282.25/40.16 % (3475019)CaDiCaL version: 2.1.3 % 282.25/40.16 % (3475019)Termination reason: Inappropriate % 282.25/40.16 % (3475019)Time elapsed: 0.0000 s % 282.25/40.16 % (3475019)Peak memory usage: 10 MB % 282.25/40.16 % (3475019)------------------------------ % 282.25/40.16 % (3475019)------------------------------ % 282.25/40.16 % (3475021)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=2117065181:i=2358:rtra=on_2650 on theBenchmark for (2650ds/2358Mi) % 282.25/40.16 % (3475021)Instruction limit reached! % 282.25/40.16 % (3475021)------------------------------ % 282.25/40.16 % (3475021)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 282.25/40.16 % (3475021)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 282.25/40.16 % (3475021)CaDiCaL version: 2.1.3 % 282.25/40.16 % (3475021)Termination reason: Instruction limit % 282.25/40.16 % (3475021)Termination phase: Saturation % 282.25/40.16 % (3475021)Time elapsed: 1.583 s % 282.25/40.16 % (3475021)Peak memory usage: 21 MB % 282.25/40.16 % (3475021)Instructions burned: 2359 (million) % 282.25/40.16 % (3475023)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=1954895181:i=1778:ins=1:rtra=on_2634 on theBenchmark for (2634ds/1778Mi) % 282.25/40.16 % (3475023)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 300.44/42.74 % (3475023)Terminated due to inappropriate strategy. % 300.44/42.74 % (3475023)------------------------------ % 300.44/42.74 % (3475023)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.44/42.74 % (3475023)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.44/42.74 % (3475023)CaDiCaL version: 2.1.3 % 300.44/42.74 % (3475023)Termination reason: Inappropriate % 300.44/42.74 % (3475023)Time elapsed: 0.0000 s % 300.44/42.74 % (3475023)Peak memory usage: 10 MB % 300.44/42.74 % (3475023)------------------------------ % 300.44/42.74 % (3475023)------------------------------ % 300.44/42.74 % (3475025)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=1375019917:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2633 on theBenchmark for (2633ds/1384Mi) % 300.44/42.74 % (3474903)Instruction limit reached! % 300.44/42.74 % (3474903)------------------------------ % 300.44/42.74 % (3474903)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.44/42.74 % (3474903)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.44/42.74 % (3474903)CaDiCaL version: 2.1.3 % 300.44/42.74 % (3474903)Termination reason: Instruction limit % 300.44/42.74 % (3474903)Termination phase: Saturation % 300.44/42.74 % (3474903)Time elapsed: 14.695 s % 300.44/42.74 % (3474903)Peak memory usage: 277 MB % 300.44/42.74 % (3474903)Instructions burned: 53301 (million) % 300.44/42.74 % (3475027)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=1549782042:i=1758:kws=inv_precedence:fsr=off:rtra=on_2625 on theBenchmark for (2625ds/1758Mi) % 300.44/42.74 % (3475025)Instruction limit reached! % 300.44/42.74 % (3475025)------------------------------ % 300.44/42.74 % (3475025)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.44/42.74 % (3475025)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.44/42.74 % (3475025)CaDiCaL version: 2.1.3 % 300.44/42.74 % (3475025)Termination reason: Instruction limit % 300.44/42.74 % (3475025)Termination phase: Saturation % 300.44/42.74 % (3475025)Time elapsed: 0.854 s % 300.44/42.74 % (3475025)Peak memory usage: 21 MB % 300.44/42.74 % (3475025)Instructions burned: 1384 (million) % 300.44/42.74 % (3475029)fmb+10_1_sil=64000:si=on:random_seed=271548661:i=44122:nm=2:rtra=on:gsp=on_2625 on theBenchmark for (2625ds/44122Mi) % 300.44/42.74 % (3475029)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 300.44/42.74 % (3475029)Terminated due to inappropriate strategy. % 300.44/42.74 % (3475029)------------------------------ % 300.44/42.74 % (3475029)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.44/42.74 % (3475029)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.44/42.74 % (3475029)CaDiCaL version: 2.1.3 % 300.44/42.74 % (3475029)Termination reason: Inappropriate % 300.44/42.74 % (3475029)Time elapsed: 0.0000 s % 300.44/42.74 % (3475029)Peak memory usage: 10 MB % 300.44/42.74 % (3475029)------------------------------ % 300.44/42.74 % (3475029)------------------------------ % 300.44/42.74 % (3475031)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=752519338:i=19030:nm=5:rtra=on_2624 on theBenchmark for (2624ds/19030Mi) % 300.44/42.74 % (3475031)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 300.44/42.74 % (3475031)Terminated due to inappropriate strategy. % 300.44/42.74 % (3475031)------------------------------ % 300.44/42.74 % (3475031)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.44/42.74 % (3475031)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.44/42.74 % (3475031)CaDiCaL version: 2.1.3 % 300.44/42.74 % (3475031)Termination reason: Inappropriate % 300.44/42.74 % (3475031)Time elapsed: 0.0000 s % 300.44/42.74 % (3475031)Peak memory usage: 10 MB % 300.44/42.74 % (3475031)------------------------------ % 300.44/42.74 % (3475031)------------------------------ % 300.44/42.74 % (3475033)fmb+10_1_sil=64000:sas=cadical:si=on:fmbss=8:random_seed=3779749537:fmbsr=1.7:i=1840:rtra=on_2624 on theBenchmark for (2624ds/1840Mi) % 300.44/42.74 % (3475033)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 300.44/42.74 % (3475033)Terminated due to inappropriate strategy. % 300.44/42.74 % (3475033)------------------------------ % 300.44/42.74 % (3475033)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.44/42.74 % (3475033)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c % 300.44/42.74 Terminated % 300.44/42.74 % Vampire exiting %------------------------------------------------------------------------------