%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : LAT366+2 : TPTP v9.3.1. Released v3.4.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % Computer : n018.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 11:48:39 AM UTC 2026 % Result : Timeout 286.06s 43.86s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : LAT366+2 : TPTP v9.3.1. Released v3.4.0. % 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.11/0.35 % Computer : n018.cluster.edu % 0.11/0.35 % Model : x86_64 x86_64 % 0.11/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.35 % Memory : 8046.5625MB % 0.11/0.35 % OS : Linux 6.8.0-71-generic % 0.11/0.35 % CPULimit : 300 % 0.11/0.35 % WCLimit : 300 % 0.11/0.35 % DateTime : Sun Sep 27 15:06:41 UTC 2026 % 0.11/0.35 % CPUTime : % 0.11/0.36 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.14/0.39 Running first-order model finding % 0.14/0.39 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.96/5.03 % (2472118)Will run a generic schedule for satisfiability detection. % 28.96/5.03 % (2472125)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=4005460955:i=88024:add=on:rawr=on_2995 on theBenchmark for (2995ds/88024Mi) % 28.96/5.03 % (2472124)% WARNING: option uhcvi not known. % 28.96/5.03 % (2472123)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1071433527_2995 on theBenchmark for (2995ds/0Mi) % 28.96/5.03 % (2472124)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1831694807:i=135531:add=off:rawr=on_2995 on theBenchmark for (2995ds/135531Mi) % 28.96/5.03 % (2472126)dis+10_1_sil=32000:sp=arity:random_seed=92124709:i=103:fgj=on_2995 on theBenchmark for (2995ds/103Mi) % 28.96/5.03 % (2472127)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1607630364:i=116_2995 on theBenchmark for (2995ds/116Mi) % 28.96/5.03 % (2472128)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1273075308:i=131_2995 on theBenchmark for (2995ds/131Mi) % 28.96/5.03 % (2472129)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3215253937:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2995 on theBenchmark for (2995ds/159Mi) % 28.96/5.03 % (2472126)Instruction limit reached! % 28.96/5.03 % (2472126)------------------------------ % 28.96/5.03 % (2472126)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 28.96/5.03 % (2472126)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.96/5.03 % (2472126)CaDiCaL version: 2.1.3 % 28.96/5.03 % (2472126)Termination reason: Instruction limit % 28.96/5.03 % (2472126)Termination phase: Unused predicate definition removal % 28.96/5.03 % (2472126)Time elapsed: 0.074 s % 28.96/5.03 % (2472126)Peak memory usage: 31 MB % 28.96/5.03 % (2472126)Instructions burned: 103 (million) % 28.96/5.03 % (2472137)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2827539738:i=714:nm=2_2994 on theBenchmark for (2994ds/714Mi) % 28.96/5.03 % (2472127)Instruction limit reached! % 28.96/5.03 % (2472127)------------------------------ % 28.96/5.03 % (2472127)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 28.96/5.03 % (2472127)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.96/5.03 % (2472127)CaDiCaL version: 2.1.3 % 28.96/5.03 % (2472127)Termination reason: Instruction limit % 28.96/5.03 % (2472127)Termination phase: Preprocessing 2 % 28.96/5.03 % (2472127)Time elapsed: 0.099 s % 28.96/5.03 % (2472127)Peak memory usage: 34 MB % 28.96/5.03 % (2472127)Instructions burned: 117 (million) % 28.96/5.03 % (2472128)Instruction limit reached! % 28.96/5.03 % (2472128)------------------------------ % 28.96/5.03 % (2472128)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 28.96/5.03 % (2472128)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.96/5.03 % (2472128)CaDiCaL version: 2.1.3 % 28.96/5.03 % (2472128)Termination reason: Instruction limit % 28.96/5.03 % (2472128)Termination phase: Preprocessing 2 % 28.96/5.03 % (2472128)Time elapsed: 0.107 s % 28.96/5.03 % (2472128)Peak memory usage: 34 MB % 28.96/5.03 % (2472128)Instructions burned: 132 (million) % 28.96/5.03 % (2472139)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2430916744:i=131:bd=preordered:fsd=on_2993 on theBenchmark for (2993ds/131Mi) % 28.96/5.03 % (2472129)Instruction limit reached! % 28.96/5.03 % (2472129)------------------------------ % 28.96/5.03 % (2472129)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 28.96/5.03 % (2472129)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.96/5.03 % (2472129)CaDiCaL version: 2.1.3 % 28.96/5.03 % (2472129)Termination reason: Instruction limit % 28.96/5.03 % (2472129)Termination phase: Preprocessing 2 % 28.96/5.03 % (2472129)Time elapsed: 0.126 s % 28.96/5.03 % (2472129)Peak memory usage: 40 MB % 28.96/5.03 % (2472129)Instructions burned: 159 (million) % 28.96/5.03 % (2472140)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=2661477349:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2993 on theBenchmark for (2993ds/684Mi) % 28.96/5.03 % (2472142)ott-21_1_sil=16000:fs=off:random_seed=3138172881:i=180:av=off:fsr=off_2993 on theBenchmark for (2993ds/180Mi) % 28.96/5.03 % (2472139)Instruction limit reached! % 28.96/5.03 % (2472139)------------------------------ % 28.96/5.03 % (2472139)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 28.96/5.03 % (2472139)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 55.88/8.71 % (2472139)CaDiCaL version: 2.1.3 % 55.88/8.71 % (2472139)Termination reason: Instruction limit % 55.88/8.71 % (2472139)Termination phase: Preprocessing 2 % 55.88/8.71 % (2472139)Time elapsed: 0.102 s % 55.88/8.71 % (2472139)Peak memory usage: 35 MB % 55.88/8.71 % (2472139)Instructions burned: 131 (million) % 55.88/8.71 % (2472145)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2185108061:i=477:bd=all_2992 on theBenchmark for (2992ds/477Mi) % 55.88/8.71 % (2472142)Instruction limit reached! % 55.88/8.71 % (2472142)------------------------------ % 55.88/8.71 % (2472142)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 55.88/8.71 % (2472142)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 55.88/8.71 % (2472142)CaDiCaL version: 2.1.3 % 55.88/8.71 % (2472142)Termination reason: Instruction limit % 55.88/8.71 % (2472142)Termination phase: Naming % 55.88/8.71 % (2472142)Time elapsed: 0.138 s % 55.88/8.71 % (2472142)Peak memory usage: 40 MB % 55.88/8.71 % (2472142)Instructions burned: 181 (million) % 55.88/8.71 % (2472147)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2952642201:fmbsr=1.3:i=865:ins=25_2991 on theBenchmark for (2991ds/865Mi) % 55.88/8.71 % (2472140)Instruction limit reached! % 55.88/8.71 % (2472140)------------------------------ % 55.88/8.71 % (2472140)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 55.88/8.71 % (2472140)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 55.88/8.71 % (2472140)CaDiCaL version: 2.1.3 % 55.88/8.71 % (2472140)Termination reason: Instruction limit % 55.88/8.71 % (2472140)Termination phase: NewCNF % 55.88/8.71 % (2472140)Time elapsed: 0.409 s % 55.88/8.71 % (2472140)Peak memory usage: 55 MB % 55.88/8.71 % (2472140)Instructions burned: 686 (million) % 55.88/8.71 % (2472137)Instruction limit reached! % 55.88/8.71 % (2472137)------------------------------ % 55.88/8.71 % (2472137)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 55.88/8.71 % (2472137)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 55.88/8.71 % (2472137)CaDiCaL version: 2.1.3 % 55.88/8.71 % (2472137)Termination reason: Instruction limit % 55.88/8.71 % (2472137)Termination phase: Property scanning % 55.88/8.71 % (2472137)Time elapsed: 0.455 s % 55.88/8.71 % (2472137)Peak memory usage: 67 MB % 55.88/8.71 % (2472137)Instructions burned: 714 (million) % 55.88/8.71 % (2472145)Instruction limit reached! % 55.88/8.71 % (2472145)------------------------------ % 55.88/8.71 % (2472145)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 55.88/8.71 % (2472145)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 55.88/8.71 % (2472145)CaDiCaL version: 2.1.3 % 55.88/8.71 % (2472145)Termination reason: Instruction limit % 55.88/8.71 % (2472145)Termination phase: Preprocessing 3 % 55.88/8.71 % (2472145)Time elapsed: 0.304 s % 55.88/8.71 % (2472145)Peak memory usage: 51 MB % 55.88/8.71 % (2472145)Instructions burned: 478 (million) % 55.88/8.71 % (2472149)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3362908215:i=1179_2989 on theBenchmark for (2989ds/1179Mi) % 55.88/8.71 % (2472150)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=601660504:i=889:ins=1_2989 on theBenchmark for (2989ds/889Mi) % 55.88/8.71 % (2472151)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=1244949209:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2989 on theBenchmark for (2989ds/692Mi) % 55.88/8.71 % (2472147)Instruction limit reached! % 55.88/8.71 % (2472147)------------------------------ % 55.88/8.71 % (2472147)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 55.88/8.71 % (2472147)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 55.88/8.71 % (2472147)CaDiCaL version: 2.1.3 % 55.88/8.71 % (2472147)Termination reason: Instruction limit % 55.88/8.71 % (2472147)Termination phase: Function definition elimination % 55.88/8.71 % (2472147)Time elapsed: 0.482 s % 55.88/8.71 % (2472147)Peak memory usage: 58 MB % 55.88/8.71 % (2472147)Instructions burned: 866 (million) % 55.88/8.71 % (2472155)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=4075881838:i=879:kws=inv_precedence:fsr=off_2986 on theBenchmark for (2986ds/879Mi) % 55.88/8.71 % (2472151)Instruction limit reached! % 55.88/8.71 % (2472151)------------------------------ % 55.88/8.71 % (2472151)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 55.88/8.71 % (2472151)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 80.76/12.23 % (2472151)CaDiCaL version: 2.1.3 % 80.76/12.23 % (2472151)Termination reason: Instruction limit % 80.76/12.23 % (2472151)Termination phase: NewCNF % 80.76/12.23 % (2472151)Time elapsed: 0.408 s % 80.76/12.23 % (2472151)Peak memory usage: 55 MB % 80.76/12.23 % (2472151)Instructions burned: 693 (million) % 80.76/12.23 % (2472157)fmb+10_1_sil=64000:random_seed=42767953:i=22061:nm=2:gsp=on_2984 on theBenchmark for (2984ds/22061Mi) % 80.76/12.23 % (2472150)Instruction limit reached! % 80.76/12.23 % (2472150)------------------------------ % 80.76/12.23 % (2472150)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 80.76/12.23 % (2472150)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 80.76/12.23 % (2472150)CaDiCaL version: 2.1.3 % 80.76/12.23 % (2472150)Termination reason: Instruction limit % 80.76/12.23 % (2472150)Termination phase: Function definition elimination % 80.76/12.23 % (2472150)Time elapsed: 0.500 s % 80.76/12.23 % (2472150)Peak memory usage: 58 MB % 80.76/12.23 % (2472150)Instructions burned: 890 (million) % 80.76/12.23 % (2472159)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2312502097:i=9515:nm=5_2983 on theBenchmark for (2983ds/9515Mi) % 80.76/12.23 % (2472149)Instruction limit reached! % 80.76/12.23 % (2472149)------------------------------ % 80.76/12.23 % (2472149)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 80.76/12.23 % (2472149)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 80.76/12.23 % (2472149)CaDiCaL version: 2.1.3 % 80.76/12.23 % (2472149)Termination reason: Instruction limit % 80.76/12.23 % (2472149)Termination phase: Property scanning % 80.76/12.23 % (2472149)Time elapsed: 0.641 s % 80.76/12.23 % (2472149)Peak memory usage: 62 MB % 80.76/12.23 % (2472149)Instructions burned: 1179 (million) % 80.76/12.23 % (2472161)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=138826115:fmbsr=1.7:i=920_2982 on theBenchmark for (2982ds/920Mi) % 80.76/12.23 % (2472155)Instruction limit reached! % 80.76/12.23 % (2472155)------------------------------ % 80.76/12.23 % (2472155)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 80.76/12.23 % (2472155)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 80.76/12.23 % (2472155)CaDiCaL version: 2.1.3 % 80.76/12.23 % (2472155)Termination reason: Instruction limit % 80.76/12.23 % (2472155)Termination phase: NewCNF % 80.76/12.23 % (2472155)Time elapsed: 0.477 s % 80.76/12.23 % (2472155)Peak memory usage: 61 MB % 80.76/12.23 % (2472155)Instructions burned: 879 (million) % 80.76/12.23 % (2472163)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1566516758:i=5131_2981 on theBenchmark for (2981ds/5131Mi) % 80.76/12.23 % (2472161)Instruction limit reached! % 80.76/12.23 % (2472161)------------------------------ % 80.76/12.23 % (2472161)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 80.76/12.23 % (2472161)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 80.76/12.23 % (2472161)CaDiCaL version: 2.1.3 % 80.76/12.23 % (2472161)Termination reason: Instruction limit % 80.76/12.23 % (2472161)Termination phase: Function definition elimination % 80.76/12.23 % (2472161)Time elapsed: 0.525 s % 80.76/12.23 % (2472161)Peak memory usage: 59 MB % 80.76/12.23 % (2472161)Instructions burned: 921 (million) % 80.76/12.23 % (2472165)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=467479875:i=1472:ins=7:fdi=8:gsp=on_2977 on theBenchmark for (2977ds/1472Mi) % 80.76/12.23 % (2472165)Instruction limit reached! % 80.76/12.23 % (2472165)------------------------------ % 80.76/12.23 % (2472165)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 80.76/12.23 % (2472165)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 80.76/12.23 % (2472165)CaDiCaL version: 2.1.3 % 80.76/12.23 % (2472165)Termination reason: Instruction limit % 80.76/12.23 % (2472165)Termination phase: Saturation % 80.76/12.23 % (2472165)Time elapsed: 0.756 s % 80.76/12.23 % (2472165)Peak memory usage: 59 MB % 80.76/12.23 % (2472165)Instructions burned: 1473 (million) % 80.76/12.23 % (2472167)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=303225592:i=6324_2969 on theBenchmark for (2969ds/6324Mi) % 80.76/12.23 % (2472163)Instruction limit reached! % 80.76/12.23 % (2472163)------------------------------ % 80.76/12.23 % (2472163)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 80.76/12.23 % (2472163)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 80.76/12.23 % (2472163)CaDiCaL version: 2.1.3 % 80.76/12.23 % (2472163)Termination reason: Instruction limit % 124.74/18.48 % (2472163)Termination phase: Saturation % 124.74/18.48 % (2472163)Time elapsed: 2.783 s % 124.74/18.48 % (2472163)Peak memory usage: 109 MB % 124.74/18.48 % (2472163)Instructions burned: 5133 (million) % 124.74/18.48 % (2472169)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=4007665226:fmbsr=2.30978:i=2174_2953 on theBenchmark for (2953ds/2174Mi) % 124.74/18.48 % (2472169)Instruction limit reached! % 124.74/18.48 % (2472169)------------------------------ % 124.74/18.48 % (2472169)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 124.74/18.48 % (2472169)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 124.74/18.48 % (2472169)CaDiCaL version: 2.1.3 % 124.74/18.48 % (2472169)Termination reason: Instruction limit % 124.74/18.48 % (2472169)Termination phase: Finite model building preprocessing % 124.74/18.48 % (2472169)Time elapsed: 1.065 s % 124.74/18.48 % (2472169)Peak memory usage: 80 MB % 124.74/18.48 % (2472169)Instructions burned: 2175 (million) % 124.74/18.48 % (2472171)ott-2_1_sil=16000:newcnf=on:random_seed=4169366503:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2942 on theBenchmark for (2942ds/869Mi) % 124.74/18.48 % (2472171)Instruction limit reached! % 124.74/18.48 % (2472171)------------------------------ % 124.74/18.48 % (2472171)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 124.74/18.48 % (2472171)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 124.74/18.48 % (2472171)CaDiCaL version: 2.1.3 % 124.74/18.48 % (2472171)Termination reason: Instruction limit % 124.74/18.48 % (2472171)Termination phase: NewCNF % 124.74/18.48 % (2472171)Time elapsed: 0.461 s % 124.74/18.48 % (2472171)Peak memory usage: 60 MB % 124.74/18.48 % (2472171)Instructions burned: 870 (million) % 124.74/18.48 % (2472173)ott+10_1_sil=32000:tgt=ground:random_seed=2073691288:i=5114:av=off_2937 on theBenchmark for (2937ds/5114Mi) % 124.74/18.48 % (2472167)Instruction limit reached! % 124.74/18.48 % (2472167)------------------------------ % 124.74/18.48 % (2472167)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 124.74/18.48 % (2472167)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 124.74/18.48 % (2472167)CaDiCaL version: 2.1.3 % 124.74/18.48 % (2472167)Termination reason: Instruction limit % 124.74/18.48 % (2472167)Termination phase: Finite model building preprocessing % 124.74/18.48 % (2472167)Time elapsed: 3.230 s % 124.74/18.48 % (2472167)Peak memory usage: 116 MB % 124.74/18.48 % (2472167)Instructions burned: 6325 (million) % 124.74/18.48 % (2472175)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=371365730:i=54282_2936 on theBenchmark for (2936ds/54282Mi) % 124.74/18.48 % (2472159)Instruction limit reached! % 124.74/18.48 % (2472159)------------------------------ % 124.74/18.48 % (2472159)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 124.74/18.48 % (2472159)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 124.74/18.48 % (2472159)CaDiCaL version: 2.1.3 % 124.74/18.48 % (2472159)Termination reason: Instruction limit % 124.74/18.48 % (2472159)Termination phase: Finite model building preprocessing % 124.74/18.48 % (2472159)Time elapsed: 4.828 s % 124.74/18.48 % (2472159)Peak memory usage: 144 MB % 124.74/18.48 % (2472159)Instructions burned: 9516 (million) % 124.74/18.48 % (2472177)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=1047407159:i=3512:aac=none_2935 on theBenchmark for (2935ds/3512Mi) % 124.74/18.48 % Detected minimum model sizes of [5] % 124.74/18.48 % Detected maximum model sizes of [max] % 124.74/18.48 % (2472157)Cannot represent all propositional literals internally % 124.74/18.48 % (2472157)Refutation not found, incomplete strategy % 124.74/18.48 % (2472157)------------------------------ % 124.74/18.48 % (2472157)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 124.74/18.48 % (2472157)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 124.74/18.48 % (2472157)CaDiCaL version: 2.1.3 % 124.74/18.48 % (2472157)Termination reason: Refutation not found, incomplete strategy % 124.74/18.48 % (2472157)Time elapsed: 5.313 s % 124.74/18.48 % (2472157)Peak memory usage: 184 MB % 124.74/18.48 % (2472157)Instructions burned: 10390 (million) % 124.74/18.48 % (2472157)------------------------------ % 124.74/18.48 % (2472157)------------------------------ % 124.74/18.48 % (2472179)dis+21_1_sil=32000:sas=cadical:random_seed=3161577504:i=3773:amm=off_2930 on theBenchmark for (2930ds/3773Mi) % 124.74/18.48 % (2472177)Instruction limit reached! % 124.74/18.48 % (2472177)------------------------------ % 124.74/18.48 % (2472177)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 124.74/18.48 % (2472177)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 180.19/26.29 % (2472177)CaDiCaL version: 2.1.3 % 180.19/26.29 % (2472177)Termination reason: Instruction limit % 180.19/26.29 % (2472177)Termination phase: Saturation % 180.19/26.29 % (2472177)Time elapsed: 1.819 s % 180.19/26.29 % (2472177)Peak memory usage: 83 MB % 180.19/26.29 % (2472177)Instructions burned: 3513 (million) % 180.19/26.29 % (2472181)ott+11_1_sil=16000:gs=on:random_seed=4217235371:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2916 on theBenchmark for (2916ds/2251Mi) % 180.19/26.29 % Detected minimum model sizes of [5] % 180.19/26.29 % Detected maximum model sizes of [max] % 180.19/26.29 % (2472123)Cannot represent all propositional literals internally % 180.19/26.29 % (2472123)Refutation not found, incomplete strategy % 180.19/26.29 % (2472123)------------------------------ % 180.19/26.29 % (2472123)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 180.19/26.29 % (2472123)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 180.19/26.29 % (2472123)CaDiCaL version: 2.1.3 % 180.19/26.29 % (2472123)Termination reason: Refutation not found, incomplete strategy % 180.19/26.29 % (2472123)Time elapsed: 8.357 s % 180.19/26.30 % (2472123)Peak memory usage: 245 MB % 180.19/26.30 % (2472123)Instructions burned: 16421 (million) % 180.19/26.30 % (2472179)Instruction limit reached! % 180.19/26.30 % (2472179)------------------------------ % 180.19/26.30 % (2472179)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 180.19/26.30 % (2472179)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 180.19/26.30 % (2472179)CaDiCaL version: 2.1.3 % 180.19/26.30 % (2472179)Termination reason: Instruction limit % 180.19/26.30 % (2472179)Termination phase: Saturation % 180.19/26.30 % (2472179)Time elapsed: 1.974 s % 180.19/26.30 % (2472179)Peak memory usage: 88 MB % 180.19/26.30 % (2472179)Instructions burned: 3775 (million) % 180.19/26.30 % (2472123)------------------------------ % 180.19/26.30 % (2472123)------------------------------ % 180.19/26.30 % (2472183)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=1944187161:fmbsr=1.6:i=67534_2910 on theBenchmark for (2910ds/67534Mi) % 180.19/26.30 % (2472185)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=2180216048:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2910 on theBenchmark for (2910ds/4591Mi) % 180.19/26.30 % (2472173)Instruction limit reached! % 180.19/26.30 % (2472173)------------------------------ % 180.19/26.30 % (2472173)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 180.19/26.30 % (2472173)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 180.19/26.30 % (2472173)CaDiCaL version: 2.1.3 % 180.19/26.30 % (2472173)Termination reason: Instruction limit % 180.19/26.30 % (2472173)Termination phase: Saturation % 180.19/26.30 % (2472173)Time elapsed: 2.847 s % 180.19/26.30 % (2472173)Peak memory usage: 119 MB % 180.19/26.30 % (2472173)Instructions burned: 5114 (million) % 180.19/26.30 % (2472187)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=554820903:i=29340_2908 on theBenchmark for (2908ds/29340Mi) % 180.19/26.30 % (2472181)Instruction limit reached! % 180.19/26.30 % (2472181)------------------------------ % 180.19/26.30 % (2472181)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 180.19/26.30 % (2472181)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 180.19/26.30 % (2472181)CaDiCaL version: 2.1.3 % 180.19/26.30 % (2472181)Termination reason: Instruction limit % 180.19/26.30 % (2472181)Termination phase: Saturation % 180.19/26.30 % (2472181)Time elapsed: 1.279 s % 180.19/26.30 % (2472181)Peak memory usage: 85 MB % 180.19/26.30 % (2472181)Instructions burned: 2251 (million) % 180.19/26.30 % (2472189)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=1947703495:i=5211_2903 on theBenchmark for (2903ds/5211Mi) % 180.19/26.30 % (2472185)Instruction limit reached! % 180.19/26.30 % (2472185)------------------------------ % 180.19/26.30 % (2472185)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 180.19/26.30 % (2472185)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 180.19/26.30 % (2472185)CaDiCaL version: 2.1.3 % 180.19/26.30 % (2472185)Termination reason: Instruction limit % 180.19/26.30 % (2472185)Termination phase: Saturation % 180.19/26.30 % (2472185)Time elapsed: 2.308 s % 180.19/26.30 % (2472185)Peak memory usage: 94 MB % 180.19/26.30 % (2472185)Instructions burned: 4591 (million) % 180.19/26.30 % (2472191)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=3745999640:i=5497:nm=2_2887 on theBenchmark for (2887ds/5497Mi) % 180.19/26.30 % (2472189)Instruction limit reached! % 180.19/26.30 % (2472189)------------------------------ % 286.06/43.86 % (2472189)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 286.06/43.86 % (2472189)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 286.06/43.86 % (2472189)CaDiCaL version: 2.1.3 % 286.06/43.86 % (2472189)Termination reason: Instruction limit % 286.06/43.86 % (2472189)Termination phase: Saturation % 286.06/43.86 % (2472189)Time elapsed: 2.181 s % 286.06/43.86 % (2472189)Peak memory usage: 106 MB % 286.06/43.86 % (2472189)Instructions burned: 5211 (million) % 286.06/43.86 % (2472193)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=3581295598:fmbsr=2:i=46332_2881 on theBenchmark for (2881ds/46332Mi) % 286.06/43.86 % (2472191)Instruction limit reached! % 286.06/43.86 % (2472191)------------------------------ % 286.06/43.86 % (2472191)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 286.06/43.86 % (2472191)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 286.06/43.86 % (2472191)CaDiCaL version: 2.1.3 % 286.06/43.86 % (2472191)Termination reason: Instruction limit % 286.06/43.86 % (2472191)Termination phase: Finite model building preprocessing % 286.06/43.87 % (2472191)Time elapsed: 2.965 s % 286.06/43.87 % (2472191)Peak memory usage: 123 MB % 286.06/43.87 % (2472191)Instructions burned: 5498 (million) % 286.06/43.87 % (2472195)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=2615866187:i=14071_2857 on theBenchmark for (2857ds/14071Mi) % 286.06/43.87 % Detected minimum model sizes of [5] % 286.06/43.87 % Detected maximum model sizes of [max] % 286.06/43.87 % (2472175)Cannot represent all propositional literals internally % 286.06/43.87 % (2472175)Refutation not found, incomplete strategy % 286.06/43.87 % (2472175)------------------------------ % 286.06/43.87 % (2472175)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 286.06/43.87 % (2472175)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 286.06/43.87 % (2472175)CaDiCaL version: 2.1.3 % 286.06/43.87 % (2472175)Termination reason: Refutation not found, incomplete strategy % 286.06/43.87 % (2472175)Time elapsed: 8.364 s % 286.06/43.87 % (2472175)Peak memory usage: 245 MB % 286.06/43.87 % (2472175)Instructions burned: 16418 (million) % 286.06/43.87 % (2472175)------------------------------ % 286.06/43.87 % (2472175)------------------------------ % 286.06/43.87 % (2472197)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3438391447:i=22565:add=on:rawr=on_2852 on theBenchmark for (2852ds/22565Mi) % 286.06/43.87 % (2472125)Instruction limit reached! % 286.06/43.87 % (2472125)------------------------------ % 286.06/43.87 % (2472125)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 286.06/43.87 % (2472125)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 286.06/43.87 % (2472125)CaDiCaL version: 2.1.3 % 286.06/43.87 % (2472125)Termination reason: Instruction limit % 286.06/43.87 % (2472125)Termination phase: Saturation % 286.06/43.87 % (2472125)Time elapsed: 14.768 s % 286.06/43.87 % (2472125)Peak memory usage: 288 MB % 286.06/43.87 % (2472125)Instructions burned: 88031 (million) % 286.06/43.87 % (2472199)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=3622303692:i=8173:av=off_2846 on theBenchmark for (2846ds/8173Mi) % 286.06/43.87 % Detected minimum model sizes of [5] % 286.06/43.87 % Detected maximum model sizes of [max] % 286.06/43.87 % (2472183)Cannot represent all propositional literals internally % 286.06/43.87 % (2472183)Refutation not found, incomplete strategy % 286.06/43.87 % (2472183)------------------------------ % 286.06/43.87 % (2472183)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 286.06/43.87 % (2472183)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 286.06/43.87 % (2472183)CaDiCaL version: 2.1.3 % 286.06/43.87 % (2472183)Termination reason: Refutation not found, incomplete strategy % 286.06/43.87 % (2472183)Time elapsed: 7.730 s % 286.06/43.87 % (2472183)Peak memory usage: 206 MB % 286.06/43.87 % (2472183)Instructions burned: 15711 (million) % 286.06/43.87 % (2472183)------------------------------ % 286.06/43.87 % (2472183)------------------------------ % 286.06/43.87 % (2472201)dis+10_16:1_sil=16000:random_seed=2911719739:i=9155:fsr=off_2832 on theBenchmark for (2832ds/9155Mi) % 286.06/43.87 % (2472199)Instruction limit reached! % 286.06/43.87 % (2472199)------------------------------ % 286.06/43.87 % (2472199)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 286.06/43.87 % (2472199)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 286.06/43.87 % (2472199)CaDiCaL version: 2.1.3 % 286.06/43.87 % (2472199)Termination reason: Instruction limit % 286.06/43.87 % (2472199)Termination phase: Saturation % 307.51/44.15 % (2472199)Time elapsed: 2.764 s % 307.51/44.15 % (2472199)Peak memory usage: 176 MB % 307.51/44.15 % (2472199)Instructions burned: 8175 (million) % 307.51/44.15 % (2472302)ott-3_8_sil=64000:random_seed=3368852585:i=20139:bs=on_2819 on theBenchmark for (2819ds/20139Mi) % 307.51/44.15 % Detected minimum model sizes of [5] % 307.51/44.15 % Detected maximum model sizes of [max] % 307.51/44.15 % (2472193)Cannot represent all propositional literals internally % 307.51/44.15 % (2472193)Refutation not found, incomplete strategy % 307.51/44.15 % (2472193)------------------------------ % 307.51/44.15 % (2472193)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 307.51/44.15 % (2472193)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 307.51/44.15 % (2472193)CaDiCaL version: 2.1.3 % 307.51/44.15 % (2472193)Termination reason: Refutation not found, incomplete strategy % 307.51/44.15 % (2472193)Time elapsed: 7.875 s % 307.51/44.15 % (2472193)Peak memory usage: 206 MB % 307.51/44.15 % (2472193)Instructions burned: 15712 (million) % 307.51/44.15 % (2472193)------------------------------ % 307.51/44.15 % (2472193)------------------------------ % 307.51/44.15 % (2472412)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=3832567411:fmbsr=2:i=32576_2801 on theBenchmark for (2801ds/32576Mi) % 307.51/44.15 % (2472195)Instruction limit reached! % 307.51/44.15 % (2472195)------------------------------ % 307.51/44.15 % (2472195)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 307.51/44.15 % (2472195)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 307.51/44.15 % (2472195)CaDiCaL version: 2.1.3 % 307.51/44.15 % (2472195)Termination reason: Instruction limit % 307.51/44.15 % (2472195)Termination phase: Finite model building preprocessing % 307.51/44.15 % (2472195)Time elapsed: 7.852 s % 307.51/44.15 % (2472195)Peak memory usage: 231 MB % 307.51/44.15 % (2472195)Instructions burned: 14072 (million) % 307.51/44.15 % (2472471)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=1004118569:i=11404_2778 on theBenchmark for (2778ds/11404Mi) % 307.51/44.15 % (2472201)Instruction limit reached! % 307.51/44.15 % (2472201)------------------------------ % 307.51/44.15 % (2472201)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 307.51/44.15 % (2472201)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 307.51/44.15 % (2472201)CaDiCaL version: 2.1.3 % 307.51/44.15 % (2472201)Termination reason: Instruction limit % 307.51/44.15 % (2472201)Termination phase: Saturation % 307.51/44.15 % (2472201)Time elapsed: 5.630 s % 307.51/44.15 % (2472201)Peak memory usage: 126 MB % 307.51/44.15 % (2472201)Instructions burned: 9156 (million) % 307.51/44.15 % (2472526)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=2824682740:i=14134_2776 on theBenchmark for (2776ds/14134Mi) % 307.51/44.15 % (2472197)Instruction limit reached! % 307.51/44.15 % (2472197)------------------------------ % 307.51/44.15 % (2472197)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 307.51/44.15 % (2472197)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 307.51/44.15 % (2472197)CaDiCaL version: 2.1.3 % 307.51/44.15 % (2472197)Termination reason: Instruction limit % 307.51/44.15 % (2472197)Termination phase: Saturation % 307.51/44.15 % (2472197)Time elapsed: 9.497 s % 307.51/44.15 % (2472197)Peak memory usage: 240 MB % 307.51/44.15 % (2472197)Instructions burned: 22568 (million) % 307.51/44.15 % (2472593)dis+33_16_sil=32000:sac=on:random_seed=2379175780:i=15851:nm=0_2756 on theBenchmark for (2756ds/15851Mi) % 307.51/44.15 % (2472302)Instruction limit reached! % 307.51/44.15 % (2472302)------------------------------ % 307.51/44.15 % (2472302)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 307.51/44.15 % (2472302)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 307.51/44.15 % (2472302)CaDiCaL version: 2.1.3 % 307.51/44.15 % (2472302)Termination reason: Instruction limit % 307.51/44.15 % (2472302)Termination phase: Saturation % 307.51/44.15 % (2472302)Time elapsed: 7.709 s % 307.51/44.15 % (2472302)Peak memory usage: 148 MB % 307.51/44.15 % (2472302)Instructions burned: 20142 (million) % 307.51/44.15 % (2472708)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=38049713:avsq=on:i=17627:add=on:amm=off_2741 on theBenchmark for (2741ds/17627Mi) % 307.51/44.15 % (2472187)Instruction limit reached! % 307.51/44.15 % (2472187)------------------------------ % 307.51/44.15 % (2472187)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 307.51/44.15 % (2472187)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 307.51/44.15 % (2472187)CaDiCaL version: 2.1.3 % 307.51/44.15 % (2472187)Termination reason: Instruction limit % 307.51/44.15 % (2472187)Termination phase: Saturation % 307.51/44.15 % (2472187)Time elapsed: 16.774 s % 307.51/44.15 % (2472187)Peak memory usage: 396 MB % 307.51/44.15 % (2472187)Instructions burned: 29341 (million) % 307.51/44.15 % (2472729)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=798655337:s2a=on:i=53295_2740 on theBenchmark for (2740ds/53295Mi) % 307.51/44.15 % (2472471)Instruction limit reached! % 307.51/44.15 % (2472471)------------------------------ % 307.51/44.15 % (2472471)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 307.51/44.15 % (2472471)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 307.51/44.15 % (2472471)CaDiCaL version: 2.1.3 % 307.51/44.15 % (2472471)Termination reason: Instruction limit % 307.51/44.15 % (2472471)Termination phase: Saturation % 307.51/44.15 % (2472471)Time elapsed: 7.831 s % 307.51/44.15 % (2472471)Peak memory usage: 182 MB % 307.51/44.15 % (2472471)Instructions burned: 11405 (million) % 307.51/44.15 % (2472889)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=3148925728:i=26857:ins=20_2699 on theBenchmark for (2699ds/26857Mi) % 307.51/44.15 % Detected minimum model sizes of [5] % 307.51/44.15 % Detected maximum model sizes of [max] % 307.51/44.15 % (2472412)Cannot represent all propositional literals internally % 307.51/44.15 % (2472412)Refutation not found, incomplete strategy % 307.51/44.15 % (2472412)------------------------------ % 307.51/44.15 % (2472412)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 307.51/44.15 % (2472412)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 307.51/44.15 % (2472412)CaDiCaL version: 2.1.3 % 307.51/44.15 % (2472412)Termination reason: Refutation not found, incomplete strategy % 307.51/44.15 % (2472412)Time elapsed: 10.575 s % 307.51/44.15 % (2472412)Peak memory usage: 241 MB % 307.51/44.15 % (2472412)Instructions burned: 16390 (million) % 307.51/44.15 % (2472412)------------------------------ % 307.51/44.15 % (2472412)------------------------------ % 307.51/44.15 % (2472891)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=255039334:i=28120:bs=on:fsr=off_2694 on theBenchmark for (2694ds/28120Mi) % 307.51/44.15 % (2472526)Instruction limit reached! % 307.51/44.15 % (2472526)------------------------------ % 307.51/44.15 % (2472526)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 307.51/44.15 % (2472526)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 307.51/44.15 % (2472526)CaDiCaL version: 2.1.3 % 307.51/44.15 % (2472526)Termination reason: Instruction limit % 307.51/44.15 % (2472526)Termination phase: Saturation % 307.51/44.15 % (2472526)Time elapsed: 11.323 s % 307.51/44.15 % (2472526)Peak memory usage: 213 MB % 307.51/44.15 % (2472526)Instructions burned: 14134 (million) % 307.51/44.15 % (2472903)fmb+10_1_sil=256000:fmbss=7:random_seed=3790573862:fmbsr=1.6:i=182295_2662 on theBenchmark for (2662ds/182295Mi) % 307.51/44.15 % (2472708)Instruction limit reached! % 307.51/44.15 % (2472708)------------------------------ % 307.51/44.15 % (2472708)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 307.51/44.15 % (2472708)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 307.51/44.15 % (2472708)CaDiCaL version: 2.1.3 % 307.51/44.15 % (2472708)Termination reason: Instruction limit % 307.51/44.15 % (2472708)Termination phase: Saturation % 307.51/44.15 % (2472708)Time elapsed: 8.214 s % 307.51/44.15 % (2472708)Peak memory usage: 346 MB % 307.51/44.15 % (2472708)Instructions burned: 17629 (million) % 307.51/44.15 % (2472905)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=3028831163:i=44625:gsp=on_2659 on theBenchmark for (2659ds/44625Mi) % 307.51/44.15 % (2472593)Instruction limit reached! % 307.51/44.15 % (2472593)------------------------------ % 307.51/44.15 % (2472593)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 307.51/44.15 % (2472593)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 307.51/44.15 % (2472593)CaDiCaL version: 2.1.3 % 307.51/44.15 % (2472593)Termination reason: Instruction limit % 307.51/44.15 % (2472593)Termination phase: Clausification % 307.51/44.15 % (2472593)Time elapsed: 18.084 s % 307.51/44.15 % (2472593)Peak memory usage: 4816 MB % 307.51/44.15 % (2472593)Instructions burned: 15851 (million) % 307.51/44.15 % Detected minimum model sizes of [5] % 307.51/44.15 % Detected maximum model sizes of [max] % 307.51/44.15 % (2472889)Cannot represent all propositional literals internally % 307.51/44.15 % (2472889)Refutation not found, incomplete strategy % 307.51/44.15 % (2472889)------------------------------ % 307.51/44.15 % (2472889)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 307.51/44.15 % (2472889)Lin % 307.51/44.15 Terminated %------------------------------------------------------------------------------