%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWW869+1 : TPTP v9.3.1. Released v7.3.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % Computer : n018.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:45:06 PM UTC 2026 % Result : Timeout 291.93s 41.46s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : SWW869+1 : TPTP v9.3.1. Released v7.3.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.08/0.18 % Computer : n018.cluster.edu % 0.08/0.18 % Model : x86_64 x86_64 % 0.08/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.08/0.18 % Memory : 8046.5625MB % 0.08/0.18 % OS : Linux 6.8.0-71-generic % 0.08/0.18 % CPULimit : 300 % 0.08/0.18 % WCLimit : 300 % 0.08/0.18 % DateTime : Mon Sep 28 14:37:55 UTC 2026 % 0.08/0.18 % CPUTime : % 0.08/0.18 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.08/0.21 Running first-order model finding % 0.08/0.21 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 % 19.83/3.11 % (3439265)Will run a generic schedule for satisfiability detection. % 19.83/3.11 % (3439273)dis+10_1_sil=32000:sp=arity:random_seed=1996521586:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 19.83/3.11 % (3439271)% WARNING: option uhcvi not known. % 19.83/3.11 % (3439270)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1569850253_2999 on theBenchmark for (2999ds/0Mi) % 19.83/3.11 % (3439271)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2499225427:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 19.83/3.11 % (3439272)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3591341001:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 19.83/3.11 % (3439274)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=320094660:i=116_2999 on theBenchmark for (2999ds/116Mi) % 19.83/3.11 % (3439275)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3688968341:i=131_2999 on theBenchmark for (2999ds/131Mi) % 19.83/3.11 % (3439276)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3386829926:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 19.83/3.11 % (3439273)Instruction limit reached! % 19.83/3.11 % (3439273)------------------------------ % 19.83/3.11 % (3439273)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 19.83/3.11 % (3439273)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.83/3.11 % (3439273)CaDiCaL version: 2.1.3 % 19.83/3.11 % (3439273)Termination reason: Instruction limit % 19.83/3.11 % (3439273)Termination phase: Saturation % 19.83/3.11 % (3439273)Time elapsed: 0.031 s % 19.83/3.11 % (3439273)Peak memory usage: 12 MB % 19.83/3.11 % (3439273)Instructions burned: 105 (million) % 19.83/3.11 % (3439284)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1927043090:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 19.83/3.11 % (3439274)Instruction limit reached! % 19.83/3.11 % (3439274)------------------------------ % 19.83/3.11 % (3439274)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 19.83/3.11 % (3439274)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.83/3.11 % (3439274)CaDiCaL version: 2.1.3 % 19.83/3.11 % (3439274)Termination reason: Instruction limit % 19.83/3.11 % (3439274)Termination phase: Saturation % 19.83/3.11 % (3439274)Time elapsed: 0.059 s % 19.83/3.11 % (3439274)Peak memory usage: 13 MB % 19.83/3.11 % (3439274)Instructions burned: 120 (million) % 19.83/3.11 % (3439275)Instruction limit reached! % 19.83/3.11 % (3439275)------------------------------ % 19.83/3.11 % (3439275)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 19.83/3.11 % (3439275)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.83/3.11 % (3439275)CaDiCaL version: 2.1.3 % 19.83/3.11 % (3439275)Termination reason: Instruction limit % 19.83/3.11 % (3439275)Termination phase: Saturation % 19.83/3.11 % (3439275)Time elapsed: 0.069 s % 19.83/3.11 % (3439275)Peak memory usage: 13 MB % 19.83/3.11 % (3439275)Instructions burned: 131 (million) % 19.83/3.11 % (3439286)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=4215849520:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi) % 19.83/3.11 % (3439287)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=1904424152:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi) % 19.83/3.11 % (3439276)Instruction limit reached! % 19.83/3.11 % (3439276)------------------------------ % 19.83/3.11 % (3439276)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 19.83/3.11 % (3439276)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.83/3.11 % (3439276)CaDiCaL version: 2.1.3 % 19.83/3.11 % (3439276)Termination reason: Instruction limit % 19.83/3.11 % (3439276)Termination phase: Saturation % 19.83/3.11 % (3439276)Time elapsed: 0.091 s % 19.83/3.11 % (3439276)Peak memory usage: 14 MB % 19.83/3.11 % (3439276)Instructions burned: 160 (million) % 19.83/3.11 % (3439290)ott-21_1_sil=16000:fs=off:random_seed=3381515359:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 19.83/3.11 % (3439286)Instruction limit reached! % 19.83/3.11 % (3439286)------------------------------ % 19.83/3.11 % (3439286)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 19.83/3.11 % (3439286)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.83/3.11 % (3439286)CaDiCaL version: 2.1.3 % 38.85/5.81 % (3439286)Termination reason: Instruction limit % 38.85/5.81 % (3439286)Termination phase: Saturation % 38.85/5.81 % (3439286)Time elapsed: 0.062 s % 38.85/5.81 % (3439286)Peak memory usage: 13 MB % 38.85/5.81 % (3439286)Instructions burned: 133 (million) % 38.85/5.81 % (3439292)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1977611723:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 38.85/5.81 % (3439290)Instruction limit reached! % 38.85/5.81 % (3439290)------------------------------ % 38.85/5.81 % (3439290)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 38.85/5.81 % (3439290)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 38.85/5.81 % (3439290)CaDiCaL version: 2.1.3 % 38.85/5.81 % (3439290)Termination reason: Instruction limit % 38.85/5.81 % (3439290)Termination phase: Saturation % 38.85/5.81 % (3439290)Time elapsed: 0.087 s % 38.85/5.81 % (3439290)Peak memory usage: 13 MB % 38.85/5.81 % (3439290)Instructions burned: 181 (million) % 38.85/5.81 % (3439294)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=389469129:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi) % 38.85/5.81 % (3439284)Instruction limit reached! % 38.85/5.81 % (3439284)------------------------------ % 38.85/5.81 % (3439284)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 38.85/5.81 % (3439284)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 38.85/5.81 % (3439284)CaDiCaL version: 2.1.3 % 38.85/5.81 % (3439284)Termination reason: Instruction limit % 38.85/5.81 % (3439284)Termination phase: Finite model building preprocessing % 38.85/5.81 % (3439284)Time elapsed: 0.204 s % 38.85/5.81 % (3439284)Peak memory usage: 16 MB % 38.85/5.81 % (3439284)Instructions burned: 714 (million) % 38.85/5.81 % (3439296)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1819723361:i=1179_2997 on theBenchmark for (2997ds/1179Mi) % 38.85/5.81 % (3439287)Instruction limit reached! % 38.85/5.81 % (3439287)------------------------------ % 38.85/5.81 % (3439287)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 38.85/5.81 % (3439287)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 38.85/5.81 % (3439287)CaDiCaL version: 2.1.3 % 38.85/5.81 % (3439287)Termination reason: Instruction limit % 38.85/5.81 % (3439287)Termination phase: Saturation % 38.85/5.81 % (3439287)Time elapsed: 0.348 s % 38.85/5.81 % (3439287)Peak memory usage: 17 MB % 38.85/5.81 % (3439287)Instructions burned: 684 (million) % 38.85/5.81 % (3439292)Instruction limit reached! % 38.85/5.81 % (3439292)------------------------------ % 38.85/5.81 % (3439292)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 38.85/5.81 % (3439292)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 38.85/5.81 % (3439292)CaDiCaL version: 2.1.3 % 38.85/5.81 % (3439292)Termination reason: Instruction limit % 38.85/5.81 % (3439292)Termination phase: Saturation % 38.85/5.81 % (3439292)Time elapsed: 0.279 s % 38.85/5.81 % (3439292)Peak memory usage: 14 MB % 38.85/5.81 % (3439292)Instructions burned: 477 (million) % 38.85/5.81 % (3439298)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3938844156:i=889:ins=1_2995 on theBenchmark for (2995ds/889Mi) % 38.85/5.81 % (3439299)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=1077186549:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2995 on theBenchmark for (2995ds/692Mi) % 38.85/5.81 % (3439296)Instruction limit reached! % 38.85/5.81 % (3439296)------------------------------ % 38.85/5.81 % (3439296)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 38.85/5.81 % (3439296)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 38.85/5.81 % (3439296)CaDiCaL version: 2.1.3 % 38.85/5.81 % (3439296)Termination reason: Instruction limit % 38.85/5.81 % (3439296)Termination phase: Saturation % 38.85/5.81 % (3439296)Time elapsed: 0.328 s % 38.85/5.81 % (3439296)Peak memory usage: 24 MB % 38.85/5.81 % (3439296)Instructions burned: 1182 (million) % 38.85/5.81 % (3439302)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=963728114:i=879:kws=inv_precedence:fsr=off_2993 on theBenchmark for (2993ds/879Mi) % 38.85/5.81 % (3439294)Instruction limit reached! % 38.85/5.81 % (3439294)------------------------------ % 38.85/5.81 % (3439294)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 38.85/5.81 % (3439294)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 101.13/14.59 % (3439294)CaDiCaL version: 2.1.3 % 101.13/14.59 % (3439294)Termination reason: Instruction limit % 101.13/14.59 % (3439294)Termination phase: Finite model building preprocessing % 101.13/14.59 % (3439294)Time elapsed: 0.491 s % 101.13/14.59 % (3439294)Peak memory usage: 15 MB % 101.13/14.59 % (3439294)Instructions burned: 865 (million) % 101.13/14.59 % (3439304)fmb+10_1_sil=64000:random_seed=3484399273:i=22061:nm=2:gsp=on_2992 on theBenchmark for (2992ds/22061Mi) % 101.13/14.59 % (3439299)Instruction limit reached! % 101.13/14.59 % (3439299)------------------------------ % 101.13/14.59 % (3439299)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 101.13/14.59 % (3439299)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 101.13/14.59 % (3439299)CaDiCaL version: 2.1.3 % 101.13/14.59 % (3439299)Termination reason: Instruction limit % 101.13/14.59 % (3439299)Termination phase: Saturation % 101.13/14.59 % (3439299)Time elapsed: 0.358 s % 101.13/14.59 % (3439299)Peak memory usage: 16 MB % 101.13/14.59 % (3439299)Instructions burned: 694 (million) % 101.13/14.59 % (3439306)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=4075116812:i=9515:nm=5_2991 on theBenchmark for (2991ds/9515Mi) % 101.13/14.59 % (3439302)Instruction limit reached! % 101.13/14.59 % (3439302)------------------------------ % 101.13/14.59 % (3439302)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 101.13/14.59 % (3439302)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 101.13/14.59 % (3439302)CaDiCaL version: 2.1.3 % 101.13/14.59 % (3439302)Termination reason: Instruction limit % 101.13/14.59 % (3439302)Termination phase: Saturation % 101.13/14.59 % (3439302)Time elapsed: 0.258 s % 101.13/14.59 % (3439302)Peak memory usage: 20 MB % 101.13/14.59 % (3439302)Instructions burned: 879 (million) % 101.13/14.59 % (3439308)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3846133778:fmbsr=1.7:i=920_2990 on theBenchmark for (2990ds/920Mi) % 101.13/14.59 % (3439298)Instruction limit reached! % 101.13/14.59 % (3439298)------------------------------ % 101.13/14.59 % (3439298)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 101.13/14.59 % (3439298)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 101.13/14.59 % (3439298)CaDiCaL version: 2.1.3 % 101.13/14.59 % (3439298)Termination reason: Instruction limit % 101.13/14.59 % (3439298)Termination phase: Finite model building preprocessing % 101.13/14.59 % (3439298)Time elapsed: 0.501 s % 101.13/14.59 % (3439298)Peak memory usage: 15 MB % 101.13/14.59 % (3439298)Instructions burned: 890 (million) % 101.13/14.59 % (3439310)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2426903462:i=5131_2989 on theBenchmark for (2989ds/5131Mi) % 101.13/14.59 % (3439308)Instruction limit reached! % 101.13/14.59 % (3439308)------------------------------ % 101.13/14.59 % (3439308)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 101.13/14.59 % (3439308)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 101.13/14.59 % (3439308)CaDiCaL version: 2.1.3 % 101.13/14.59 % (3439308)Termination reason: Instruction limit % 101.13/14.59 % (3439308)Termination phase: Finite model building preprocessing % 101.13/14.59 % (3439308)Time elapsed: 0.278 s % 101.13/14.59 % (3439308)Peak memory usage: 15 MB % 101.13/14.59 % (3439308)Instructions burned: 922 (million) % 101.13/14.59 % TRYING [1] % 101.13/14.59 % (3439312)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1450180808:i=1472:ins=7:fdi=8:gsp=on_2988 on theBenchmark for (2988ds/1472Mi) % 101.13/14.59 % TRYING [2] % 101.13/14.59 % (3439312)Instruction limit reached! % 101.13/14.59 % (3439312)------------------------------ % 101.13/14.59 % (3439312)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 101.13/14.59 % (3439312)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 101.13/14.59 % (3439312)CaDiCaL version: 2.1.3 % 101.13/14.59 % (3439312)Termination reason: Instruction limit % 101.13/14.59 % (3439312)Termination phase: Saturation % 101.13/14.59 % (3439312)Time elapsed: 0.385 s % 101.13/14.59 % (3439312)Peak memory usage: 43 MB % 101.13/14.59 % (3439312)Instructions burned: 1472 (million) % 101.13/14.59 % (3439314)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=559590166:i=6324_2984 on theBenchmark for (2984ds/6324Mi) % 101.13/14.59 % TRYING [3] % 101.13/14.59 % TRYING [1] % 101.13/14.59 % TRYING [2] % 101.13/14.59 % TRYING [3] % 101.13/14.59 % (3439314)Cannot represent all propositional literals internally % 101.13/14.59 % (3439314)Refutation not found, incomplete strategy % 101.13/14.59 % (3439314)------------------------------ % 101.13/14.59 % (3439314)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 101.13/14.59 % (3439314)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 177.73/25.34 % (3439314)CaDiCaL version: 2.1.3 % 177.73/25.34 % (3439314)Termination reason: Refutation not found, incomplete strategy % 177.73/25.34 % (3439314)Time elapsed: 1.290 s % 177.73/25.34 % (3439314)Peak memory usage: 29 MB % 177.73/25.34 % (3439314)Instructions burned: 4324 (million) % 177.73/25.34 % (3439314)------------------------------ % 177.73/25.34 % (3439314)------------------------------ % 177.73/25.34 % (3439316)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=2705447519:fmbsr=2.30978:i=2174_2971 on theBenchmark for (2971ds/2174Mi) % 177.73/25.34 % (3439306)Cannot represent all propositional literals internally % 177.73/25.34 % (3439306)Refutation not found, incomplete strategy % 177.73/25.34 % (3439306)------------------------------ % 177.73/25.34 % (3439306)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 177.73/25.34 % (3439306)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 177.73/25.34 % (3439306)CaDiCaL version: 2.1.3 % 177.73/25.34 % (3439306)Termination reason: Refutation not found, incomplete strategy % 177.73/25.34 % (3439306)Time elapsed: 2.411 s % 177.73/25.34 % (3439306)Peak memory usage: 29 MB % 177.73/25.34 % (3439306)Instructions burned: 4306 (million) % 177.73/25.34 % (3439306)------------------------------ % 177.73/25.34 % (3439306)------------------------------ % 177.73/25.34 % (3439318)ott-2_1_sil=16000:newcnf=on:random_seed=2858115079:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2966 on theBenchmark for (2966ds/869Mi) % 177.73/25.34 % (3439316)Instruction limit reached! % 177.73/25.34 % (3439316)------------------------------ % 177.73/25.34 % (3439316)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 177.73/25.34 % (3439316)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 177.73/25.34 % (3439316)CaDiCaL version: 2.1.3 % 177.73/25.34 % (3439316)Termination reason: Instruction limit % 177.73/25.34 % (3439316)Termination phase: Finite model building preprocessing % 177.73/25.34 % (3439316)Time elapsed: 0.649 s % 177.73/25.34 % (3439316)Peak memory usage: 20 MB % 177.73/25.34 % (3439316)Instructions burned: 2176 (million) % 177.73/25.34 % (3439320)ott+10_1_sil=32000:tgt=ground:random_seed=892413000:i=5114:av=off_2964 on theBenchmark for (2964ds/5114Mi) % 177.73/25.34 % TRYING [4] % 177.73/25.34 % (3439310)Instruction limit reached! % 177.73/25.34 % (3439310)------------------------------ % 177.73/25.34 % (3439310)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 177.73/25.34 % (3439310)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 177.73/25.34 % (3439310)CaDiCaL version: 2.1.3 % 177.73/25.34 % (3439310)Termination reason: Instruction limit % 177.73/25.34 % (3439310)Termination phase: Saturation % 177.73/25.34 % (3439310)Time elapsed: 2.668 s % 177.73/25.34 % (3439310)Peak memory usage: 42 MB % 177.73/25.34 % (3439310)Instructions burned: 5132 (million) % 177.73/25.34 % (3439318)Instruction limit reached! % 177.73/25.34 % (3439318)------------------------------ % 177.73/25.34 % (3439318)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 177.73/25.34 % (3439318)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 177.73/25.34 % (3439318)CaDiCaL version: 2.1.3 % 177.73/25.34 % (3439318)Termination reason: Instruction limit % 177.73/25.34 % (3439318)Termination phase: Saturation % 177.73/25.34 % (3439318)Time elapsed: 0.394 s % 177.73/25.34 % (3439318)Peak memory usage: 16 MB % 177.73/25.34 % (3439318)Instructions burned: 869 (million) % 177.73/25.34 % (3439322)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2399976560:i=54282_2962 on theBenchmark for (2962ds/54282Mi) % 177.73/25.34 % (3439324)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=2572019314:i=3512:aac=none_2962 on theBenchmark for (2962ds/3512Mi) % 177.73/25.34 % TRYING [4] % 177.73/25.34 % (3439320)Instruction limit reached! % 177.73/25.34 % (3439320)------------------------------ % 177.73/25.34 % (3439320)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 177.73/25.34 % (3439320)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 177.73/25.34 % (3439320)CaDiCaL version: 2.1.3 % 177.73/25.34 % (3439320)Termination reason: Instruction limit % 177.73/25.34 % (3439320)Termination phase: Saturation % 177.73/25.34 % (3439320)Time elapsed: 1.402 s % 177.73/25.34 % (3439320)Peak memory usage: 49 MB % 177.73/25.34 % (3439320)Instructions burned: 5119 (million) % 177.73/25.34 % (3439326)dis+21_1_sil=32000:sas=cadical:random_seed=703141792:i=3773:amm=off_2950 on theBenchmark for (2950ds/3773Mi) % 177.73/25.34 % (3439324)Instruction limit reached! % 177.73/25.34 % (3439324)------------------------------ % 177.73/25.34 % (3439324)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 249.39/35.41 % (3439324)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 249.39/35.41 % (3439324)CaDiCaL version: 2.1.3 % 249.39/35.41 % (3439324)Termination reason: Instruction limit % 249.39/35.41 % (3439324)Termination phase: Saturation % 249.39/35.41 % (3439324)Time elapsed: 1.847 s % 249.39/35.41 % (3439324)Peak memory usage: 37 MB % 249.39/35.41 % (3439324)Instructions burned: 3512 (million) % 249.39/35.41 % (3439328)ott+11_1_sil=16000:gs=on:random_seed=2510205872:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2944 on theBenchmark for (2944ds/2251Mi) % 249.39/35.41 % (3439326)Instruction limit reached! % 249.39/35.41 % (3439326)------------------------------ % 249.39/35.41 % (3439326)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 249.39/35.41 % (3439326)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 249.39/35.41 % (3439326)CaDiCaL version: 2.1.3 % 249.39/35.41 % (3439326)Termination reason: Instruction limit % 249.39/35.41 % (3439326)Termination phase: Saturation % 249.39/35.41 % (3439326)Time elapsed: 1.001 s % 249.39/35.41 % (3439326)Peak memory usage: 36 MB % 249.39/35.41 % (3439326)Instructions burned: 3773 (million) % 249.39/35.41 % (3439330)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=2214139105:fmbsr=1.6:i=67534_2939 on theBenchmark for (2939ds/67534Mi) % 249.39/35.41 % TRYING [1] % 249.39/35.41 % TRYING [2] % 249.39/35.41 % TRYING [3] % 249.39/35.41 % (3439328)Instruction limit reached! % 249.39/35.41 % (3439328)------------------------------ % 249.39/35.41 % (3439328)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 249.39/35.41 % (3439328)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 249.39/35.41 % (3439328)CaDiCaL version: 2.1.3 % 249.39/35.41 % (3439328)Termination reason: Instruction limit % 249.39/35.41 % (3439328)Termination phase: Saturation % 249.39/35.41 % (3439328)Time elapsed: 1.100 s % 249.39/35.41 % (3439328)Peak memory usage: 19 MB % 249.39/35.41 % (3439328)Instructions burned: 2251 (million) % 249.39/35.41 % (3439332)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=1443543570:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2932 on theBenchmark for (2932ds/4591Mi) % 249.39/35.41 % TRYING [4] % 249.39/35.41 % (3439332)Instruction limit reached! % 249.39/35.41 % (3439332)------------------------------ % 249.39/35.41 % (3439332)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 249.39/35.41 % (3439332)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 249.39/35.41 % (3439332)CaDiCaL version: 2.1.3 % 249.39/35.41 % (3439332)Termination reason: Instruction limit % 249.39/35.41 % (3439332)Termination phase: Saturation % 249.39/35.41 % (3439332)Time elapsed: 2.117 s % 249.39/35.41 % (3439332)Peak memory usage: 63 MB % 249.39/35.41 % (3439332)Instructions burned: 4592 (million) % 249.39/35.41 % (3439334)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=1777554787:i=29340_2911 on theBenchmark for (2911ds/29340Mi) % 249.39/35.41 % TRYING [5] % 249.39/35.41 % (3439304)Instruction limit reached! % 249.39/35.41 % (3439304)------------------------------ % 249.39/35.41 % (3439304)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 249.39/35.41 % (3439304)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 249.39/35.41 % (3439304)CaDiCaL version: 2.1.3 % 249.39/35.41 % (3439304)Termination reason: Instruction limit % 249.39/35.41 % (3439304)Termination phase: Finite model building SAT solving % 249.39/35.41 % (3439304)Time elapsed: 9.497 s % 249.39/35.41 % (3439304)Peak memory usage: 559 MB % 249.39/35.41 % (3439304)Instructions burned: 22062 (million) % 249.39/35.41 % (3439336)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=1495313882:i=5211_2896 on theBenchmark for (2896ds/5211Mi) % 249.39/35.41 % TRYING [7] % 249.39/35.41 % (3439336)Instruction limit reached! % 249.39/35.41 % (3439336)------------------------------ % 249.39/35.41 % (3439336)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 249.39/35.41 % (3439336)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 249.39/35.41 % (3439336)CaDiCaL version: 2.1.3 % 249.39/35.41 % (3439336)Termination reason: Instruction limit % 249.39/35.41 % (3439336)Termination phase: Saturation % 249.39/35.41 % (3439336)Time elapsed: 2.710 s % 249.39/35.41 % (3439336)Peak memory usage: 52 MB % 249.39/35.41 % (3439336)Instructions burned: 5212 (million) % 249.39/35.41 % (3439338)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=3232014695:i=5497:nm=2_2869 on theBenchmark for (2869ds/5497Mi) % 249.39/35.41 % TRYING [5] % 249.39/35.41 % (3439338)Cannot represent all propositional literals internally % 291.93/41.46 % (3439338)Refutation not found, incomplete strategy % 291.93/41.46 % (3439338)------------------------------ % 291.93/41.46 % (3439338)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 291.93/41.46 % (3439338)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 291.93/41.46 % (3439338)CaDiCaL version: 2.1.3 % 291.93/41.46 % (3439338)Termination reason: Refutation not found, incomplete strategy % 291.93/41.46 % (3439338)Time elapsed: 1.263 s % 291.93/41.46 % (3439338)Peak memory usage: 23 MB % 291.93/41.46 % (3439338)Instructions burned: 2280 (million) % 291.93/41.46 % (3439338)------------------------------ % 291.93/41.46 % (3439338)------------------------------ % 291.93/41.46 % (3439340)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=2264769990:fmbsr=2:i=46332_2856 on theBenchmark for (2856ds/46332Mi) % 291.93/41.46 % (3439340)Cannot represent all propositional literals internally % 291.93/41.46 % (3439340)Refutation not found, incomplete strategy % 291.93/41.46 % (3439340)------------------------------ % 291.93/41.46 % (3439340)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 291.93/41.46 % (3439340)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 291.93/41.46 % (3439340)CaDiCaL version: 2.1.3 % 291.93/41.46 % (3439340)Termination reason: Refutation not found, incomplete strategy % 291.93/41.46 % (3439340)Time elapsed: 2.427 s % 291.93/41.46 % (3439340)Peak memory usage: 27 MB % 291.93/41.46 % (3439340)Instructions burned: 4295 (million) % 291.93/41.46 % (3439340)------------------------------ % 291.93/41.46 % (3439340)------------------------------ % 291.93/41.46 % (3439342)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=2195908395:i=14071_2831 on theBenchmark for (2831ds/14071Mi) % 291.93/41.46 % TRYING [12] % 291.93/41.46 % (3439330)Instruction limit reached! % 291.93/41.46 % (3439330)------------------------------ % 291.93/41.46 % (3439330)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 291.93/41.46 % (3439330)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 291.93/41.46 % (3439330)CaDiCaL version: 2.1.3 % 291.93/41.46 % (3439330)Termination reason: Instruction limit % 291.93/41.46 % (3439330)Termination phase: Finite model building constraint generation % 291.93/41.46 % (3439330)Time elapsed: 13.608 s % 291.93/41.46 % (3439330)Peak memory usage: 3796 MB % 291.93/41.46 % (3439330)Instructions burned: 67536 (million) % 291.93/41.46 % (3439344)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2965428850:i=22565:add=on:rawr=on_2800 on theBenchmark for (2800ds/22565Mi) % 291.93/41.46 % (3439342)Instruction limit reached! % 291.93/41.46 % (3439342)------------------------------ % 291.93/41.46 % (3439342)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 291.93/41.46 % (3439342)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 291.93/41.46 % (3439342)CaDiCaL version: 2.1.3 % 291.93/41.46 % (3439342)Termination reason: Instruction limit % 291.93/41.46 % (3439342)Termination phase: Finite model building constraint generation % 291.93/41.46 % (3439342)Time elapsed: 5.897 s % 291.93/41.46 % (3439342)Peak memory usage: 667 MB % 291.93/41.46 % (3439342)Instructions burned: 14072 (million) % 291.93/41.46 % (3439346)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=703508352:i=8173:av=off_2771 on theBenchmark for (2771ds/8173Mi) % 291.93/41.46 % (3439334)Instruction limit reached! % 291.93/41.46 % (3439334)------------------------------ % 291.93/41.46 % (3439334)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 291.93/41.46 % (3439334)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 291.93/41.46 % (3439334)CaDiCaL version: 2.1.3 % 291.93/41.46 % (3439334)Termination reason: Instruction limit % 291.93/41.46 % (3439334)Termination phase: Saturation % 291.93/41.46 % (3439334)Time elapsed: 14.393 s % 291.93/41.46 % (3439334)Peak memory usage: 120 MB % 291.93/41.46 % (3439334)Instructions burned: 29340 (million) % 291.93/41.46 % (3439348)dis+10_16:1_sil=16000:random_seed=1665917611:i=9155:fsr=off_2767 on theBenchmark for (2767ds/9155Mi) % 291.93/41.46 % (3439344)Instruction limit reached! % 291.93/41.46 % (3439344)------------------------------ % 291.93/41.46 % (3439344)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 291.93/41.46 % (3439344)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 291.93/41.46 % (3439344)CaDiCaL version: 2.1.3 % 291.93/41.46 % (3439344)Termination reason: Instruction limit % 291.93/41.46 % (3439344)Termination phase: Saturation % 291.93/41.46 % (3439344)Time elapsed: 5.170 s % 291.93/41.46 % (3439344)Peak memory usage: 99 MB % 300.47/42.63 % (3439344)Instructions burned: 22565 (million) % 300.47/42.63 % (3439350)ott-3_8_sil=64000:random_seed=2551342821:i=20139:bs=on_2748 on theBenchmark for (2748ds/20139Mi) % 300.47/42.63 % (3439322)Instruction limit reached! % 300.47/42.63 % (3439322)------------------------------ % 300.47/42.63 % (3439322)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.47/42.63 % (3439322)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.47/42.63 % (3439322)CaDiCaL version: 2.1.3 % 300.47/42.63 % (3439322)Termination reason: Instruction limit % 300.47/42.63 % (3439322)Termination phase: Finite model building constraint generation % 300.47/42.63 % (3439322)Time elapsed: 22.516 s % 300.47/42.63 % (3439322)Peak memory usage: 2247 MB % 300.47/42.63 % (3439322)Instructions burned: 54283 (million) % 300.47/42.63 % (3439352)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=2519901128:fmbsr=2:i=32576_2734 on theBenchmark for (2734ds/32576Mi) % 300.47/42.63 % (3439346)Instruction limit reached! % 300.47/42.63 % (3439346)------------------------------ % 300.47/42.63 % (3439346)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.47/42.63 % (3439346)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.47/42.63 % (3439346)CaDiCaL version: 2.1.3 % 300.47/42.63 % (3439346)Termination reason: Instruction limit % 300.47/42.63 % (3439346)Termination phase: Saturation % 300.47/42.63 % (3439346)Time elapsed: 4.326 s % 300.47/42.63 % (3439346)Peak memory usage: 62 MB % 300.47/42.63 % (3439346)Instructions burned: 8174 (million) % 300.47/42.63 % (3439354)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=3372111637:i=11404_2728 on theBenchmark for (2728ds/11404Mi) % 300.47/42.63 % (3439348)Instruction limit reached! % 300.47/42.63 % (3439348)------------------------------ % 300.47/42.63 % (3439348)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.47/42.63 % (3439348)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.47/42.63 % (3439348)CaDiCaL version: 2.1.3 % 300.47/42.63 % (3439348)Termination reason: Instruction limit % 300.47/42.63 % (3439348)Termination phase: Saturation % 300.47/42.63 % (3439348)Time elapsed: 4.602 s % 300.47/42.63 % (3439348)Peak memory usage: 85 MB % 300.47/42.63 % (3439348)Instructions burned: 9156 (million) % 300.47/42.63 % (3439356)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=442322800:i=14134_2720 on theBenchmark for (2720ds/14134Mi) % 300.47/42.64 % TRYING [9] % 300.47/42.64 % (3439350)Instruction limit reached! % 300.47/42.64 % (3439350)------------------------------ % 300.47/42.64 % (3439350)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.47/42.64 % (3439350)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.47/42.64 % (3439350)CaDiCaL version: 2.1.3 % 300.47/42.64 % (3439350)Termination reason: Instruction limit % 300.47/42.64 % (3439350)Termination phase: Saturation % 300.47/42.64 % (3439350)Time elapsed: 6.401 s % 300.47/42.64 % (3439350)Peak memory usage: 134 MB % 300.47/42.64 % (3439350)Instructions burned: 20140 (million) % 300.47/42.64 % (3439358)dis+33_16_sil=32000:sac=on:random_seed=1340218955:i=15851:nm=0_2684 on theBenchmark for (2684ds/15851Mi) % 300.47/42.64 % (3439354)Instruction limit reached! % 300.47/42.64 % (3439354)------------------------------ % 300.47/42.64 % (3439354)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.47/42.64 % (3439354)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.47/42.64 % (3439354)CaDiCaL version: 2.1.3 % 300.47/42.64 % (3439354)Termination reason: Instruction limit % 300.47/42.64 % (3439354)Termination phase: Saturation % 300.47/42.64 % (3439354)Time elapsed: 6.461 s % 300.47/42.64 % (3439354)Peak memory usage: 134 MB % 300.47/42.64 % (3439354)Instructions burned: 11404 (million) % 300.47/42.64 % (3439361)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=163519836:avsq=on:i=17627:add=on:amm=off_2663 on theBenchmark for (2663ds/17627Mi) % 300.47/42.64 % (3439358)Instruction limit reached! % 300.47/42.64 % (3439358)------------------------------ % 300.47/42.64 % (3439358)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.47/42.64 % (3439358)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.47/42.64 % (3439358)CaDiCaL version: 2.1.3 % 300.47/42.64 % (3439358)Termination reason: Instruction limit % 300.47/42.64 % (3439358)Termination phase: Saturation % 300.47/42.64 % (3439358)Time elapsed: 3.618 s % 300.47/42.64 % (3439358)Peak memory usage: 39 MB % 300.47/42.64 % (3439358)Instructions burned: 15854 (million) % 300.47/42.64 % (3439363)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=26 % 300.47/42.64 Terminated % 300.47/42.64 % Vampire exiting %------------------------------------------------------------------------------