%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWW358+1 : TPTP v9.3.1. Released v5.2.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % Computer : n011.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 29 01:39:52 PM UTC 2026 % Result : Timeout 293.24s 42.03s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWW358+1 : TPTP v9.3.1. Released v5.2.0. % 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.09/0.21 % Computer : n011.cluster.edu % 0.09/0.21 % Model : x86_64 x86_64 % 0.09/0.21 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.21 % Memory : 8046.5625MB % 0.09/0.21 % OS : Linux 6.8.0-71-generic % 0.09/0.21 % CPULimit : 300 % 0.09/0.21 % WCLimit : 300 % 0.09/0.21 % DateTime : Mon Sep 28 13:41:01 UTC 2026 % 0.09/0.22 % CPUTime : % 0.09/0.22 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.09/0.25 Running first-order model finding % 0.09/0.25 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 % 22.28/3.79 % (3386783)Will run a generic schedule for satisfiability detection. % 22.28/3.79 % (3386793)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=361943310:i=131_2996 on theBenchmark for (2996ds/131Mi) % 22.28/3.79 % (3386789)% WARNING: option uhcvi not known. % 22.28/3.79 % (3386788)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=518325732_2996 on theBenchmark for (2996ds/0Mi) % 22.28/3.79 % (3386789)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=605478764:i=135531:add=off:rawr=on_2996 on theBenchmark for (2996ds/135531Mi) % 22.28/3.79 % (3386790)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2096955117:i=88024:add=on:rawr=on_2996 on theBenchmark for (2996ds/88024Mi) % 22.28/3.79 % (3386791)dis+10_1_sil=32000:sp=arity:random_seed=3608663001:i=103:fgj=on_2996 on theBenchmark for (2996ds/103Mi) % 22.28/3.79 % (3386792)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=20711997:i=116_2996 on theBenchmark for (2996ds/116Mi) % 22.28/3.79 % (3386794)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3645333413:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2996 on theBenchmark for (2996ds/159Mi) % 22.28/3.79 % (3386793)Instruction limit reached! % 22.28/3.79 % (3386793)------------------------------ % 22.28/3.79 % (3386793)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.28/3.79 % (3386793)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.28/3.79 % (3386793)CaDiCaL version: 2.1.3 % 22.28/3.79 % (3386793)Termination reason: Instruction limit % 22.28/3.79 % (3386793)Termination phase: Preprocessing 3 % 22.28/3.79 % (3386793)Time elapsed: 0.045 s % 22.28/3.79 % (3386793)Peak memory usage: 20 MB % 22.28/3.79 % (3386793)Instructions burned: 134 (million) % 22.28/3.79 % (3386802)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2015186852:i=714:nm=2_2995 on theBenchmark for (2995ds/714Mi) % 22.28/3.79 % (3386791)Instruction limit reached! % 22.28/3.79 % (3386791)------------------------------ % 22.28/3.79 % (3386791)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.28/3.79 % (3386791)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.28/3.79 % (3386791)CaDiCaL version: 2.1.3 % 22.28/3.79 % (3386791)Termination reason: Instruction limit % 22.28/3.79 % (3386791)Termination phase: Preprocessing 3 % 22.28/3.79 % (3386791)Time elapsed: 0.064 s % 22.28/3.79 % (3386791)Peak memory usage: 20 MB % 22.28/3.79 % (3386791)Instructions burned: 103 (million) % 22.28/3.79 % (3386792)Instruction limit reached! % 22.28/3.79 % (3386792)------------------------------ % 22.28/3.79 % (3386792)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.28/3.79 % (3386792)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.28/3.79 % (3386792)CaDiCaL version: 2.1.3 % 22.28/3.79 % (3386792)Termination reason: Instruction limit % 22.28/3.79 % (3386792)Termination phase: NewCNF % 22.28/3.79 % (3386792)Time elapsed: 0.075 s % 22.28/3.79 % (3386792)Peak memory usage: 21 MB % 22.28/3.79 % (3386792)Instructions burned: 117 (million) % 22.28/3.79 % (3386804)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2256950627:i=131:bd=preordered:fsd=on_2995 on theBenchmark for (2995ds/131Mi) % 22.28/3.79 % (3386794)Instruction limit reached! % 22.28/3.79 % (3386794)------------------------------ % 22.28/3.79 % (3386794)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.28/3.79 % (3386794)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.28/3.79 % (3386794)CaDiCaL version: 2.1.3 % 22.28/3.79 % (3386794)Termination reason: Instruction limit % 22.28/3.79 % (3386794)Termination phase: Clausification % 22.28/3.79 % (3386794)Time elapsed: 0.096 s % 22.28/3.79 % (3386794)Peak memory usage: 21 MB % 22.28/3.79 % (3386794)Instructions burned: 160 (million) % 22.28/3.79 % (3386805)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=3981186707:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2995 on theBenchmark for (2995ds/684Mi) % 22.28/3.79 % (3386808)ott-21_1_sil=16000:fs=off:random_seed=3608662356:i=180:av=off:fsr=off_2995 on theBenchmark for (2995ds/180Mi) % 22.28/3.79 % (3386804)Instruction limit reached! % 22.28/3.79 % (3386804)------------------------------ % 22.28/3.79 % (3386804)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.28/3.79 % (3386804)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 54.88/8.33 % (3386804)CaDiCaL version: 2.1.3 % 54.88/8.33 % (3386804)Termination reason: Instruction limit % 54.88/8.33 % (3386804)Termination phase: Preprocessing 3 % 54.88/8.33 % (3386804)Time elapsed: 0.079 s % 54.88/8.33 % (3386804)Peak memory usage: 20 MB % 54.88/8.33 % (3386804)Instructions burned: 131 (million) % 54.88/8.33 % (3386810)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2726971796:i=477:bd=all_2994 on theBenchmark for (2994ds/477Mi) % 54.88/8.33 % (3386808)Instruction limit reached! % 54.88/8.33 % (3386808)------------------------------ % 54.88/8.33 % (3386808)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 54.88/8.33 % (3386808)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 54.88/8.33 % (3386808)CaDiCaL version: 2.1.3 % 54.88/8.33 % (3386808)Termination reason: Instruction limit % 54.88/8.33 % (3386808)Termination phase: Property scanning % 54.88/8.33 % (3386808)Time elapsed: 0.105 s % 54.88/8.33 % (3386808)Peak memory usage: 22 MB % 54.88/8.33 % (3386808)Instructions burned: 180 (million) % 54.88/8.33 % (3386802)Instruction limit reached! % 54.88/8.33 % (3386802)------------------------------ % 54.88/8.33 % (3386802)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 54.88/8.33 % (3386802)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 54.88/8.33 % (3386802)CaDiCaL version: 2.1.3 % 54.88/8.33 % (3386802)Termination reason: Instruction limit % 54.88/8.33 % (3386802)Termination phase: Finite model building preprocessing % 54.88/8.33 % (3386802)Time elapsed: 0.180 s % 54.88/8.33 % (3386802)Peak memory usage: 25 MB % 54.88/8.33 % (3386802)Instructions burned: 718 (million) % 54.88/8.33 % (3386813)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2161579655:i=1179_2993 on theBenchmark for (2993ds/1179Mi) % 54.88/8.33 % (3386812)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3195575995:fmbsr=1.3:i=865:ins=25_2993 on theBenchmark for (2993ds/865Mi) % 54.88/8.33 % (3386810)Instruction limit reached! % 54.88/8.33 % (3386810)------------------------------ % 54.88/8.33 % (3386810)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 54.88/8.33 % (3386810)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 54.88/8.33 % (3386810)CaDiCaL version: 2.1.3 % 54.88/8.33 % (3386810)Termination reason: Instruction limit % 54.88/8.33 % (3386810)Termination phase: Property scanning % 54.88/8.33 % (3386810)Time elapsed: 0.224 s % 54.88/8.33 % (3386810)Peak memory usage: 23 MB % 54.88/8.33 % (3386810)Instructions burned: 479 (million) % 54.88/8.33 % (3386805)Instruction limit reached! % 54.88/8.33 % (3386805)------------------------------ % 54.88/8.33 % (3386805)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 54.88/8.33 % (3386805)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 54.88/8.33 % (3386805)CaDiCaL version: 2.1.3 % 54.88/8.33 % (3386805)Termination reason: Instruction limit % 54.88/8.33 % (3386805)Termination phase: Saturation % 54.88/8.33 % (3386805)Time elapsed: 0.319 s % 54.88/8.33 % (3386805)Peak memory usage: 25 MB % 54.88/8.33 % (3386805)Instructions burned: 686 (million) % 54.88/8.33 % (3386816)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2450995099:i=889:ins=1_2992 on theBenchmark for (2992ds/889Mi) % 54.88/8.33 % (3386817)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=1408643385:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2991 on theBenchmark for (2991ds/692Mi) % 54.88/8.33 % (3386813)Instruction limit reached! % 54.88/8.33 % (3386813)------------------------------ % 54.88/8.33 % (3386813)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 54.88/8.33 % (3386813)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 54.88/8.33 % (3386813)CaDiCaL version: 2.1.3 % 54.88/8.33 % (3386813)Termination reason: Instruction limit % 54.88/8.33 % (3386813)Termination phase: Saturation % 54.88/8.33 % (3386813)Time elapsed: 0.339 s % 54.88/8.33 % (3386813)Peak memory usage: 31 MB % 54.88/8.33 % (3386813)Instructions burned: 1180 (million) % 54.88/8.33 % (3386820)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=507159766:i=879:kws=inv_precedence:fsr=off_2990 on theBenchmark for (2990ds/879Mi) % 54.88/8.33 % (3386812)Instruction limit reached! % 54.88/8.33 % (3386812)------------------------------ % 54.88/8.33 % (3386812)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 54.88/8.33 % (3386812)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 122.30/17.83 % (3386812)CaDiCaL version: 2.1.3 % 122.30/17.83 % (3386812)Termination reason: Instruction limit % 122.30/17.83 % (3386812)Termination phase: Finite model building preprocessing % 122.30/17.83 % (3386812)Time elapsed: 0.401 s % 122.30/17.83 % (3386812)Peak memory usage: 30 MB % 122.30/17.83 % (3386812)Instructions burned: 865 (million) % 122.30/17.83 % (3386822)fmb+10_1_sil=64000:random_seed=2156771881:i=22061:nm=2:gsp=on_2989 on theBenchmark for (2989ds/22061Mi) % 122.30/17.83 % (3386817)Instruction limit reached! % 122.30/17.83 % (3386817)------------------------------ % 122.30/17.83 % (3386817)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 122.30/17.83 % (3386817)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 122.30/17.83 % (3386817)CaDiCaL version: 2.1.3 % 122.30/17.83 % (3386817)Termination reason: Instruction limit % 122.30/17.83 % (3386817)Termination phase: Saturation % 122.30/17.83 % (3386817)Time elapsed: 0.346 s % 122.30/17.83 % (3386817)Peak memory usage: 28 MB % 122.30/17.83 % (3386817)Instructions burned: 692 (million) % 122.30/17.83 % (3386824)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3207092290:i=9515:nm=5_2988 on theBenchmark for (2988ds/9515Mi) % 122.30/17.83 % (3386820)Instruction limit reached! % 122.30/17.83 % (3386820)------------------------------ % 122.30/17.83 % (3386820)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 122.30/17.83 % (3386820)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 122.30/17.83 % (3386820)CaDiCaL version: 2.1.3 % 122.30/17.83 % (3386820)Termination reason: Instruction limit % 122.30/17.83 % (3386820)Termination phase: Saturation % 122.30/17.83 % (3386820)Time elapsed: 0.229 s % 122.30/17.83 % (3386820)Peak memory usage: 30 MB % 122.30/17.83 % (3386820)Instructions burned: 885 (million) % 122.30/17.83 % (3386826)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2253280852:fmbsr=1.7:i=920_2987 on theBenchmark for (2987ds/920Mi) % 122.30/17.83 % (3386816)Instruction limit reached! % 122.30/17.83 % (3386816)------------------------------ % 122.30/17.83 % (3386816)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 122.30/17.83 % (3386816)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 122.30/17.83 % (3386816)CaDiCaL version: 2.1.3 % 122.30/17.83 % (3386816)Termination reason: Instruction limit % 122.30/17.83 % (3386816)Termination phase: Finite model building preprocessing % 122.30/17.83 % (3386816)Time elapsed: 0.419 s % 122.30/17.83 % (3386816)Peak memory usage: 31 MB % 122.30/17.83 % (3386816)Instructions burned: 889 (million) % 122.30/17.83 % (3386828)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=63836031:i=5131_2987 on theBenchmark for (2987ds/5131Mi) % 122.30/17.83 % (3386826)Instruction limit reached! % 122.30/17.83 % (3386826)------------------------------ % 122.30/17.83 % (3386826)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 122.30/17.83 % (3386826)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 122.30/17.83 % (3386826)CaDiCaL version: 2.1.3 % 122.30/17.83 % (3386826)Termination reason: Instruction limit % 122.30/17.83 % (3386826)Termination phase: Finite model building preprocessing % 122.30/17.83 % (3386826)Time elapsed: 0.237 s % 122.30/17.83 % (3386826)Peak memory usage: 32 MB % 122.30/17.83 % (3386826)Instructions burned: 924 (million) % 122.30/17.83 % (3386830)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1334393100:i=1472:ins=7:fdi=8:gsp=on_2985 on theBenchmark for (2985ds/1472Mi) % 122.30/17.83 % (3386830)Instruction limit reached! % 122.30/17.83 % (3386830)------------------------------ % 122.30/17.83 % (3386830)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 122.30/17.83 % (3386830)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 122.30/17.83 % (3386830)CaDiCaL version: 2.1.3 % 122.30/17.83 % (3386830)Termination reason: Instruction limit % 122.30/17.83 % (3386830)Termination phase: Saturation % 122.30/17.83 % (3386830)Time elapsed: 0.340 s % 122.30/17.83 % (3386830)Peak memory usage: 28 MB % 122.30/17.83 % (3386830)Instructions burned: 1477 (million) % 122.30/17.83 % (3386832)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=18576101:i=6324_2981 on theBenchmark for (2981ds/6324Mi) % 122.30/17.83 % (3386832)Instruction limit reached! % 122.30/17.83 % (3386832)------------------------------ % 122.30/17.83 % (3386832)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 122.30/17.83 % (3386832)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 122.30/17.83 % (3386832)CaDiCaL version: 2.1.3 % 122.30/17.83 % (3386832)Termination reason: Instruction limit % 209.21/30.12 % (3386832)Termination phase: Finite model building preprocessing % 209.21/30.12 % (3386832)Time elapsed: 1.702 s % 209.21/30.12 % (3386832)Peak memory usage: 68 MB % 209.21/30.12 % (3386832)Instructions burned: 6327 (million) % 209.21/30.12 % (3386834)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=3911912992:fmbsr=2.30978:i=2174_2964 on theBenchmark for (2964ds/2174Mi) % 209.21/30.12 % (3386834)Instruction limit reached! % 209.21/30.12 % (3386834)------------------------------ % 209.21/30.12 % (3386834)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 209.21/30.12 % (3386834)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 209.21/30.12 % (3386834)CaDiCaL version: 2.1.3 % 209.21/30.12 % (3386834)Termination reason: Instruction limit % 209.21/30.12 % (3386834)Termination phase: Finite model building preprocessing % 209.21/30.12 % (3386834)Time elapsed: 0.542 s % 209.21/30.12 % (3386834)Peak memory usage: 47 MB % 209.21/30.12 % (3386834)Instructions burned: 2177 (million) % 209.21/30.12 % (3386836)ott-2_1_sil=16000:newcnf=on:random_seed=3169723708:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2959 on theBenchmark for (2959ds/869Mi) % 209.21/30.12 % (3386828)Instruction limit reached! % 209.21/30.12 % (3386828)------------------------------ % 209.21/30.12 % (3386828)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 209.21/30.12 % (3386828)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 209.21/30.12 % (3386828)CaDiCaL version: 2.1.3 % 209.21/30.12 % (3386828)Termination reason: Instruction limit % 209.21/30.12 % (3386828)Termination phase: Saturation % 209.21/30.12 % (3386828)Time elapsed: 2.893 s % 209.21/30.12 % (3386828)Peak memory usage: 62 MB % 209.21/30.12 % (3386828)Instructions burned: 5131 (million) % 209.21/30.12 % (3386838)ott+10_1_sil=32000:tgt=ground:random_seed=3210077755:i=5114:av=off_2958 on theBenchmark for (2958ds/5114Mi) % 209.21/30.12 % (3386836)Instruction limit reached! % 209.21/30.12 % (3386836)------------------------------ % 209.21/30.12 % (3386836)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 209.21/30.12 % (3386836)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 209.21/30.12 % (3386836)CaDiCaL version: 2.1.3 % 209.21/30.12 % (3386836)Termination reason: Instruction limit % 209.21/30.12 % (3386836)Termination phase: Saturation % 209.21/30.12 % (3386836)Time elapsed: 0.238 s % 209.21/30.12 % (3386836)Peak memory usage: 28 MB % 209.21/30.12 % (3386836)Instructions burned: 871 (million) % 209.21/30.12 % (3386840)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=692666047:i=54282_2956 on theBenchmark for (2956ds/54282Mi) % 209.21/30.12 % (3386824)Instruction limit reached! % 209.21/30.12 % (3386824)------------------------------ % 209.21/30.12 % (3386824)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 209.21/30.12 % (3386824)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 209.21/30.12 % (3386824)CaDiCaL version: 2.1.3 % 209.21/30.12 % (3386824)Termination reason: Instruction limit % 209.21/30.12 % (3386824)Termination phase: Finite model building preprocessing % 209.21/30.12 % (3386824)Time elapsed: 4.893 s % 209.21/30.12 % (3386824)Peak memory usage: 96 MB % 209.21/30.12 % (3386824)Instructions burned: 9516 (million) % 209.21/30.12 % (3386842)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3518693165:i=3512:aac=none_2939 on theBenchmark for (2939ds/3512Mi) % 209.21/30.12 % (3386838)Instruction limit reached! % 209.21/30.12 % (3386838)------------------------------ % 209.21/30.12 % (3386838)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 209.21/30.12 % (3386838)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 209.21/30.12 % (3386838)CaDiCaL version: 2.1.3 % 209.21/30.12 % (3386838)Termination reason: Instruction limit % 209.21/30.12 % (3386838)Termination phase: Saturation % 209.21/30.12 % (3386838)Time elapsed: 3.122 s % 209.21/30.12 % (3386838)Peak memory usage: 65 MB % 209.21/30.12 % (3386838)Instructions burned: 5114 (million) % 209.21/30.12 % (3386844)dis+21_1_sil=32000:sas=cadical:random_seed=859743217:i=3773:amm=off_2926 on theBenchmark for (2926ds/3773Mi) % 209.21/30.12 % (3386842)Instruction limit reached! % 209.21/30.12 % (3386842)------------------------------ % 209.21/30.12 % (3386842)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 209.21/30.12 % (3386842)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 209.21/30.12 % (3386842)CaDiCaL version: 2.1.3 % 209.21/30.12 % (3386842)Termination reason: Instruction limit % 209.21/30.12 % (3386842)Termination phase: Saturation % 209.21/30.12 % (3386842)Time elapsed: 1.951 s % 293.24/42.03 % (3386842)Peak memory usage: 52 MB % 293.24/42.03 % (3386842)Instructions burned: 3512 (million) % 293.24/42.03 % (3386846)ott+11_1_sil=16000:gs=on:random_seed=989624513:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2919 on theBenchmark for (2919ds/2251Mi) % 293.24/42.03 % (3386846)Instruction limit reached! % 293.24/42.03 % (3386846)------------------------------ % 293.24/42.03 % (3386846)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 293.24/42.03 % (3386846)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 293.24/42.03 % (3386846)CaDiCaL version: 2.1.3 % 293.24/42.03 % (3386846)Termination reason: Instruction limit % 293.24/42.03 % (3386846)Termination phase: Saturation % 293.24/42.03 % (3386846)Time elapsed: 1.188 s % 293.24/42.03 % (3386846)Peak memory usage: 34 MB % 293.24/42.03 % (3386846)Instructions burned: 2252 (million) % 293.24/42.03 % (3386848)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=1734846447:fmbsr=1.6:i=67534_2907 on theBenchmark for (2907ds/67534Mi) % 293.24/42.03 % (3386844)Instruction limit reached! % 293.24/42.03 % (3386844)------------------------------ % 293.24/42.03 % (3386844)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 293.24/42.03 % (3386844)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 293.24/42.03 % (3386844)CaDiCaL version: 2.1.3 % 293.24/42.03 % (3386844)Termination reason: Instruction limit % 293.24/42.03 % (3386844)Termination phase: Saturation % 293.24/42.03 % (3386844)Time elapsed: 2.107 s % 293.24/42.03 % (3386844)Peak memory usage: 56 MB % 293.24/42.03 % (3386844)Instructions burned: 3774 (million) % 293.24/42.03 % (3386850)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=2630409436:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2905 on theBenchmark for (2905ds/4591Mi) % 293.24/42.03 % TRYING [1] % 293.24/42.03 % (3386850)Instruction limit reached! % 293.24/42.03 % (3386850)------------------------------ % 293.24/42.03 % (3386850)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 293.24/42.03 % (3386850)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 293.24/42.03 % (3386850)CaDiCaL version: 2.1.3 % 293.24/42.03 % (3386850)Termination reason: Instruction limit % 293.24/42.03 % (3386850)Termination phase: Saturation % 293.24/42.03 % (3386850)Time elapsed: 1.724 s % 293.24/42.03 % (3386850)Peak memory usage: 31 MB % 293.24/42.03 % (3386850)Instructions burned: 4593 (million) % 293.24/42.03 % (3386852)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=3412546128:i=29340_2888 on theBenchmark for (2888ds/29340Mi) % 293.24/42.03 % TRYING [2] % 293.24/42.03 % (3386822)Instruction limit reached! % 293.24/42.03 % (3386822)------------------------------ % 293.24/42.03 % (3386822)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 293.24/42.03 % (3386822)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 293.24/42.03 % (3386822)CaDiCaL version: 2.1.3 % 293.24/42.03 % (3386822)Termination reason: Instruction limit % 293.24/42.03 % (3386822)Termination phase: Finite model building preprocessing % 293.24/42.03 % (3386822)Time elapsed: 11.509 s % 293.24/42.03 % (3386822)Peak memory usage: 216 MB % 293.24/42.03 % (3386822)Instructions burned: 22061 (million) % 293.24/42.03 % (3386854)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=2531880170:i=5211_2874 on theBenchmark for (2874ds/5211Mi) % 293.24/42.03 % TRYING [1] % 293.24/42.03 % TRYING [3] % 293.24/42.03 % TRYING [2] % 293.24/42.03 % (3386854)Instruction limit reached! % 293.24/42.03 % (3386854)------------------------------ % 293.24/42.03 % (3386854)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 293.24/42.03 % (3386854)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 293.24/42.03 % (3386854)CaDiCaL version: 2.1.3 % 293.24/42.03 % (3386854)Termination reason: Instruction limit % 293.24/42.03 % (3386854)Termination phase: Saturation % 293.24/42.03 % (3386854)Time elapsed: 2.109 s % 293.24/42.03 % (3386854)Peak memory usage: 45 MB % 293.24/42.03 % (3386854)Instructions burned: 5212 (million) % 293.24/42.03 % (3386857)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=3750506588:i=5497:nm=2_2852 on theBenchmark for (2852ds/5497Mi) % 293.24/42.03 % TRYING [3] % 293.24/42.03 % (3386857)Instruction limit reached! % 293.24/42.03 % (3386857)------------------------------ % 293.24/42.03 % (3386857)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 293.24/42.03 % (3386857)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 293.24/42.03 % (3386857)CaDiCaL version: 2.1.3 % 293.24/42.03 % (3386857)Termination reason: Instruction limit % 293.24/42.03 % (3386857)Termination phase: Finite model building preprocessing % 301.40/43.09 % (3386857)Time elapsed: 2.819 s % 301.40/43.09 % (3386857)Peak memory usage: 65 MB % 301.40/43.09 % (3386857)Instructions burned: 5497 (million) % 301.40/43.09 % (3386859)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=3703394152:fmbsr=2:i=46332_2824 on theBenchmark for (2824ds/46332Mi) % 301.40/43.09 % (3386840)Instruction limit reached! % 301.40/43.09 % (3386840)------------------------------ % 301.40/43.09 % (3386840)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 301.40/43.09 % (3386840)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 301.40/43.09 % (3386840)CaDiCaL version: 2.1.3 % 301.40/43.09 % (3386840)Termination reason: Instruction limit % 301.40/43.09 % (3386840)Termination phase: Finite model building constraint generation % 301.40/43.09 % (3386840)Time elapsed: 14.037 s % 301.40/43.09 % (3386840)Peak memory usage: 2592 MB % 301.40/43.09 % (3386840)Instructions burned: 54287 (million) % 301.40/43.09 % (3386861)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=4151523937:i=14071_2814 on theBenchmark for (2814ds/14071Mi) % 301.40/43.09 % (3386848)Cannot represent all propositional literals internally % 301.40/43.09 % (3386848)Refutation not found, incomplete strategy % 301.40/43.09 % (3386848)------------------------------ % 301.40/43.09 % (3386848)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 301.40/43.09 % (3386848)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 301.40/43.09 % (3386848)CaDiCaL version: 2.1.3 % 301.40/43.09 % (3386848)Termination reason: Refutation not found, incomplete strategy % 301.40/43.09 % (3386848)Time elapsed: 12.369 s % 301.40/43.09 % (3386848)Peak memory usage: 192 MB % 301.40/43.09 % (3386848)Instructions burned: 23956 (million) % 301.40/43.09 % (3386848)------------------------------ % 301.40/43.09 % (3386848)------------------------------ % 301.40/43.09 % (3386863)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3308445066:i=22565:add=on:rawr=on_2782 on theBenchmark for (2782ds/22565Mi) % 301.40/43.09 % (3386861)Instruction limit reached! % 301.40/43.09 % (3386861)------------------------------ % 301.40/43.09 % (3386861)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 301.40/43.09 % (3386861)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 301.40/43.09 % (3386861)CaDiCaL version: 2.1.3 % 301.40/43.09 % (3386861)Termination reason: Instruction limit % 301.40/43.09 % (3386861)Termination phase: Finite model building preprocessing % 301.40/43.09 % (3386861)Time elapsed: 3.913 s % 301.40/43.09 % (3386861)Peak memory usage: 109 MB % 301.40/43.09 % (3386861)Instructions burned: 14072 (million) % 301.40/43.09 % (3386865)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=1210863678:i=8173:av=off_2774 on theBenchmark for (2774ds/8173Mi) % 301.40/43.09 % (3386852)Instruction limit reached! % 301.40/43.09 % (3386852)------------------------------ % 301.40/43.09 % (3386852)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 301.40/43.09 % (3386852)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 301.40/43.09 % (3386852)CaDiCaL version: 2.1.3 % 301.40/43.09 % (3386852)Termination reason: Instruction limit % 301.40/43.09 % (3386852)Termination phase: Saturation % 301.40/43.09 % (3386852)Time elapsed: 13.516 s % 301.40/43.09 % (3386852)Peak memory usage: 416 MB % 301.40/43.09 % (3386852)Instructions burned: 29342 (million) % 301.40/43.09 % (3386867)dis+10_16:1_sil=16000:random_seed=1983840784:i=9155:fsr=off_2752 on theBenchmark for (2752ds/9155Mi) % 301.40/43.09 % (3386865)Instruction limit reached! % 301.40/43.09 % (3386865)------------------------------ % 301.40/43.09 % (3386865)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 301.40/43.09 % (3386865)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 301.40/43.09 % (3386865)CaDiCaL version: 2.1.3 % 301.40/43.09 % (3386865)Termination reason: Instruction limit % 301.40/43.09 % (3386865)Termination phase: Saturation % 301.40/43.09 % (3386865)Time elapsed: 2.817 s % 301.40/43.09 % (3386865)Peak memory usage: 97 MB % 301.40/43.09 % (3386865)Instructions burned: 8175 (million) % 301.40/43.09 % (3386869)ott-3_8_sil=64000:random_seed=3637413588:i=20139:bs=on_2746 on theBenchmark for (2746ds/20139Mi) % 301.40/43.09 % (3386867)Instruction limit reached! % 301.40/43.09 % (3386867)------------------------------ % 301.40/43.09 % (3386867)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 301.40/43.09 % (3386867)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 301.40/43.09 % (3386867)CaDiCaL version: 2.1. % 301.40/43.09 Terminated % 301.40/43.09 % Vampire exiting % 301.40/43.09 Terminated %------------------------------------------------------------------------------