%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWW252+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 : n001.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 29 01:39:42 PM UTC 2026 % Result : Timeout 300.49s 42.74s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.04 % Problem : SWW252+1 : TPTP v9.3.1. Released v5.2.0. % 0.00/0.08 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.11/0.28 % Computer : n001.cluster.edu % 0.11/0.28 % Model : x86_64 x86_64 % 0.11/0.28 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.28 % Memory : 8046.5625MB % 0.11/0.28 % OS : Linux 6.8.0-71-generic % 0.11/0.29 % CPULimit : 300 % 0.11/0.29 % WCLimit : 300 % 0.11/0.29 % DateTime : Mon Sep 28 13:30:03 UTC 2026 % 0.12/0.29 % CPUTime : % 0.12/0.29 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.12/0.34 Running first-order model finding % 0.12/0.34 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 % 28.41/4.46 % (350783)Will run a generic schedule for satisfiability detection. % 28.41/4.46 % (350789)% WARNING: option uhcvi not known. % 28.41/4.46 % (350789)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1464721543:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 28.41/4.46 % (350791)dis+10_1_sil=32000:sp=arity:random_seed=331143160:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 28.41/4.46 % (350788)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=4291432142_2999 on theBenchmark for (2999ds/0Mi) % 28.41/4.46 % (350792)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1775828997:i=116_2999 on theBenchmark for (2999ds/116Mi) % 28.41/4.46 % (350793)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3749586436:i=131_2999 on theBenchmark for (2999ds/131Mi) % 28.41/4.46 % (350794)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=79350303:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 28.41/4.46 % (350790)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=4193382143:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 28.41/4.46 % (350791)Instruction limit reached! % 28.41/4.46 % (350791)------------------------------ % 28.41/4.46 % (350791)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 28.41/4.46 % (350791)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.41/4.46 % (350791)CaDiCaL version: 2.1.3 % 28.41/4.46 % (350791)Termination reason: Instruction limit % 28.41/4.46 % (350791)Termination phase: Saturation % 28.41/4.46 % (350791)Time elapsed: 0.088 s % 28.41/4.46 % (350791)Peak memory usage: 13 MB % 28.41/4.46 % (350791)Instructions burned: 103 (million) % 28.41/4.46 % (350792)Instruction limit reached! % 28.41/4.46 % (350792)------------------------------ % 28.41/4.46 % (350792)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 28.41/4.46 % (350792)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.41/4.46 % (350792)CaDiCaL version: 2.1.3 % 28.41/4.46 % (350792)Termination reason: Instruction limit % 28.41/4.46 % (350792)Termination phase: Property scanning % 28.41/4.46 % (350792)Time elapsed: 0.102 s % 28.41/4.46 % (350792)Peak memory usage: 14 MB % 28.41/4.46 % (350792)Instructions burned: 116 (million) % 28.41/4.46 % (350793)Instruction limit reached! % 28.41/4.46 % (350793)------------------------------ % 28.41/4.46 % (350793)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 28.41/4.46 % (350793)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.41/4.46 % (350793)CaDiCaL version: 2.1.3 % 28.41/4.46 % (350793)Termination reason: Instruction limit % 28.41/4.46 % (350793)Termination phase: Saturation % 28.41/4.46 % (350793)Time elapsed: 0.119 s % 28.41/4.46 % (350793)Peak memory usage: 14 MB % 28.41/4.46 % (350793)Instructions burned: 132 (million) % 28.41/4.46 % (350802)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2607989576:i=714:nm=2_2997 on theBenchmark for (2997ds/714Mi) % 28.41/4.46 % (350803)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2686199094:i=131:bd=preordered:fsd=on_2997 on theBenchmark for (2997ds/131Mi) % 28.41/4.46 % (350804)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=182810419:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2997 on theBenchmark for (2997ds/684Mi) % 28.41/4.46 % (350794)Instruction limit reached! % 28.41/4.46 % (350794)------------------------------ % 28.41/4.46 % (350794)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 28.41/4.46 % (350794)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.41/4.46 % (350794)CaDiCaL version: 2.1.3 % 28.41/4.46 % (350794)Termination reason: Instruction limit % 28.41/4.46 % (350794)Termination phase: Saturation % 28.41/4.46 % (350794)Time elapsed: 0.151 s % 28.41/4.46 % (350794)Peak memory usage: 16 MB % 28.41/4.46 % (350794)Instructions burned: 159 (million) % 28.41/4.46 % (350808)ott-21_1_sil=16000:fs=off:random_seed=1437477614:i=180:av=off:fsr=off_2997 on theBenchmark for (2997ds/180Mi) % 28.41/4.46 % (350803)Instruction limit reached! % 28.41/4.46 % (350803)------------------------------ % 28.41/4.46 % (350803)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 28.41/4.46 % (350803)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.41/4.46 % (350803)CaDiCaL version: 2.1.3 % 28.41/4.46 % (350803)Termination reason: Instruction limit % 73.52/10.81 % (350803)Termination phase: Property scanning % 73.52/10.81 % (350803)Time elapsed: 0.115 s % 73.52/10.81 % (350803)Peak memory usage: 14 MB % 73.52/10.81 % (350803)Instructions burned: 131 (million) % 73.52/10.81 % (350810)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=284606581:i=477:bd=all_2996 on theBenchmark for (2996ds/477Mi) % 73.52/10.81 % (350808)Instruction limit reached! % 73.52/10.81 % (350808)------------------------------ % 73.52/10.81 % (350808)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 73.52/10.81 % (350808)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 73.52/10.81 % (350808)CaDiCaL version: 2.1.3 % 73.52/10.81 % (350808)Termination reason: Instruction limit % 73.52/10.81 % (350808)Termination phase: Saturation % 73.52/10.81 % (350808)Time elapsed: 0.166 s % 73.52/10.81 % (350808)Peak memory usage: 14 MB % 73.52/10.81 % (350808)Instructions burned: 180 (million) % 73.52/10.81 % (350812)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=4225476142:fmbsr=1.3:i=865:ins=25_2995 on theBenchmark for (2995ds/865Mi) % 73.52/10.81 % (350802)Instruction limit reached! % 73.52/10.81 % (350802)------------------------------ % 73.52/10.81 % (350802)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 73.52/10.81 % (350802)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 73.52/10.81 % (350802)CaDiCaL version: 2.1.3 % 73.52/10.81 % (350802)Termination reason: Instruction limit % 73.52/10.81 % (350802)Termination phase: Finite model building preprocessing % 73.52/10.81 % (350802)Time elapsed: 0.619 s % 73.52/10.81 % (350802)Peak memory usage: 22 MB % 73.52/10.81 % (350802)Instructions burned: 714 (million) % 73.52/10.81 % (350814)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1293995580:i=1179_2991 on theBenchmark for (2991ds/1179Mi) % 73.52/10.81 % (350810)Instruction limit reached! % 73.52/10.81 % (350810)------------------------------ % 73.52/10.81 % (350810)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 73.52/10.81 % (350810)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 73.52/10.81 % (350810)CaDiCaL version: 2.1.3 % 73.52/10.81 % (350810)Termination reason: Instruction limit % 73.52/10.81 % (350810)Termination phase: Saturation % 73.52/10.81 % (350810)Time elapsed: 0.504 s % 73.52/10.81 % (350810)Peak memory usage: 16 MB % 73.52/10.81 % (350810)Instructions burned: 477 (million) % 73.52/10.81 % (350804)Instruction limit reached! % 73.52/10.81 % (350804)------------------------------ % 73.52/10.81 % (350804)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 73.52/10.81 % (350804)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 73.52/10.81 % (350804)CaDiCaL version: 2.1.3 % 73.52/10.81 % (350804)Termination reason: Instruction limit % 73.52/10.81 % (350804)Termination phase: Saturation % 73.52/10.81 % (350804)Time elapsed: 0.661 s % 73.52/10.81 % (350804)Peak memory usage: 20 MB % 73.52/10.81 % (350804)Instructions burned: 684 (million) % 73.52/10.81 % (350816)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=4132124650:i=889:ins=1_2990 on theBenchmark for (2990ds/889Mi) % 73.52/10.81 % (350817)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=998342143:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2990 on theBenchmark for (2990ds/692Mi) % 73.52/10.81 % TRYING [1] % 73.52/10.81 % (350812)Instruction limit reached! % 73.52/10.81 % (350812)------------------------------ % 73.52/10.81 % (350812)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 73.52/10.81 % (350812)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 73.52/10.81 % (350812)CaDiCaL version: 2.1.3 % 73.52/10.81 % (350812)Termination reason: Instruction limit % 73.52/10.81 % (350812)Termination phase: Finite model building preprocessing % 73.52/10.81 % (350812)Time elapsed: 0.757 s % 73.52/10.81 % (350812)Peak memory usage: 24 MB % 73.52/10.81 % (350812)Instructions burned: 865 (million) % 73.52/10.81 % (350820)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3154572980:i=879:kws=inv_precedence:fsr=off_2987 on theBenchmark for (2987ds/879Mi) % 73.52/10.81 % TRYING [2] % 73.52/10.81 % (350817)Instruction limit reached! % 73.52/10.81 % (350817)------------------------------ % 73.52/10.81 % (350817)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 73.52/10.81 % (350817)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 73.52/10.81 % (350817)CaDiCaL version: 2.1.3 % 73.52/10.81 % (350817)Termination reason: Instruction limit % 198.36/28.36 % (350817)Termination phase: Saturation % 198.36/28.36 % (350817)Time elapsed: 0.694 s % 198.36/28.36 % (350817)Peak memory usage: 20 MB % 198.36/28.36 % (350817)Instructions burned: 692 (million) % 198.36/28.36 % (350822)fmb+10_1_sil=64000:random_seed=1103711386:i=22061:nm=2:gsp=on_2983 on theBenchmark for (2983ds/22061Mi) % 198.36/28.36 % (350816)Instruction limit reached! % 198.36/28.36 % (350816)------------------------------ % 198.36/28.36 % (350816)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 198.36/28.36 % (350816)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 198.36/28.36 % (350816)CaDiCaL version: 2.1.3 % 198.36/28.36 % (350816)Termination reason: Instruction limit % 198.36/28.36 % (350816)Termination phase: Finite model building preprocessing % 198.36/28.36 % (350816)Time elapsed: 0.815 s % 198.36/28.36 % (350816)Peak memory usage: 28 MB % 198.36/28.36 % (350816)Instructions burned: 890 (million) % 198.36/28.36 % TRYING [3] % 198.36/28.36 % (350824)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2418971789:i=9515:nm=5_2982 on theBenchmark for (2982ds/9515Mi) % 198.36/28.36 % (350814)Instruction limit reached! % 198.36/28.36 % (350814)------------------------------ % 198.36/28.36 % (350814)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 198.36/28.36 % (350814)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 198.36/28.36 % (350814)CaDiCaL version: 2.1.3 % 198.36/28.36 % (350814)Termination reason: Instruction limit % 198.36/28.36 % (350814)Termination phase: Saturation % 198.36/28.36 % (350814)Time elapsed: 1.117 s % 198.36/28.36 % (350814)Peak memory usage: 25 MB % 198.36/28.36 % (350814)Instructions burned: 1180 (million) % 198.36/28.36 % (350820)Instruction limit reached! % 198.36/28.36 % (350820)------------------------------ % 198.36/28.36 % (350820)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 198.36/28.36 % (350820)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 198.36/28.36 % (350820)CaDiCaL version: 2.1.3 % 198.36/28.36 % (350820)Termination reason: Instruction limit % 198.36/28.36 % (350820)Termination phase: Saturation % 198.36/28.36 % (350820)Time elapsed: 0.742 s % 198.36/28.36 % (350820)Peak memory usage: 22 MB % 198.36/28.36 % (350820)Instructions burned: 879 (million) % 198.36/28.36 % (350826)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2395569376:fmbsr=1.7:i=920_2979 on theBenchmark for (2979ds/920Mi) % 198.36/28.36 % (350828)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1176148750:i=5131_2979 on theBenchmark for (2979ds/5131Mi) % 198.36/28.36 % TRYING [1] % 198.36/28.36 % (350826)Instruction limit reached! % 198.36/28.36 % (350826)------------------------------ % 198.36/28.36 % (350826)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 198.36/28.36 % (350826)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 198.36/28.36 % (350826)CaDiCaL version: 2.1.3 % 198.36/28.36 % (350826)Termination reason: Instruction limit % 198.36/28.36 % (350826)Termination phase: Finite model building preprocessing % 198.36/28.36 % (350826)Time elapsed: 0.822 s % 198.36/28.36 % (350826)Peak memory usage: 27 MB % 198.36/28.36 % (350826)Instructions burned: 921 (million) % 198.36/28.36 % (350830)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=4088989246:i=1472:ins=7:fdi=8:gsp=on_2971 on theBenchmark for (2971ds/1472Mi) % 198.36/28.36 % (350824)Cannot represent all propositional literals internally % 198.36/28.36 % (350824)Refutation not found, incomplete strategy % 198.36/28.36 % (350824)------------------------------ % 198.36/28.36 % (350824)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 198.36/28.36 % (350824)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 198.36/28.36 % (350824)CaDiCaL version: 2.1.3 % 198.36/28.36 % (350824)Termination reason: Refutation not found, incomplete strategy % 198.36/28.36 % (350824)Time elapsed: 1.097 s % 198.36/28.36 % (350824)Peak memory usage: 32 MB % 198.36/28.36 % (350824)Instructions burned: 1227 (million) % 198.36/28.36 % TRYING [2] % 198.36/28.36 % (350824)------------------------------ % 198.36/28.36 % (350824)------------------------------ % 198.36/28.36 % (350832)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=393530975:i=6324_2970 on theBenchmark for (2970ds/6324Mi) % 198.36/28.36 % (350832)Cannot represent all propositional literals internally % 198.36/28.36 % (350832)Refutation not found, incomplete strategy % 198.36/28.36 % (350832)------------------------------ % 198.36/28.36 % (350832)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 198.36/28.36 % (350832)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.49/42.74 % (350832)CaDiCaL version: 2.1.3 % 300.49/42.74 % (350832)Termination reason: Refutation not found, incomplete strategy % 300.49/42.74 % (350832)Time elapsed: 1.135 s % 300.49/42.74 % (350832)Peak memory usage: 33 MB % 300.49/42.74 % (350832)Instructions burned: 1263 (million) % 300.49/42.74 % (350832)------------------------------ % 300.49/42.74 % (350832)------------------------------ % 300.49/42.74 % (350834)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=841794276:fmbsr=2.30978:i=2174_2958 on theBenchmark for (2958ds/2174Mi) % 300.49/42.74 % (350830)Instruction limit reached! % 300.49/42.74 % (350830)------------------------------ % 300.49/42.74 % (350830)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.49/42.74 % (350830)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.49/42.74 % (350830)CaDiCaL version: 2.1.3 % 300.49/42.74 % (350830)Termination reason: Instruction limit % 300.49/42.74 % (350830)Termination phase: Saturation % 300.49/42.74 % (350830)Time elapsed: 1.276 s % 300.49/42.74 % (350830)Peak memory usage: 27 MB % 300.49/42.74 % (350830)Instructions burned: 1472 (million) % 300.49/42.74 % (350836)ott-2_1_sil=16000:newcnf=on:random_seed=753661358:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2958 on theBenchmark for (2958ds/869Mi) % 300.49/42.74 % TRYING [4] % 300.49/42.74 % TRYING [3] % 300.49/42.74 % (350836)Instruction limit reached! % 300.49/42.74 % (350836)------------------------------ % 300.49/42.74 % (350836)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.49/42.74 % (350836)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.49/42.74 % (350836)CaDiCaL version: 2.1.3 % 300.49/42.74 % (350836)Termination reason: Instruction limit % 300.49/42.74 % (350836)Termination phase: Saturation % 300.49/42.74 % (350836)Time elapsed: 0.753 s % 300.49/42.74 % (350836)Peak memory usage: 19 MB % 300.49/42.74 % (350836)Instructions burned: 869 (million) % 300.49/42.74 % (350838)ott+10_1_sil=32000:tgt=ground:random_seed=44980585:i=5114:av=off_2950 on theBenchmark for (2950ds/5114Mi) % 300.49/42.74 % (350834)Instruction limit reached! % 300.49/42.74 % (350834)------------------------------ % 300.49/42.74 % (350834)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.49/42.74 % (350834)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.49/42.74 % (350834)CaDiCaL version: 2.1.3 % 300.49/42.74 % (350834)Termination reason: Instruction limit % 300.49/42.74 % (350834)Termination phase: Finite model building preprocessing % 300.49/42.74 % (350834)Time elapsed: 1.923 s % 300.49/42.74 % (350834)Peak memory usage: 32 MB % 300.49/42.74 % (350834)Instructions burned: 2175 (million) % 300.49/42.74 % (350840)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2083591157:i=54282_2939 on theBenchmark for (2939ds/54282Mi) % 300.49/42.74 % (350828)Instruction limit reached! % 300.49/42.74 % (350828)------------------------------ % 300.49/42.74 % (350828)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.49/42.74 % (350828)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.49/42.74 % (350828)CaDiCaL version: 2.1.3 % 300.49/42.74 % (350828)Termination reason: Instruction limit % 300.49/42.74 % (350828)Termination phase: Saturation % 300.49/42.74 % (350828)Time elapsed: 4.875 s % 300.49/42.74 % (350828)Peak memory usage: 39 MB % 300.49/42.74 % (350828)Instructions burned: 5131 (million) % 300.49/42.74 % (350842)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=4113653347:i=3512:aac=none_2930 on theBenchmark for (2930ds/3512Mi) % 300.49/42.74 % TRYING [1] % 300.49/42.74 % TRYING [2] % 300.49/42.74 % TRYING [3] % 300.49/42.74 % (350838)Instruction limit reached! % 300.49/42.74 % (350838)------------------------------ % 300.49/42.74 % (350838)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.49/42.74 % (350838)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.49/42.74 % (350838)CaDiCaL version: 2.1.3 % 300.49/42.74 % (350838)Termination reason: Instruction limit % 300.49/42.74 % (350838)Termination phase: Saturation % 300.49/42.74 % (350838)Time elapsed: 5.039 s % 300.49/42.74 % (350838)Peak memory usage: 43 MB % 300.49/42.74 % (350838)Instructions burned: 5115 (million) % 300.49/42.74 % (350846)dis+21_1_sil=32000:sas=cadical:random_seed=2820627956:i=3773:amm=off_2899 on theBenchmark for (2899ds/3773Mi) % 300.49/42.74 % (350842)Instruction limit reached! % 300.49/42.74 % (350842)------------------------------ % 300.49/42.74 % (350842)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.49/42.74 % (350842)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.49/42.74 % (350842)CaDiCaL version: 2.1.3 % 300.49/42.74 % (350842)Termination r % 300.49/42.74 Terminated %------------------------------------------------------------------------------