%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWV575-1 : TPTP v9.3.1. Released v4.1.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % Computer : n016.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:26:03 PM UTC 2026 % Result : Timeout 296.42s 42.04s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : SWV575-1 : TPTP v9.3.1. Released v4.1.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.07/0.17 % Computer : n016.cluster.edu % 0.07/0.17 % Model : x86_64 x86_64 % 0.07/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.07/0.17 % Memory : 8046.5625MB % 0.07/0.17 % OS : Linux 6.8.0-71-generic % 0.07/0.17 % CPULimit : 300 % 0.07/0.17 % WCLimit : 300 % 0.07/0.17 % DateTime : Mon Sep 28 11:59:33 UTC 2026 % 0.07/0.18 % CPUTime : % 0.07/0.18 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.07/0.21 Running first-order model finding % 0.07/0.21 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 % 9.55/1.73 % (3581658)Will run a generic schedule for satisfiability detection. % 9.55/1.73 % (3581669)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3794705270:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 9.55/1.73 % (3581664)% WARNING: option uhcvi not known. % 9.55/1.73 % (3581663)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2723378399_2999 on theBenchmark for (2999ds/0Mi) % 9.55/1.73 % (3581667)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2778646835:i=116_2999 on theBenchmark for (2999ds/116Mi) % 9.55/1.73 % (3581664)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1224804563:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 9.55/1.73 % (3581665)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1295031663:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 9.55/1.73 % (3581666)dis+10_1_sil=32000:sp=arity:random_seed=1641083951:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 9.55/1.73 % (3581668)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=359382263:i=131_2999 on theBenchmark for (2999ds/131Mi) % 9.55/1.73 % (3581669)Instruction limit reached! % 9.55/1.73 % (3581669)------------------------------ % 9.55/1.73 % (3581669)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 9.55/1.73 % (3581669)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.55/1.73 % (3581669)CaDiCaL version: 2.1.3 % 9.55/1.73 % (3581669)Termination reason: Instruction limit % 9.55/1.73 % (3581669)Termination phase: Saturation % 9.55/1.73 % (3581669)Time elapsed: 0.058 s % 9.55/1.73 % (3581669)Peak memory usage: 16 MB % 9.55/1.73 % (3581669)Instructions burned: 160 (million) % 9.55/1.73 % (3581677)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3369433375:i=714:nm=2_2998 on theBenchmark for (2998ds/714Mi) % 9.55/1.73 % (3581666)Instruction limit reached! % 9.55/1.73 % (3581666)------------------------------ % 9.55/1.73 % (3581666)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 9.55/1.73 % (3581666)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.55/1.73 % (3581666)CaDiCaL version: 2.1.3 % 9.55/1.73 % (3581666)Termination reason: Instruction limit % 9.55/1.73 % (3581666)Termination phase: Saturation % 9.55/1.73 % (3581666)Time elapsed: 0.067 s % 9.55/1.73 % (3581666)Peak memory usage: 14 MB % 9.55/1.73 % (3581666)Instructions burned: 103 (million) % 9.55/1.73 % (3581667)Instruction limit reached! % 9.55/1.73 % (3581667)------------------------------ % 9.55/1.73 % (3581667)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 9.55/1.73 % (3581667)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.55/1.73 % (3581667)CaDiCaL version: 2.1.3 % 9.55/1.73 % (3581667)Termination reason: Instruction limit % 9.55/1.73 % (3581667)Termination phase: Saturation % 9.55/1.73 % (3581667)Time elapsed: 0.073 s % 9.55/1.73 % (3581667)Peak memory usage: 15 MB % 9.55/1.73 % (3581667)Instructions burned: 117 (million) % 9.55/1.73 % (3581668)Instruction limit reached! % 9.55/1.73 % (3581668)------------------------------ % 9.55/1.73 % (3581668)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 9.55/1.73 % (3581668)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.55/1.73 % (3581668)CaDiCaL version: 2.1.3 % 9.55/1.73 % (3581668)Termination reason: Instruction limit % 9.55/1.73 % (3581668)Termination phase: Saturation % 9.55/1.73 % (3581668)Time elapsed: 0.081 s % 9.55/1.73 % (3581668)Peak memory usage: 15 MB % 9.55/1.73 % (3581668)Instructions burned: 131 (million) % 9.55/1.73 % (3581679)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2179479379:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi) % 9.55/1.73 % (3581680)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=2921476398:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi) % 9.55/1.73 % (3581681)ott-21_1_sil=16000:fs=off:random_seed=695601556:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 9.55/1.73 % (3581679)Instruction limit reached! % 9.55/1.73 % (3581679)------------------------------ % 9.55/1.73 % (3581679)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 9.55/1.73 % (3581679)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.55/1.73 % (3581679)CaDiCaL version: 2.1.3 % 34.72/5.15 % (3581679)Termination reason: Instruction limit % 34.72/5.15 % (3581679)Termination phase: Saturation % 34.72/5.15 % (3581679)Time elapsed: 0.079 s % 34.72/5.15 % (3581679)Peak memory usage: 14 MB % 34.72/5.15 % (3581679)Instructions burned: 132 (million) % 34.72/5.15 % (3581685)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2770079575:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi) % 34.72/5.15 % (3581681)Instruction limit reached! % 34.72/5.15 % (3581681)------------------------------ % 34.72/5.15 % (3581681)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 34.72/5.15 % (3581681)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.72/5.15 % (3581681)CaDiCaL version: 2.1.3 % 34.72/5.15 % (3581681)Termination reason: Instruction limit % 34.72/5.15 % (3581681)Termination phase: Saturation % 34.72/5.15 % (3581681)Time elapsed: 0.096 s % 34.72/5.15 % (3581681)Peak memory usage: 14 MB % 34.72/5.15 % (3581681)Instructions burned: 181 (million) % 34.72/5.15 % (3581687)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1090377:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi) % 34.72/5.15 % TRYING [1] % 34.72/5.15 % TRYING [2] % 34.72/5.15 % (3581677)Instruction limit reached! % 34.72/5.15 % (3581677)------------------------------ % 34.72/5.15 % (3581677)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 34.72/5.15 % (3581677)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.72/5.15 % (3581677)CaDiCaL version: 2.1.3 % 34.72/5.15 % (3581677)Termination reason: Instruction limit % 34.72/5.15 % (3581677)Termination phase: Finite model building constraint generation % 34.72/5.15 % (3581677)Time elapsed: 0.184 s % 34.72/5.15 % (3581677)Peak memory usage: 26 MB % 34.72/5.15 % (3581677)Instructions burned: 719 (million) % 34.72/5.15 % (3581689)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=992946272:i=1179_2996 on theBenchmark for (2996ds/1179Mi) % 34.72/5.15 % TRYING [1] % 34.72/5.15 % TRYING [2] % 34.72/5.15 % TRYING [3] % 34.72/5.15 % (3581680)Instruction limit reached! % 34.72/5.15 % (3581680)------------------------------ % 34.72/5.15 % (3581680)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 34.72/5.15 % (3581680)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.72/5.15 % (3581680)CaDiCaL version: 2.1.3 % 34.72/5.15 % (3581680)Termination reason: Instruction limit % 34.72/5.15 % (3581680)Termination phase: Saturation % 34.72/5.15 % (3581680)Time elapsed: 0.411 s % 34.72/5.15 % (3581680)Peak memory usage: 18 MB % 34.72/5.15 % (3581680)Instructions burned: 684 (million) % 34.72/5.15 % (3581685)Instruction limit reached! % 34.72/5.15 % (3581685)------------------------------ % 34.72/5.15 % (3581685)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 34.72/5.15 % (3581685)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.72/5.15 % (3581685)CaDiCaL version: 2.1.3 % 34.72/5.15 % (3581685)Termination reason: Instruction limit % 34.72/5.15 % (3581685)Termination phase: Saturation % 34.72/5.15 % (3581685)Time elapsed: 0.325 s % 34.72/5.15 % (3581685)Peak memory usage: 15 MB % 34.72/5.15 % (3581685)Instructions burned: 478 (million) % 34.72/5.15 % (3581691)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3638757634:i=889:ins=1_2994 on theBenchmark for (2994ds/889Mi) % 34.72/5.15 % (3581692)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=1354143042: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) % 34.72/5.15 % (3581689)Instruction limit reached! % 34.72/5.15 % (3581689)------------------------------ % 34.72/5.15 % (3581689)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 34.72/5.15 % (3581689)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.72/5.15 % (3581689)CaDiCaL version: 2.1.3 % 34.72/5.15 % (3581689)Termination reason: Instruction limit % 34.72/5.15 % (3581689)Termination phase: Saturation % 34.72/5.15 % (3581689)Time elapsed: 0.389 s % 34.72/5.15 % (3581689)Peak memory usage: 22 MB % 34.72/5.15 % (3581689)Instructions burned: 1182 (million) % 34.72/5.15 % (3581687)Instruction limit reached! % 34.72/5.15 % (3581687)------------------------------ % 34.72/5.15 % (3581687)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 34.72/5.15 % (3581687)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.72/5.15 % (3581687)CaDiCaL version: 2.1.3 % 34.72/5.15 % (3581687)Termination reason: Instruction limit % 34.72/5.15 % (3581687)Termination phase: Finite model building preprocessing % 93.73/13.56 % (3581687)Time elapsed: 0.440 s % 93.73/13.56 % (3581687)Peak memory usage: 27 MB % 93.73/13.56 % (3581687)Instructions burned: 865 (million) % 93.73/13.56 % (3581695)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2863880064:i=879:kws=inv_precedence:fsr=off_2992 on theBenchmark for (2992ds/879Mi) % 93.73/13.56 % (3581697)fmb+10_1_sil=64000:random_seed=3509940060:i=22061:nm=2:gsp=on_2992 on theBenchmark for (2992ds/22061Mi) % 93.73/13.56 % (3581695)Instruction limit reached! % 93.73/13.56 % (3581695)------------------------------ % 93.73/13.56 % (3581695)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 93.73/13.56 % (3581695)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 93.73/13.56 % (3581695)CaDiCaL version: 2.1.3 % 93.73/13.56 % (3581695)Termination reason: Instruction limit % 93.73/13.56 % (3581695)Termination phase: Saturation % 93.73/13.56 % (3581695)Time elapsed: 0.258 s % 93.73/13.56 % (3581695)Peak memory usage: 21 MB % 93.73/13.56 % (3581695)Instructions burned: 882 (million) % 93.73/13.56 % (3581699)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1895819185:i=9515:nm=5_2990 on theBenchmark for (2990ds/9515Mi) % 93.73/13.56 % (3581691)Instruction limit reached! % 93.73/13.56 % (3581691)------------------------------ % 93.73/13.56 % (3581691)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 93.73/13.56 % (3581691)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 93.73/13.56 % (3581691)CaDiCaL version: 2.1.3 % 93.73/13.56 % (3581691)Termination reason: Instruction limit % 93.73/13.56 % (3581691)Termination phase: Finite model building constraint generation % 93.73/13.56 % (3581691)Time elapsed: 0.429 s % 93.73/13.56 % (3581691)Peak memory usage: 53 MB % 93.73/13.56 % (3581691)Instructions burned: 889 (million) % 93.73/13.56 % (3581692)Instruction limit reached! % 93.73/13.56 % (3581692)------------------------------ % 93.73/13.56 % (3581692)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 93.73/13.56 % (3581692)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 93.73/13.56 % (3581692)CaDiCaL version: 2.1.3 % 93.73/13.56 % (3581692)Termination reason: Instruction limit % 93.73/13.56 % (3581692)Termination phase: Saturation % 93.73/13.56 % (3581692)Time elapsed: 0.444 s % 93.73/13.56 % (3581692)Peak memory usage: 20 MB % 93.73/13.56 % (3581692)Instructions burned: 693 (million) % 93.73/13.56 % (3581701)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2207613227:fmbsr=1.7:i=920_2989 on theBenchmark for (2989ds/920Mi) % 93.73/13.56 % TRYING [1] % 93.73/13.56 % (3581702)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=3793094807:i=5131_2989 on theBenchmark for (2989ds/5131Mi) % 93.73/13.56 % TRYING [2] % 93.73/13.56 % (3581699)Cannot represent all propositional literals internally % 93.73/13.56 % (3581699)Refutation not found, incomplete strategy % 93.73/13.56 % (3581699)------------------------------ % 93.73/13.56 % (3581699)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 93.73/13.56 % (3581699)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 93.73/13.56 % (3581699)CaDiCaL version: 2.1.3 % 93.73/13.56 % (3581699)Termination reason: Refutation not found, incomplete strategy % 93.73/13.56 % (3581699)Time elapsed: 0.161 s % 93.73/13.56 % (3581699)Peak memory usage: 23 MB % 93.73/13.56 % (3581699)Instructions burned: 601 (million) % 93.73/13.56 % (3581699)------------------------------ % 93.73/13.56 % (3581699)------------------------------ % 93.73/13.56 % (3581705)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2111052471:i=1472:ins=7:fdi=8:gsp=on_2988 on theBenchmark for (2988ds/1472Mi) % 93.73/13.56 % TRYING [8] % 93.73/13.56 % (3581701)Instruction limit reached! % 93.73/13.56 % (3581701)------------------------------ % 93.73/13.56 % (3581701)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 93.73/13.56 % (3581701)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 93.73/13.56 % (3581701)CaDiCaL version: 2.1.3 % 93.73/13.56 % (3581701)Termination reason: Instruction limit % 93.73/13.56 % (3581701)Termination phase: Finite model building constraint generation % 93.73/13.56 % (3581701)Time elapsed: 0.411 s % 93.73/13.56 % (3581701)Peak memory usage: 43 MB % 93.73/13.56 % (3581701)Instructions burned: 920 (million) % 93.73/13.56 % (3581707)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=966133762:i=6324_2985 on theBenchmark for (2985ds/6324Mi) % 93.73/13.56 % (3581705)Instruction limit reached! % 93.73/13.56 % (3581705)------------------------------ % 93.73/13.56 % (3581705)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 198.26/28.22 % (3581705)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 198.26/28.22 % (3581705)CaDiCaL version: 2.1.3 % 198.26/28.22 % (3581705)Termination reason: Instruction limit % 198.26/28.22 % (3581705)Termination phase: Saturation % 198.26/28.22 % (3581705)Time elapsed: 0.351 s % 198.26/28.22 % (3581705)Peak memory usage: 24 MB % 198.26/28.22 % (3581705)Instructions burned: 1475 (million) % 198.26/28.22 % (3581709)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=797111448:fmbsr=2.30978:i=2174_2984 on theBenchmark for (2984ds/2174Mi) % 198.26/28.22 % TRYING [4] % 198.26/28.22 % (3581707)Cannot represent all propositional literals internally % 198.26/28.22 % (3581707)Refutation not found, incomplete strategy % 198.26/28.22 % (3581707)------------------------------ % 198.26/28.22 % (3581707)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 198.26/28.22 % (3581707)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 198.26/28.22 % (3581707)CaDiCaL version: 2.1.3 % 198.26/28.22 % (3581707)Termination reason: Refutation not found, incomplete strategy % 198.26/28.22 % (3581707)Time elapsed: 0.314 s % 198.26/28.22 % (3581707)Peak memory usage: 23 MB % 198.26/28.22 % (3581707)Instructions burned: 631 (million) % 198.26/28.22 % (3581707)------------------------------ % 198.26/28.22 % (3581707)------------------------------ % 198.26/28.22 % (3581711)ott-2_1_sil=16000:newcnf=on:random_seed=558641638:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2982 on theBenchmark for (2982ds/869Mi) % 198.26/28.22 % TRYING [3] % 198.26/28.22 % (3581709)Instruction limit reached! % 198.26/28.22 % (3581709)------------------------------ % 198.26/28.22 % (3581709)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 198.26/28.22 % (3581709)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 198.26/28.22 % (3581709)CaDiCaL version: 2.1.3 % 198.26/28.22 % (3581709)Termination reason: Instruction limit % 198.26/28.22 % (3581709)Termination phase: Finite model building preprocessing % 198.26/28.22 % (3581709)Time elapsed: 0.573 s % 198.26/28.22 % (3581709)Peak memory usage: 35 MB % 198.26/28.22 % (3581709)Instructions burned: 2176 (million) % 198.26/28.22 % (3581713)ott+10_1_sil=32000:tgt=ground:random_seed=3865431671:i=5114:av=off_2978 on theBenchmark for (2978ds/5114Mi) % 198.26/28.22 % (3581711)Instruction limit reached! % 198.26/28.22 % (3581711)------------------------------ % 198.26/28.22 % (3581711)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 198.26/28.22 % (3581711)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 198.26/28.22 % (3581711)CaDiCaL version: 2.1.3 % 198.26/28.22 % (3581711)Termination reason: Instruction limit % 198.26/28.22 % (3581711)Termination phase: Saturation % 198.26/28.22 % (3581711)Time elapsed: 0.462 s % 198.26/28.22 % (3581711)Peak memory usage: 18 MB % 198.26/28.22 % (3581711)Instructions burned: 869 (million) % 198.26/28.22 % (3581715)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=810859354:i=54282_2977 on theBenchmark for (2977ds/54282Mi) % 198.26/28.22 % TRYING [1] % 198.26/28.22 % TRYING [2] % 198.26/28.22 % TRYING [3] % 198.26/28.22 % (3581713)Instruction limit reached! % 198.26/28.22 % (3581713)------------------------------ % 198.26/28.22 % (3581713)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 198.26/28.22 % (3581713)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 198.26/28.22 % (3581713)CaDiCaL version: 2.1.3 % 198.26/28.22 % (3581713)Termination reason: Instruction limit % 198.26/28.22 % (3581713)Termination phase: Saturation % 198.26/28.22 % (3581713)Time elapsed: 1.681 s % 198.26/28.22 % (3581713)Peak memory usage: 36 MB % 198.26/28.22 % (3581713)Instructions burned: 5115 (million) % 198.26/28.22 % (3581717)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=530606102:i=3512:aac=none_2961 on theBenchmark for (2961ds/3512Mi) % 198.26/28.22 % TRYING [4] % 198.26/28.22 % (3581702)Instruction limit reached! % 198.26/28.22 % (3581702)------------------------------ % 198.26/28.22 % (3581702)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 198.26/28.22 % (3581702)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 198.26/28.22 % (3581702)CaDiCaL version: 2.1.3 % 198.26/28.22 % (3581702)Termination reason: Instruction limit % 198.26/28.22 % (3581702)Termination phase: Saturation % 198.26/28.22 % (3581702)Time elapsed: 2.964 s % 198.26/28.22 % (3581702)Peak memory usage: 34 MB % 198.26/28.22 % (3581702)Instructions burned: 5132 (million) % 198.26/28.22 % (3581719)dis+21_1_sil=32000:sas=cadical:random_seed=2007412007:i=3773:amm=off_2959 on theBenchmark for (2959ds/3773Mi) % 198.26/28.22 % (3581717)Instruction limit reached! % 296.42/42.04 % (3581717)------------------------------ % 296.42/42.04 % (3581717)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 296.42/42.04 % (3581717)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 296.42/42.04 % (3581717)CaDiCaL version: 2.1.3 % 296.42/42.04 % (3581717)Termination reason: Instruction limit % 296.42/42.04 % (3581717)Termination phase: Saturation % 296.42/42.04 % (3581717)Time elapsed: 1.122 s % 296.42/42.04 % (3581717)Peak memory usage: 31 MB % 296.42/42.04 % (3581717)Instructions burned: 3515 (million) % 296.42/42.04 % (3581721)ott+11_1_sil=16000:gs=on:random_seed=921325459:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2950 on theBenchmark for (2950ds/2251Mi) % 296.42/42.04 % (3581721)Instruction limit reached! % 296.42/42.04 % (3581721)------------------------------ % 296.42/42.04 % (3581721)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 296.42/42.04 % (3581721)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 296.42/42.04 % (3581721)CaDiCaL version: 2.1.3 % 296.42/42.04 % (3581721)Termination reason: Instruction limit % 296.42/42.04 % (3581721)Termination phase: Saturation % 296.42/42.04 % (3581721)Time elapsed: 0.640 s % 296.42/42.04 % (3581721)Peak memory usage: 22 MB % 296.42/42.04 % (3581721)Instructions burned: 2252 (million) % 296.42/42.04 % (3581723)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=295076100:fmbsr=1.6:i=67534_2944 on theBenchmark for (2944ds/67534Mi) % 296.42/42.04 % TRYING [5] % 296.42/42.04 % TRYING [4] % 296.42/42.04 % (3581719)Instruction limit reached! % 296.42/42.04 % (3581719)------------------------------ % 296.42/42.04 % (3581719)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 296.42/42.04 % (3581719)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 296.42/42.04 % (3581719)CaDiCaL version: 2.1.3 % 296.42/42.04 % (3581719)Termination reason: Instruction limit % 296.42/42.04 % (3581719)Termination phase: Saturation % 296.42/42.04 % (3581719)Time elapsed: 2.291 s % 296.42/42.04 % (3581719)Peak memory usage: 35 MB % 296.42/42.04 % (3581719)Instructions burned: 3774 (million) % 296.42/42.04 % (3581725)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=122525600:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2936 on theBenchmark for (2936ds/4591Mi) % 296.42/42.04 % TRYING [7] % 296.42/42.04 % TRYING [5] % 296.42/42.04 % (3581725)Instruction limit reached! % 296.42/42.04 % (3581725)------------------------------ % 296.42/42.04 % (3581725)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 296.42/42.04 % (3581725)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 296.42/42.04 % (3581725)CaDiCaL version: 2.1.3 % 296.42/42.04 % (3581725)Termination reason: Instruction limit % 296.42/42.04 % (3581725)Termination phase: Saturation % 296.42/42.04 % (3581725)Time elapsed: 2.148 s % 296.42/42.04 % (3581725)Peak memory usage: 48 MB % 296.42/42.04 % (3581725)Instructions burned: 4592 (million) % 296.42/42.04 % (3581727)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=3183550670:i=29340_2914 on theBenchmark for (2914ds/29340Mi) % 296.42/42.04 % (3581697)Instruction limit reached! % 296.42/42.04 % (3581697)------------------------------ % 296.42/42.04 % (3581697)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 296.42/42.04 % (3581697)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 296.42/42.04 % (3581697)CaDiCaL version: 2.1.3 % 296.42/42.04 % (3581697)Termination reason: Instruction limit % 296.42/42.04 % (3581697)Termination phase: Finite model building SAT solving % 296.42/42.04 % (3581697)Time elapsed: 9.470 s % 296.42/42.04 % (3581697)Peak memory usage: 529 MB % 296.42/42.04 % (3581697)Instructions burned: 22063 (million) % 296.42/42.04 % (3581729)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=2591785920:i=5211_2897 on theBenchmark for (2897ds/5211Mi) % 296.42/42.04 % (3581729)Instruction limit reached! % 296.42/42.04 % (3581729)------------------------------ % 296.42/42.04 % (3581729)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 296.42/42.04 % (3581729)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 296.42/42.04 % (3581729)CaDiCaL version: 2.1.3 % 296.42/42.04 % (3581729)Termination reason: Instruction limit % 296.42/42.04 % (3581729)Termination phase: Saturation % 296.42/42.04 % (3581729)Time elapsed: 2.706 s % 296.42/42.04 % (3581729)Peak memory usage: 44 MB % 296.42/42.04 % (3581729)Instructions burned: 5213 (million) % 296.42/42.04 % (3581731)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=2142564339:i=5497:nm=2_2869 on theBenchmark for (2869ds/5497Mi) % 296.42/42.04 % TRYING [17] % 300.45/42.73 % (3581731)Instruction limit reached! % 300.45/42.73 % (3581731)------------------------------ % 300.45/42.73 % (3581731)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.45/42.73 % (3581731)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.45/42.73 % (3581731)CaDiCaL version: 2.1.3 % 300.45/42.73 % (3581731)Termination reason: Instruction limit % 300.45/42.73 % (3581731)Termination phase: Finite model building constraint generation % 300.45/42.73 % (3581731)Time elapsed: 1.995 s % 300.45/42.73 % (3581731)Peak memory usage: 329 MB % 300.45/42.73 % (3581731)Instructions burned: 5498 (million) % 300.45/42.73 % (3581733)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=3770685746:fmbsr=2:i=46332_2849 on theBenchmark for (2849ds/46332Mi) % 300.45/42.73 % TRYING [15] % 300.45/42.73 % (3581723)Instruction limit reached! % 300.45/42.73 % (3581723)------------------------------ % 300.45/42.73 % (3581723)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.45/42.73 % (3581723)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.45/42.73 % (3581723)CaDiCaL version: 2.1.3 % 300.45/42.73 % (3581723)Termination reason: Instruction limit % 300.45/42.73 % (3581723)Termination phase: Finite model building constraint generation % 300.45/42.73 % (3581723)Time elapsed: 12.610 s % 300.45/42.73 % (3581723)Peak memory usage: 3658 MB % 300.45/42.73 % (3581723)Instructions burned: 67537 (million) % 300.45/42.73 % (3581735)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=4184806299:i=14071_2815 on theBenchmark for (2815ds/14071Mi) % 300.45/42.73 % TRYING [12] % 300.45/42.73 % TRYING [6] % 300.45/42.73 % (3581735)Instruction limit reached! % 300.45/42.73 % (3581735)------------------------------ % 300.45/42.73 % (3581735)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.45/42.73 % (3581735)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.45/42.73 % (3581735)CaDiCaL version: 2.1.3 % 300.45/42.73 % (3581735)Termination reason: Instruction limit % 300.45/42.73 % (3581735)Termination phase: Finite model building constraint generation % 300.45/42.73 % (3581735)Time elapsed: 2.741 s % 300.45/42.73 % (3581735)Peak memory usage: 858 MB % 300.45/42.73 % (3581735)Instructions burned: 14071 (million) % 300.45/42.73 % (3581737)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3801242248:i=22565:add=on:rawr=on_2786 on theBenchmark for (2786ds/22565Mi) % 300.45/42.73 % (3581727)Instruction limit reached! % 300.45/42.73 % (3581727)------------------------------ % 300.45/42.73 % (3581727)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.45/42.73 % (3581727)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.45/42.73 % (3581727)CaDiCaL version: 2.1.3 % 300.45/42.73 % (3581727)Termination reason: Instruction limit % 300.45/42.73 % (3581727)Termination phase: Saturation % 300.45/42.73 % (3581727)Time elapsed: 14.058 s % 300.45/42.73 % (3581727)Peak memory usage: 116 MB % 300.45/42.73 % (3581727)Instructions burned: 29342 (million) % 300.45/42.73 % (3581739)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=1935947333:i=8173:av=off_2773 on theBenchmark for (2773ds/8173Mi) % 300.45/42.73 % TRYING [6] % 300.45/42.73 % (3581715)Instruction limit reached! % 300.45/42.73 % (3581715)------------------------------ % 300.45/42.73 % (3581715)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.45/42.73 % (3581715)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.45/42.73 % (3581715)CaDiCaL version: 2.1.3 % 300.45/42.73 % (3581715)Termination reason: Instruction limit % 300.45/42.73 % (3581715)Termination phase: Finite model building constraint generation % 300.45/42.73 % (3581715)Time elapsed: 21.283 s % 300.45/42.73 % (3581715)Peak memory usage: 1996 MB % 300.45/42.73 % (3581715)Instructions burned: 54284 (million) % 300.45/42.73 % (3581741)dis+10_16:1_sil=16000:random_seed=2944508833:i=9155:fsr=off_2761 on theBenchmark for (2761ds/9155Mi) % 300.45/42.73 % (3581739)Instruction limit reached! % 300.45/42.73 % (3581739)------------------------------ % 300.45/42.73 % (3581739)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.45/42.73 % (3581739)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.45/42.73 % (3581739)CaDiCaL version: 2.1.3 % 300.45/42.73 % (3581739)Termination reason: Instruction limit % 300.45/42.73 % (3581739)Termination phase: Saturation % 300.45/42.73 % (3581739)Time elapsed: 5.350 s % 300.45/42.73 % (3581739)Peak memory usage: 66 MB % 300.45/42.73 % (3581739)Instructions burned: 8174 (million) % 300.45/42.73 % (3581744)ott-3_8_sil=64000:random_seed=465170193:i=20139 % 300.45/42.73 Terminated % 300.45/42.73 % Vampire exiting % 300.45/42.73 Terminated %------------------------------------------------------------------------------