%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWV948-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 : n005.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:42 PM UTC 2026 % Result : Timeout 288.39s 41.01s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : SWV948-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.05/0.18 % Computer : n005.cluster.edu % 0.05/0.18 % Model : x86_64 x86_64 % 0.05/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.05/0.18 % Memory : 8046.5625MB % 0.05/0.18 % OS : Linux 6.8.0-71-generic % 0.05/0.18 % CPULimit : 300 % 0.05/0.18 % WCLimit : 300 % 0.05/0.18 % DateTime : Mon Sep 28 12:59:50 UTC 2026 % 0.05/0.18 % CPUTime : % 0.05/0.18 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.05/0.21 Running first-order model finding % 0.05/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 % 7.41/1.31 % (766957)Will run a generic schedule for satisfiability detection. % 7.41/1.31 % (766966)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3935167893:i=116_2999 on theBenchmark for (2999ds/116Mi) % 7.41/1.31 % (766963)% WARNING: option uhcvi not known. % 7.41/1.31 % (766963)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2300951559:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 7.41/1.31 % (766962)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3398992237_2999 on theBenchmark for (2999ds/0Mi) % 7.41/1.31 % (766964)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3862534701:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 7.41/1.31 % (766965)dis+10_1_sil=32000:sp=arity:random_seed=1440018636:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 7.41/1.31 % (766967)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=965150242:i=131_2999 on theBenchmark for (2999ds/131Mi) % 7.41/1.31 % (766968)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1565398515:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 7.41/1.31 % (766966)Instruction limit reached! % 7.41/1.31 % (766966)------------------------------ % 7.41/1.31 % (766966)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.41/1.31 % (766966)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.41/1.31 % (766966)CaDiCaL version: 2.1.3 % 7.41/1.31 % (766966)Termination reason: Instruction limit % 7.41/1.31 % (766966)Termination phase: Saturation % 7.41/1.31 % (766966)Time elapsed: 0.029 s % 7.41/1.31 % (766966)Peak memory usage: 12 MB % 7.41/1.31 % (766966)Instructions burned: 120 (million) % 7.41/1.31 % (766976)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3717338016:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 7.41/1.31 % (766965)Instruction limit reached! % 7.41/1.31 % (766965)------------------------------ % 7.41/1.31 % (766965)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.41/1.31 % (766965)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.41/1.31 % (766965)CaDiCaL version: 2.1.3 % 7.41/1.31 % (766965)Termination reason: Instruction limit % 7.41/1.31 % (766965)Termination phase: Saturation % 7.41/1.31 % (766965)Time elapsed: 0.062 s % 7.41/1.31 % (766965)Peak memory usage: 12 MB % 7.41/1.31 % (766965)Instructions burned: 104 (million) % 7.41/1.31 % TRYING [1] % 7.41/1.31 % TRYING [2] % 7.41/1.31 % TRYING [1] % 7.41/1.31 % TRYING [2] % 7.41/1.31 % (766968)Instruction limit reached! % 7.41/1.31 % (766968)------------------------------ % 7.41/1.31 % (766968)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.41/1.31 % (766968)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.41/1.31 % (766968)CaDiCaL version: 2.1.3 % 7.41/1.31 % (766968)Termination reason: Instruction limit % 7.41/1.31 % (766968)Termination phase: Saturation % 7.41/1.31 % (766968)Time elapsed: 0.077 s % 7.41/1.31 % (766968)Peak memory usage: 13 MB % 7.41/1.31 % (766968)Instructions burned: 160 (million) % 7.41/1.31 % (766967)Instruction limit reached! % 7.41/1.31 % (766967)------------------------------ % 7.41/1.31 % (766967)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.41/1.31 % (766967)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.41/1.31 % (766967)CaDiCaL version: 2.1.3 % 7.41/1.31 % (766967)Termination reason: Instruction limit % 7.41/1.31 % (766967)Termination phase: Saturation % 7.41/1.31 % (766967)Time elapsed: 0.078 s % 7.41/1.31 % (766967)Peak memory usage: 13 MB % 7.41/1.31 % (766967)Instructions burned: 133 (million) % 7.41/1.31 % (766978)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2794741668:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi) % 7.41/1.31 % (766980)ott-21_1_sil=16000:fs=off:random_seed=2553157397:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 7.41/1.31 % (766979)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=1903786214:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi) % 7.41/1.31 % (766978)Instruction limit reached! % 7.41/1.31 % (766978)------------------------------ % 7.41/1.31 % (766978)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.41/1.31 % (766978)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.41/1.31 % (766978)CaDiCaL version: 2.1.3 % 22.50/3.43 % (766978)Termination reason: Instruction limit % 22.50/3.43 % (766978)Termination phase: Saturation % 22.50/3.43 % (766978)Time elapsed: 0.079 s % 22.50/3.43 % (766978)Peak memory usage: 13 MB % 22.50/3.43 % (766978)Instructions burned: 131 (million) % 22.50/3.43 % (766976)Instruction limit reached! % 22.50/3.43 % (766976)------------------------------ % 22.50/3.43 % (766976)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.50/3.43 % (766976)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.50/3.43 % (766976)CaDiCaL version: 2.1.3 % 22.50/3.43 % (766976)Termination reason: Instruction limit % 22.50/3.43 % (766976)Termination phase: Finite model building constraint generation % 22.50/3.43 % (766976)Time elapsed: 0.131 s % 22.50/3.43 % (766976)Peak memory usage: 19 MB % 22.50/3.43 % (766976)Instructions burned: 716 (million) % 22.50/3.43 % (766985)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=517013145:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi) % 22.50/3.43 % (766984)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3226501787:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi) % 22.50/3.43 % (766980)Instruction limit reached! % 22.50/3.43 % (766980)------------------------------ % 22.50/3.43 % (766980)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.50/3.43 % (766980)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.50/3.43 % (766980)CaDiCaL version: 2.1.3 % 22.50/3.43 % (766980)Termination reason: Instruction limit % 22.50/3.43 % (766980)Termination phase: Saturation % 22.50/3.43 % (766980)Time elapsed: 0.099 s % 22.50/3.43 % (766980)Peak memory usage: 14 MB % 22.50/3.43 % (766980)Instructions burned: 181 (million) % 22.50/3.43 % TRYING [1] % 22.50/3.43 % (766988)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1437030561:i=1179_2997 on theBenchmark for (2997ds/1179Mi) % 22.50/3.43 % (766979)Instruction limit reached! % 22.50/3.43 % (766979)------------------------------ % 22.50/3.43 % (766979)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.50/3.43 % (766979)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.50/3.43 % (766979)CaDiCaL version: 2.1.3 % 22.50/3.43 % (766979)Termination reason: Instruction limit % 22.50/3.43 % (766979)Termination phase: Saturation % 22.50/3.43 % (766979)Time elapsed: 0.295 s % 22.50/3.43 % (766979)Peak memory usage: 17 MB % 22.50/3.43 % (766979)Instructions burned: 685 (million) % 22.50/3.43 % (766990)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=195673880:i=889:ins=1_2995 on theBenchmark for (2995ds/889Mi) % 22.50/3.43 % (766985)Instruction limit reached! % 22.50/3.43 % (766985)------------------------------ % 22.50/3.43 % (766985)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.50/3.43 % (766985)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.50/3.43 % (766985)CaDiCaL version: 2.1.3 % 22.50/3.43 % (766985)Termination reason: Instruction limit % 22.50/3.43 % (766985)Termination phase: Finite model building constraint generation % 22.50/3.43 % (766985)Time elapsed: 0.243 s % 22.50/3.43 % (766985)Peak memory usage: 102 MB % 22.50/3.43 % (766985)Instructions burned: 867 (million) % 22.50/3.43 % (766992)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=2244795809:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2995 on theBenchmark for (2995ds/692Mi) % 22.50/3.43 % (766984)Instruction limit reached! % 22.50/3.43 % (766984)------------------------------ % 22.50/3.43 % (766984)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.50/3.43 % (766984)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.50/3.43 % (766984)CaDiCaL version: 2.1.3 % 22.50/3.43 % (766984)Termination reason: Instruction limit % 22.50/3.43 % (766984)Termination phase: Saturation % 22.50/3.43 % (766984)Time elapsed: 0.282 s % 22.50/3.43 % (766984)Peak memory usage: 15 MB % 22.50/3.43 % (766984)Instructions burned: 477 (million) % 22.50/3.43 % (766990)Cannot represent all propositional literals internally % 22.50/3.43 % (766990)Refutation not found, incomplete strategy % 22.50/3.43 % (766990)------------------------------ % 22.50/3.43 % (766990)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.50/3.43 % (766990)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.50/3.43 % (766990)CaDiCaL version: 2.1.3 % 22.50/3.43 % (766990)Termination reason: Refutation not found, incomplete strategy % 65.76/9.57 % (766990)Time elapsed: 0.064 s % 65.76/9.57 % (766990)Peak memory usage: 12 MB % 65.76/9.57 % (766990)Instructions burned: 124 (million) % 65.76/9.57 % (766990)------------------------------ % 65.76/9.57 % (766990)------------------------------ % 65.76/9.57 % (766994)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3128836524:i=879:kws=inv_precedence:fsr=off_2994 on theBenchmark for (2994ds/879Mi) % 65.76/9.57 % (766995)fmb+10_1_sil=64000:random_seed=3225609243:i=22061:nm=2:gsp=on_2994 on theBenchmark for (2994ds/22061Mi) % 65.76/9.57 % TRYING [1] % 65.76/9.57 % (766992)Instruction limit reached! % 65.76/9.57 % (766992)------------------------------ % 65.76/9.57 % (766992)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 65.76/9.57 % (766992)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 65.76/9.57 % (766992)CaDiCaL version: 2.1.3 % 65.76/9.57 % (766992)Termination reason: Instruction limit % 65.76/9.57 % (766992)Termination phase: Saturation % 65.76/9.57 % (766992)Time elapsed: 0.202 s % 65.76/9.57 % (766992)Peak memory usage: 20 MB % 65.76/9.57 % (766992)Instructions burned: 694 (million) % 65.76/9.57 % (766998)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2308156573:i=9515:nm=5_2993 on theBenchmark for (2993ds/9515Mi) % 65.76/9.57 % (766998)Cannot represent all propositional literals internally % 65.76/9.57 % (766998)Refutation not found, incomplete strategy % 65.76/9.57 % (766998)------------------------------ % 65.76/9.57 % (766998)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 65.76/9.57 % (766998)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 65.76/9.57 % (766998)CaDiCaL version: 2.1.3 % 65.76/9.57 % (766998)Termination reason: Refutation not found, incomplete strategy % 65.76/9.57 % (766998)Time elapsed: 0.033 s % 65.76/9.57 % (766998)Peak memory usage: 12 MB % 65.76/9.57 % (766998)Instructions burned: 120 (million) % 65.76/9.57 % (766998)------------------------------ % 65.76/9.57 % (766998)------------------------------ % 65.76/9.57 % (767000)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=490414910:fmbsr=1.7:i=920_2992 on theBenchmark for (2992ds/920Mi) % 65.76/9.57 % (767000)Cannot represent all propositional literals internally % 65.76/9.57 % (767000)Refutation not found, incomplete strategy % 65.76/9.57 % (767000)------------------------------ % 65.76/9.57 % (767000)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 65.76/9.57 % (767000)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 65.76/9.57 % (767000)CaDiCaL version: 2.1.3 % 65.76/9.57 % (767000)Termination reason: Refutation not found, incomplete strategy % 65.76/9.57 % (767000)Time elapsed: 0.034 s % 65.76/9.57 % (767000)Peak memory usage: 12 MB % 65.76/9.57 % (767000)Instructions burned: 120 (million) % 65.76/9.57 % (767000)------------------------------ % 65.76/9.57 % (767000)------------------------------ % 65.76/9.57 % (767002)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=3320813401:i=5131_2992 on theBenchmark for (2992ds/5131Mi) % 65.76/9.57 % (766988)Instruction limit reached! % 65.76/9.57 % (766988)------------------------------ % 65.76/9.57 % (766988)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 65.76/9.57 % (766988)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 65.76/9.57 % (766988)CaDiCaL version: 2.1.3 % 65.76/9.57 % (766988)Termination reason: Instruction limit % 65.76/9.57 % (766988)Termination phase: Saturation % 65.76/9.57 % (766988)Time elapsed: 0.658 s % 65.76/9.57 % (766988)Peak memory usage: 28 MB % 65.76/9.57 % (766988)Instructions burned: 1179 (million) % 65.76/9.57 % (767004)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3052274360:i=1472:ins=7:fdi=8:gsp=on_2990 on theBenchmark for (2990ds/1472Mi) % 65.76/9.57 % (766994)Instruction limit reached! % 65.76/9.57 % (766994)------------------------------ % 65.76/9.57 % (766994)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 65.76/9.57 % (766994)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 65.76/9.57 % (766994)CaDiCaL version: 2.1.3 % 65.76/9.57 % (766994)Termination reason: Instruction limit % 65.76/9.57 % (766994)Termination phase: Saturation % 65.76/9.57 % (766994)Time elapsed: 0.477 s % 65.76/9.57 % (766994)Peak memory usage: 18 MB % 65.76/9.57 % (766994)Instructions burned: 880 (million) % 65.76/9.57 % (767006)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=938371341:i=6324_2989 on theBenchmark for (2989ds/6324Mi) % 65.76/9.57 % (767006)Cannot represent all propositional literals internally % 106.19/15.23 % (767006)Refutation not found, incomplete strategy % 106.19/15.23 % (767006)------------------------------ % 106.19/15.23 % (767006)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 106.19/15.23 % (767006)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 106.19/15.23 % (767006)CaDiCaL version: 2.1.3 % 106.19/15.23 % (767006)Termination reason: Refutation not found, incomplete strategy % 106.19/15.23 % (767006)Time elapsed: 0.067 s % 106.19/15.23 % (767006)Peak memory usage: 13 MB % 106.19/15.23 % (767006)Instructions burned: 123 (million) % 106.19/15.23 % (767006)------------------------------ % 106.19/15.23 % (767006)------------------------------ % 106.19/15.23 % (767008)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1782739745:fmbsr=2.30978:i=2174_2989 on theBenchmark for (2989ds/2174Mi) % 106.19/15.23 % (767004)Instruction limit reached! % 106.19/15.23 % (767004)------------------------------ % 106.19/15.23 % (767004)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 106.19/15.23 % (767004)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 106.19/15.23 % (767004)CaDiCaL version: 2.1.3 % 106.19/15.23 % (767004)Termination reason: Instruction limit % 106.19/15.23 % (767004)Termination phase: Saturation % 106.19/15.23 % (767004)Time elapsed: 0.670 s % 106.19/15.23 % (767004)Peak memory usage: 23 MB % 106.19/15.23 % (767004)Instructions burned: 1472 (million) % 106.19/15.23 % (767010)ott-2_1_sil=16000:newcnf=on:random_seed=426775342:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2983 on theBenchmark for (2983ds/869Mi) % 106.19/15.23 % (767008)Cannot represent all propositional literals internally % 106.19/15.23 % (767008)Refutation not found, incomplete strategy % 106.19/15.23 % (767008)------------------------------ % 106.19/15.23 % (767008)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 106.19/15.23 % (767008)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 106.19/15.23 % (767008)CaDiCaL version: 2.1.3 % 106.19/15.23 % (767008)Termination reason: Refutation not found, incomplete strategy % 106.19/15.23 % (767008)Time elapsed: 0.520 s % 106.19/15.23 % (767008)Peak memory usage: 18 MB % 106.19/15.23 % (767008)Instructions burned: 947 (million) % 106.19/15.23 % (767008)------------------------------ % 106.19/15.23 % (767008)------------------------------ % 106.19/15.23 % (767012)ott+10_1_sil=32000:tgt=ground:random_seed=3466248331:i=5114:av=off_2983 on theBenchmark for (2983ds/5114Mi) % 106.19/15.23 % (767010)Instruction limit reached! % 106.19/15.23 % (767010)------------------------------ % 106.19/15.23 % (767010)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 106.19/15.23 % (767010)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 106.19/15.23 % (767010)CaDiCaL version: 2.1.3 % 106.19/15.23 % (767010)Termination reason: Instruction limit % 106.19/15.23 % (767010)Termination phase: Saturation % 106.19/15.23 % (767010)Time elapsed: 0.481 s % 106.19/15.23 % (767010)Peak memory usage: 19 MB % 106.19/15.23 % (767010)Instructions burned: 869 (million) % 106.19/15.23 % (767014)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=3923881048:i=54282_2978 on theBenchmark for (2978ds/54282Mi) % 106.19/15.23 % TRYING [1] % 106.19/15.23 % TRYING [2] % 106.19/15.23 % (767002)Instruction limit reached! % 106.19/15.23 % (767002)------------------------------ % 106.19/15.23 % (767002)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 106.19/15.23 % (767002)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 106.19/15.23 % (767002)CaDiCaL version: 2.1.3 % 106.19/15.23 % (767002)Termination reason: Instruction limit % 106.19/15.23 % (767002)Termination phase: Saturation % 106.19/15.23 % (767002)Time elapsed: 1.417 s % 106.19/15.23 % (767002)Peak memory usage: 47 MB % 106.19/15.23 % (767002)Instructions burned: 5131 (million) % 106.19/15.23 % (767016)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=257735949:i=3512:aac=none_2977 on theBenchmark for (2977ds/3512Mi) % 106.19/15.23 % (767016)Instruction limit reached! % 106.19/15.23 % (767016)------------------------------ % 106.19/15.23 % (767016)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 106.19/15.23 % (767016)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 106.19/15.23 % (767016)CaDiCaL version: 2.1.3 % 106.19/15.23 % (767016)Termination reason: Instruction limit % 106.19/15.23 % (767016)Termination phase: Saturation % 106.19/15.23 % (767016)Time elapsed: 0.978 s % 106.19/15.23 % (767016)Peak memory usage: 37 MB % 106.19/15.23 % (767016)Instructions burned: 3515 (million) % 106.19/15.23 % (767018)dis+21_1_sil=32000:sas=cadical:random_seed=849638311:i=3773:amm=off_2967 on theBenchmark for (2967ds/3773Mi) % 162.48/23.17 % (767018)Instruction limit reached! % 162.48/23.17 % (767018)------------------------------ % 162.48/23.17 % (767018)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 162.48/23.17 % (767018)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 162.48/23.17 % (767018)CaDiCaL version: 2.1.3 % 162.48/23.17 % (767018)Termination reason: Instruction limit % 162.48/23.17 % (767018)Termination phase: Saturation % 162.48/23.17 % (767018)Time elapsed: 1.048 s % 162.48/23.17 % (767018)Peak memory usage: 39 MB % 162.48/23.17 % (767018)Instructions burned: 3774 (million) % 162.48/23.17 % (767020)ott+11_1_sil=16000:gs=on:random_seed=1678766681:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2957 on theBenchmark for (2957ds/2251Mi) % 162.48/23.17 % (767012)Instruction limit reached! % 162.48/23.17 % (767012)------------------------------ % 162.48/23.17 % (767012)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 162.48/23.17 % (767012)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 162.48/23.17 % (767012)CaDiCaL version: 2.1.3 % 162.48/23.17 % (767012)Termination reason: Instruction limit % 162.48/23.17 % (767012)Termination phase: Saturation % 162.48/23.17 % (767012)Time elapsed: 2.993 s % 162.48/23.17 % (767012)Peak memory usage: 93 MB % 162.48/23.17 % (767012)Instructions burned: 5114 (million) % 162.48/23.17 % (767022)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=3407701510:fmbsr=1.6:i=67534_2953 on theBenchmark for (2953ds/67534Mi) % 162.48/23.17 % (767022)Cannot represent all propositional literals internally % 162.48/23.17 % (767022)Refutation not found, incomplete strategy % 162.48/23.17 % (767022)------------------------------ % 162.48/23.17 % (767022)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 162.48/23.17 % (767022)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 162.48/23.17 % (767022)CaDiCaL version: 2.1.3 % 162.48/23.17 % (767022)Termination reason: Refutation not found, incomplete strategy % 162.48/23.17 % (767022)Time elapsed: 0.076 s % 162.48/23.17 % (767022)Peak memory usage: 12 MB % 162.48/23.17 % (767022)Instructions burned: 157 (million) % 162.48/23.17 % (767022)------------------------------ % 162.48/23.17 % (767022)------------------------------ % 162.48/23.17 % (767024)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=2198169457:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2952 on theBenchmark for (2952ds/4591Mi) % 162.48/23.17 % (767020)Instruction limit reached! % 162.48/23.17 % (767020)------------------------------ % 162.48/23.17 % (767020)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 162.48/23.17 % (767020)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 162.48/23.17 % (767020)CaDiCaL version: 2.1.3 % 162.48/23.17 % (767020)Termination reason: Instruction limit % 162.48/23.17 % (767020)Termination phase: Saturation % 162.48/23.17 % (767020)Time elapsed: 0.676 s % 162.48/23.17 % (767020)Peak memory usage: 39 MB % 162.48/23.17 % (767020)Instructions burned: 2254 (million) % 162.48/23.17 % (767026)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=5448185:i=29340_2950 on theBenchmark for (2950ds/29340Mi) % 162.48/23.17 % (767024)Instruction limit reached! % 162.48/23.17 % (767024)------------------------------ % 162.48/23.17 % (767024)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 162.48/23.17 % (767024)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 162.48/23.17 % (767024)CaDiCaL version: 2.1.3 % 162.48/23.17 % (767024)Termination reason: Instruction limit % 162.48/23.17 % (767024)Termination phase: Saturation % 162.48/23.17 % (767024)Time elapsed: 1.716 s % 162.48/23.17 % (767024)Peak memory usage: 25 MB % 162.48/23.17 % (767024)Instructions burned: 4592 (million) % 162.48/23.17 % (767028)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=2631440394:i=5211_2935 on theBenchmark for (2935ds/5211Mi) % 162.48/23.17 % (767028)Instruction limit reached! % 162.48/23.17 % (767028)------------------------------ % 162.48/23.17 % (767028)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 162.48/23.17 % (767028)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 162.48/23.17 % (767028)CaDiCaL version: 2.1.3 % 162.48/23.17 % (767028)Termination reason: Instruction limit % 162.48/23.17 % (767028)Termination phase: Saturation % 162.48/23.17 % (767028)Time elapsed: 2.814 s % 162.48/23.17 % (767028)Peak memory usage: 47 MB % 162.48/23.17 % (767028)Instructions burned: 5212 (million) % 162.48/23.17 % (767030)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=4124651891:i=5497:nm=2_2906 on theBenchmark for (2906ds/5497Mi) % 219.16/31.16 % (767030)Cannot represent all propositional literals internally % 219.16/31.16 % (767030)Refutation not found, incomplete strategy % 219.16/31.16 % (767030)------------------------------ % 219.16/31.16 % (767030)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 219.16/31.16 % (767030)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 219.16/31.16 % (767030)CaDiCaL version: 2.1.3 % 219.16/31.16 % (767030)Termination reason: Refutation not found, incomplete strategy % 219.16/31.16 % (767030)Time elapsed: 0.065 s % 219.16/31.16 % (767030)Peak memory usage: 12 MB % 219.16/31.16 % (767030)Instructions burned: 123 (million) % 219.16/31.16 % (767030)------------------------------ % 219.16/31.16 % (767030)------------------------------ % 219.16/31.16 % (767032)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=904118989:fmbsr=2:i=46332_2905 on theBenchmark for (2905ds/46332Mi) % 219.16/31.16 % (767032)Cannot represent all propositional literals internally % 219.16/31.16 % (767032)Refutation not found, incomplete strategy % 219.16/31.16 % (767032)------------------------------ % 219.16/31.16 % (767032)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 219.16/31.16 % (767032)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 219.16/31.16 % (767032)CaDiCaL version: 2.1.3 % 219.16/31.16 % (767032)Termination reason: Refutation not found, incomplete strategy % 219.16/31.16 % (767032)Time elapsed: 0.076 s % 219.16/31.16 % (767032)Peak memory usage: 12 MB % 219.16/31.16 % (767032)Instructions burned: 156 (million) % 219.16/31.16 % (767032)------------------------------ % 219.16/31.16 % (767032)------------------------------ % 219.16/31.16 % (767034)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=1345171719:i=14071_2904 on theBenchmark for (2904ds/14071Mi) % 219.16/31.16 % (767034)Cannot represent all propositional literals internally % 219.16/31.16 % (767034)Refutation not found, incomplete strategy % 219.16/31.16 % (767034)------------------------------ % 219.16/31.16 % (767034)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 219.16/31.16 % (767034)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 219.16/31.16 % (767034)CaDiCaL version: 2.1.3 % 219.16/31.16 % (767034)Termination reason: Refutation not found, incomplete strategy % 219.16/31.16 % (767034)Time elapsed: 0.065 s % 219.16/31.16 % (767034)Peak memory usage: 12 MB % 219.16/31.16 % (767034)Instructions burned: 127 (million) % 219.16/31.16 % (767034)------------------------------ % 219.16/31.16 % (767034)------------------------------ % 219.16/31.16 % (767036)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3614841662:i=22565:add=on:rawr=on_2903 on theBenchmark for (2903ds/22565Mi) % 219.16/31.16 % (766995)Instruction limit reached! % 219.16/31.16 % (766995)------------------------------ % 219.16/31.16 % (766995)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 219.16/31.16 % (766995)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 219.16/31.16 % (766995)CaDiCaL version: 2.1.3 % 219.16/31.16 % (766995)Termination reason: Instruction limit % 219.16/31.16 % (766995)Termination phase: Finite model building constraint generation % 219.16/31.16 % (766995)Time elapsed: 9.557 s % 219.16/31.16 % (766995)Peak memory usage: 2129 MB % 219.16/31.16 % (766995)Instructions burned: 22063 (million) % 219.16/31.16 % (767038)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=2488566561:i=8173:av=off_2895 on theBenchmark for (2895ds/8173Mi) % 219.16/31.16 % (767026)Instruction limit reached! % 219.16/31.16 % (767026)------------------------------ % 219.16/31.16 % (767026)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 219.16/31.16 % (767026)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 219.16/31.16 % (767026)CaDiCaL version: 2.1.3 % 219.16/31.16 % (767026)Termination reason: Instruction limit % 219.16/31.16 % (767026)Termination phase: Saturation % 219.16/31.16 % (767026)Time elapsed: 7.456 s % 219.16/31.16 % (767026)Peak memory usage: 262 MB % 219.16/31.16 % (767026)Instructions burned: 29343 (million) % 219.16/31.16 % (767040)dis+10_16:1_sil=16000:random_seed=1132348868:i=9155:fsr=off_2875 on theBenchmark for (2875ds/9155Mi) % 219.16/31.16 % (767040)Instruction limit reached! % 219.16/31.16 % (767040)------------------------------ % 219.16/31.16 % (767040)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 219.16/31.16 % (767040)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 219.16/31.16 % (767040)CaDiCaL version: 2.1.3 % 219.16/31.16 % (767040)Termination reason: Instruction limit % 204.66/35.06 % (767040)Termination phase: Saturation % 204.66/35.06 % (767040)Time elapsed: 2.552 s % 204.66/35.06 % (767040)Peak memory usage: 72 MB % 204.66/35.06 % (767040)Instructions burned: 9158 (million) % 204.66/35.06 % (767042)ott-3_8_sil=64000:random_seed=3721401646:i=20139:bs=on_2849 on theBenchmark for (2849ds/20139Mi) % 204.66/35.06 % (767038)Instruction limit reached! % 204.66/35.06 % (767038)------------------------------ % 204.66/35.06 % (767038)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 204.66/35.06 % (767038)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 204.66/35.06 % (767038)CaDiCaL version: 2.1.3 % 204.66/35.06 % (767038)Termination reason: Instruction limit % 204.66/35.06 % (767038)Termination phase: Saturation % 204.66/35.06 % (767038)Time elapsed: 4.772 s % 204.66/35.06 % (767038)Peak memory usage: 136 MB % 204.66/35.06 % (767038)Instructions burned: 8175 (million) % 204.66/35.06 % (767044)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=709290929:fmbsr=2:i=32576_2847 on theBenchmark for (2847ds/32576Mi) % 204.66/35.06 % (767044)Cannot represent all propositional literals internally % 204.66/35.06 % (767044)Refutation not found, incomplete strategy % 204.66/35.06 % (767044)------------------------------ % 204.66/35.06 % (767044)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 204.66/35.06 % (767044)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 204.66/35.06 % (767044)CaDiCaL version: 2.1.3 % 204.66/35.06 % (767044)Termination reason: Refutation not found, incomplete strategy % 204.66/35.06 % (767044)Time elapsed: 0.067 s % 204.66/35.06 % (767044)Peak memory usage: 12 MB % 204.66/35.06 % (767044)Instructions burned: 130 (million) % 204.66/35.06 % (767044)------------------------------ % 204.66/35.06 % (767044)------------------------------ % 204.66/35.06 % (767046)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=3395880937:i=11404_2846 on theBenchmark for (2846ds/11404Mi) % 204.66/35.06 % (767042)Instruction limit reached! % 204.66/35.06 % (767042)------------------------------ % 204.66/35.06 % (767042)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 204.66/35.06 % (767042)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 204.66/35.06 % (767042)CaDiCaL version: 2.1.3 % 204.66/35.06 % (767042)Termination reason: Instruction limit % 204.66/35.06 % (767042)Termination phase: Saturation % 204.66/35.06 % (767042)Time elapsed: 3.125 s % 204.66/35.06 % (767042)Peak memory usage: 12 MB % 204.66/35.06 % (767042)Instructions burned: 20145 (million) % 204.66/35.06 % (767048)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=18018560:i=14134_2818 on theBenchmark for (2818ds/14134Mi) % 204.66/35.06 % (767046)Instruction limit reached! % 204.66/35.06 % (767046)------------------------------ % 204.66/35.06 % (767046)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 204.66/35.06 % (767046)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 204.66/35.06 % (767046)CaDiCaL version: 2.1.3 % 204.66/35.06 % (767046)Termination reason: Instruction limit % 204.66/35.06 % (767046)Termination phase: Saturation % 204.66/35.06 % (767046)Time elapsed: 6.718 s % 204.66/35.06 % (767046)Peak memory usage: 185 MB % 204.66/35.06 % (767046)Instructions burned: 11404 (million) % 204.66/35.06 % (767050)dis+33_16_sil=32000:sac=on:random_seed=728051664:i=15851:nm=0_2778 on theBenchmark for (2778ds/15851Mi) % 204.66/35.06 % (767048)Instruction limit reached! % 204.66/35.06 % (767048)------------------------------ % 204.66/35.06 % (767048)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 204.66/35.06 % (767048)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 204.66/35.06 % (767048)CaDiCaL version: 2.1.3 % 204.66/35.06 % (767048)Termination reason: Instruction limit % 204.66/35.06 % (767048)Termination phase: Saturation % 204.66/35.06 % (767048)Time elapsed: 4.541 s % 204.66/35.06 % (767048)Peak memory usage: 248 MB % 204.66/35.06 % (767048)Instructions burned: 14136 (million) % 204.66/35.06 % (767052)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=3630672812:avsq=on:i=17627:add=on:amm=off_2772 on theBenchmark for (2772ds/17627Mi) % 204.66/35.06 % (767036)Instruction limit reached! % 204.66/35.06 % (767036)------------------------------ % 204.66/35.06 % (767036)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 204.66/35.06 % (767036)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 204.66/35.06 % (767036)CaDiCaL version: 2.1.3 % 204.66/35.06 % (767036)Termination reason: Instruction limit % 204.66/35.06 % (767036)Termination phase: Saturation % 204.66/35.06 % (767036)Time elapsed: 13.330 s % 204.66/35.06 % (767036)Peak memory usage: 147 MB % 204.66/35.06 % (767036)Instructions burned: 22566 (million) % 262.06/37.24 % (767054)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=52112922:s2a=on:i=53295_2770 on theBenchmark for (2770ds/53295Mi) % 262.06/37.24 % (767052)Instruction limit reached! % 262.06/37.24 % (767052)------------------------------ % 262.06/37.24 % (767052)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 262.06/37.24 % (767052)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 262.06/37.24 % (767052)CaDiCaL version: 2.1.3 % 262.06/37.24 % (767052)Termination reason: Instruction limit % 262.06/37.24 % (767052)Termination phase: Saturation % 262.06/37.24 % (767052)Time elapsed: 3.013 s % 262.06/37.24 % (767052)Peak memory usage: 43 MB % 262.06/37.24 % (767052)Instructions burned: 17627 (million) % 262.06/37.24 % (767056)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=3544293815:i=26857:ins=20_2742 on theBenchmark for (2742ds/26857Mi) % 262.06/37.24 % (767056)Cannot represent all propositional literals internally % 262.06/37.24 % (767056)Refutation not found, incomplete strategy % 262.06/37.24 % (767056)------------------------------ % 262.06/37.24 % (767056)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 262.06/37.25 % (767056)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 262.06/37.25 % (767056)CaDiCaL version: 2.1.3 % 262.06/37.25 % (767056)Termination reason: Refutation not found, incomplete strategy % 262.06/37.25 % (767056)Time elapsed: 0.033 s % 262.06/37.25 % (767056)Peak memory usage: 12 MB % 262.06/37.25 % (767056)Instructions burned: 120 (million) % 262.06/37.25 % (767056)------------------------------ % 262.06/37.25 % (767056)------------------------------ % 262.06/37.25 % (767058)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=1440104409:i=28120:bs=on:fsr=off_2742 on theBenchmark for (2742ds/28120Mi) % 262.06/37.25 % (767050)Instruction limit reached! % 262.06/37.25 % (767050)------------------------------ % 262.06/37.25 % (767050)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 262.06/37.25 % (767050)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 262.06/37.25 % (767050)CaDiCaL version: 2.1.3 % 262.06/37.25 % (767050)Termination reason: Instruction limit % 262.06/37.25 % (767050)Termination phase: Saturation % 262.06/37.25 % (767050)Time elapsed: 8.539 s % 262.06/37.25 % (767050)Peak memory usage: 130 MB % 262.06/37.25 % (767050)Instructions burned: 15852 (million) % 262.06/37.25 % (767060)fmb+10_1_sil=256000:fmbss=7:random_seed=1115125843:fmbsr=1.6:i=182295_2693 on theBenchmark for (2693ds/182295Mi) % 262.06/37.25 % (767060)Cannot represent all propositional literals internally % 262.06/37.25 % (767060)Refutation not found, incomplete strategy % 262.06/37.25 % (767060)------------------------------ % 262.06/37.25 % (767060)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 262.06/37.25 % (767060)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 262.06/37.25 % (767060)CaDiCaL version: 2.1.3 % 262.06/37.25 % (767060)Termination reason: Refutation not found, incomplete strategy % 262.06/37.25 % (767060)Time elapsed: 0.063 s % 262.06/37.25 % (767060)Peak memory usage: 12 MB % 262.06/37.25 % (767060)Instructions burned: 120 (million) % 262.06/37.25 % (767060)------------------------------ % 262.06/37.25 % (767060)------------------------------ % 262.06/37.25 % (767062)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=3424659995:i=44625:gsp=on_2692 on theBenchmark for (2692ds/44625Mi) % 262.06/37.25 % (767062)Cannot represent all propositional literals internally % 262.06/37.25 % (767062)Refutation not found, incomplete strategy % 262.06/37.25 % (767062)------------------------------ % 262.06/37.25 % (767062)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 262.06/37.25 % (767062)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 262.06/37.25 % (767062)CaDiCaL version: 2.1.3 % 262.06/37.25 % (767062)Termination reason: Refutation not found, incomplete strategy % 262.06/37.25 % (767062)Time elapsed: 0.063 s % 262.06/37.25 % (767062)Peak memory usage: 12 MB % 262.06/37.25 % (767062)Instructions burned: 120 (million) % 262.06/37.25 % (767062)------------------------------ % 262.06/37.25 % (767062)------------------------------ % 262.06/37.25 % (767064)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=3066601470:i=160505_2691 on theBenchmark for (2691ds/160505Mi) % 262.06/37.25 % (767064)Cannot represent all propositional literals internally % 262.06/37.25 % (767064)Refutation not found, incomplete strategy % 262.06/37.25 % (767064)------------------------------ % 262.06/37.25 % (767064)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 262.06/37.25 % (767064)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 288.39/41.01 % (767064)CaDiCaL version: 2.1.3 % 288.39/41.01 % (767064)Termination reason: Refutation not found, incomplete strategy % 288.39/41.01 % (767064)Time elapsed: 0.063 s % 288.39/41.01 % (767064)Peak memory usage: 12 MB % 288.39/41.01 % (767064)Instructions burned: 120 (million) % 288.39/41.01 % (767064)------------------------------ % 288.39/41.01 % (767064)------------------------------ % 288.39/41.01 % (767066)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=2577973025:fmbsr=1.3:i=225729_2690 on theBenchmark for (2690ds/225729Mi) % 288.39/41.01 % (767066)Cannot represent all propositional literals internally % 288.39/41.01 % (767066)Refutation not found, incomplete strategy % 288.39/41.01 % (767066)------------------------------ % 288.39/41.01 % (767066)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 288.39/41.01 % (767066)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 288.39/41.01 % (767066)CaDiCaL version: 2.1.3 % 288.39/41.01 % (767066)Termination reason: Refutation not found, incomplete strategy % 288.39/41.01 % (767066)Time elapsed: 0.066 s % 288.39/41.01 % (767066)Peak memory usage: 12 MB % 288.39/41.01 % (767066)Instructions burned: 127 (million) % 288.39/41.01 % (767066)------------------------------ % 288.39/41.01 % (767066)------------------------------ % 288.39/41.01 % (767068)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=1094063257:fmbsr=2:i=185024:ins=7_2689 on theBenchmark for (2689ds/185024Mi) % 288.39/41.01 % (767068)Cannot represent all propositional literals internally % 288.39/41.01 % (767068)Refutation not found, incomplete strategy % 288.39/41.01 % (767068)------------------------------ % 288.39/41.01 % (767068)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 288.39/41.01 % (767068)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 288.39/41.01 % (767068)CaDiCaL version: 2.1.3 % 288.39/41.01 % (767068)Termination reason: Refutation not found, incomplete strategy % 288.39/41.01 % (767068)Time elapsed: 0.066 s % 288.39/41.01 % (767068)Peak memory usage: 12 MB % 288.39/41.01 % (767068)Instructions burned: 127 (million) % 288.39/41.01 % (767068)------------------------------ % 288.39/41.01 % (767068)------------------------------ % 288.39/41.01 % (767070)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=250234103:rtra=on_2688 on theBenchmark for (2688ds/0Mi) % 288.39/41.01 % TRYING [1] % 288.39/41.01 % TRYING [2] % 288.39/41.01 % (766964)Instruction limit reached! % 288.39/41.01 % (766964)------------------------------ % 288.39/41.01 % (766964)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 288.39/41.01 % (766964)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 288.39/41.01 % (766964)CaDiCaL version: 2.1.3 % 288.39/41.01 % (766964)Termination reason: Instruction limit % 288.39/41.01 % (766964)Termination phase: Saturation % 288.39/41.01 % (766964)Time elapsed: 31.345 s % 288.39/41.01 % (766964)Peak memory usage: 184 MB % 288.39/41.01 % (766964)Instructions burned: 88027 (million) % 288.39/41.01 % (767072)% WARNING: option uhcvi not known. % 288.39/41.01 % (767072)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1488449906:i=271062:add=off:rtra=on:rawr=on_2685 on theBenchmark for (2685ds/271062Mi) % 288.39/41.01 % (767014)Instruction limit reached! % 288.39/41.01 % (767014)------------------------------ % 288.39/41.01 % (767014)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 288.39/41.01 % (767014)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 288.39/41.01 % (767014)CaDiCaL version: 2.1.3 % 288.39/41.01 % (767014)Termination reason: Instruction limit % 288.39/41.01 % (767014)Termination phase: Finite model building constraint generation % 288.39/41.01 % (767014)Time elapsed: 32.286 s % 288.39/41.01 % (767014)Peak memory usage: 10689 MB % 288.39/41.01 % (767014)Instructions burned: 54286 (million) % 288.39/41.01 % (767058)Instruction limit reached! % 288.39/41.01 % (767058)------------------------------ % 288.39/41.01 % (767058)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 288.39/41.01 % (767058)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 288.39/41.01 % (767058)CaDiCaL version: 2.1.3 % 288.39/41.01 % (767058)Termination reason: Instruction limit % 288.39/41.01 % (767058)Termination phase: Saturation % 288.39/41.01 % (767058)Time elapsed: 8.998 s % 288.39/41.01 % (767058)Peak memory usage: 307 MB % 288.39/41.01 % (767058)Instructions burned: 28121 (million) % 288.39/41.01 % (767074)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=4018457490:i=176048:add=on:rtra=on:rawr=on_2651 on theBenchmark forTerminated % 300.45/42.64 % Vampire exiting %------------------------------------------------------------------------------