%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWW009_1 : TPTP v9.3.1. Released v5.0.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % Computer : n026.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:38:12 PM UTC 2026 % Result : Timeout 300.58s 42.64s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : SWW009_1 : TPTP v9.3.1. Released v5.0.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.08/0.19 % Computer : n026.cluster.edu % 0.08/0.19 % Model : x86_64 x86_64 % 0.08/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.08/0.19 % Memory : 8046.5625MB % 0.08/0.19 % OS : Linux 6.8.0-71-generic % 0.08/0.19 % CPULimit : 300 % 0.08/0.19 % WCLimit : 300 % 0.08/0.19 % DateTime : Mon Sep 28 13:11:12 UTC 2026 % 0.08/0.19 % CPUTime : % 0.08/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.08/0.23 Running first-order model finding % 0.08/0.23 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 % 3.11/0.73 % (3837705)Will run a generic schedule for satisfiability detection. % 3.11/0.73 % (3837715)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2960163863:i=131_2999 on theBenchmark for (2999ds/131Mi) % 3.11/0.73 % (3837711)% WARNING: option uhcvi not known. % 3.11/0.73 % (3837710)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=4247947885_2999 on theBenchmark for (2999ds/0Mi) % 3.11/0.73 % (3837713)dis+10_1_sil=32000:sp=arity:random_seed=2921824232:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 3.11/0.73 % (3837711)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=470340561:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 3.11/0.73 % (3837712)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1669802112:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 3.11/0.73 % (3837714)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3334206877:i=116_2999 on theBenchmark for (2999ds/116Mi) % 3.11/0.73 % (3837716)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1759542173:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 3.11/0.73 % (3837715)Instruction limit reached! % 3.11/0.73 % (3837715)------------------------------ % 3.11/0.73 % (3837715)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.11/0.73 % (3837715)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.11/0.73 % (3837715)CaDiCaL version: 2.1.3 % 3.11/0.73 % (3837715)Termination reason: Instruction limit % 3.11/0.73 % (3837715)Termination phase: Saturation % 3.11/0.73 % (3837715)Time elapsed: 0.029 s % 3.11/0.73 % (3837715)Peak memory usage: 14 MB % 3.11/0.73 % (3837715)Instructions burned: 133 (million) % 3.11/0.73 % (3837710)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.11/0.73 % (3837710)Terminated due to inappropriate strategy. % 3.11/0.73 % (3837710)------------------------------ % 3.11/0.73 % (3837710)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.11/0.73 % (3837710)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.11/0.73 % (3837710)CaDiCaL version: 2.1.3 % 3.11/0.73 % (3837710)Termination reason: Inappropriate % 3.11/0.73 % (3837710)Time elapsed: 0.029 s % 3.11/0.73 % (3837710)Peak memory usage: 13 MB % 3.11/0.73 % (3837710)Instructions burned: 67 (million) % 3.11/0.73 % (3837710)------------------------------ % 3.11/0.73 % (3837710)------------------------------ % 3.11/0.73 % (3837724)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1126746330:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 3.11/0.73 % (3837713)Instruction limit reached! % 3.11/0.73 % (3837713)------------------------------ % 3.11/0.73 % (3837713)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.11/0.73 % (3837713)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.11/0.73 % (3837713)CaDiCaL version: 2.1.3 % 3.11/0.73 % (3837713)Termination reason: Instruction limit % 3.11/0.73 % (3837713)Termination phase: Saturation % 3.11/0.73 % (3837713)Time elapsed: 0.046 s % 3.11/0.73 % (3837713)Peak memory usage: 14 MB % 3.11/0.73 % (3837713)Instructions burned: 103 (million) % 3.11/0.73 % (3837725)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3413665923:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 3.11/0.73 % (3837724)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.11/0.73 % (3837724)Terminated due to inappropriate strategy. % 3.11/0.73 % (3837724)------------------------------ % 3.11/0.73 % (3837724)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.11/0.73 % (3837724)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.11/0.73 % (3837724)CaDiCaL version: 2.1.3 % 3.11/0.73 % (3837724)Termination reason: Inappropriate % 3.11/0.73 % (3837724)Time elapsed: 0.015 s % 3.11/0.73 % (3837724)Peak memory usage: 13 MB % 3.11/0.73 % (3837724)Instructions burned: 67 (million) % 3.11/0.73 % (3837724)------------------------------ % 3.11/0.73 % (3837724)------------------------------ % 3.11/0.73 % (3837714)Instruction limit reached! % 3.11/0.73 % (3837714)------------------------------ % 3.11/0.73 % (3837714)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.11/0.73 % (3837714)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.11/0.73 % (3837714)CaDiCaL version: 2.1.3 % 3.11/0.73 % (3837714)Termination reason: Instruction limit % 5.50/1.11 % (3837714)Termination phase: Saturation % 5.50/1.11 % (3837714)Time elapsed: 0.052 s % 5.50/1.11 % (3837714)Peak memory usage: 14 MB % 5.50/1.11 % (3837714)Instructions burned: 118 (million) % 5.50/1.11 % (3837729)ott-21_1_sil=16000:fs=off:random_seed=1598766965:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 5.50/1.11 % (3837727)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=2808855678:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi) % 5.50/1.11 % (3837716)Instruction limit reached! % 5.50/1.11 % (3837716)------------------------------ % 5.50/1.11 % (3837716)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.50/1.11 % (3837716)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.50/1.11 % (3837716)CaDiCaL version: 2.1.3 % 5.50/1.11 % (3837716)Termination reason: Instruction limit % 5.50/1.11 % (3837716)Termination phase: Saturation % 5.50/1.11 % (3837716)Time elapsed: 0.068 s % 5.50/1.11 % (3837716)Peak memory usage: 15 MB % 5.50/1.11 % (3837716)Instructions burned: 160 (million) % 5.50/1.11 % (3837730)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=58796988:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 5.50/1.11 % (3837733)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3783525068:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 5.50/1.11 % (3837725)Instruction limit reached! % 5.50/1.11 % (3837725)------------------------------ % 5.50/1.11 % (3837725)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.50/1.11 % (3837725)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.50/1.11 % (3837725)CaDiCaL version: 2.1.3 % 5.50/1.11 % (3837725)Termination reason: Instruction limit % 5.50/1.11 % (3837725)Termination phase: Saturation % 5.50/1.11 % (3837725)Time elapsed: 0.055 s % 5.50/1.11 % (3837725)Peak memory usage: 14 MB % 5.50/1.11 % (3837725)Instructions burned: 132 (million) % 5.50/1.11 % (3837729)Instruction limit reached! % 5.50/1.11 % (3837729)------------------------------ % 5.50/1.11 % (3837729)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.50/1.11 % (3837729)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.50/1.11 % (3837729)CaDiCaL version: 2.1.3 % 5.50/1.11 % (3837729)Termination reason: Instruction limit % 5.50/1.11 % (3837729)Termination phase: Saturation % 5.50/1.11 % (3837729)Time elapsed: 0.046 s % 5.50/1.11 % (3837729)Peak memory usage: 14 MB % 5.50/1.11 % (3837729)Instructions burned: 183 (million) % 5.50/1.11 % (3837737)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3704828049:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi) % 5.50/1.11 % (3837733)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 5.50/1.11 % (3837733)Terminated due to inappropriate strategy. % 5.50/1.11 % (3837733)------------------------------ % 5.50/1.11 % (3837733)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.50/1.11 % (3837733)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.50/1.11 % (3837733)CaDiCaL version: 2.1.3 % 5.50/1.11 % (3837733)Termination reason: Inappropriate % 5.50/1.11 % (3837733)Time elapsed: 0.028 s % 5.50/1.11 % (3837733)Peak memory usage: 13 MB % 5.50/1.11 % (3837733)Instructions burned: 66 (million) % 5.50/1.11 % (3837733)------------------------------ % 5.50/1.11 % (3837733)------------------------------ % 5.50/1.11 % (3837736)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=449981926:i=1179_2998 on theBenchmark for (2998ds/1179Mi) % 5.50/1.11 % (3837739)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=1300756260: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) % 5.50/1.11 % (3837737)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 5.50/1.11 % (3837737)Terminated due to inappropriate strategy. % 5.50/1.11 % (3837737)------------------------------ % 5.50/1.11 % (3837737)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.50/1.11 % (3837737)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.50/1.11 % (3837737)CaDiCaL version: 2.1.3 % 5.50/1.11 % (3837737)Termination reason: Inappropriate % 5.50/1.11 % (3837737)Time elapsed: 0.022 s % 5.50/1.11 % (3837737)Peak memory usage: 14 MB % 17.51/2.94 % (3837737)Instructions burned: 94 (million) % 17.51/2.94 % (3837737)------------------------------ % 17.51/2.94 % (3837737)------------------------------ % 17.51/2.94 % (3837742)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3862502151:i=879:kws=inv_precedence:fsr=off_2998 on theBenchmark for (2998ds/879Mi) % 17.51/2.94 % (3837730)Instruction limit reached! % 17.51/2.94 % (3837730)------------------------------ % 17.51/2.94 % (3837730)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 17.51/2.94 % (3837730)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.51/2.94 % (3837730)CaDiCaL version: 2.1.3 % 17.51/2.94 % (3837730)Termination reason: Instruction limit % 17.51/2.94 % (3837730)Termination phase: Saturation % 17.51/2.94 % (3837730)Time elapsed: 0.246 s % 17.51/2.94 % (3837730)Peak memory usage: 16 MB % 17.51/2.94 % (3837730)Instructions burned: 479 (million) % 17.51/2.94 % (3837744)fmb+10_1_sil=64000:random_seed=211696098:i=22061:nm=2:gsp=on_2996 on theBenchmark for (2996ds/22061Mi) % 17.51/2.94 % (3837744)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 17.51/2.94 % (3837744)Terminated due to inappropriate strategy. % 17.51/2.94 % (3837744)------------------------------ % 17.51/2.94 % (3837744)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 17.51/2.94 % (3837744)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.51/2.94 % (3837744)CaDiCaL version: 2.1.3 % 17.51/2.94 % (3837744)Termination reason: Inappropriate % 17.51/2.94 % (3837744)Time elapsed: 0.032 s % 17.51/2.94 % (3837744)Peak memory usage: 13 MB % 17.51/2.94 % (3837744)Instructions burned: 73 (million) % 17.51/2.94 % (3837744)------------------------------ % 17.51/2.94 % (3837744)------------------------------ % 17.51/2.94 % (3837746)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=4176568824:i=9515:nm=5_2995 on theBenchmark for (2995ds/9515Mi) % 17.51/2.94 % (3837727)Instruction limit reached! % 17.51/2.94 % (3837727)------------------------------ % 17.51/2.94 % (3837727)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 17.51/2.94 % (3837727)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.51/2.94 % (3837727)CaDiCaL version: 2.1.3 % 17.51/2.94 % (3837727)Termination reason: Instruction limit % 17.51/2.94 % (3837727)Termination phase: Saturation % 17.51/2.94 % (3837727)Time elapsed: 0.330 s % 17.51/2.94 % (3837727)Peak memory usage: 18 MB % 17.51/2.94 % (3837727)Instructions burned: 686 (million) % 17.51/2.94 % (3837748)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3154689531:fmbsr=1.7:i=920_2995 on theBenchmark for (2995ds/920Mi) % 17.51/2.94 % (3837742)Instruction limit reached! % 17.51/2.94 % (3837742)------------------------------ % 17.51/2.94 % (3837742)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 17.51/2.94 % (3837742)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.51/2.94 % (3837742)CaDiCaL version: 2.1.3 % 17.51/2.94 % (3837742)Termination reason: Instruction limit % 17.51/2.94 % (3837742)Termination phase: Saturation % 17.51/2.94 % (3837742)Time elapsed: 0.266 s % 17.51/2.94 % (3837742)Peak memory usage: 21 MB % 17.51/2.94 % (3837742)Instructions burned: 882 (million) % 17.51/2.94 % (3837746)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 17.51/2.94 % (3837746)Terminated due to inappropriate strategy. % 17.51/2.94 % (3837746)------------------------------ % 17.51/2.94 % (3837746)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 17.51/2.94 % (3837746)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.51/2.94 % (3837746)CaDiCaL version: 2.1.3 % 17.51/2.94 % (3837746)Termination reason: Inappropriate % 17.51/2.94 % (3837746)Time elapsed: 0.028 s % 17.51/2.94 % (3837746)Peak memory usage: 13 MB % 17.51/2.94 % (3837746)Instructions burned: 67 (million) % 17.51/2.94 % (3837746)------------------------------ % 17.51/2.94 % (3837746)------------------------------ % 17.51/2.94 % (3837750)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=3255408886:i=5131_2995 on theBenchmark for (2995ds/5131Mi) % 17.51/2.94 % (3837751)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3598278747:i=1472:ins=7:fdi=8:gsp=on_2995 on theBenchmark for (2995ds/1472Mi) % 17.51/2.94 % (3837748)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 17.51/2.94 % (3837748)Terminated due to inappropriate strategy. % 17.51/2.94 % (3837748)------------------------------ % 17.51/2.94 % (3837748)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.65/3.57 % (3837748)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.65/3.57 % (3837748)CaDiCaL version: 2.1.3 % 22.65/3.57 % (3837748)Termination reason: Inappropriate % 22.65/3.57 % (3837748)Time elapsed: 0.028 s % 22.65/3.57 % (3837748)Peak memory usage: 13 MB % 22.65/3.57 % (3837748)Instructions burned: 67 (million) % 22.65/3.57 % (3837748)------------------------------ % 22.65/3.57 % (3837748)------------------------------ % 22.65/3.57 % (3837754)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=254534747:i=6324_2994 on theBenchmark for (2994ds/6324Mi) % 22.65/3.57 % (3837739)Instruction limit reached! % 22.65/3.57 % (3837739)------------------------------ % 22.65/3.57 % (3837739)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.65/3.57 % (3837739)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.65/3.57 % (3837739)CaDiCaL version: 2.1.3 % 22.65/3.57 % (3837739)Termination reason: Instruction limit % 22.65/3.57 % (3837739)Termination phase: Saturation % 22.65/3.57 % (3837739)Time elapsed: 0.329 s % 22.65/3.57 % (3837739)Peak memory usage: 20 MB % 22.65/3.57 % (3837739)Instructions burned: 693 (million) % 22.65/3.57 % (3837756)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1217091957:fmbsr=2.30978:i=2174_2994 on theBenchmark for (2994ds/2174Mi) % 22.65/3.57 % (3837754)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 22.65/3.57 % (3837754)Terminated due to inappropriate strategy. % 22.65/3.57 % (3837754)------------------------------ % 22.65/3.57 % (3837754)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.65/3.57 % (3837754)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.65/3.57 % (3837754)CaDiCaL version: 2.1.3 % 22.65/3.57 % (3837754)Termination reason: Inappropriate % 22.65/3.57 % (3837754)Time elapsed: 0.028 s % 22.65/3.57 % (3837754)Peak memory usage: 13 MB % 22.65/3.57 % (3837754)Instructions burned: 67 (million) % 22.65/3.57 % (3837754)------------------------------ % 22.65/3.57 % (3837754)------------------------------ % 22.65/3.57 % (3837758)ott-2_1_sil=16000:newcnf=on:random_seed=1921236025:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2994 on theBenchmark for (2994ds/869Mi) % 22.65/3.57 % (3837756)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 22.65/3.57 % (3837756)Terminated due to inappropriate strategy. % 22.65/3.57 % (3837756)------------------------------ % 22.65/3.57 % (3837756)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.65/3.57 % (3837756)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.65/3.57 % (3837756)CaDiCaL version: 2.1.3 % 22.65/3.57 % (3837756)Termination reason: Inappropriate % 22.65/3.57 % (3837756)Time elapsed: 0.028 s % 22.65/3.57 % (3837756)Peak memory usage: 13 MB % 22.65/3.57 % (3837756)Instructions burned: 67 (million) % 22.65/3.57 % (3837756)------------------------------ % 22.65/3.57 % (3837756)------------------------------ % 22.65/3.57 % (3837760)ott+10_1_sil=32000:tgt=ground:random_seed=3063913963:i=5114:av=off_2994 on theBenchmark for (2994ds/5114Mi) % 22.65/3.57 % (3837736)Instruction limit reached! % 22.65/3.57 % (3837736)------------------------------ % 22.65/3.57 % (3837736)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.65/3.57 % (3837736)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.65/3.57 % (3837736)CaDiCaL version: 2.1.3 % 22.65/3.57 % (3837736)Termination reason: Instruction limit % 22.65/3.57 % (3837736)Termination phase: Saturation % 22.65/3.57 % (3837736)Time elapsed: 0.643 s % 22.65/3.57 % (3837736)Peak memory usage: 20 MB % 22.65/3.57 % (3837736)Instructions burned: 1179 (million) % 22.65/3.57 % (3837762)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=3634798022:i=54282_2991 on theBenchmark for (2991ds/54282Mi) % 22.65/3.57 % (3837762)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 22.65/3.57 % (3837762)Terminated due to inappropriate strategy. % 22.65/3.57 % (3837762)------------------------------ % 22.65/3.57 % (3837762)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.65/3.57 % (3837762)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.65/3.57 % (3837762)CaDiCaL version: 2.1.3 % 22.65/3.57 % (3837762)Termination reason: Inappropriate % 22.65/3.57 % (3837762)Time elapsed: 0.029 s % 22.65/3.57 % (3837762)Peak memory usage: 13 MB % 22.65/3.57 % (3837762)Instructions burned: 67 (million) % 87.60/12.64 % (3837762)------------------------------ % 87.60/12.64 % (3837762)------------------------------ % 87.60/12.64 % (3837764)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=1666424817:i=3512:aac=none_2991 on theBenchmark for (2991ds/3512Mi) % 87.60/12.64 % (3837758)Instruction limit reached! % 87.60/12.64 % (3837758)------------------------------ % 87.60/12.64 % (3837758)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 87.60/12.64 % (3837758)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 87.60/12.64 % (3837758)CaDiCaL version: 2.1.3 % 87.60/12.64 % (3837758)Termination reason: Instruction limit % 87.60/12.64 % (3837758)Termination phase: Saturation % 87.60/12.64 % (3837758)Time elapsed: 0.482 s % 87.60/12.64 % (3837758)Peak memory usage: 19 MB % 87.60/12.64 % (3837758)Instructions burned: 870 (million) % 87.60/12.64 % (3837766)dis+21_1_sil=32000:sas=cadical:random_seed=4046680171:i=3773:amm=off_2989 on theBenchmark for (2989ds/3773Mi) % 87.60/12.64 % (3837751)Instruction limit reached! % 87.60/12.64 % (3837751)------------------------------ % 87.60/12.64 % (3837751)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 87.60/12.64 % (3837751)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 87.60/12.64 % (3837751)CaDiCaL version: 2.1.3 % 87.60/12.64 % (3837751)Termination reason: Instruction limit % 87.60/12.64 % (3837751)Termination phase: Saturation % 87.60/12.64 % (3837751)Time elapsed: 0.616 s % 87.60/12.64 % (3837751)Peak memory usage: 20 MB % 87.60/12.64 % (3837751)Instructions burned: 1474 (million) % 87.60/12.64 % (3837768)ott+11_1_sil=16000:gs=on:random_seed=2509241385:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2988 on theBenchmark for (2988ds/2251Mi) % 87.60/12.64 % (3837750)Instruction limit reached! % 87.60/12.64 % (3837750)------------------------------ % 87.60/12.64 % (3837750)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 87.60/12.64 % (3837750)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 87.60/12.64 % (3837750)CaDiCaL version: 2.1.3 % 87.60/12.64 % (3837750)Termination reason: Instruction limit % 87.60/12.64 % (3837750)Termination phase: Saturation % 87.60/12.64 % (3837750)Time elapsed: 1.443 s % 87.60/12.64 % (3837750)Peak memory usage: 43 MB % 87.60/12.64 % (3837750)Instructions burned: 5134 (million) % 87.60/12.64 % (3837770)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=3818074510:fmbsr=1.6:i=67534_2980 on theBenchmark for (2980ds/67534Mi) % 87.60/12.64 % (3837770)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 87.60/12.64 % (3837770)Terminated due to inappropriate strategy. % 87.60/12.64 % (3837770)------------------------------ % 87.60/12.64 % (3837770)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 87.60/12.64 % (3837770)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 87.60/12.64 % (3837770)CaDiCaL version: 2.1.3 % 87.60/12.64 % (3837770)Termination reason: Inappropriate % 87.60/12.64 % (3837770)Time elapsed: 0.020 s % 87.60/12.64 % (3837770)Peak memory usage: 13 MB % 87.60/12.64 % (3837770)Instructions burned: 90 (million) % 87.60/12.64 % (3837770)------------------------------ % 87.60/12.64 % (3837770)------------------------------ % 87.60/12.64 % (3837772)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=3622345597:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2980 on theBenchmark for (2980ds/4591Mi) % 87.60/12.64 % (3837768)Instruction limit reached! % 87.60/12.64 % (3837768)------------------------------ % 87.60/12.64 % (3837768)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 87.60/12.64 % (3837768)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 87.60/12.64 % (3837768)CaDiCaL version: 2.1.3 % 87.60/12.64 % (3837768)Termination reason: Instruction limit % 87.60/12.64 % (3837768)Termination phase: Saturation % 87.60/12.64 % (3837768)Time elapsed: 0.982 s % 87.60/12.64 % (3837768)Peak memory usage: 21 MB % 87.60/12.64 % (3837768)Instructions burned: 2252 (million) % 87.60/12.64 % (3837774)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=1365258502:i=29340_2978 on theBenchmark for (2978ds/29340Mi) % 87.60/12.64 % (3837766)Instruction limit reached! % 87.60/12.64 % (3837766)------------------------------ % 87.60/12.64 % (3837766)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 87.60/12.64 % (3837766)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 87.60/12.64 % (3837766)CaDiCaL version: 2.1.3 % 87.60/12.64 % (3837766)Termination reason: Instruction limit % 111.99/16.12 % (3837766)Termination phase: Saturation % 111.99/16.12 % (3837766)Time elapsed: 1.632 s % 111.99/16.12 % (3837766)Peak memory usage: 22 MB % 111.99/16.12 % (3837766)Instructions burned: 3773 (million) % 111.99/16.12 % (3837776)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=3843751579:i=5211_2972 on theBenchmark for (2972ds/5211Mi) % 111.99/16.12 % (3837764)Instruction limit reached! % 111.99/16.12 % (3837764)------------------------------ % 111.99/16.12 % (3837764)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 111.99/16.12 % (3837764)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 111.99/16.12 % (3837764)CaDiCaL version: 2.1.3 % 111.99/16.12 % (3837764)Termination reason: Instruction limit % 111.99/16.12 % (3837764)Termination phase: Saturation % 111.99/16.12 % (3837764)Time elapsed: 1.834 s % 111.99/16.12 % (3837764)Peak memory usage: 30 MB % 111.99/16.12 % (3837764)Instructions burned: 3514 (million) % 111.99/16.12 % (3837778)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=4218295420:i=5497:nm=2_2972 on theBenchmark for (2972ds/5497Mi) % 111.99/16.12 % (3837778)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 111.99/16.12 % (3837778)Terminated due to inappropriate strategy. % 111.99/16.12 % (3837778)------------------------------ % 111.99/16.12 % (3837778)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 111.99/16.12 % (3837778)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 111.99/16.12 % (3837778)CaDiCaL version: 2.1.3 % 111.99/16.12 % (3837778)Termination reason: Inappropriate % 111.99/16.12 % (3837778)Time elapsed: 0.029 s % 111.99/16.12 % (3837778)Peak memory usage: 13 MB % 111.99/16.12 % (3837778)Instructions burned: 67 (million) % 111.99/16.12 % (3837778)------------------------------ % 111.99/16.12 % (3837778)------------------------------ % 111.99/16.12 % (3837780)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=486236713:fmbsr=2:i=46332_2972 on theBenchmark for (2972ds/46332Mi) % 111.99/16.12 % (3837780)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 111.99/16.12 % (3837780)Terminated due to inappropriate strategy. % 111.99/16.12 % (3837780)------------------------------ % 111.99/16.12 % (3837780)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 111.99/16.12 % (3837780)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 111.99/16.12 % (3837780)CaDiCaL version: 2.1.3 % 111.99/16.12 % (3837780)Termination reason: Inappropriate % 111.99/16.12 % (3837780)Time elapsed: 0.038 s % 111.99/16.12 % (3837780)Peak memory usage: 13 MB % 111.99/16.12 % (3837780)Instructions burned: 93 (million) % 111.99/16.12 % (3837780)------------------------------ % 111.99/16.12 % (3837780)------------------------------ % 111.99/16.12 % (3837782)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=941626969:i=14071_2971 on theBenchmark for (2971ds/14071Mi) % 111.99/16.12 % (3837782)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 111.99/16.12 % (3837782)Terminated due to inappropriate strategy. % 111.99/16.12 % (3837782)------------------------------ % 111.99/16.12 % (3837782)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 111.99/16.12 % (3837782)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 111.99/16.12 % (3837782)CaDiCaL version: 2.1.3 % 111.99/16.12 % (3837782)Termination reason: Inappropriate % 111.99/16.12 % (3837782)Time elapsed: 0.039 s % 111.99/16.12 % (3837782)Peak memory usage: 13 MB % 111.99/16.12 % (3837782)Instructions burned: 93 (million) % 111.99/16.12 % (3837782)------------------------------ % 111.99/16.12 % (3837782)------------------------------ % 111.99/16.12 % (3837784)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=816815610:i=22565:add=on:rawr=on_2971 on theBenchmark for (2971ds/22565Mi) % 111.99/16.12 % (3837772)Instruction limit reached! % 111.99/16.12 % (3837772)------------------------------ % 111.99/16.12 % (3837772)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 111.99/16.12 % (3837772)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 111.99/16.12 % (3837772)CaDiCaL version: 2.1.3 % 111.99/16.12 % (3837772)Termination reason: Instruction limit % 111.99/16.12 % (3837772)Termination phase: Saturation % 111.99/16.12 % (3837772)Time elapsed: 1.333 s % 111.99/16.12 % (3837772)Peak memory usage: 45 MB % 111.99/16.12 % (3837772)Instructions burned: 4593 (million) % 111.99/16.12 % (3837786)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=2104153315:i=8173:av=off_2966 on theBenchmark for (2966ds/8173Mi) % 114.58/16.40 % (3837760)Instruction limit reached! % 114.58/16.40 % (3837760)------------------------------ % 114.58/16.40 % (3837760)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 114.58/16.40 % (3837760)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 114.58/16.40 % (3837760)CaDiCaL version: 2.1.3 % 114.58/16.40 % (3837760)Termination reason: Instruction limit % 114.58/16.40 % (3837760)Termination phase: Saturation % 114.58/16.40 % (3837760)Time elapsed: 3.047 s % 114.58/16.40 % (3837760)Peak memory usage: 32 MB % 114.58/16.40 % (3837760)Instructions burned: 5115 (million) % 114.58/16.40 % (3837788)dis+10_16:1_sil=16000:random_seed=1826343931:i=9155:fsr=off_2963 on theBenchmark for (2963ds/9155Mi) % 114.58/16.40 % (3837786)Instruction limit reached! % 114.58/16.40 % (3837786)------------------------------ % 114.58/16.40 % (3837786)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 114.58/16.40 % (3837786)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 114.58/16.40 % (3837786)CaDiCaL version: 2.1.3 % 114.58/16.40 % (3837786)Termination reason: Instruction limit % 114.58/16.40 % (3837786)Termination phase: Saturation % 114.58/16.40 % (3837786)Time elapsed: 2.036 s % 114.58/16.40 % (3837786)Peak memory usage: 39 MB % 114.58/16.40 % (3837786)Instructions burned: 8174 (million) % 114.58/16.40 % (3837790)ott-3_8_sil=64000:random_seed=3021647760:i=20139:bs=on_2946 on theBenchmark for (2946ds/20139Mi) % 114.58/16.40 % (3837776)Instruction limit reached! % 114.58/16.40 % (3837776)------------------------------ % 114.58/16.40 % (3837776)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 114.58/16.40 % (3837776)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 114.58/16.40 % (3837776)CaDiCaL version: 2.1.3 % 114.58/16.40 % (3837776)Termination reason: Instruction limit % 114.58/16.40 % (3837776)Termination phase: Saturation % 114.58/16.40 % (3837776)Time elapsed: 2.743 s % 114.58/16.40 % (3837776)Peak memory usage: 46 MB % 114.58/16.40 % (3837776)Instructions burned: 5212 (million) % 114.58/16.40 % (3837792)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=309558068:fmbsr=2:i=32576_2945 on theBenchmark for (2945ds/32576Mi) % 114.58/16.40 % (3837792)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 114.58/16.40 % (3837792)Terminated due to inappropriate strategy. % 114.58/16.40 % (3837792)------------------------------ % 114.58/16.40 % (3837792)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 114.58/16.40 % (3837792)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 114.58/16.40 % (3837792)CaDiCaL version: 2.1.3 % 114.58/16.40 % (3837792)Termination reason: Inappropriate % 114.58/16.40 % (3837792)Time elapsed: 0.038 s % 114.58/16.40 % (3837792)Peak memory usage: 13 MB % 114.58/16.40 % (3837792)Instructions burned: 91 (million) % 114.58/16.40 % (3837792)------------------------------ % 114.58/16.40 % (3837792)------------------------------ % 114.58/16.40 % (3837794)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=3258439082:i=11404_2944 on theBenchmark for (2944ds/11404Mi) % 114.58/16.40 % (3837788)Instruction limit reached! % 114.58/16.40 % (3837788)------------------------------ % 114.58/16.40 % (3837788)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 114.58/16.40 % (3837788)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 114.58/16.40 % (3837788)CaDiCaL version: 2.1.3 % 114.58/16.40 % (3837788)Termination reason: Instruction limit % 114.58/16.40 % (3837788)Termination phase: Saturation % 114.58/16.40 % (3837788)Time elapsed: 4.699 s % 114.58/16.40 % (3837788)Peak memory usage: 54 MB % 114.58/16.40 % (3837788)Instructions burned: 9156 (million) % 114.58/16.40 % (3837796)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=4002844861:i=14134_2916 on theBenchmark for (2916ds/14134Mi) % 114.58/16.40 % (3837790)Instruction limit reached! % 114.58/16.40 % (3837790)------------------------------ % 114.58/16.40 % (3837790)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 114.58/16.40 % (3837790)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 114.58/16.40 % (3837790)CaDiCaL version: 2.1.3 % 114.58/16.40 % (3837790)Termination reason: Instruction limit % 114.58/16.40 % (3837790)Termination phase: Saturation % 114.58/16.40 % (3837790)Time elapsed: 6.177 s % 114.58/16.40 % (3837790)Peak memory usage: 60 MB % 114.58/16.40 % (3837790)Instructions burned: 20139 (million) % 114.58/16.40 % (3837798)dis+33_16_sil=32000:sac=on:random_seed=2482945487:i=15851:nm=0_2884 on theBenchmark for (2884ds/15851Mi) % 114.58/16.40 % (3837784)Instruction limit reached! % 114.58/16.40 % (3837784)------------------------------ % 114.58/16.40 % (3837784)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 153.64/21.90 % (3837784)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 153.64/21.90 % (3837784)CaDiCaL version: 2.1.3 % 153.64/21.90 % (3837784)Termination reason: Instruction limit % 153.64/21.90 % (3837784)Termination phase: Saturation % 153.64/21.90 % (3837784)Time elapsed: 9.488 s % 153.64/21.90 % (3837784)Peak memory usage: 75 MB % 153.64/21.90 % (3837784)Instructions burned: 22569 (million) % 153.64/21.90 % (3837800)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=4048547874:avsq=on:i=17627:add=on:amm=off_2875 on theBenchmark for (2875ds/17627Mi) % 153.64/21.90 % (3837794)Instruction limit reached! % 153.64/21.90 % (3837794)------------------------------ % 153.64/21.90 % (3837794)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 153.64/21.90 % (3837794)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 153.64/21.90 % (3837794)CaDiCaL version: 2.1.3 % 153.64/21.90 % (3837794)Termination reason: Instruction limit % 153.64/21.90 % (3837794)Termination phase: Saturation % 153.64/21.90 % (3837794)Time elapsed: 7.373 s % 153.64/21.90 % (3837794)Peak memory usage: 47 MB % 153.64/21.90 % (3837794)Instructions burned: 11405 (million) % 153.64/21.90 % (3837802)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=258147251:s2a=on:i=53295_2870 on theBenchmark for (2870ds/53295Mi) % 153.64/21.90 % (3837798)Instruction limit reached! % 153.64/21.90 % (3837798)------------------------------ % 153.64/21.90 % (3837798)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 153.64/21.90 % (3837798)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 153.64/21.90 % (3837798)CaDiCaL version: 2.1.3 % 153.64/21.90 % (3837798)Termination reason: Instruction limit % 153.64/21.90 % (3837798)Termination phase: Saturation % 153.64/21.90 % (3837798)Time elapsed: 3.671 s % 153.64/21.90 % (3837798)Peak memory usage: 35 MB % 153.64/21.90 % (3837798)Instructions burned: 15852 (million) % 153.64/21.90 % (3837804)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=3601940636:i=26857:ins=20_2847 on theBenchmark for (2847ds/26857Mi) % 153.64/21.90 % (3837804)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 153.64/21.90 % (3837804)Terminated due to inappropriate strategy. % 153.64/21.90 % (3837804)------------------------------ % 153.64/21.90 % (3837804)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 153.64/21.90 % (3837804)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 153.64/21.90 % (3837804)CaDiCaL version: 2.1.3 % 153.64/21.90 % (3837804)Termination reason: Inappropriate % 153.64/21.90 % (3837804)Time elapsed: 0.015 s % 153.64/21.90 % (3837804)Peak memory usage: 13 MB % 153.64/21.90 % (3837804)Instructions burned: 67 (million) % 153.64/21.90 % (3837804)------------------------------ % 153.64/21.90 % (3837804)------------------------------ % 153.64/21.90 % (3837806)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=699148560:i=28120:bs=on:fsr=off_2847 on theBenchmark for (2847ds/28120Mi) % 153.64/21.90 % (3837774)Instruction limit reached! % 153.64/21.90 % (3837774)------------------------------ % 153.64/21.90 % (3837774)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 153.64/21.90 % (3837774)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 153.64/21.90 % (3837774)CaDiCaL version: 2.1.3 % 153.64/21.90 % (3837774)Termination reason: Instruction limit % 153.64/21.91 % (3837774)Termination phase: Saturation % 153.64/21.91 % (3837774)Time elapsed: 13.677 s % 153.64/21.91 % (3837774)Peak memory usage: 41 MB % 153.64/21.91 % (3837774)Instructions burned: 29340 (million) % 153.64/21.91 % (3837808)fmb+10_1_sil=256000:fmbss=7:random_seed=2925275481:fmbsr=1.6:i=182295_2841 on theBenchmark for (2841ds/182295Mi) % 153.64/21.91 % (3837808)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 153.64/21.91 % (3837808)Terminated due to inappropriate strategy. % 153.64/21.91 % (3837808)------------------------------ % 153.64/21.91 % (3837808)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 153.64/21.91 % (3837808)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 153.64/21.91 % (3837808)CaDiCaL version: 2.1.3 % 153.64/21.91 % (3837808)Termination reason: Inappropriate % 153.64/21.91 % (3837808)Time elapsed: 0.028 s % 153.64/21.91 % (3837808)Peak memory usage: 13 MB % 153.64/21.91 % (3837808)Instructions burned: 67 (million) % 153.64/21.91 % (3837808)------------------------------ % 153.64/21.91 % (3837808)------------------------------ % 153.64/21.91 % (3837810)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=2212007810:i=44625:gsp=on_2841 on theBenchmark for (2841ds/44625Mi) % 159.72/22.84 % (3837810)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 159.72/22.84 % (3837810)Terminated due to inappropriate strategy. % 159.72/22.84 % (3837810)------------------------------ % 159.72/22.84 % (3837810)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 159.72/22.84 % (3837810)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 159.72/22.84 % (3837810)CaDiCaL version: 2.1.3 % 159.72/22.84 % (3837810)Termination reason: Inappropriate % 159.72/22.84 % (3837810)Time elapsed: 0.032 s % 159.72/22.84 % (3837810)Peak memory usage: 13 MB % 159.72/22.84 % (3837810)Instructions burned: 70 (million) % 159.72/22.84 % (3837810)------------------------------ % 159.72/22.84 % (3837810)------------------------------ % 159.72/22.84 % (3837812)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=3203748080:i=160505_2840 on theBenchmark for (2840ds/160505Mi) % 159.72/22.84 % (3837812)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 159.72/22.84 % (3837812)Terminated due to inappropriate strategy. % 159.72/22.84 % (3837812)------------------------------ % 159.72/22.84 % (3837812)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 159.72/22.84 % (3837812)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 159.72/22.84 % (3837812)CaDiCaL version: 2.1.3 % 159.72/22.84 % (3837812)Termination reason: Inappropriate % 159.72/22.84 % (3837812)Time elapsed: 0.030 s % 159.72/22.84 % (3837812)Peak memory usage: 13 MB % 159.72/22.84 % (3837812)Instructions burned: 67 (million) % 159.72/22.84 % (3837812)------------------------------ % 159.72/22.84 % (3837812)------------------------------ % 159.72/22.84 % (3837814)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=1283804931:fmbsr=1.3:i=225729_2840 on theBenchmark for (2840ds/225729Mi) % 159.72/22.84 % (3837814)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 159.72/22.84 % (3837814)Terminated due to inappropriate strategy. % 159.72/22.84 % (3837814)------------------------------ % 159.72/22.84 % (3837814)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 159.72/22.84 % (3837814)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 159.72/22.84 % (3837814)CaDiCaL version: 2.1.3 % 159.72/22.84 % (3837814)Termination reason: Inappropriate % 159.72/22.84 % (3837814)Time elapsed: 0.039 s % 159.72/22.84 % (3837814)Peak memory usage: 13 MB % 159.72/22.84 % (3837814)Instructions burned: 93 (million) % 159.72/22.84 % (3837814)------------------------------ % 159.72/22.84 % (3837814)------------------------------ % 159.72/22.84 % (3837816)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=93391542:fmbsr=2:i=185024:ins=7_2839 on theBenchmark for (2839ds/185024Mi) % 159.72/22.84 % (3837816)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 159.72/22.84 % (3837816)Terminated due to inappropriate strategy. % 159.72/22.84 % (3837816)------------------------------ % 159.72/22.84 % (3837816)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 159.72/22.84 % (3837816)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 159.72/22.84 % (3837816)CaDiCaL version: 2.1.3 % 159.72/22.84 % (3837816)Termination reason: Inappropriate % 159.72/22.84 % (3837816)Time elapsed: 0.039 s % 159.72/22.84 % (3837816)Peak memory usage: 13 MB % 159.72/22.84 % (3837816)Instructions burned: 94 (million) % 159.72/22.84 % (3837816)------------------------------ % 159.72/22.84 % (3837816)------------------------------ % 159.72/22.84 % (3837818)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=1729758571:rtra=on_2839 on theBenchmark for (2839ds/0Mi) % 159.72/22.84 % (3837818)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 159.72/22.84 % (3837818)Terminated due to inappropriate strategy. % 159.72/22.84 % (3837818)------------------------------ % 159.72/22.84 % (3837818)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 159.72/22.84 % (3837818)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 159.72/22.84 % (3837818)CaDiCaL version: 2.1.3 % 159.72/22.84 % (3837818)Termination reason: Inappropriate % 159.72/22.84 % (3837818)Time elapsed: 0.037 s % 159.72/22.84 % (3837818)Peak memory usage: 14 MB % 159.72/22.84 % (3837818)Instructions burned: 79 (million) % 159.72/22.84 % (3837818)------------------------------ % 159.72/22.84 % (3837818)------------------------------ % 159.72/22.84 % (3837820)% WARNING: option uhcvi not known. % 159.72/22.84 % (3837820)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3518511105:i=271062:add=off:rtra=on:rawr=on_2838 on theBenchmark for (2838ds/271062Mi) % 168.71/24.05 % (3837796)Instruction limit reached! % 168.71/24.05 % (3837796)------------------------------ % 168.71/24.05 % (3837796)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 168.71/24.05 % (3837796)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 168.71/24.05 % (3837796)CaDiCaL version: 2.1.3 % 168.71/24.05 % (3837796)Termination reason: Instruction limit % 168.71/24.05 % (3837796)Termination phase: Saturation % 168.71/24.05 % (3837796)Time elapsed: 8.836 s % 168.71/24.05 % (3837796)Peak memory usage: 51 MB % 168.71/24.05 % (3837796)Instructions burned: 14135 (million) % 168.71/24.05 % (3837822)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1590858099:i=176048:add=on:rtra=on:rawr=on_2827 on theBenchmark for (2827ds/176048Mi) % 168.71/24.05 % (3837806)Instruction limit reached! % 168.71/24.05 % (3837806)------------------------------ % 168.71/24.05 % (3837806)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 168.71/24.05 % (3837806)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 168.71/24.05 % (3837806)CaDiCaL version: 2.1.3 % 168.71/24.05 % (3837806)Termination reason: Instruction limit % 168.71/24.05 % (3837806)Termination phase: Saturation % 168.71/24.05 % (3837806)Time elapsed: 6.049 s % 168.71/24.05 % (3837806)Peak memory usage: 24 MB % 168.71/24.05 % (3837806)Instructions burned: 28121 (million) % 168.71/24.05 % (3837824)dis+10_1_sil=32000:si=on:sp=arity:random_seed=272537029:i=206:fgj=on:rtra=on_2786 on theBenchmark for (2786ds/206Mi) % 168.71/24.05 % (3837824)Instruction limit reached! % 168.71/24.05 % (3837824)------------------------------ % 168.71/24.05 % (3837824)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 168.71/24.05 % (3837824)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 168.71/24.05 % (3837824)CaDiCaL version: 2.1.3 % 168.71/24.05 % (3837824)Termination reason: Instruction limit % 168.71/24.05 % (3837824)Termination phase: Saturation % 168.71/24.05 % (3837824)Time elapsed: 0.057 s % 168.71/24.05 % (3837824)Peak memory usage: 16 MB % 168.71/24.05 % (3837824)Instructions burned: 209 (million) % 168.71/24.05 % (3837826)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=3956466226:i=232:rtra=on_2785 on theBenchmark for (2785ds/232Mi) % 168.71/24.05 % (3837826)Instruction limit reached! % 168.71/24.05 % (3837826)------------------------------ % 168.71/24.05 % (3837826)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 168.71/24.05 % (3837826)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 168.71/24.05 % (3837826)CaDiCaL version: 2.1.3 % 168.71/24.05 % (3837826)Termination reason: Instruction limit % 168.71/24.05 % (3837826)Termination phase: Saturation % 168.71/24.05 % (3837826)Time elapsed: 0.061 s % 168.71/24.05 % (3837826)Peak memory usage: 16 MB % 168.71/24.05 % (3837826)Instructions burned: 235 (million) % 168.71/24.05 % (3837828)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=1633728667:i=262:rtra=on_2785 on theBenchmark for (2785ds/262Mi) % 168.71/24.05 % (3837828)Instruction limit reached! % 168.71/24.05 % (3837828)------------------------------ % 168.71/24.05 % (3837828)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 168.71/24.05 % (3837828)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 168.71/24.05 % (3837828)CaDiCaL version: 2.1.3 % 168.71/24.05 % (3837828)Termination reason: Instruction limit % 168.71/24.05 % (3837828)Termination phase: Saturation % 168.71/24.05 % (3837828)Time elapsed: 0.063 s % 168.71/24.05 % (3837828)Peak memory usage: 16 MB % 168.71/24.05 % (3837828)Instructions burned: 263 (million) % 168.71/24.05 % (3837830)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=229315186:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2784 on theBenchmark for (2784ds/318Mi) % 168.71/24.05 % (3837830)Instruction limit reached! % 168.71/24.05 % (3837830)------------------------------ % 168.71/24.05 % (3837830)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 168.71/24.05 % (3837830)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 168.71/24.05 % (3837830)CaDiCaL version: 2.1.3 % 168.71/24.05 % (3837830)Termination reason: Instruction limit % 168.71/24.05 % (3837830)Termination phase: Saturation % 168.71/24.05 % (3837830)Time elapsed: 0.087 s % 168.71/24.05 % (3837830)Peak memory usage: 18 MB % 168.71/24.05 % (3837830)Instructions burned: 320 (million) % 168.71/24.05 % (3837832)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=1199390002:i=1428:nm=2:rtra=on_2783 on theBenchmark for (2783ds/1428Mi) % 182.02/25.94 % (3837832)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 182.02/25.94 % (3837832)Terminated due to inappropriate strategy. % 182.02/25.94 % (3837832)------------------------------ % 182.02/25.94 % (3837832)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 182.02/25.94 % (3837832)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 182.02/25.94 % (3837832)CaDiCaL version: 2.1.3 % 182.02/25.94 % (3837832)Termination reason: Inappropriate % 182.02/25.94 % (3837832)Time elapsed: 0.020 s % 182.02/25.94 % (3837832)Peak memory usage: 14 MB % 182.02/25.94 % (3837832)Instructions burned: 79 (million) % 182.02/25.94 % (3837832)------------------------------ % 182.02/25.94 % (3837832)------------------------------ % 182.02/25.94 % (3837834)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=227589859:i=262:bd=preordered:rtra=on:fsd=on_2783 on theBenchmark for (2783ds/262Mi) % 182.02/25.94 % (3837834)Instruction limit reached! % 182.02/25.94 % (3837834)------------------------------ % 182.02/25.94 % (3837834)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 182.02/25.94 % (3837834)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 182.02/25.94 % (3837834)CaDiCaL version: 2.1.3 % 182.02/25.94 % (3837834)Termination reason: Instruction limit % 182.02/25.94 % (3837834)Termination phase: Saturation % 182.02/25.94 % (3837834)Time elapsed: 0.063 s % 182.02/25.94 % (3837834)Peak memory usage: 16 MB % 182.02/25.94 % (3837834)Instructions burned: 262 (million) % 182.02/25.94 % (3837836)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=2681013420:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2782 on theBenchmark for (2782ds/1368Mi) % 182.02/25.94 % (3837836)Instruction limit reached! % 182.02/25.94 % (3837836)------------------------------ % 182.02/25.94 % (3837836)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 182.02/25.94 % (3837836)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 182.02/25.94 % (3837836)CaDiCaL version: 2.1.3 % 182.02/25.94 % (3837836)Termination reason: Instruction limit % 182.02/25.94 % (3837836)Termination phase: Saturation % 182.02/25.94 % (3837836)Time elapsed: 0.376 s % 182.02/25.94 % (3837836)Peak memory usage: 21 MB % 182.02/25.94 % (3837836)Instructions burned: 1369 (million) % 182.02/25.94 % (3837838)ott-21_1_sil=16000:si=on:fs=off:random_seed=1850381249:i=360:av=off:fsr=off:rtra=on_2778 on theBenchmark for (2778ds/360Mi) % 182.02/25.94 % (3837838)Instruction limit reached! % 182.02/25.94 % (3837838)------------------------------ % 182.02/25.94 % (3837838)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 182.02/25.94 % (3837838)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 182.02/25.94 % (3837838)CaDiCaL version: 2.1.3 % 182.02/25.94 % (3837838)Termination reason: Instruction limit % 182.02/25.94 % (3837838)Termination phase: Saturation % 182.02/25.94 % (3837838)Time elapsed: 0.095 s % 182.02/25.94 % (3837838)Peak memory usage: 16 MB % 182.02/25.94 % (3837838)Instructions burned: 362 (million) % 182.02/25.94 % (3837840)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2963909913:i=954:bd=all:rtra=on_2777 on theBenchmark for (2777ds/954Mi) % 182.02/25.94 % (3837840)Instruction limit reached! % 182.02/25.94 % (3837840)------------------------------ % 182.02/25.94 % (3837840)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 182.02/25.94 % (3837840)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 182.02/25.94 % (3837840)CaDiCaL version: 2.1.3 % 182.02/25.94 % (3837840)Termination reason: Instruction limit % 182.02/25.94 % (3837840)Termination phase: Saturation % 182.02/25.94 % (3837840)Time elapsed: 0.298 s % 182.02/25.94 % (3837840)Peak memory usage: 19 MB % 182.02/25.94 % (3837840)Instructions burned: 955 (million) % 182.02/25.94 % (3837842)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=3978434543:fmbsr=1.3:i=1730:ins=25:rtra=on_2774 on theBenchmark for (2774ds/1730Mi) % 182.02/25.94 % (3837842)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 182.02/25.94 % (3837842)Terminated due to inappropriate strategy. % 182.02/25.94 % (3837842)------------------------------ % 182.02/25.94 % (3837842)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 182.02/25.94 % (3837842)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 182.02/25.94 % (3837842)CaDiCaL version: 2.1.3 % 182.02/25.94 % (3837842)Termination reason: Inappropriate % 220.35/31.38 % (3837842)Time elapsed: 0.020 s % 220.35/31.38 % (3837842)Peak memory usage: 14 MB % 220.35/31.38 % (3837842)Instructions burned: 78 (million) % 220.35/31.38 % (3837842)------------------------------ % 220.35/31.38 % (3837842)------------------------------ % 220.35/31.38 % (3837844)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=3929004508:i=2358:rtra=on_2773 on theBenchmark for (2773ds/2358Mi) % 220.35/31.38 % (3837800)Instruction limit reached! % 220.35/31.38 % (3837800)------------------------------ % 220.35/31.38 % (3837800)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 220.35/31.38 % (3837800)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 220.35/31.38 % (3837800)CaDiCaL version: 2.1.3 % 220.35/31.38 % (3837800)Termination reason: Instruction limit % 220.35/31.38 % (3837800)Termination phase: Saturation % 220.35/31.38 % (3837800)Time elapsed: 10.433 s % 220.35/31.38 % (3837800)Peak memory usage: 122 MB % 220.35/31.38 % (3837800)Instructions burned: 17627 (million) % 220.35/31.38 % (3837846)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=4038682482:i=1778:ins=1:rtra=on_2771 on theBenchmark for (2771ds/1778Mi) % 220.35/31.38 % (3837846)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 220.35/31.38 % (3837846)Terminated due to inappropriate strategy. % 220.35/31.38 % (3837846)------------------------------ % 220.35/31.38 % (3837846)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 220.35/31.38 % (3837846)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 220.35/31.38 % (3837846)CaDiCaL version: 2.1.3 % 220.35/31.38 % (3837846)Termination reason: Inappropriate % 220.35/31.38 % (3837846)Time elapsed: 0.050 s % 220.35/31.38 % (3837846)Peak memory usage: 15 MB % 220.35/31.38 % (3837846)Instructions burned: 105 (million) % 220.35/31.38 % (3837846)------------------------------ % 220.35/31.38 % (3837846)------------------------------ % 220.35/31.38 % (3837848)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=1955206705:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2770 on theBenchmark for (2770ds/1384Mi) % 220.35/31.38 % (3837844)Instruction limit reached! % 220.35/31.38 % (3837844)------------------------------ % 220.35/31.38 % (3837844)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 220.35/31.38 % (3837844)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 220.35/31.38 % (3837844)CaDiCaL version: 2.1.3 % 220.35/31.38 % (3837844)Termination reason: Instruction limit % 220.35/31.38 % (3837844)Termination phase: Saturation % 220.35/31.38 % (3837844)Time elapsed: 0.723 s % 220.35/31.38 % (3837844)Peak memory usage: 24 MB % 220.35/31.38 % (3837844)Instructions burned: 2361 (million) % 220.35/31.38 % (3837850)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=2984797077:i=1758:kws=inv_precedence:fsr=off:rtra=on_2766 on theBenchmark for (2766ds/1758Mi) % 220.35/31.38 % (3837848)Instruction limit reached! % 220.35/31.38 % (3837848)------------------------------ % 220.35/31.38 % (3837848)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 220.35/31.38 % (3837848)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 220.35/31.38 % (3837848)CaDiCaL version: 2.1.3 % 220.35/31.38 % (3837848)Termination reason: Instruction limit % 220.35/31.38 % (3837848)Termination phase: Saturation % 220.35/31.38 % (3837848)Time elapsed: 0.762 s % 220.35/31.38 % (3837848)Peak memory usage: 23 MB % 220.35/31.38 % (3837848)Instructions burned: 1384 (million) % 220.35/31.38 % (3837852)fmb+10_1_sil=64000:si=on:random_seed=3157645638:i=44122:nm=2:rtra=on:gsp=on_2762 on theBenchmark for (2762ds/44122Mi) % 220.35/31.38 % (3837852)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 220.35/31.38 % (3837852)Terminated due to inappropriate strategy. % 220.35/31.38 % (3837852)------------------------------ % 220.35/31.38 % (3837852)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 220.35/31.38 % (3837852)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 220.35/31.38 % (3837852)CaDiCaL version: 2.1.3 % 220.35/31.38 % (3837852)Termination reason: Inappropriate % 220.35/31.38 % (3837852)Time elapsed: 0.040 s % 220.35/31.38 % (3837852)Peak memory usage: 14 MB % 220.35/31.38 % (3837852)Instructions burned: 85 (million) % 220.35/31.38 % (3837852)------------------------------ % 220.35/31.38 % (3837852)------------------------------ % 220.35/31.38 % (3837854)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=2796472117:i=19030:nm=5:rtra=on_2762 on theBenchmark for (2762ds/19030Mi) % 250.16/35.59 % (3837854)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 250.16/35.59 % (3837854)Terminated due to inappropriate strategy. % 250.16/35.59 % (3837854)------------------------------ % 250.16/35.59 % (3837854)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 250.16/35.59 % (3837854)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 250.16/35.59 % (3837854)CaDiCaL version: 2.1.3 % 250.16/35.59 % (3837854)Termination reason: Inappropriate % 250.16/35.59 % (3837854)Time elapsed: 0.037 s % 250.16/35.59 % (3837854)Peak memory usage: 14 MB % 250.16/35.59 % (3837854)Instructions burned: 79 (million) % 250.16/35.59 % (3837854)------------------------------ % 250.16/35.59 % (3837854)------------------------------ % 250.16/35.59 % (3837856)fmb+10_1_sil=64000:sas=cadical:si=on:fmbss=8:random_seed=3502086225:fmbsr=1.7:i=1840:rtra=on_2761 on theBenchmark for (2761ds/1840Mi) % 250.16/35.59 % (3837850)Instruction limit reached! % 250.16/35.59 % (3837850)------------------------------ % 250.16/35.59 % (3837850)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 250.16/35.59 % (3837850)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 250.16/35.59 % (3837850)CaDiCaL version: 2.1.3 % 250.16/35.59 % (3837850)Termination reason: Instruction limit % 250.16/35.59 % (3837850)Termination phase: Saturation % 250.16/35.59 % (3837850)Time elapsed: 0.542 s % 250.16/35.59 % (3837850)Peak memory usage: 29 MB % 250.16/35.59 % (3837850)Instructions burned: 1758 (million) % 250.16/35.59 % (3837858)dis-4_1_sil=16000:drc=ordering:si=on:sp=const_frequency:sac=on:newcnf=on:random_seed=3579913654:i=10262:rtra=on_2761 on theBenchmark for (2761ds/10262Mi) % 250.16/35.59 % (3837856)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 250.16/35.59 % (3837856)Terminated due to inappropriate strategy. % 250.16/35.59 % (3837856)------------------------------ % 250.16/35.59 % (3837856)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 250.16/35.59 % (3837856)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 250.16/35.59 % (3837856)CaDiCaL version: 2.1.3 % 250.16/35.59 % (3837856)Termination reason: Inappropriate % 250.16/35.59 % (3837856)Time elapsed: 0.038 s % 250.16/35.59 % (3837856)Peak memory usage: 14 MB % 250.16/35.59 % (3837856)Instructions burned: 79 (million) % 250.16/35.59 % (3837856)------------------------------ % 250.16/35.59 % (3837856)------------------------------ % 250.16/35.59 % (3837860)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:si=on:sp=arity:spb=units:lsd=10:nwc=3:random_seed=169632520:i=2944:ins=7:rtra=on:fdi=8:gsp=on_2760 on theBenchmark for (2760ds/2944Mi) % 250.16/35.59 % (3837860)Instruction limit reached! % 250.16/35.59 % (3837860)------------------------------ % 250.16/35.59 % (3837860)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 250.16/35.59 % (3837860)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 250.16/35.59 % (3837860)CaDiCaL version: 2.1.3 % 250.16/35.59 % (3837860)Termination reason: Instruction limit % 250.16/35.59 % (3837860)Termination phase: Saturation % 250.16/35.59 % (3837860)Time elapsed: 1.655 s % 250.16/35.59 % (3837860)Peak memory usage: 33 MB % 250.16/35.59 % (3837860)Instructions burned: 2945 (million) % 250.16/35.59 % (3837862)fmb+10_1_sil=16000:sas=cadical:si=on:bce=on:fmbss=77:random_seed=1899609729:i=12648:rtra=on_2744 on theBenchmark for (2744ds/12648Mi) % 250.16/35.59 % (3837862)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 250.16/35.59 % (3837862)Terminated due to inappropriate strategy. % 250.16/35.59 % (3837862)------------------------------ % 250.16/35.59 % (3837862)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 250.16/35.59 % (3837862)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 250.16/35.59 % (3837862)CaDiCaL version: 2.1.3 % 250.16/35.59 % (3837862)Termination reason: Inappropriate % 250.16/35.59 % (3837862)Time elapsed: 0.038 s % 250.16/35.59 % (3837862)Peak memory usage: 14 MB % 250.16/35.59 % (3837862)Instructions burned: 79 (million) % 250.16/35.59 % (3837862)------------------------------ % 250.16/35.59 % (3837862)------------------------------ % 250.16/35.59 % (3837864)fmb+10_1_fmbas=function:sil=32000:sas=cadical:si=on:fmbss=16:random_seed=3222973578:fmbsr=2.30978:i=4348:rtra=on_2743 on theBenchmark for (2743ds/4348Mi) % 250.16/35.59 % (3837864)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 250.16/35.59 % (3837864)Terminated due to inappropriate strategy. % 250.16/35.59 % (3837864)-----------------------Terminated % 300.58/42.64 % Vampire exiting % 300.58/42.64 Terminated %------------------------------------------------------------------------------