%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWW274+1 : TPTP v9.3.1. Released v5.2.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % Computer : n012.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:44 PM UTC 2026 % Result : Timeout 300.49s 42.83s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.01 % Problem : SWW274+1 : TPTP v9.3.1. Released v5.2.0. % 0.00/0.03 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.05/0.12 % Computer : n012.cluster.edu % 0.05/0.12 % Model : x86_64 x86_64 % 0.05/0.12 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.05/0.12 % Memory : 8046.5625MB % 0.05/0.12 % OS : Linux 6.8.0-71-generic % 0.05/0.12 % CPULimit : 300 % 0.05/0.12 % WCLimit : 300 % 0.05/0.12 % DateTime : Mon Sep 28 13:27:33 UTC 2026 % 0.05/0.12 % CPUTime : % 0.05/0.12 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.05/0.14 Running first-order model finding % 0.05/0.14 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 % 7.06/1.22 % (3375077)Will run a generic schedule for satisfiability detection. % 7.06/1.22 % (3375083)% WARNING: option uhcvi not known. % 7.06/1.22 % (3375084)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3144552769:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 7.06/1.22 % (3375087)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2019191453:i=131_2999 on theBenchmark for (2999ds/131Mi) % 7.06/1.22 % (3375082)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=592509377_2999 on theBenchmark for (2999ds/0Mi) % 7.06/1.22 % (3375083)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=926591481:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 7.06/1.22 % (3375085)dis+10_1_sil=32000:sp=arity:random_seed=4079821620:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 7.06/1.22 % (3375086)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1464770852:i=116_2999 on theBenchmark for (2999ds/116Mi) % 7.06/1.22 % (3375088)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2437565662:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 7.06/1.22 % (3375085)Instruction limit reached! % 7.06/1.22 % (3375085)------------------------------ % 7.06/1.22 % (3375085)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.06/1.22 % (3375085)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.06/1.22 % (3375085)CaDiCaL version: 2.1.3 % 7.06/1.22 % (3375085)Termination reason: Instruction limit % 7.06/1.22 % (3375085)Termination phase: Saturation % 7.06/1.22 % (3375085)Time elapsed: 0.029 s % 7.06/1.22 % (3375085)Peak memory usage: 14 MB % 7.06/1.22 % (3375085)Instructions burned: 105 (million) % 7.06/1.22 % (3375086)Instruction limit reached! % 7.06/1.22 % (3375086)------------------------------ % 7.06/1.22 % (3375086)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.06/1.22 % (3375086)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.06/1.22 % (3375086)CaDiCaL version: 2.1.3 % 7.06/1.22 % (3375086)Termination reason: Instruction limit % 7.06/1.22 % (3375086)Termination phase: Saturation % 7.06/1.22 % (3375086)Time elapsed: 0.031 s % 7.06/1.22 % (3375086)Peak memory usage: 14 MB % 7.06/1.22 % (3375086)Instructions burned: 118 (million) % 7.06/1.22 % (3375087)Instruction limit reached! % 7.06/1.22 % (3375087)------------------------------ % 7.06/1.22 % (3375087)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.06/1.22 % (3375087)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.06/1.22 % (3375087)CaDiCaL version: 2.1.3 % 7.06/1.22 % (3375087)Termination reason: Instruction limit % 7.06/1.22 % (3375087)Termination phase: Saturation % 7.06/1.22 % (3375087)Time elapsed: 0.037 s % 7.06/1.22 % (3375087)Peak memory usage: 14 MB % 7.06/1.22 % (3375087)Instructions burned: 133 (million) % 7.06/1.22 % (3375096)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=4016914068:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 7.06/1.22 % (3375097)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3883820378:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 7.06/1.22 % (3375098)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=1015172775:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi) % 7.06/1.22 % (3375088)Instruction limit reached! % 7.06/1.22 % (3375088)------------------------------ % 7.06/1.22 % (3375088)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.06/1.22 % (3375088)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.06/1.22 % (3375088)CaDiCaL version: 2.1.3 % 7.06/1.22 % (3375088)Termination reason: Instruction limit % 7.06/1.22 % (3375088)Termination phase: Saturation % 7.06/1.22 % (3375088)Time elapsed: 0.049 s % 7.06/1.22 % (3375088)Peak memory usage: 15 MB % 7.06/1.22 % (3375088)Instructions burned: 160 (million) % 7.06/1.22 % (3375102)ott-21_1_sil=16000:fs=off:random_seed=4063820250:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi) % 7.06/1.22 % (3375097)Instruction limit reached! % 7.06/1.22 % (3375097)------------------------------ % 7.06/1.22 % (3375097)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.06/1.22 % (3375097)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.06/1.22 % (3375097)CaDiCaL version: 2.1.3 % 22.02/3.36 % (3375097)Termination reason: Instruction limit % 22.02/3.36 % (3375097)Termination phase: Saturation % 22.02/3.36 % (3375097)Time elapsed: 0.035 s % 22.02/3.36 % (3375097)Peak memory usage: 15 MB % 22.02/3.36 % (3375097)Instructions burned: 132 (million) % 22.02/3.36 % (3375104)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2336277343:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 22.02/3.36 % (3375102)Instruction limit reached! % 22.02/3.36 % (3375102)------------------------------ % 22.02/3.36 % (3375102)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.02/3.36 % (3375102)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.02/3.36 % (3375102)CaDiCaL version: 2.1.3 % 22.02/3.36 % (3375102)Termination reason: Instruction limit % 22.02/3.36 % (3375102)Termination phase: Saturation % 22.02/3.36 % (3375102)Time elapsed: 0.049 s % 22.02/3.36 % (3375102)Peak memory usage: 14 MB % 22.02/3.36 % (3375102)Instructions burned: 183 (million) % 22.02/3.36 % (3375106)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2001575783:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 22.02/3.36 % TRYING [1] % 22.02/3.36 % TRYING [2] % 22.02/3.36 % TRYING [1] % 22.02/3.36 % TRYING [2] % 22.02/3.36 % (3375096)Instruction limit reached! % 22.02/3.36 % (3375096)------------------------------ % 22.02/3.36 % (3375096)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.02/3.36 % (3375096)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.02/3.36 % (3375096)CaDiCaL version: 2.1.3 % 22.02/3.36 % (3375096)Termination reason: Instruction limit % 22.02/3.36 % (3375096)Termination phase: Finite model building constraint generation % 22.02/3.36 % (3375096)Time elapsed: 0.183 s % 22.02/3.36 % (3375096)Peak memory usage: 31 MB % 22.02/3.36 % (3375096)Instructions burned: 714 (million) % 22.02/3.36 % (3375108)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1535581437:i=1179_2997 on theBenchmark for (2997ds/1179Mi) % 22.02/3.36 % (3375104)Instruction limit reached! % 22.02/3.36 % (3375104)------------------------------ % 22.02/3.36 % (3375104)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.02/3.36 % (3375104)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.02/3.36 % (3375104)CaDiCaL version: 2.1.3 % 22.02/3.36 % (3375104)Termination reason: Instruction limit % 22.02/3.36 % (3375104)Termination phase: Saturation % 22.02/3.36 % (3375104)Time elapsed: 0.160 s % 22.02/3.36 % (3375104)Peak memory usage: 16 MB % 22.02/3.36 % (3375104)Instructions burned: 477 (million) % 22.02/3.36 % (3375110)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2099355211:i=889:ins=1_2997 on theBenchmark for (2997ds/889Mi) % 22.02/3.36 % (3375098)Instruction limit reached! % 22.02/3.36 % (3375098)------------------------------ % 22.02/3.36 % (3375098)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.02/3.36 % (3375098)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.02/3.36 % (3375098)CaDiCaL version: 2.1.3 % 22.02/3.36 % (3375098)Termination reason: Instruction limit % 22.02/3.36 % (3375098)Termination phase: Saturation % 22.02/3.36 % (3375098)Time elapsed: 0.219 s % 22.02/3.36 % (3375098)Peak memory usage: 20 MB % 22.02/3.36 % (3375098)Instructions burned: 685 (million) % 22.02/3.36 % TRYING [3] % 22.02/3.36 % (3375112)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=2885949843:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2996 on theBenchmark for (2996ds/692Mi) % 22.02/3.36 % TRYING [1] % 22.02/3.36 % TRYING [2] % 22.02/3.36 % (3375106)Instruction limit reached! % 22.02/3.36 % (3375106)------------------------------ % 22.02/3.36 % (3375106)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.02/3.36 % (3375106)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.02/3.36 % (3375106)CaDiCaL version: 2.1.3 % 22.02/3.36 % (3375106)Termination reason: Instruction limit % 22.02/3.36 % (3375106)Termination phase: Finite model building constraint generation % 22.02/3.36 % (3375106)Time elapsed: 0.226 s % 22.02/3.36 % (3375106)Peak memory usage: 34 MB % 22.02/3.36 % (3375106)Instructions burned: 866 (million) % 22.02/3.36 % (3375114)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3787595759:i=879:kws=inv_precedence:fsr=off_2996 on theBenchmark for (2996ds/879Mi) % 22.02/3.36 % (3375110)Instruction limit reached! % 22.02/3.36 % (3375110)------------------------------ % 22.02/3.36 % (3375110)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 53.06/7.71 % (3375110)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 53.06/7.71 % (3375110)CaDiCaL version: 2.1.3 % 53.06/7.71 % (3375110)Termination reason: Instruction limit % 53.06/7.71 % (3375110)Termination phase: Finite model building constraint generation % 53.06/7.71 % (3375110)Time elapsed: 0.251 s % 53.06/7.71 % (3375110)Peak memory usage: 65 MB % 53.06/7.71 % (3375110)Instructions burned: 893 (million) % 53.06/7.71 % (3375112)Instruction limit reached! % 53.06/7.71 % (3375112)------------------------------ % 53.06/7.71 % (3375112)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 53.06/7.71 % (3375112)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 53.06/7.71 % (3375112)CaDiCaL version: 2.1.3 % 53.06/7.71 % (3375112)Termination reason: Instruction limit % 53.06/7.71 % (3375112)Termination phase: Saturation % 53.06/7.71 % (3375112)Time elapsed: 0.242 s % 53.06/7.71 % (3375112)Peak memory usage: 21 MB % 53.06/7.71 % (3375112)Instructions burned: 692 (million) % 53.06/7.71 % (3375116)fmb+10_1_sil=64000:random_seed=3178724282:i=22061:nm=2:gsp=on_2994 on theBenchmark for (2994ds/22061Mi) % 53.06/7.71 % (3375117)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2167071604:i=9515:nm=5_2994 on theBenchmark for (2994ds/9515Mi) % 53.06/7.71 % (3375114)Instruction limit reached! % 53.06/7.71 % (3375114)------------------------------ % 53.06/7.71 % (3375114)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 53.06/7.71 % (3375114)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 53.06/7.71 % (3375114)CaDiCaL version: 2.1.3 % 53.06/7.71 % (3375114)Termination reason: Instruction limit % 53.06/7.71 % (3375114)Termination phase: Saturation % 53.06/7.71 % (3375114)Time elapsed: 0.252 s % 53.06/7.71 % (3375114)Peak memory usage: 21 MB % 53.06/7.71 % (3375114)Instructions burned: 881 (million) % 53.06/7.71 % (3375120)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1634184514:fmbsr=1.7:i=920_2993 on theBenchmark for (2993ds/920Mi) % 53.06/7.71 % (3375108)Instruction limit reached! % 53.06/7.71 % (3375108)------------------------------ % 53.06/7.71 % (3375108)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 53.06/7.71 % (3375108)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 53.06/7.71 % (3375108)CaDiCaL version: 2.1.3 % 53.06/7.71 % (3375108)Termination reason: Instruction limit % 53.06/7.71 % (3375108)Termination phase: Saturation % 53.06/7.71 % (3375108)Time elapsed: 0.403 s % 53.06/7.71 % (3375108)Peak memory usage: 22 MB % 53.06/7.71 % (3375108)Instructions burned: 1181 (million) % 53.06/7.71 % (3375122)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1761491435:i=5131_2993 on theBenchmark for (2993ds/5131Mi) % 53.06/7.71 % (3375117)Cannot represent all propositional literals internally % 53.06/7.71 % (3375117)Refutation not found, incomplete strategy % 53.06/7.71 % (3375117)------------------------------ % 53.06/7.71 % (3375117)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 53.06/7.71 % (3375117)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 53.06/7.71 % (3375117)CaDiCaL version: 2.1.3 % 53.06/7.71 % (3375117)Termination reason: Refutation not found, incomplete strategy % 53.06/7.71 % (3375117)Time elapsed: 0.150 s % 53.06/7.71 % (3375117)Peak memory usage: 22 MB % 53.06/7.71 % (3375117)Instructions burned: 563 (million) % 53.06/7.71 % TRYING [1] % 53.06/7.71 % (3375117)------------------------------ % 53.06/7.71 % (3375117)------------------------------ % 53.06/7.71 % (3375124)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2564806259:i=1472:ins=7:fdi=8:gsp=on_2992 on theBenchmark for (2992ds/1472Mi) % 53.06/7.71 % TRYING [2] % 53.06/7.71 % TRYING [8] % 53.06/7.71 % (3375120)Instruction limit reached! % 53.06/7.71 % (3375120)------------------------------ % 53.06/7.71 % (3375120)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 53.06/7.71 % (3375120)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 53.06/7.71 % (3375120)CaDiCaL version: 2.1.3 % 53.06/7.71 % (3375120)Termination reason: Instruction limit % 53.06/7.71 % (3375120)Termination phase: Finite model building constraint generation % 53.06/7.71 % (3375120)Time elapsed: 0.219 s % 53.06/7.71 % (3375120)Peak memory usage: 45 MB % 53.06/7.71 % (3375120)Instructions burned: 921 (million) % 53.06/7.71 % (3375126)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=794568469:i=6324_2991 on theBenchmark for (2991ds/6324Mi) % 53.06/7.71 % TRYING [4] % 53.06/7.71 % (3375126)Cannot represent all propositional literals internally % 119.42/17.19 % (3375126)Refutation not found, incomplete strategy % 119.42/17.19 % (3375126)------------------------------ % 119.42/17.19 % (3375126)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 119.42/17.19 % (3375126)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 119.42/17.19 % (3375126)CaDiCaL version: 2.1.3 % 119.42/17.19 % (3375126)Termination reason: Refutation not found, incomplete strategy % 119.42/17.19 % (3375126)Time elapsed: 0.163 s % 119.42/17.19 % (3375126)Peak memory usage: 22 MB % 119.42/17.19 % (3375126)Instructions burned: 598 (million) % 119.42/17.19 % (3375126)------------------------------ % 119.42/17.19 % (3375126)------------------------------ % 119.42/17.19 % (3375128)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=2685365580:fmbsr=2.30978:i=2174_2989 on theBenchmark for (2989ds/2174Mi) % 119.42/17.19 % (3375124)Instruction limit reached! % 119.42/17.19 % (3375124)------------------------------ % 119.42/17.19 % (3375124)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 119.42/17.19 % (3375124)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 119.42/17.19 % (3375124)CaDiCaL version: 2.1.3 % 119.42/17.19 % (3375124)Termination reason: Instruction limit % 119.42/17.19 % (3375124)Termination phase: Saturation % 119.42/17.19 % (3375124)Time elapsed: 0.393 s % 119.42/17.19 % (3375124)Peak memory usage: 26 MB % 119.42/17.19 % (3375124)Instructions burned: 1472 (million) % 119.42/17.19 % (3375130)ott-2_1_sil=16000:newcnf=on:random_seed=485758597:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2988 on theBenchmark for (2988ds/869Mi) % 119.42/17.19 % TRYING [3] % 119.42/17.19 % (3375130)Instruction limit reached! % 119.42/17.19 % (3375130)------------------------------ % 119.42/17.19 % (3375130)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 119.42/17.19 % (3375130)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 119.42/17.19 % (3375130)CaDiCaL version: 2.1.3 % 119.42/17.19 % (3375130)Termination reason: Instruction limit % 119.42/17.19 % (3375130)Termination phase: Saturation % 119.42/17.19 % (3375130)Time elapsed: 0.275 s % 119.42/17.19 % (3375130)Peak memory usage: 18 MB % 119.42/17.19 % (3375130)Instructions burned: 872 (million) % 119.42/17.19 % (3375132)ott+10_1_sil=32000:tgt=ground:random_seed=1649157672:i=5114:av=off_2985 on theBenchmark for (2985ds/5114Mi) % 119.42/17.19 % (3375128)Instruction limit reached! % 119.42/17.19 % (3375128)------------------------------ % 119.42/17.19 % (3375128)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 119.42/17.19 % (3375128)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 119.42/17.19 % (3375128)CaDiCaL version: 2.1.3 % 119.42/17.19 % (3375128)Termination reason: Instruction limit % 119.42/17.19 % (3375128)Termination phase: Finite model building preprocessing % 119.42/17.19 % (3375128)Time elapsed: 0.579 s % 119.42/17.19 % (3375128)Peak memory usage: 41 MB % 119.42/17.19 % (3375128)Instructions burned: 2178 (million) % 119.42/17.19 % (3375134)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=923170806:i=54282_2983 on theBenchmark for (2983ds/54282Mi) % 119.42/17.19 % TRYING [1] % 119.42/17.19 % TRYING [2] % 119.42/17.19 % TRYING [3] % 119.42/17.19 % (3375122)Instruction limit reached! % 119.42/17.19 % (3375122)------------------------------ % 119.42/17.19 % (3375122)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 119.42/17.19 % (3375122)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 119.42/17.19 % (3375122)CaDiCaL version: 2.1.3 % 119.42/17.19 % (3375122)Termination reason: Instruction limit % 119.42/17.19 % (3375122)Termination phase: Saturation % 119.42/17.19 % (3375122)Time elapsed: 1.637 s % 119.42/17.19 % (3375122)Peak memory usage: 36 MB % 119.42/17.19 % (3375122)Instructions burned: 5134 (million) % 119.42/17.19 % (3375137)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=2517611048:i=3512:aac=none_2976 on theBenchmark for (2976ds/3512Mi) % 119.42/17.19 % TRYING [4] % 119.42/17.19 % TRYING [4] % 119.42/17.19 % (3375132)Instruction limit reached! % 119.42/17.19 % (3375132)------------------------------ % 119.42/17.19 % (3375132)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 119.42/17.19 % (3375132)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 119.42/17.19 % (3375132)CaDiCaL version: 2.1.3 % 119.42/17.19 % (3375132)Termination reason: Instruction limit % 119.42/17.19 % (3375132)Termination phase: Saturation % 119.42/17.19 % (3375132)Time elapsed: 1.768 s % 119.42/17.19 % (3375132)Peak memory usage: 39 MB % 119.42/17.19 % (3375132)Instructions burned: 5116 (million) % 119.42/17.19 % (3375139)dis+21_1_sil=32000:sas=cadical:random_seed=1896501839:i=3773:amm=off_2967 on theBenchmark for (2967ds/3773Mi) % 174.30/24.99 % (3375137)Instruction limit reached! % 174.30/24.99 % (3375137)------------------------------ % 174.30/24.99 % (3375137)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 174.30/24.99 % (3375137)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 174.30/24.99 % (3375137)CaDiCaL version: 2.1.3 % 174.30/24.99 % (3375137)Termination reason: Instruction limit % 174.30/24.99 % (3375137)Termination phase: Saturation % 174.30/24.99 % (3375137)Time elapsed: 1.145 s % 174.30/24.99 % (3375137)Peak memory usage: 34 MB % 174.30/24.99 % (3375137)Instructions burned: 3514 (million) % 174.30/24.99 % (3375141)ott+11_1_sil=16000:gs=on:random_seed=1290799753:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2964 on theBenchmark for (2964ds/2251Mi) % 174.30/24.99 % (3375141)Instruction limit reached! % 174.30/24.99 % (3375141)------------------------------ % 174.30/24.99 % (3375141)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 174.30/24.99 % (3375141)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 174.30/24.99 % (3375141)CaDiCaL version: 2.1.3 % 174.30/24.99 % (3375141)Termination reason: Instruction limit % 174.30/24.99 % (3375141)Termination phase: Saturation % 174.30/24.99 % (3375141)Time elapsed: 0.727 s % 174.30/24.99 % (3375141)Peak memory usage: 26 MB % 174.30/24.99 % (3375141)Instructions burned: 2253 (million) % 174.30/24.99 % (3375143)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=1267791027:fmbsr=1.6:i=67534_2957 on theBenchmark for (2957ds/67534Mi) % 174.30/24.99 % (3375139)Instruction limit reached! % 174.30/24.99 % (3375139)------------------------------ % 174.30/24.99 % (3375139)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 174.30/24.99 % (3375139)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 174.30/24.99 % (3375139)CaDiCaL version: 2.1.3 % 174.30/24.99 % (3375139)Termination reason: Instruction limit % 174.30/24.99 % (3375139)Termination phase: Saturation % 174.30/24.99 % (3375139)Time elapsed: 1.271 s % 174.30/24.99 % (3375139)Peak memory usage: 35 MB % 174.30/24.99 % (3375139)Instructions burned: 3773 (million) % 174.30/24.99 % (3375145)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=106750218:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2955 on theBenchmark for (2955ds/4591Mi) % 174.30/24.99 % TRYING [5] % 174.30/24.99 % (3375145)Instruction limit reached! % 174.30/24.99 % (3375145)------------------------------ % 174.30/24.99 % (3375145)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 174.30/24.99 % (3375145)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 174.30/24.99 % (3375145)CaDiCaL version: 2.1.3 % 174.30/24.99 % (3375145)Termination reason: Instruction limit % 174.30/24.99 % (3375145)Termination phase: Saturation % 174.30/24.99 % (3375145)Time elapsed: 1.114 s % 174.30/24.99 % (3375145)Peak memory usage: 40 MB % 174.30/24.99 % (3375145)Instructions burned: 4594 (million) % 174.30/24.99 % (3375147)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=459597991:i=29340_2943 on theBenchmark for (2943ds/29340Mi) % 174.30/24.99 % (3375116)Instruction limit reached! % 174.30/24.99 % (3375116)------------------------------ % 174.30/24.99 % (3375116)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 174.30/24.99 % (3375116)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 174.30/24.99 % (3375116)CaDiCaL version: 2.1.3 % 174.30/24.99 % (3375116)Termination reason: Instruction limit % 174.30/24.99 % (3375116)Termination phase: Finite model building SAT solving % 174.30/24.99 % (3375116)Time elapsed: 5.433 s % 174.30/24.99 % (3375116)Peak memory usage: 606 MB % 174.30/24.99 % (3375116)Instructions burned: 22063 (million) % 174.30/24.99 % (3375149)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=3423264104:i=5211_2939 on theBenchmark for (2939ds/5211Mi) % 174.30/24.99 % TRYING [7] % 174.30/24.99 % TRYING [5] % 174.30/24.99 % (3375149)Instruction limit reached! % 174.30/24.99 % (3375149)------------------------------ % 174.30/24.99 % (3375149)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 174.30/24.99 % (3375149)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 174.30/24.99 % (3375149)CaDiCaL version: 2.1.3 % 174.30/24.99 % (3375149)Termination reason: Instruction limit % 174.30/24.99 % (3375149)Termination phase: Saturation % 174.30/24.99 % (3375149)Time elapsed: 1.480 s % 174.30/24.99 % (3375149)Peak memory usage: 46 MB % 174.30/24.99 % (3375149)Instructions burned: 5216 (million) % 174.30/24.99 % (3375151)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=2738993968:i=5497:nm=2_2924 on theBenchmark for (2924ds/5497Mi) % 211.08/30.19 % (3375151)Cannot represent all propositional literals internally % 211.08/30.19 % (3375151)Refutation not found, incomplete strategy % 211.08/30.19 % (3375151)------------------------------ % 211.08/30.19 % (3375151)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 211.08/30.19 % (3375151)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 211.08/30.19 % (3375151)CaDiCaL version: 2.1.3 % 211.08/30.19 % (3375151)Termination reason: Refutation not found, incomplete strategy % 211.08/30.19 % (3375151)Time elapsed: 0.154 s % 211.08/30.19 % (3375151)Peak memory usage: 22 MB % 211.08/30.19 % (3375151)Instructions burned: 576 (million) % 211.08/30.19 % (3375151)------------------------------ % 211.08/30.19 % (3375151)------------------------------ % 211.08/30.19 % (3375153)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=2037141459:fmbsr=2:i=46332_2922 on theBenchmark for (2922ds/46332Mi) % 211.08/30.19 % TRYING [15] % 211.08/30.19 % (3375147)Instruction limit reached! % 211.08/30.19 % (3375147)------------------------------ % 211.08/30.19 % (3375147)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 211.08/30.19 % (3375147)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 211.08/30.19 % (3375147)CaDiCaL version: 2.1.3 % 211.08/30.19 % (3375147)Termination reason: Instruction limit % 211.08/30.19 % (3375147)Termination phase: Saturation % 211.08/30.19 % (3375147)Time elapsed: 7.618 s % 211.08/30.19 % (3375147)Peak memory usage: 186 MB % 211.08/30.19 % (3375147)Instructions burned: 29345 (million) % 211.08/30.19 % (3375155)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=2676388155:i=14071_2867 on theBenchmark for (2867ds/14071Mi) % 211.08/30.19 % TRYING [12] % 211.08/30.19 % (3375134)Instruction limit reached! % 211.08/30.19 % (3375134)------------------------------ % 211.08/30.19 % (3375134)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 211.08/30.19 % (3375134)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 211.08/30.19 % (3375134)CaDiCaL version: 2.1.3 % 211.08/30.19 % (3375134)Termination reason: Instruction limit % 211.08/30.19 % (3375134)Termination phase: Finite model building constraint generation % 211.08/30.19 % (3375134)Time elapsed: 12.380 s % 211.08/30.19 % (3375134)Peak memory usage: 2161 MB % 211.08/30.19 % (3375134)Instructions burned: 54285 (million) % 211.08/30.19 % (3375157)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2402429284:i=22565:add=on:rawr=on_2857 on theBenchmark for (2857ds/22565Mi) % 211.08/30.19 % (3375155)Instruction limit reached! % 211.08/30.19 % (3375155)------------------------------ % 211.08/30.19 % (3375155)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 211.08/30.19 % (3375155)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 211.08/30.19 % (3375155)CaDiCaL version: 2.1.3 % 211.08/30.19 % (3375155)Termination reason: Instruction limit % 211.08/30.19 % (3375155)Termination phase: Finite model building constraint generation % 211.08/30.19 % (3375155)Time elapsed: 2.868 s % 211.08/30.19 % (3375155)Peak memory usage: 1013 MB % 211.08/30.19 % (3375155)Instructions burned: 14071 (million) % 211.08/30.19 % (3375159)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=1366462113:i=8173:av=off_2837 on theBenchmark for (2837ds/8173Mi) % 211.08/30.19 % (3375153)Instruction limit reached! % 211.08/30.19 % (3375153)------------------------------ % 211.08/30.19 % (3375153)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 211.08/30.19 % (3375153)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 211.08/30.19 % (3375153)CaDiCaL version: 2.1.3 % 211.08/30.19 % (3375153)Termination reason: Instruction limit % 211.08/30.19 % (3375153)Termination phase: Finite model building constraint generation % 211.08/30.19 % (3375153)Time elapsed: 8.784 s % 211.08/30.19 % (3375153)Peak memory usage: 2597 MB % 211.08/30.19 % (3375153)Instructions burned: 46335 (million) % 211.08/30.19 % (3375161)dis+10_16:1_sil=16000:random_seed=1169024891:i=9155:fsr=off_2832 on theBenchmark for (2832ds/9155Mi) % 211.08/30.19 % (3375143)Instruction limit reached! % 211.08/30.19 % (3375143)------------------------------ % 211.08/30.19 % (3375143)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 211.08/30.19 % (3375143)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 211.08/30.19 % (3375143)CaDiCaL version: 2.1.3 % 211.08/30.19 % (3375143)Termination reason: Instruction limit % 211.08/30.19 % (3375143)Termination phase: Finite model building constraint generation % 211.08/30.19 % (3375143)Time elapsed: 12.790 s % 300.49/42.83 % (3375143)Peak memory usage: 3585 MB % 300.49/42.83 % (3375143)Instructions burned: 67535 (million) % 300.49/42.83 % (3375163)ott-3_8_sil=64000:random_seed=3018852815:i=20139:bs=on_2825 on theBenchmark for (2825ds/20139Mi) % 300.49/42.83 % (3375159)Instruction limit reached! % 300.49/42.83 % (3375159)------------------------------ % 300.49/42.83 % (3375159)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.49/42.83 % (3375159)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.49/42.83 % (3375159)CaDiCaL version: 2.1.3 % 300.49/42.83 % (3375159)Termination reason: Instruction limit % 300.49/42.83 % (3375159)Termination phase: Saturation % 300.49/42.83 % (3375159)Time elapsed: 3.024 s % 300.49/42.83 % (3375159)Peak memory usage: 61 MB % 300.49/42.83 % (3375159)Instructions burned: 8174 (million) % 300.49/42.83 % (3375165)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=1581428901:fmbsr=2:i=32576_2807 on theBenchmark for (2807ds/32576Mi) % 300.49/42.83 % (3375084)Instruction limit reached! % 300.49/42.83 % (3375084)------------------------------ % 300.49/42.83 % (3375084)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.49/42.83 % (3375084)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.49/42.83 % (3375084)CaDiCaL version: 2.1.3 % 300.49/42.83 % (3375084)Termination reason: Instruction limit % 300.49/42.83 % (3375084)Termination phase: Saturation % 300.49/42.83 % (3375084)Time elapsed: 19.355 s % 300.49/42.83 % (3375084)Peak memory usage: 158 MB % 300.49/42.83 % (3375084)Instructions burned: 88032 (million) % 300.49/42.83 % (3375167)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=4007819289:i=11404_2805 on theBenchmark for (2805ds/11404Mi) % 300.49/42.83 % (3375161)Instruction limit reached! % 300.49/42.83 % (3375161)------------------------------ % 300.49/42.83 % (3375161)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.49/42.83 % (3375161)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.49/42.83 % (3375161)CaDiCaL version: 2.1.3 % 300.49/42.83 % (3375161)Termination reason: Instruction limit % 300.49/42.83 % (3375161)Termination phase: Saturation % 300.49/42.83 % (3375161)Time elapsed: 2.661 s % 300.49/42.83 % (3375161)Peak memory usage: 79 MB % 300.49/42.83 % (3375161)Instructions burned: 9158 (million) % 300.49/42.83 % TRYING [9] % 300.49/42.83 % (3375169)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=4181649783:i=14134_2805 on theBenchmark for (2805ds/14134Mi) % 300.49/42.83 % (3375157)Instruction limit reached! % 300.49/42.83 % (3375157)------------------------------ % 300.49/42.83 % (3375157)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.49/42.83 % (3375157)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.49/42.83 % (3375157)CaDiCaL version: 2.1.3 % 300.49/42.83 % (3375157)Termination reason: Instruction limit % 300.49/42.83 % (3375157)Termination phase: Saturation % 300.49/42.83 % (3375157)Time elapsed: 6.076 s % 300.49/42.83 % (3375157)Peak memory usage: 78 MB % 300.49/42.83 % (3375157)Instructions burned: 22568 (million) % 300.49/42.83 % (3375171)dis+33_16_sil=32000:sac=on:random_seed=3409537139:i=15851:nm=0_2796 on theBenchmark for (2796ds/15851Mi) % 300.49/42.83 % (3375167)Instruction limit reached! % 300.49/42.83 % (3375167)------------------------------ % 300.49/42.83 % (3375167)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.49/42.83 % (3375167)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.49/42.83 % (3375167)CaDiCaL version: 2.1.3 % 300.49/42.83 % (3375167)Termination reason: Instruction limit % 300.49/42.83 % (3375167)Termination phase: Saturation % 300.49/42.83 % (3375167)Time elapsed: 4.409 s % 300.49/42.83 % (3375167)Peak memory usage: 83 MB % 300.49/42.83 % (3375167)Instructions burned: 11406 (million) % 300.49/42.83 % (3375173)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=2327827288:avsq=on:i=17627:add=on:amm=off_2761 on theBenchmark for (2761ds/17627Mi) % 300.49/42.83 % (3375169)Instruction limit reached! % 300.49/42.83 % (3375169)------------------------------ % 300.49/42.83 % (3375169)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.49/42.83 % (3375169)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.49/42.83 % (3375169)CaDiCaL version: 2.1.3 % 300.49/42.83 % (3375169)Termination reason: Instruction limit % 300.49/42.83 % (3375169)Termination phase: Saturation % 300.49/42.83 % (3375169)Time elapsed: 5.366 s % 300.49/42.83 % (3375169)Peak memory usage: 73 MB % 300.49/42.83 % (3375169)Instructions burned: 14136 (million) % 300.49/42.83 % (3375175)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=172 % 300.49/42.83 Terminated % 300.49/42.83 % Vampire exiting %------------------------------------------------------------------------------