%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWW665_2 : TPTP v9.3.1. Released v6.1.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % Computer : n004.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 29 01:40:37 PM UTC 2026 % Result : Timeout 300.01s 42.54s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWW665_2 : TPTP v9.3.1. Released v6.1.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.11/0.17 % Computer : n004.cluster.edu % 0.11/0.17 % Model : x86_64 x86_64 % 0.11/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.17 % Memory : 8046.5625MB % 0.11/0.17 % OS : Linux 6.8.0-71-generic % 0.11/0.17 % CPULimit : 300 % 0.11/0.17 % WCLimit : 300 % 0.11/0.17 % DateTime : Mon Sep 28 14:24:37 UTC 2026 % 0.11/0.17 % CPUTime : % 0.11/0.17 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.11/0.20 Running first-order model finding % 0.11/0.20 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 4.57/1.07 % (385738)Will run a generic schedule for satisfiability detection. % 4.57/1.07 % (385747)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3491783024:i=116_2999 on theBenchmark for (2999ds/116Mi) % 4.57/1.07 % (385744)% WARNING: option uhcvi not known. % 4.57/1.07 % (385746)dis+10_1_sil=32000:sp=arity:random_seed=2895230620:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 4.57/1.07 % (385743)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2399562798_2999 on theBenchmark for (2999ds/0Mi) % 4.57/1.07 % (385744)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3645242246:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 4.57/1.07 % (385745)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1695242636:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 4.57/1.07 % (385749)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=88959328:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 4.57/1.07 % (385743)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 4.57/1.07 % (385743)Terminated due to inappropriate strategy. % 4.57/1.07 % (385743)------------------------------ % 4.57/1.07 % (385743)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 4.57/1.07 % (385743)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.57/1.07 % (385743)CaDiCaL version: 2.1.3 % 4.57/1.07 % (385743)Termination reason: Inappropriate % 4.57/1.07 % (385743)Time elapsed: 0.006 s % 4.57/1.07 % (385743)Peak memory usage: 11 MB % 4.57/1.07 % (385743)Instructions burned: 11 (million) % 4.57/1.07 % (385743)------------------------------ % 4.57/1.07 % (385743)------------------------------ % 4.57/1.07 % (385748)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3228041191:i=131_2999 on theBenchmark for (2999ds/131Mi) % 4.57/1.07 % (385756)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3236464744:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 4.57/1.07 % (385747)Instruction limit reached! % 4.57/1.07 % (385747)------------------------------ % 4.57/1.07 % (385747)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 4.57/1.07 % (385747)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.57/1.07 % (385747)CaDiCaL version: 2.1.3 % 4.57/1.07 % (385747)Termination reason: Instruction limit % 4.57/1.07 % (385747)Termination phase: Saturation % 4.57/1.07 % (385747)Time elapsed: 0.038 s % 4.57/1.07 % (385747)Peak memory usage: 13 MB % 4.57/1.07 % (385747)Instructions burned: 117 (million) % 4.57/1.07 % (385756)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 4.57/1.07 % (385756)Terminated due to inappropriate strategy. % 4.57/1.07 % (385756)------------------------------ % 4.57/1.07 % (385756)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 4.57/1.07 % (385756)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.57/1.07 % (385756)CaDiCaL version: 2.1.3 % 4.57/1.07 % (385756)Termination reason: Inappropriate % 4.57/1.07 % (385756)Time elapsed: 0.006 s % 4.57/1.07 % (385756)Peak memory usage: 11 MB % 4.57/1.07 % (385756)Instructions burned: 10 (million) % 4.57/1.07 % (385756)------------------------------ % 4.57/1.07 % (385756)------------------------------ % 4.57/1.07 % (385759)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1151474419:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 4.57/1.07 % (385760)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=2832584665:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi) % 4.57/1.07 % (385746)Instruction limit reached! % 4.57/1.07 % (385746)------------------------------ % 4.57/1.07 % (385746)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 4.57/1.07 % (385746)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.57/1.07 % (385746)CaDiCaL version: 2.1.3 % 4.57/1.07 % (385746)Termination reason: Instruction limit % 4.57/1.07 % (385746)Termination phase: Saturation % 4.57/1.07 % (385746)Time elapsed: 0.064 s % 4.57/1.07 % (385746)Peak memory usage: 13 MB % 4.57/1.07 % (385746)Instructions burned: 104 (million) % 4.57/1.07 % (385763)ott-21_1_sil=16000:fs=off:random_seed=813144689:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 4.57/1.07 % (385759)Instruction limit reached! % 4.57/1.07 % (385759)------------------------------ % 9.83/1.98 % (385759)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 9.83/1.98 % (385759)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.83/1.98 % (385759)CaDiCaL version: 2.1.3 % 9.83/1.98 % (385759)Termination reason: Instruction limit % 9.83/1.98 % (385759)Termination phase: Saturation % 9.83/1.98 % (385759)Time elapsed: 0.045 s % 9.83/1.98 % (385759)Peak memory usage: 13 MB % 9.83/1.98 % (385759)Instructions burned: 132 (million) % 9.83/1.98 % (385765)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1587452364:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 9.83/1.98 % (385749)Instruction limit reached! % 9.83/1.98 % (385749)------------------------------ % 9.83/1.98 % (385749)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 9.83/1.98 % (385749)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.83/1.98 % (385749)CaDiCaL version: 2.1.3 % 9.83/1.98 % (385749)Termination reason: Instruction limit % 9.83/1.98 % (385749)Termination phase: Saturation % 9.83/1.98 % (385749)Time elapsed: 0.104 s % 9.83/1.98 % (385749)Peak memory usage: 13 MB % 9.83/1.98 % (385749)Instructions burned: 160 (million) % 9.83/1.98 % (385767)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1080260072:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 9.83/1.98 % (385767)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 9.83/1.98 % (385767)Terminated due to inappropriate strategy. % 9.83/1.98 % (385767)------------------------------ % 9.83/1.98 % (385767)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 9.83/1.98 % (385767)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.83/1.98 % (385767)CaDiCaL version: 2.1.3 % 9.83/1.98 % (385767)Termination reason: Inappropriate % 9.83/1.98 % (385767)Time elapsed: 0.005 s % 9.83/1.98 % (385767)Peak memory usage: 11 MB % 9.83/1.98 % (385767)Instructions burned: 10 (million) % 9.83/1.98 % (385767)------------------------------ % 9.83/1.98 % (385767)------------------------------ % 9.83/1.98 % (385748)Instruction limit reached! % 9.83/1.98 % (385748)------------------------------ % 9.83/1.98 % (385748)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 9.83/1.98 % (385748)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.83/1.98 % (385748)CaDiCaL version: 2.1.3 % 9.83/1.98 % (385748)Termination reason: Instruction limit % 9.83/1.98 % (385748)Termination phase: Saturation % 9.83/1.98 % (385748)Time elapsed: 0.130 s % 9.83/1.98 % (385748)Peak memory usage: 13 MB % 9.83/1.98 % (385748)Instructions burned: 131 (million) % 9.83/1.98 % (385769)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3102258833:i=1179_2998 on theBenchmark for (2998ds/1179Mi) % 9.83/1.98 % (385770)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1195381748:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi) % 9.83/1.98 % (385770)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 9.83/1.98 % (385770)Terminated due to inappropriate strategy. % 9.83/1.98 % (385770)------------------------------ % 9.83/1.98 % (385770)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 9.83/1.98 % (385770)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.83/1.98 % (385770)CaDiCaL version: 2.1.3 % 9.83/1.98 % (385770)Termination reason: Inappropriate % 9.83/1.98 % (385770)Time elapsed: 0.005 s % 9.83/1.98 % (385770)Peak memory usage: 11 MB % 9.83/1.98 % (385770)Instructions burned: 10 (million) % 9.83/1.98 % (385770)------------------------------ % 9.83/1.98 % (385770)------------------------------ % 9.83/1.98 % (385763)Instruction limit reached! % 9.83/1.98 % (385763)------------------------------ % 9.83/1.98 % (385763)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 9.83/1.98 % (385763)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.83/1.98 % (385763)CaDiCaL version: 2.1.3 % 9.83/1.98 % (385763)Termination reason: Instruction limit % 9.83/1.98 % (385763)Termination phase: Saturation % 9.83/1.98 % (385763)Time elapsed: 0.096 s % 9.83/1.98 % (385763)Peak memory usage: 13 MB % 9.83/1.98 % (385763)Instructions burned: 182 (million) % 9.83/1.98 % (385775)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=3531868323: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) % 23.67/3.62 % (385781)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=513990641:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi) % 23.67/3.62 % (385765)Instruction limit reached! % 23.67/3.62 % (385765)------------------------------ % 23.67/3.62 % (385765)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 23.67/3.62 % (385765)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.67/3.62 % (385765)CaDiCaL version: 2.1.3 % 23.67/3.62 % (385765)Termination reason: Instruction limit % 23.67/3.62 % (385765)Termination phase: Saturation % 23.67/3.62 % (385765)Time elapsed: 0.203 s % 23.67/3.62 % (385765)Peak memory usage: 14 MB % 23.67/3.62 % (385765)Instructions burned: 480 (million) % 23.67/3.62 % (385785)fmb+10_1_sil=64000:random_seed=1993348669:i=22061:nm=2:gsp=on_2996 on theBenchmark for (2996ds/22061Mi) % 23.67/3.62 % (385785)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 23.67/3.62 % (385785)Terminated due to inappropriate strategy. % 23.67/3.62 % (385785)------------------------------ % 23.67/3.62 % (385785)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 23.67/3.62 % (385785)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.67/3.62 % (385785)CaDiCaL version: 2.1.3 % 23.67/3.62 % (385785)Termination reason: Inappropriate % 23.67/3.62 % (385785)Time elapsed: 0.019 s % 23.67/3.62 % (385785)Peak memory usage: 11 MB % 23.67/3.62 % (385785)Instructions burned: 10 (million) % 23.67/3.62 % (385785)------------------------------ % 23.67/3.62 % (385785)------------------------------ % 23.67/3.62 % (385793)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2919792636:i=9515:nm=5_2995 on theBenchmark for (2995ds/9515Mi) % 23.67/3.62 % (385793)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 23.67/3.62 % (385793)Terminated due to inappropriate strategy. % 23.67/3.62 % (385793)------------------------------ % 23.67/3.62 % (385793)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 23.67/3.62 % (385793)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.67/3.62 % (385793)CaDiCaL version: 2.1.3 % 23.67/3.62 % (385793)Termination reason: Inappropriate % 23.67/3.62 % (385793)Time elapsed: 0.005 s % 23.67/3.62 % (385793)Peak memory usage: 11 MB % 23.67/3.62 % (385793)Instructions burned: 10 (million) % 23.67/3.62 % (385793)------------------------------ % 23.67/3.62 % (385793)------------------------------ % 23.67/3.62 % (385797)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2398705229:fmbsr=1.7:i=920_2995 on theBenchmark for (2995ds/920Mi) % 23.67/3.62 % (385797)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 23.67/3.62 % (385797)Terminated due to inappropriate strategy. % 23.67/3.62 % (385797)------------------------------ % 23.67/3.62 % (385797)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 23.67/3.62 % (385797)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.67/3.62 % (385797)CaDiCaL version: 2.1.3 % 23.67/3.62 % (385797)Termination reason: Inappropriate % 23.67/3.62 % (385797)Time elapsed: 0.005 s % 23.67/3.62 % (385797)Peak memory usage: 10 MB % 23.67/3.62 % (385797)Instructions burned: 10 (million) % 23.67/3.62 % (385797)------------------------------ % 23.67/3.62 % (385797)------------------------------ % 23.67/3.62 % (385801)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1430031816:i=5131_2995 on theBenchmark for (2995ds/5131Mi) % 23.67/3.62 % (385760)Instruction limit reached! % 23.67/3.62 % (385760)------------------------------ % 23.67/3.62 % (385760)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 23.67/3.62 % (385760)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.67/3.62 % (385760)CaDiCaL version: 2.1.3 % 23.67/3.62 % (385760)Termination reason: Instruction limit % 23.67/3.62 % (385760)Termination phase: Saturation % 23.67/3.62 % (385760)Time elapsed: 0.569 s % 23.67/3.62 % (385760)Peak memory usage: 18 MB % 23.67/3.62 % (385760)Instructions burned: 684 (million) % 23.67/3.62 % (385809)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3170266809:i=1472:ins=7:fdi=8:gsp=on_2993 on theBenchmark for (2993ds/1472Mi) % 23.67/3.62 % (385775)Instruction limit reached! % 23.67/3.62 % (385775)------------------------------ % 23.67/3.62 % (385775)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 23.67/3.62 % (385775)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.84/4.35 % (385775)CaDiCaL version: 2.1.3 % 28.84/4.35 % (385775)Termination reason: Instruction limit % 28.84/4.35 % (385775)Termination phase: Saturation % 28.84/4.35 % (385775)Time elapsed: 0.623 s % 28.84/4.35 % (385775)Peak memory usage: 19 MB % 28.84/4.35 % (385775)Instructions burned: 692 (million) % 28.84/4.35 % (385821)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=1936746151:i=6324_2991 on theBenchmark for (2991ds/6324Mi) % 28.84/4.35 % (385781)Instruction limit reached! % 28.84/4.35 % (385781)------------------------------ % 28.84/4.35 % (385781)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 28.84/4.35 % (385781)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.84/4.35 % (385781)CaDiCaL version: 2.1.3 % 28.84/4.35 % (385781)Termination reason: Instruction limit % 28.84/4.35 % (385781)Termination phase: Saturation % 28.84/4.35 % (385781)Time elapsed: 0.657 s % 28.84/4.35 % (385781)Peak memory usage: 19 MB % 28.84/4.35 % (385781)Instructions burned: 879 (million) % 28.84/4.35 % (385821)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 28.84/4.35 % (385821)Terminated due to inappropriate strategy. % 28.84/4.35 % (385821)------------------------------ % 28.84/4.35 % (385821)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 28.84/4.35 % (385821)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.84/4.35 % (385821)CaDiCaL version: 2.1.3 % 28.84/4.35 % (385821)Termination reason: Inappropriate % 28.84/4.35 % (385821)Time elapsed: 0.009 s % 28.84/4.35 % (385821)Peak memory usage: 11 MB % 28.84/4.35 % (385821)Instructions burned: 11 (million) % 28.84/4.35 % (385821)------------------------------ % 28.84/4.35 % (385821)------------------------------ % 28.84/4.35 % (385823)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1191973934:fmbsr=2.30978:i=2174_2990 on theBenchmark for (2990ds/2174Mi) % 28.84/4.35 % (385823)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 28.84/4.35 % (385823)Terminated due to inappropriate strategy. % 28.84/4.35 % (385823)------------------------------ % 28.84/4.35 % (385823)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 28.84/4.35 % (385823)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.84/4.35 % (385823)CaDiCaL version: 2.1.3 % 28.84/4.35 % (385823)Termination reason: Inappropriate % 28.84/4.35 % (385823)Time elapsed: 0.007 s % 28.84/4.35 % (385823)Peak memory usage: 11 MB % 28.84/4.35 % (385823)Instructions burned: 10 (million) % 28.84/4.35 % (385823)------------------------------ % 28.84/4.35 % (385823)------------------------------ % 28.84/4.35 % (385824)ott-2_1_sil=16000:newcnf=on:random_seed=1849890952:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2990 on theBenchmark for (2990ds/869Mi) % 28.84/4.35 % (385828)ott+10_1_sil=32000:tgt=ground:random_seed=246953141:i=5114:av=off_2990 on theBenchmark for (2990ds/5114Mi) % 28.84/4.35 % (385769)Instruction limit reached! % 28.84/4.35 % (385769)------------------------------ % 28.84/4.35 % (385769)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 28.84/4.35 % (385769)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.84/4.35 % (385769)CaDiCaL version: 2.1.3 % 28.84/4.35 % (385769)Termination reason: Instruction limit % 28.84/4.35 % (385769)Termination phase: Saturation % 28.84/4.35 % (385769)Time elapsed: 0.991 s % 28.84/4.35 % (385769)Peak memory usage: 22 MB % 28.84/4.35 % (385769)Instructions burned: 1180 (million) % 28.84/4.35 % (385845)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=661868337:i=54282_2988 on theBenchmark for (2988ds/54282Mi) % 28.84/4.35 % (385845)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 28.84/4.35 % (385845)Terminated due to inappropriate strategy. % 28.84/4.35 % (385845)------------------------------ % 28.84/4.35 % (385845)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 28.84/4.35 % (385845)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.84/4.35 % (385845)CaDiCaL version: 2.1.3 % 28.84/4.35 % (385845)Termination reason: Inappropriate % 28.84/4.35 % (385845)Time elapsed: 0.009 s % 28.84/4.35 % (385845)Peak memory usage: 11 MB % 28.84/4.35 % (385845)Instructions burned: 11 (million) % 28.84/4.35 % (385845)------------------------------ % 28.84/4.35 % (385845)------------------------------ % 28.84/4.35 % (385849)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=1703386603:i=3512:aac=none_2987 on theBenchmark for (2987ds/3512Mi) % 28.84/4.35 % (385824)Instruction limit reached! % 110.48/15.85 % (385824)------------------------------ % 110.48/15.85 % (385824)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 110.48/15.85 % (385824)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 110.48/15.85 % (385824)CaDiCaL version: 2.1.3 % 110.48/15.85 % (385824)Termination reason: Instruction limit % 110.48/15.85 % (385824)Termination phase: Saturation % 110.48/15.85 % (385824)Time elapsed: 0.825 s % 110.48/15.85 % (385824)Peak memory usage: 18 MB % 110.48/15.85 % (385824)Instructions burned: 869 (million) % 110.48/15.85 % (385871)dis+21_1_sil=32000:sas=cadical:random_seed=2728966381:i=3773:amm=off_2982 on theBenchmark for (2982ds/3773Mi) % 110.48/15.85 % (385809)Instruction limit reached! % 110.48/15.85 % (385809)------------------------------ % 110.48/15.85 % (385809)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 110.48/15.85 % (385809)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 110.48/15.85 % (385809)CaDiCaL version: 2.1.3 % 110.48/15.85 % (385809)Termination reason: Instruction limit % 110.48/15.85 % (385809)Termination phase: Saturation % 110.48/15.85 % (385809)Time elapsed: 1.208 s % 110.48/15.85 % (385809)Peak memory usage: 31 MB % 110.48/15.85 % (385809)Instructions burned: 1472 (million) % 110.48/15.85 % (385873)ott+11_1_sil=16000:gs=on:random_seed=2741985311:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2980 on theBenchmark for (2980ds/2251Mi) % 110.48/15.85 % (385801)Instruction limit reached! % 110.48/15.85 % (385801)------------------------------ % 110.48/15.85 % (385801)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 110.48/15.85 % (385801)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 110.48/15.85 % (385801)CaDiCaL version: 2.1.3 % 110.48/15.85 % (385801)Termination reason: Instruction limit % 110.48/15.85 % (385801)Termination phase: Saturation % 110.48/15.85 % (385801)Time elapsed: 1.765 s % 110.48/15.85 % (385801)Peak memory usage: 36 MB % 110.48/15.85 % (385801)Instructions burned: 5134 (million) % 110.48/15.85 % (385936)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=1223509374:fmbsr=1.6:i=67534_2977 on theBenchmark for (2977ds/67534Mi) % 110.48/15.85 % (385936)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 110.48/15.85 % (385936)Terminated due to inappropriate strategy. % 110.48/15.85 % (385936)------------------------------ % 110.48/15.85 % (385936)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 110.48/15.85 % (385936)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 110.48/15.85 % (385936)CaDiCaL version: 2.1.3 % 110.48/15.85 % (385936)Termination reason: Inappropriate % 110.48/15.85 % (385936)Time elapsed: 0.003 s % 110.48/15.85 % (385936)Peak memory usage: 11 MB % 110.48/15.85 % (385936)Instructions burned: 10 (million) % 110.48/15.85 % (385936)------------------------------ % 110.48/15.85 % (385936)------------------------------ % 110.48/15.85 % (385945)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=2990337221:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2977 on theBenchmark for (2977ds/4591Mi) % 110.48/15.85 % (385873)Instruction limit reached! % 110.48/15.85 % (385873)------------------------------ % 110.48/15.85 % (385873)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 110.48/15.85 % (385873)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 110.48/15.85 % (385873)CaDiCaL version: 2.1.3 % 110.48/15.85 % (385873)Termination reason: Instruction limit % 110.48/15.85 % (385873)Termination phase: Saturation % 110.48/15.85 % (385873)Time elapsed: 1.244 s % 110.48/15.85 % (385873)Peak memory usage: 20 MB % 110.48/15.85 % (385873)Instructions burned: 2251 (million) % 110.48/15.85 % (386032)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=754545027:i=29340_2968 on theBenchmark for (2968ds/29340Mi) % 110.48/15.85 % (385849)Instruction limit reached! % 110.48/15.85 % (385849)------------------------------ % 110.48/15.85 % (385849)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 110.48/15.85 % (385849)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 110.48/15.85 % (385849)CaDiCaL version: 2.1.3 % 110.48/15.85 % (385849)Termination reason: Instruction limit % 110.48/15.85 % (385849)Termination phase: Saturation % 110.48/15.85 % (385849)Time elapsed: 2.053 s % 110.48/15.85 % (385849)Peak memory usage: 33 MB % 110.48/15.85 % (385849)Instructions burned: 3512 (million) % 110.48/15.85 % (386034)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=1840566531:i=5211_2966 on theBenchmark for (2966ds/5211Mi) % 110.48/15.85 % (385945)Instruction limit reached! % 123.98/17.75 % (385945)------------------------------ % 123.98/17.75 % (385945)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 123.98/17.75 % (385945)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 123.98/17.75 % (385945)CaDiCaL version: 2.1.3 % 123.98/17.75 % (385945)Termination reason: Instruction limit % 123.98/17.75 % (385945)Termination phase: Saturation % 123.98/17.75 % (385945)Time elapsed: 1.108 s % 123.98/17.75 % (385945)Peak memory usage: 46 MB % 123.98/17.75 % (385945)Instructions burned: 4592 (million) % 123.98/17.75 % (386036)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=3945808422:i=5497:nm=2_2965 on theBenchmark for (2965ds/5497Mi) % 123.98/17.75 % (386036)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 123.98/17.75 % (386036)Terminated due to inappropriate strategy. % 123.98/17.75 % (386036)------------------------------ % 123.98/17.75 % (386036)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 123.98/17.75 % (386036)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 123.98/17.75 % (386036)CaDiCaL version: 2.1.3 % 123.98/17.75 % (386036)Termination reason: Inappropriate % 123.98/17.75 % (386036)Time elapsed: 0.003 s % 123.98/17.75 % (386036)Peak memory usage: 11 MB % 123.98/17.75 % (386036)Instructions burned: 11 (million) % 123.98/17.75 % (386036)------------------------------ % 123.98/17.75 % (386036)------------------------------ % 123.98/17.75 % (386038)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=2179597350:fmbsr=2:i=46332_2965 on theBenchmark for (2965ds/46332Mi) % 123.98/17.75 % (386038)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 123.98/17.75 % (386038)Terminated due to inappropriate strategy. % 123.98/17.75 % (386038)------------------------------ % 123.98/17.75 % (386038)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 123.98/17.75 % (386038)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 123.98/17.75 % (386038)CaDiCaL version: 2.1.3 % 123.98/17.75 % (386038)Termination reason: Inappropriate % 123.98/17.75 % (386038)Time elapsed: 0.003 s % 123.98/17.75 % (386038)Peak memory usage: 11 MB % 123.98/17.75 % (386038)Instructions burned: 11 (million) % 123.98/17.75 % (386038)------------------------------ % 123.98/17.75 % (386038)------------------------------ % 123.98/17.75 % (386040)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=31243218:i=14071_2965 on theBenchmark for (2965ds/14071Mi) % 123.98/17.75 % (386040)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 123.98/17.75 % (386040)Terminated due to inappropriate strategy. % 123.98/17.75 % (386040)------------------------------ % 123.98/17.75 % (386040)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 123.98/17.75 % (386040)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 123.98/17.75 % (386040)CaDiCaL version: 2.1.3 % 123.98/17.75 % (386040)Termination reason: Inappropriate % 123.98/17.75 % (386040)Time elapsed: 0.003 s % 123.98/17.75 % (386040)Peak memory usage: 11 MB % 123.98/17.75 % (386040)Instructions burned: 11 (million) % 123.98/17.75 % (386040)------------------------------ % 123.98/17.75 % (386040)------------------------------ % 123.98/17.75 % (386042)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1354452256:i=22565:add=on:rawr=on_2965 on theBenchmark for (2965ds/22565Mi) % 123.98/17.75 % (385871)Instruction limit reached! % 123.98/17.75 % (385871)------------------------------ % 123.98/17.75 % (385871)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 123.98/17.75 % (385871)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 123.98/17.75 % (385871)CaDiCaL version: 2.1.3 % 123.98/17.75 % (385871)Termination reason: Instruction limit % 123.98/17.75 % (385871)Termination phase: Saturation % 123.98/17.75 % (385871)Time elapsed: 1.985 s % 123.98/17.75 % (385871)Peak memory usage: 32 MB % 123.98/17.75 % (385871)Instructions burned: 3774 (million) % 123.98/17.75 % (386044)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=2891163877:i=8173:av=off_2962 on theBenchmark for (2962ds/8173Mi) % 123.98/17.75 % (385828)Instruction limit reached! % 123.98/17.75 % (385828)------------------------------ % 123.98/17.75 % (385828)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 123.98/17.75 % (385828)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 123.98/17.75 % (385828)CaDiCaL version: 2.1.3 % 123.98/17.75 % (385828)Termination reason: Instruction limit % 123.98/17.75 % (385828)Termination phase: Saturation % 132.50/18.96 % (385828)Time elapsed: 3.168 s % 132.50/18.96 % (385828)Peak memory usage: 40 MB % 132.50/18.96 % (385828)Instructions burned: 5117 (million) % 132.50/18.96 % (386046)dis+10_16:1_sil=16000:random_seed=205671081:i=9155:fsr=off_2958 on theBenchmark for (2958ds/9155Mi) % 132.50/18.96 % (386034)Instruction limit reached! % 132.50/18.96 % (386034)------------------------------ % 132.50/18.96 % (386034)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 132.50/18.96 % (386034)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 132.50/18.96 % (386034)CaDiCaL version: 2.1.3 % 132.50/18.96 % (386034)Termination reason: Instruction limit % 132.50/18.96 % (386034)Termination phase: Saturation % 132.50/18.96 % (386034)Time elapsed: 2.677 s % 132.50/18.96 % (386034)Peak memory usage: 46 MB % 132.50/18.96 % (386034)Instructions burned: 5212 (million) % 132.50/18.96 % (386048)ott-3_8_sil=64000:random_seed=1379118314:i=20139:bs=on_2939 on theBenchmark for (2939ds/20139Mi) % 132.50/18.96 % (386044)Instruction limit reached! % 132.50/18.96 % (386044)------------------------------ % 132.50/18.96 % (386044)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 132.50/18.96 % (386044)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 132.50/18.96 % (386044)CaDiCaL version: 2.1.3 % 132.50/18.96 % (386044)Termination reason: Instruction limit % 132.50/18.96 % (386044)Termination phase: Saturation % 132.50/18.96 % (386044)Time elapsed: 4.770 s % 132.50/18.96 % (386044)Peak memory usage: 58 MB % 132.50/18.96 % (386044)Instructions burned: 8173 (million) % 132.50/18.96 % (386050)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=2064168577:fmbsr=2:i=32576_2914 on theBenchmark for (2914ds/32576Mi) % 132.50/18.96 % (386050)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 132.50/18.96 % (386050)Terminated due to inappropriate strategy. % 132.50/18.96 % (386050)------------------------------ % 132.50/18.96 % (386050)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 132.50/18.96 % (386050)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 132.50/18.96 % (386050)CaDiCaL version: 2.1.3 % 132.50/18.96 % (386050)Termination reason: Inappropriate % 132.50/18.96 % (386050)Time elapsed: 0.006 s % 132.50/18.96 % (386050)Peak memory usage: 11 MB % 132.50/18.96 % (386050)Instructions burned: 11 (million) % 132.50/18.96 % (386050)------------------------------ % 132.50/18.96 % (386050)------------------------------ % 132.50/18.96 % (386052)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=4240181080:i=11404_2913 on theBenchmark for (2913ds/11404Mi) % 132.50/18.96 % (386046)Instruction limit reached! % 132.50/18.96 % (386046)------------------------------ % 132.50/18.96 % (386046)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 132.50/18.96 % (386046)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 132.50/18.96 % (386046)CaDiCaL version: 2.1.3 % 132.50/18.96 % (386046)Termination reason: Instruction limit % 132.50/18.96 % (386046)Termination phase: Saturation % 132.50/18.96 % (386046)Time elapsed: 4.764 s % 132.50/18.96 % (386046)Peak memory usage: 56 MB % 132.50/18.96 % (386046)Instructions burned: 9157 (million) % 132.50/18.96 % (386054)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=2074853010:i=14134_2910 on theBenchmark for (2910ds/14134Mi) % 132.50/18.96 % (386042)Instruction limit reached! % 132.50/18.96 % (386042)------------------------------ % 132.50/18.96 % (386042)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 132.50/18.96 % (386042)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 132.50/18.96 % (386042)CaDiCaL version: 2.1.3 % 132.50/18.96 % (386042)Termination reason: Instruction limit % 132.50/18.96 % (386042)Termination phase: Saturation % 132.50/18.96 % (386042)Time elapsed: 8.103 s % 132.50/18.96 % (386042)Peak memory usage: 138 MB % 132.50/18.96 % (386042)Instructions burned: 22565 (million) % 132.50/18.96 % (386056)dis+33_16_sil=32000:sac=on:random_seed=1179294278:i=15851:nm=0_2884 on theBenchmark for (2884ds/15851Mi) % 132.50/18.96 % (386052)Instruction limit reached! % 132.50/18.96 % (386052)------------------------------ % 132.50/18.96 % (386052)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 132.50/18.96 % (386052)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 132.50/18.96 % (386052)CaDiCaL version: 2.1.3 % 132.50/18.96 % (386052)Termination reason: Instruction limit % 132.50/18.96 % (386052)Termination phase: Saturation % 132.50/18.96 % (386052)Time elapsed: 6.994 s % 132.50/18.96 % (386052)Peak memory usage: 69 MB % 132.50/18.96 % (386052)Instructions burned: 11405 (million) % 132.50/18.96 % (386401)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=197427810:avsq=on:i=17627:add=on:amm=off_2843 on theBenchmark for (2843ds/17627Mi) % 190.93/27.13 % (386056)Instruction limit reached! % 190.93/27.13 % (386056)------------------------------ % 190.93/27.13 % (386056)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 190.93/27.13 % (386056)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 190.93/27.13 % (386056)CaDiCaL version: 2.1.3 % 190.93/27.13 % (386056)Termination reason: Instruction limit % 190.93/27.13 % (386056)Termination phase: Saturation % 190.93/27.13 % (386056)Time elapsed: 4.502 s % 190.93/27.13 % (386056)Peak memory usage: 102 MB % 190.93/27.13 % (386056)Instructions burned: 15852 (million) % 190.93/27.13 % (386403)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=4276130136:s2a=on:i=53295_2838 on theBenchmark for (2838ds/53295Mi) % 190.93/27.13 % (386032)Instruction limit reached! % 190.93/27.13 % (386032)------------------------------ % 190.93/27.13 % (386032)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 190.93/27.13 % (386032)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 190.93/27.13 % (386032)CaDiCaL version: 2.1.3 % 190.93/27.13 % (386032)Termination reason: Instruction limit % 190.93/27.13 % (386032)Termination phase: Saturation % 190.93/27.13 % (386032)Time elapsed: 13.351 s % 190.93/27.13 % (386032)Peak memory usage: 177 MB % 190.93/27.13 % (386032)Instructions burned: 29342 (million) % 190.93/27.13 % (386405)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=945854511:i=26857:ins=20_2834 on theBenchmark for (2834ds/26857Mi) % 190.93/27.13 % (386405)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 190.93/27.13 % (386405)Terminated due to inappropriate strategy. % 190.93/27.13 % (386405)------------------------------ % 190.93/27.13 % (386405)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 190.93/27.13 % (386405)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 190.93/27.13 % (386405)CaDiCaL version: 2.1.3 % 190.93/27.13 % (386405)Termination reason: Inappropriate % 190.93/27.13 % (386405)Time elapsed: 0.005 s % 190.93/27.13 % (386405)Peak memory usage: 11 MB % 190.93/27.13 % (386405)Instructions burned: 10 (million) % 190.93/27.13 % (386405)------------------------------ % 190.93/27.13 % (386405)------------------------------ % 190.93/27.13 % (386407)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=3684633051:i=28120:bs=on:fsr=off_2833 on theBenchmark for (2833ds/28120Mi) % 190.93/27.13 % (386054)Instruction limit reached! % 190.93/27.13 % (386054)------------------------------ % 190.93/27.13 % (386054)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 190.93/27.13 % (386054)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 190.93/27.13 % (386054)CaDiCaL version: 2.1.3 % 190.93/27.13 % (386054)Termination reason: Instruction limit % 190.93/27.13 % (386054)Termination phase: Saturation % 190.93/27.13 % (386054)Time elapsed: 8.529 s % 190.93/27.13 % (386054)Peak memory usage: 78 MB % 190.93/27.13 % (386054)Instructions burned: 14134 (million) % 190.93/27.13 % (386409)fmb+10_1_sil=256000:fmbss=7:random_seed=3522841019:fmbsr=1.6:i=182295_2825 on theBenchmark for (2825ds/182295Mi) % 190.93/27.13 % (386409)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 190.93/27.13 % (386409)Terminated due to inappropriate strategy. % 190.93/27.13 % (386409)------------------------------ % 190.93/27.13 % (386409)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 190.93/27.13 % (386409)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 190.93/27.13 % (386409)CaDiCaL version: 2.1.3 % 190.93/27.13 % (386409)Termination reason: Inappropriate % 190.93/27.13 % (386409)Time elapsed: 0.005 s % 190.93/27.13 % (386409)Peak memory usage: 11 MB % 190.93/27.13 % (386409)Instructions burned: 10 (million) % 190.93/27.13 % (386409)------------------------------ % 190.93/27.13 % (386409)------------------------------ % 190.93/27.13 % (386411)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=2189209240:i=44625:gsp=on_2824 on theBenchmark for (2824ds/44625Mi) % 190.93/27.13 % (386411)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 190.93/27.13 % (386411)Terminated due to inappropriate strategy. % 190.93/27.13 % (386411)------------------------------ % 190.93/27.13 % (386411)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 190.93/27.13 % (386411)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 190.93/27.13 % (386411)CaDiCaL version: 2.1.3 % 190.93/27.13 % (386411)Termination reason: Inappropriate % 205.40/29.26 % (386411)Time elapsed: 0.006 s % 205.40/29.26 % (386411)Peak memory usage: 11 MB % 205.40/29.26 % (386411)Instructions burned: 13 (million) % 205.40/29.26 % (386411)------------------------------ % 205.40/29.26 % (386411)------------------------------ % 205.40/29.26 % (386413)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=3744664252:i=160505_2824 on theBenchmark for (2824ds/160505Mi) % 205.40/29.26 % (386413)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 205.40/29.26 % (386413)Terminated due to inappropriate strategy. % 205.40/29.26 % (386413)------------------------------ % 205.40/29.26 % (386413)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 205.40/29.26 % (386413)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 205.40/29.26 % (386413)CaDiCaL version: 2.1.3 % 205.40/29.26 % (386413)Termination reason: Inappropriate % 205.40/29.26 % (386413)Time elapsed: 0.005 s % 205.40/29.26 % (386413)Peak memory usage: 11 MB % 205.40/29.26 % (386413)Instructions burned: 10 (million) % 205.40/29.26 % (386413)------------------------------ % 205.40/29.26 % (386413)------------------------------ % 205.40/29.26 % (386415)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=108497790:fmbsr=1.3:i=225729_2824 on theBenchmark for (2824ds/225729Mi) % 205.40/29.26 % (386415)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 205.40/29.26 % (386415)Terminated due to inappropriate strategy. % 205.40/29.26 % (386415)------------------------------ % 205.40/29.26 % (386415)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 205.40/29.26 % (386415)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 205.40/29.26 % (386415)CaDiCaL version: 2.1.3 % 205.40/29.26 % (386415)Termination reason: Inappropriate % 205.40/29.26 % (386415)Time elapsed: 0.006 s % 205.40/29.26 % (386415)Peak memory usage: 11 MB % 205.40/29.26 % (386415)Instructions burned: 11 (million) % 205.40/29.26 % (386415)------------------------------ % 205.40/29.26 % (386415)------------------------------ % 205.40/29.26 % (386417)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=950622035:fmbsr=2:i=185024:ins=7_2824 on theBenchmark for (2824ds/185024Mi) % 205.40/29.26 % (386417)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 205.40/29.26 % (386417)Terminated due to inappropriate strategy. % 205.40/29.26 % (386417)------------------------------ % 205.40/29.26 % (386417)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 205.40/29.26 % (386417)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 205.40/29.26 % (386417)CaDiCaL version: 2.1.3 % 205.40/29.26 % (386417)Termination reason: Inappropriate % 205.40/29.26 % (386417)Time elapsed: 0.006 s % 205.40/29.26 % (386417)Peak memory usage: 11 MB % 205.40/29.26 % (386417)Instructions burned: 11 (million) % 205.40/29.26 % (386417)------------------------------ % 205.40/29.26 % (386417)------------------------------ % 205.40/29.26 % (386419)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=3582911568:rtra=on_2823 on theBenchmark for (2823ds/0Mi) % 205.40/29.26 % (386419)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 205.40/29.26 % (386419)Terminated due to inappropriate strategy. % 205.40/29.26 % (386419)------------------------------ % 205.40/29.26 % (386419)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 205.40/29.26 % (386419)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 205.40/29.26 % (386419)CaDiCaL version: 2.1.3 % 205.40/29.26 % (386419)Termination reason: Inappropriate % 205.40/29.26 % (386419)Time elapsed: 0.007 s % 205.40/29.26 % (386419)Peak memory usage: 11 MB % 205.40/29.26 % (386419)Instructions burned: 12 (million) % 205.40/29.26 % (386419)------------------------------ % 205.40/29.26 % (386419)------------------------------ % 205.40/29.26 % (386421)% WARNING: option uhcvi not known. % 205.40/29.26 % (386421)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=4176214764:i=271062:add=off:rtra=on:rawr=on_2823 on theBenchmark for (2823ds/271062Mi) % 205.40/29.26 % (386048)Instruction limit reached! % 205.40/29.26 % (386048)------------------------------ % 205.40/29.26 % (386048)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 205.40/29.26 % (386048)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 205.40/29.26 % (386048)CaDiCaL version: 2.1.3 % 205.40/29.26 % (386048)Termination reason: Instruction limit % 205.40/29.26 % (386048)Termination phase: Saturation % 205.40/29.26 % (386048)Time elapsed: 12.705 s % 205.40/29.26 % (386048)Peak memory usage: 112 MB % 205.40/29.26 % (386048)Instructions burned: 20139 (million) % 213.42/30.39 % (386423)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1522845846:i=176048:add=on:rtra=on:rawr=on_2812 on theBenchmark for (2812ds/176048Mi) % 213.42/30.39 % (386401)Instruction limit reached! % 213.42/30.39 % (386401)------------------------------ % 213.42/30.39 % (386401)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 213.42/30.39 % (386401)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 213.42/30.39 % (386401)CaDiCaL version: 2.1.3 % 213.42/30.39 % (386401)Termination reason: Instruction limit % 213.42/30.39 % (386401)Termination phase: Saturation % 213.42/30.39 % (386401)Time elapsed: 10.510 s % 213.42/30.39 % (386401)Peak memory usage: 131 MB % 213.42/30.39 % (386401)Instructions burned: 17628 (million) % 213.42/30.39 % (386427)dis+10_1_sil=32000:si=on:sp=arity:random_seed=1236593800:i=206:fgj=on:rtra=on_2738 on theBenchmark for (2738ds/206Mi) % 213.42/30.39 % (386427)Instruction limit reached! % 213.42/30.39 % (386427)------------------------------ % 213.42/30.39 % (386427)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 213.42/30.39 % (386427)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 213.42/30.39 % (386427)CaDiCaL version: 2.1.3 % 213.42/30.39 % (386427)Termination reason: Instruction limit % 213.42/30.39 % (386427)Termination phase: Saturation % 213.42/30.39 % (386427)Time elapsed: 0.127 s % 213.42/30.39 % (386427)Peak memory usage: 14 MB % 213.42/30.39 % (386427)Instructions burned: 207 (million) % 213.42/30.39 % (386429)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=3965709316:i=232:rtra=on_2736 on theBenchmark for (2736ds/232Mi) % 213.42/30.39 % (386429)Instruction limit reached! % 213.42/30.39 % (386429)------------------------------ % 213.42/30.39 % (386429)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 213.42/30.39 % (386429)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 213.42/30.39 % (386429)CaDiCaL version: 2.1.3 % 213.42/30.39 % (386429)Termination reason: Instruction limit % 213.42/30.39 % (386429)Termination phase: Saturation % 213.42/30.39 % (386429)Time elapsed: 0.142 s % 213.42/30.39 % (386429)Peak memory usage: 14 MB % 213.42/30.39 % (386429)Instructions burned: 233 (million) % 213.42/30.39 % (386431)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=3943218021:i=262:rtra=on_2735 on theBenchmark for (2735ds/262Mi) % 213.42/30.39 % (386431)Instruction limit reached! % 213.42/30.39 % (386431)------------------------------ % 213.42/30.39 % (386431)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 213.42/30.39 % (386431)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 213.42/30.39 % (386431)CaDiCaL version: 2.1.3 % 213.42/30.39 % (386431)Termination reason: Instruction limit % 213.42/30.39 % (386431)Termination phase: Saturation % 213.42/30.39 % (386431)Time elapsed: 0.163 s % 213.42/30.39 % (386431)Peak memory usage: 14 MB % 213.42/30.39 % (386431)Instructions burned: 263 (million) % 213.42/30.39 % (386433)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=745424782:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2733 on theBenchmark for (2733ds/318Mi) % 213.42/30.39 % (386433)Instruction limit reached! % 213.42/30.39 % (386433)------------------------------ % 213.42/30.39 % (386433)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 213.42/30.39 % (386433)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 213.42/30.39 % (386433)CaDiCaL version: 2.1.3 % 213.42/30.39 % (386433)Termination reason: Instruction limit % 213.42/30.39 % (386433)Termination phase: Saturation % 213.42/30.39 % (386433)Time elapsed: 0.213 s % 213.42/30.39 % (386433)Peak memory usage: 15 MB % 213.42/30.39 % (386433)Instructions burned: 319 (million) % 213.42/30.39 % (386435)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=563799685:i=1428:nm=2:rtra=on_2731 on theBenchmark for (2731ds/1428Mi) % 213.42/30.39 % (386435)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 213.42/30.39 % (386435)Terminated due to inappropriate strategy. % 213.42/30.39 % (386435)------------------------------ % 213.42/30.39 % (386435)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 213.42/30.39 % (386435)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 213.42/30.39 % (386435)CaDiCaL version: 2.1.3 % 213.42/30.39 % (386435)Termination reason: Inappropriate % 213.42/30.39 % (386435)Time elapsed: 0.006 s % 213.42/30.39 % (386435)Peak memory usage: 11 MB % 213.42/30.39 % (386435)Instructions burned: 11 (million) % 213.42/30.39 % (386435)------------------------------ % 224.46/31.95 % (386435)------------------------------ % 224.46/31.95 % (386437)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=3874062823:i=262:bd=preordered:rtra=on:fsd=on_2730 on theBenchmark for (2730ds/262Mi) % 224.46/31.95 % (386437)Instruction limit reached! % 224.46/31.95 % (386437)------------------------------ % 224.46/31.95 % (386437)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 224.46/31.95 % (386437)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 224.46/31.95 % (386437)CaDiCaL version: 2.1.3 % 224.46/31.95 % (386437)Termination reason: Instruction limit % 224.46/31.95 % (386437)Termination phase: Saturation % 224.46/31.95 % (386437)Time elapsed: 0.164 s % 224.46/31.95 % (386437)Peak memory usage: 13 MB % 224.46/31.95 % (386437)Instructions burned: 263 (million) % 224.46/31.95 % (386439)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=1516936007:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2728 on theBenchmark for (2728ds/1368Mi) % 224.46/31.95 % (386439)Instruction limit reached! % 224.46/31.95 % (386439)------------------------------ % 224.46/31.95 % (386439)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 224.46/31.95 % (386439)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 224.46/31.95 % (386439)CaDiCaL version: 2.1.3 % 224.46/31.95 % (386439)Termination reason: Instruction limit % 224.46/31.95 % (386439)Termination phase: Saturation % 224.46/31.95 % (386439)Time elapsed: 0.783 s % 224.46/31.95 % (386439)Peak memory usage: 23 MB % 224.46/31.95 % (386439)Instructions burned: 1369 (million) % 224.46/31.95 % (386441)ott-21_1_sil=16000:si=on:fs=off:random_seed=2229514149:i=360:av=off:fsr=off:rtra=on_2720 on theBenchmark for (2720ds/360Mi) % 224.46/31.95 % (386441)Instruction limit reached! % 224.46/31.95 % (386441)------------------------------ % 224.46/31.95 % (386441)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 224.46/31.95 % (386441)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 224.46/31.95 % (386441)CaDiCaL version: 2.1.3 % 224.46/31.95 % (386441)Termination reason: Instruction limit % 224.46/31.95 % (386441)Termination phase: Saturation % 224.46/31.95 % (386441)Time elapsed: 0.179 s % 224.46/31.95 % (386441)Peak memory usage: 14 MB % 224.46/31.95 % (386441)Instructions burned: 362 (million) % 224.46/31.95 % (386443)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3151117091:i=954:bd=all:rtra=on_2718 on theBenchmark for (2718ds/954Mi) % 224.46/31.95 % (386443)Instruction limit reached! % 224.46/31.95 % (386443)------------------------------ % 224.46/31.95 % (386443)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 224.46/31.95 % (386443)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 224.46/31.95 % (386443)CaDiCaL version: 2.1.3 % 224.46/31.95 % (386443)Termination reason: Instruction limit % 224.46/31.95 % (386443)Termination phase: Saturation % 224.46/31.95 % (386443)Time elapsed: 0.628 s % 224.46/31.95 % (386443)Peak memory usage: 16 MB % 224.46/31.95 % (386443)Instructions burned: 955 (million) % 224.46/31.95 % (386446)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=1555303693:fmbsr=1.3:i=1730:ins=25:rtra=on_2712 on theBenchmark for (2712ds/1730Mi) % 224.46/31.95 % (386446)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 224.46/31.95 % (386446)Terminated due to inappropriate strategy. % 224.46/31.95 % (386446)------------------------------ % 224.46/31.95 % (386446)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 224.46/31.95 % (386446)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 224.46/31.95 % (386446)CaDiCaL version: 2.1.3 % 224.46/31.95 % (386446)Termination reason: Inappropriate % 224.46/31.95 % (386446)Time elapsed: 0.006 s % 224.46/31.95 % (386446)Peak memory usage: 10 MB % 224.46/31.95 % (386446)Instructions burned: 11 (million) % 224.46/31.95 % (386446)------------------------------ % 224.46/31.95 % (386446)------------------------------ % 224.46/31.95 % (386449)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=3173108567:i=2358:rtra=on_2712 on theBenchmark for (2712ds/2358Mi) % 224.46/31.95 % (386403)Instruction limit reached! % 224.46/31.95 % (386403)------------------------------ % 224.46/31.95 % (386403)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 224.46/31.95 % (386403)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 224.46/31.95 % (386403)CaDiCaL version: 2.1.3 % 224.46/31.95 % (386403)Termination reason: Instruction limit % 258.14/36.62 % (386403)Termination phase: Saturation % 258.14/36.62 % (386403)Time elapsed: 12.934 s % 258.14/36.62 % (386403)Peak memory usage: 381 MB % 258.14/36.62 % (386403)Instructions burned: 53297 (million) % 258.14/36.62 % (386451)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=2926340028:i=1778:ins=1:rtra=on_2709 on theBenchmark for (2709ds/1778Mi) % 258.14/36.62 % (386451)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 258.14/36.62 % (386451)Terminated due to inappropriate strategy. % 258.14/36.62 % (386451)------------------------------ % 258.14/36.62 % (386451)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 258.14/36.62 % (386451)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 258.14/36.62 % (386451)CaDiCaL version: 2.1.3 % 258.14/36.62 % (386451)Termination reason: Inappropriate % 258.14/36.62 % (386451)Time elapsed: 0.003 s % 258.14/36.62 % (386451)Peak memory usage: 10 MB % 258.14/36.62 % (386451)Instructions burned: 11 (million) % 258.14/36.62 % (386451)------------------------------ % 258.14/36.62 % (386451)------------------------------ % 258.14/36.62 % (386453)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=3168283730:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2709 on theBenchmark for (2709ds/1384Mi) % 258.14/36.62 % (386453)Instruction limit reached! % 258.14/36.62 % (386453)------------------------------ % 258.14/36.62 % (386453)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 258.14/36.62 % (386453)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 258.14/36.62 % (386453)CaDiCaL version: 2.1.3 % 258.14/36.62 % (386453)Termination reason: Instruction limit % 258.14/36.62 % (386453)Termination phase: Saturation % 258.14/36.62 % (386453)Time elapsed: 0.482 s % 258.14/36.62 % (386453)Peak memory usage: 27 MB % 258.14/36.62 % (386453)Instructions burned: 1385 (million) % 258.14/36.62 % (386499)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=4213150378:i=1758:kws=inv_precedence:fsr=off:rtra=on_2704 on theBenchmark for (2704ds/1758Mi) % 258.14/36.62 % (386499)Instruction limit reached! % 258.14/36.62 % (386499)------------------------------ % 258.14/36.62 % (386499)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 258.14/36.62 % (386499)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 258.14/36.62 % (386499)CaDiCaL version: 2.1.3 % 258.14/36.62 % (386499)Termination reason: Instruction limit % 258.14/36.62 % (386499)Termination phase: Saturation % 258.14/36.62 % (386499)Time elapsed: 0.537 s % 258.14/36.62 % (386499)Peak memory usage: 25 MB % 258.14/36.62 % (386499)Instructions burned: 1760 (million) % 258.14/36.62 % (386501)fmb+10_1_sil=64000:si=on:random_seed=2460791493:i=44122:nm=2:rtra=on:gsp=on_2698 on theBenchmark for (2698ds/44122Mi) % 258.14/36.62 % (386501)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 258.14/36.62 % (386501)Terminated due to inappropriate strategy. % 258.14/36.62 % (386501)------------------------------ % 258.14/36.62 % (386501)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 258.14/36.62 % (386501)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 258.14/36.62 % (386501)CaDiCaL version: 2.1.3 % 258.14/36.62 % (386501)Termination reason: Inappropriate % 258.14/36.62 % (386501)Time elapsed: 0.003 s % 258.14/36.62 % (386501)Peak memory usage: 11 MB % 258.14/36.62 % (386501)Instructions burned: 11 (million) % 258.14/36.62 % (386501)------------------------------ % 258.14/36.62 % (386501)------------------------------ % 258.14/36.62 % (386503)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=3755876674:i=19030:nm=5:rtra=on_2698 on theBenchmark for (2698ds/19030Mi) % 258.14/36.62 % (386503)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 258.14/36.62 % (386503)Terminated due to inappropriate strategy. % 258.14/36.62 % (386503)------------------------------ % 258.14/36.62 % (386503)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 258.14/36.62 % (386503)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 258.14/36.62 % (386503)CaDiCaL version: 2.1.3 % 258.14/36.62 % (386503)Termination reason: Inappropriate % 258.14/36.62 % (386503)Time elapsed: 0.003 s % 258.14/36.62 % (386503)Peak memory usage: 11 MB % 258.14/36.62 % (386503)Instructions burned: 11 (million) % 258.14/36.62 % (386503)------------------------------ % 258.14/36.62 % (386503)------------------------------ % 258.14/36.62 % (386505)fmb+10_1_sil=64000:sas=cadical:si=on:fmbss=8:random_seed=324409166:fmbsr=1.7:i=1840:rtra=on_2698 on theBenchmark for (2698ds/1840Mi) % 285.11/40.48 % (386505)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 285.11/40.48 % (386505)Terminated due to inappropriate strategy. % 285.11/40.48 % (386505)------------------------------ % 285.11/40.48 % (386505)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 285.11/40.48 % (386505)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 285.11/40.48 % (386505)CaDiCaL version: 2.1.3 % 285.11/40.48 % (386505)Termination reason: Inappropriate % 285.11/40.48 % (386505)Time elapsed: 0.003 s % 285.11/40.48 % (386505)Peak memory usage: 11 MB % 285.11/40.48 % (386505)Instructions burned: 11 (million) % 285.11/40.48 % (386505)------------------------------ % 285.11/40.48 % (386505)------------------------------ % 285.11/40.48 % (386507)dis-4_1_sil=16000:drc=ordering:si=on:sp=const_frequency:sac=on:newcnf=on:random_seed=493896723:i=10262:rtra=on_2698 on theBenchmark for (2698ds/10262Mi) % 285.11/40.48 % (386449)Instruction limit reached! % 285.11/40.48 % (386449)------------------------------ % 285.11/40.48 % (386449)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 285.11/40.48 % (386449)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 285.11/40.48 % (386449)CaDiCaL version: 2.1.3 % 285.11/40.48 % (386449)Termination reason: Instruction limit % 285.11/40.48 % (386449)Termination phase: Saturation % 285.11/40.48 % (386449)Time elapsed: 1.567 s % 285.11/40.48 % (386449)Peak memory usage: 29 MB % 285.11/40.48 % (386449)Instructions burned: 2359 (million) % 285.11/40.48 % (386509)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:si=on:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1111464291:i=2944:ins=7:rtra=on:fdi=8:gsp=on_2696 on theBenchmark for (2696ds/2944Mi) % 285.11/40.48 % (386407)Instruction limit reached! % 285.11/40.48 % (386407)------------------------------ % 285.11/40.48 % (386407)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 285.11/40.48 % (386407)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 285.11/40.48 % (386407)CaDiCaL version: 2.1.3 % 285.11/40.48 % (386407)Termination reason: Instruction limit % 285.11/40.48 % (386407)Termination phase: Saturation % 285.11/40.48 % (386407)Time elapsed: 14.660 s % 285.11/40.48 % (386407)Peak memory usage: 98 MB % 285.11/40.48 % (386407)Instructions burned: 28122 (million) % 285.11/40.48 % (386511)fmb+10_1_sil=16000:sas=cadical:si=on:bce=on:fmbss=77:random_seed=1114891050:i=12648:rtra=on_2686 on theBenchmark for (2686ds/12648Mi) % 285.11/40.48 % (386511)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 285.11/40.48 % (386511)Terminated due to inappropriate strategy. % 285.11/40.48 % (386511)------------------------------ % 285.11/40.48 % (386511)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 285.11/40.48 % (386511)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 285.11/40.48 % (386511)CaDiCaL version: 2.1.3 % 285.11/40.48 % (386511)Termination reason: Inappropriate % 285.11/40.48 % (386511)Time elapsed: 0.007 s % 285.11/40.48 % (386511)Peak memory usage: 11 MB % 285.11/40.48 % (386511)Instructions burned: 12 (million) % 285.11/40.48 % (386511)------------------------------ % 285.11/40.48 % (386511)------------------------------ % 285.11/40.48 % (386513)fmb+10_1_fmbas=function:sil=32000:sas=cadical:si=on:fmbss=16:random_seed=1435218850:fmbsr=2.30978:i=4348:rtra=on_2686 on theBenchmark for (2686ds/4348Mi) % 285.11/40.48 % (386513)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 285.11/40.48 % (386513)Terminated due to inappropriate strategy. % 285.11/40.48 % (386513)------------------------------ % 285.11/40.48 % (386513)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 285.11/40.48 % (386513)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 285.11/40.48 % (386513)CaDiCaL version: 2.1.3 % 285.11/40.48 % (386513)Termination reason: Inappropriate % 285.11/40.48 % (386513)Time elapsed: 0.006 s % 285.11/40.48 % (386513)Peak memory usage: 11 MB % 285.11/40.48 % (386513)Instructions burned: 11 (million) % 285.11/40.48 % (386513)------------------------------ % 285.11/40.48 % (386513)------------------------------ % 285.11/40.48 % (386515)ott-2_1_sil=16000:si=on:newcnf=on:random_seed=3557381738:avsq=on:i=1738:avsqr=1,16:kws=inv_arity_squared:rtra=on_2686 on theBenchmark for (2686ds/1738Mi) % 285.11/40.48 % (386509)Instruction limit reached! % 285.11/40.48 % (386509)------------------------------ % 285.11/40.48 % (386509)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 285.11/40.48 % (386509)Linked with Z3 4.14.0Terminated % 300.01/42.54 % Vampire exiting % 300.01/42.54 Terminated %------------------------------------------------------------------------------