%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWX198-1 : TPTP v9.3.1. Released v9.3.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:46:42 PM UTC 2026 % Result : Timeout 300.02s 42.73s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.01 % Problem : SWX198-1 : TPTP v9.3.1. Released v9.3.0. % 0.00/0.03 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.05/0.11 % Computer : n012.cluster.edu % 0.05/0.11 % Model : x86_64 x86_64 % 0.05/0.11 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.05/0.11 % Memory : 8046.5625MB % 0.05/0.11 % OS : Linux 6.8.0-71-generic % 0.05/0.11 % CPULimit : 300 % 0.05/0.11 % WCLimit : 300 % 0.05/0.11 % DateTime : Mon Sep 28 15:07:34 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.13 Running first-order model finding % 0.05/0.13 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 % 8.74/1.42 % (3446487)Will run a generic schedule for satisfiability detection. % 8.74/1.42 % (3446493)% WARNING: option uhcvi not known. % 8.74/1.42 % (3446492)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2910449068_2999 on theBenchmark for (2999ds/0Mi) % 8.74/1.42 % (3446496)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1262083711:i=116_2999 on theBenchmark for (2999ds/116Mi) % 8.74/1.42 % (3446493)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1310337109:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 8.74/1.42 % (3446495)dis+10_1_sil=32000:sp=arity:random_seed=3335983528:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 8.74/1.42 % (3446494)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=934305795:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 8.74/1.42 % (3446497)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3927141108:i=131_2999 on theBenchmark for (2999ds/131Mi) % 8.74/1.42 % (3446498)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2303356198:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 8.74/1.42 % TRYING [1] % 8.74/1.42 % TRYING [2] % 8.74/1.42 % TRYING [3] % 8.74/1.42 % TRYING [4] % 8.74/1.42 % TRYING [5] % 8.74/1.42 % (3446495)Instruction limit reached! % 8.74/1.42 % (3446495)------------------------------ % 8.74/1.42 % (3446495)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.74/1.42 % (3446495)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.74/1.42 % (3446495)CaDiCaL version: 2.1.3 % 8.74/1.42 % (3446495)Termination reason: Instruction limit % 8.74/1.42 % (3446495)Termination phase: Saturation % 8.74/1.42 % (3446495)Time elapsed: 0.029 s % 8.74/1.42 % (3446495)Peak memory usage: 12 MB % 8.74/1.42 % (3446495)Instructions burned: 103 (million) % 8.74/1.42 % (3446496)Instruction limit reached! % 8.74/1.42 % (3446496)------------------------------ % 8.74/1.42 % (3446496)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.74/1.42 % (3446496)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.74/1.42 % (3446496)CaDiCaL version: 2.1.3 % 8.74/1.42 % (3446496)Termination reason: Instruction limit % 8.74/1.42 % (3446496)Termination phase: Saturation % 8.74/1.42 % (3446496)Time elapsed: 0.035 s % 8.74/1.42 % (3446496)Peak memory usage: 12 MB % 8.74/1.42 % (3446496)Instructions burned: 118 (million) % 8.74/1.42 % (3446497)Instruction limit reached! % 8.74/1.42 % (3446497)------------------------------ % 8.74/1.42 % (3446497)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.74/1.42 % (3446497)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.74/1.42 % (3446497)CaDiCaL version: 2.1.3 % 8.74/1.42 % (3446497)Termination reason: Instruction limit % 8.74/1.42 % (3446497)Termination phase: Saturation % 8.74/1.42 % (3446497)Time elapsed: 0.037 s % 8.74/1.42 % (3446497)Peak memory usage: 12 MB % 8.74/1.42 % (3446497)Instructions burned: 133 (million) % 8.74/1.42 % TRYING [6] % 8.74/1.42 % (3446506)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=4199146550:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 8.74/1.42 % TRYING [1] % 8.74/1.42 % TRYING [2] % 8.74/1.42 % TRYING [3] % 8.74/1.42 % (3446507)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1796942537:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 8.74/1.42 % (3446508)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=3932943039:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi) % 8.74/1.42 % (3446498)Instruction limit reached! % 8.74/1.42 % (3446498)------------------------------ % 8.74/1.42 % (3446498)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.74/1.42 % (3446498)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.74/1.42 % (3446498)CaDiCaL version: 2.1.3 % 8.74/1.42 % (3446498)Termination reason: Instruction limit % 8.74/1.42 % (3446498)Termination phase: Saturation % 8.74/1.42 % (3446498)Time elapsed: 0.048 s % 8.74/1.42 % (3446498)Peak memory usage: 12 MB % 8.74/1.42 % (3446498)Instructions burned: 173 (million) % 8.74/1.42 % TRYING [4] % 8.74/1.42 % (3446512)ott-21_1_sil=16000:fs=off:random_seed=2326424496:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi) % 8.74/1.42 % TRYING [5] % 8.74/1.42 % (3446507)Instruction limit reached! % 8.74/1.42 % (3446507)------------------------------ % 8.74/1.42 % (3446507)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 26.36/3.99 % (3446507)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.36/3.99 % (3446507)CaDiCaL version: 2.1.3 % 26.36/3.99 % (3446507)Termination reason: Instruction limit % 26.36/3.99 % (3446507)Termination phase: Saturation % 26.36/3.99 % (3446507)Time elapsed: 0.042 s % 26.36/3.99 % (3446507)Peak memory usage: 13 MB % 26.36/3.99 % (3446507)Instructions burned: 131 (million) % 26.36/3.99 % (3446514)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2851737863:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 26.36/3.99 % TRYING [7] % 26.36/3.99 % (3446512)Instruction limit reached! % 26.36/3.99 % (3446512)------------------------------ % 26.36/3.99 % (3446512)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 26.36/3.99 % (3446512)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.36/3.99 % (3446512)CaDiCaL version: 2.1.3 % 26.36/3.99 % (3446512)Termination reason: Instruction limit % 26.36/3.99 % (3446512)Termination phase: Saturation % 26.36/3.99 % (3446512)Time elapsed: 0.049 s % 26.36/3.99 % (3446512)Peak memory usage: 12 MB % 26.36/3.99 % (3446512)Instructions burned: 181 (million) % 26.36/3.99 % TRYING [6] % 26.36/3.99 % (3446516)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1234037771:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 26.36/3.99 % TRYING [1] % 26.36/3.99 % TRYING [2] % 26.36/3.99 % TRYING [3] % 26.36/3.99 % TRYING [4] % 26.36/3.99 % TRYING [5] % 26.36/3.99 % (3446506)Instruction limit reached! % 26.36/3.99 % (3446506)------------------------------ % 26.36/3.99 % (3446506)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 26.36/3.99 % (3446506)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.36/3.99 % (3446506)CaDiCaL version: 2.1.3 % 26.36/3.99 % (3446506)Termination reason: Instruction limit % 26.36/3.99 % (3446506)Termination phase: Finite model building SAT solving % 26.36/3.99 % (3446506)Time elapsed: 0.177 s % 26.36/3.99 % (3446506)Peak memory usage: 30 MB % 26.36/3.99 % (3446506)Instructions burned: 716 (million) % 26.36/3.99 % TRYING [6] % 26.36/3.99 % (3446518)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=280303343:i=1179_2997 on theBenchmark for (2997ds/1179Mi) % 26.36/3.99 % (3446514)Instruction limit reached! % 26.36/3.99 % (3446514)------------------------------ % 26.36/3.99 % (3446514)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 26.36/3.99 % (3446514)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.36/3.99 % (3446514)CaDiCaL version: 2.1.3 % 26.36/3.99 % (3446514)Termination reason: Instruction limit % 26.36/3.99 % (3446514)Termination phase: Saturation % 26.36/3.99 % (3446514)Time elapsed: 0.143 s % 26.36/3.99 % (3446514)Peak memory usage: 15 MB % 26.36/3.99 % (3446514)Instructions burned: 480 (million) % 26.36/3.99 % TRYING [8] % 26.36/3.99 % (3446508)Instruction limit reached! % 26.36/3.99 % (3446508)------------------------------ % 26.36/3.99 % (3446508)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 26.36/3.99 % (3446508)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.36/3.99 % (3446508)CaDiCaL version: 2.1.3 % 26.36/3.99 % (3446508)Termination reason: Instruction limit % 26.36/3.99 % (3446508)Termination phase: Saturation % 26.36/3.99 % (3446508)Time elapsed: 0.202 s % 26.36/3.99 % (3446508)Peak memory usage: 17 MB % 26.36/3.99 % (3446508)Instructions burned: 690 (million) % 26.36/3.99 % (3446520)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=528877862:i=889:ins=1_2997 on theBenchmark for (2997ds/889Mi) % 26.36/3.99 % (3446521)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=1584067710:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2997 on theBenchmark for (2997ds/692Mi) % 26.36/3.99 % (3446516)Instruction limit reached! % 26.36/3.99 % (3446516)------------------------------ % 26.36/3.99 % (3446516)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 26.36/3.99 % (3446516)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.36/3.99 % (3446516)CaDiCaL version: 2.1.3 % 26.36/3.99 % (3446516)Termination reason: Instruction limit % 26.36/3.99 % (3446516)Termination phase: Finite model building SAT solving % 26.36/3.99 % (3446516)Time elapsed: 0.181 s % 26.36/3.99 % (3446516)Peak memory usage: 24 MB % 26.36/3.99 % (3446516)Instructions burned: 867 (million) % 26.36/3.99 % (3446524)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=256653574:i=879:kws=inv_precedence:fsr=off_2996 on theBenchmark for (2996ds/879Mi) % 56.13/8.13 % TRYING [14] % 56.13/8.13 % (3446520)Instruction limit reached! % 56.13/8.13 % (3446520)------------------------------ % 56.13/8.13 % (3446520)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 56.13/8.13 % (3446520)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 56.13/8.13 % (3446520)CaDiCaL version: 2.1.3 % 56.13/8.13 % (3446520)Termination reason: Instruction limit % 56.13/8.13 % (3446520)Termination phase: Finite model building constraint generation % 56.13/8.13 % (3446520)Time elapsed: 0.191 s % 56.13/8.13 % (3446520)Peak memory usage: 81 MB % 56.13/8.13 % (3446520)Instructions burned: 889 (million) % 56.13/8.13 % (3446526)fmb+10_1_sil=64000:random_seed=3640342576:i=22061:nm=2:gsp=on_2995 on theBenchmark for (2995ds/22061Mi) % 56.13/8.13 % TRYING [1] % 56.13/8.13 % TRYING [2] % 56.13/8.13 % TRYING [3] % 56.13/8.13 % (3446521)Instruction limit reached! % 56.13/8.13 % (3446521)------------------------------ % 56.13/8.13 % (3446521)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 56.13/8.13 % (3446521)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 56.13/8.13 % (3446521)CaDiCaL version: 2.1.3 % 56.13/8.13 % (3446521)Termination reason: Instruction limit % 56.13/8.13 % (3446521)Termination phase: Saturation % 56.13/8.13 % (3446521)Time elapsed: 0.210 s % 56.13/8.13 % (3446521)Peak memory usage: 20 MB % 56.13/8.13 % (3446521)Instructions burned: 694 (million) % 56.13/8.13 % TRYING [4] % 56.13/8.13 % (3446528)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2874639935:i=9515:nm=5_2994 on theBenchmark for (2994ds/9515Mi) % 56.13/8.13 % TRYING [20] % 56.13/8.13 % TRYING [5] % 56.13/8.13 % TRYING [6] % 56.13/8.13 % (3446524)Instruction limit reached! % 56.13/8.13 % (3446524)------------------------------ % 56.13/8.13 % (3446524)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 56.13/8.13 % (3446524)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 56.13/8.13 % (3446524)CaDiCaL version: 2.1.3 % 56.13/8.13 % (3446524)Termination reason: Instruction limit % 56.13/8.13 % (3446524)Termination phase: Saturation % 56.13/8.13 % (3446524)Time elapsed: 0.259 s % 56.13/8.13 % (3446524)Peak memory usage: 18 MB % 56.13/8.13 % (3446524)Instructions burned: 879 (million) % 56.13/8.13 % TRYING [9] % 56.13/8.13 % (3446530)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3856824091:fmbsr=1.7:i=920_2993 on theBenchmark for (2993ds/920Mi) % 56.13/8.13 % TRYING [8] % 56.13/8.13 % (3446518)Instruction limit reached! % 56.13/8.13 % (3446518)------------------------------ % 56.13/8.13 % (3446518)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 56.13/8.13 % (3446518)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 56.13/8.13 % (3446518)CaDiCaL version: 2.1.3 % 56.13/8.13 % (3446518)Termination reason: Instruction limit % 56.13/8.13 % (3446518)Termination phase: Saturation % 56.13/8.13 % (3446518)Time elapsed: 0.359 s % 56.13/8.13 % (3446518)Peak memory usage: 20 MB % 56.13/8.13 % (3446518)Instructions burned: 1180 (million) % 56.13/8.13 % (3446532)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2344108219:i=5131_2993 on theBenchmark for (2993ds/5131Mi) % 56.13/8.13 % TRYING [7] % 56.13/8.13 % (3446530)Instruction limit reached! % 56.13/8.13 % (3446530)------------------------------ % 56.13/8.13 % (3446530)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 56.13/8.13 % (3446530)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 56.13/8.13 % (3446530)CaDiCaL version: 2.1.3 % 56.13/8.13 % (3446530)Termination reason: Instruction limit % 56.13/8.13 % (3446530)Termination phase: Finite model building SAT solving % 56.13/8.13 % (3446530)Time elapsed: 0.199 s % 56.13/8.13 % (3446530)Peak memory usage: 66 MB % 56.13/8.13 % (3446530)Instructions burned: 921 (million) % 56.13/8.13 % (3446534)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=4183365477:i=1472:ins=7:fdi=8:gsp=on_2991 on theBenchmark for (2991ds/1472Mi) % 56.13/8.13 % TRYING [8] % 56.13/8.13 % (3446534)Instruction limit reached! % 56.13/8.13 % (3446534)------------------------------ % 56.13/8.13 % (3446534)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 56.13/8.13 % (3446534)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 56.13/8.13 % (3446534)CaDiCaL version: 2.1.3 % 56.13/8.13 % (3446534)Termination reason: Instruction limit % 56.13/8.13 % (3446534)Termination phase: Saturation % 56.13/8.13 % (3446534)Time elapsed: 0.424 s % 56.13/8.13 % (3446534)Peak memory usage: 28 MB % 56.13/8.13 % (3446534)Instructions burned: 1476 (million) % 56.13/8.13 % (3446536)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3566354377:i=6324_2987 on theBenchmark for (2987ds/6324Mi) % 154.87/22.15 % TRYING [77] % 154.87/22.15 % TRYING [10] % 154.87/22.15 % (3446532)Instruction limit reached! % 154.87/22.15 % (3446532)------------------------------ % 154.87/22.15 % (3446532)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 154.87/22.15 % (3446532)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 154.87/22.15 % (3446532)CaDiCaL version: 2.1.3 % 154.87/22.15 % (3446532)Termination reason: Instruction limit % 154.87/22.15 % (3446532)Termination phase: Saturation % 154.87/22.15 % (3446532)Time elapsed: 1.456 s % 154.87/22.15 % (3446532)Peak memory usage: 39 MB % 154.87/22.15 % (3446532)Instructions burned: 5133 (million) % 154.87/22.15 % (3446538)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1585900964:fmbsr=2.30978:i=2174_2979 on theBenchmark for (2979ds/2174Mi) % 154.87/22.15 % TRYING [16] % 154.87/22.15 % TRYING [9] % 154.87/22.15 % (3446528)Instruction limit reached! % 154.87/22.15 % (3446528)------------------------------ % 154.87/22.15 % (3446528)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 154.87/22.15 % (3446528)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 154.87/22.15 % (3446528)CaDiCaL version: 2.1.3 % 154.87/22.15 % (3446528)Termination reason: Instruction limit % 154.87/22.15 % (3446528)Termination phase: Finite model building constraint generation % 154.87/22.15 % (3446528)Time elapsed: 1.938 s % 154.87/22.15 % (3446528)Peak memory usage: 667 MB % 154.87/22.15 % (3446528)Instructions burned: 9519 (million) % 154.87/22.15 % (3446538)Instruction limit reached! % 154.87/22.15 % (3446538)------------------------------ % 154.87/22.15 % (3446538)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 154.87/22.15 % (3446538)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 154.87/22.15 % (3446538)CaDiCaL version: 2.1.3 % 154.87/22.15 % (3446538)Termination reason: Instruction limit % 154.87/22.15 % (3446538)Termination phase: Finite model building constraint generation % 154.87/22.15 % (3446538)Time elapsed: 0.405 s % 154.87/22.15 % (3446538)Peak memory usage: 134 MB % 154.87/22.15 % (3446538)Instructions burned: 2179 (million) % 154.87/22.15 % (3446540)ott-2_1_sil=16000:newcnf=on:random_seed=4248418301:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2974 on theBenchmark for (2974ds/869Mi) % 154.87/22.15 % (3446542)ott+10_1_sil=32000:tgt=ground:random_seed=519958830:i=5114:av=off_2974 on theBenchmark for (2974ds/5114Mi) % 154.87/22.15 % (3446536)Instruction limit reached! % 154.87/22.15 % (3446536)------------------------------ % 154.87/22.15 % (3446536)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 154.87/22.15 % (3446536)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 154.87/22.15 % (3446536)CaDiCaL version: 2.1.3 % 154.87/22.15 % (3446536)Termination reason: Instruction limit % 154.87/22.15 % (3446536)Termination phase: Finite model building constraint generation % 154.87/22.15 % (3446536)Time elapsed: 1.294 s % 154.87/22.15 % (3446536)Peak memory usage: 523 MB % 154.87/22.15 % (3446536)Instructions burned: 6324 (million) % 154.87/22.15 % (3446544)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=1006008510:i=54282_2973 on theBenchmark for (2973ds/54282Mi) % 154.87/22.15 % TRYING [1] % 154.87/22.15 % TRYING [2] % 154.87/22.15 % TRYING [3] % 154.87/22.15 % TRYING [4] % 154.87/22.15 % TRYING [5] % 154.87/22.15 % TRYING [6] % 154.87/22.15 % TRYING [7] % 154.87/22.15 % (3446540)Instruction limit reached! % 154.87/22.15 % (3446540)------------------------------ % 154.87/22.15 % (3446540)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 154.87/22.15 % (3446540)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 154.87/22.15 % (3446540)CaDiCaL version: 2.1.3 % 154.87/22.15 % (3446540)Termination reason: Instruction limit % 154.87/22.15 % (3446540)Termination phase: Saturation % 154.87/22.15 % (3446540)Time elapsed: 0.264 s % 154.87/22.15 % (3446540)Peak memory usage: 20 MB % 154.87/22.15 % (3446540)Instructions burned: 871 (million) % 154.87/22.15 % (3446546)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=4059270078:i=3512:aac=none_2972 on theBenchmark for (2972ds/3512Mi) % 154.87/22.15 % TRYING [8] % 154.87/22.15 % TRYING [9] % 154.87/22.15 % TRYING [11] % 154.87/22.15 % (3446546)Instruction limit reached! % 154.87/22.15 % (3446546)------------------------------ % 154.87/22.15 % (3446546)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 154.87/22.15 % (3446546)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 154.87/22.15 % (3446546)CaDiCaL version: 2.1.3 % 154.87/22.15 % (3446546)Termination reason: Instruction limit % 154.87/22.15 % (3446546)Termination phase: Saturation % 154.87/22.15 % (3446546)Time elapsed: 1.047 s % 154.87/22.15 % (3446546)Peak memory usage: 36 MB % 204.25/29.18 % (3446546)Instructions burned: 3513 (million) % 204.25/29.18 % (3446548)dis+21_1_sil=32000:sas=cadical:random_seed=3709255085:i=3773:amm=off_2961 on theBenchmark for (2961ds/3773Mi) % 204.25/29.18 % TRYING [10] % 204.25/29.18 % (3446542)Instruction limit reached! % 204.25/29.18 % (3446542)------------------------------ % 204.25/29.18 % (3446542)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 204.25/29.18 % (3446542)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 204.25/29.18 % (3446542)CaDiCaL version: 2.1.3 % 204.25/29.18 % (3446542)Termination reason: Instruction limit % 204.25/29.18 % (3446542)Termination phase: Saturation % 204.25/29.18 % (3446542)Time elapsed: 1.624 s % 204.25/29.18 % (3446542)Peak memory usage: 46 MB % 204.25/29.18 % (3446542)Instructions burned: 5115 (million) % 204.25/29.18 % (3446550)ott+11_1_sil=16000:gs=on:random_seed=1687309006:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2958 on theBenchmark for (2958ds/2251Mi) % 204.25/29.18 % TRYING [10] % 204.25/29.18 % (3446550)Instruction limit reached! % 204.25/29.18 % (3446550)------------------------------ % 204.25/29.18 % (3446550)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 204.25/29.18 % (3446550)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 204.25/29.18 % (3446550)CaDiCaL version: 2.1.3 % 204.25/29.18 % (3446550)Termination reason: Instruction limit % 204.25/29.18 % (3446550)Termination phase: Saturation % 204.25/29.18 % (3446550)Time elapsed: 0.643 s % 204.25/29.18 % (3446550)Peak memory usage: 30 MB % 204.25/29.18 % (3446550)Instructions burned: 2253 (million) % 204.25/29.18 % (3446552)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=1039205673:fmbsr=1.6:i=67534_2951 on theBenchmark for (2951ds/67534Mi) % 204.25/29.18 % TRYING [7] % 204.25/29.18 % (3446548)Instruction limit reached! % 204.25/29.18 % (3446548)------------------------------ % 204.25/29.18 % (3446548)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 204.25/29.18 % (3446548)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 204.25/29.18 % (3446548)CaDiCaL version: 2.1.3 % 204.25/29.18 % (3446548)Termination reason: Instruction limit % 204.25/29.18 % (3446548)Termination phase: Saturation % 204.25/29.18 % (3446548)Time elapsed: 1.136 s % 204.25/29.18 % (3446548)Peak memory usage: 36 MB % 204.25/29.18 % (3446548)Instructions burned: 3776 (million) % 204.25/29.18 % (3446554)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=1131405065:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2949 on theBenchmark for (2949ds/4591Mi) % 204.25/29.18 % (3446526)Instruction limit reached! % 204.25/29.18 % (3446526)------------------------------ % 204.25/29.18 % (3446526)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 204.25/29.18 % (3446526)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 204.25/29.18 % (3446526)CaDiCaL version: 2.1.3 % 204.25/29.18 % (3446526)Termination reason: Instruction limit % 204.25/29.18 % (3446526)Termination phase: Finite model building SAT solving % 204.25/29.18 % (3446526)Time elapsed: 5.016 s % 204.25/29.18 % (3446526)Peak memory usage: 149 MB % 204.25/29.18 % (3446526)Instructions burned: 22063 (million) % 204.25/29.18 % (3446556)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=3164394722:i=29340_2944 on theBenchmark for (2944ds/29340Mi) % 204.25/29.18 % TRYING [8] % 204.25/29.18 % TRYING [11] % 204.25/29.18 % (3446554)Instruction limit reached! % 204.25/29.18 % (3446554)------------------------------ % 204.25/29.18 % (3446554)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 204.25/29.18 % (3446554)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 204.25/29.18 % (3446554)CaDiCaL version: 2.1.3 % 204.25/29.18 % (3446554)Termination reason: Instruction limit % 204.25/29.18 % (3446554)Termination phase: Saturation % 204.25/29.18 % (3446554)Time elapsed: 1.368 s % 204.25/29.18 % (3446554)Peak memory usage: 72 MB % 204.25/29.18 % (3446554)Instructions burned: 4592 (million) % 204.25/29.18 % (3446558)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=3645872651:i=5211_2936 on theBenchmark for (2936ds/5211Mi) % 204.25/29.18 % (3446558)Instruction limit reached! % 204.25/29.18 % (3446558)------------------------------ % 204.25/29.18 % (3446558)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 204.25/29.18 % (3446558)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 204.25/29.18 % (3446558)CaDiCaL version: 2.1.3 % 204.25/29.18 % (3446558)Termination reason: Instruction limit % 204.25/29.18 % (3446558)Termination phase: Saturation % 204.25/29.18 % (3446558)Time elapsed: 1.574 s % 204.25/29.18 % (3446558)Peak memory usage: 43 MB % 280.26/39.94 % (3446558)Instructions burned: 5211 (million) % 280.26/39.94 % (3446560)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=283627868:i=5497:nm=2_2920 on theBenchmark for (2920ds/5497Mi) % 280.26/39.94 % TRYING [17] % 280.26/39.94 % (3446560)Instruction limit reached! % 280.26/39.94 % (3446560)------------------------------ % 280.26/39.94 % (3446560)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 280.26/39.94 % (3446560)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 280.26/39.94 % (3446560)CaDiCaL version: 2.1.3 % 280.26/39.94 % (3446560)Termination reason: Instruction limit % 280.26/39.94 % (3446560)Termination phase: Finite model building constraint generation % 280.26/39.94 % (3446560)Time elapsed: 1.104 s % 280.26/39.94 % (3446560)Peak memory usage: 391 MB % 280.26/39.94 % (3446560)Instructions burned: 5498 (million) % 280.26/39.94 % (3446562)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=2929346440:fmbsr=2:i=46332_2908 on theBenchmark for (2908ds/46332Mi) % 280.26/39.94 % TRYING [15] % 280.26/39.94 % TRYING [9] % 280.26/39.94 % (3446556)Instruction limit reached! % 280.26/39.94 % (3446556)------------------------------ % 280.26/39.94 % (3446556)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 280.26/39.94 % (3446556)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 280.26/39.94 % (3446556)CaDiCaL version: 2.1.3 % 280.26/39.94 % (3446556)Termination reason: Instruction limit % 280.26/39.94 % (3446556)Termination phase: Saturation % 280.26/39.94 % (3446556)Time elapsed: 9.053 s % 280.26/39.94 % (3446556)Peak memory usage: 180 MB % 280.26/39.94 % (3446556)Instructions burned: 29342 (million) % 280.26/39.94 % (3446564)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=1895095549:i=14071_2853 on theBenchmark for (2853ds/14071Mi) % 280.26/39.94 % TRYING [12] % 280.26/39.94 % TRYING [12] % 280.26/39.94 % TRYING [12] % 280.26/39.94 % (3446494)Instruction limit reached! % 280.26/39.94 % (3446494)------------------------------ % 280.26/39.94 % (3446494)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 280.26/39.94 % (3446494)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 280.26/39.94 % (3446494)CaDiCaL version: 2.1.3 % 280.26/39.94 % (3446494)Termination reason: Instruction limit % 280.26/39.94 % (3446494)Termination phase: Saturation % 280.26/39.94 % (3446494)Time elapsed: 18.798 s % 280.26/39.94 % (3446494)Peak memory usage: 318 MB % 280.26/39.94 % (3446494)Instructions burned: 88029 (million) % 280.26/39.94 % (3446566)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3951810508:i=22565:add=on:rawr=on_2811 on theBenchmark for (2811ds/22565Mi) % 280.26/39.94 % (3446544)Instruction limit reached! % 280.26/39.94 % (3446544)------------------------------ % 280.26/39.94 % (3446544)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 280.26/39.94 % (3446544)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 280.26/39.94 % (3446544)CaDiCaL version: 2.1.3 % 280.26/39.94 % (3446544)Termination reason: Instruction limit % 280.26/39.94 % (3446544)Termination phase: Finite model building constraint generation % 280.26/39.94 % (3446544)Time elapsed: 16.715 s % 280.26/39.94 % (3446544)Peak memory usage: 389 MB % 280.26/39.94 % (3446544)Instructions burned: 54286 (million) % 280.26/39.94 % (3446568)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=3227607369:i=8173:av=off_2806 on theBenchmark for (2806ds/8173Mi) % 280.26/39.94 % (3446564)Instruction limit reached! % 280.26/39.94 % (3446564)------------------------------ % 280.26/39.94 % (3446564)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 280.26/39.94 % (3446564)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 280.26/39.94 % (3446564)CaDiCaL version: 2.1.3 % 280.26/39.94 % (3446564)Termination reason: Instruction limit % 280.26/39.94 % (3446564)Termination phase: Finite model building SAT solving % 280.26/39.94 % (3446564)Time elapsed: 5.031 s % 280.26/39.94 % (3446564)Peak memory usage: 572 MB % 280.26/39.94 % (3446564)Instructions burned: 14071 (million) % 280.26/39.94 % (3446570)dis+10_16:1_sil=16000:random_seed=3515406514:i=9155:fsr=off_2803 on theBenchmark for (2803ds/9155Mi) % 280.26/39.94 % (3446568)Instruction limit reached! % 280.26/39.94 % (3446568)------------------------------ % 280.26/39.94 % (3446568)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 280.26/39.94 % (3446568)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 280.26/39.94 % (3446568)CaDiCaL version: 2.1.3 % 280.26/39.94 % (3446568)Termination reason: Instruction limit % 280.26/39.94 % (3446568)Termination phase: SaturatTerminated % 300.02/42.73 % Vampire exiting %------------------------------------------------------------------------------