%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWX085_1 : TPTP v9.3.1. Released v9.1.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % Computer : n016.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:27 PM UTC 2026 % Result : Timeout 300.10s 42.54s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : SWX085_1 : TPTP v9.3.1. Released v9.1.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.05/0.17 % Computer : n016.cluster.edu % 0.05/0.17 % Model : x86_64 x86_64 % 0.05/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.05/0.17 % Memory : 8046.5625MB % 0.05/0.17 % OS : Linux 6.8.0-71-generic % 0.05/0.17 % CPULimit : 300 % 0.05/0.17 % WCLimit : 300 % 0.05/0.17 % DateTime : Mon Sep 28 15:05:19 UTC 2026 % 0.05/0.18 % CPUTime : % 0.05/0.18 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.05/0.20 Running first-order model finding % 0.05/0.21 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 3.87/0.85 % (3688576)Will run a generic schedule for satisfiability detection. % 3.87/0.85 % (3688583)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1847933355:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 3.87/0.85 % (3688582)% WARNING: option uhcvi not known. % 3.87/0.85 % (3688584)dis+10_1_sil=32000:sp=arity:random_seed=348753409:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 3.87/0.85 % (3688581)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=827525521_2999 on theBenchmark for (2999ds/0Mi) % 3.87/0.85 % (3688582)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1684506627:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 3.87/0.85 % (3688586)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=772647832:i=131_2999 on theBenchmark for (2999ds/131Mi) % 3.87/0.85 % (3688585)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2631649718:i=116_2999 on theBenchmark for (2999ds/116Mi) % 3.87/0.85 % (3688587)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1239882010:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 3.87/0.85 % (3688581)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.87/0.85 % (3688581)Terminated due to inappropriate strategy. % 3.87/0.85 % (3688581)------------------------------ % 3.87/0.85 % (3688581)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.87/0.85 % (3688581)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.87/0.85 % (3688581)CaDiCaL version: 2.1.3 % 3.87/0.85 % (3688581)Termination reason: Inappropriate % 3.87/0.85 % (3688581)Time elapsed: 0.002 s % 3.87/0.85 % (3688581)Peak memory usage: 11 MB % 3.87/0.85 % (3688581)Instructions burned: 2 (million) % 3.87/0.85 % (3688581)------------------------------ % 3.87/0.85 % (3688581)------------------------------ % 3.87/0.85 % (3688595)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1217120076:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 3.87/0.85 % (3688595)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.87/0.85 % (3688595)Terminated due to inappropriate strategy. % 3.87/0.85 % (3688595)------------------------------ % 3.87/0.85 % (3688595)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.87/0.85 % (3688595)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.87/0.85 % (3688595)CaDiCaL version: 2.1.3 % 3.87/0.85 % (3688595)Termination reason: Inappropriate % 3.87/0.85 % (3688595)Time elapsed: 0.001 s % 3.87/0.85 % (3688595)Peak memory usage: 11 MB % 3.87/0.85 % (3688595)Instructions burned: 2 (million) % 3.87/0.85 % (3688595)------------------------------ % 3.87/0.85 % (3688595)------------------------------ % 3.87/0.85 % (3688597)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=428506526:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 3.87/0.85 % (3688584)Instruction limit reached! % 3.87/0.85 % (3688584)------------------------------ % 3.87/0.85 % (3688584)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.87/0.85 % (3688584)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.87/0.85 % (3688584)CaDiCaL version: 2.1.3 % 3.87/0.85 % (3688584)Termination reason: Instruction limit % 3.87/0.85 % (3688584)Termination phase: Saturation % 3.87/0.85 % (3688584)Time elapsed: 0.067 s % 3.87/0.85 % (3688584)Peak memory usage: 13 MB % 3.87/0.85 % (3688584)Instructions burned: 104 (million) % 3.87/0.85 % (3688585)Instruction limit reached! % 3.87/0.85 % (3688585)------------------------------ % 3.87/0.85 % (3688585)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.87/0.85 % (3688585)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.87/0.85 % (3688585)CaDiCaL version: 2.1.3 % 3.87/0.85 % (3688585)Termination reason: Instruction limit % 3.87/0.85 % (3688585)Termination phase: Saturation % 3.87/0.85 % (3688585)Time elapsed: 0.069 s % 3.87/0.85 % (3688585)Peak memory usage: 12 MB % 3.87/0.85 % (3688585)Instructions burned: 118 (million) % 3.87/0.85 % (3688586)Instruction limit reached! % 3.87/0.85 % (3688586)------------------------------ % 3.87/0.85 % (3688586)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.87/0.85 % (3688586)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.87/0.85 % (3688586)CaDiCaL version: 2.1.3 % 3.87/0.85 % (3688586)Termination reason: Instruction limit % 4.37/1.04 % (3688586)Termination phase: Saturation % 4.37/1.04 % (3688586)Time elapsed: 0.084 s % 4.37/1.04 % (3688586)Peak memory usage: 13 MB % 4.37/1.04 % (3688586)Instructions burned: 133 (million) % 4.37/1.04 % (3688599)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=740109814:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi) % 4.37/1.04 % (3688587)Instruction limit reached! % 4.37/1.04 % (3688587)------------------------------ % 4.37/1.04 % (3688587)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 4.37/1.04 % (3688587)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.37/1.04 % (3688587)CaDiCaL version: 2.1.3 % 4.37/1.04 % (3688587)Termination reason: Instruction limit % 4.37/1.04 % (3688587)Termination phase: Saturation % 4.37/1.04 % (3688587)Time elapsed: 0.085 s % 4.37/1.04 % (3688587)Peak memory usage: 12 MB % 4.37/1.04 % (3688587)Instructions burned: 161 (million) % 4.37/1.04 % (3688600)ott-21_1_sil=16000:fs=off:random_seed=2217756883:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 4.37/1.04 % (3688602)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=4008909663:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 4.37/1.04 % (3688603)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3349376427:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 4.37/1.04 % (3688597)Instruction limit reached! % 4.37/1.04 % (3688597)------------------------------ % 4.37/1.04 % (3688597)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 4.37/1.04 % (3688597)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.37/1.04 % (3688597)CaDiCaL version: 2.1.3 % 4.37/1.04 % (3688597)Termination reason: Instruction limit % 4.37/1.04 % (3688597)Termination phase: Saturation % 4.37/1.04 % (3688597)Time elapsed: 0.082 s % 4.37/1.04 % (3688597)Peak memory usage: 13 MB % 4.37/1.04 % (3688597)Instructions burned: 133 (million) % 4.37/1.04 % (3688603)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 4.37/1.04 % (3688603)Terminated due to inappropriate strategy. % 4.37/1.04 % (3688603)------------------------------ % 4.37/1.04 % (3688603)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 4.37/1.04 % (3688603)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.37/1.04 % (3688603)CaDiCaL version: 2.1.3 % 4.37/1.04 % (3688603)Termination reason: Inappropriate % 4.37/1.04 % (3688603)Time elapsed: 0.001 s % 4.37/1.04 % (3688603)Peak memory usage: 10 MB % 4.37/1.04 % (3688603)Instructions burned: 1 (million) % 4.37/1.04 % (3688603)------------------------------ % 4.37/1.04 % (3688603)------------------------------ % 4.37/1.04 % (3688607)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1099184228:i=1179_2998 on theBenchmark for (2998ds/1179Mi) % 4.37/1.04 % (3688608)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=340667634:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi) % 4.37/1.04 % (3688608)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 4.37/1.04 % (3688608)Terminated due to inappropriate strategy. % 4.37/1.04 % (3688608)------------------------------ % 4.37/1.04 % (3688608)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 4.37/1.04 % (3688608)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.37/1.04 % (3688608)CaDiCaL version: 2.1.3 % 4.37/1.04 % (3688608)Termination reason: Inappropriate % 4.37/1.04 % (3688608)Time elapsed: 0.001 s % 4.37/1.04 % (3688608)Peak memory usage: 10 MB % 4.37/1.04 % (3688608)Instructions burned: 2 (million) % 4.37/1.04 % (3688608)------------------------------ % 4.37/1.04 % (3688608)------------------------------ % 4.37/1.04 % (3688611)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=3645039059:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2998 on theBenchmark for (2998ds/692Mi) % 4.37/1.04 % (3688600)Instruction limit reached! % 4.37/1.04 % (3688600)------------------------------ % 4.37/1.04 % (3688600)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 4.37/1.04 % (3688600)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.37/1.04 % (3688600)CaDiCaL version: 2.1.3 % 4.37/1.04 % (3688600)Termination reason: Instruction limit % 4.37/1.04 % (3688600)Termination phase: Saturation % 22.53/3.47 % (3688600)Time elapsed: 0.083 s % 22.53/3.47 % (3688600)Peak memory usage: 12 MB % 22.53/3.47 % (3688600)Instructions burned: 181 (million) % 22.53/3.47 % (3688613)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1524671869:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi) % 22.53/3.47 % (3688599)Instruction limit reached! % 22.53/3.47 % (3688599)------------------------------ % 22.53/3.47 % (3688599)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.53/3.47 % (3688599)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.53/3.47 % (3688599)CaDiCaL version: 2.1.3 % 22.53/3.47 % (3688599)Termination reason: Instruction limit % 22.53/3.47 % (3688599)Termination phase: Saturation % 22.53/3.47 % (3688599)Time elapsed: 0.305 s % 22.53/3.47 % (3688599)Peak memory usage: 14 MB % 22.53/3.47 % (3688599)Instructions burned: 686 (million) % 22.53/3.47 % (3688602)Instruction limit reached! % 22.53/3.47 % (3688602)------------------------------ % 22.53/3.47 % (3688602)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.53/3.47 % (3688602)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.53/3.47 % (3688602)CaDiCaL version: 2.1.3 % 22.53/3.47 % (3688602)Termination reason: Instruction limit % 22.53/3.47 % (3688602)Termination phase: Saturation % 22.53/3.47 % (3688602)Time elapsed: 0.299 s % 22.53/3.47 % (3688602)Peak memory usage: 14 MB % 22.53/3.47 % (3688602)Instructions burned: 477 (million) % 22.53/3.47 % (3688615)fmb+10_1_sil=64000:random_seed=1736404168:i=22061:nm=2:gsp=on_2995 on theBenchmark for (2995ds/22061Mi) % 22.53/3.47 % (3688615)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 22.53/3.47 % (3688615)Terminated due to inappropriate strategy. % 22.53/3.47 % (3688615)------------------------------ % 22.53/3.47 % (3688615)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.53/3.47 % (3688615)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.53/3.47 % (3688615)CaDiCaL version: 2.1.3 % 22.53/3.47 % (3688615)Termination reason: Inappropriate % 22.53/3.47 % (3688615)Time elapsed: 0.001 s % 22.53/3.47 % (3688615)Peak memory usage: 10 MB % 22.53/3.47 % (3688615)Instructions burned: 2 (million) % 22.53/3.47 % (3688615)------------------------------ % 22.53/3.47 % (3688615)------------------------------ % 22.53/3.47 % (3688616)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=192253875:i=9515:nm=5_2995 on theBenchmark for (2995ds/9515Mi) % 22.53/3.47 % (3688616)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 22.53/3.47 % (3688616)Terminated due to inappropriate strategy. % 22.53/3.47 % (3688616)------------------------------ % 22.53/3.47 % (3688616)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.53/3.47 % (3688616)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.53/3.47 % (3688616)CaDiCaL version: 2.1.3 % 22.53/3.47 % (3688616)Termination reason: Inappropriate % 22.53/3.47 % (3688616)Time elapsed: 0.001 s % 22.53/3.47 % (3688616)Peak memory usage: 10 MB % 22.53/3.47 % (3688616)Instructions burned: 2 (million) % 22.53/3.47 % (3688616)------------------------------ % 22.53/3.47 % (3688616)------------------------------ % 22.53/3.47 % (3688618)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=971567375:fmbsr=1.7:i=920_2995 on theBenchmark for (2995ds/920Mi) % 22.53/3.47 % (3688618)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 22.53/3.47 % (3688618)Terminated due to inappropriate strategy. % 22.53/3.47 % (3688618)------------------------------ % 22.53/3.47 % (3688618)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.53/3.47 % (3688618)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.53/3.47 % (3688618)CaDiCaL version: 2.1.3 % 22.53/3.47 % (3688618)Termination reason: Inappropriate % 22.53/3.47 % (3688618)Time elapsed: 0.001 s % 22.53/3.47 % (3688618)Peak memory usage: 10 MB % 22.53/3.47 % (3688618)Instructions burned: 2 (million) % 22.53/3.47 % (3688618)------------------------------ % 22.53/3.47 % (3688618)------------------------------ % 22.53/3.47 % (3688620)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1960401700:i=5131_2995 on theBenchmark for (2995ds/5131Mi) % 22.53/3.47 % (3688622)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=321100434:i=1472:ins=7:fdi=8:gsp=on_2995 on theBenchmark for (2995ds/1472Mi) % 22.53/3.47 % (3688611)Instruction limit reached! % 22.53/3.47 % (3688611)------------------------------ % 36.74/5.40 % (3688611)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 36.74/5.40 % (3688611)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 36.74/5.40 % (3688611)CaDiCaL version: 2.1.3 % 36.74/5.40 % (3688611)Termination reason: Instruction limit % 36.74/5.40 % (3688611)Termination phase: Saturation % 36.74/5.40 % (3688611)Time elapsed: 0.427 s % 36.74/5.40 % (3688611)Peak memory usage: 19 MB % 36.74/5.40 % (3688611)Instructions burned: 693 (million) % 36.74/5.40 % (3688625)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=876603583:i=6324_2993 on theBenchmark for (2993ds/6324Mi) % 36.74/5.40 % (3688625)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 36.74/5.40 % (3688625)Terminated due to inappropriate strategy. % 36.74/5.40 % (3688625)------------------------------ % 36.74/5.40 % (3688625)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 36.74/5.40 % (3688625)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 36.74/5.40 % (3688625)CaDiCaL version: 2.1.3 % 36.74/5.40 % (3688625)Termination reason: Inappropriate % 36.74/5.40 % (3688625)Time elapsed: 0.002 s % 36.74/5.40 % (3688625)Peak memory usage: 11 MB % 36.74/5.40 % (3688625)Instructions burned: 2 (million) % 36.74/5.40 % (3688625)------------------------------ % 36.74/5.40 % (3688625)------------------------------ % 36.74/5.40 % (3688627)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=734125633:fmbsr=2.30978:i=2174_2993 on theBenchmark for (2993ds/2174Mi) % 36.74/5.40 % (3688627)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 36.74/5.40 % (3688627)Terminated due to inappropriate strategy. % 36.74/5.40 % (3688627)------------------------------ % 36.74/5.40 % (3688627)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 36.74/5.40 % (3688627)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 36.74/5.40 % (3688627)CaDiCaL version: 2.1.3 % 36.74/5.40 % (3688627)Termination reason: Inappropriate % 36.74/5.40 % (3688627)Time elapsed: 0.001 s % 36.74/5.40 % (3688627)Peak memory usage: 10 MB % 36.74/5.40 % (3688627)Instructions burned: 2 (million) % 36.74/5.40 % (3688627)------------------------------ % 36.74/5.40 % (3688627)------------------------------ % 36.74/5.40 % (3688629)ott-2_1_sil=16000:newcnf=on:random_seed=3875876204:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2993 on theBenchmark for (2993ds/869Mi) % 36.74/5.40 % (3688613)Instruction limit reached! % 36.74/5.40 % (3688613)------------------------------ % 36.74/5.40 % (3688613)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 36.74/5.40 % (3688613)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 36.74/5.40 % (3688613)CaDiCaL version: 2.1.3 % 36.74/5.40 % (3688613)Termination reason: Instruction limit % 36.74/5.40 % (3688613)Termination phase: Saturation % 36.74/5.40 % (3688613)Time elapsed: 0.520 s % 36.74/5.40 % (3688613)Peak memory usage: 18 MB % 36.74/5.40 % (3688613)Instructions burned: 879 (million) % 36.74/5.40 % (3688631)ott+10_1_sil=32000:tgt=ground:random_seed=2640805563:i=5114:av=off_2992 on theBenchmark for (2992ds/5114Mi) % 36.74/5.40 % (3688607)Instruction limit reached! % 36.74/5.40 % (3688607)------------------------------ % 36.74/5.40 % (3688607)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 36.74/5.40 % (3688607)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 36.74/5.40 % (3688607)CaDiCaL version: 2.1.3 % 36.74/5.40 % (3688607)Termination reason: Instruction limit % 36.74/5.40 % (3688607)Termination phase: Saturation % 36.74/5.40 % (3688607)Time elapsed: 0.615 s % 36.74/5.40 % (3688607)Peak memory usage: 18 MB % 36.74/5.40 % (3688607)Instructions burned: 1180 (million) % 36.74/5.40 % (3688633)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=911107841:i=54282_2992 on theBenchmark for (2992ds/54282Mi) % 36.74/5.40 % (3688633)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 36.74/5.40 % (3688633)Terminated due to inappropriate strategy. % 36.74/5.40 % (3688633)------------------------------ % 36.74/5.40 % (3688633)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 36.74/5.40 % (3688633)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 36.74/5.40 % (3688633)CaDiCaL version: 2.1.3 % 36.74/5.40 % (3688633)Termination reason: Inappropriate % 36.74/5.40 % (3688633)Time elapsed: 0.002 s % 36.74/5.40 % (3688633)Peak memory usage: 11 MB % 36.74/5.40 % (3688633)Instructions burned: 2 (million) % 109.16/15.66 % (3688633)------------------------------ % 109.16/15.66 % (3688633)------------------------------ % 109.16/15.66 % (3688635)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3336861542:i=3512:aac=none_2991 on theBenchmark for (2991ds/3512Mi) % 109.16/15.66 % (3688629)Instruction limit reached! % 109.16/15.66 % (3688629)------------------------------ % 109.16/15.66 % (3688629)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 109.16/15.66 % (3688629)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 109.16/15.66 % (3688629)CaDiCaL version: 2.1.3 % 109.16/15.66 % (3688629)Termination reason: Instruction limit % 109.16/15.66 % (3688629)Termination phase: Saturation % 109.16/15.66 % (3688629)Time elapsed: 0.494 s % 109.16/15.66 % (3688629)Peak memory usage: 15 MB % 109.16/15.66 % (3688629)Instructions burned: 869 (million) % 109.16/15.66 % (3688637)dis+21_1_sil=32000:sas=cadical:random_seed=1235839745:i=3773:amm=off_2988 on theBenchmark for (2988ds/3773Mi) % 109.16/15.66 % (3688622)Instruction limit reached! % 109.16/15.66 % (3688622)------------------------------ % 109.16/15.66 % (3688622)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 109.16/15.66 % (3688622)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 109.16/15.66 % (3688622)CaDiCaL version: 2.1.3 % 109.16/15.66 % (3688622)Termination reason: Instruction limit % 109.16/15.66 % (3688622)Termination phase: Saturation % 109.16/15.66 % (3688622)Time elapsed: 0.812 s % 109.16/15.66 % (3688622)Peak memory usage: 31 MB % 109.16/15.66 % (3688622)Instructions burned: 1474 (million) % 109.16/15.66 % (3688639)ott+11_1_sil=16000:gs=on:random_seed=3755196665:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2986 on theBenchmark for (2986ds/2251Mi) % 109.16/15.66 % (3688639)Instruction limit reached! % 109.16/15.66 % (3688639)------------------------------ % 109.16/15.66 % (3688639)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 109.16/15.66 % (3688639)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 109.16/15.66 % (3688639)CaDiCaL version: 2.1.3 % 109.16/15.66 % (3688639)Termination reason: Instruction limit % 109.16/15.66 % (3688639)Termination phase: Saturation % 109.16/15.66 % (3688639)Time elapsed: 1.264 s % 109.16/15.66 % (3688639)Peak memory usage: 24 MB % 109.16/15.66 % (3688639)Instructions burned: 2251 (million) % 109.16/15.66 % (3688641)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=3032156291:fmbsr=1.6:i=67534_2974 on theBenchmark for (2974ds/67534Mi) % 109.16/15.66 % (3688641)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 109.16/15.66 % (3688641)Terminated due to inappropriate strategy. % 109.16/15.66 % (3688641)------------------------------ % 109.16/15.66 % (3688641)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 109.16/15.66 % (3688641)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 109.16/15.66 % (3688641)CaDiCaL version: 2.1.3 % 109.16/15.66 % (3688641)Termination reason: Inappropriate % 109.16/15.66 % (3688641)Time elapsed: 0.001 s % 109.16/15.66 % (3688641)Peak memory usage: 10 MB % 109.16/15.66 % (3688641)Instructions burned: 2 (million) % 109.16/15.66 % (3688641)------------------------------ % 109.16/15.66 % (3688641)------------------------------ % 109.16/15.66 % (3688643)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=3432758672:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2973 on theBenchmark for (2973ds/4591Mi) % 109.16/15.66 % (3688635)Instruction limit reached! % 109.16/15.66 % (3688635)------------------------------ % 109.16/15.66 % (3688635)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 109.16/15.66 % (3688635)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 109.16/15.66 % (3688635)CaDiCaL version: 2.1.3 % 109.16/15.66 % (3688635)Termination reason: Instruction limit % 109.16/15.66 % (3688635)Termination phase: Saturation % 109.16/15.66 % (3688635)Time elapsed: 1.890 s % 109.16/15.66 % (3688635)Peak memory usage: 30 MB % 109.16/15.66 % (3688635)Instructions burned: 3513 (million) % 109.16/15.66 % (3688645)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=1987026527:i=29340_2972 on theBenchmark for (2972ds/29340Mi) % 109.16/15.66 % (3688637)Instruction limit reached! % 109.16/15.66 % (3688637)------------------------------ % 109.16/15.66 % (3688637)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 109.16/15.66 % (3688637)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 109.16/15.66 % (3688637)CaDiCaL version: 2.1.3 % 109.16/15.66 % (3688637)Termination reason: Instruction limit % 134.73/19.26 % (3688637)Termination phase: Saturation % 134.73/19.26 % (3688637)Time elapsed: 2.040 s % 134.73/19.26 % (3688637)Peak memory usage: 32 MB % 134.73/19.26 % (3688637)Instructions burned: 3774 (million) % 134.73/19.26 % (3688620)Instruction limit reached! % 134.73/19.26 % (3688620)------------------------------ % 134.73/19.26 % (3688620)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 134.73/19.26 % (3688620)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 134.73/19.26 % (3688620)CaDiCaL version: 2.1.3 % 134.73/19.26 % (3688620)Termination reason: Instruction limit % 134.73/19.26 % (3688620)Termination phase: Saturation % 134.73/19.26 % (3688620)Time elapsed: 2.785 s % 134.73/19.26 % (3688620)Peak memory usage: 40 MB % 134.73/19.26 % (3688620)Instructions burned: 5132 (million) % 134.73/19.26 % (3688647)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=3401923625:i=5211_2967 on theBenchmark for (2967ds/5211Mi) % 134.73/19.26 % (3688648)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=2235136755:i=5497:nm=2_2967 on theBenchmark for (2967ds/5497Mi) % 134.73/19.26 % (3688648)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 134.73/19.26 % (3688648)Terminated due to inappropriate strategy. % 134.73/19.26 % (3688648)------------------------------ % 134.73/19.26 % (3688648)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 134.73/19.26 % (3688648)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 134.73/19.26 % (3688648)CaDiCaL version: 2.1.3 % 134.73/19.26 % (3688648)Termination reason: Inappropriate % 134.73/19.26 % (3688648)Time elapsed: 0.002 s % 134.73/19.26 % (3688648)Peak memory usage: 11 MB % 134.73/19.26 % (3688648)Instructions burned: 2 (million) % 134.73/19.26 % (3688648)------------------------------ % 134.73/19.26 % (3688648)------------------------------ % 134.73/19.26 % (3688651)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=799179908:fmbsr=2:i=46332_2967 on theBenchmark for (2967ds/46332Mi) % 134.73/19.26 % (3688651)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 134.73/19.26 % (3688651)Terminated due to inappropriate strategy. % 134.73/19.26 % (3688651)------------------------------ % 134.73/19.26 % (3688651)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 134.73/19.26 % (3688651)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 134.73/19.26 % (3688651)CaDiCaL version: 2.1.3 % 134.73/19.26 % (3688651)Termination reason: Inappropriate % 134.73/19.26 % (3688651)Time elapsed: 0.001 s % 134.73/19.26 % (3688651)Peak memory usage: 11 MB % 134.73/19.26 % (3688651)Instructions burned: 2 (million) % 134.73/19.26 % (3688651)------------------------------ % 134.73/19.26 % (3688651)------------------------------ % 134.73/19.26 % (3688653)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=1292918491:i=14071_2966 on theBenchmark for (2966ds/14071Mi) % 134.73/19.26 % (3688653)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 134.73/19.26 % (3688653)Terminated due to inappropriate strategy. % 134.73/19.26 % (3688653)------------------------------ % 134.73/19.26 % (3688653)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 134.73/19.26 % (3688653)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 134.73/19.26 % (3688653)CaDiCaL version: 2.1.3 % 134.73/19.26 % (3688653)Termination reason: Inappropriate % 134.73/19.26 % (3688653)Time elapsed: 0.001 s % 134.73/19.26 % (3688653)Peak memory usage: 11 MB % 134.73/19.26 % (3688653)Instructions burned: 2 (million) % 134.73/19.26 % (3688653)------------------------------ % 134.73/19.26 % (3688653)------------------------------ % 134.73/19.26 % (3688655)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1228561424:i=22565:add=on:rawr=on_2966 on theBenchmark for (2966ds/22565Mi) % 134.73/19.26 % (3688631)Instruction limit reached! % 134.73/19.26 % (3688631)------------------------------ % 134.73/19.26 % (3688631)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 134.73/19.26 % (3688631)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 134.73/19.26 % (3688631)CaDiCaL version: 2.1.3 % 134.73/19.26 % (3688631)Termination reason: Instruction limit % 134.73/19.26 % (3688631)Termination phase: Saturation % 134.73/19.26 % (3688631)Time elapsed: 3.166 s % 134.73/19.26 % (3688631)Peak memory usage: 32 MB % 134.73/19.26 % (3688631)Instructions burned: 5115 (million) % 134.73/19.26 % (3688657)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=3664593699:i=8173:av=off_2960 on theBenchmark for (2960ds/8173Mi) % 134.73/19.26 % (3688643)Instruction limit reached! % 135.42/19.38 % (3688643)------------------------------ % 135.42/19.38 % (3688643)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 135.42/19.38 % (3688643)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 135.42/19.38 % (3688643)CaDiCaL version: 2.1.3 % 135.42/19.38 % (3688643)Termination reason: Instruction limit % 135.42/19.38 % (3688643)Termination phase: Saturation % 135.42/19.38 % (3688643)Time elapsed: 2.555 s % 135.42/19.38 % (3688643)Peak memory usage: 47 MB % 135.42/19.38 % (3688643)Instructions burned: 4591 (million) % 135.42/19.38 % (3688659)dis+10_16:1_sil=16000:random_seed=335841769:i=9155:fsr=off_2948 on theBenchmark for (2948ds/9155Mi) % 135.42/19.38 % (3688647)Instruction limit reached! % 135.42/19.38 % (3688647)------------------------------ % 135.42/19.38 % (3688647)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 135.42/19.38 % (3688647)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 135.42/19.38 % (3688647)CaDiCaL version: 2.1.3 % 135.42/19.38 % (3688647)Termination reason: Instruction limit % 135.42/19.38 % (3688647)Termination phase: Saturation % 135.42/19.38 % (3688647)Time elapsed: 2.695 s % 135.42/19.38 % (3688647)Peak memory usage: 45 MB % 135.42/19.38 % (3688647)Instructions burned: 5213 (million) % 135.42/19.38 % (3688662)ott-3_8_sil=64000:random_seed=31041428:i=20139:bs=on_2940 on theBenchmark for (2940ds/20139Mi) % 135.42/19.38 % (3688657)Instruction limit reached! % 135.42/19.38 % (3688657)------------------------------ % 135.42/19.38 % (3688657)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 135.42/19.38 % (3688657)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 135.42/19.38 % (3688657)CaDiCaL version: 2.1.3 % 135.42/19.38 % (3688657)Termination reason: Instruction limit % 135.42/19.38 % (3688657)Termination phase: Saturation % 135.42/19.38 % (3688657)Time elapsed: 5.163 s % 135.42/19.38 % (3688657)Peak memory usage: 47 MB % 135.42/19.38 % (3688657)Instructions burned: 8173 (million) % 135.42/19.38 % (3688664)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=1766356932:fmbsr=2:i=32576_2908 on theBenchmark for (2908ds/32576Mi) % 135.42/19.38 % (3688664)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 135.42/19.38 % (3688664)Terminated due to inappropriate strategy. % 135.42/19.38 % (3688664)------------------------------ % 135.42/19.38 % (3688664)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 135.42/19.38 % (3688664)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 135.42/19.38 % (3688664)CaDiCaL version: 2.1.3 % 135.42/19.38 % (3688664)Termination reason: Inappropriate % 135.42/19.38 % (3688664)Time elapsed: 0.002 s % 135.42/19.38 % (3688664)Peak memory usage: 11 MB % 135.42/19.38 % (3688664)Instructions burned: 2 (million) % 135.42/19.38 % (3688664)------------------------------ % 135.42/19.38 % (3688664)------------------------------ % 135.42/19.38 % (3688666)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=1072862818:i=11404_2908 on theBenchmark for (2908ds/11404Mi) % 135.42/19.38 % (3688659)Instruction limit reached! % 135.42/19.38 % (3688659)------------------------------ % 135.42/19.38 % (3688659)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 135.42/19.38 % (3688659)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 135.42/19.38 % (3688659)CaDiCaL version: 2.1.3 % 135.42/19.38 % (3688659)Termination reason: Instruction limit % 135.42/19.38 % (3688659)Termination phase: Saturation % 135.42/19.38 % (3688659)Time elapsed: 4.747 s % 135.42/19.38 % (3688659)Peak memory usage: 51 MB % 135.42/19.38 % (3688659)Instructions burned: 9156 (million) % 135.42/19.38 % (3688668)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=4239452582:i=14134_2900 on theBenchmark for (2900ds/14134Mi) % 135.42/19.38 % (3688655)Instruction limit reached! % 135.42/19.38 % (3688655)------------------------------ % 135.42/19.38 % (3688655)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 135.42/19.38 % (3688655)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 135.42/19.38 % (3688655)CaDiCaL version: 2.1.3 % 135.42/19.38 % (3688655)Termination reason: Instruction limit % 135.42/19.38 % (3688655)Termination phase: Saturation % 135.42/19.38 % (3688655)Time elapsed: 11.089 s % 135.42/19.38 % (3688655)Peak memory usage: 525 MB % 135.42/19.38 % (3688655)Instructions burned: 22566 (million) % 135.42/19.38 % (3688670)dis+33_16_sil=32000:sac=on:random_seed=1765082575:i=15851:nm=0_2854 on theBenchmark for (2854ds/15851Mi) % 135.42/19.38 % (3688645)Instruction limit reached! % 135.42/19.38 % (3688645)------------------------------ % 135.42/19.38 % (3688645)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 169.17/24.12 % (3688645)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 169.17/24.12 % (3688645)CaDiCaL version: 2.1.3 % 169.17/24.12 % (3688645)Termination reason: Instruction limit % 169.17/24.12 % (3688645)Termination phase: Saturation % 169.17/24.12 % (3688645)Time elapsed: 12.693 s % 169.17/24.12 % (3688645)Peak memory usage: 214 MB % 169.17/24.12 % (3688645)Instructions burned: 29341 (million) % 169.17/24.12 % (3688672)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=3766193671:avsq=on:i=17627:add=on:amm=off_2845 on theBenchmark for (2845ds/17627Mi) % 169.17/24.12 % (3688666)Instruction limit reached! % 169.17/24.12 % (3688666)------------------------------ % 169.17/24.12 % (3688666)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 169.17/24.12 % (3688666)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 169.17/24.12 % (3688666)CaDiCaL version: 2.1.3 % 169.17/24.12 % (3688666)Termination reason: Instruction limit % 169.17/24.12 % (3688666)Termination phase: Saturation % 169.17/24.12 % (3688666)Time elapsed: 7.357 s % 169.17/24.12 % (3688666)Peak memory usage: 59 MB % 169.17/24.12 % (3688666)Instructions burned: 11405 (million) % 169.17/24.12 % (3688674)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=612683387:s2a=on:i=53295_2834 on theBenchmark for (2834ds/53295Mi) % 169.17/24.12 % (3688662)Instruction limit reached! % 169.17/24.12 % (3688662)------------------------------ % 169.17/24.12 % (3688662)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 169.17/24.12 % (3688662)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 169.17/24.12 % (3688662)CaDiCaL version: 2.1.3 % 169.17/24.12 % (3688662)Termination reason: Instruction limit % 169.17/24.12 % (3688662)Termination phase: Saturation % 169.17/24.12 % (3688662)Time elapsed: 10.768 s % 169.17/24.12 % (3688662)Peak memory usage: 59 MB % 169.17/24.12 % (3688662)Instructions burned: 20139 (million) % 169.17/24.12 % (3688676)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=1511396743:i=26857:ins=20_2832 on theBenchmark for (2832ds/26857Mi) % 169.17/24.12 % (3688676)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 169.17/24.12 % (3688676)Terminated due to inappropriate strategy. % 169.17/24.12 % (3688676)------------------------------ % 169.17/24.12 % (3688676)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 169.17/24.12 % (3688676)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 169.17/24.12 % (3688676)CaDiCaL version: 2.1.3 % 169.17/24.12 % (3688676)Termination reason: Inappropriate % 169.17/24.12 % (3688676)Time elapsed: 0.002 s % 169.17/24.12 % (3688676)Peak memory usage: 10 MB % 169.17/24.12 % (3688676)Instructions burned: 2 (million) % 169.17/24.12 % (3688676)------------------------------ % 169.17/24.12 % (3688676)------------------------------ % 169.17/24.12 % (3688678)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=2298746312:i=28120:bs=on:fsr=off_2832 on theBenchmark for (2832ds/28120Mi) % 169.17/24.12 % (3688668)Instruction limit reached! % 169.17/24.12 % (3688668)------------------------------ % 169.17/24.12 % (3688668)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 169.17/24.12 % (3688668)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 169.17/24.12 % (3688668)CaDiCaL version: 2.1.3 % 169.17/24.12 % (3688668)Termination reason: Instruction limit % 169.17/24.12 % (3688668)Termination phase: Saturation % 169.17/24.12 % (3688668)Time elapsed: 9.011 s % 169.17/24.12 % (3688668)Peak memory usage: 75 MB % 169.17/24.12 % (3688668)Instructions burned: 14134 (million) % 169.17/24.12 % (3688680)fmb+10_1_sil=256000:fmbss=7:random_seed=1779040893:fmbsr=1.6:i=182295_2809 on theBenchmark for (2809ds/182295Mi) % 169.17/24.12 % (3688680)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 169.17/24.12 % (3688680)Terminated due to inappropriate strategy. % 169.17/24.12 % (3688680)------------------------------ % 169.17/24.12 % (3688680)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 169.17/24.12 % (3688680)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 169.17/24.12 % (3688680)CaDiCaL version: 2.1.3 % 169.17/24.12 % (3688680)Termination reason: Inappropriate % 169.17/24.12 % (3688680)Time elapsed: 0.001 s % 169.17/24.12 % (3688680)Peak memory usage: 10 MB % 169.17/24.12 % (3688680)Instructions burned: 2 (million) % 169.17/24.12 % (3688680)------------------------------ % 169.17/24.12 % (3688680)------------------------------ % 169.17/24.12 % (3688682)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=1669021556:i=44625:gsp=on_2809 on theBenchmark for (2809ds/44625Mi) % 171.79/24.54 % (3688682)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 171.79/24.54 % (3688682)Terminated due to inappropriate strategy. % 171.79/24.54 % (3688682)------------------------------ % 171.79/24.54 % (3688682)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 171.79/24.54 % (3688682)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 171.79/24.54 % (3688682)CaDiCaL version: 2.1.3 % 171.79/24.54 % (3688682)Termination reason: Inappropriate % 171.79/24.54 % (3688682)Time elapsed: 0.002 s % 171.79/24.54 % (3688682)Peak memory usage: 11 MB % 171.79/24.54 % (3688682)Instructions burned: 2 (million) % 171.79/24.54 % (3688682)------------------------------ % 171.79/24.54 % (3688682)------------------------------ % 171.79/24.54 % (3688684)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=3756096619:i=160505_2809 on theBenchmark for (2809ds/160505Mi) % 171.79/24.54 % (3688684)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 171.79/24.54 % (3688684)Terminated due to inappropriate strategy. % 171.79/24.54 % (3688684)------------------------------ % 171.79/24.54 % (3688684)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 171.79/24.54 % (3688684)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 171.79/24.54 % (3688684)CaDiCaL version: 2.1.3 % 171.79/24.54 % (3688684)Termination reason: Inappropriate % 171.79/24.54 % (3688684)Time elapsed: 0.001 s % 171.79/24.54 % (3688684)Peak memory usage: 10 MB % 171.79/24.54 % (3688684)Instructions burned: 2 (million) % 171.79/24.54 % (3688684)------------------------------ % 171.79/24.54 % (3688684)------------------------------ % 171.79/24.54 % (3688686)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=1267844855:fmbsr=1.3:i=225729_2809 on theBenchmark for (2809ds/225729Mi) % 171.79/24.54 % (3688686)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 171.79/24.54 % (3688686)Terminated due to inappropriate strategy. % 171.79/24.54 % (3688686)------------------------------ % 171.79/24.54 % (3688686)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 171.79/24.54 % (3688686)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 171.79/24.54 % (3688686)CaDiCaL version: 2.1.3 % 171.79/24.54 % (3688686)Termination reason: Inappropriate % 171.79/24.54 % (3688686)Time elapsed: 0.002 s % 171.79/24.54 % (3688686)Peak memory usage: 11 MB % 171.79/24.54 % (3688686)Instructions burned: 2 (million) % 171.79/24.54 % (3688686)------------------------------ % 171.79/24.54 % (3688686)------------------------------ % 171.79/24.54 % (3688688)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=30886889:fmbsr=2:i=185024:ins=7_2809 on theBenchmark for (2809ds/185024Mi) % 171.79/24.54 % (3688688)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 171.79/24.54 % (3688688)Terminated due to inappropriate strategy. % 171.79/24.54 % (3688688)------------------------------ % 171.79/24.54 % (3688688)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 171.79/24.54 % (3688688)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 171.79/24.54 % (3688688)CaDiCaL version: 2.1.3 % 171.79/24.54 % (3688688)Termination reason: Inappropriate % 171.79/24.54 % (3688688)Time elapsed: 0.002 s % 171.79/24.54 % (3688688)Peak memory usage: 11 MB % 171.79/24.54 % (3688688)Instructions burned: 2 (million) % 171.79/24.54 % (3688688)------------------------------ % 171.79/24.54 % (3688688)------------------------------ % 171.79/24.54 % (3688690)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=2303651795:rtra=on_2808 on theBenchmark for (2808ds/0Mi) % 171.79/24.54 % (3688690)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 171.79/24.54 % (3688690)Terminated due to inappropriate strategy. % 171.79/24.54 % (3688690)------------------------------ % 171.79/24.54 % (3688690)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 171.79/24.54 % (3688690)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 171.79/24.54 % (3688690)CaDiCaL version: 2.1.3 % 171.79/24.54 % (3688690)Termination reason: Inappropriate % 171.79/24.54 % (3688690)Time elapsed: 0.002 s % 171.79/24.54 % (3688690)Peak memory usage: 11 MB % 171.79/24.54 % (3688690)Instructions burned: 2 (million) % 171.79/24.54 % (3688690)------------------------------ % 171.79/24.54 % (3688690)------------------------------ % 171.79/24.54 % (3688692)% WARNING: option uhcvi not known. % 171.79/24.54 % (3688692)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3388231838:i=271062:add=off:rtra=on:rawr=on_2808 on theBenchmark for (2808ds/271062Mi) % 180.41/25.83 % (3688670)Instruction limit reached! % 180.41/25.83 % (3688670)------------------------------ % 180.41/25.83 % (3688670)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 180.41/25.83 % (3688670)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 180.41/25.83 % (3688670)CaDiCaL version: 2.1.3 % 180.41/25.83 % (3688670)Termination reason: Instruction limit % 180.41/25.83 % (3688670)Termination phase: Saturation % 180.41/25.83 % (3688670)Time elapsed: 8.186 s % 180.41/25.83 % (3688670)Peak memory usage: 129 MB % 180.41/25.83 % (3688670)Instructions burned: 15852 (million) % 180.41/25.83 % (3688694)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3326407897:i=176048:add=on:rtra=on:rawr=on_2772 on theBenchmark for (2772ds/176048Mi) % 180.41/25.83 % (3688583)Instruction limit reached! % 180.41/25.83 % (3688583)------------------------------ % 180.41/25.83 % (3688583)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 180.41/25.83 % (3688583)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 180.41/25.83 % (3688583)CaDiCaL version: 2.1.3 % 180.41/25.83 % (3688583)Termination reason: Instruction limit % 180.41/25.83 % (3688583)Termination phase: Saturation % 180.41/25.83 % (3688583)Time elapsed: 23.366 s % 180.41/25.83 % (3688583)Peak memory usage: 1805 MB % 180.41/25.83 % (3688583)Instructions burned: 88030 (million) % 180.41/25.83 % (3688696)dis+10_1_sil=32000:si=on:sp=arity:random_seed=1913555592:i=206:fgj=on:rtra=on_2764 on theBenchmark for (2764ds/206Mi) % 180.41/25.83 % (3688696)Instruction limit reached! % 180.41/25.83 % (3688696)------------------------------ % 180.41/25.83 % (3688696)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 180.41/25.83 % (3688696)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 180.41/25.83 % (3688696)CaDiCaL version: 2.1.3 % 180.41/25.83 % (3688696)Termination reason: Instruction limit % 180.41/25.83 % (3688696)Termination phase: Saturation % 180.41/25.83 % (3688696)Time elapsed: 0.069 s % 180.41/25.83 % (3688696)Peak memory usage: 14 MB % 180.41/25.83 % (3688696)Instructions burned: 209 (million) % 180.41/25.83 % (3688698)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=1759301142:i=232:rtra=on_2763 on theBenchmark for (2763ds/232Mi) % 180.41/25.83 % (3688698)Instruction limit reached! % 180.41/25.83 % (3688698)------------------------------ % 180.41/25.83 % (3688698)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 180.41/25.83 % (3688698)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 180.41/25.83 % (3688698)CaDiCaL version: 2.1.3 % 180.41/25.83 % (3688698)Termination reason: Instruction limit % 180.41/25.83 % (3688698)Termination phase: Saturation % 180.41/25.83 % (3688698)Time elapsed: 0.076 s % 180.41/25.83 % (3688698)Peak memory usage: 13 MB % 180.41/25.83 % (3688698)Instructions burned: 234 (million) % 180.41/25.83 % (3688700)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=976506240:i=262:rtra=on_2762 on theBenchmark for (2762ds/262Mi) % 180.41/25.83 % (3688700)Instruction limit reached! % 180.41/25.83 % (3688700)------------------------------ % 180.41/25.83 % (3688700)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 180.41/25.83 % (3688700)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 180.41/25.83 % (3688700)CaDiCaL version: 2.1.3 % 180.41/25.83 % (3688700)Termination reason: Instruction limit % 180.41/25.83 % (3688700)Termination phase: Saturation % 180.41/25.83 % (3688700)Time elapsed: 0.084 s % 180.41/25.83 % (3688700)Peak memory usage: 13 MB % 180.41/25.83 % (3688700)Instructions burned: 263 (million) % 180.41/25.83 % (3688702)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=943182991:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2761 on theBenchmark for (2761ds/318Mi) % 180.41/25.83 % (3688672)Instruction limit reached! % 180.41/25.83 % (3688672)------------------------------ % 180.41/25.83 % (3688672)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 180.41/25.83 % (3688672)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 180.41/25.83 % (3688672)CaDiCaL version: 2.1.3 % 180.41/25.83 % (3688672)Termination reason: Instruction limit % 180.41/25.83 % (3688672)Termination phase: Saturation % 180.41/25.83 % (3688672)Time elapsed: 8.368 s % 180.41/25.83 % (3688672)Peak memory usage: 229 MB % 180.41/25.83 % (3688672)Instructions burned: 17628 (million) % 180.41/25.83 % (3688704)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=4279710560:i=1428:nm=2:rtra=on_2761 on theBenchmark for (2761ds/1428Mi) % 195.06/27.79 % (3688704)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 195.06/27.79 % (3688704)Terminated due to inappropriate strategy. % 195.06/27.79 % (3688704)------------------------------ % 195.06/27.79 % (3688704)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 195.06/27.79 % (3688704)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 195.06/27.79 % (3688704)CaDiCaL version: 2.1.3 % 195.06/27.79 % (3688704)Termination reason: Inappropriate % 195.06/27.79 % (3688704)Time elapsed: 0.002 s % 195.06/27.79 % (3688704)Peak memory usage: 10 MB % 195.06/27.79 % (3688704)Instructions burned: 2 (million) % 195.06/27.79 % (3688704)------------------------------ % 195.06/27.79 % (3688704)------------------------------ % 195.06/27.79 % (3688702)Instruction limit reached! % 195.06/27.79 % (3688702)------------------------------ % 195.06/27.79 % (3688702)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 195.06/27.79 % (3688702)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 195.06/27.79 % (3688702)CaDiCaL version: 2.1.3 % 195.06/27.79 % (3688702)Termination reason: Instruction limit % 195.06/27.79 % (3688702)Termination phase: Saturation % 195.06/27.79 % (3688702)Time elapsed: 0.091 s % 195.06/27.79 % (3688702)Peak memory usage: 13 MB % 195.06/27.79 % (3688702)Instructions burned: 319 (million) % 195.06/27.79 % (3688707)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=2790616201:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2760 on theBenchmark for (2760ds/1368Mi) % 195.06/27.79 % (3688706)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=2888283160:i=262:bd=preordered:rtra=on:fsd=on_2760 on theBenchmark for (2760ds/262Mi) % 195.06/27.79 % (3688706)Instruction limit reached! % 195.06/27.79 % (3688706)------------------------------ % 195.06/27.79 % (3688706)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 195.06/27.79 % (3688706)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 195.06/27.79 % (3688706)CaDiCaL version: 2.1.3 % 195.06/27.79 % (3688706)Termination reason: Instruction limit % 195.06/27.79 % (3688706)Termination phase: Saturation % 195.06/27.79 % (3688706)Time elapsed: 0.175 s % 195.06/27.79 % (3688706)Peak memory usage: 14 MB % 195.06/27.79 % (3688706)Instructions burned: 263 (million) % 195.06/27.79 % (3688710)ott-21_1_sil=16000:si=on:fs=off:random_seed=803778856:i=360:av=off:fsr=off:rtra=on_2758 on theBenchmark for (2758ds/360Mi) % 195.06/27.79 % (3688710)Instruction limit reached! % 195.06/27.79 % (3688710)------------------------------ % 195.06/27.79 % (3688710)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 195.06/27.79 % (3688710)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 195.06/27.79 % (3688710)CaDiCaL version: 2.1.3 % 195.06/27.79 % (3688710)Termination reason: Instruction limit % 195.06/27.79 % (3688710)Termination phase: Saturation % 195.06/27.79 % (3688710)Time elapsed: 0.162 s % 195.06/27.79 % (3688710)Peak memory usage: 13 MB % 195.06/27.79 % (3688710)Instructions burned: 363 (million) % 195.06/27.79 % (3688712)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2268125239:i=954:bd=all:rtra=on_2757 on theBenchmark for (2757ds/954Mi) % 195.06/27.79 % (3688707)Instruction limit reached! % 195.06/27.79 % (3688707)------------------------------ % 195.06/27.79 % (3688707)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 195.06/27.79 % (3688707)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 195.06/27.79 % (3688707)CaDiCaL version: 2.1.3 % 195.06/27.79 % (3688707)Termination reason: Instruction limit % 195.06/27.79 % (3688707)Termination phase: Saturation % 195.06/27.79 % (3688707)Time elapsed: 0.386 s % 195.06/27.79 % (3688707)Peak memory usage: 16 MB % 195.06/27.79 % (3688707)Instructions burned: 1370 (million) % 195.06/27.79 % (3688714)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=1131324644:fmbsr=1.3:i=1730:ins=25:rtra=on_2756 on theBenchmark for (2756ds/1730Mi) % 195.06/27.79 % (3688714)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 195.06/27.79 % (3688714)Terminated due to inappropriate strategy. % 195.06/27.79 % (3688714)------------------------------ % 195.06/27.79 % (3688714)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 195.06/27.79 % (3688714)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 195.06/27.79 % (3688714)CaDiCaL version: 2.1.3 % 195.06/27.79 % (3688714)Termination reason: Inappropriate % 195.06/27.79 % (3688714)Time elapsed: 0.0000 s % 219.90/31.26 % (3688714)Peak memory usage: 10 MB % 219.90/31.26 % (3688714)Instructions burned: 2 (million) % 219.90/31.26 % (3688714)------------------------------ % 219.90/31.26 % (3688714)------------------------------ % 219.90/31.26 % (3688716)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=4011454647:i=2358:rtra=on_2756 on theBenchmark for (2756ds/2358Mi) % 219.90/31.26 % (3688712)Instruction limit reached! % 219.90/31.26 % (3688712)------------------------------ % 219.90/31.26 % (3688712)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 219.90/31.26 % (3688712)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 219.90/31.26 % (3688712)CaDiCaL version: 2.1.3 % 219.90/31.26 % (3688712)Termination reason: Instruction limit % 219.90/31.26 % (3688712)Termination phase: Saturation % 219.90/31.26 % (3688712)Time elapsed: 0.630 s % 219.90/31.26 % (3688712)Peak memory usage: 16 MB % 219.90/31.26 % (3688712)Instructions burned: 954 (million) % 219.90/31.26 % (3688718)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=2120171619:i=1778:ins=1:rtra=on_2750 on theBenchmark for (2750ds/1778Mi) % 219.90/31.26 % (3688718)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 219.90/31.26 % (3688718)Terminated due to inappropriate strategy. % 219.90/31.26 % (3688718)------------------------------ % 219.90/31.26 % (3688718)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 219.90/31.26 % (3688718)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 219.90/31.26 % (3688718)CaDiCaL version: 2.1.3 % 219.90/31.26 % (3688718)Termination reason: Inappropriate % 219.90/31.26 % (3688718)Time elapsed: 0.001 s % 219.90/31.26 % (3688718)Peak memory usage: 10 MB % 219.90/31.26 % (3688718)Instructions burned: 2 (million) % 219.90/31.26 % (3688718)------------------------------ % 219.90/31.26 % (3688718)------------------------------ % 219.90/31.26 % (3688720)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=1879151954:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2750 on theBenchmark for (2750ds/1384Mi) % 219.90/31.26 % (3688716)Instruction limit reached! % 219.90/31.26 % (3688716)------------------------------ % 219.90/31.26 % (3688716)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 219.90/31.26 % (3688716)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 219.90/31.26 % (3688716)CaDiCaL version: 2.1.3 % 219.90/31.26 % (3688716)Termination reason: Instruction limit % 219.90/31.26 % (3688716)Termination phase: Saturation % 219.90/31.26 % (3688716)Time elapsed: 0.704 s % 219.90/31.26 % (3688716)Peak memory usage: 22 MB % 219.90/31.26 % (3688716)Instructions burned: 2359 (million) % 219.90/31.26 % (3688722)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=3690822617:i=1758:kws=inv_precedence:fsr=off:rtra=on_2749 on theBenchmark for (2749ds/1758Mi) % 219.90/31.26 % (3688722)Instruction limit reached! % 219.90/31.26 % (3688722)------------------------------ % 219.90/31.26 % (3688722)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 219.90/31.26 % (3688722)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 219.90/31.26 % (3688722)CaDiCaL version: 2.1.3 % 219.90/31.26 % (3688722)Termination reason: Instruction limit % 219.90/31.26 % (3688722)Termination phase: Saturation % 219.90/31.26 % (3688722)Time elapsed: 0.543 s % 219.90/31.26 % (3688722)Peak memory usage: 22 MB % 219.90/31.26 % (3688722)Instructions burned: 1760 (million) % 219.90/31.26 % (3688724)fmb+10_1_sil=64000:si=on:random_seed=701328024:i=44122:nm=2:rtra=on:gsp=on_2744 on theBenchmark for (2744ds/44122Mi) % 219.90/31.26 % (3688724)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 219.90/31.26 % (3688724)Terminated due to inappropriate strategy. % 219.90/31.26 % (3688724)------------------------------ % 219.90/31.26 % (3688724)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 219.90/31.26 % (3688724)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 219.90/31.26 % (3688724)CaDiCaL version: 2.1.3 % 219.90/31.26 % (3688724)Termination reason: Inappropriate % 219.90/31.26 % (3688724)Time elapsed: 0.001 s % 219.90/31.26 % (3688724)Peak memory usage: 10 MB % 219.90/31.26 % (3688724)Instructions burned: 2 (million) % 219.90/31.26 % (3688724)------------------------------ % 219.90/31.26 % (3688724)------------------------------ % 219.90/31.26 % (3688726)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=2077195864:i=19030:nm=5:rtra=on_2743 on theBenchmark for (2743ds/19030Mi) % 252.07/35.84 % (3688726)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 252.07/35.84 % (3688726)Terminated due to inappropriate strategy. % 252.07/35.84 % (3688726)------------------------------ % 252.07/35.84 % (3688726)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 252.07/35.84 % (3688726)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 252.07/35.84 % (3688726)CaDiCaL version: 2.1.3 % 252.07/35.84 % (3688726)Termination reason: Inappropriate % 252.07/35.84 % (3688726)Time elapsed: 0.001 s % 252.07/35.84 % (3688726)Peak memory usage: 10 MB % 252.07/35.84 % (3688726)Instructions burned: 2 (million) % 252.07/35.84 % (3688726)------------------------------ % 252.07/35.84 % (3688726)------------------------------ % 252.07/35.84 % (3688728)fmb+10_1_sil=64000:sas=cadical:si=on:fmbss=8:random_seed=3155955360:fmbsr=1.7:i=1840:rtra=on_2743 on theBenchmark for (2743ds/1840Mi) % 252.07/35.84 % (3688728)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 252.07/35.84 % (3688728)Terminated due to inappropriate strategy. % 252.07/35.84 % (3688728)------------------------------ % 252.07/35.84 % (3688728)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 252.07/35.84 % (3688728)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 252.07/35.84 % (3688728)CaDiCaL version: 2.1.3 % 252.07/35.84 % (3688728)Termination reason: Inappropriate % 252.07/35.84 % (3688728)Time elapsed: 0.001 s % 252.07/35.84 % (3688728)Peak memory usage: 10 MB % 252.07/35.84 % (3688728)Instructions burned: 2 (million) % 252.07/35.84 % (3688728)------------------------------ % 252.07/35.84 % (3688728)------------------------------ % 252.07/35.84 % (3688730)dis-4_1_sil=16000:drc=ordering:si=on:sp=const_frequency:sac=on:newcnf=on:random_seed=4169769212:i=10262:rtra=on_2743 on theBenchmark for (2743ds/10262Mi) % 252.07/35.84 % (3688720)Instruction limit reached! % 252.07/35.84 % (3688720)------------------------------ % 252.07/35.84 % (3688720)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 252.07/35.84 % (3688720)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 252.07/35.84 % (3688720)CaDiCaL version: 2.1.3 % 252.07/35.84 % (3688720)Termination reason: Instruction limit % 252.07/35.84 % (3688720)Termination phase: Saturation % 252.07/35.84 % (3688720)Time elapsed: 0.843 s % 252.07/35.84 % (3688720)Peak memory usage: 26 MB % 252.07/35.84 % (3688720)Instructions burned: 1386 (million) % 252.07/35.84 % (3688732)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:si=on:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1425655207:i=2944:ins=7:rtra=on:fdi=8:gsp=on_2741 on theBenchmark for (2741ds/2944Mi) % 252.07/35.84 % (3688732)Instruction limit reached! % 252.07/35.84 % (3688732)------------------------------ % 252.07/35.84 % (3688732)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 252.07/35.84 % (3688732)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 252.07/35.84 % (3688732)CaDiCaL version: 2.1.3 % 252.07/35.84 % (3688732)Termination reason: Instruction limit % 252.07/35.84 % (3688732)Termination phase: Saturation % 252.07/35.84 % (3688732)Time elapsed: 1.684 s % 252.07/35.84 % (3688732)Peak memory usage: 41 MB % 252.07/35.84 % (3688732)Instructions burned: 2945 (million) % 252.07/35.84 % (3688734)fmb+10_1_sil=16000:sas=cadical:si=on:bce=on:fmbss=77:random_seed=2546092399:i=12648:rtra=on_2724 on theBenchmark for (2724ds/12648Mi) % 252.07/35.84 % (3688734)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 252.07/35.84 % (3688734)Terminated due to inappropriate strategy. % 252.07/35.84 % (3688734)------------------------------ % 252.07/35.84 % (3688734)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 252.07/35.84 % (3688734)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 252.07/35.84 % (3688734)CaDiCaL version: 2.1.3 % 252.07/35.84 % (3688734)Termination reason: Inappropriate % 252.07/35.84 % (3688734)Time elapsed: 0.002 s % 252.07/35.84 % (3688734)Peak memory usage: 11 MB % 252.07/35.84 % (3688734)Instructions burned: 3 (million) % 252.07/35.84 % (3688734)------------------------------ % 252.07/35.84 % (3688734)------------------------------ % 252.07/35.84 % (3688736)fmb+10_1_fmbas=function:sil=32000:sas=cadical:si=on:fmbss=16:random_seed=3543234393:fmbsr=2.30978:i=4348:rtra=on_2724 on theBenchmark for (2724ds/4348Mi) % 252.07/35.84 % (3688736)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 252.07/35.84 % (3688736)Terminated due to inappropriate strategy. % 252.07/35.84 % (3688736)------------------------------ % 252.07/35.84 % (3688736)Version:Terminated % 300.10/42.54 % Vampire exiting % 300.10/42.54 Terminated %------------------------------------------------------------------------------