%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWW475_3 : TPTP v9.3.1. Released v5.3.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % Computer : n003.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:13 PM UTC 2026 % Result : Timeout 300.31s 42.74s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.04 % Problem : SWW475_3 : TPTP v9.3.1. Released v5.3.0. % 0.00/0.08 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.10/0.26 % Computer : n003.cluster.edu % 0.10/0.26 % Model : x86_64 x86_64 % 0.10/0.26 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.26 % Memory : 8046.5625MB % 0.10/0.26 % OS : Linux 6.8.0-71-generic % 0.10/0.26 % CPULimit : 300 % 0.10/0.26 % WCLimit : 300 % 0.10/0.26 % DateTime : Mon Sep 28 14:11:42 UTC 2026 % 0.10/0.27 % CPUTime : % 0.10/0.27 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.26/0.32 Running first-order model finding % 0.26/0.32 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 % 28.66/4.52 % (1606981)Will run a generic schedule for satisfiability detection. % 28.66/4.52 % (1606991)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3818478748:i=131_2998 on theBenchmark for (2998ds/131Mi) % 28.66/4.52 % (1606986)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=586946938_2998 on theBenchmark for (2998ds/0Mi) % 28.66/4.52 % (1606987)% WARNING: option uhcvi not known. % 28.66/4.52 % (1606990)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1641361373:i=116_2998 on theBenchmark for (2998ds/116Mi) % 28.66/4.52 % (1606989)dis+10_1_sil=32000:sp=arity:random_seed=2455229581:i=103:fgj=on_2998 on theBenchmark for (2998ds/103Mi) % 28.66/4.52 % (1606988)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=167633157:i=88024:add=on:rawr=on_2998 on theBenchmark for (2998ds/88024Mi) % 28.66/4.52 % (1606987)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1316481533:i=135531:add=off:rawr=on_2998 on theBenchmark for (2998ds/135531Mi) % 28.66/4.52 % (1606992)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=4132884953:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2998 on theBenchmark for (2998ds/159Mi) % 28.66/4.52 % (1606991)Instruction limit reached! % 28.66/4.52 % (1606991)------------------------------ % 28.66/4.52 % (1606991)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 28.66/4.52 % (1606991)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.66/4.52 % (1606991)CaDiCaL version: 2.1.3 % 28.66/4.52 % (1606991)Termination reason: Instruction limit % 28.66/4.52 % (1606991)Termination phase: Saturation % 28.66/4.52 % (1606991)Time elapsed: 0.063 s % 28.66/4.52 % (1606991)Peak memory usage: 15 MB % 28.66/4.52 % (1606991)Instructions burned: 132 (million) % 28.66/4.52 % (1607000)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=117505439:i=714:nm=2_2998 on theBenchmark for (2998ds/714Mi) % 28.66/4.52 % (1606989)Instruction limit reached! % 28.66/4.52 % (1606989)------------------------------ % 28.66/4.52 % (1606989)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 28.66/4.52 % (1606989)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.66/4.52 % (1606989)CaDiCaL version: 2.1.3 % 28.66/4.52 % (1606989)Termination reason: Instruction limit % 28.66/4.52 % (1606989)Termination phase: Property scanning % 28.66/4.52 % (1606989)Time elapsed: 0.093 s % 28.66/4.52 % (1606989)Peak memory usage: 14 MB % 28.66/4.52 % (1606989)Instructions burned: 104 (million) % 28.66/4.52 % (1606990)Instruction limit reached! % 28.66/4.52 % (1606990)------------------------------ % 28.66/4.52 % (1606990)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 28.66/4.52 % (1606990)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.66/4.52 % (1606990)CaDiCaL version: 2.1.3 % 28.66/4.52 % (1606990)Termination reason: Instruction limit % 28.66/4.52 % (1606990)Termination phase: Property scanning % 28.66/4.52 % (1606990)Time elapsed: 0.101 s % 28.66/4.52 % (1606990)Peak memory usage: 14 MB % 28.66/4.52 % (1606990)Instructions burned: 116 (million) % 28.66/4.52 % (1607002)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=166580263:i=131:bd=preordered:fsd=on_2997 on theBenchmark for (2997ds/131Mi) % 28.66/4.52 % (1607003)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=1310351775:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2997 on theBenchmark for (2997ds/684Mi) % 28.66/4.52 % (1606992)Instruction limit reached! % 28.66/4.52 % (1606992)------------------------------ % 28.66/4.52 % (1606992)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 28.66/4.52 % (1606992)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.66/4.52 % (1606992)CaDiCaL version: 2.1.3 % 28.66/4.52 % (1606992)Termination reason: Instruction limit % 28.66/4.52 % (1606992)Termination phase: Saturation % 28.66/4.52 % (1606992)Time elapsed: 0.145 s % 28.66/4.52 % (1606992)Peak memory usage: 16 MB % 28.66/4.52 % (1606992)Instructions burned: 159 (million) % 28.66/4.52 % (1607006)ott-21_1_sil=16000:fs=off:random_seed=2513447807:i=180:av=off:fsr=off_2997 on theBenchmark for (2997ds/180Mi) % 28.66/4.52 % (1607002)Instruction limit reached! % 28.66/4.52 % (1607002)------------------------------ % 28.66/4.52 % (1607002)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 28.66/4.52 % (1607002)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 91.60/13.32 % (1607002)CaDiCaL version: 2.1.3 % 91.60/13.32 % (1607002)Termination reason: Instruction limit % 91.60/13.32 % (1607002)Termination phase: Blocked clause elimination % 91.60/13.32 % (1607002)Time elapsed: 0.111 s % 91.60/13.32 % (1607002)Peak memory usage: 15 MB % 91.60/13.32 % (1607002)Instructions burned: 131 (million) % 91.60/13.32 % (1607008)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=770078451:i=477:bd=all_2996 on theBenchmark for (2996ds/477Mi) % 91.60/13.32 % (1607006)Instruction limit reached! % 91.60/13.32 % (1607006)------------------------------ % 91.60/13.32 % (1607006)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 91.60/13.32 % (1607006)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 91.60/13.32 % (1607006)CaDiCaL version: 2.1.3 % 91.60/13.32 % (1607006)Termination reason: Instruction limit % 91.60/13.32 % (1607006)Termination phase: Saturation % 91.60/13.32 % (1607006)Time elapsed: 0.133 s % 91.60/13.32 % (1607006)Peak memory usage: 15 MB % 91.60/13.32 % (1607006)Instructions burned: 180 (million) % 91.60/13.32 % (1607012)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=976181437:fmbsr=1.3:i=865:ins=25_2995 on theBenchmark for (2995ds/865Mi) % 91.60/13.32 % (1607000)Instruction limit reached! % 91.60/13.32 % (1607000)------------------------------ % 91.60/13.32 % (1607000)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 91.60/13.32 % (1607000)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 91.60/13.32 % (1607000)CaDiCaL version: 2.1.3 % 91.60/13.32 % (1607000)Termination reason: Instruction limit % 91.60/13.32 % (1607000)Termination phase: Finite model building preprocessing % 91.60/13.32 % (1607000)Time elapsed: 0.306 s % 91.60/13.32 % (1607000)Peak memory usage: 18 MB % 91.60/13.32 % (1607000)Instructions burned: 716 (million) % 91.60/13.32 % (1607014)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1658235165:i=1179_2994 on theBenchmark for (2994ds/1179Mi) % 91.60/13.32 % (1607008)Instruction limit reached! % 91.60/13.32 % (1607008)------------------------------ % 91.60/13.32 % (1607008)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 91.60/13.32 % (1607008)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 91.60/13.32 % (1607008)CaDiCaL version: 2.1.3 % 91.60/13.32 % (1607008)Termination reason: Instruction limit % 91.60/13.32 % (1607008)Termination phase: Saturation % 91.60/13.32 % (1607008)Time elapsed: 0.399 s % 91.60/13.32 % (1607008)Peak memory usage: 17 MB % 91.60/13.32 % (1607008)Instructions burned: 478 (million) % 91.60/13.32 % (1607016)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2164065005:i=889:ins=1_2991 on theBenchmark for (2991ds/889Mi) % 91.60/13.32 % (1607003)Instruction limit reached! % 91.60/13.32 % (1607003)------------------------------ % 91.60/13.32 % (1607003)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 91.60/13.32 % (1607003)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 91.60/13.32 % (1607003)CaDiCaL version: 2.1.3 % 91.60/13.32 % (1607003)Termination reason: Instruction limit % 91.60/13.32 % (1607003)Termination phase: Saturation % 91.60/13.32 % (1607003)Time elapsed: 0.628 s % 91.60/13.32 % (1607003)Peak memory usage: 19 MB % 91.60/13.32 % (1607003)Instructions burned: 684 (million) % 91.60/13.32 % (1607019)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=498617160:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2990 on theBenchmark for (2990ds/692Mi) % 91.60/13.32 % (1607014)Instruction limit reached! % 91.60/13.32 % (1607014)------------------------------ % 91.60/13.32 % (1607014)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 91.60/13.32 % (1607014)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 91.60/13.32 % (1607014)CaDiCaL version: 2.1.3 % 91.60/13.32 % (1607014)Termination reason: Instruction limit % 91.60/13.32 % (1607014)Termination phase: Saturation % 91.60/13.32 % (1607014)Time elapsed: 0.620 s % 91.60/13.32 % (1607014)Peak memory usage: 24 MB % 91.60/13.32 % (1607014)Instructions burned: 1179 (million) % 91.60/13.32 % (1607021)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2765450089:i=879:kws=inv_precedence:fsr=off_2988 on theBenchmark for (2988ds/879Mi) % 91.60/13.32 % (1607012)Instruction limit reached! % 91.60/13.32 % (1607012)------------------------------ % 91.60/13.32 % (1607012)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 91.60/13.32 % (1607012)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 110.93/16.08 % (1607012)CaDiCaL version: 2.1.3 % 110.93/16.08 % (1607012)Termination reason: Instruction limit % 110.93/16.08 % (1607012)Termination phase: Finite model building preprocessing % 110.93/16.08 % (1607012)Time elapsed: 0.779 s % 110.93/16.08 % (1607012)Peak memory usage: 24 MB % 110.93/16.08 % (1607012)Instructions burned: 865 (million) % 110.93/16.08 % (1607023)fmb+10_1_sil=64000:random_seed=2034480200:i=22061:nm=2:gsp=on_2987 on theBenchmark for (2987ds/22061Mi) % 110.93/16.08 % (1607016)Instruction limit reached! % 110.93/16.08 % (1607016)------------------------------ % 110.93/16.08 % (1607016)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 110.93/16.08 % (1607016)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 110.93/16.08 % (1607016)CaDiCaL version: 2.1.3 % 110.93/16.08 % (1607016)Termination reason: Instruction limit % 110.93/16.08 % (1607016)Termination phase: Finite model building preprocessing % 110.93/16.08 % (1607016)Time elapsed: 0.750 s % 110.93/16.08 % (1607016)Peak memory usage: 24 MB % 110.93/16.08 % (1607016)Instructions burned: 890 (million) % 110.93/16.08 % (1607019)Instruction limit reached! % 110.93/16.08 % (1607019)------------------------------ % 110.93/16.08 % (1607019)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 110.93/16.08 % (1607019)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 110.93/16.08 % (1607019)CaDiCaL version: 2.1.3 % 110.93/16.08 % (1607019)Termination reason: Instruction limit % 110.93/16.08 % (1607019)Termination phase: Saturation % 110.93/16.08 % (1607019)Time elapsed: 0.638 s % 110.93/16.08 % (1607019)Peak memory usage: 20 MB % 110.93/16.08 % (1607019)Instructions burned: 692 (million) % 110.93/16.08 % (1607026)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=4153076197:fmbsr=1.7:i=920_2984 on theBenchmark for (2984ds/920Mi) % 110.93/16.08 % (1607025)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1485319787:i=9515:nm=5_2984 on theBenchmark for (2984ds/9515Mi) % 110.93/16.08 % (1607021)Instruction limit reached! % 110.93/16.08 % (1607021)------------------------------ % 110.93/16.08 % (1607021)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 110.93/16.08 % (1607021)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 110.93/16.08 % (1607021)CaDiCaL version: 2.1.3 % 110.93/16.08 % (1607021)Termination reason: Instruction limit % 110.93/16.08 % (1607021)Termination phase: Saturation % 110.93/16.08 % (1607021)Time elapsed: 0.453 s % 110.93/16.08 % (1607021)Peak memory usage: 21 MB % 110.93/16.08 % (1607021)Instructions burned: 880 (million) % 110.93/16.08 % (1607029)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=3663708895:i=5131_2983 on theBenchmark for (2983ds/5131Mi) % 110.93/16.08 % (1607026)Instruction limit reached! % 110.93/16.08 % (1607026)------------------------------ % 110.93/16.08 % (1607026)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 110.93/16.08 % (1607026)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 110.93/16.08 % (1607026)CaDiCaL version: 2.1.3 % 110.93/16.08 % (1607026)Termination reason: Instruction limit % 110.93/16.08 % (1607026)Termination phase: Finite model building preprocessing % 110.93/16.08 % (1607026)Time elapsed: 0.826 s % 110.93/16.08 % (1607026)Peak memory usage: 25 MB % 110.93/16.08 % (1607026)Instructions burned: 920 (million) % 110.93/16.08 % (1607031)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1825186608:i=1472:ins=7:fdi=8:gsp=on_2975 on theBenchmark for (2975ds/1472Mi) % 110.93/16.08 % (1607031)Instruction limit reached! % 110.93/16.08 % (1607031)------------------------------ % 110.93/16.08 % (1607031)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 110.93/16.08 % (1607031)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 110.93/16.08 % (1607031)CaDiCaL version: 2.1.3 % 110.93/16.08 % (1607031)Termination reason: Instruction limit % 110.93/16.08 % (1607031)Termination phase: Saturation % 110.93/16.08 % (1607031)Time elapsed: 1.272 s % 110.93/16.08 % (1607031)Peak memory usage: 24 MB % 110.93/16.08 % (1607031)Instructions burned: 1473 (million) % 110.93/16.08 % (1607033)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=4056914620:i=6324_2962 on theBenchmark for (2962ds/6324Mi) % 110.93/16.08 % (1607029)Instruction limit reached! % 110.93/16.08 % (1607029)------------------------------ % 110.93/16.08 % (1607029)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 110.93/16.08 % (1607029)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 110.93/16.08 % (1607029)CaDiCaL version: 2.1.3 % 110.93/16.08 % (1607029)Termination reason: Instruction limit % 134.18/19.35 % (1607029)Termination phase: Saturation % 134.18/19.35 % (1607029)Time elapsed: 2.499 s % 134.18/19.35 % (1607029)Peak memory usage: 39 MB % 134.18/19.35 % (1607029)Instructions burned: 5133 (million) % 134.18/19.35 % (1607035)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=3693946822:fmbsr=2.30978:i=2174_2958 on theBenchmark for (2958ds/2174Mi) % 134.18/19.35 % (1607035)Instruction limit reached! % 134.18/19.35 % (1607035)------------------------------ % 134.18/19.35 % (1607035)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 134.18/19.35 % (1607035)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 134.18/19.35 % (1607035)CaDiCaL version: 2.1.3 % 134.18/19.35 % (1607035)Termination reason: Instruction limit % 134.18/19.35 % (1607035)Termination phase: Finite model building preprocessing % 134.18/19.35 % (1607035)Time elapsed: 1.023 s % 134.18/19.35 % (1607035)Peak memory usage: 33 MB % 134.18/19.35 % (1607035)Instructions burned: 2176 (million) % 134.18/19.35 % (1607037)ott-2_1_sil=16000:newcnf=on:random_seed=3988731412:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2947 on theBenchmark for (2947ds/869Mi) % 134.18/19.35 % (1607037)Instruction limit reached! % 134.18/19.35 % (1607037)------------------------------ % 134.18/19.35 % (1607037)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 134.18/19.35 % (1607037)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 134.18/19.35 % (1607037)CaDiCaL version: 2.1.3 % 134.18/19.35 % (1607037)Termination reason: Instruction limit % 134.18/19.35 % (1607037)Termination phase: Saturation % 134.18/19.35 % (1607037)Time elapsed: 0.422 s % 134.18/19.35 % (1607037)Peak memory usage: 19 MB % 134.18/19.35 % (1607037)Instructions burned: 871 (million) % 134.18/19.35 % (1607039)ott+10_1_sil=32000:tgt=ground:random_seed=2779678907:i=5114:av=off_2943 on theBenchmark for (2943ds/5114Mi) % 134.18/19.35 % (1607033)Instruction limit reached! % 134.18/19.35 % (1607033)------------------------------ % 134.18/19.35 % (1607033)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 134.18/19.35 % (1607033)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 134.18/19.35 % (1607033)CaDiCaL version: 2.1.3 % 134.18/19.35 % (1607033)Termination reason: Instruction limit % 134.18/19.35 % (1607033)Termination phase: Finite model building preprocessing % 134.18/19.35 % (1607033)Time elapsed: 5.473 s % 134.18/19.35 % (1607033)Peak memory usage: 63 MB % 134.18/19.35 % (1607033)Instructions burned: 6324 (million) % 134.18/19.35 % (1607055)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=109873503:i=54282_2907 on theBenchmark for (2907ds/54282Mi) % 134.18/19.35 % (1607025)Instruction limit reached! % 134.18/19.35 % (1607025)------------------------------ % 134.18/19.35 % (1607025)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 134.18/19.35 % (1607025)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 134.18/19.35 % (1607025)CaDiCaL version: 2.1.3 % 134.18/19.35 % (1607025)Termination reason: Instruction limit % 134.18/19.35 % (1607025)Termination phase: Finite model building preprocessing % 134.18/19.35 % (1607025)Time elapsed: 8.103 s % 134.18/19.35 % (1607025)Peak memory usage: 76 MB % 134.18/19.35 % (1607025)Instructions burned: 9516 (million) % 134.18/19.35 % (1607057)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3590420040:i=3512:aac=none_2902 on theBenchmark for (2902ds/3512Mi) % 134.18/19.35 % (1607039)Instruction limit reached! % 134.18/19.35 % (1607039)------------------------------ % 134.18/19.35 % (1607039)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 134.18/19.35 % (1607039)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 134.18/19.35 % (1607039)CaDiCaL version: 2.1.3 % 134.18/19.35 % (1607039)Termination reason: Instruction limit % 134.18/19.35 % (1607039)Termination phase: Saturation % 134.18/19.35 % (1607039)Time elapsed: 4.883 s % 134.18/19.35 % (1607039)Peak memory usage: 48 MB % 134.18/19.35 % (1607039)Instructions burned: 5114 (million) % 134.18/19.35 % (1607063)dis+21_1_sil=32000:sas=cadical:random_seed=240653741:i=3773:amm=off_2893 on theBenchmark for (2893ds/3773Mi) % 134.18/19.35 % (1607057)Instruction limit reached! % 134.18/19.35 % (1607057)------------------------------ % 134.18/19.35 % (1607057)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 134.18/19.35 % (1607057)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 134.18/19.35 % (1607057)CaDiCaL version: 2.1.3 % 134.18/19.35 % (1607057)Termination reason: Instruction limit % 134.18/19.35 % (1607057)Termination phase: Saturation % 134.18/19.35 % (1607057)Time elapsed: 3.232 s % 176.82/25.33 % (1607057)Peak memory usage: 36 MB % 176.82/25.33 % (1607057)Instructions burned: 3513 (million) % 176.82/25.33 % (1607069)ott+11_1_sil=16000:gs=on:random_seed=4105463665:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2870 on theBenchmark for (2870ds/2251Mi) % 176.82/25.33 % Detected minimum model sizes of [1,1,1,1,1,1,1,1,1,1,1,1,4,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1] % 176.82/25.33 % Detected maximum model sizes of [max,max,max,max,2,max,max,max,max,max,max,2,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max] % 176.82/25.33 % TRYING [1,1,1,1,1,1,1,1,1,1,1,1,4,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1] % 176.82/25.33 % TRYING [1,1,1,1,1,1,1,1,1,1,1,1,4,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,2,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1] % 176.82/25.33 % TRYING [1,1,1,1,1,1,1,1,1,1,1,1,4,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,3,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1] % 176.82/25.33 % TRYING [1,1,1,1,1,1,1,1,1,1,1,1,4,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,4,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1] % 176.82/25.33 % TRYING [1,1,1,1,1,1,1,1,1,1,1,1,4,1,1,1,1,1,1,1,1,1,1,1,1,1,2,1,4,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1] % 176.82/25.33 % TRYING [1,1,1,1,1,1,1,1,1,1,1,1,4,1,1,1,1,1,1,1,1,1,1,1,1,1,2,2,4,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1] % 176.82/25.33 % TRYING [1,1,1,1,1,1,1,1,1,1,1,1,4,1,1,1,1,1,1,1,1,1,1,1,1,1,3,2,4,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1] % 176.82/25.33 % TRYING [1,1,1,1,1,1,1,1,1,1,1,1,4,1,1,1,1,1,1,1,1,1,1,1,1,1,3,3,4,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1] % 176.82/25.33 % TRYING [1,1,1,1,1,1,1,1,1,1,1,1,4,1,1,1,1,1,1,1,1,1,1,1,1,1,4,3,4,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1] % 176.82/25.33 % TRYING [1,1,1,1,1,1,1,1,1,1,1,1,4,1,1,1,1,1,1,1,1,1,1,1,1,1,4,4,4,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1] % 176.82/25.33 % (1607063)Instruction limit reached! % 176.82/25.33 % (1607063)------------------------------ % 176.82/25.33 % (1607063)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 176.82/25.33 % (1607063)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 176.82/25.33 % (1607063)CaDiCaL version: 2.1.3 % 176.82/25.33 % (1607063)Termination reason: Instruction limit % 176.82/25.33 % (1607063)Termination phase: Saturation % 176.82/25.33 % (1607063)Time elapsed: 3.670 s % 176.82/25.33 % (1607063)Peak memory usage: 37 MB % 176.82/25.33 % (1607063)Instructions burned: 3774 (million) % 176.82/25.33 % TRYING [1,1,1,1,1,1,1,1,1,1,1,1,4,1,1,1,1,1,1,1,1,1,1,1,1,2,4,4,4,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1] % 176.82/25.33 % (1607077)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=2638951690:fmbsr=1.6:i=67534_2856 on theBenchmark for (2856ds/67534Mi) % 176.82/25.33 % TRYING [1,1,1,1,1,1,1,1,1,1,1,1,4,1,1,1,1,1,1,1,1,1,1,1,1,2,4,4,4,2,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1] % 176.82/25.33 % TRYING [1,1,1,1,1,1,1,1,1,1,1,1,4,1,1,1,1,1,1,1,1,1,1,1,1,2,4,4,4,2,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,2,1,1,1,1] % 176.82/25.33 % TRYING [1,1,1,1,1,1,1,1,1,1,1,1,4,1,1,1,1,1,1,1,1,1,1,1,1,2,4,4,4,2,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,3,1,1,1,1] % 176.82/25.33 % TRYING [1,1,1,1,1,1,1,1,1,1,1,1,4,1,1,1,1,1,1,1,1,1,1,1,1,2,4,4,4,2,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,4,1,1,1,1] % 176.82/25.33 % (1607069)Instruction limit reached! % 176.82/25.33 % (1607069)------------------------------ % 176.82/25.33 % (1607069)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 176.82/25.33 % (1607069)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 176.82/25.33 % (1607069)CaDiCaL version: 2.1.3 % 176.82/25.33 % (1607069)Termination reason: Instruction limit % 176.82/25.33 % (1607069)Termination phase: Saturation % 176.82/25.33 % (1607069)Time elapsed: 2.048 s % 176.82/25.33 % (1607069)Peak memory usage: 54 MB % 176.82/25.33 % (1607069)Instructions burned: 2252 (million) % 176.82/25.33 % (1607087)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=2077928690:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2849 on theBenchmark for (2849ds/4591Mi) % 176.82/25.33 % TRYING [1,1,1,1,1,1,1,1,1,1,1,1,4,1,1,1,1,1,1,1,1,1,1,1,1,2,4,4,4,3,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,4,1,1,1,1] % 176.82/25.33 % TRYING [1,1,1,1,1,1,1,1,1,1,1,1,4,1,1,1,1,1,1,1,1,1,1,1,1,3,4,4,4,3,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,4,1,1,1,1] % 176.82/25.33 % TRYING [1,1,1,1,1,1,1,1,1,1,1,1,4,1,1,1,1,1,1,1,1,1,1,1,1,4,4,4,4,3,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,4,1,1,1,1] % 176.82/25.33 % Detected minimum model sizes of [1,1,1,1,1,1,1,1,1,1,1,1,4,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1] % 200.56/28.71 % Detected maximum model sizes of [max,max,max,max,2,max,max,max,max,max,max,2,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max] % 200.56/28.71 % TRYING [1,1,1,1,1,1,1,1,1,1,1,1,4,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1] % 200.56/28.71 % TRYING [1,1,1,1,1,1,1,1,1,1,1,1,4,1,1,1,1,1,1,1,1,1,1,1,1,2,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1] % 200.56/28.71 % TRYING [1,1,1,1,1,1,1,1,1,1,1,1,4,1,1,1,1,1,1,1,1,1,1,1,1,2,1,1,1,2,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1] % 200.56/28.71 % TRYING [1,1,1,1,1,1,1,1,1,1,1,1,4,1,1,1,1,1,1,1,1,1,1,1,1,2,1,1,1,2,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,2,1,1,1,1] % 200.56/28.71 % TRYING [1,1,1,1,1,1,1,1,1,1,1,1,4,1,1,1,1,1,1,1,1,2,1,1,1,4,4,4,4,3,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,4,1,1,1,1] % 200.56/28.71 % TRYING [1,1,1,1,1,1,1,1,1,1,1,1,4,1,1,1,1,1,1,1,1,2,1,1,1,2,1,1,1,2,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,2,1,1,1,1] % 200.56/28.71 % TRYING [1,1,1,1,1,1,1,1,1,1,1,1,4,1,1,1,1,1,1,1,2,2,1,1,1,2,1,1,1,2,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,2,1,1,1,1] % 200.56/28.71 % TRYING [1,1,1,1,1,1,1,1,1,1,1,2,4,1,1,1,1,1,1,1,2,2,1,1,1,2,1,1,1,2,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,2,1,1,1,1] % 200.56/28.71 % TRYING [1,1,1,1,1,1,1,1,1,1,1,2,4,1,1,1,1,1,1,1,2,2,1,1,1,3,1,1,1,2,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,2,1,1,1,1] % 200.56/28.71 % TRYING [1,1,1,1,1,1,1,1,1,1,1,1,4,1,1,1,1,1,1,1,1,2,1,1,1,4,4,4,4,3,1,1,1,1,1,1,2,1,1,1,1,1,1,1,1,1,4,1,1,1,1] % 200.56/28.71 % TRYING [1,1,1,1,1,1,1,1,1,1,1,2,4,1,1,1,1,1,2,1,2,2,1,1,1,3,1,1,1,2,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,2,1,1,1,1] % 200.56/28.71 % TRYING [1,1,1,1,1,1,1,1,1,1,1,2,5,1,1,1,1,1,2,1,2,2,1,1,1,3,1,1,1,2,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,2,1,1,1,1] % 200.56/28.71 % TRYING [1,1,1,1,2,1,1,1,1,1,1,2,5,1,1,1,1,1,2,1,2,2,1,1,1,3,1,1,1,2,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,2,1,1,1,1] % 200.56/28.71 % TRYING [1,1,1,1,1,1,1,1,1,1,1,1,4,1,1,1,1,1,1,1,1,2,1,1,1,4,4,4,4,3,1,1,1,1,1,1,2,1,1,1,1,1,1,1,1,2,4,1,1,1,1] % 200.56/28.71 % TRYING [1,1,1,1,2,1,1,1,1,1,1,2,5,1,1,1,1,1,2,1,2,2,1,1,1,3,1,1,1,2,1,1,1,1,1,1,2,1,1,1,1,1,1,1,1,1,2,1,1,1,1] % 200.56/28.71 % TRYING [1,1,1,1,2,1,1,1,1,1,1,2,5,1,1,1,1,1,2,1,2,2,1,1,1,3,1,1,1,2,1,1,1,1,1,1,2,1,1,1,1,1,1,1,1,2,2,1,1,1,1] % 200.56/28.71 % TRYING [1,1,1,1,1,1,1,1,1,1,1,1,4,1,1,1,1,1,1,1,1,2,1,1,1,4,4,4,4,3,1,1,1,1,1,1,2,1,1,1,1,1,1,1,1,3,4,1,1,1,1] % 200.56/28.71 % TRYING [1,1,1,1,2,1,1,1,1,1,1,2,5,1,1,1,1,1,2,1,2,2,1,1,1,3,1,1,1,2,1,1,1,1,2,1,2,1,1,1,1,1,1,1,1,2,2,1,1,1,1] % 200.56/28.71 % TRYING [1,1,1,1,2,1,1,1,1,1,1,2,5,1,1,1,1,1,2,1,2,2,1,1,1,3,1,1,1,2,1,1,1,1,2,1,2,1,1,1,1,1,1,1,2,2,2,1,1,1,1] % 200.56/28.71 % TRYING [1,1,1,1,2,1,1,1,1,1,1,2,5,1,1,1,1,1,2,1,2,2,1,1,1,3,1,1,1,2,1,1,1,2,2,1,2,1,1,1,1,1,1,1,2,2,2,1,1,1,1] % 200.56/28.71 % TRYING [1,1,1,1,1,1,1,1,1,1,1,1,4,1,1,1,1,1,1,1,1,2,1,1,1,4,4,4,4,3,1,1,1,1,1,1,2,1,1,1,1,1,1,1,1,4,4,1,1,1,1] % 200.56/28.71 % TRYING [1,1,1,1,2,1,1,1,1,1,1,2,5,1,1,1,1,1,2,1,2,2,1,1,1,3,1,1,1,2,1,1,1,2,2,1,2,1,1,1,1,2,1,1,2,2,2,1,1,1,1] % 200.56/28.71 % TRYING [1,1,1,1,2,1,1,1,1,1,1,2,5,1,1,1,1,1,2,1,2,2,1,1,1,3,1,1,1,2,1,1,2,2,2,1,2,1,1,1,1,2,1,1,2,2,2,1,1,1,1] % 200.56/28.71 % TRYING [1,1,1,1,1,1,1,1,1,1,1,1,4,1,1,1,1,1,1,1,1,2,1,1,1,4,4,4,4,3,1,1,1,1,2,1,2,1,1,1,1,1,1,1,1,4,4,1,1,1,1] % 200.56/28.71 % TRYING [1,1,1,1,2,1,1,1,1,1,1,2,5,1,1,1,1,1,2,1,2,2,1,1,1,3,1,1,1,2,1,1,2,2,2,1,2,1,1,1,2,2,1,1,2,2,2,1,1,1,1] % 200.56/28.71 % TRYING [1,1,1,1,2,1,1,1,1,1,1,2,5,1,1,1,1,1,2,1,2,2,1,1,1,3,1,1,2,2,1,1,2,2,2,1,2,1,1,1,2,2,1,1,2,2,2,1,1,1,1] % 200.56/28.71 % TRYING [1,1,1,1,1,1,1,1,1,1,1,1,4,1,1,1,1,1,1,1,1,2,1,1,1,4,4,4,4,3,1,1,1,1,2,1,2,1,1,1,1,1,1,1,2,4,4,1,1,1,1] % 200.56/28.71 % TRYING [1,1,1,1,2,1,1,1,1,1,1,2,5,1,1,1,1,1,2,1,2,2,1,1,1,3,2,1,2,2,1,1,2,2,2,1,2,1,1,1,2,2,1,1,2,2,2,1,1,1,1] % 200.56/28.71 % TRYING [1,1,1,1,2,1,1,1,1,1,1,2,5,1,1,1,1,1,2,1,2,2,1,1,1,3,2,2,2,2,1,1,2,2,2,1,2,1,1,1,2,2,1,1,2,2,2,1,1,1,1] % 200.56/28.71 % (1607087)Instruction limit reached! % 200.56/28.71 % (1607087)------------------------------ % 200.56/28.71 % (1607087)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 200.56/28.71 % (1607087)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 200.56/28.71 % (1607087)CaDiCaL version: 2.1.3 % 200.56/28.71 % (1607087)Termination reason: Instruction limit % 200.56/28.71 % (1607087)Termination phase: Saturation % 200.56/28.71 % (1607087)Time elapsed: 3.919 s % 200.56/28.71 % (1607087)Peak memory usage: 51 MB % 200.56/28.71 % (1607087)Instructions burned: 4592 (million) % 235.06/33.53 % (1607099)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=1558184166:i=29340_2809 on theBenchmark for (2809ds/29340Mi) % 235.06/33.53 % TRYING [1,1,1,1,1,1,1,1,1,1,1,1,4,1,1,1,1,1,1,1,1,2,1,1,1,4,4,4,4,3,1,1,1,1,2,1,2,1,1,1,1,1,1,1,3,4,4,1,1,1,1] % 235.06/33.53 % TRYING [1,1,1,1,2,1,1,1,1,1,1,2,5,1,1,1,1,1,2,1,2,2,1,1,1,4,2,2,2,2,1,1,2,2,2,1,2,1,1,1,2,2,1,1,2,2,2,1,1,1,1] % 235.06/33.53 % (1607023)Instruction limit reached! % 235.06/33.53 % (1607023)------------------------------ % 235.06/33.53 % (1607023)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 235.06/33.53 % (1607023)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 235.06/33.53 % (1607023)CaDiCaL version: 2.1.3 % 235.06/33.53 % (1607023)Termination reason: Instruction limit % 235.06/33.53 % (1607023)Termination phase: Finite model building constraint generation % 235.06/33.53 % (1607023)Time elapsed: 17.874 s % 235.06/33.53 % (1607023)Peak memory usage: 111 MB % 235.06/33.53 % (1607023)Instructions burned: 22062 (million) % 235.06/33.53 % (1607101)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=2655429710:i=5211_2807 on theBenchmark for (2807ds/5211Mi) % 235.06/33.53 % TRYING [1,1,1,1,2,1,1,1,1,1,1,2,5,1,1,1,1,1,2,1,2,3,1,1,1,4,2,2,2,2,1,1,2,2,2,1,2,1,1,1,2,2,1,1,2,2,2,1,1,1,1] % 235.06/33.53 % TRYING [1,1,1,1,2,1,1,1,1,1,1,2,5,1,1,1,1,1,2,1,3,3,1,1,1,4,2,2,2,2,1,1,2,2,2,1,2,1,1,1,2,2,1,1,2,2,2,1,1,1,1] % 235.06/33.53 % TRYING [1,1,1,1,2,1,1,1,1,1,1,2,5,1,2,1,1,1,2,1,3,3,1,1,1,4,2,2,2,2,1,1,2,2,2,1,2,1,1,1,2,2,1,1,2,2,2,1,1,1,1] % 235.06/33.53 % TRYING [1,1,1,1,2,1,1,1,1,1,2,2,5,1,2,1,1,1,2,1,3,3,1,1,1,4,2,2,2,2,1,1,2,2,2,1,2,1,1,1,2,2,1,1,2,2,2,1,1,1,1] % 235.06/33.53 % TRYING [1,1,1,1,2,1,1,1,1,1,2,2,5,1,2,1,1,1,2,1,3,3,1,1,1,4,2,2,2,2,1,1,2,2,2,1,2,2,1,1,2,2,1,1,2,2,2,1,1,1,1] % 235.06/33.53 % TRYING [1,1,1,2,2,1,1,1,1,1,2,2,5,1,2,1,1,1,2,1,3,3,1,1,1,4,2,2,2,2,1,1,2,2,2,1,2,2,1,1,2,2,1,1,2,2,2,1,1,1,1] % 235.06/33.53 % TRYING [1,1,1,2,2,1,1,1,1,1,2,2,5,1,2,1,1,1,2,1,3,3,1,1,1,4,2,2,2,2,1,2,2,2,2,1,2,2,1,1,2,2,1,1,2,2,2,1,1,1,1] % 235.06/33.53 % TRYING [1,1,1,2,2,1,1,1,1,1,2,2,5,1,2,1,1,1,2,1,3,3,1,1,1,4,2,2,2,2,1,2,2,2,2,1,2,2,1,2,2,2,1,1,2,2,2,1,1,1,1] % 235.06/33.53 % TRYING [1,1,1,2,2,1,1,1,1,1,2,2,5,1,2,1,1,1,2,1,3,3,1,1,1,4,2,2,2,2,1,2,2,2,2,1,2,2,1,2,2,2,1,1,2,2,2,1,1,2,1] % 235.06/33.53 % TRYING [1,1,1,2,2,1,1,1,1,2,2,2,5,1,2,1,1,1,2,1,3,3,1,1,1,4,2,2,2,2,1,2,2,2,2,1,2,2,1,2,2,2,1,1,2,2,2,1,1,2,1] % 235.06/33.53 % TRYING [1,1,1,2,2,1,1,1,1,1,2,2,5,1,2,1,2,1,2,1,3,3,1,1,1,4,2,2,2,2,1,2,2,2,2,1,2,2,1,2,2,2,1,1,2,2,2,1,1,2,1] % 235.06/33.53 % TRYING [1,1,1,2,2,1,1,1,1,1,2,2,5,1,2,1,2,1,2,1,3,3,1,1,1,4,2,2,2,2,1,2,2,2,2,2,2,2,1,2,2,2,1,1,2,2,2,1,1,2,1] % 235.06/33.53 % (1607101)Instruction limit reached! % 235.06/33.53 % (1607101)------------------------------ % 235.06/33.53 % (1607101)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 235.06/33.53 % (1607101)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 235.06/33.53 % (1607101)CaDiCaL version: 2.1.3 % 235.06/33.53 % (1607101)Termination reason: Instruction limit % 235.06/33.53 % (1607101)Termination phase: Saturation % 235.06/33.53 % (1607101)Time elapsed: 4.053 s % 235.06/33.53 % (1607101)Peak memory usage: 42 MB % 235.06/33.53 % (1607101)Instructions burned: 5211 (million) % 235.06/33.53 % (1607111)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=566311340:i=5497:nm=2_2766 on theBenchmark for (2766ds/5497Mi) % 235.06/33.53 % TRYING [1,1,1,2,2,1,1,1,1,2,2,2,5,2,2,1,1,1,2,1,3,3,1,1,1,4,2,2,2,2,1,2,2,2,2,1,2,2,1,2,2,2,1,1,2,2,2,1,1,2,1] % 235.06/33.53 % TRYING [1,1,1,2,2,2,1,1,1,2,2,2,5,2,2,1,1,1,2,1,3,3,1,1,1,4,2,2,2,2,1,2,2,2,2,1,2,2,1,2,2,2,1,1,2,2,2,1,1,2,1] % 235.06/33.53 % TRYING [1,1,1,2,2,2,2,1,1,2,2,2,5,2,2,1,1,1,2,1,3,3,1,1,1,4,2,2,2,2,1,2,2,2,2,1,2,2,1,2,2,2,1,1,2,2,2,1,1,2,1] % 235.06/33.53 % TRYING [1,1,2,2,2,2,2,1,1,2,2,2,5,2,2,1,1,1,2,1,3,3,1,1,1,4,2,2,2,2,1,2,2,2,2,1,2,2,1,2,2,2,1,1,2,2,2,1,1,2,1] % 235.06/33.53 % Detected minimum model sizes of [1,1,1,1,1,1,1,1,1,1,1,1,4,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1] % 235.06/33.53 % Detected maximum model sizes of [max,max,max,max,2,max,max,max,max,max,max,2,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max] % 235.06/33.53 % TRYING [1,1,1,1,1,1,1,1,1,1,1,1,4,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1] % 235.06/33.53 % TRYING [1,1,2,2,2,2,2,1,1,2,2,2,5,2,2,1,1,1,2,1,3,3,1,1,1,4,2,2,2,2,1Terminated % 300.31/42.74 % Vampire exiting % 300.31/42.74 Terminated %------------------------------------------------------------------------------