%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : CSR080+6 : TPTP v9.3.1. Bugfixed v7.3.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % Computer : n019.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 09:45:01 AM UTC 2026 % Result : Timeout 295.53s 43.25s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : CSR080+6 : TPTP v9.3.1. Bugfixed v7.3.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.07/0.17 % Computer : n019.cluster.edu % 0.07/0.17 % Model : x86_64 x86_64 % 0.07/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.07/0.17 % Memory : 8046.5625MB % 0.07/0.17 % OS : Linux 6.8.0-71-generic % 0.07/0.17 % CPULimit : 300 % 0.07/0.17 % WCLimit : 300 % 0.07/0.17 % DateTime : Mon Sep 28 22:31:03 UTC 2026 % 0.07/0.18 % CPUTime : % 0.07/0.18 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.07/0.21 Running first-order model finding % 0.07/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 % 27.21/5.40 % (352891)Will run a generic schedule for satisfiability detection. % 27.21/5.40 % (352897)% WARNING: option uhcvi not known. % 27.21/5.40 % (352899)dis+10_1_sil=32000:sp=arity:random_seed=327003888:i=103:fgj=on_2984 on theBenchmark for (2984ds/103Mi) % 27.21/5.40 % (352896)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=418707376_2984 on theBenchmark for (2984ds/0Mi) % 27.21/5.40 % (352897)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2187581828:i=135531:add=off:rawr=on_2984 on theBenchmark for (2984ds/135531Mi) % 27.21/5.40 % (352898)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=23549731:i=88024:add=on:rawr=on_2984 on theBenchmark for (2984ds/88024Mi) % 27.21/5.40 % (352900)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=858436165:i=116_2984 on theBenchmark for (2984ds/116Mi) % 27.21/5.40 % (352901)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=168700846:i=131_2984 on theBenchmark for (2984ds/131Mi) % 27.21/5.40 % (352902)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3560478861:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2984 on theBenchmark for (2984ds/159Mi) % 27.21/5.40 % (352899)Instruction limit reached! % 27.21/5.40 % (352899)------------------------------ % 27.21/5.40 % (352899)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 27.21/5.40 % (352899)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.21/5.40 % (352899)CaDiCaL version: 2.1.3 % 27.21/5.40 % (352899)Termination reason: Instruction limit % 27.21/5.40 % (352899)Termination phase: Preprocessing 1 % 27.21/5.40 % (352899)Time elapsed: 0.041 s % 27.21/5.40 % (352899)Peak memory usage: 90 MB % 27.21/5.40 % (352899)Instructions burned: 103 (million) % 27.21/5.40 % (352910)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1467913769:i=714:nm=2_2983 on theBenchmark for (2983ds/714Mi) % 27.21/5.40 % (352900)Instruction limit reached! % 27.21/5.40 % (352900)------------------------------ % 27.21/5.40 % (352900)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 27.21/5.40 % (352900)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.21/5.40 % (352900)CaDiCaL version: 2.1.3 % 27.21/5.40 % (352900)Termination reason: Instruction limit % 27.21/5.40 % (352900)Termination phase: Preprocessing 1 % 27.21/5.40 % (352900)Time elapsed: 0.083 s % 27.21/5.40 % (352900)Peak memory usage: 90 MB % 27.21/5.40 % (352900)Instructions burned: 116 (million) % 27.21/5.40 % (352901)Instruction limit reached! % 27.21/5.40 % (352901)------------------------------ % 27.21/5.40 % (352901)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 27.21/5.40 % (352901)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.21/5.40 % (352901)CaDiCaL version: 2.1.3 % 27.21/5.40 % (352901)Termination reason: Instruction limit % 27.21/5.40 % (352901)Termination phase: Preprocessing 1 % 27.21/5.40 % (352901)Time elapsed: 0.084 s % 27.21/5.40 % (352901)Peak memory usage: 90 MB % 27.21/5.40 % (352901)Instructions burned: 131 (million) % 27.21/5.40 % (352902)Instruction limit reached! % 27.21/5.40 % (352902)------------------------------ % 27.21/5.40 % (352902)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 27.21/5.40 % (352902)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.21/5.40 % (352902)CaDiCaL version: 2.1.3 % 27.21/5.40 % (352902)Termination reason: Instruction limit % 27.21/5.40 % (352902)Termination phase: Preprocessing 1 % 27.21/5.40 % (352902)Time elapsed: 0.104 s % 27.21/5.40 % (352902)Peak memory usage: 90 MB % 27.21/5.40 % (352902)Instructions burned: 160 (million) % 27.21/5.40 % (352912)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=101085458:i=131:bd=preordered:fsd=on_2983 on theBenchmark for (2983ds/131Mi) % 27.21/5.40 % (352913)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=2276367986:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2983 on theBenchmark for (2983ds/684Mi) % 27.21/5.40 % (352916)ott-21_1_sil=16000:fs=off:random_seed=416190432:i=180:av=off:fsr=off_2982 on theBenchmark for (2982ds/180Mi) % 27.21/5.40 % (352912)Instruction limit reached! % 27.21/5.40 % (352912)------------------------------ % 27.21/5.40 % (352912)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 27.21/5.40 % (352912)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.21/5.40 % (352912)CaDiCaL version: 2.1.3 % 27.21/5.40 % (352912)Termination reason: Instruction limit % 38.98/7.84 % (352912)Termination phase: Preprocessing 1 % 38.98/7.84 % (352912)Time elapsed: 0.084 s % 38.98/7.84 % (352912)Peak memory usage: 90 MB % 38.98/7.84 % (352912)Instructions burned: 131 (million) % 38.98/7.84 % (352918)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3033757719:i=477:bd=all_2981 on theBenchmark for (2981ds/477Mi) % 38.98/7.84 % (352916)Instruction limit reached! % 38.98/7.84 % (352916)------------------------------ % 38.98/7.84 % (352916)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 38.98/7.84 % (352916)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 38.98/7.84 % (352916)CaDiCaL version: 2.1.3 % 38.98/7.84 % (352916)Termination reason: Instruction limit % 38.98/7.84 % (352916)Termination phase: Unused predicate definition removal % 38.98/7.84 % (352916)Time elapsed: 0.124 s % 38.98/7.84 % (352916)Peak memory usage: 91 MB % 38.98/7.84 % (352916)Instructions burned: 180 (million) % 38.98/7.84 % (352910)Instruction limit reached! % 38.98/7.84 % (352910)------------------------------ % 38.98/7.84 % (352910)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 38.98/7.84 % (352910)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 38.98/7.84 % (352910)CaDiCaL version: 2.1.3 % 38.98/7.84 % (352910)Termination reason: Instruction limit % 38.98/7.84 % (352910)Termination phase: Unused predicate definition removal % 38.98/7.84 % (352910)Time elapsed: 0.238 s % 38.98/7.84 % (352910)Peak memory usage: 127 MB % 38.98/7.84 % (352910)Instructions burned: 715 (million) % 38.98/7.84 % (352920)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1500200657:fmbsr=1.3:i=865:ins=25_2981 on theBenchmark for (2981ds/865Mi) % 38.98/7.84 % (352922)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1715339886:i=1179_2980 on theBenchmark for (2980ds/1179Mi) % 38.98/7.84 % (352913)Instruction limit reached! % 38.98/7.84 % (352913)------------------------------ % 38.98/7.84 % (352913)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 38.98/7.84 % (352913)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 38.98/7.84 % (352913)CaDiCaL version: 2.1.3 % 38.98/7.84 % (352913)Termination reason: Instruction limit % 38.98/7.84 % (352913)Termination phase: NewCNF % 38.98/7.84 % (352913)Time elapsed: 0.436 s % 38.98/7.84 % (352913)Peak memory usage: 106 MB % 38.98/7.84 % (352913)Instructions burned: 684 (million) % 38.98/7.84 % (352918)Instruction limit reached! % 38.98/7.84 % (352918)------------------------------ % 38.98/7.84 % (352918)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 38.98/7.84 % (352918)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 38.98/7.84 % (352918)CaDiCaL version: 2.1.3 % 38.98/7.84 % (352918)Termination reason: Instruction limit % 38.98/7.84 % (352918)Termination phase: Preprocessing 3 % 38.98/7.84 % (352918)Time elapsed: 0.339 s % 38.98/7.84 % (352918)Peak memory usage: 102 MB % 38.98/7.84 % (352918)Instructions burned: 478 (million) % 38.98/7.84 % (352924)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=977928164:i=889:ins=1_2978 on theBenchmark for (2978ds/889Mi) % 38.98/7.84 % (352925)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=3835393697:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2978 on theBenchmark for (2978ds/692Mi) % 38.98/7.84 % (352922)Instruction limit reached! % 38.98/7.84 % (352922)------------------------------ % 38.98/7.84 % (352922)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 38.98/7.84 % (352922)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 38.98/7.84 % (352922)CaDiCaL version: 2.1.3 % 38.98/7.84 % (352922)Termination reason: Instruction limit % 38.98/7.84 % (352922)Termination phase: Property scanning % 38.98/7.84 % (352922)Time elapsed: 0.396 s % 38.98/7.84 % (352922)Peak memory usage: 111 MB % 38.98/7.84 % (352922)Instructions burned: 1180 (million) % 38.98/7.84 % (352928)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=310586596:i=879:kws=inv_precedence:fsr=off_2976 on theBenchmark for (2976ds/879Mi) % 38.98/7.84 % (352920)Instruction limit reached! % 38.98/7.84 % (352920)------------------------------ % 38.98/7.84 % (352920)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 38.98/7.84 % (352920)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 38.98/7.84 % (352920)CaDiCaL version: 2.1.3 % 38.98/7.84 % (352920)Termination reason: Instruction limit % 74.29/12.12 % (352920)Termination phase: Naming % 74.29/12.12 % (352920)Time elapsed: 0.518 s % 74.29/12.12 % (352920)Peak memory usage: 156 MB % 74.29/12.12 % (352920)Instructions burned: 867 (million) % 74.29/12.12 % (352930)fmb+10_1_sil=64000:random_seed=2299858409:i=22061:nm=2:gsp=on_2975 on theBenchmark for (2975ds/22061Mi) % 74.29/12.12 % (352928)Instruction limit reached! % 74.29/12.12 % (352928)------------------------------ % 74.29/12.12 % (352928)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 74.29/12.12 % (352928)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 74.29/12.12 % (352928)CaDiCaL version: 2.1.3 % 74.29/12.12 % (352928)Termination reason: Instruction limit % 74.29/12.12 % (352928)Termination phase: NewCNF % 74.29/12.12 % (352928)Time elapsed: 0.273 s % 74.29/12.12 % (352928)Peak memory usage: 114 MB % 74.29/12.12 % (352928)Instructions burned: 884 (million) % 74.29/12.12 % (352932)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1240677203:i=9515:nm=5_2973 on theBenchmark for (2973ds/9515Mi) % 74.29/12.12 % (352925)Instruction limit reached! % 74.29/12.12 % (352925)------------------------------ % 74.29/12.12 % (352925)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 74.29/12.12 % (352925)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 74.29/12.12 % (352925)CaDiCaL version: 2.1.3 % 74.29/12.12 % (352925)Termination reason: Instruction limit % 74.29/12.12 % (352925)Termination phase: NewCNF % 74.29/12.12 % (352925)Time elapsed: 0.434 s % 74.29/12.12 % (352925)Peak memory usage: 106 MB % 74.29/12.12 % (352925)Instructions burned: 694 (million) % 74.29/12.12 % (352934)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3542408903:fmbsr=1.7:i=920_2973 on theBenchmark for (2973ds/920Mi) % 74.29/12.12 % (352924)Instruction limit reached! % 74.29/12.12 % (352924)------------------------------ % 74.29/12.12 % (352924)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 74.29/12.12 % (352924)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 74.29/12.12 % (352924)CaDiCaL version: 2.1.3 % 74.29/12.12 % (352924)Termination reason: Instruction limit % 74.29/12.12 % (352924)Termination phase: Naming % 74.29/12.12 % (352924)Time elapsed: 0.536 s % 74.29/12.12 % (352924)Peak memory usage: 149 MB % 74.29/12.12 % (352924)Instructions burned: 889 (million) % 74.29/12.12 % (352936)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=945991766:i=5131_2972 on theBenchmark for (2972ds/5131Mi) % 74.29/12.12 % (352934)Instruction limit reached! % 74.29/12.12 % (352934)------------------------------ % 74.29/12.12 % (352934)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 74.29/12.12 % (352934)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 74.29/12.12 % (352934)CaDiCaL version: 2.1.3 % 74.29/12.12 % (352934)Termination reason: Instruction limit % 74.29/12.12 % (352934)Termination phase: Preprocessing 3 % 74.29/12.12 % (352934)Time elapsed: 0.583 s % 74.29/12.12 % (352934)Peak memory usage: 149 MB % 74.29/12.12 % (352934)Instructions burned: 921 (million) % 74.29/12.12 % (352938)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3558942512:i=1472:ins=7:fdi=8:gsp=on_2967 on theBenchmark for (2967ds/1472Mi) % 74.29/12.12 % (352938)Instruction limit reached! % 74.29/12.12 % (352938)------------------------------ % 74.29/12.12 % (352938)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 74.29/12.12 % (352938)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 74.29/12.12 % (352938)CaDiCaL version: 2.1.3 % 74.29/12.12 % (352938)Termination reason: Instruction limit % 74.29/12.12 % (352938)Termination phase: Saturation % 74.29/12.12 % (352938)Time elapsed: 0.823 s % 74.29/12.12 % (352938)Peak memory usage: 117 MB % 74.29/12.12 % (352938)Instructions burned: 1472 (million) % 74.29/12.12 % (352940)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=690969848:i=6324_2958 on theBenchmark for (2958ds/6324Mi) % 74.29/12.12 % (352932)Instruction limit reached! % 74.29/12.12 % (352932)------------------------------ % 74.29/12.12 % (352932)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 74.29/12.12 % (352932)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 74.29/12.12 % (352932)CaDiCaL version: 2.1.3 % 74.29/12.12 % (352932)Termination reason: Instruction limit % 74.29/12.12 % (352932)Termination phase: Finite model building preprocessing % 74.29/12.12 % (352932)Time elapsed: 2.520 s % 74.29/12.12 % (352932)Peak memory usage: 284 MB % 74.29/12.12 % (352932)Instructions burned: 9520 (million) % 74.29/12.12 % (352942)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=970831251:fmbsr=2.30978:i=2174_2948 on theBenchmark for (2948ds/2174Mi) % 115.22/17.82 % (352936)Instruction limit reached! % 115.22/17.82 % (352936)------------------------------ % 115.22/17.82 % (352936)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 115.22/17.82 % (352936)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 115.22/17.82 % (352936)CaDiCaL version: 2.1.3 % 115.22/17.82 % (352936)Termination reason: Instruction limit % 115.22/17.82 % (352936)Termination phase: Saturation % 115.22/17.82 % (352936)Time elapsed: 2.792 s % 115.22/17.82 % (352936)Peak memory usage: 167 MB % 115.22/17.82 % (352936)Instructions burned: 5132 (million) % 115.22/17.82 % (352944)ott-2_1_sil=16000:newcnf=on:random_seed=2056254130:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2944 on theBenchmark for (2944ds/869Mi) % 115.22/17.82 % (352942)Instruction limit reached! % 115.22/17.82 % (352942)------------------------------ % 115.22/17.82 % (352942)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 115.22/17.82 % (352942)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 115.22/17.82 % (352942)CaDiCaL version: 2.1.3 % 115.22/17.82 % (352942)Termination reason: Instruction limit % 115.22/17.82 % (352942)Termination phase: Equality resolution with deletion % 115.22/17.82 % (352942)Time elapsed: 0.651 s % 115.22/17.82 % (352942)Peak memory usage: 168 MB % 115.22/17.82 % (352942)Instructions burned: 2176 (million) % 115.22/17.82 % (352946)ott+10_1_sil=32000:tgt=ground:random_seed=4231703570:i=5114:av=off_2941 on theBenchmark for (2941ds/5114Mi) % 115.22/17.82 % (352944)Instruction limit reached! % 115.22/17.82 % (352944)------------------------------ % 115.22/17.82 % (352944)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 115.22/17.82 % (352944)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 115.22/17.82 % (352944)CaDiCaL version: 2.1.3 % 115.22/17.82 % (352944)Termination reason: Instruction limit % 115.22/17.82 % (352944)Termination phase: NewCNF % 115.22/17.82 % (352944)Time elapsed: 0.475 s % 115.22/17.82 % (352944)Peak memory usage: 114 MB % 115.22/17.82 % (352944)Instructions burned: 871 (million) % 115.22/17.82 % (352948)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=1197041905:i=54282_2939 on theBenchmark for (2939ds/54282Mi) % 115.22/17.82 % Detected minimum model sizes of [617] % 115.22/17.82 % Detected maximum model sizes of [max] % 115.22/17.82 % (352930)Cannot represent all propositional literals internally % 115.22/17.82 % (352930)Refutation not found, incomplete strategy % 115.22/17.82 % (352930)------------------------------ % 115.22/17.82 % (352930)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 115.22/17.82 % (352930)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 115.22/17.82 % (352930)CaDiCaL version: 2.1.3 % 115.22/17.82 % (352930)Termination reason: Refutation not found, incomplete strategy % 115.22/17.82 % (352930)Time elapsed: 5.007 s % 115.22/17.82 % (352930)Peak memory usage: 286 MB % 115.22/17.82 % (352930)Instructions burned: 10356 (million) % 115.22/17.82 % (352940)Instruction limit reached! % 115.22/17.82 % (352940)------------------------------ % 115.22/17.82 % (352940)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 115.22/17.82 % (352940)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 115.22/17.82 % (352940)CaDiCaL version: 2.1.3 % 115.22/17.82 % (352940)Termination reason: Instruction limit % 115.22/17.82 % (352940)Termination phase: Finite model building preprocessing % 115.22/17.82 % (352940)Time elapsed: 3.331 s % 115.22/17.82 % (352940)Peak memory usage: 269 MB % 115.22/17.82 % (352940)Instructions burned: 6324 (million) % 115.22/17.82 % (352946)Instruction limit reached! % 115.22/17.82 % (352946)------------------------------ % 115.22/17.82 % (352946)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 115.22/17.82 % (352946)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 115.22/17.82 % (352946)CaDiCaL version: 2.1.3 % 115.22/17.82 % (352946)Termination reason: Instruction limit % 115.22/17.82 % (352946)Termination phase: Saturation % 115.22/17.82 % (352946)Time elapsed: 1.676 s % 115.22/17.82 % (352946)Peak memory usage: 179 MB % 115.22/17.82 % (352946)Instructions burned: 5117 (million) % 115.22/17.82 % (352950)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=208250694:i=3512:aac=none_2924 on theBenchmark for (2924ds/3512Mi) % 115.22/17.82 % (352930)------------------------------ % 115.22/17.82 % (352930)------------------------------ % 115.22/17.82 % (352952)dis+21_1_sil=32000:sas=cadical:random_seed=498477993:i=3773:amm=off_2924 on theBenchmark for (2924ds/3773Mi) % 115.22/17.82 % (352954)ott+11_1_sil=16000:gs=on:random_seed=1233698259:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2924 on theBenchmark for (2924ds/2251Mi) % 162.07/24.45 % Detected minimum model sizes of [617] % 162.07/24.45 % Detected maximum model sizes of [max] % 162.07/24.45 % (352896)Cannot represent all propositional literals internally % 162.07/24.45 % (352896)Refutation not found, incomplete strategy % 162.07/24.45 % (352896)------------------------------ % 162.07/24.45 % (352896)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 162.07/24.45 % (352896)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 162.07/24.45 % (352896)CaDiCaL version: 2.1.3 % 162.07/24.45 % (352896)Termination reason: Refutation not found, incomplete strategy % 162.07/24.45 % (352896)Time elapsed: 6.169 s % 162.07/24.45 % (352896)Peak memory usage: 327 MB % 162.07/24.45 % (352896)Instructions burned: 12450 (million) % 162.07/24.45 % (352896)------------------------------ % 162.07/24.45 % (352896)------------------------------ % 162.07/24.45 % (352956)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=3959836883:fmbsr=1.6:i=67534_2920 on theBenchmark for (2920ds/67534Mi) % 162.07/24.45 % (352952)Instruction limit reached! % 162.07/24.45 % (352952)------------------------------ % 162.07/24.45 % (352952)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 162.07/24.45 % (352952)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 162.07/24.45 % (352952)CaDiCaL version: 2.1.3 % 162.07/24.45 % (352952)Termination reason: Instruction limit % 162.07/24.45 % (352952)Termination phase: Saturation % 162.07/24.45 % (352952)Time elapsed: 1.172 s % 162.07/24.45 % (352952)Peak memory usage: 152 MB % 162.07/24.45 % (352952)Instructions burned: 3774 (million) % 162.07/24.45 % (352958)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=1115747610:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2912 on theBenchmark for (2912ds/4591Mi) % 162.07/24.45 % (352954)Instruction limit reached! % 162.07/24.45 % (352954)------------------------------ % 162.07/24.45 % (352954)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 162.07/24.45 % (352954)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 162.07/24.45 % (352954)CaDiCaL version: 2.1.3 % 162.07/24.45 % (352954)Termination reason: Instruction limit % 162.07/24.45 % (352954)Termination phase: Saturation % 162.07/24.45 % (352954)Time elapsed: 1.350 s % 162.07/24.45 % (352954)Peak memory usage: 130 MB % 162.07/24.45 % (352954)Instructions burned: 2251 (million) % 162.07/24.45 % (352960)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=98418569:i=29340_2910 on theBenchmark for (2910ds/29340Mi) % 162.07/24.45 % (352950)Instruction limit reached! % 162.07/24.45 % (352950)------------------------------ % 162.07/24.45 % (352950)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 162.07/24.45 % (352950)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 162.07/24.45 % (352950)CaDiCaL version: 2.1.3 % 162.07/24.45 % (352950)Termination reason: Instruction limit % 162.07/24.45 % (352950)Termination phase: Saturation % 162.07/24.45 % (352950)Time elapsed: 1.974 s % 162.07/24.45 % (352950)Peak memory usage: 149 MB % 162.07/24.45 % (352950)Instructions burned: 3513 (million) % 162.07/24.45 % (352962)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=1357082042:i=5211_2904 on theBenchmark for (2904ds/5211Mi) % 162.07/24.45 % (352958)Instruction limit reached! % 162.07/24.45 % (352958)------------------------------ % 162.07/24.45 % (352958)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 162.07/24.45 % (352958)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 162.07/24.45 % (352958)CaDiCaL version: 2.1.3 % 162.07/24.45 % (352958)Termination reason: Instruction limit % 162.07/24.45 % (352958)Termination phase: Saturation % 162.07/24.45 % (352958)Time elapsed: 1.421 s % 162.07/24.45 % (352958)Peak memory usage: 155 MB % 162.07/24.45 % (352958)Instructions burned: 4592 (million) % 162.07/24.45 % (352964)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=1328400173:i=5497:nm=2_2898 on theBenchmark for (2898ds/5497Mi) % 162.07/24.45 % (352964)Instruction limit reached! % 162.07/24.45 % (352964)------------------------------ % 162.07/24.45 % (352964)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 162.07/24.45 % (352964)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 162.07/24.45 % (352964)CaDiCaL version: 2.1.3 % 162.07/24.45 % (352964)Termination reason: Instruction limit % 162.07/24.45 % (352964)Termination phase: Finite model building preprocessing % 242.66/35.81 % (352964)Time elapsed: 1.693 s % 242.66/35.81 % (352964)Peak memory usage: 260 MB % 242.66/35.81 % (352964)Instructions burned: 5499 (million) % 242.66/35.81 % (352966)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=3363374850:fmbsr=2:i=46332_2880 on theBenchmark for (2880ds/46332Mi) % 242.66/35.81 % Detected minimum model sizes of [617] % 242.66/35.81 % Detected maximum model sizes of [max] % 242.66/35.81 % (352948)Cannot represent all propositional literals internally % 242.66/35.81 % (352948)Refutation not found, incomplete strategy % 242.66/35.81 % (352948)------------------------------ % 242.66/35.81 % (352948)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 242.66/35.81 % (352948)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 242.66/35.81 % (352948)CaDiCaL version: 2.1.3 % 242.66/35.81 % (352948)Termination reason: Refutation not found, incomplete strategy % 242.66/35.81 % (352948)Time elapsed: 6.060 s % 242.66/35.81 % (352948)Peak memory usage: 325 MB % 242.66/35.81 % (352948)Instructions burned: 12414 (million) % 242.66/35.81 % (352962)Instruction limit reached! % 242.66/35.81 % (352962)------------------------------ % 242.66/35.81 % (352962)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 242.66/35.81 % (352962)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 242.66/35.81 % (352962)CaDiCaL version: 2.1.3 % 242.66/35.81 % (352962)Termination reason: Instruction limit % 242.66/35.81 % (352962)Termination phase: Saturation % 242.66/35.81 % (352962)Time elapsed: 2.619 s % 242.66/35.81 % (352962)Peak memory usage: 182 MB % 242.66/35.81 % (352962)Instructions burned: 5211 (million) % 242.66/35.81 % (352968)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=1847582556:i=14071_2878 on theBenchmark for (2878ds/14071Mi) % 242.66/35.81 % (352948)------------------------------ % 242.66/35.81 % (352948)------------------------------ % 242.66/35.81 % (352970)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1544557320:i=22565:add=on:rawr=on_2876 on theBenchmark for (2876ds/22565Mi) % 242.66/35.81 % Detected minimum model sizes of [617] % 242.66/35.81 % Detected maximum model sizes of [max] % 242.66/35.81 % (352956)Cannot represent all propositional literals internally % 242.66/35.81 % (352956)Refutation not found, incomplete strategy % 242.66/35.81 % (352956)------------------------------ % 242.66/35.81 % (352956)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 242.66/35.81 % (352956)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 242.66/35.81 % (352956)CaDiCaL version: 2.1.3 % 242.66/35.81 % (352956)Termination reason: Refutation not found, incomplete strategy % 242.66/35.81 % (352956)Time elapsed: 5.819 s % 242.66/35.81 % (352956)Peak memory usage: 312 MB % 242.66/35.81 % (352956)Instructions burned: 12440 (million) % 242.66/35.81 % (352956)------------------------------ % 242.66/35.81 % (352956)------------------------------ % 242.66/35.81 % (352972)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=2750651791:i=8173:av=off_2861 on theBenchmark for (2861ds/8173Mi) % 242.66/35.81 % Detected minimum model sizes of [617] % 242.66/35.81 % Detected maximum model sizes of [max] % 242.66/35.81 % (352966)Cannot represent all propositional literals internally % 242.66/35.81 % (352966)Refutation not found, incomplete strategy % 242.66/35.81 % (352966)------------------------------ % 242.66/35.81 % (352966)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 242.66/35.81 % (352966)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 242.66/35.81 % (352966)CaDiCaL version: 2.1.3 % 242.66/35.81 % (352966)Termination reason: Refutation not found, incomplete strategy % 242.66/35.81 % (352966)Time elapsed: 3.277 s % 242.66/35.81 % (352966)Peak memory usage: 312 MB % 242.66/35.81 % (352966)Instructions burned: 12441 (million) % 242.66/35.81 % (352966)------------------------------ % 242.66/35.81 % (352966)------------------------------ % 242.66/35.81 % (352974)dis+10_16:1_sil=16000:random_seed=987016670:i=9155:fsr=off_2846 on theBenchmark for (2846ds/9155Mi) % 242.66/35.81 % Detected minimum model sizes of [617] % 242.66/35.81 % Detected maximum model sizes of [max] % 242.66/35.81 % (352968)Cannot represent all propositional literals internally % 242.66/35.81 % (352968)Refutation not found, incomplete strategy % 242.66/35.81 % (352968)------------------------------ % 242.66/35.81 % (352968)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 242.66/35.81 % (352968)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 242.66/35.81 % (352968)CaDiCaL version: 2.1.3 % 242.66/35.81 % (352968)Termination reason: Refutation not found, incomplete strategy % 242.66/35.81 % (352968)Time elapsed: 5.369 s % 295.53/43.25 % (352968)Peak memory usage: 304 MB % 295.53/43.25 % (352968)Instructions burned: 11289 (million) % 295.53/43.25 % (352968)------------------------------ % 295.53/43.25 % (352968)------------------------------ % 295.53/43.25 % (352978)ott-3_8_sil=64000:random_seed=3520971698:i=20139:bs=on_2822 on theBenchmark for (2822ds/20139Mi) % 295.53/43.25 % (352972)Instruction limit reached! % 295.53/43.25 % (352972)------------------------------ % 295.53/43.25 % (352972)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 295.53/43.25 % (352972)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 295.53/43.25 % (352972)CaDiCaL version: 2.1.3 % 295.53/43.25 % (352972)Termination reason: Instruction limit % 295.53/43.25 % (352972)Termination phase: Saturation % 295.53/43.25 % (352972)Time elapsed: 4.091 s % 295.53/43.25 % (352972)Peak memory usage: 206 MB % 295.53/43.25 % (352972)Instructions burned: 8174 (million) % 295.53/43.25 % (352980)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=152061333:fmbsr=2:i=32576_2819 on theBenchmark for (2819ds/32576Mi) % 295.53/43.25 % (352974)Instruction limit reached! % 295.53/43.25 % (352974)------------------------------ % 295.53/43.25 % (352974)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 295.53/43.25 % (352974)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 295.53/43.25 % (352974)CaDiCaL version: 2.1.3 % 295.53/43.25 % (352974)Termination reason: Instruction limit % 295.53/43.25 % (352974)Termination phase: Saturation % 295.53/43.25 % (352974)Time elapsed: 2.818 s % 295.53/43.25 % (352974)Peak memory usage: 220 MB % 295.53/43.25 % (352974)Instructions burned: 9158 (million) % 295.53/43.25 % (352982)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=402567780:i=11404_2818 on theBenchmark for (2818ds/11404Mi) % 295.53/43.25 % (352970)Instruction limit reached! % 295.53/43.25 % (352970)------------------------------ % 295.53/43.25 % (352970)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 295.53/43.25 % (352970)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 295.53/43.25 % (352970)CaDiCaL version: 2.1.3 % 295.53/43.25 % (352970)Termination reason: Instruction limit % 295.53/43.25 % (352970)Termination phase: Saturation % 295.53/43.25 % (352970)Time elapsed: 9.012 s % 295.53/43.25 % (352970)Peak memory usage: 294 MB % 295.53/43.25 % (352970)Instructions burned: 22565 (million) % 295.53/43.25 % (352984)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=3448162079:i=14134_2786 on theBenchmark for (2786ds/14134Mi) % 295.53/43.25 % (352982)Instruction limit reached! % 295.53/43.25 % (352982)------------------------------ % 295.53/43.25 % (352982)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 295.53/43.25 % (352982)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 295.53/43.25 % (352982)CaDiCaL version: 2.1.3 % 295.53/43.25 % (352982)Termination reason: Instruction limit % 295.53/43.25 % (352982)Termination phase: Saturation % 295.53/43.25 % (352982)Time elapsed: 3.584 s % 295.53/43.25 % (352982)Peak memory usage: 266 MB % 295.53/43.25 % (352982)Instructions burned: 11404 (million) % 295.53/43.25 % (352986)dis+33_16_sil=32000:sac=on:random_seed=1806265233:i=15851:nm=0_2782 on theBenchmark for (2782ds/15851Mi) % 295.53/43.25 % (352960)Instruction limit reached! % 295.53/43.25 % (352960)------------------------------ % 295.53/43.25 % (352960)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 295.53/43.25 % (352960)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 295.53/43.25 % (352960)CaDiCaL version: 2.1.3 % 295.53/43.25 % (352960)Termination reason: Instruction limit % 295.53/43.25 % (352960)Termination phase: Saturation % 295.53/43.25 % (352960)Time elapsed: 15.107 s % 295.53/43.25 % (352960)Peak memory usage: 374 MB % 295.53/43.25 % (352960)Instructions burned: 29341 (million) % 295.53/43.25 % (352988)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=1274817166:avsq=on:i=17627:add=on:amm=off_2758 on theBenchmark for (2758ds/17627Mi) % 295.53/43.25 % Detected minimum model sizes of [617] % 295.53/43.25 % Detected maximum model sizes of [max] % 295.53/43.25 % (352980)Cannot represent all propositional literals internally % 295.53/43.25 % (352980)Refutation not found, incomplete strategy % 295.53/43.25 % (352980)------------------------------ % 295.53/43.25 % (352980)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 295.53/43.25 % (352980)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 295.53/43.25 % (352980)CaDiCaL version: 2.1.3 % 295.53/43.25 % (352980)Termination reason: Refutation not found, incomplete strategy % 295.53/43.25 % (352980)Time elapsed: 6.155 s % 295.53/43.25 % (35298 %------------------------------------------------------------------------------