%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : TOP042+3 : TPTP v9.3.1. Released v3.4.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % Computer : n008.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 02:34:28 PM UTC 2026 % Result : Timeout 289.20s 41.59s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : TOP042+3 : TPTP v9.3.1. Released v3.4.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.08/0.18 % Computer : n008.cluster.edu % 0.08/0.18 % Model : x86_64 x86_64 % 0.08/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.08/0.18 % Memory : 8046.5625MB % 0.08/0.18 % OS : Linux 6.8.0-71-generic % 0.08/0.18 % CPULimit : 300 % 0.08/0.18 % WCLimit : 300 % 0.08/0.18 % DateTime : Mon Sep 28 19:03:56 UTC 2026 % 0.08/0.18 % CPUTime : % 0.08/0.18 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.08/0.21 Running first-order model finding % 0.08/0.21 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 29.59/4.95 % (2531107)Will run a generic schedule for satisfiability detection. % 29.59/4.95 % (2531113)% WARNING: option uhcvi not known. % 29.59/4.95 % (2531113)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1526578969:i=135531:add=off:rawr=on_2994 on theBenchmark for (2994ds/135531Mi) % 29.59/4.95 % (2531112)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1103522484_2994 on theBenchmark for (2994ds/0Mi) % 29.59/4.95 % (2531114)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1675062467:i=88024:add=on:rawr=on_2994 on theBenchmark for (2994ds/88024Mi) % 29.59/4.95 % (2531115)dis+10_1_sil=32000:sp=arity:random_seed=3157989902:i=103:fgj=on_2994 on theBenchmark for (2994ds/103Mi) % 29.59/4.95 % (2531116)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1565303350:i=116_2994 on theBenchmark for (2994ds/116Mi) % 29.59/4.95 % (2531117)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2768655274:i=131_2994 on theBenchmark for (2994ds/131Mi) % 29.59/4.95 % (2531118)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1320271976:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2994 on theBenchmark for (2994ds/159Mi) % 29.59/4.95 % (2531115)Instruction limit reached! % 29.59/4.95 % (2531115)------------------------------ % 29.59/4.95 % (2531115)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 29.59/4.95 % (2531115)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.59/4.95 % (2531115)CaDiCaL version: 2.1.3 % 29.59/4.95 % (2531115)Termination reason: Instruction limit % 29.59/4.95 % (2531115)Termination phase: Preprocessing 1 % 29.59/4.95 % (2531115)Time elapsed: 0.070 s % 29.59/4.95 % (2531115)Peak memory usage: 35 MB % 29.59/4.95 % (2531115)Instructions burned: 104 (million) % 29.59/4.95 % (2531126)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3815933430:i=714:nm=2_2993 on theBenchmark for (2993ds/714Mi) % 29.59/4.95 % (2531117)Instruction limit reached! % 29.59/4.95 % (2531117)------------------------------ % 29.59/4.95 % (2531117)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 29.59/4.95 % (2531117)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.59/4.95 % (2531117)CaDiCaL version: 2.1.3 % 29.59/4.95 % (2531117)Termination reason: Instruction limit % 29.59/4.95 % (2531117)Termination phase: Preprocessing 2 % 29.59/4.95 % (2531117)Time elapsed: 0.100 s % 29.59/4.95 % (2531117)Peak memory usage: 37 MB % 29.59/4.95 % (2531117)Instructions burned: 131 (million) % 29.59/4.95 % (2531116)Instruction limit reached! % 29.59/4.95 % (2531116)------------------------------ % 29.59/4.95 % (2531116)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 29.59/4.95 % (2531116)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.59/4.95 % (2531116)CaDiCaL version: 2.1.3 % 29.59/4.95 % (2531116)Termination reason: Instruction limit % 29.59/4.95 % (2531116)Termination phase: Preprocessing 2 % 29.59/4.95 % (2531116)Time elapsed: 0.102 s % 29.59/4.95 % (2531116)Peak memory usage: 37 MB % 29.59/4.95 % (2531116)Instructions burned: 116 (million) % 29.59/4.95 % (2531128)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2948685451:i=131:bd=preordered:fsd=on_2992 on theBenchmark for (2992ds/131Mi) % 29.59/4.95 % (2531118)Instruction limit reached! % 29.59/4.95 % (2531118)------------------------------ % 29.59/4.95 % (2531118)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 29.59/4.95 % (2531129)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=3857423819:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2992 on theBenchmark for (2992ds/684Mi) % 29.59/4.95 % (2531118)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.59/4.95 % (2531118)CaDiCaL version: 2.1.3 % 29.59/4.95 % (2531118)Termination reason: Instruction limit % 29.59/4.95 % (2531118)Termination phase: Preprocessing 2 % 29.59/4.95 % (2531118)Time elapsed: 0.124 s % 29.59/4.95 % (2531118)Peak memory usage: 41 MB % 29.59/4.95 % (2531118)Instructions burned: 159 (million) % 29.59/4.95 % (2531132)ott-21_1_sil=16000:fs=off:random_seed=1920991264:i=180:av=off:fsr=off_2992 on theBenchmark for (2992ds/180Mi) % 29.59/4.95 % (2531128)Instruction limit reached! % 29.59/4.95 % (2531128)------------------------------ % 29.59/4.95 % (2531128)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 29.59/4.95 % (2531128)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 60.81/9.38 % (2531128)CaDiCaL version: 2.1.3 % 60.81/9.38 % (2531128)Termination reason: Instruction limit % 60.81/9.38 % (2531128)Termination phase: Preprocessing 2 % 60.81/9.38 % (2531128)Time elapsed: 0.104 s % 60.81/9.38 % (2531128)Peak memory usage: 37 MB % 60.81/9.38 % (2531128)Instructions burned: 131 (million) % 60.81/9.38 % (2531134)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=867557069:i=477:bd=all_2991 on theBenchmark for (2991ds/477Mi) % 60.81/9.38 % (2531132)Instruction limit reached! % 60.81/9.38 % (2531132)------------------------------ % 60.81/9.38 % (2531132)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 60.81/9.38 % (2531132)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 60.81/9.38 % (2531132)CaDiCaL version: 2.1.3 % 60.81/9.38 % (2531132)Termination reason: Instruction limit % 60.81/9.38 % (2531132)Termination phase: Preprocessing 2 % 60.81/9.38 % (2531132)Time elapsed: 0.139 s % 60.81/9.38 % (2531132)Peak memory usage: 45 MB % 60.81/9.38 % (2531132)Instructions burned: 181 (million) % 60.81/9.38 % (2531136)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=105208775:fmbsr=1.3:i=865:ins=25_2990 on theBenchmark for (2990ds/865Mi) % 60.81/9.38 % (2531129)Instruction limit reached! % 60.81/9.38 % (2531129)------------------------------ % 60.81/9.38 % (2531129)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 60.81/9.38 % (2531129)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 60.81/9.38 % (2531129)CaDiCaL version: 2.1.3 % 60.81/9.38 % (2531129)Termination reason: Instruction limit % 60.81/9.38 % (2531129)Termination phase: NewCNF % 60.81/9.38 % (2531129)Time elapsed: 0.411 s % 60.81/9.38 % (2531129)Peak memory usage: 61 MB % 60.81/9.38 % (2531129)Instructions burned: 686 (million) % 60.81/9.38 % (2531126)Instruction limit reached! % 60.81/9.38 % (2531126)------------------------------ % 60.81/9.38 % (2531126)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 60.81/9.38 % (2531126)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 60.81/9.38 % (2531126)CaDiCaL version: 2.1.3 % 60.81/9.38 % (2531126)Termination reason: Instruction limit % 60.81/9.38 % (2531126)Termination phase: Preprocessing 3 % 60.81/9.38 % (2531126)Time elapsed: 0.458 s % 60.81/9.38 % (2531126)Peak memory usage: 69 MB % 60.81/9.38 % (2531126)Instructions burned: 715 (million) % 60.81/9.38 % (2531138)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2778345134:i=1179_2988 on theBenchmark for (2988ds/1179Mi) % 60.81/9.38 % (2531134)Instruction limit reached! % 60.81/9.38 % (2531134)------------------------------ % 60.81/9.38 % (2531134)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 60.81/9.38 % (2531134)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 60.81/9.38 % (2531134)CaDiCaL version: 2.1.3 % 60.81/9.38 % (2531134)Termination reason: Instruction limit % 60.81/9.38 % (2531134)Termination phase: Preprocessing 3 % 60.81/9.38 % (2531134)Time elapsed: 0.314 s % 60.81/9.38 % (2531134)Peak memory usage: 57 MB % 60.81/9.38 % (2531134)Instructions burned: 477 (million) % 60.81/9.38 % (2531139)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2470128289:i=889:ins=1_2988 on theBenchmark for (2988ds/889Mi) % 60.81/9.38 % (2531141)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=187729392:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2988 on theBenchmark for (2988ds/692Mi) % 60.81/9.38 % (2531136)Instruction limit reached! % 60.81/9.38 % (2531136)------------------------------ % 60.81/9.38 % (2531136)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 60.81/9.38 % (2531136)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 60.81/9.38 % (2531136)CaDiCaL version: 2.1.3 % 60.81/9.38 % (2531136)Termination reason: Instruction limit % 60.81/9.38 % (2531136)Termination phase: Property scanning % 60.81/9.38 % (2531136)Time elapsed: 0.491 s % 60.81/9.38 % (2531136)Peak memory usage: 65 MB % 60.81/9.38 % (2531136)Instructions burned: 866 (million) % 60.81/9.38 % (2531144)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2921845977:i=879:kws=inv_precedence:fsr=off_2985 on theBenchmark for (2985ds/879Mi) % 60.81/9.38 % (2531141)Instruction limit reached! % 60.81/9.38 % (2531141)------------------------------ % 60.81/9.38 % (2531141)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 60.81/9.38 % (2531141)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 130.60/19.17 % (2531141)CaDiCaL version: 2.1.3 % 130.60/19.17 % (2531141)Termination reason: Instruction limit % 130.60/19.17 % (2531141)Termination phase: NewCNF % 130.60/19.17 % (2531141)Time elapsed: 0.423 s % 130.60/19.17 % (2531141)Peak memory usage: 61 MB % 130.60/19.17 % (2531141)Instructions burned: 692 (million) % 130.60/19.17 % (2531146)fmb+10_1_sil=64000:random_seed=2910215948:i=22061:nm=2:gsp=on_2983 on theBenchmark for (2983ds/22061Mi) % 130.60/19.17 % (2531139)Instruction limit reached! % 130.60/19.17 % (2531139)------------------------------ % 130.60/19.17 % (2531139)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 130.60/19.17 % (2531139)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 130.60/19.17 % (2531139)CaDiCaL version: 2.1.3 % 130.60/19.17 % (2531139)Termination reason: Instruction limit % 130.60/19.17 % (2531139)Termination phase: Property scanning % 130.60/19.17 % (2531139)Time elapsed: 0.515 s % 130.60/19.17 % (2531139)Peak memory usage: 65 MB % 130.60/19.17 % (2531139)Instructions burned: 891 (million) % 130.60/19.17 % (2531148)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1011382013:i=9515:nm=5_2982 on theBenchmark for (2982ds/9515Mi) % 130.60/19.17 % (2531138)Instruction limit reached! % 130.60/19.18 % (2531138)------------------------------ % 130.60/19.18 % (2531138)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 130.60/19.18 % (2531138)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 130.60/19.18 % (2531138)CaDiCaL version: 2.1.3 % 130.60/19.18 % (2531138)Termination reason: Instruction limit % 130.60/19.18 % (2531138)Termination phase: Property scanning % 130.60/19.18 % (2531138)Time elapsed: 0.659 s % 130.60/19.18 % (2531138)Peak memory usage: 71 MB % 130.60/19.18 % (2531138)Instructions burned: 1180 (million) % 130.60/19.18 % (2531150)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=882276493:fmbsr=1.7:i=920_2981 on theBenchmark for (2981ds/920Mi) % 130.60/19.18 % (2531144)Instruction limit reached! % 130.60/19.18 % (2531144)------------------------------ % 130.60/19.18 % (2531144)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 130.60/19.18 % (2531144)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 130.60/19.18 % (2531144)CaDiCaL version: 2.1.3 % 130.60/19.18 % (2531144)Termination reason: Instruction limit % 130.60/19.18 % (2531144)Termination phase: NewCNF % 130.60/19.18 % (2531144)Time elapsed: 0.467 s % 130.60/19.18 % (2531144)Peak memory usage: 67 MB % 130.60/19.18 % (2531144)Instructions burned: 879 (million) % 130.60/19.18 % (2531152)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2512021572:i=5131_2980 on theBenchmark for (2980ds/5131Mi) % 130.60/19.18 % (2531150)Instruction limit reached! % 130.60/19.18 % (2531150)------------------------------ % 130.60/19.18 % (2531150)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 130.60/19.18 % (2531150)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 130.60/19.18 % (2531150)CaDiCaL version: 2.1.3 % 130.60/19.18 % (2531150)Termination reason: Instruction limit % 130.60/19.18 % (2531150)Termination phase: Property scanning % 130.60/19.18 % (2531150)Time elapsed: 0.523 s % 130.60/19.18 % (2531150)Peak memory usage: 65 MB % 130.60/19.18 % (2531150)Instructions burned: 920 (million) % 130.60/19.18 % (2531154)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3807440012:i=1472:ins=7:fdi=8:gsp=on_2975 on theBenchmark for (2975ds/1472Mi) % 130.60/19.18 % (2531154)Instruction limit reached! % 130.60/19.18 % (2531154)------------------------------ % 130.60/19.18 % (2531154)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 130.60/19.18 % (2531154)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 130.60/19.18 % (2531154)CaDiCaL version: 2.1.3 % 130.60/19.18 % (2531154)Termination reason: Instruction limit % 130.60/19.18 % (2531154)Termination phase: Property scanning % 130.60/19.18 % (2531154)Time elapsed: 0.773 s % 130.60/19.18 % (2531154)Peak memory usage: 67 MB % 130.60/19.18 % (2531154)Instructions burned: 1474 (million) % 130.60/19.18 % (2531156)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3102167633:i=6324_2967 on theBenchmark for (2967ds/6324Mi) % 130.60/19.18 % (2531152)Instruction limit reached! % 130.60/19.18 % (2531152)------------------------------ % 130.60/19.18 % (2531152)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 130.60/19.18 % (2531152)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 130.60/19.18 % (2531152)CaDiCaL version: 2.1.3 % 130.60/19.18 % (2531152)Termination reason: Instruction limit % 130.60/19.18 % (2531152)Termination phase: Saturation % 289.20/41.59 % (2531152)Time elapsed: 2.776 s % 289.20/41.59 % (2531152)Peak memory usage: 117 MB % 289.20/41.59 % (2531152)Instructions burned: 5132 (million) % 289.20/41.59 % (2531158)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=3540868304:fmbsr=2.30978:i=2174_2952 on theBenchmark for (2952ds/2174Mi) % 289.20/41.59 % (2531158)Instruction limit reached! % 289.20/41.59 % (2531158)------------------------------ % 289.20/41.59 % (2531158)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 289.20/41.59 % (2531158)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 289.20/41.59 % (2531158)CaDiCaL version: 2.1.3 % 289.20/41.59 % (2531158)Termination reason: Instruction limit % 289.20/41.59 % (2531158)Termination phase: Finite model building preprocessing % 289.20/41.59 % (2531158)Time elapsed: 1.059 s % 289.20/41.59 % (2531158)Peak memory usage: 83 MB % 289.20/41.59 % (2531158)Instructions burned: 2174 (million) % 289.20/41.59 % (2531160)ott-2_1_sil=16000:newcnf=on:random_seed=3525814680:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2941 on theBenchmark for (2941ds/869Mi) % 289.20/41.59 % (2531160)Instruction limit reached! % 289.20/41.59 % (2531160)------------------------------ % 289.20/41.59 % (2531160)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 289.20/41.59 % (2531160)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 289.20/41.59 % (2531160)CaDiCaL version: 2.1.3 % 289.20/41.59 % (2531160)Termination reason: Instruction limit % 289.20/41.59 % (2531160)Termination phase: NewCNF % 289.20/41.59 % (2531160)Time elapsed: 0.470 s % 289.20/41.59 % (2531160)Peak memory usage: 67 MB % 289.20/41.59 % (2531160)Instructions burned: 871 (million) % 289.20/41.59 % (2531162)ott+10_1_sil=32000:tgt=ground:random_seed=1710121393:i=5114:av=off_2936 on theBenchmark for (2936ds/5114Mi) % 289.20/41.59 % (2531156)Instruction limit reached! % 289.20/41.59 % (2531156)------------------------------ % 289.20/41.59 % (2531156)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 289.20/41.59 % (2531156)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 289.20/41.59 % (2531156)CaDiCaL version: 2.1.3 % 289.20/41.59 % (2531156)Termination reason: Instruction limit % 289.20/41.59 % (2531156)Termination phase: Finite model building preprocessing % 289.20/41.59 % (2531156)Time elapsed: 3.301 s % 289.20/41.59 % (2531156)Peak memory usage: 123 MB % 289.20/41.59 % (2531156)Instructions burned: 6326 (million) % 289.20/41.59 % (2531164)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2088307020:i=54282_2934 on theBenchmark for (2934ds/54282Mi) % 289.20/41.59 % (2531148)Instruction limit reached! % 289.20/41.59 % (2531148)------------------------------ % 289.20/41.59 % (2531148)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 289.20/41.59 % (2531148)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 289.20/41.59 % (2531148)CaDiCaL version: 2.1.3 % 289.20/41.59 % (2531148)Termination reason: Instruction limit % 289.20/41.59 % (2531148)Termination phase: Finite model building preprocessing % 289.20/41.59 % (2531148)Time elapsed: 4.908 s % 289.20/41.59 % (2531148)Peak memory usage: 141 MB % 289.20/41.59 % (2531148)Instructions burned: 9515 (million) % 289.20/41.59 % (2531166)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=2121583655:i=3512:aac=none_2933 on theBenchmark for (2933ds/3512Mi) % 289.20/41.59 % (2531166)Instruction limit reached! % 289.20/41.59 % (2531166)------------------------------ % 289.20/41.59 % (2531166)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 289.20/41.59 % (2531166)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 289.20/41.59 % (2531166)CaDiCaL version: 2.1.3 % 289.20/41.59 % (2531166)Termination reason: Instruction limit % 289.20/41.59 % (2531166)Termination phase: Saturation % 289.20/41.59 % (2531166)Time elapsed: 1.830 s % 289.20/41.59 % (2531166)Peak memory usage: 91 MB % 289.20/41.59 % (2531166)Instructions burned: 3512 (million) % 289.20/41.59 % (2531168)dis+21_1_sil=32000:sas=cadical:random_seed=413971328:i=3773:amm=off_2914 on theBenchmark for (2914ds/3773Mi) % 289.20/41.59 % (2531162)Instruction limit reached! % 289.20/41.59 % (2531162)------------------------------ % 289.20/41.59 % (2531162)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 289.20/41.59 % (2531162)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 289.20/41.59 % (2531162)CaDiCaL version: 2.1.3 % 289.20/41.59 % (2531162)Termination reason: Instruction limit % 289.20/41.59 % (2531162)Termination phase: Saturation % 289.20/41.59 % (2531162)Time elapsed: 2.813 s % 289.20/41.59 % (2531162)Peak memory usage: 118 MB % 289.20/41.59 % (2531162)InstructionsTerminated %------------------------------------------------------------------------------