%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWC246-1 : TPTP v9.3.1. Released v2.4.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % Computer : n001.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:05:15 PM UTC 2026 % Result : Timeout 300.60s 42.64s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : SWC246-1 : TPTP v9.3.1. Released v2.4.0. % 0.00/0.04 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.06/0.17 % Computer : n001.cluster.edu % 0.06/0.17 % Model : x86_64 x86_64 % 0.06/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.06/0.17 % Memory : 8046.5625MB % 0.06/0.17 % OS : Linux 6.8.0-71-generic % 0.06/0.17 % CPULimit : 300 % 0.06/0.17 % WCLimit : 300 % 0.06/0.17 % DateTime : Mon Sep 28 08:45:17 UTC 2026 % 0.06/0.17 % CPUTime : % 0.06/0.17 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.06/0.20 Running first-order model finding % 0.06/0.20 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 % 26.10/3.94 % (222589)Will run a generic schedule for satisfiability detection. % 26.10/3.94 % (222598)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=41505542:i=116_2999 on theBenchmark for (2999ds/116Mi) % 26.10/3.94 % (222594)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1172724428_2999 on theBenchmark for (2999ds/0Mi) % 26.10/3.94 % (222597)dis+10_1_sil=32000:sp=arity:random_seed=1718970339:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 26.10/3.94 % (222596)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1472238815:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 26.10/3.94 % (222599)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3832735529:i=131_2999 on theBenchmark for (2999ds/131Mi) % 26.10/3.94 % (222600)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=876985371:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 26.10/3.94 % (222595)% WARNING: option uhcvi not known. % 26.10/3.94 % (222595)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2955046192:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 26.10/3.94 % TRYING [1] % 26.10/3.94 % TRYING [2] % 26.10/3.94 % TRYING [3] % 26.10/3.94 % (222598)Instruction limit reached! % 26.10/3.94 % (222598)------------------------------ % 26.10/3.94 % (222598)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 26.10/3.94 % (222598)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.10/3.94 % (222598)CaDiCaL version: 2.1.3 % 26.10/3.94 % (222598)Termination reason: Instruction limit % 26.10/3.94 % (222598)Termination phase: Saturation % 26.10/3.94 % (222598)Time elapsed: 0.033 s % 26.10/3.94 % (222598)Peak memory usage: 13 MB % 26.10/3.94 % (222598)Instructions burned: 117 (million) % 26.10/3.94 % TRYING [4] % 26.10/3.94 % (222608)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3833161227:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 26.10/3.94 % TRYING [1] % 26.10/3.94 % TRYING [2] % 26.10/3.94 % (222597)Instruction limit reached! % 26.10/3.94 % (222597)------------------------------ % 26.10/3.94 % (222597)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 26.10/3.94 % (222597)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.10/3.94 % (222597)CaDiCaL version: 2.1.3 % 26.10/3.94 % (222597)Termination reason: Instruction limit % 26.10/3.94 % (222597)Termination phase: Saturation % 26.10/3.94 % (222597)Time elapsed: 0.059 s % 26.10/3.94 % (222597)Peak memory usage: 13 MB % 26.10/3.94 % (222597)Instructions burned: 103 (million) % 26.10/3.94 % TRYING [3] % 26.10/3.94 % (222599)Instruction limit reached! % 26.10/3.94 % (222599)------------------------------ % 26.10/3.94 % (222599)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 26.10/3.94 % (222599)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.10/3.94 % (222599)CaDiCaL version: 2.1.3 % 26.10/3.94 % (222599)Termination reason: Instruction limit % 26.10/3.94 % (222599)Termination phase: Saturation % 26.10/3.94 % (222599)Time elapsed: 0.067 s % 26.10/3.94 % (222599)Peak memory usage: 14 MB % 26.10/3.94 % (222599)Instructions burned: 133 (million) % 26.10/3.94 % (222610)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1683483978:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 26.10/3.94 % TRYING [4] % 26.10/3.94 % (222611)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=3827298416:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi) % 26.10/3.94 % (222600)Instruction limit reached! % 26.10/3.94 % (222600)------------------------------ % 26.10/3.94 % (222600)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 26.10/3.94 % (222600)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.10/3.94 % (222600)CaDiCaL version: 2.1.3 % 26.10/3.94 % (222600)Termination reason: Instruction limit % 26.10/3.94 % (222600)Termination phase: Saturation % 26.10/3.94 % (222600)Time elapsed: 0.100 s % 26.10/3.94 % (222600)Peak memory usage: 14 MB % 26.10/3.94 % (222600)Instructions burned: 159 (million) % 26.10/3.94 % TRYING [5] % 26.10/3.94 % (222614)ott-21_1_sil=16000:fs=off:random_seed=2577771576:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 26.10/3.94 % TRYING [5] % 26.10/3.94 % (222610)Instruction limit reached! % 26.10/3.94 % (222610)------------------------------ % 26.10/3.94 % (222610)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 26.10/3.94 % (222610)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 45.24/6.65 % (222610)CaDiCaL version: 2.1.3 % 45.24/6.65 % (222610)Termination reason: Instruction limit % 45.24/6.65 % (222610)Termination phase: Saturation % 45.24/6.65 % (222610)Time elapsed: 0.071 s % 45.24/6.65 % (222610)Peak memory usage: 13 MB % 45.24/6.65 % (222610)Instructions burned: 131 (million) % 45.24/6.65 % (222616)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=53714802:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 45.24/6.65 % (222614)Instruction limit reached! % 45.24/6.65 % (222614)------------------------------ % 45.24/6.65 % (222614)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 45.24/6.65 % (222614)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 45.24/6.65 % (222614)CaDiCaL version: 2.1.3 % 45.24/6.65 % (222614)Termination reason: Instruction limit % 45.24/6.65 % (222614)Termination phase: Saturation % 45.24/6.65 % (222614)Time elapsed: 0.086 s % 45.24/6.65 % (222614)Peak memory usage: 13 MB % 45.24/6.65 % (222614)Instructions burned: 181 (million) % 45.24/6.65 % (222608)Instruction limit reached! % 45.24/6.65 % (222608)------------------------------ % 45.24/6.65 % (222608)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 45.24/6.65 % (222608)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 45.24/6.65 % (222608)CaDiCaL version: 2.1.3 % 45.24/6.65 % (222608)Termination reason: Instruction limit % 45.24/6.65 % (222608)Termination phase: Finite model building SAT solving % 45.24/6.65 % (222608)Time elapsed: 0.169 s % 45.24/6.65 % (222608)Peak memory usage: 37 MB % 45.24/6.65 % (222608)Instructions burned: 715 (million) % 45.24/6.65 % (222619)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=485782383:i=1179_2997 on theBenchmark for (2997ds/1179Mi) % 45.24/6.65 % (222618)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=951446748:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi) % 45.24/6.65 % TRYING [1] % 45.24/6.65 % TRYING [2] % 45.24/6.65 % TRYING [3] % 45.24/6.65 % TRYING [6] % 45.24/6.65 % TRYING [4] % 45.24/6.65 % TRYING [5] % 45.24/6.65 % (222616)Instruction limit reached! % 45.24/6.65 % (222616)------------------------------ % 45.24/6.65 % (222616)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 45.24/6.65 % (222616)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 45.24/6.65 % (222616)CaDiCaL version: 2.1.3 % 45.24/6.65 % (222616)Termination reason: Instruction limit % 45.24/6.65 % (222616)Termination phase: Saturation % 45.24/6.65 % (222616)Time elapsed: 0.303 s % 45.24/6.65 % (222616)Peak memory usage: 14 MB % 45.24/6.65 % (222616)Instructions burned: 479 (million) % 45.24/6.65 % (222611)Instruction limit reached! % 45.24/6.65 % (222611)------------------------------ % 45.24/6.65 % (222611)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 45.24/6.65 % (222611)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 45.24/6.65 % (222611)CaDiCaL version: 2.1.3 % 45.24/6.65 % (222611)Termination reason: Instruction limit % 45.24/6.65 % (222611)Termination phase: Saturation % 45.24/6.65 % (222611)Time elapsed: 0.401 s % 45.24/6.65 % (222611)Peak memory usage: 19 MB % 45.24/6.65 % (222611)Instructions burned: 686 (million) % 45.24/6.65 % (222622)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2656997410:i=889:ins=1_2994 on theBenchmark for (2994ds/889Mi) % 45.24/6.65 % (222623)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=1795525582:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2994 on theBenchmark for (2994ds/692Mi) % 45.24/6.65 % (222618)Instruction limit reached! % 45.24/6.65 % (222618)------------------------------ % 45.24/6.65 % (222618)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 45.24/6.65 % (222618)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 45.24/6.65 % (222618)CaDiCaL version: 2.1.3 % 45.24/6.65 % (222618)Termination reason: Instruction limit % 45.24/6.65 % (222618)Termination phase: Finite model building SAT solving % 45.24/6.65 % (222618)Time elapsed: 0.338 s % 45.24/6.65 % (222618)Peak memory usage: 24 MB % 45.24/6.65 % (222618)Instructions burned: 866 (million) % 45.24/6.65 % (222626)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1134345502:i=879:kws=inv_precedence:fsr=off_2993 on theBenchmark for (2993ds/879Mi) % 45.24/6.65 % (222619)Instruction limit reached! % 45.24/6.65 % (222619)------------------------------ % 45.24/6.65 % (222619)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 73.62/10.62 % (222619)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 73.62/10.62 % (222619)CaDiCaL version: 2.1.3 % 73.62/10.62 % (222619)Termination reason: Instruction limit % 73.62/10.62 % (222619)Termination phase: Saturation % 73.62/10.62 % (222619)Time elapsed: 0.363 s % 73.62/10.62 % (222619)Peak memory usage: 27 MB % 73.62/10.62 % (222619)Instructions burned: 1181 (million) % 73.62/10.62 % (222628)fmb+10_1_sil=64000:random_seed=3490300373:i=22061:nm=2:gsp=on_2993 on theBenchmark for (2993ds/22061Mi) % 73.62/10.62 % TRYING [1] % 73.62/10.62 % TRYING [2] % 73.62/10.62 % TRYING [3] % 73.62/10.62 % TRYING [14] % 73.62/10.62 % TRYING [4] % 73.62/10.62 % TRYING [7] % 73.62/10.62 % TRYING [5] % 73.62/10.62 % (222622)Instruction limit reached! % 73.62/10.62 % (222622)------------------------------ % 73.62/10.62 % (222622)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 73.62/10.62 % (222622)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 73.62/10.62 % (222622)CaDiCaL version: 2.1.3 % 73.62/10.62 % (222622)Termination reason: Instruction limit % 73.62/10.62 % (222622)Termination phase: Finite model building constraint generation % 73.62/10.62 % (222622)Time elapsed: 0.336 s % 73.62/10.62 % (222622)Peak memory usage: 77 MB % 73.62/10.62 % (222622)Instructions burned: 891 (million) % 73.62/10.62 % (222630)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3194110756:i=9515:nm=5_2991 on theBenchmark for (2991ds/9515Mi) % 73.62/10.62 % (222623)Instruction limit reached! % 73.62/10.62 % (222623)------------------------------ % 73.62/10.62 % (222623)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 73.62/10.62 % (222623)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 73.62/10.62 % (222623)CaDiCaL version: 2.1.3 % 73.62/10.62 % (222623)Termination reason: Instruction limit % 73.62/10.62 % (222623)Termination phase: Saturation % 73.62/10.62 % (222623)Time elapsed: 0.356 s % 73.62/10.62 % (222623)Peak memory usage: 19 MB % 73.62/10.62 % (222623)Instructions burned: 693 (million) % 73.62/10.62 % TRYING [20] % 73.62/10.62 % (222632)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2182233346:fmbsr=1.7:i=920_2990 on theBenchmark for (2990ds/920Mi) % 73.62/10.62 % TRYING [8] % 73.62/10.62 % TRYING [6] % 73.62/10.62 % (222626)Instruction limit reached! % 73.62/10.62 % (222626)------------------------------ % 73.62/10.62 % (222626)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 73.62/10.62 % (222626)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 73.62/10.62 % (222626)CaDiCaL version: 2.1.3 % 73.62/10.62 % (222626)Termination reason: Instruction limit % 73.62/10.62 % (222626)Termination phase: Saturation % 73.62/10.62 % (222626)Time elapsed: 0.464 s % 73.62/10.62 % (222626)Peak memory usage: 21 MB % 73.62/10.62 % (222626)Instructions burned: 880 (million) % 73.62/10.62 % (222634)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=404884942:i=5131_2989 on theBenchmark for (2989ds/5131Mi) % 73.62/10.62 % (222632)Instruction limit reached! % 73.62/10.62 % (222632)------------------------------ % 73.62/10.62 % (222632)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 73.62/10.62 % (222632)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 73.62/10.62 % (222632)CaDiCaL version: 2.1.3 % 73.62/10.62 % (222632)Termination reason: Instruction limit % 73.62/10.62 % (222632)Termination phase: Finite model building constraint generation % 73.62/10.62 % (222632)Time elapsed: 0.328 s % 73.62/10.62 % (222632)Peak memory usage: 77 MB % 73.62/10.62 % (222632)Instructions burned: 921 (million) % 73.62/10.62 % (222636)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3651676549:i=1472:ins=7:fdi=8:gsp=on_2987 on theBenchmark for (2987ds/1472Mi) % 73.62/10.62 % TRYING [7] % 73.62/10.62 % TRYING [8] % 73.62/10.62 % (222636)Instruction limit reached! % 73.62/10.62 % (222636)------------------------------ % 73.62/10.62 % (222636)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 73.62/10.62 % (222636)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 73.62/10.62 % (222636)CaDiCaL version: 2.1.3 % 73.62/10.62 % (222636)Termination reason: Instruction limit % 73.62/10.62 % (222636)Termination phase: Saturation % 73.62/10.62 % (222636)Time elapsed: 0.663 s % 73.62/10.62 % (222636)Peak memory usage: 15 MB % 73.62/10.62 % (222636)Instructions burned: 1474 (million) % 73.62/10.62 % (222638)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3585406588:i=6324_2980 on theBenchmark for (2980ds/6324Mi) % 73.62/10.62 % TRYING [77] % 73.62/10.62 % TRYING [8] % 73.62/10.62 % (222634)Instruction limit reached! % 73.62/10.62 % (222634)------------------------------ % 73.62/10.62 % (222634)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 226.84/32.23 % (222634)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 226.84/32.23 % (222634)CaDiCaL version: 2.1.3 % 226.84/32.23 % (222634)Termination reason: Instruction limit % 226.84/32.23 % (222634)Termination phase: Saturation % 226.84/32.23 % (222634)Time elapsed: 2.612 s % 226.84/32.23 % (222634)Peak memory usage: 53 MB % 226.84/32.23 % (222634)Instructions burned: 5131 (million) % 226.84/32.23 % (222640)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1854555167:fmbsr=2.30978:i=2174_2962 on theBenchmark for (2962ds/2174Mi) % 226.84/32.23 % TRYING [16] % 226.84/32.23 % TRYING [9] % 226.84/32.23 % (222630)Instruction limit reached! % 226.84/32.23 % (222630)------------------------------ % 226.84/32.23 % (222630)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 226.84/32.23 % (222630)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 226.84/32.23 % (222630)CaDiCaL version: 2.1.3 % 226.84/32.23 % (222630)Termination reason: Instruction limit % 226.84/32.23 % (222630)Termination phase: Finite model building constraint generation % 226.84/32.23 % (222630)Time elapsed: 3.284 s % 226.84/32.23 % (222630)Peak memory usage: 593 MB % 226.84/32.23 % (222630)Instructions burned: 9517 (million) % 226.84/32.23 % (222642)ott-2_1_sil=16000:newcnf=on:random_seed=1553521916:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2957 on theBenchmark for (2957ds/869Mi) % 226.84/32.23 % (222638)Instruction limit reached! % 226.84/32.23 % (222638)------------------------------ % 226.84/32.23 % (222638)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 226.84/32.23 % (222638)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 226.84/32.23 % (222638)CaDiCaL version: 2.1.3 % 226.84/32.23 % (222638)Termination reason: Instruction limit % 226.84/32.23 % (222638)Termination phase: Finite model building constraint generation % 226.84/32.23 % (222638)Time elapsed: 2.405 s % 226.84/32.23 % (222638)Peak memory usage: 524 MB % 226.84/32.23 % (222638)Instructions burned: 6325 (million) % 226.84/32.23 % (222644)ott+10_1_sil=32000:tgt=ground:random_seed=3448027130:i=5114:av=off_2955 on theBenchmark for (2955ds/5114Mi) % 226.84/32.23 % (222640)Instruction limit reached! % 226.84/32.23 % (222640)------------------------------ % 226.84/32.23 % (222640)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 226.84/32.23 % (222640)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 226.84/32.23 % (222640)CaDiCaL version: 2.1.3 % 226.84/32.23 % (222640)Termination reason: Instruction limit % 226.84/32.23 % (222640)Termination phase: Finite model building constraint generation % 226.84/32.23 % (222640)Time elapsed: 0.755 s % 226.84/32.23 % (222640)Peak memory usage: 129 MB % 226.84/32.23 % (222640)Instructions burned: 2176 (million) % 226.84/32.23 % (222646)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=4115271080:i=54282_2954 on theBenchmark for (2954ds/54282Mi) % 226.84/32.23 % TRYING [1] % 226.84/32.23 % TRYING [2] % 226.84/32.23 % TRYING [3] % 226.84/32.23 % TRYING [4] % 226.84/32.23 % TRYING [5] % 226.84/32.23 % (222642)Instruction limit reached! % 226.84/32.23 % (222642)------------------------------ % 226.84/32.23 % (222642)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 226.84/32.23 % (222642)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 226.84/32.23 % (222642)CaDiCaL version: 2.1.3 % 226.84/32.23 % (222642)Termination reason: Instruction limit % 226.84/32.23 % (222642)Termination phase: Saturation % 226.84/32.23 % (222642)Time elapsed: 0.480 s % 226.84/32.23 % (222642)Peak memory usage: 21 MB % 226.84/32.23 % (222642)Instructions burned: 871 (million) % 226.84/32.23 % (222648)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=2047864747:i=3512:aac=none_2952 on theBenchmark for (2952ds/3512Mi) % 226.84/32.23 % TRYING [6] % 226.84/32.23 % TRYING [9] % 226.84/32.23 % TRYING [7] % 226.84/32.23 % (222628)Instruction limit reached! % 226.84/32.23 % (222628)------------------------------ % 226.84/32.23 % (222628)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 226.84/32.23 % (222628)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 226.84/32.23 % (222628)CaDiCaL version: 2.1.3 % 226.84/32.23 % (222628)Termination reason: Instruction limit % 226.84/32.23 % (222628)Termination phase: Finite model building constraint generation % 226.84/32.23 % (222628)Time elapsed: 4.712 s % 226.84/32.23 % (222628)Peak memory usage: 172 MB % 226.84/32.23 % (222628)Instructions burned: 22062 (million) % 226.84/32.23 % (222650)dis+21_1_sil=32000:sas=cadical:random_seed=631439532:i=3773:amm=off_2946 on theBenchmark for (2946ds/3773Mi) % 226.84/32.23 % TRYING [8] % 226.84/32.23 % (222650)Instruction limit reached! % 226.84/32.23 % (222650)------------------------------ % 226.84/32.23 % (222650)Version: VampTerminated % 300.60/42.64 % Vampire exiting % 300.60/42.64 Terminated %------------------------------------------------------------------------------