%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWW334+1 : TPTP v9.3.1. Released v5.2.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % Computer : n008.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:39:50 PM UTC 2026 % Result : Timeout 290.31s 41.44s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : SWW334+1 : TPTP v9.3.1. Released v5.2.0. % 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.07/0.23 % Computer : n008.cluster.edu % 0.07/0.23 % Model : x86_64 x86_64 % 0.07/0.23 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.07/0.23 % Memory : 8046.5625MB % 0.07/0.23 % OS : Linux 6.8.0-71-generic % 0.07/0.23 % CPULimit : 300 % 0.07/0.23 % WCLimit : 300 % 0.07/0.23 % DateTime : Mon Sep 28 13:38:53 UTC 2026 % 0.07/0.23 % CPUTime : % 0.07/0.23 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.16/0.27 Running first-order model finding % 0.16/0.27 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 29.56/4.68 % (2254450)Will run a generic schedule for satisfiability detection. % 29.56/4.68 % (2254476)% WARNING: option uhcvi not known. % 29.56/4.68 % (2254475)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1618720812_2998 on theBenchmark for (2998ds/0Mi) % 29.56/4.68 % (2254478)dis+10_1_sil=32000:sp=arity:random_seed=2639581252:i=103:fgj=on_2998 on theBenchmark for (2998ds/103Mi) % 29.56/4.68 % (2254476)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3043977119:i=135531:add=off:rawr=on_2998 on theBenchmark for (2998ds/135531Mi) % 29.56/4.68 % (2254481)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2878408114:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2998 on theBenchmark for (2998ds/159Mi) % 29.56/4.68 % (2254477)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1049709794:i=88024:add=on:rawr=on_2998 on theBenchmark for (2998ds/88024Mi) % 29.56/4.68 % (2254479)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=92478193:i=116_2998 on theBenchmark for (2998ds/116Mi) % 29.56/4.68 % (2254480)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=986301534:i=131_2998 on theBenchmark for (2998ds/131Mi) % 29.56/4.68 % (2254480)Instruction limit reached! % 29.56/4.68 % (2254480)------------------------------ % 29.56/4.68 % (2254480)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 29.56/4.68 % (2254480)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.56/4.68 % (2254480)CaDiCaL version: 2.1.3 % 29.56/4.68 % (2254480)Termination reason: Instruction limit % 29.56/4.68 % (2254480)Termination phase: Preprocessing 3 % 29.56/4.68 % (2254480)Time elapsed: 0.057 s % 29.56/4.68 % (2254480)Peak memory usage: 20 MB % 29.56/4.68 % (2254480)Instructions burned: 135 (million) % 29.56/4.68 % (2254478)Instruction limit reached! % 29.56/4.68 % (2254478)------------------------------ % 29.56/4.68 % (2254478)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 29.56/4.68 % (2254478)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.56/4.68 % (2254478)CaDiCaL version: 2.1.3 % 29.56/4.68 % (2254478)Termination reason: Instruction limit % 29.56/4.68 % (2254478)Termination phase: Preprocessing 3 % 29.56/4.68 % (2254478)Time elapsed: 0.063 s % 29.56/4.68 % (2254478)Peak memory usage: 20 MB % 29.56/4.68 % (2254478)Instructions burned: 104 (million) % 29.56/4.68 % (2254489)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2147392722:i=714:nm=2_2997 on theBenchmark for (2997ds/714Mi) % 29.56/4.68 % (2254479)Instruction limit reached! % 29.56/4.68 % (2254479)------------------------------ % 29.56/4.68 % (2254479)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 29.56/4.68 % (2254479)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.56/4.68 % (2254479)CaDiCaL version: 2.1.3 % 29.56/4.68 % (2254479)Termination reason: Instruction limit % 29.56/4.68 % (2254479)Termination phase: NewCNF % 29.56/4.68 % (2254479)Time elapsed: 0.075 s % 29.56/4.68 % (2254479)Peak memory usage: 21 MB % 29.56/4.68 % (2254479)Instructions burned: 118 (million) % 29.56/4.68 % (2254490)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1047032812:i=131:bd=preordered:fsd=on_2997 on theBenchmark for (2997ds/131Mi) % 29.56/4.68 % (2254492)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=1568698957:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2997 on theBenchmark for (2997ds/684Mi) % 29.56/4.68 % (2254481)Instruction limit reached! % 29.56/4.68 % (2254481)------------------------------ % 29.56/4.68 % (2254481)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 29.56/4.68 % (2254481)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.56/4.68 % (2254481)CaDiCaL version: 2.1.3 % 29.56/4.68 % (2254481)Termination reason: Instruction limit % 29.56/4.68 % (2254481)Termination phase: Property scanning % 29.56/4.68 % (2254481)Time elapsed: 0.123 s % 29.56/4.68 % (2254481)Peak memory usage: 21 MB % 29.56/4.68 % (2254481)Instructions burned: 159 (million) % 29.56/4.68 % (2254495)ott-21_1_sil=16000:fs=off:random_seed=912266973:i=180:av=off:fsr=off_2996 on theBenchmark for (2996ds/180Mi) % 29.56/4.68 % (2254490)Instruction limit reached! % 29.56/4.68 % (2254490)------------------------------ % 29.56/4.68 % (2254490)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 29.56/4.68 % (2254490)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 56.51/8.46 % (2254490)CaDiCaL version: 2.1.3 % 56.51/8.46 % (2254490)Termination reason: Instruction limit % 56.51/8.46 % (2254490)Termination phase: Preprocessing 3 % 56.51/8.46 % (2254490)Time elapsed: 0.077 s % 56.51/8.46 % (2254490)Peak memory usage: 20 MB % 56.51/8.46 % (2254490)Instructions burned: 131 (million) % 56.51/8.46 % (2254497)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2920754038:i=477:bd=all_2996 on theBenchmark for (2996ds/477Mi) % 56.51/8.46 % (2254489)Instruction limit reached! % 56.51/8.46 % (2254489)------------------------------ % 56.51/8.46 % (2254489)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 56.51/8.46 % (2254489)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 56.51/8.46 % (2254489)CaDiCaL version: 2.1.3 % 56.51/8.46 % (2254489)Termination reason: Instruction limit % 56.51/8.46 % (2254489)Termination phase: Finite model building preprocessing % 56.51/8.46 % (2254489)Time elapsed: 0.176 s % 56.51/8.46 % (2254489)Peak memory usage: 25 MB % 56.51/8.46 % (2254489)Instructions burned: 716 (million) % 56.51/8.46 % (2254499)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3170704420:fmbsr=1.3:i=865:ins=25_2995 on theBenchmark for (2995ds/865Mi) % 56.51/8.46 % (2254495)Instruction limit reached! % 56.51/8.46 % (2254495)------------------------------ % 56.51/8.46 % (2254495)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 56.51/8.46 % (2254495)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 56.51/8.46 % (2254495)CaDiCaL version: 2.1.3 % 56.51/8.46 % (2254495)Termination reason: Instruction limit % 56.51/8.46 % (2254495)Termination phase: Property scanning % 56.51/8.46 % (2254495)Time elapsed: 0.160 s % 56.51/8.46 % (2254495)Peak memory usage: 22 MB % 56.51/8.46 % (2254495)Instructions burned: 181 (million) % 56.51/8.46 % (2254501)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=304234965:i=1179_2994 on theBenchmark for (2994ds/1179Mi) % 56.51/8.46 % (2254497)Instruction limit reached! % 56.51/8.46 % (2254497)------------------------------ % 56.51/8.46 % (2254497)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 56.51/8.46 % (2254497)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 56.51/8.46 % (2254497)CaDiCaL version: 2.1.3 % 56.51/8.46 % (2254497)Termination reason: Instruction limit % 56.51/8.46 % (2254497)Termination phase: Property scanning % 56.51/8.46 % (2254497)Time elapsed: 0.223 s % 56.51/8.46 % (2254497)Peak memory usage: 22 MB % 56.51/8.46 % (2254497)Instructions burned: 479 (million) % 56.51/8.46 % (2254492)Instruction limit reached! % 56.51/8.46 % (2254492)------------------------------ % 56.51/8.46 % (2254492)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 56.51/8.46 % (2254492)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 56.51/8.46 % (2254492)CaDiCaL version: 2.1.3 % 56.51/8.46 % (2254492)Termination reason: Instruction limit % 56.51/8.46 % (2254492)Termination phase: Saturation % 56.51/8.46 % (2254492)Time elapsed: 0.325 s % 56.51/8.46 % (2254492)Peak memory usage: 24 MB % 56.51/8.46 % (2254492)Instructions burned: 684 (million) % 56.51/8.46 % (2254504)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1549376455:i=889:ins=1_2993 on theBenchmark for (2993ds/889Mi) % 56.51/8.46 % (2254505)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=222146863:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2993 on theBenchmark for (2993ds/692Mi) % 56.51/8.46 % (2254499)Instruction limit reached! % 56.51/8.46 % (2254499)------------------------------ % 56.51/8.46 % (2254499)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 56.51/8.46 % (2254499)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 56.51/8.46 % (2254499)CaDiCaL version: 2.1.3 % 56.51/8.46 % (2254499)Termination reason: Instruction limit % 56.51/8.46 % (2254499)Termination phase: Finite model building preprocessing % 56.51/8.46 % (2254499)Time elapsed: 0.219 s % 56.51/8.46 % (2254499)Peak memory usage: 30 MB % 56.51/8.46 % (2254499)Instructions burned: 868 (million) % 56.51/8.46 % (2254508)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3645296656:i=879:kws=inv_precedence:fsr=off_2993 on theBenchmark for (2993ds/879Mi) % 56.51/8.46 % (2254508)Instruction limit reached! % 56.51/8.46 % (2254508)------------------------------ % 56.51/8.46 % (2254508)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 56.51/8.46 % (2254508)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 108.25/15.78 % (2254508)CaDiCaL version: 2.1.3 % 108.25/15.78 % (2254508)Termination reason: Instruction limit % 108.25/15.78 % (2254508)Termination phase: Saturation % 108.25/15.78 % (2254508)Time elapsed: 0.223 s % 108.25/15.78 % (2254508)Peak memory usage: 30 MB % 108.25/15.78 % (2254508)Instructions burned: 886 (million) % 108.25/15.78 % (2254510)fmb+10_1_sil=64000:random_seed=316433861:i=22061:nm=2:gsp=on_2990 on theBenchmark for (2990ds/22061Mi) % 108.25/15.78 % (2254505)Instruction limit reached! % 108.25/15.78 % (2254505)------------------------------ % 108.25/15.78 % (2254505)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 108.25/15.78 % (2254505)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 108.25/15.78 % (2254505)CaDiCaL version: 2.1.3 % 108.25/15.78 % (2254505)Termination reason: Instruction limit % 108.25/15.78 % (2254505)Termination phase: Saturation % 108.25/15.78 % (2254505)Time elapsed: 0.344 s % 108.25/15.78 % (2254505)Peak memory usage: 27 MB % 108.25/15.78 % (2254505)Instructions burned: 692 (million) % 108.25/15.78 % (2254512)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1515666296:i=9515:nm=5_2990 on theBenchmark for (2990ds/9515Mi) % 108.25/15.78 % (2254504)Instruction limit reached! % 108.25/15.78 % (2254504)------------------------------ % 108.25/15.78 % (2254504)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 108.25/15.78 % (2254504)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 108.25/15.78 % (2254504)CaDiCaL version: 2.1.3 % 108.25/15.78 % (2254504)Termination reason: Instruction limit % 108.25/15.78 % (2254504)Termination phase: Finite model building preprocessing % 108.25/15.78 % (2254504)Time elapsed: 0.413 s % 108.25/15.78 % (2254504)Peak memory usage: 31 MB % 108.25/15.78 % (2254504)Instructions burned: 890 (million) % 108.25/15.78 % (2254514)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1063032707:fmbsr=1.7:i=920_2989 on theBenchmark for (2989ds/920Mi) % 108.25/15.78 % (2254501)Instruction limit reached! % 108.25/15.78 % (2254501)------------------------------ % 108.25/15.78 % (2254501)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 108.25/15.78 % (2254501)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 108.25/15.78 % (2254501)CaDiCaL version: 2.1.3 % 108.25/15.78 % (2254501)Termination reason: Instruction limit % 108.25/15.78 % (2254501)Termination phase: Saturation % 108.25/15.78 % (2254501)Time elapsed: 0.796 s % 108.25/15.78 % (2254501)Peak memory usage: 30 MB % 108.25/15.78 % (2254501)Instructions burned: 1179 (million) % 108.25/15.78 % (2254525)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=770865949:i=5131_2986 on theBenchmark for (2986ds/5131Mi) % 108.25/15.78 % (2254514)Instruction limit reached! % 108.25/15.78 % (2254514)------------------------------ % 108.25/15.78 % (2254514)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 108.25/15.78 % (2254514)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 108.25/15.78 % (2254514)CaDiCaL version: 2.1.3 % 108.25/15.78 % (2254514)Termination reason: Instruction limit % 108.25/15.78 % (2254514)Termination phase: Finite model building preprocessing % 108.25/15.78 % (2254514)Time elapsed: 0.527 s % 108.25/15.78 % (2254514)Peak memory usage: 31 MB % 108.25/15.78 % (2254514)Instructions burned: 921 (million) % 108.25/15.78 % (2254536)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1936804083:i=1472:ins=7:fdi=8:gsp=on_2983 on theBenchmark for (2983ds/1472Mi) % 108.25/15.78 % (2254536)Instruction limit reached! % 108.25/15.78 % (2254536)------------------------------ % 108.25/15.78 % (2254536)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 108.25/15.78 % (2254536)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 108.25/15.78 % (2254536)CaDiCaL version: 2.1.3 % 108.25/15.78 % (2254536)Termination reason: Instruction limit % 108.25/15.78 % (2254536)Termination phase: Saturation % 108.25/15.78 % (2254536)Time elapsed: 0.684 s % 108.25/15.78 % (2254536)Peak memory usage: 28 MB % 108.25/15.78 % (2254536)Instructions burned: 1472 (million) % 108.25/15.78 % (2254628)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=824954476:i=6324_2976 on theBenchmark for (2976ds/6324Mi) % 108.25/15.78 % (2254525)Instruction limit reached! % 108.25/15.78 % (2254525)------------------------------ % 108.25/15.78 % (2254525)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 108.25/15.78 % (2254525)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 108.25/15.78 % (2254525)CaDiCaL version: 2.1.3 % 108.25/15.78 % (2254525)Termination reason: Instruction limit % 201.25/28.98 % (2254525)Termination phase: Saturation % 201.25/28.98 % (2254525)Time elapsed: 3.042 s % 201.25/28.98 % (2254525)Peak memory usage: 60 MB % 201.25/28.98 % (2254525)Instructions burned: 5132 (million) % 201.25/28.98 % (2254695)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=861854205:fmbsr=2.30978:i=2174_2955 on theBenchmark for (2955ds/2174Mi) % 201.25/28.98 % (2254695)Instruction limit reached! % 201.25/28.98 % (2254695)------------------------------ % 201.25/28.98 % (2254695)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 201.25/28.98 % (2254695)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 201.25/28.98 % (2254695)CaDiCaL version: 2.1.3 % 201.25/28.98 % (2254695)Termination reason: Instruction limit % 201.25/28.98 % (2254695)Termination phase: Finite model building preprocessing % 201.25/28.98 % (2254695)Time elapsed: 0.995 s % 201.25/28.98 % (2254695)Peak memory usage: 48 MB % 201.25/28.98 % (2254695)Instructions burned: 2174 (million) % 201.25/28.98 % (2254697)ott-2_1_sil=16000:newcnf=on:random_seed=2498698793:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2945 on theBenchmark for (2945ds/869Mi) % 201.25/28.98 % (2254628)Instruction limit reached! % 201.25/28.98 % (2254628)------------------------------ % 201.25/28.98 % (2254628)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 201.25/28.98 % (2254628)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 201.25/28.98 % (2254628)CaDiCaL version: 2.1.3 % 201.25/28.98 % (2254628)Termination reason: Instruction limit % 201.25/28.98 % (2254628)Termination phase: Finite model building preprocessing % 201.25/28.98 % (2254628)Time elapsed: 3.244 s % 201.25/28.98 % (2254628)Peak memory usage: 63 MB % 201.25/28.98 % (2254628)Instructions burned: 6325 (million) % 201.25/28.98 % (2254699)ott+10_1_sil=32000:tgt=ground:random_seed=1886413730:i=5114:av=off_2944 on theBenchmark for (2944ds/5114Mi) % 201.25/28.98 % (2254697)Instruction limit reached! % 201.25/28.98 % (2254697)------------------------------ % 201.25/28.98 % (2254697)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 201.25/28.98 % (2254697)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 201.25/28.98 % (2254697)CaDiCaL version: 2.1.3 % 201.25/28.98 % (2254697)Termination reason: Instruction limit % 201.25/28.98 % (2254697)Termination phase: Saturation % 201.25/28.98 % (2254697)Time elapsed: 0.439 s % 201.25/28.98 % (2254697)Peak memory usage: 28 MB % 201.25/28.98 % (2254697)Instructions burned: 869 (million) % 201.25/28.98 % (2254701)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=3402936700:i=54282_2941 on theBenchmark for (2941ds/54282Mi) % 201.25/28.98 % (2254512)Instruction limit reached! % 201.25/28.98 % (2254512)------------------------------ % 201.25/28.98 % (2254512)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 201.25/28.98 % (2254512)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 201.25/28.98 % (2254512)CaDiCaL version: 2.1.3 % 201.25/28.98 % (2254512)Termination reason: Instruction limit % 201.25/28.98 % (2254512)Termination phase: Finite model building preprocessing % 201.25/28.98 % (2254512)Time elapsed: 5.127 s % 201.25/28.98 % (2254512)Peak memory usage: 86 MB % 201.25/28.98 % (2254512)Instructions burned: 9516 (million) % 201.25/28.98 % (2254703)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=44193749:i=3512:aac=none_2938 on theBenchmark for (2938ds/3512Mi) % 201.25/28.98 % (2254510)Instruction limit reached! % 201.25/28.98 % (2254510)------------------------------ % 201.25/28.98 % (2254510)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 201.25/28.98 % (2254510)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 201.25/28.98 % (2254510)CaDiCaL version: 2.1.3 % 201.25/28.98 % (2254510)Termination reason: Instruction limit % 201.25/28.98 % (2254510)Termination phase: Finite model building preprocessing % 201.25/28.98 % (2254510)Time elapsed: 6.426 s % 201.25/28.98 % (2254510)Peak memory usage: 195 MB % 201.25/28.98 % (2254510)Instructions burned: 22064 (million) % 201.25/28.98 % (2254705)dis+21_1_sil=32000:sas=cadical:random_seed=1302564723:i=3773:amm=off_2926 on theBenchmark for (2926ds/3773Mi) % 201.25/28.98 % (2254703)Instruction limit reached! % 201.25/28.98 % (2254703)------------------------------ % 201.25/28.98 % (2254703)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 201.25/28.98 % (2254703)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 201.25/28.98 % (2254703)CaDiCaL version: 2.1.3 % 201.25/28.98 % (2254703)Termination reason: Instruction limit % 201.25/28.98 % (2254703)Termination phase: Saturation % 201.25/28.98 % (2254703)Time elapsed: 2.016 s % 290.31/41.44 % (2254703)Peak memory usage: 50 MB % 290.31/41.44 % (2254703)Instructions burned: 3512 (million) % 290.31/41.44 % (2254707)ott+11_1_sil=16000:gs=on:random_seed=2095299315:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2918 on theBenchmark for (2918ds/2251Mi) % 290.31/41.44 % (2254705)Instruction limit reached! % 290.31/41.44 % (2254705)------------------------------ % 290.31/41.44 % (2254705)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 290.31/41.44 % (2254705)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 290.31/41.44 % (2254705)CaDiCaL version: 2.1.3 % 290.31/41.44 % (2254705)Termination reason: Instruction limit % 290.31/41.44 % (2254705)Termination phase: Saturation % 290.31/41.44 % (2254705)Time elapsed: 1.178 s % 290.31/41.44 % (2254705)Peak memory usage: 51 MB % 290.31/41.44 % (2254705)Instructions burned: 3775 (million) % 290.31/41.44 % (2254709)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=1297840178:fmbsr=1.6:i=67534_2914 on theBenchmark for (2914ds/67534Mi) % 290.31/41.44 % (2254699)Instruction limit reached! % 290.31/41.44 % (2254699)------------------------------ % 290.31/41.44 % (2254699)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 290.31/41.44 % (2254699)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 290.31/41.44 % (2254699)CaDiCaL version: 2.1.3 % 290.31/41.44 % (2254699)Termination reason: Instruction limit % 290.31/41.44 % (2254699)Termination phase: Saturation % 290.31/41.44 % (2254699)Time elapsed: 3.139 s % 290.31/41.44 % (2254699)Peak memory usage: 68 MB % 290.31/41.44 % (2254699)Instructions burned: 5114 (million) % 290.31/41.44 % (2254711)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=3585884870:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2912 on theBenchmark for (2912ds/4591Mi) % 290.31/41.44 % (2254707)Instruction limit reached! % 290.31/41.44 % (2254707)------------------------------ % 290.31/41.44 % (2254707)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 290.31/41.44 % (2254707)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 290.31/41.44 % (2254707)CaDiCaL version: 2.1.3 % 290.31/41.44 % (2254707)Termination reason: Instruction limit % 290.31/41.44 % (2254707)Termination phase: Saturation % 290.31/41.44 % (2254707)Time elapsed: 1.160 s % 290.31/41.44 % (2254707)Peak memory usage: 33 MB % 290.31/41.44 % (2254707)Instructions burned: 2252 (million) % 290.31/41.44 % (2254713)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=1988187268:i=29340_2906 on theBenchmark for (2906ds/29340Mi) % 290.31/41.44 % (2254711)Instruction limit reached! % 290.31/41.44 % (2254711)------------------------------ % 290.31/41.44 % (2254711)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 290.31/41.44 % (2254711)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 290.31/41.44 % (2254711)CaDiCaL version: 2.1.3 % 290.31/41.44 % (2254711)Termination reason: Instruction limit % 290.31/41.44 % (2254711)Termination phase: Saturation % 290.31/41.44 % (2254711)Time elapsed: 1.732 s % 290.31/41.44 % (2254711)Peak memory usage: 32 MB % 290.31/41.44 % (2254711)Instructions burned: 4594 (million) % 290.31/41.44 % (2254715)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=2018053040:i=5211_2894 on theBenchmark for (2894ds/5211Mi) % 290.31/41.44 % (2254715)Instruction limit reached! % 290.31/41.44 % (2254715)------------------------------ % 290.31/41.44 % (2254715)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 290.31/41.44 % (2254715)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 290.31/41.44 % (2254715)CaDiCaL version: 2.1.3 % 290.31/41.44 % (2254715)Termination reason: Instruction limit % 290.31/41.44 % (2254715)Termination phase: Saturation % 290.31/41.44 % (2254715)Time elapsed: 2.102 s % 290.31/41.44 % (2254715)Peak memory usage: 49 MB % 290.31/41.44 % (2254715)Instructions burned: 5211 (million) % 290.31/41.44 % (2254717)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=203037449:i=5497:nm=2_2873 on theBenchmark for (2873ds/5497Mi) % 290.31/41.44 % TRYING [1] % 290.31/41.44 % TRYING [2] % 290.31/41.44 % (2254717)Instruction limit reached! % 290.31/41.44 % (2254717)------------------------------ % 290.31/41.44 % (2254717)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 290.31/41.44 % (2254717)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 290.31/41.44 % (2254717)CaDiCaL version: 2.1.3 % 290.31/41.44 % (2254717)Termination reason: Instruction limit % 290.31/41.44 % (2254717)Termination phase: Finite model building preprocessing % 290.31/41.44 % (2254717)TimeTerminated % 300.43/42.93 % Vampire exiting %------------------------------------------------------------------------------