%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWW466-1 : TPTP v9.3.1. Released v5.2.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/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:40:03 PM UTC 2026 % Result : Timeout 300.32s 42.74s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.01 % Problem : SWW466-1 : TPTP v9.3.1. Released v5.2.0. % 0.00/0.03 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.00/0.10 % Computer : n012.cluster.edu % 0.00/0.10 % Model : x86_64 x86_64 % 0.00/0.10 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.00/0.10 % Memory : 8046.5625MB % 0.00/0.10 % OS : Linux 6.8.0-71-generic % 0.00/0.11 % CPULimit : 300 % 0.00/0.11 % WCLimit : 300 % 0.00/0.11 % DateTime : Mon Sep 28 13:59:34 UTC 2026 % 0.00/0.11 % CPUTime : % 0.00/0.11 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.09/0.12 Running first-order model finding % 0.09/0.12 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 % 11.71/2.01 % (3387415)Will run a generic schedule for satisfiability detection. % 11.71/2.01 % (3387421)% WARNING: option uhcvi not known. % 11.71/2.01 % (3387421)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1477855570:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 11.71/2.01 % (3387420)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3264173600_2999 on theBenchmark for (2999ds/0Mi) % 11.71/2.01 % (3387423)dis+10_1_sil=32000:sp=arity:random_seed=762489983:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 11.71/2.01 % (3387424)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=4194518264:i=116_2999 on theBenchmark for (2999ds/116Mi) % 11.71/2.01 % (3387425)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3099439768:i=131_2999 on theBenchmark for (2999ds/131Mi) % 11.71/2.01 % (3387422)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3004126036:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 11.71/2.01 % (3387426)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=858051342:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 11.71/2.01 % TRYING [1] % 11.71/2.01 % TRYING [2] % 11.71/2.01 % TRYING [3] % 11.71/2.01 % TRYING [4] % 11.71/2.01 % (3387424)Instruction limit reached! % 11.71/2.01 % (3387424)------------------------------ % 11.71/2.01 % (3387424)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 11.71/2.01 % (3387424)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.71/2.01 % (3387424)CaDiCaL version: 2.1.3 % 11.71/2.01 % (3387424)Termination reason: Instruction limit % 11.71/2.01 % (3387424)Termination phase: Saturation % 11.71/2.01 % (3387424)Time elapsed: 0.027 s % 11.71/2.01 % (3387424)Peak memory usage: 11 MB % 11.71/2.01 % (3387424)Instructions burned: 121 (million) % 11.71/2.01 % (3387425)Instruction limit reached! % 11.71/2.01 % (3387425)------------------------------ % 11.71/2.01 % (3387425)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 11.71/2.01 % (3387425)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.71/2.01 % (3387425)CaDiCaL version: 2.1.3 % 11.71/2.01 % (3387425)Termination reason: Instruction limit % 11.71/2.01 % (3387425)Termination phase: Saturation % 11.71/2.01 % (3387425)Time elapsed: 0.030 s % 11.71/2.01 % (3387425)Peak memory usage: 12 MB % 11.71/2.01 % (3387425)Instructions burned: 132 (million) % 11.71/2.01 % (3387423)Instruction limit reached! % 11.71/2.01 % (3387423)------------------------------ % 11.71/2.01 % (3387423)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 11.71/2.01 % (3387423)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.71/2.01 % (3387423)CaDiCaL version: 2.1.3 % 11.71/2.01 % (3387423)Termination reason: Instruction limit % 11.71/2.01 % (3387423)Termination phase: Saturation % 11.71/2.01 % (3387423)Time elapsed: 0.031 s % 11.71/2.01 % (3387423)Peak memory usage: 11 MB % 11.71/2.01 % (3387423)Instructions burned: 103 (million) % 11.71/2.01 % (3387434)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3489188732:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 11.71/2.01 % (3387435)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=102278845:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 11.71/2.01 % TRYING [1] % 11.71/2.01 % TRYING [2] % 11.71/2.01 % (3387436)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=804299034:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi) % 11.71/2.01 % TRYING [3] % 11.71/2.01 % (3387426)Instruction limit reached! % 11.71/2.01 % (3387426)------------------------------ % 11.71/2.01 % (3387426)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 11.71/2.01 % (3387426)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.71/2.01 % (3387426)CaDiCaL version: 2.1.3 % 11.71/2.01 % (3387426)Termination reason: Instruction limit % 11.71/2.01 % (3387426)Termination phase: Saturation % 11.71/2.01 % (3387426)Time elapsed: 0.044 s % 11.71/2.01 % (3387426)Peak memory usage: 12 MB % 11.71/2.01 % (3387426)Instructions burned: 162 (million) % 11.71/2.01 % (3387440)ott-21_1_sil=16000:fs=off:random_seed=1990420337:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi) % 11.71/2.01 % (3387435)Instruction limit reached! % 11.71/2.01 % (3387435)------------------------------ % 11.71/2.01 % (3387435)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 11.71/2.01 % (3387435)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.89/3.75 % (3387435)CaDiCaL version: 2.1.3 % 24.89/3.75 % (3387435)Termination reason: Instruction limit % 24.89/3.75 % (3387435)Termination phase: Saturation % 24.89/3.75 % (3387435)Time elapsed: 0.033 s % 24.89/3.75 % (3387435)Peak memory usage: 12 MB % 24.89/3.75 % (3387435)Instructions burned: 134 (million) % 24.89/3.75 % TRYING [4] % 24.89/3.75 % (3387442)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1494091381:i=477:bd=all_2999 on theBenchmark for (2999ds/477Mi) % 24.89/3.75 % TRYING [5] % 24.89/3.75 % (3387440)Instruction limit reached! % 24.89/3.75 % (3387440)------------------------------ % 24.89/3.75 % (3387440)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 24.89/3.75 % (3387440)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.89/3.75 % (3387440)CaDiCaL version: 2.1.3 % 24.89/3.75 % (3387440)Termination reason: Instruction limit % 24.89/3.75 % (3387440)Termination phase: Saturation % 24.89/3.75 % (3387440)Time elapsed: 0.040 s % 24.89/3.75 % (3387440)Peak memory usage: 11 MB % 24.89/3.75 % (3387440)Instructions burned: 185 (million) % 24.89/3.75 % (3387444)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1634530234:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 24.89/3.75 % TRYING [1] % 24.89/3.75 % TRYING [2] % 24.89/3.75 % TRYING [3] % 24.89/3.75 % TRYING [4] % 24.89/3.75 % (3387436)Instruction limit reached! % 24.89/3.75 % (3387436)------------------------------ % 24.89/3.75 % (3387436)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 24.89/3.75 % (3387436)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.89/3.75 % (3387436)CaDiCaL version: 2.1.3 % 24.89/3.75 % (3387436)Termination reason: Instruction limit % 24.89/3.75 % (3387436)Termination phase: Saturation % 24.89/3.75 % (3387436)Time elapsed: 0.163 s % 24.89/3.75 % (3387436)Peak memory usage: 14 MB % 24.89/3.75 % (3387436)Instructions burned: 687 (million) % 24.89/3.75 % (3387442)Instruction limit reached! % 24.89/3.75 % (3387442)------------------------------ % 24.89/3.75 % (3387442)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 24.89/3.75 % (3387442)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.89/3.75 % (3387442)CaDiCaL version: 2.1.3 % 24.89/3.75 % (3387442)Termination reason: Instruction limit % 24.89/3.75 % (3387442)Termination phase: Saturation % 24.89/3.75 % (3387442)Time elapsed: 0.125 s % 24.89/3.75 % (3387442)Peak memory usage: 13 MB % 24.89/3.75 % (3387442)Instructions burned: 479 (million) % 24.89/3.75 % (3387446)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=910999242:i=1179_2997 on theBenchmark for (2997ds/1179Mi) % 24.89/3.75 % (3387447)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3875100846:i=889:ins=1_2997 on theBenchmark for (2997ds/889Mi) % 24.89/3.75 % (3387434)Instruction limit reached! % 24.89/3.75 % (3387434)------------------------------ % 24.89/3.75 % (3387434)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 24.89/3.75 % (3387434)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.89/3.75 % (3387434)CaDiCaL version: 2.1.3 % 24.89/3.75 % (3387434)Termination reason: Instruction limit % 24.89/3.75 % (3387434)Termination phase: Finite model building SAT solving % 24.89/3.75 % (3387434)Time elapsed: 0.220 s % 24.89/3.75 % (3387434)Peak memory usage: 20 MB % 24.89/3.75 % (3387434)Instructions burned: 715 (million) % 24.89/3.75 % (3387450)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=1133578608: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) % 24.89/3.75 % TRYING [5] % 24.89/3.75 % (3387444)Instruction limit reached! % 24.89/3.75 % (3387444)------------------------------ % 24.89/3.75 % (3387444)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 24.89/3.75 % (3387444)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.89/3.75 % (3387444)CaDiCaL version: 2.1.3 % 24.89/3.75 % (3387444)Termination reason: Instruction limit % 24.89/3.75 % (3387444)Termination phase: Finite model building SAT solving % 24.89/3.75 % (3387444)Time elapsed: 0.216 s % 24.89/3.75 % (3387444)Peak memory usage: 21 MB % 24.89/3.75 % (3387444)Instructions burned: 869 (million) % 24.89/3.75 % (3387452)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3153196861:i=879:kws=inv_precedence:fsr=off_2996 on theBenchmark for (2996ds/879Mi) % 24.89/3.75 % TRYING [14] % 24.89/3.75 % (3387450)Instruction limit reached! % 24.89/3.75 % (3387450)------------------------------ % 69.62/10.08 % (3387450)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 69.62/10.08 % (3387450)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 69.62/10.08 % (3387450)CaDiCaL version: 2.1.3 % 69.62/10.08 % (3387450)Termination reason: Instruction limit % 69.62/10.08 % (3387450)Termination phase: Saturation % 69.62/10.08 % (3387450)Time elapsed: 0.149 s % 69.62/10.08 % (3387450)Peak memory usage: 13 MB % 69.62/10.08 % (3387450)Instructions burned: 692 (million) % 69.62/10.08 % (3387447)Instruction limit reached! % 69.62/10.08 % (3387447)------------------------------ % 69.62/10.08 % (3387447)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 69.62/10.08 % (3387447)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 69.62/10.08 % (3387447)CaDiCaL version: 2.1.3 % 69.62/10.08 % (3387447)Termination reason: Instruction limit % 69.62/10.08 % (3387447)Termination phase: Finite model building constraint generation % 69.62/10.08 % (3387447)Time elapsed: 0.211 s % 69.62/10.08 % (3387447)Peak memory usage: 92 MB % 69.62/10.08 % (3387447)Instructions burned: 890 (million) % 69.62/10.08 % (3387454)fmb+10_1_sil=64000:random_seed=1629724877:i=22061:nm=2:gsp=on_2995 on theBenchmark for (2995ds/22061Mi) % 69.62/10.08 % TRYING [1] % 69.62/10.08 % TRYING [2] % 69.62/10.08 % TRYING [3] % 69.62/10.08 % (3387456)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3883778676:i=9515:nm=5_2995 on theBenchmark for (2995ds/9515Mi) % 69.62/10.08 % TRYING [20] % 69.62/10.08 % TRYING [4] % 69.62/10.08 % (3387446)Instruction limit reached! % 69.62/10.08 % (3387446)------------------------------ % 69.62/10.08 % (3387446)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 69.62/10.08 % (3387446)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 69.62/10.08 % (3387446)CaDiCaL version: 2.1.3 % 69.62/10.08 % (3387446)Termination reason: Instruction limit % 69.62/10.08 % (3387446)Termination phase: Saturation % 69.62/10.08 % (3387446)Time elapsed: 0.267 s % 69.62/10.08 % (3387446)Peak memory usage: 20 MB % 69.62/10.08 % (3387446)Instructions burned: 1181 (million) % 69.62/10.08 % (3387458)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3456591293:fmbsr=1.7:i=920_2994 on theBenchmark for (2994ds/920Mi) % 69.62/10.08 % TRYING [8] % 69.62/10.08 % (3387452)Instruction limit reached! % 69.62/10.08 % (3387452)------------------------------ % 69.62/10.08 % (3387452)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 69.62/10.08 % (3387452)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 69.62/10.08 % (3387452)CaDiCaL version: 2.1.3 % 69.62/10.08 % (3387452)Termination reason: Instruction limit % 69.62/10.08 % (3387452)Termination phase: Saturation % 69.62/10.08 % (3387452)Time elapsed: 0.238 s % 69.62/10.08 % (3387452)Peak memory usage: 17 MB % 69.62/10.08 % (3387452)Instructions burned: 882 (million) % 69.62/10.08 % TRYING [5] % 69.62/10.08 % (3387460)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1553199515:i=5131_2993 on theBenchmark for (2993ds/5131Mi) % 69.62/10.08 % (3387458)Instruction limit reached! % 69.62/10.08 % (3387458)------------------------------ % 69.62/10.08 % (3387458)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 69.62/10.08 % (3387458)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 69.62/10.08 % (3387458)CaDiCaL version: 2.1.3 % 69.62/10.08 % (3387458)Termination reason: Instruction limit % 69.62/10.08 % (3387458)Termination phase: Finite model building constraint generation % 69.62/10.08 % (3387458)Time elapsed: 0.197 s % 69.62/10.08 % (3387458)Peak memory usage: 75 MB % 69.62/10.08 % (3387458)Instructions burned: 925 (million) % 69.62/10.08 % (3387462)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3130819265:i=1472:ins=7:fdi=8:gsp=on_2992 on theBenchmark for (2992ds/1472Mi) % 69.62/10.08 % TRYING [6] % 69.62/10.08 % (3387462)Instruction limit reached! % 69.62/10.08 % (3387462)------------------------------ % 69.62/10.08 % (3387462)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 69.62/10.08 % (3387462)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 69.62/10.08 % (3387462)CaDiCaL version: 2.1.3 % 69.62/10.08 % (3387462)Termination reason: Instruction limit % 69.62/10.08 % (3387462)Termination phase: Saturation % 69.62/10.08 % (3387462)Time elapsed: 0.359 s % 69.62/10.08 % (3387462)Peak memory usage: 23 MB % 69.62/10.08 % (3387462)Instructions burned: 1472 (million) % 69.62/10.08 % (3387464)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=2401298391:i=6324_2989 on theBenchmark for (2989ds/6324Mi) % 69.62/10.08 % TRYING [77] % 69.62/10.08 % (3387460)Instruction limit reached! % 205.04/29.27 % (3387460)------------------------------ % 205.04/29.27 % (3387460)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 205.04/29.27 % (3387460)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 205.04/29.27 % (3387460)CaDiCaL version: 2.1.3 % 205.04/29.27 % (3387460)Termination reason: Instruction limit % 205.04/29.27 % (3387460)Termination phase: Saturation % 205.04/29.27 % (3387460)Time elapsed: 1.265 s % 205.04/29.27 % (3387460)Peak memory usage: 33 MB % 205.04/29.27 % (3387460)Instructions burned: 5144 (million) % 205.04/29.27 % (3387466)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1350952349:fmbsr=2.30978:i=2174_2981 on theBenchmark for (2981ds/2174Mi) % 205.04/29.27 % TRYING [16] % 205.04/29.27 % (3387466)Instruction limit reached! % 205.04/29.27 % (3387466)------------------------------ % 205.04/29.27 % (3387466)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 205.04/29.27 % (3387466)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 205.04/29.27 % (3387466)CaDiCaL version: 2.1.3 % 205.04/29.27 % (3387466)Termination reason: Instruction limit % 205.04/29.27 % (3387466)Termination phase: Finite model building constraint generation % 205.04/29.27 % (3387466)Time elapsed: 0.408 s % 205.04/29.27 % (3387466)Peak memory usage: 137 MB % 205.04/29.27 % (3387466)Instructions burned: 2179 (million) % 205.04/29.27 % (3387468)ott-2_1_sil=16000:newcnf=on:random_seed=77740475:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2976 on theBenchmark for (2976ds/869Mi) % 205.04/29.27 % (3387456)Instruction limit reached! % 205.04/29.27 % (3387456)------------------------------ % 205.04/29.27 % (3387456)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 205.04/29.27 % (3387456)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 205.04/29.27 % (3387456)CaDiCaL version: 2.1.3 % 205.04/29.27 % (3387456)Termination reason: Instruction limit % 205.04/29.27 % (3387456)Termination phase: Finite model building constraint generation % 205.04/29.27 % (3387456)Time elapsed: 1.882 s % 205.04/29.27 % (3387456)Peak memory usage: 666 MB % 205.04/29.27 % (3387456)Instructions burned: 9521 (million) % 205.04/29.27 % (3387464)Instruction limit reached! % 205.04/29.27 % (3387464)------------------------------ % 205.04/29.27 % (3387464)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 205.04/29.27 % (3387464)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 205.04/29.27 % (3387464)CaDiCaL version: 2.1.3 % 205.04/29.27 % (3387464)Termination reason: Instruction limit % 205.04/29.27 % (3387464)Termination phase: Finite model building constraint generation % 205.04/29.27 % (3387464)Time elapsed: 1.253 s % 205.04/29.27 % (3387464)Peak memory usage: 457 MB % 205.04/29.27 % (3387464)Instructions burned: 6328 (million) % 205.04/29.27 % (3387470)ott+10_1_sil=32000:tgt=ground:random_seed=1269529749:i=5114:av=off_2975 on theBenchmark for (2975ds/5114Mi) % 205.04/29.27 % (3387472)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=3511850492:i=54282_2975 on theBenchmark for (2975ds/54282Mi) % 205.04/29.27 % TRYING [1] % 205.04/29.27 % TRYING [2] % 205.04/29.27 % TRYING [3] % 205.04/29.27 % TRYING [4] % 205.04/29.27 % (3387468)Instruction limit reached! % 205.04/29.27 % (3387468)------------------------------ % 205.04/29.27 % (3387468)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 205.04/29.27 % (3387468)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 205.04/29.27 % (3387468)CaDiCaL version: 2.1.3 % 205.04/29.27 % (3387468)Termination reason: Instruction limit % 205.04/29.27 % (3387468)Termination phase: Saturation % 205.04/29.27 % (3387468)Time elapsed: 0.192 s % 205.04/29.27 % (3387468)Peak memory usage: 14 MB % 205.04/29.27 % (3387468)Instructions burned: 874 (million) % 205.04/29.27 % TRYING [5] % 205.04/29.27 % (3387474)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=2779578483:i=3512:aac=none_2974 on theBenchmark for (2974ds/3512Mi) % 205.04/29.27 % TRYING [6] % 205.04/29.27 % (3387474)Instruction limit reached! % 205.04/29.27 % (3387474)------------------------------ % 205.04/29.27 % (3387474)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 205.04/29.27 % (3387474)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 205.04/29.27 % (3387474)CaDiCaL version: 2.1.3 % 205.04/29.27 % (3387474)Termination reason: Instruction limit % 205.04/29.27 % (3387474)Termination phase: Saturation % 205.04/29.27 % (3387474)Time elapsed: 0.844 s % 205.04/29.27 % (3387474)Peak memory usage: 25 MB % 205.04/29.27 % (3387474)Instructions burned: 3512 (million) % 205.04/29.27 % (3387476)dis+21_1_sil=32000:sas=cadical:random_seed=2215288856:i=3773:amm=off_2966 on theBenchmark for (2966ds/3773Mi) % 205.04/29.27 % TRYING [6] % 205.04/29.27 % (3387470)Instruction limit reached! % 281.41/40.05 % (3387470)------------------------------ % 281.41/40.05 % (3387470)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 281.41/40.05 % (3387470)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 281.41/40.05 % (3387470)CaDiCaL version: 2.1.3 % 281.41/40.05 % (3387470)Termination reason: Instruction limit % 281.41/40.05 % (3387470)Termination phase: Saturation % 281.41/40.05 % (3387470)Time elapsed: 1.210 s % 281.41/40.05 % (3387470)Peak memory usage: 27 MB % 281.41/40.05 % (3387470)Instructions burned: 5117 (million) % 281.41/40.05 % (3387478)ott+11_1_sil=16000:gs=on:random_seed=4118071486:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2963 on theBenchmark for (2963ds/2251Mi) % 281.41/40.05 % (3387478)Instruction limit reached! % 281.41/40.05 % (3387478)------------------------------ % 281.41/40.05 % (3387478)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 281.41/40.05 % (3387478)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 281.41/40.05 % (3387478)CaDiCaL version: 2.1.3 % 281.41/40.05 % (3387478)Termination reason: Instruction limit % 281.41/40.05 % (3387478)Termination phase: Saturation % 281.41/40.05 % (3387478)Time elapsed: 0.459 s % 281.41/40.05 % (3387478)Peak memory usage: 14 MB % 281.41/40.05 % (3387478)Instructions burned: 2253 (million) % 281.41/40.05 % (3387480)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=108919641:fmbsr=1.6:i=67534_2959 on theBenchmark for (2959ds/67534Mi) % 281.41/40.05 % TRYING [7] % 281.41/40.05 % (3387476)Instruction limit reached! % 281.41/40.05 % (3387476)------------------------------ % 281.41/40.05 % (3387476)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 281.41/40.05 % (3387476)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 281.41/40.05 % (3387476)CaDiCaL version: 2.1.3 % 281.41/40.05 % (3387476)Termination reason: Instruction limit % 281.41/40.05 % (3387476)Termination phase: Saturation % 281.41/40.05 % (3387476)Time elapsed: 0.939 s % 281.41/40.05 % (3387476)Peak memory usage: 27 MB % 281.41/40.05 % (3387476)Instructions burned: 3776 (million) % 281.41/40.05 % (3387482)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=3695193689:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2956 on theBenchmark for (2956ds/4591Mi) % 281.41/40.05 % (3387482)Instruction limit reached! % 281.41/40.05 % (3387482)------------------------------ % 281.41/40.05 % (3387482)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 281.41/40.05 % (3387482)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 281.41/40.05 % (3387482)CaDiCaL version: 2.1.3 % 281.41/40.05 % (3387482)Termination reason: Instruction limit % 281.41/40.05 % (3387482)Termination phase: Saturation % 281.41/40.05 % (3387482)Time elapsed: 1.150 s % 281.41/40.05 % (3387482)Peak memory usage: 54 MB % 281.41/40.05 % (3387482)Instructions burned: 4595 (million) % 281.41/40.05 % (3387484)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=3254894819:i=29340_2945 on theBenchmark for (2945ds/29340Mi) % 281.41/40.05 % (3387454)Instruction limit reached! % 281.41/40.05 % (3387454)------------------------------ % 281.41/40.05 % (3387454)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 281.41/40.05 % (3387454)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 281.41/40.05 % (3387454)CaDiCaL version: 2.1.3 % 281.41/40.05 % (3387454)Termination reason: Instruction limit % 281.41/40.05 % (3387454)Termination phase: Finite model building SAT solving % 281.41/40.05 % (3387454)Time elapsed: 7.039 s % 281.41/40.05 % (3387454)Peak memory usage: 50 MB % 281.41/40.05 % (3387454)Instructions burned: 22062 (million) % 281.41/40.05 % (3387486)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=837951418:i=5211_2924 on theBenchmark for (2924ds/5211Mi) % 281.41/40.05 % (3387486)Instruction limit reached! % 281.41/40.05 % (3387486)------------------------------ % 281.41/40.05 % (3387486)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 281.41/40.05 % (3387486)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 281.41/40.05 % (3387486)CaDiCaL version: 2.1.3 % 281.41/40.05 % (3387486)Termination reason: Instruction limit % 281.41/40.05 % (3387486)Termination phase: Saturation % 281.41/40.05 % (3387486)Time elapsed: 1.356 s % 281.41/40.05 % (3387486)Peak memory usage: 40 MB % 281.41/40.05 % (3387486)Instructions burned: 5213 (million) % 281.41/40.05 % (3387488)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=3270886343:i=5497:nm=2_2911 on theBenchmark for (2911ds/5497Mi) % 281.41/40.05 % TRYING [17] % 281.41/40.05 % TRYING [7] % 281.41/40.05 %Terminated % 300.32/42.74 % Vampire exiting % 300.32/42.74 Terminated %------------------------------------------------------------------------------