%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWX220-1 : TPTP v9.3.1. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % Computer : n017.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:46 PM UTC 2026 % Result : Timeout 300.71s 42.63s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWX220-1 : TPTP v9.3.1. Released v9.3.0. % 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.10/0.19 % Computer : n017.cluster.edu % 0.10/0.19 % Model : x86_64 x86_64 % 0.10/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.19 % Memory : 8046.5625MB % 0.10/0.19 % OS : Linux 6.8.0-71-generic % 0.10/0.19 % CPULimit : 300 % 0.10/0.19 % WCLimit : 300 % 0.10/0.19 % DateTime : Mon Sep 28 15:08:21 UTC 2026 % 0.10/0.19 % CPUTime : % 0.10/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.10/0.22 Running first-order model finding % 0.10/0.22 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 % 16.77/2.60 % (3622662)Will run a generic schedule for satisfiability detection. % 16.77/2.60 % (3622668)% WARNING: option uhcvi not known. % 16.77/2.60 % (3622668)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=983970245:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 16.77/2.60 % (3622667)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=114299443_2999 on theBenchmark for (2999ds/0Mi) % 16.77/2.60 % (3622670)dis+10_1_sil=32000:sp=arity:random_seed=2872505221:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 16.77/2.60 % (3622669)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1009866355:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 16.77/2.60 % (3622671)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2005509953:i=116_2999 on theBenchmark for (2999ds/116Mi) % 16.77/2.60 % (3622673)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2825190491:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 16.77/2.60 % (3622672)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2905633999:i=131_2999 on theBenchmark for (2999ds/131Mi) % 16.77/2.60 % TRYING [1] % 16.77/2.60 % TRYING [2] % 16.77/2.60 % TRYING [3] % 16.77/2.60 % TRYING [4] % 16.77/2.60 % (3622670)Instruction limit reached! % 16.77/2.60 % (3622670)------------------------------ % 16.77/2.60 % (3622670)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 16.77/2.60 % (3622670)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.77/2.60 % (3622670)CaDiCaL version: 2.1.3 % 16.77/2.60 % (3622670)Termination reason: Instruction limit % 16.77/2.60 % (3622670)Termination phase: Saturation % 16.77/2.60 % (3622670)Time elapsed: 0.058 s % 16.77/2.60 % (3622670)Peak memory usage: 12 MB % 16.77/2.60 % (3622670)Instructions burned: 104 (million) % 16.77/2.60 % (3622671)Instruction limit reached! % 16.77/2.60 % (3622671)------------------------------ % 16.77/2.60 % (3622671)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 16.77/2.60 % (3622671)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.77/2.60 % (3622671)CaDiCaL version: 2.1.3 % 16.77/2.60 % (3622671)Termination reason: Instruction limit % 16.77/2.60 % (3622671)Termination phase: Saturation % 16.77/2.60 % (3622671)Time elapsed: 0.068 s % 16.77/2.60 % (3622671)Peak memory usage: 13 MB % 16.77/2.60 % (3622671)Instructions burned: 117 (million) % 16.77/2.60 % (3622672)Instruction limit reached! % 16.77/2.60 % (3622672)------------------------------ % 16.77/2.60 % (3622672)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 16.77/2.60 % (3622672)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.77/2.60 % (3622672)CaDiCaL version: 2.1.3 % 16.77/2.60 % (3622672)Termination reason: Instruction limit % 16.77/2.60 % (3622672)Termination phase: Saturation % 16.77/2.60 % (3622672)Time elapsed: 0.074 s % 16.77/2.60 % (3622672)Peak memory usage: 12 MB % 16.77/2.60 % (3622672)Instructions burned: 132 (million) % 16.77/2.60 % (3622681)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=246525651:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 16.77/2.60 % TRYING [1] % 16.77/2.60 % TRYING [2] % 16.77/2.60 % (3622682)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3056465951:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi) % 16.77/2.60 % TRYING [3] % 16.77/2.60 % (3622673)Instruction limit reached! % 16.77/2.60 % (3622673)------------------------------ % 16.77/2.60 % (3622673)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 16.77/2.60 % (3622673)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.77/2.60 % (3622673)CaDiCaL version: 2.1.3 % 16.77/2.60 % (3622673)Termination reason: Instruction limit % 16.77/2.60 % (3622673)Termination phase: Saturation % 16.77/2.60 % (3622673)Time elapsed: 0.091 s % 16.77/2.60 % (3622673)Peak memory usage: 13 MB % 16.77/2.60 % (3622673)Instructions burned: 160 (million) % 16.77/2.60 % (3622683)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=2788105446:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi) % 16.77/2.60 % TRYING [5] % 16.77/2.60 % (3622686)ott-21_1_sil=16000:fs=off:random_seed=2616812740:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 16.77/2.60 % TRYING [4] % 16.77/2.60 % (3622682)Instruction limit reached! % 16.77/2.60 % (3622682)------------------------------ % 16.77/2.60 % (3622682)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 43.74/6.45 % (3622682)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 43.74/6.45 % (3622682)CaDiCaL version: 2.1.3 % 43.74/6.45 % (3622682)Termination reason: Instruction limit % 43.74/6.45 % (3622682)Termination phase: Saturation % 43.74/6.45 % (3622682)Time elapsed: 0.077 s % 43.74/6.45 % (3622682)Peak memory usage: 13 MB % 43.74/6.45 % (3622682)Instructions burned: 132 (million) % 43.74/6.45 % (3622689)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2780309582:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi) % 43.74/6.45 % (3622686)Instruction limit reached! % 43.74/6.45 % (3622686)------------------------------ % 43.74/6.45 % (3622686)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 43.74/6.45 % (3622686)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 43.74/6.45 % (3622686)CaDiCaL version: 2.1.3 % 43.74/6.45 % (3622686)Termination reason: Instruction limit % 43.74/6.45 % (3622686)Termination phase: Saturation % 43.74/6.45 % (3622686)Time elapsed: 0.093 s % 43.74/6.45 % (3622686)Peak memory usage: 13 MB % 43.74/6.45 % (3622686)Instructions burned: 181 (million) % 43.74/6.45 % (3622691)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3404855852:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi) % 43.74/6.45 % TRYING [1] % 43.74/6.45 % TRYING [2] % 43.74/6.45 % TRYING [3] % 43.74/6.45 % TRYING [4] % 43.74/6.45 % TRYING [6] % 43.74/6.45 % (3622681)Instruction limit reached! % 43.74/6.45 % (3622681)------------------------------ % 43.74/6.45 % (3622681)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 43.74/6.45 % (3622681)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 43.74/6.45 % (3622681)CaDiCaL version: 2.1.3 % 43.74/6.45 % (3622681)Termination reason: Instruction limit % 43.74/6.45 % (3622681)Termination phase: Finite model building SAT solving % 43.74/6.45 % (3622681)Time elapsed: 0.361 s % 43.74/6.45 % (3622681)Peak memory usage: 33 MB % 43.74/6.45 % (3622681)Instructions burned: 715 (million) % 43.74/6.45 % (3622683)Instruction limit reached! % 43.74/6.45 % (3622683)------------------------------ % 43.74/6.45 % (3622683)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 43.74/6.45 % (3622683)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 43.74/6.45 % (3622683)CaDiCaL version: 2.1.3 % 43.74/6.45 % (3622683)Termination reason: Instruction limit % 43.74/6.45 % (3622683)Termination phase: Saturation % 43.74/6.45 % (3622683)Time elapsed: 0.352 s % 43.74/6.45 % (3622683)Peak memory usage: 17 MB % 43.74/6.45 % (3622683)Instructions burned: 686 (million) % 43.74/6.45 % (3622689)Instruction limit reached! % 43.74/6.45 % (3622689)------------------------------ % 43.74/6.45 % (3622689)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 43.74/6.45 % (3622689)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 43.74/6.45 % (3622689)CaDiCaL version: 2.1.3 % 43.74/6.45 % (3622689)Termination reason: Instruction limit % 43.74/6.45 % (3622689)Termination phase: Saturation % 43.74/6.45 % (3622689)Time elapsed: 0.269 s % 43.74/6.45 % (3622689)Peak memory usage: 16 MB % 43.74/6.45 % (3622689)Instructions burned: 480 (million) % 43.74/6.45 % (3622693)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1253206922:i=1179_2995 on theBenchmark for (2995ds/1179Mi) % 43.74/6.45 % (3622694)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1412194249:i=889:ins=1_2995 on theBenchmark for (2995ds/889Mi) % 43.74/6.45 % (3622695)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=1687743511:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2995 on theBenchmark for (2995ds/692Mi) % 43.74/6.45 % TRYING [5] % 43.74/6.45 % (3622691)Instruction limit reached! % 43.74/6.45 % (3622691)------------------------------ % 43.74/6.45 % (3622691)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 43.74/6.45 % (3622691)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 43.74/6.45 % (3622691)CaDiCaL version: 2.1.3 % 43.74/6.45 % (3622691)Termination reason: Instruction limit % 43.74/6.45 % (3622691)Termination phase: Finite model building constraint generation % 43.74/6.45 % (3622691)Time elapsed: 0.330 s % 43.74/6.45 % (3622691)Peak memory usage: 24 MB % 43.74/6.45 % (3622691)Instructions burned: 865 (million) % 43.74/6.45 % (3622699)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2170720593:i=879:kws=inv_precedence:fsr=off_2994 on theBenchmark for (2994ds/879Mi) % 43.74/6.45 % (3622695)Instruction limit reached! % 43.74/6.45 % (3622695)------------------------------ % 89.85/13.00 % (3622695)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 89.85/13.00 % (3622695)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 89.85/13.00 % (3622695)CaDiCaL version: 2.1.3 % 89.85/13.00 % (3622695)Termination reason: Instruction limit % 89.85/13.00 % (3622695)Termination phase: Saturation % 89.85/13.00 % (3622695)Time elapsed: 0.375 s % 89.85/13.00 % (3622695)Peak memory usage: 18 MB % 89.85/13.00 % (3622695)Instructions burned: 693 (million) % 89.85/13.00 % (3622701)fmb+10_1_sil=64000:random_seed=2566804371:i=22061:nm=2:gsp=on_2991 on theBenchmark for (2991ds/22061Mi) % 89.85/13.00 % (3622694)Instruction limit reached! % 89.85/13.00 % (3622694)------------------------------ % 89.85/13.00 % (3622694)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 89.85/13.00 % (3622694)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 89.85/13.00 % (3622694)CaDiCaL version: 2.1.3 % 89.85/13.00 % (3622694)Termination reason: Instruction limit % 89.85/13.00 % (3622694)Termination phase: Finite model building constraint generation % 89.85/13.00 % (3622694)Time elapsed: 0.408 s % 89.85/13.00 % (3622694)Peak memory usage: 107 MB % 89.85/13.00 % (3622694)Instructions burned: 891 (million) % 89.85/13.00 % TRYING [1] % 89.85/13.00 % TRYING [2] % 89.85/13.00 % TRYING [3] % 89.85/13.00 % (3622703)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2447119383:i=9515:nm=5_2990 on theBenchmark for (2990ds/9515Mi) % 89.85/13.00 % TRYING [20] % 89.85/13.00 % TRYING [4] % 89.85/13.00 % (3622699)Instruction limit reached! % 89.85/13.00 % (3622699)------------------------------ % 89.85/13.00 % (3622699)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 89.85/13.00 % (3622699)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 89.85/13.00 % (3622699)CaDiCaL version: 2.1.3 % 89.85/13.00 % (3622699)Termination reason: Instruction limit % 89.85/13.00 % (3622699)Termination phase: Saturation % 89.85/13.00 % (3622699)Time elapsed: 0.457 s % 89.85/13.00 % (3622699)Peak memory usage: 20 MB % 89.85/13.00 % (3622699)Instructions burned: 879 (million) % 89.85/13.00 % (3622705)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3155582990:fmbsr=1.7:i=920_2989 on theBenchmark for (2989ds/920Mi) % 89.85/13.00 % TRYING [8] % 89.85/13.00 % (3622693)Instruction limit reached! % 89.85/13.00 % (3622693)------------------------------ % 89.85/13.00 % (3622693)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 89.85/13.00 % (3622693)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 89.85/13.00 % (3622693)CaDiCaL version: 2.1.3 % 89.85/13.00 % (3622693)Termination reason: Instruction limit % 89.85/13.00 % (3622693)Termination phase: Saturation % 89.85/13.00 % (3622693)Time elapsed: 0.648 s % 89.85/13.00 % (3622693)Peak memory usage: 23 MB % 89.85/13.00 % (3622693)Instructions burned: 1179 (million) % 89.85/13.00 % (3622707)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2326603892:i=5131_2988 on theBenchmark for (2988ds/5131Mi) % 89.85/13.00 % TRYING [7] % 89.85/13.00 % TRYING [5] % 89.85/13.00 % (3622705)Instruction limit reached! % 89.85/13.00 % (3622705)------------------------------ % 89.85/13.00 % (3622705)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 89.85/13.00 % (3622705)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 89.85/13.00 % (3622705)CaDiCaL version: 2.1.3 % 89.85/13.00 % (3622705)Termination reason: Instruction limit % 89.85/13.00 % (3622705)Termination phase: Finite model building constraint generation % 89.85/13.00 % (3622705)Time elapsed: 0.334 s % 89.85/13.00 % (3622705)Peak memory usage: 73 MB % 89.85/13.00 % (3622705)Instructions burned: 922 (million) % 89.85/13.00 % (3622710)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2546657209:i=1472:ins=7:fdi=8:gsp=on_2985 on theBenchmark for (2985ds/1472Mi) % 89.85/13.00 % TRYING [6] % 89.85/13.00 % (3622710)Instruction limit reached! % 89.85/13.00 % (3622710)------------------------------ % 89.85/13.00 % (3622710)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 89.85/13.00 % (3622710)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 89.85/13.00 % (3622710)CaDiCaL version: 2.1.3 % 89.85/13.00 % (3622710)Termination reason: Instruction limit % 89.85/13.00 % (3622710)Termination phase: Saturation % 89.85/13.00 % (3622710)Time elapsed: 0.887 s % 89.85/13.00 % (3622710)Peak memory usage: 31 MB % 89.85/13.00 % (3622710)Instructions burned: 1473 (million) % 89.85/13.00 % (3622712)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=2315470709:i=6324_2976 on theBenchmark for (2976ds/6324Mi) % 89.85/13.00 % (3622712)Cannot represent all propositional literals internally % 238.87/34.05 % (3622712)Refutation not found, incomplete strategy % 238.87/34.05 % (3622712)------------------------------ % 238.87/34.05 % (3622712)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 238.87/34.05 % (3622712)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 238.87/34.05 % (3622712)CaDiCaL version: 2.1.3 % 238.87/34.05 % (3622712)Termination reason: Refutation not found, incomplete strategy % 238.87/34.05 % (3622712)Time elapsed: 0.006 s % 238.87/34.05 % (3622712)Peak memory usage: 10 MB % 238.87/34.05 % (3622712)Instructions burned: 10 (million) % 238.87/34.05 % (3622712)------------------------------ % 238.87/34.05 % (3622712)------------------------------ % 238.87/34.05 % (3622714)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=3371394736:fmbsr=2.30978:i=2174_2976 on theBenchmark for (2976ds/2174Mi) % 238.87/34.05 % TRYING [16] % 238.87/34.05 % (3622714)Instruction limit reached! % 238.87/34.05 % (3622714)------------------------------ % 238.87/34.05 % (3622714)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 238.87/34.05 % (3622714)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 238.87/34.05 % (3622714)CaDiCaL version: 2.1.3 % 238.87/34.05 % (3622714)Termination reason: Instruction limit % 238.87/34.05 % (3622714)Termination phase: Finite model building constraint generation % 238.87/34.05 % (3622714)Time elapsed: 0.742 s % 238.87/34.05 % (3622714)Peak memory usage: 134 MB % 238.87/34.05 % (3622714)Instructions burned: 2175 (million) % 238.87/34.05 % (3622716)ott-2_1_sil=16000:newcnf=on:random_seed=2820649848:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2968 on theBenchmark for (2968ds/869Mi) % 238.87/34.05 % TRYING [8] % 238.87/34.05 % (3622716)Instruction limit reached! % 238.87/34.05 % (3622716)------------------------------ % 238.87/34.05 % (3622716)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 238.87/34.05 % (3622716)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 238.87/34.05 % (3622716)CaDiCaL version: 2.1.3 % 238.87/34.05 % (3622716)Termination reason: Instruction limit % 238.87/34.05 % (3622716)Termination phase: Saturation % 238.87/34.05 % (3622716)Time elapsed: 0.496 s % 238.87/34.05 % (3622716)Peak memory usage: 24 MB % 238.87/34.05 % (3622716)Instructions burned: 871 (million) % 238.87/34.05 % (3622718)ott+10_1_sil=32000:tgt=ground:random_seed=89367658:i=5114:av=off_2963 on theBenchmark for (2963ds/5114Mi) % 238.87/34.05 % (3622707)Instruction limit reached! % 238.87/34.05 % (3622707)------------------------------ % 238.87/34.05 % (3622707)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 238.87/34.05 % (3622707)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 238.87/34.05 % (3622707)CaDiCaL version: 2.1.3 % 238.87/34.05 % (3622707)Termination reason: Instruction limit % 238.87/34.05 % (3622707)Termination phase: Saturation % 238.87/34.05 % (3622707)Time elapsed: 2.554 s % 238.87/34.05 % (3622707)Peak memory usage: 60 MB % 238.87/34.05 % (3622707)Instructions burned: 5132 (million) % 238.87/34.05 % (3622720)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=1308585809:i=54282_2962 on theBenchmark for (2962ds/54282Mi) % 238.87/34.05 % TRYING [1] % 238.87/34.05 % TRYING [2] % 238.87/34.05 % TRYING [3] % 238.87/34.05 % TRYING [4] % 238.87/34.05 % TRYING [5] % 238.87/34.05 % TRYING [6] % 238.87/34.05 % (3622703)Instruction limit reached! % 238.87/34.05 % (3622703)------------------------------ % 238.87/34.05 % (3622703)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 238.87/34.05 % (3622703)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 238.87/34.05 % (3622703)CaDiCaL version: 2.1.3 % 238.87/34.05 % (3622703)Termination reason: Instruction limit % 238.87/34.05 % (3622703)Termination phase: Finite model building constraint generation % 238.87/34.05 % (3622703)Time elapsed: 3.428 s % 238.87/34.05 % (3622703)Peak memory usage: 665 MB % 238.87/34.05 % (3622703)Instructions burned: 9518 (million) % 238.87/34.05 % (3622722)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=1099607319:i=3512:aac=none_2955 on theBenchmark for (2955ds/3512Mi) % 238.87/34.05 % TRYING [7] % 238.87/34.05 % TRYING [7] % 238.87/34.05 % (3622722)Instruction limit reached! % 238.87/34.05 % (3622722)------------------------------ % 238.87/34.05 % (3622722)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 238.87/34.05 % (3622722)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 238.87/34.05 % (3622722)CaDiCaL version: 2.1.3 % 238.87/34.05 % (3622722)Termination reason: Instruction limit % 238.87/34.05 % (3622722)Termination phase: Saturation % 238.87/34.05 % (3622722)Time elapsed: 1.746 s % 238.87/34.05 % (3622722)Peak memory usage: 46 MB % 238.87/34.05 % (3622722)Instructions burned: 3514 (million) % 300.71/42.63 % (3622724)dis+21_1_sil=32000:sas=cadical:random_seed=20813122:i=3773:amm=off_2937 on theBenchmark for (2937ds/3773Mi) % 300.71/42.63 % (3622718)Instruction limit reached! % 300.71/42.63 % (3622718)------------------------------ % 300.71/42.63 % (3622718)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.71/42.63 % (3622718)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.71/42.63 % (3622718)CaDiCaL version: 2.1.3 % 300.71/42.63 % (3622718)Termination reason: Instruction limit % 300.71/42.63 % (3622718)Termination phase: Saturation % 300.71/42.63 % (3622718)Time elapsed: 2.734 s % 300.71/42.63 % (3622718)Peak memory usage: 76 MB % 300.71/42.63 % (3622718)Instructions burned: 5115 (million) % 300.71/42.63 % (3622726)ott+11_1_sil=16000:gs=on:random_seed=1777599930:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2935 on theBenchmark for (2935ds/2251Mi) % 300.71/42.63 % TRYING [8] % 300.71/42.63 % (3622726)Instruction limit reached! % 300.71/42.63 % (3622726)------------------------------ % 300.71/42.63 % (3622726)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.71/42.63 % (3622726)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.71/42.64 % (3622726)CaDiCaL version: 2.1.3 % 300.71/42.64 % (3622726)Termination reason: Instruction limit % 300.71/42.64 % (3622726)Termination phase: Saturation % 300.71/42.64 % (3622726)Time elapsed: 1.088 s % 300.71/42.64 % (3622726)Peak memory usage: 27 MB % 300.71/42.64 % (3622726)Instructions burned: 2251 (million) % 300.71/42.64 % (3622728)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=3418081763:fmbsr=1.6:i=67534_2924 on theBenchmark for (2924ds/67534Mi) % 300.71/42.64 % TRYING [7] % 300.71/42.64 % TRYING [9] % 300.71/42.64 % (3622724)Instruction limit reached! % 300.71/42.64 % (3622724)------------------------------ % 300.71/42.64 % (3622724)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.71/42.64 % (3622724)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.71/42.64 % (3622724)CaDiCaL version: 2.1.3 % 300.71/42.64 % (3622724)Termination reason: Instruction limit % 300.71/42.64 % (3622724)Termination phase: Saturation % 300.71/42.64 % (3622724)Time elapsed: 1.890 s % 300.71/42.64 % (3622724)Peak memory usage: 50 MB % 300.71/42.64 % (3622724)Instructions burned: 3773 (million) % 300.71/42.64 % (3622730)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=699542539:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2918 on theBenchmark for (2918ds/4591Mi) % 300.71/42.64 % (3622701)Instruction limit reached! % 300.71/42.64 % (3622701)------------------------------ % 300.71/42.64 % (3622701)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.71/42.64 % (3622701)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.71/42.64 % (3622701)CaDiCaL version: 2.1.3 % 300.71/42.64 % (3622701)Termination reason: Instruction limit % 300.71/42.64 % (3622701)Termination phase: Finite model building SAT solving % 300.71/42.64 % (3622701)Time elapsed: 8.309 s % 300.71/42.64 % (3622701)Peak memory usage: 265 MB % 300.71/42.64 % (3622701)Instructions burned: 22063 (million) % 300.71/42.64 % (3622732)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=2548356713:i=29340_2907 on theBenchmark for (2907ds/29340Mi) % 300.71/42.64 % (3622730)Instruction limit reached! % 300.71/42.64 % (3622730)------------------------------ % 300.71/42.64 % (3622730)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.71/42.64 % (3622730)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.71/42.64 % (3622730)CaDiCaL version: 2.1.3 % 300.71/42.64 % (3622730)Termination reason: Instruction limit % 300.71/42.64 % (3622730)Termination phase: Saturation % 300.71/42.64 % (3622730)Time elapsed: 1.951 s % 300.71/42.64 % (3622730)Peak memory usage: 35 MB % 300.71/42.64 % (3622730)Instructions burned: 4592 (million) % 300.71/42.64 % (3622734)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=3081201204:i=5211_2898 on theBenchmark for (2898ds/5211Mi) % 300.71/42.64 % TRYING [9] % 300.71/42.64 % (3622734)Instruction limit reached! % 300.71/42.64 % (3622734)------------------------------ % 300.71/42.64 % (3622734)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.71/42.64 % (3622734)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.71/42.64 % (3622734)CaDiCaL version: 2.1.3 % 300.71/42.64 % (3622734)Termination reason: Instruction limit % 300.71/42.64 % (3622734)Termination phase: Saturation % 300.71/42.64 % (3622734)Time elapsed: 2.631 s % 300.71/42.64 % (3622734)Peak memory usage: 63 MB % 300.71/42.64 % (3622734)Instruction % 300.71/42.64 Terminated % 300.71/42.64 % Vampire exiting % 300.71/42.64 Terminated %------------------------------------------------------------------------------