%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWV863-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 : n009.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:33 PM UTC 2026 % Result : Timeout 290.24s 41.23s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWV863-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.08/0.19 % Computer : n009.cluster.edu % 0.08/0.19 % Model : x86_64 x86_64 % 0.08/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.08/0.19 % Memory : 8046.5625MB % 0.08/0.19 % OS : Linux 6.8.0-71-generic % 0.08/0.19 % CPULimit : 300 % 0.08/0.19 % WCLimit : 300 % 0.08/0.19 % DateTime : Mon Sep 28 12:45:15 UTC 2026 % 0.08/0.20 % CPUTime : % 0.08/0.20 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.08/0.23 Running first-order model finding % 0.08/0.23 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.68/1.94 % (3004839)Will run a generic schedule for satisfiability detection. % 9.68/1.94 % (3004845)% WARNING: option uhcvi not known. % 9.68/1.94 % (3004845)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3717171772:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 9.68/1.94 % (3004844)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3669918996_2999 on theBenchmark for (2999ds/0Mi) % 9.68/1.94 % (3004846)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2001469766:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 9.68/1.94 % (3004847)dis+10_1_sil=32000:sp=arity:random_seed=2750984279:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 9.68/1.94 % (3004848)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1603749495:i=116_2999 on theBenchmark for (2999ds/116Mi) % 9.68/1.94 % (3004849)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3902265951:i=131_2999 on theBenchmark for (2999ds/131Mi) % 9.68/1.94 % (3004850)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3002131949:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 9.68/1.94 % (3004848)Instruction limit reached! % 9.68/1.94 % (3004848)------------------------------ % 9.68/1.94 % (3004848)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 9.68/1.94 % (3004848)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.68/1.94 % (3004848)CaDiCaL version: 2.1.3 % 9.68/1.94 % (3004848)Termination reason: Instruction limit % 9.68/1.94 % (3004848)Termination phase: Saturation % 9.68/1.94 % (3004848)Time elapsed: 0.062 s % 9.68/1.94 % (3004848)Peak memory usage: 13 MB % 9.68/1.94 % (3004848)Instructions burned: 117 (million) % 9.68/1.94 % (3004847)Instruction limit reached! % 9.68/1.94 % (3004847)------------------------------ % 9.68/1.94 % (3004847)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 9.68/1.94 % (3004847)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.68/1.94 % (3004847)CaDiCaL version: 2.1.3 % 9.68/1.94 % (3004847)Termination reason: Instruction limit % 9.68/1.94 % (3004847)Termination phase: Saturation % 9.68/1.94 % (3004847)Time elapsed: 0.065 s % 9.68/1.94 % (3004847)Peak memory usage: 13 MB % 9.68/1.94 % (3004847)Instructions burned: 104 (million) % 9.68/1.94 % (3004849)Instruction limit reached! % 9.68/1.94 % (3004849)------------------------------ % 9.68/1.94 % (3004849)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 9.68/1.94 % (3004849)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.68/1.94 % (3004849)CaDiCaL version: 2.1.3 % 9.68/1.94 % (3004849)Termination reason: Instruction limit % 9.68/1.94 % (3004849)Termination phase: Saturation % 9.68/1.94 % (3004849)Time elapsed: 0.080 s % 9.68/1.94 % (3004849)Peak memory usage: 14 MB % 9.68/1.94 % (3004849)Instructions burned: 131 (million) % 9.68/1.94 % (3004858)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1054437930:i=714:nm=2_2998 on theBenchmark for (2998ds/714Mi) % 9.68/1.94 % (3004859)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1576538873:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi) % 9.68/1.94 % (3004860)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=2363122323:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi) % 9.68/1.94 % (3004850)Instruction limit reached! % 9.68/1.94 % (3004850)------------------------------ % 9.68/1.94 % (3004850)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 9.68/1.94 % (3004850)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.68/1.94 % (3004850)CaDiCaL version: 2.1.3 % 9.68/1.94 % (3004850)Termination reason: Instruction limit % 9.68/1.94 % (3004850)Termination phase: Saturation % 9.68/1.94 % (3004850)Time elapsed: 0.102 s % 9.68/1.94 % (3004850)Peak memory usage: 14 MB % 9.68/1.94 % (3004850)Instructions burned: 159 (million) % 9.68/1.94 % (3004864)ott-21_1_sil=16000:fs=off:random_seed=1350144699:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 9.68/1.94 % (3004859)Instruction limit reached! % 9.68/1.94 % (3004859)------------------------------ % 9.68/1.94 % (3004859)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 9.68/1.94 % (3004859)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.68/1.94 % (3004859)CaDiCaL version: 2.1.3 % 39.92/5.94 % (3004859)Termination reason: Instruction limit % 39.92/5.94 % (3004859)Termination phase: Saturation % 39.92/5.94 % (3004859)Time elapsed: 0.074 s % 39.92/5.94 % (3004859)Peak memory usage: 13 MB % 39.92/5.94 % (3004859)Instructions burned: 131 (million) % 39.92/5.94 % (3004866)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=867210208:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi) % 39.92/5.94 % (3004864)Instruction limit reached! % 39.92/5.94 % (3004864)------------------------------ % 39.92/5.94 % (3004864)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 39.92/5.94 % (3004864)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.92/5.94 % (3004864)CaDiCaL version: 2.1.3 % 39.92/5.94 % (3004864)Termination reason: Instruction limit % 39.92/5.94 % (3004864)Termination phase: Saturation % 39.92/5.94 % (3004864)Time elapsed: 0.099 s % 39.92/5.94 % (3004864)Peak memory usage: 13 MB % 39.92/5.94 % (3004864)Instructions burned: 180 (million) % 39.92/5.94 % (3004868)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2738151057:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi) % 39.92/5.94 % TRYING [1] % 39.92/5.94 % TRYING [2] % 39.92/5.94 % TRYING [1] % 39.92/5.94 % TRYING [2] % 39.92/5.94 % (3004858)Instruction limit reached! % 39.92/5.94 % (3004858)------------------------------ % 39.92/5.94 % (3004858)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 39.92/5.94 % (3004858)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.92/5.94 % (3004858)CaDiCaL version: 2.1.3 % 39.92/5.94 % (3004858)Termination reason: Instruction limit % 39.92/5.94 % (3004858)Termination phase: Finite model building constraint generation % 39.92/5.94 % (3004858)Time elapsed: 0.341 s % 39.92/5.94 % (3004858)Peak memory usage: 21 MB % 39.92/5.94 % (3004858)Instructions burned: 717 (million) % 39.92/5.94 % (3004870)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3854615308:i=1179_2995 on theBenchmark for (2995ds/1179Mi) % 39.92/5.94 % (3004866)Instruction limit reached! % 39.92/5.94 % (3004866)------------------------------ % 39.92/5.94 % (3004866)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 39.92/5.94 % (3004866)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.92/5.94 % (3004866)CaDiCaL version: 2.1.3 % 39.92/5.94 % (3004866)Termination reason: Instruction limit % 39.92/5.94 % (3004866)Termination phase: Saturation % 39.92/5.94 % (3004866)Time elapsed: 0.302 s % 39.92/5.94 % (3004866)Peak memory usage: 14 MB % 39.92/5.94 % (3004866)Instructions burned: 478 (million) % 39.92/5.94 % TRYING [3] % 39.92/5.94 % (3004860)Instruction limit reached! % 39.92/5.94 % (3004860)------------------------------ % 39.92/5.94 % (3004860)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 39.92/5.94 % (3004860)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.92/5.94 % (3004860)CaDiCaL version: 2.1.3 % 39.92/5.94 % (3004860)Termination reason: Instruction limit % 39.92/5.94 % (3004860)Termination phase: Saturation % 39.92/5.94 % (3004860)Time elapsed: 0.401 s % 39.92/5.94 % (3004860)Peak memory usage: 18 MB % 39.92/5.94 % (3004860)Instructions burned: 684 (million) % 39.92/5.94 % (3004872)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1846201042:i=889:ins=1_2994 on theBenchmark for (2994ds/889Mi) % 39.92/5.94 % (3004874)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=1414403411: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) % 39.92/5.94 % (3004868)Instruction limit reached! % 39.92/5.94 % (3004868)------------------------------ % 39.92/5.94 % (3004868)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 39.92/5.94 % (3004868)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.92/5.94 % (3004868)CaDiCaL version: 2.1.3 % 39.92/5.94 % (3004868)Termination reason: Instruction limit % 39.92/5.94 % (3004868)Termination phase: Finite model building preprocessing % 39.92/5.94 % (3004868)Time elapsed: 0.432 s % 39.92/5.94 % (3004868)Peak memory usage: 24 MB % 39.92/5.94 % (3004868)Instructions burned: 867 (million) % 39.92/5.94 % (3004876)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2556210463:i=879:kws=inv_precedence:fsr=off_2992 on theBenchmark for (2992ds/879Mi) % 39.92/5.94 % (3004872)Cannot represent all propositional literals internally % 39.92/5.94 % (3004872)Refutation not found, incomplete strategy % 39.92/5.94 % (3004872)------------------------------ % 39.92/5.94 % (3004872)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 93.83/13.59 % (3004872)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 93.83/13.59 % (3004872)CaDiCaL version: 2.1.3 % 93.83/13.59 % (3004872)Termination reason: Refutation not found, incomplete strategy % 93.83/13.59 % (3004872)Time elapsed: 0.321 s % 93.83/13.59 % (3004872)Peak memory usage: 21 MB % 93.83/13.59 % (3004872)Instructions burned: 655 (million) % 93.83/13.59 % (3004872)------------------------------ % 93.83/13.59 % (3004872)------------------------------ % 93.83/13.59 % (3004878)fmb+10_1_sil=64000:random_seed=407608465:i=22061:nm=2:gsp=on_2990 on theBenchmark for (2990ds/22061Mi) % 93.83/13.59 % (3004874)Instruction limit reached! % 93.83/13.59 % (3004874)------------------------------ % 93.83/13.59 % (3004874)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 93.83/13.59 % (3004874)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 93.83/13.59 % (3004874)CaDiCaL version: 2.1.3 % 93.83/13.59 % (3004874)Termination reason: Instruction limit % 93.83/13.59 % (3004874)Termination phase: Saturation % 93.83/13.59 % (3004874)Time elapsed: 0.408 s % 93.83/13.59 % (3004874)Peak memory usage: 21 MB % 93.83/13.59 % (3004874)Instructions burned: 693 (million) % 93.83/13.59 % (3004880)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1433401286:i=9515:nm=5_2989 on theBenchmark for (2989ds/9515Mi) % 93.83/13.59 % (3004870)Instruction limit reached! % 93.83/13.59 % (3004870)------------------------------ % 93.83/13.59 % (3004870)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 93.83/13.59 % (3004870)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 93.83/13.59 % (3004870)CaDiCaL version: 2.1.3 % 93.83/13.59 % (3004870)Termination reason: Instruction limit % 93.83/13.59 % (3004870)Termination phase: Saturation % 93.83/13.59 % (3004870)Time elapsed: 0.724 s % 93.83/13.59 % (3004870)Peak memory usage: 25 MB % 93.83/13.59 % (3004870)Instructions burned: 1180 (million) % 93.83/13.59 % TRYING [1] % 93.83/13.59 % (3004876)Instruction limit reached! % 93.83/13.59 % (3004876)------------------------------ % 93.83/13.59 % (3004876)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 93.83/13.59 % (3004876)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 93.83/13.59 % (3004876)CaDiCaL version: 2.1.3 % 93.83/13.59 % (3004876)Termination reason: Instruction limit % 93.83/13.59 % (3004876)Termination phase: Saturation % 93.83/13.59 % (3004876)Time elapsed: 0.492 s % 93.83/13.59 % (3004876)Peak memory usage: 20 MB % 93.83/13.59 % (3004876)Instructions burned: 883 (million) % 93.83/13.59 % (3004882)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2238868604:fmbsr=1.7:i=920_2987 on theBenchmark for (2987ds/920Mi) % 93.83/13.59 % (3004884)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2507442183:i=5131_2987 on theBenchmark for (2987ds/5131Mi) % 93.83/13.59 % TRYING [2] % 93.83/13.59 % (3004880)Cannot represent all propositional literals internally % 93.83/13.59 % (3004880)Refutation not found, incomplete strategy % 93.83/13.59 % (3004880)------------------------------ % 93.83/13.59 % (3004880)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 93.83/13.59 % (3004880)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 93.83/13.59 % (3004880)CaDiCaL version: 2.1.3 % 93.83/13.59 % (3004880)Termination reason: Refutation not found, incomplete strategy % 93.83/13.59 % (3004880)Time elapsed: 0.325 s % 93.83/13.59 % (3004880)Peak memory usage: 20 MB % 93.83/13.59 % (3004880)Instructions burned: 655 (million) % 93.83/13.59 % (3004880)------------------------------ % 93.83/13.59 % (3004880)------------------------------ % 93.83/13.59 % (3004886)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2335682510:i=1472:ins=7:fdi=8:gsp=on_2986 on theBenchmark for (2986ds/1472Mi) % 93.83/13.59 % TRYING [8] % 93.83/13.59 % (3004882)Instruction limit reached! % 93.83/13.59 % (3004882)------------------------------ % 93.83/13.59 % (3004882)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 93.83/13.59 % (3004882)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 93.83/13.59 % (3004882)CaDiCaL version: 2.1.3 % 93.83/13.59 % (3004882)Termination reason: Instruction limit % 93.83/13.59 % (3004882)Termination phase: Finite model building constraint generation % 93.83/13.59 % (3004882)Time elapsed: 0.415 s % 93.83/13.59 % (3004882)Peak memory usage: 38 MB % 93.83/13.59 % (3004882)Instructions burned: 920 (million) % 93.83/13.59 % (3004888)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=664370952:i=6324_2983 on theBenchmark for (2983ds/6324Mi) % 205.89/29.32 % TRYING [3] % 205.89/29.32 % (3004888)Cannot represent all propositional literals internally % 205.89/29.32 % (3004888)Refutation not found, incomplete strategy % 205.89/29.32 % (3004888)------------------------------ % 205.89/29.32 % (3004888)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 205.89/29.32 % (3004888)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 205.89/29.32 % (3004888)CaDiCaL version: 2.1.3 % 205.89/29.32 % (3004888)Termination reason: Refutation not found, incomplete strategy % 205.89/29.32 % (3004888)Time elapsed: 0.329 s % 205.89/29.32 % (3004888)Peak memory usage: 21 MB % 205.89/29.32 % (3004888)Instructions burned: 657 (million) % 205.89/29.32 % (3004888)------------------------------ % 205.89/29.32 % (3004888)------------------------------ % 205.89/29.32 % (3004890)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=2855340829:fmbsr=2.30978:i=2174_2979 on theBenchmark for (2979ds/2174Mi) % 205.89/29.32 % (3004886)Instruction limit reached! % 205.89/29.32 % (3004886)------------------------------ % 205.89/29.32 % (3004886)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 205.89/29.32 % (3004886)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 205.89/29.32 % (3004886)CaDiCaL version: 2.1.3 % 205.89/29.32 % (3004886)Termination reason: Instruction limit % 205.89/29.32 % (3004886)Termination phase: Saturation % 205.89/29.32 % (3004886)Time elapsed: 0.760 s % 205.89/29.32 % (3004886)Peak memory usage: 31 MB % 205.89/29.32 % (3004886)Instructions burned: 1474 (million) % 205.89/29.32 % (3004892)ott-2_1_sil=16000:newcnf=on:random_seed=641143530:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2978 on theBenchmark for (2978ds/869Mi) % 205.89/29.32 % (3004892)Instruction limit reached! % 205.89/29.32 % (3004892)------------------------------ % 205.89/29.32 % (3004892)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 205.89/29.32 % (3004892)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 205.89/29.32 % (3004892)CaDiCaL version: 2.1.3 % 205.89/29.32 % (3004892)Termination reason: Instruction limit % 205.89/29.32 % (3004892)Termination phase: Saturation % 205.89/29.32 % (3004892)Time elapsed: 0.310 s % 205.89/29.32 % (3004892)Peak memory usage: 13 MB % 205.89/29.32 % (3004892)Instructions burned: 871 (million) % 205.89/29.32 % (3004894)ott+10_1_sil=32000:tgt=ground:random_seed=262149831:i=5114:av=off_2975 on theBenchmark for (2975ds/5114Mi) % 205.89/29.32 % TRYING [4] % 205.89/29.32 % (3004890)Instruction limit reached! % 205.89/29.32 % (3004890)------------------------------ % 205.89/29.32 % (3004890)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 205.89/29.32 % (3004890)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 205.89/29.32 % (3004890)CaDiCaL version: 2.1.3 % 205.89/29.32 % (3004890)Termination reason: Instruction limit % 205.89/29.32 % (3004890)Termination phase: Finite model building preprocessing % 205.89/29.32 % (3004890)Time elapsed: 1.079 s % 205.89/29.32 % (3004890)Peak memory usage: 28 MB % 205.89/29.32 % (3004890)Instructions burned: 2176 (million) % 205.89/29.32 % (3004896)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2372223230:i=54282_2968 on theBenchmark for (2968ds/54282Mi) % 205.89/29.32 % TRYING [1] % 205.89/29.32 % TRYING [2] % 205.89/29.32 % TRYING [3] % 205.89/29.32 % (3004884)Instruction limit reached! % 205.89/29.32 % (3004884)------------------------------ % 205.89/29.32 % (3004884)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 205.89/29.32 % (3004884)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 205.89/29.32 % (3004884)CaDiCaL version: 2.1.3 % 205.89/29.32 % (3004884)Termination reason: Instruction limit % 205.89/29.32 % (3004884)Termination phase: Saturation % 205.89/29.32 % (3004884)Time elapsed: 2.702 s % 205.89/29.32 % (3004884)Peak memory usage: 37 MB % 205.89/29.32 % (3004884)Instructions burned: 5131 (million) % 205.89/29.32 % (3004898)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=1151226780:i=3512:aac=none_2960 on theBenchmark for (2960ds/3512Mi) % 205.89/29.32 % (3004898)Instruction limit reached! % 205.89/29.32 % (3004898)------------------------------ % 205.89/29.32 % (3004898)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 205.89/29.32 % (3004898)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 205.89/29.32 % (3004898)CaDiCaL version: 2.1.3 % 205.89/29.32 % (3004898)Termination reason: Instruction limit % 205.89/29.32 % (3004898)Termination phase: Saturation % 205.89/29.32 % (3004898)Time elapsed: 1.667 s % 205.89/29.32 % (3004898)Peak memory usage: 24 MB % 205.89/29.32 % (3004898)Instructions burned: 3513 (million) % 205.89/29.32 % TRYING [4] % 205.89/29.32 % (3004900)dis+21_1_sil=32000:sas=cadical:random_seed=1526663935:i=3773:amm=off_2943 on theBenchmark for (2943ds/3773Mi) % 290.24/41.23 % (3004894)Instruction limit reached! % 290.24/41.23 % (3004894)------------------------------ % 290.24/41.23 % (3004894)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 290.24/41.23 % (3004894)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 290.24/41.23 % (3004894)CaDiCaL version: 2.1.3 % 290.24/41.23 % (3004894)Termination reason: Instruction limit % 290.24/41.23 % (3004894)Termination phase: Saturation % 290.24/41.23 % (3004894)Time elapsed: 3.242 s % 290.24/41.23 % (3004894)Peak memory usage: 56 MB % 290.24/41.23 % (3004894)Instructions burned: 5114 (million) % 290.24/41.23 % (3004902)ott+11_1_sil=16000:gs=on:random_seed=2227184224:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2942 on theBenchmark for (2942ds/2251Mi) % 290.24/41.23 % (3004902)Instruction limit reached! % 290.24/41.23 % (3004902)------------------------------ % 290.24/41.23 % (3004902)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 290.24/41.23 % (3004902)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 290.24/41.23 % (3004902)CaDiCaL version: 2.1.3 % 290.24/41.23 % (3004902)Termination reason: Instruction limit % 290.24/41.23 % (3004902)Termination phase: Saturation % 290.24/41.23 % (3004902)Time elapsed: 1.231 s % 290.24/41.23 % (3004902)Peak memory usage: 22 MB % 290.24/41.23 % (3004902)Instructions burned: 2252 (million) % 290.24/41.23 % (3004904)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=2466298638:fmbsr=1.6:i=67534_2930 on theBenchmark for (2930ds/67534Mi) % 290.24/41.23 % (3004900)Instruction limit reached! % 290.24/41.23 % (3004900)------------------------------ % 290.24/41.23 % (3004900)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 290.24/41.23 % (3004900)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 290.24/41.23 % (3004900)CaDiCaL version: 2.1.3 % 290.24/41.23 % (3004900)Termination reason: Instruction limit % 290.24/41.23 % (3004900)Termination phase: Saturation % 290.24/41.23 % (3004900)Time elapsed: 2.237 s % 290.24/41.23 % (3004900)Peak memory usage: 44 MB % 290.24/41.23 % (3004900)Instructions burned: 3774 (million) % 290.24/41.23 % (3004906)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=358506472:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2920 on theBenchmark for (2920ds/4591Mi) % 290.24/41.23 % (3004906)Instruction limit reached! % 290.24/41.23 % (3004906)------------------------------ % 290.24/41.23 % (3004906)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 290.24/41.23 % (3004906)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 290.24/41.23 % (3004906)CaDiCaL version: 2.1.3 % 290.24/41.23 % (3004906)Termination reason: Instruction limit % 290.24/41.23 % (3004906)Termination phase: Saturation % 290.24/41.23 % (3004906)Time elapsed: 1.797 s % 290.24/41.23 % (3004906)Peak memory usage: 31 MB % 290.24/41.23 % (3004906)Instructions burned: 4591 (million) % 290.24/41.23 % (3004908)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=1424749138:i=29340_2902 on theBenchmark for (2902ds/29340Mi) % 290.24/41.23 % TRYING [4] % 290.24/41.23 % (3004878)Instruction limit reached! % 290.24/41.23 % (3004878)------------------------------ % 290.24/41.23 % (3004878)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 290.24/41.23 % (3004878)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 290.24/41.23 % (3004878)CaDiCaL version: 2.1.3 % 290.24/41.23 % (3004878)Termination reason: Instruction limit % 290.24/41.23 % (3004878)Termination phase: Finite model building constraint generation % 290.24/41.23 % (3004878)Time elapsed: 9.540 s % 290.24/41.23 % (3004878)Peak memory usage: 376 MB % 290.24/41.23 % (3004878)Instructions burned: 22062 (million) % 290.24/41.23 % (3004910)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=1950163427:i=5211_2894 on theBenchmark for (2894ds/5211Mi) % 290.24/41.23 % (3004910)Instruction limit reached! % 290.24/41.23 % (3004910)------------------------------ % 290.24/41.23 % (3004910)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 290.24/41.23 % (3004910)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 290.24/41.23 % (3004910)CaDiCaL version: 2.1.3 % 290.24/41.23 % (3004910)Termination reason: Instruction limit % 290.24/41.23 % (3004910)Termination phase: Saturation % 290.24/41.23 % (3004910)Time elapsed: 2.795 s % 290.24/41.23 % (3004910)Peak memory usage: 53 MB % 290.24/41.23 % (3004910)Instructions burned: 5211 (million) % 290.24/41.23 % (3004912)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=1608811464:i=5497:nm=2_2866 on theBenchmark for (2866ds/5497Mi) % 300.57/42.73 % (3004912)Cannot represent all propositional literals internally % 300.57/42.73 % (3004912)Refutation not found, incomplete strategy % 300.57/42.73 % (3004912)------------------------------ % 300.57/42.73 % (3004912)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.57/42.73 % (3004912)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.57/42.73 % (3004912)CaDiCaL version: 2.1.3 % 300.57/42.73 % (3004912)Termination reason: Refutation not found, incomplete strategy % 300.57/42.73 % (3004912)Time elapsed: 0.327 s % 300.57/42.73 % (3004912)Peak memory usage: 21 MB % 300.57/42.73 % (3004912)Instructions burned: 657 (million) % 300.57/42.73 % (3004912)------------------------------ % 300.57/42.73 % (3004912)------------------------------ % 300.57/42.73 % (3004914)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=184494086:fmbsr=2:i=46332_2863 on theBenchmark for (2863ds/46332Mi) % 300.57/42.73 % (3004914)Cannot represent all propositional literals internally % 300.57/42.73 % (3004914)Refutation not found, incomplete strategy % 300.57/42.73 % (3004914)------------------------------ % 300.57/42.73 % (3004914)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.57/42.73 % (3004914)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.57/42.73 % (3004914)CaDiCaL version: 2.1.3 % 300.57/42.73 % (3004914)Termination reason: Refutation not found, incomplete strategy % 300.57/42.73 % (3004914)Time elapsed: 0.324 s % 300.57/42.73 % (3004914)Peak memory usage: 19 MB % 300.57/42.73 % (3004914)Instructions burned: 668 (million) % 300.57/42.73 % (3004914)------------------------------ % 300.57/42.73 % (3004914)------------------------------ % 300.57/42.73 % (3004916)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=1751957920:i=14071_2859 on theBenchmark for (2859ds/14071Mi) % 300.57/42.73 % (3004916)Cannot represent all propositional literals internally % 300.57/42.73 % (3004916)Refutation not found, incomplete strategy % 300.57/42.73 % (3004916)------------------------------ % 300.57/42.73 % (3004916)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.57/42.73 % (3004916)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.57/42.73 % (3004916)CaDiCaL version: 2.1.3 % 300.57/42.73 % (3004916)Termination reason: Refutation not found, incomplete strategy % 300.57/42.73 % (3004916)Time elapsed: 0.325 s % 300.57/42.73 % (3004916)Peak memory usage: 21 MB % 300.57/42.73 % (3004916)Instructions burned: 657 (million) % 300.57/42.73 % (3004916)------------------------------ % 300.57/42.73 % (3004916)------------------------------ % 300.57/42.73 % (3004918)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3337317624:i=22565:add=on:rawr=on_2856 on theBenchmark for (2856ds/22565Mi) % 300.57/42.73 % TRYING [5] % 300.57/42.73 % (3004908)Instruction limit reached! % 300.57/42.73 % (3004908)------------------------------ % 300.57/42.73 % (3004908)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.57/42.73 % (3004908)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.57/42.73 % (3004908)CaDiCaL version: 2.1.3 % 300.57/42.73 % (3004908)Termination reason: Instruction limit % 300.57/42.73 % (3004908)Termination phase: Saturation % 300.57/42.73 % (3004908)Time elapsed: 14.493 s % 300.57/42.73 % (3004908)Peak memory usage: 217 MB % 300.57/42.73 % (3004908)Instructions burned: 29341 (million) % 300.57/42.73 % (3004920)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=3523246563:i=8173:av=off_2756 on theBenchmark for (2756ds/8173Mi) % 300.57/42.73 % TRYING [5] % 300.57/42.73 % (3004918)Instruction limit reached! % 300.57/42.73 % (3004918)------------------------------ % 300.57/42.73 % (3004918)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.57/42.73 % (3004918)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.57/42.73 % (3004918)CaDiCaL version: 2.1.3 % 300.57/42.73 % (3004918)Termination reason: Instruction limit % 300.57/42.73 % (3004918)Termination phase: Saturation % 300.57/42.73 % (3004918)Time elapsed: 13.989 s % 300.57/42.73 % (3004918)Peak memory usage: 118 MB % 300.57/42.73 % (3004918)Instructions burned: 22566 (million) % 300.57/42.73 % (3004922)dis+10_16:1_sil=16000:random_seed=173855472:i=9155:fsr=off_2715 on theBenchmark for (2715ds/9155Mi) % 300.57/42.73 % (3004896)Instruction limit reached! % 300.57/42.73 % (3004896)------------------------------ % 300.57/42.73 % (3004896)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.57/42.73 % (3004896)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c % 300.57/42.73 Terminated %------------------------------------------------------------------------------