%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : CSR080+5 : 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 : n016.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 300.40s 42.94s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : CSR080+5 : TPTP v9.3.1. Bugfixed v7.3.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.09/0.20 % Computer : n016.cluster.edu % 0.09/0.20 % Model : x86_64 x86_64 % 0.09/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.20 % Memory : 8046.5625MB % 0.09/0.20 % OS : Linux 6.8.0-71-generic % 0.09/0.20 % CPULimit : 300 % 0.09/0.20 % WCLimit : 300 % 0.09/0.20 % DateTime : Mon Sep 28 22:35:34 UTC 2026 % 0.09/0.20 % CPUTime : % 0.09/0.20 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.09/0.23 Running first-order model finding % 0.09/0.23 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 % 17.41/3.13 % (4114814)Will run a generic schedule for satisfiability detection. % 17.41/3.13 % (4114822)dis+10_1_sil=32000:sp=arity:random_seed=496319855:i=103:fgj=on_2995 on theBenchmark for (2995ds/103Mi) % 17.41/3.13 % (4114820)% WARNING: option uhcvi not known. % 17.41/3.13 % (4114819)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1912587044_2995 on theBenchmark for (2995ds/0Mi) % 17.41/3.13 % (4114820)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1384442105:i=135531:add=off:rawr=on_2995 on theBenchmark for (2995ds/135531Mi) % 17.41/3.13 % (4114821)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3157745402:i=88024:add=on:rawr=on_2995 on theBenchmark for (2995ds/88024Mi) % 17.41/3.13 % (4114823)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1369081293:i=116_2995 on theBenchmark for (2995ds/116Mi) % 17.41/3.13 % (4114824)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=452238973:i=131_2995 on theBenchmark for (2995ds/131Mi) % 17.41/3.13 % (4114825)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2214950802:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2995 on theBenchmark for (2995ds/159Mi) % 17.41/3.13 % (4114822)Instruction limit reached! % 17.41/3.13 % (4114822)------------------------------ % 17.41/3.13 % (4114822)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 17.41/3.13 % (4114822)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.41/3.13 % (4114822)CaDiCaL version: 2.1.3 % 17.41/3.13 % (4114822)Termination reason: Instruction limit % 17.41/3.13 % (4114822)Termination phase: Preprocessing 3 % 17.41/3.13 % (4114822)Time elapsed: 0.050 s % 17.41/3.13 % (4114822)Peak memory usage: 36 MB % 17.41/3.13 % (4114822)Instructions burned: 103 (million) % 17.41/3.13 % (4114833)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3870055095:i=714:nm=2_2995 on theBenchmark for (2995ds/714Mi) % 17.41/3.13 % (4114823)Instruction limit reached! % 17.41/3.13 % (4114823)------------------------------ % 17.41/3.13 % (4114823)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 17.41/3.13 % (4114823)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.41/3.13 % (4114823)CaDiCaL version: 2.1.3 % 17.41/3.13 % (4114823)Termination reason: Instruction limit % 17.41/3.13 % (4114823)Termination phase: NewCNF % 17.41/3.13 % (4114823)Time elapsed: 0.089 s % 17.41/3.13 % (4114823)Peak memory usage: 38 MB % 17.41/3.13 % (4114823)Instructions burned: 116 (million) % 17.41/3.13 % (4114824)Instruction limit reached! % 17.41/3.13 % (4114824)------------------------------ % 17.41/3.13 % (4114824)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 17.41/3.13 % (4114824)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.41/3.13 % (4114824)CaDiCaL version: 2.1.3 % 17.41/3.13 % (4114824)Termination reason: Instruction limit % 17.41/3.13 % (4114824)Termination phase: Preprocessing 3 % 17.41/3.13 % (4114824)Time elapsed: 0.089 s % 17.41/3.13 % (4114824)Peak memory usage: 36 MB % 17.41/3.13 % (4114824)Instructions burned: 132 (million) % 17.41/3.13 % (4114825)Instruction limit reached! % 17.41/3.13 % (4114825)------------------------------ % 17.41/3.13 % (4114825)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 17.41/3.13 % (4114825)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.41/3.13 % (4114825)CaDiCaL version: 2.1.3 % 17.41/3.13 % (4114825)Termination reason: Instruction limit % 17.41/3.13 % (4114825)Termination phase: Preprocessing 3 % 17.41/3.13 % (4114825)Time elapsed: 0.102 s % 17.41/3.13 % (4114825)Peak memory usage: 38 MB % 17.41/3.13 % (4114825)Instructions burned: 159 (million) % 17.41/3.13 % (4114835)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2284507702:i=131:bd=preordered:fsd=on_2994 on theBenchmark for (2994ds/131Mi) % 17.41/3.13 % (4114836)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=1627987109:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2994 on theBenchmark for (2994ds/684Mi) % 17.41/3.13 % (4114837)ott-21_1_sil=16000:fs=off:random_seed=1240368660:i=180:av=off:fsr=off_2994 on theBenchmark for (2994ds/180Mi) % 17.41/3.13 % (4114835)Instruction limit reached! % 17.41/3.13 % (4114835)------------------------------ % 17.41/3.13 % (4114835)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 17.41/3.13 % (4114835)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.93/4.00 % (4114835)CaDiCaL version: 2.1.3 % 22.93/4.00 % (4114835)Termination reason: Instruction limit % 22.93/4.00 % (4114835)Termination phase: Preprocessing 3 % 22.93/4.00 % (4114835)Time elapsed: 0.088 s % 22.93/4.00 % (4114835)Peak memory usage: 36 MB % 22.93/4.00 % (4114835)Instructions burned: 133 (million) % 22.93/4.00 % (4114841)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=566025497:i=477:bd=all_2993 on theBenchmark for (2993ds/477Mi) % 22.93/4.00 % (4114837)Instruction limit reached! % 22.93/4.00 % (4114837)------------------------------ % 22.93/4.00 % (4114837)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.93/4.00 % (4114837)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.93/4.00 % (4114837)CaDiCaL version: 2.1.3 % 22.93/4.00 % (4114837)Termination reason: Instruction limit % 22.93/4.00 % (4114837)Termination phase: Preprocessing 3 % 22.93/4.00 % (4114837)Time elapsed: 0.121 s % 22.93/4.00 % (4114837)Peak memory usage: 38 MB % 22.93/4.00 % (4114837)Instructions burned: 180 (million) % 22.93/4.00 % (4114843)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1153606140:fmbsr=1.3:i=865:ins=25_2993 on theBenchmark for (2993ds/865Mi) % 22.93/4.01 % (4114833)Instruction limit reached! % 22.93/4.01 % (4114833)------------------------------ % 22.93/4.01 % (4114833)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.93/4.01 % (4114833)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.93/4.01 % (4114833)CaDiCaL version: 2.1.3 % 22.93/4.01 % (4114833)Termination reason: Instruction limit % 22.93/4.01 % (4114833)Termination phase: Property scanning % 22.93/4.01 % (4114833)Time elapsed: 0.255 s % 22.93/4.01 % (4114833)Peak memory usage: 73 MB % 22.93/4.01 % (4114833)Instructions burned: 716 (million) % 22.93/4.01 % (4114845)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2141758649:i=1179_2992 on theBenchmark for (2992ds/1179Mi) % 22.93/4.01 % (4114836)Instruction limit reached! % 22.93/4.01 % (4114836)------------------------------ % 22.93/4.01 % (4114836)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.93/4.01 % (4114836)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.93/4.01 % (4114836)CaDiCaL version: 2.1.3 % 22.93/4.01 % (4114836)Termination reason: Instruction limit % 22.93/4.01 % (4114836)Termination phase: Saturation % 22.93/4.01 % (4114836)Time elapsed: 0.365 s % 22.93/4.01 % (4114836)Peak memory usage: 46 MB % 22.93/4.01 % (4114836)Instructions burned: 684 (million) % 22.93/4.01 % (4114841)Instruction limit reached! % 22.93/4.01 % (4114841)------------------------------ % 22.93/4.01 % (4114841)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.93/4.01 % (4114841)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.93/4.01 % (4114841)CaDiCaL version: 2.1.3 % 22.93/4.01 % (4114841)Termination reason: Instruction limit % 22.93/4.01 % (4114841)Termination phase: Saturation % 22.93/4.01 % (4114841)Time elapsed: 0.255 s % 22.93/4.01 % (4114841)Peak memory usage: 43 MB % 22.93/4.01 % (4114841)Instructions burned: 477 (million) % 22.93/4.01 % (4114847)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1838780719:i=889:ins=1_2990 on theBenchmark for (2990ds/889Mi) % 22.93/4.01 % (4114848)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=3443717684:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2990 on theBenchmark for (2990ds/692Mi) % 22.93/4.01 % (4114845)Instruction limit reached! % 22.93/4.01 % (4114845)------------------------------ % 22.93/4.01 % (4114845)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.93/4.01 % (4114845)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.93/4.01 % (4114845)CaDiCaL version: 2.1.3 % 22.93/4.01 % (4114845)Termination reason: Instruction limit % 22.93/4.01 % (4114845)Termination phase: Saturation % 22.93/4.01 % (4114845)Time elapsed: 0.349 s % 22.93/4.01 % (4114845)Peak memory usage: 54 MB % 22.93/4.01 % (4114845)Instructions burned: 1180 (million) % 22.93/4.01 % (4114851)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=357686755:i=879:kws=inv_precedence:fsr=off_2988 on theBenchmark for (2988ds/879Mi) % 22.93/4.01 % (4114843)Instruction limit reached! % 22.93/4.01 % (4114843)------------------------------ % 22.93/4.01 % (4114843)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.93/4.01 % (4114843)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 42.11/6.64 % (4114843)CaDiCaL version: 2.1.3 % 42.11/6.64 % (4114843)Termination reason: Instruction limit % 42.11/6.64 % (4114843)Termination phase: Property scanning % 42.11/6.64 % (4114843)Time elapsed: 0.450 s % 42.11/6.64 % (4114843)Peak memory usage: 71 MB % 42.11/6.64 % (4114843)Instructions burned: 866 (million) % 42.11/6.64 % (4114853)fmb+10_1_sil=64000:random_seed=1345103685:i=22061:nm=2:gsp=on_2988 on theBenchmark for (2988ds/22061Mi) % 42.11/6.64 % (4114848)Instruction limit reached! % 42.11/6.64 % (4114848)------------------------------ % 42.11/6.64 % (4114848)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 42.11/6.64 % (4114848)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 42.11/6.64 % (4114848)CaDiCaL version: 2.1.3 % 42.11/6.64 % (4114848)Termination reason: Instruction limit % 42.11/6.64 % (4114848)Termination phase: Saturation % 42.11/6.64 % (4114848)Time elapsed: 0.362 s % 42.11/6.64 % (4114848)Peak memory usage: 49 MB % 42.11/6.64 % (4114848)Instructions burned: 694 (million) % 42.11/6.64 % (4114855)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3610030692:i=9515:nm=5_2986 on theBenchmark for (2986ds/9515Mi) % 42.11/6.64 % (4114847)Instruction limit reached! % 42.11/6.64 % (4114847)------------------------------ % 42.11/6.64 % (4114847)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 42.11/6.64 % (4114847)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 42.11/6.64 % (4114847)CaDiCaL version: 2.1.3 % 42.11/6.64 % (4114847)Termination reason: Instruction limit % 42.11/6.64 % (4114847)Termination phase: Property scanning % 42.11/6.64 % (4114847)Time elapsed: 0.447 s % 42.11/6.64 % (4114847)Peak memory usage: 71 MB % 42.11/6.64 % (4114847)Instructions burned: 889 (million) % 42.11/6.64 % (4114851)Instruction limit reached! % 42.11/6.64 % (4114851)------------------------------ % 42.11/6.64 % (4114851)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 42.11/6.64 % (4114851)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 42.11/6.64 % (4114851)CaDiCaL version: 2.1.3 % 42.11/6.64 % (4114851)Termination reason: Instruction limit % 42.11/6.64 % (4114851)Termination phase: Saturation % 42.11/6.64 % (4114851)Time elapsed: 0.263 s % 42.11/6.64 % (4114851)Peak memory usage: 58 MB % 42.11/6.64 % (4114851)Instructions burned: 881 (million) % 42.11/6.64 % (4114858)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1750311867:i=5131_2985 on theBenchmark for (2985ds/5131Mi) % 42.11/6.64 % (4114857)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1390162308:fmbsr=1.7:i=920_2986 on theBenchmark for (2986ds/920Mi) % 42.11/6.64 % (4114857)Instruction limit reached! % 42.11/6.64 % (4114857)------------------------------ % 42.11/6.64 % (4114857)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 42.11/6.64 % (4114857)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 42.11/6.64 % (4114857)CaDiCaL version: 2.1.3 % 42.11/6.64 % (4114857)Termination reason: Instruction limit % 42.11/6.64 % (4114857)Termination phase: Property scanning % 42.11/6.64 % (4114857)Time elapsed: 0.480 s % 42.11/6.64 % (4114857)Peak memory usage: 71 MB % 42.11/6.64 % (4114857)Instructions burned: 920 (million) % 42.11/6.64 % (4114861)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3794337157:i=1472:ins=7:fdi=8:gsp=on_2980 on theBenchmark for (2980ds/1472Mi) % 42.11/6.64 % (4114861)Instruction limit reached! % 42.11/6.64 % (4114861)------------------------------ % 42.11/6.64 % (4114861)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 42.11/6.64 % (4114861)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 42.11/6.64 % (4114861)CaDiCaL version: 2.1.3 % 42.11/6.64 % (4114861)Termination reason: Instruction limit % 42.11/6.64 % (4114861)Termination phase: Saturation % 42.11/6.64 % (4114861)Time elapsed: 0.822 s % 42.11/6.64 % (4114861)Peak memory usage: 60 MB % 42.11/6.64 % (4114861)Instructions burned: 1472 (million) % 42.11/6.64 % (4114863)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3796370068:i=6324_2972 on theBenchmark for (2972ds/6324Mi) % 42.11/6.64 % (4114858)Instruction limit reached! % 42.11/6.64 % (4114858)------------------------------ % 42.11/6.64 % (4114858)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 42.11/6.64 % (4114858)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 42.11/6.64 % (4114858)CaDiCaL version: 2.1.3 % 42.11/6.64 % (4114858)Termination reason: Instruction limit % 42.11/6.64 % (4114858)Termination phase: Saturation % 42.11/6.64 % (4114858)Time elapsed: 1.483 s % 61.87/9.33 % (4114858)Peak memory usage: 95 MB % 61.87/9.33 % (4114858)Instructions burned: 5136 (million) % 61.87/9.33 % (4114865)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=934442685:fmbsr=2.30978:i=2174_2970 on theBenchmark for (2970ds/2174Mi) % 61.87/9.33 % Detected minimum model sizes of [447] % 61.87/9.33 % Detected maximum model sizes of [max] % 61.87/9.33 % (4114819)Cannot represent all propositional literals internally % 61.87/9.33 % (4114819)Refutation not found, incomplete strategy % 61.87/9.33 % (4114819)------------------------------ % 61.87/9.33 % (4114819)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 61.87/9.33 % (4114819)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 61.87/9.33 % (4114819)CaDiCaL version: 2.1.3 % 61.87/9.33 % (4114819)Termination reason: Refutation not found, incomplete strategy % 61.87/9.33 % (4114819)Time elapsed: 2.771 s % 61.87/9.33 % (4114819)Peak memory usage: 148 MB % 61.87/9.33 % (4114819)Instructions burned: 5800 (million) % 61.87/9.33 % (4114819)------------------------------ % 61.87/9.33 % (4114819)------------------------------ % 61.87/9.33 % (4114867)ott-2_1_sil=16000:newcnf=on:random_seed=1162400398:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2967 on theBenchmark for (2967ds/869Mi) % 61.87/9.33 % (4114865)Instruction limit reached! % 61.87/9.33 % (4114865)------------------------------ % 61.87/9.33 % (4114865)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 61.87/9.33 % (4114865)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 61.87/9.33 % (4114865)CaDiCaL version: 2.1.3 % 61.87/9.33 % (4114865)Termination reason: Instruction limit % 61.87/9.33 % (4114865)Termination phase: Finite model building preprocessing % 61.87/9.33 % (4114865)Time elapsed: 0.612 s % 61.87/9.33 % (4114865)Peak memory usage: 109 MB % 61.87/9.33 % (4114865)Instructions burned: 2175 (million) % 61.87/9.33 % Detected minimum model sizes of [447] % 61.87/9.33 % Detected maximum model sizes of [max] % 61.87/9.33 % (4114853)Cannot represent all propositional literals internally % 61.87/9.33 % (4114853)Refutation not found, incomplete strategy % 61.87/9.33 % (4114853)------------------------------ % 61.87/9.33 % (4114853)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 61.87/9.33 % (4114853)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 61.87/9.33 % (4114853)CaDiCaL version: 2.1.3 % 61.87/9.33 % (4114853)Termination reason: Refutation not found, incomplete strategy % 61.87/9.33 % (4114853)Time elapsed: 2.356 s % 61.87/9.33 % (4114853)Peak memory usage: 132 MB % 61.87/9.33 % (4114853)Instructions burned: 5024 (million) % 61.87/9.33 % (4114869)ott+10_1_sil=32000:tgt=ground:random_seed=126526189:i=5114:av=off_2964 on theBenchmark for (2964ds/5114Mi) % 61.87/9.33 % (4114853)------------------------------ % 61.87/9.33 % (4114853)------------------------------ % 61.87/9.33 % (4114871)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=790870583:i=54282_2964 on theBenchmark for (2964ds/54282Mi) % 61.87/9.33 % Detected minimum model sizes of [447] % 61.87/9.33 % Detected maximum model sizes of [max] % 61.87/9.33 % (4114855)Cannot represent all propositional literals internally % 61.87/9.33 % (4114855)Refutation not found, incomplete strategy % 61.87/9.33 % (4114855)------------------------------ % 61.87/9.33 % (4114855)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 61.87/9.33 % (4114855)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 61.87/9.33 % (4114855)CaDiCaL version: 2.1.3 % 61.87/9.33 % (4114855)Termination reason: Refutation not found, incomplete strategy % 61.87/9.33 % (4114855)Time elapsed: 2.405 s % 61.87/9.33 % (4114855)Peak memory usage: 137 MB % 61.87/9.33 % (4114855)Instructions burned: 5222 (million) % 61.87/9.33 % (4114867)Instruction limit reached! % 61.87/9.33 % (4114867)------------------------------ % 61.87/9.33 % (4114867)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 61.87/9.33 % (4114867)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 61.87/9.33 % (4114867)CaDiCaL version: 2.1.3 % 61.87/9.33 % (4114867)Termination reason: Instruction limit % 61.87/9.33 % (4114867)Termination phase: Saturation % 61.87/9.33 % (4114867)Time elapsed: 0.464 s % 61.87/9.33 % (4114867)Peak memory usage: 51 MB % 61.87/9.33 % (4114867)Instructions burned: 869 (million) % 61.87/9.33 % (4114855)------------------------------ % 61.87/9.33 % (4114855)------------------------------ % 61.87/9.33 % (4114873)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=4235038510:i=3512:aac=none_2962 on theBenchmark for (2962ds/3512Mi) % 147.04/21.38 % (4114875)dis+21_1_sil=32000:sas=cadical:random_seed=2731781624:i=3773:amm=off_2962 on theBenchmark for (2962ds/3773Mi) % 147.04/21.38 % (4114869)Instruction limit reached! % 147.04/21.38 % (4114869)------------------------------ % 147.04/21.38 % (4114869)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 147.04/21.38 % (4114869)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 147.04/21.38 % (4114869)CaDiCaL version: 2.1.3 % 147.04/21.38 % (4114869)Termination reason: Instruction limit % 147.04/21.38 % (4114869)Termination phase: Saturation % 147.04/21.38 % (4114869)Time elapsed: 1.441 s % 147.04/21.38 % (4114869)Peak memory usage: 76 MB % 147.04/21.38 % (4114869)Instructions burned: 5117 (million) % 147.04/21.38 % (4114877)ott+11_1_sil=16000:gs=on:random_seed=2907308572:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2950 on theBenchmark for (2950ds/2251Mi) % 147.04/21.38 % (4114875)Instruction limit reached! % 147.04/21.38 % (4114875)------------------------------ % 147.04/21.38 % (4114875)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 147.04/21.38 % (4114875)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 147.04/21.38 % (4114875)CaDiCaL version: 2.1.3 % 147.04/21.38 % (4114875)Termination reason: Instruction limit % 147.04/21.38 % (4114875)Termination phase: Saturation % 147.04/21.38 % (4114875)Time elapsed: 1.605 s % 147.04/21.38 % (4114875)Peak memory usage: 67 MB % 147.04/21.38 % (4114875)Instructions burned: 3774 (million) % 147.04/21.38 % (4114879)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=3616268170:fmbsr=1.6:i=67534_2945 on theBenchmark for (2945ds/67534Mi) % 147.04/21.38 % Detected minimum model sizes of [447] % 147.04/21.38 % Detected maximum model sizes of [max] % 147.04/21.38 % (4114863)Cannot represent all propositional literals internally % 147.04/21.38 % (4114863)Refutation not found, incomplete strategy % 147.04/21.38 % (4114863)------------------------------ % 147.04/21.38 % (4114863)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 147.04/21.38 % (4114863)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 147.04/21.38 % (4114863)CaDiCaL version: 2.1.3 % 147.04/21.38 % (4114863)Termination reason: Refutation not found, incomplete strategy % 147.04/21.38 % (4114863)Time elapsed: 2.714 s % 147.04/21.38 % (4114863)Peak memory usage: 147 MB % 147.04/21.38 % (4114863)Instructions burned: 5781 (million) % 147.04/21.38 % (4114863)------------------------------ % 147.04/21.38 % (4114863)------------------------------ % 147.04/21.38 % (4114881)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=50568366:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2944 on theBenchmark for (2944ds/4591Mi) % 147.04/21.38 % (4114873)Instruction limit reached! % 147.04/21.38 % (4114873)------------------------------ % 147.04/21.38 % (4114873)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 147.04/21.38 % (4114873)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 147.04/21.38 % (4114873)CaDiCaL version: 2.1.3 % 147.04/21.38 % (4114873)Termination reason: Instruction limit % 147.04/21.38 % (4114873)Termination phase: Saturation % 147.04/21.38 % (4114873)Time elapsed: 1.865 s % 147.04/21.38 % (4114873)Peak memory usage: 106 MB % 147.04/21.38 % (4114873)Instructions burned: 3514 (million) % 147.04/21.38 % (4114883)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=3456480487:i=29340_2943 on theBenchmark for (2943ds/29340Mi) % 147.04/21.38 % (4114877)Instruction limit reached! % 147.04/21.38 % (4114877)------------------------------ % 147.04/21.38 % (4114877)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 147.04/21.38 % (4114877)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 147.04/21.38 % (4114877)CaDiCaL version: 2.1.3 % 147.04/21.38 % (4114877)Termination reason: Instruction limit % 147.04/21.38 % (4114877)Termination phase: Saturation % 147.04/21.38 % (4114877)Time elapsed: 0.770 s % 147.04/21.38 % (4114877)Peak memory usage: 93 MB % 147.04/21.38 % (4114877)Instructions burned: 2253 (million) % 147.04/21.38 % (4114885)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=2879602370:i=5211_2942 on theBenchmark for (2942ds/5211Mi) % 147.04/21.38 % Detected minimum model sizes of [447] % 147.04/21.38 % Detected maximum model sizes of [max] % 147.04/21.38 % (4114871)Cannot represent all propositional literals internally % 147.04/21.38 % (4114871)Refutation not found, incomplete strategy % 147.04/21.38 % (4114871)------------------------------ % 147.04/21.38 % (4114871)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 147.04/21.38 % (4114871)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 175.42/25.35 % (4114871)CaDiCaL version: 2.1.3 % 175.42/25.35 % (4114871)Termination reason: Refutation not found, incomplete strategy % 175.42/25.35 % (4114871)Time elapsed: 2.797 s % 175.42/25.35 % (4114871)Peak memory usage: 150 MB % 175.42/25.35 % (4114871)Instructions burned: 5811 (million) % 175.42/25.35 % (4114871)------------------------------ % 175.42/25.35 % (4114871)------------------------------ % 175.42/25.35 % (4114887)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=2749732382:i=5497:nm=2_2935 on theBenchmark for (2935ds/5497Mi) % 175.42/25.35 % (4114885)Instruction limit reached! % 175.42/25.35 % (4114885)------------------------------ % 175.42/25.35 % (4114885)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 175.42/25.35 % (4114885)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 175.42/25.35 % (4114885)CaDiCaL version: 2.1.3 % 175.42/25.35 % (4114885)Termination reason: Instruction limit % 175.42/25.35 % (4114885)Termination phase: Saturation % 175.42/25.35 % (4114885)Time elapsed: 1.233 s % 175.42/25.35 % (4114885)Peak memory usage: 70 MB % 175.42/25.35 % (4114885)Instructions burned: 5211 (million) % 175.42/25.35 % (4114890)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=557897171:fmbsr=2:i=46332_2929 on theBenchmark for (2929ds/46332Mi) % 175.42/25.35 % (4114881)Instruction limit reached! % 175.42/25.35 % (4114881)------------------------------ % 175.42/25.35 % (4114881)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 175.42/25.35 % (4114881)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 175.42/25.35 % (4114881)CaDiCaL version: 2.1.3 % 175.42/25.35 % (4114881)Termination reason: Instruction limit % 175.42/25.35 % (4114881)Termination phase: Saturation % 175.42/25.35 % (4114881)Time elapsed: 2.248 s % 175.42/25.35 % (4114881)Peak memory usage: 69 MB % 175.42/25.35 % (4114881)Instructions burned: 4591 (million) % 175.42/25.35 % (4114892)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=3732707754:i=14071_2921 on theBenchmark for (2921ds/14071Mi) % 175.42/25.35 % Detected minimum model sizes of [447] % 175.42/25.35 % Detected maximum model sizes of [max] % 175.42/25.35 % (4114879)Cannot represent all propositional literals internally % 175.42/25.35 % (4114879)Refutation not found, incomplete strategy % 175.42/25.35 % (4114879)------------------------------ % 175.42/25.35 % (4114879)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 175.42/25.35 % (4114879)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 175.42/25.35 % (4114879)CaDiCaL version: 2.1.3 % 175.42/25.35 % (4114879)Termination reason: Refutation not found, incomplete strategy % 175.42/25.35 % (4114879)Time elapsed: 2.612 s % 175.42/25.35 % (4114879)Peak memory usage: 141 MB % 175.42/25.35 % (4114879)Instructions burned: 5797 (million) % 175.42/25.35 % (4114879)------------------------------ % 175.42/25.35 % (4114879)------------------------------ % 175.42/25.35 % (4114894)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3631273088:i=22565:add=on:rawr=on_2919 on theBenchmark for (2919ds/22565Mi) % 175.42/25.35 % Detected minimum model sizes of [447] % 175.42/25.35 % Detected maximum model sizes of [max] % 175.42/25.35 % (4114890)Cannot represent all propositional literals internally % 175.42/25.35 % (4114890)Refutation not found, incomplete strategy % 175.42/25.35 % (4114890)------------------------------ % 175.42/25.35 % (4114890)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 175.42/25.35 % (4114890)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 175.42/25.35 % (4114890)CaDiCaL version: 2.1.3 % 175.42/25.35 % (4114890)Termination reason: Refutation not found, incomplete strategy % 175.42/25.35 % (4114890)Time elapsed: 1.420 s % 175.42/25.35 % (4114890)Peak memory usage: 141 MB % 175.42/25.35 % (4114890)Instructions burned: 5797 (million) % 175.42/25.35 % (4114890)------------------------------ % 175.42/25.35 % (4114890)------------------------------ % 175.42/25.35 % (4114896)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=3087901796:i=8173:av=off_2915 on theBenchmark for (2915ds/8173Mi) % 175.42/25.35 % Detected minimum model sizes of [447] % 175.42/25.35 % Detected maximum model sizes of [max] % 175.42/25.35 % (4114887)Cannot represent all propositional literals internally % 175.42/25.35 % (4114887)Refutation not found, incomplete strategy % 175.42/25.35 % (4114887)------------------------------ % 175.42/25.35 % (4114887)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 175.42/25.35 % (4114887)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 175.42/25.35 % (4114887)CaDiCaL version: 2.1.3 % 202.66/29.19 % (4114887)Termination reason: Refutation not found, incomplete strategy % 202.66/29.19 % (4114887)Time elapsed: 2.622 s % 202.66/29.19 % (4114887)Peak memory usage: 141 MB % 202.66/29.19 % (4114887)Instructions burned: 5377 (million) % 202.66/29.19 % (4114887)------------------------------ % 202.66/29.19 % (4114887)------------------------------ % 202.66/29.19 % (4114898)dis+10_16:1_sil=16000:random_seed=1781665072:i=9155:fsr=off_2908 on theBenchmark for (2908ds/9155Mi) % 202.66/29.19 % Detected minimum model sizes of [447] % 202.66/29.19 % Detected maximum model sizes of [max] % 202.66/29.19 % (4114892)Cannot represent all propositional literals internally % 202.66/29.19 % (4114892)Refutation not found, incomplete strategy % 202.66/29.19 % (4114892)------------------------------ % 202.66/29.19 % (4114892)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 202.66/29.19 % (4114892)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 202.66/29.19 % (4114892)CaDiCaL version: 2.1.3 % 202.66/29.19 % (4114892)Termination reason: Refutation not found, incomplete strategy % 202.66/29.19 % (4114892)Time elapsed: 2.481 s % 202.66/29.19 % (4114892)Peak memory usage: 139 MB % 202.66/29.19 % (4114892)Instructions burned: 5347 (million) % 202.66/29.19 % (4114892)------------------------------ % 202.66/29.19 % (4114892)------------------------------ % 202.66/29.19 % (4114900)ott-3_8_sil=64000:random_seed=1568192766:i=20139:bs=on_2896 on theBenchmark for (2896ds/20139Mi) % 202.66/29.19 % (4114896)Instruction limit reached! % 202.66/29.19 % (4114896)------------------------------ % 202.66/29.19 % (4114896)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 202.66/29.19 % (4114896)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 202.66/29.19 % (4114896)CaDiCaL version: 2.1.3 % 202.66/29.19 % (4114896)Termination reason: Instruction limit % 202.66/29.19 % (4114896)Termination phase: Saturation % 202.66/29.19 % (4114896)Time elapsed: 2.545 s % 202.66/29.19 % (4114896)Peak memory usage: 93 MB % 202.66/29.19 % (4114896)Instructions burned: 8176 (million) % 202.66/29.19 % (4114902)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=111350737:fmbsr=2:i=32576_2889 on theBenchmark for (2889ds/32576Mi) % 202.66/29.19 % Detected minimum model sizes of [447] % 202.66/29.19 % Detected maximum model sizes of [max] % 202.66/29.19 % (4114902)Cannot represent all propositional literals internally % 202.66/29.19 % (4114902)Refutation not found, incomplete strategy % 202.66/29.19 % (4114902)------------------------------ % 202.66/29.19 % (4114902)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 202.66/29.19 % (4114902)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 202.66/29.19 % (4114902)CaDiCaL version: 2.1.3 % 202.66/29.19 % (4114902)Termination reason: Refutation not found, incomplete strategy % 202.66/29.19 % (4114902)Time elapsed: 1.515 s % 202.66/29.19 % (4114902)Peak memory usage: 147 MB % 202.66/29.19 % (4114902)Instructions burned: 5783 (million) % 202.66/29.19 % (4114902)------------------------------ % 202.66/29.19 % (4114902)------------------------------ % 202.66/29.19 % (4114904)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=1451423843:i=11404_2873 on theBenchmark for (2873ds/11404Mi) % 202.66/29.19 % (4114898)Instruction limit reached! % 202.66/29.19 % (4114898)------------------------------ % 202.66/29.19 % (4114898)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 202.66/29.19 % (4114898)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 202.66/29.19 % (4114898)CaDiCaL version: 2.1.3 % 202.66/29.19 % (4114898)Termination reason: Instruction limit % 202.66/29.19 % (4114898)Termination phase: Saturation % 202.66/29.19 % (4114898)Time elapsed: 4.550 s % 202.66/29.19 % (4114898)Peak memory usage: 130 MB % 202.66/29.19 % (4114898)Instructions burned: 9156 (million) % 202.66/29.19 % (4114906)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=3664015099:i=14134_2862 on theBenchmark for (2862ds/14134Mi) % 202.66/29.19 % (4114904)Instruction limit reached! % 202.66/29.19 % (4114904)------------------------------ % 202.66/29.19 % (4114904)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 202.66/29.19 % (4114904)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 202.66/29.19 % (4114904)CaDiCaL version: 2.1.3 % 202.66/29.19 % (4114904)Termination reason: Instruction limit % 202.66/29.19 % (4114904)Termination phase: Saturation % 202.66/29.19 % (4114904)Time elapsed: 4.129 s % 202.66/29.19 % (4114904)Peak memory usage: 311 MB % 202.66/29.19 % (4114904)Instructions burned: 11406 (million) % 202.66/29.19 % (4114908)dis+33_16_sil=32000:sac=on:random_seed=49344620:i=15851:nm=0_2832 on theBenchmark for (2832ds/15851Mi) % 202.66/29.19 % (4114908)Instruction limit reached! % 218.65/31.46 % (4114908)------------------------------ % 218.65/31.46 % (4114908)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 218.65/31.46 % (4114908)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 218.65/31.46 % (4114908)CaDiCaL version: 2.1.3 % 218.65/31.46 % (4114908)Termination reason: Instruction limit % 218.65/31.46 % (4114908)Termination phase: Saturation % 218.65/31.46 % (4114908)Time elapsed: 4.358 s % 218.65/31.46 % (4114908)Peak memory usage: 101 MB % 218.65/31.46 % (4114908)Instructions burned: 15854 (million) % 218.65/31.46 % (4114910)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=3092804744:avsq=on:i=17627:add=on:amm=off_2788 on theBenchmark for (2788ds/17627Mi) % 218.65/31.46 % (4114906)Instruction limit reached! % 218.65/31.46 % (4114906)------------------------------ % 218.65/31.46 % (4114906)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 218.65/31.46 % (4114906)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 218.65/31.46 % (4114906)CaDiCaL version: 2.1.3 % 218.65/31.46 % (4114906)Termination reason: Instruction limit % 218.65/31.46 % (4114906)Termination phase: Saturation % 218.65/31.46 % (4114906)Time elapsed: 8.270 s % 218.65/31.46 % (4114906)Peak memory usage: 172 MB % 218.65/31.46 % (4114906)Instructions burned: 14134 (million) % 218.65/31.46 % (4114912)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=532993166:s2a=on:i=53295_2779 on theBenchmark for (2779ds/53295Mi) % 218.65/31.46 % (4114883)Instruction limit reached! % 218.65/31.46 % (4114883)------------------------------ % 218.65/31.46 % (4114883)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 218.65/31.46 % (4114883)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 218.65/31.46 % (4114883)CaDiCaL version: 2.1.3 % 218.65/31.46 % (4114883)Termination reason: Instruction limit % 218.65/31.46 % (4114883)Termination phase: Saturation % 218.65/31.46 % (4114883)Time elapsed: 16.794 s % 218.65/31.46 % (4114883)Peak memory usage: 73 MB % 218.65/31.46 % (4114883)Instructions burned: 29340 (million) % 218.65/31.46 % (4114914)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=3872819677:i=26857:ins=20_2775 on theBenchmark for (2775ds/26857Mi) % 218.65/31.46 % (4114894)Instruction limit reached! % 218.65/31.46 % (4114894)------------------------------ % 218.65/31.46 % (4114894)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 218.65/31.46 % (4114894)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 218.65/31.46 % (4114894)CaDiCaL version: 2.1.3 % 218.65/31.46 % (4114894)Termination reason: Instruction limit % 218.65/31.46 % (4114894)Termination phase: Saturation % 218.65/31.46 % (4114894)Time elapsed: 15.416 s % 218.65/31.46 % (4114894)Peak memory usage: 909 MB % 218.65/31.46 % (4114894)Instructions burned: 22565 (million) % 218.65/31.46 % (4114916)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=1628490252:i=28120:bs=on:fsr=off_2763 on theBenchmark for (2763ds/28120Mi) % 218.65/31.46 % (4114900)Instruction limit reached! % 218.65/31.46 % (4114900)------------------------------ % 218.65/31.46 % (4114900)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 218.65/31.46 % (4114900)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 218.65/31.46 % (4114900)CaDiCaL version: 2.1.3 % 218.65/31.46 % (4114900)Termination reason: Instruction limit % 218.65/31.46 % (4114900)Termination phase: Saturation % 218.65/31.46 % (4114900)Time elapsed: 13.452 s % 218.65/31.46 % (4114900)Peak memory usage: 129 MB % 218.65/31.46 % (4114900)Instructions burned: 20140 (million) % 218.65/31.46 % (4114918)fmb+10_1_sil=256000:fmbss=7:random_seed=1061398743:fmbsr=1.6:i=182295_2761 on theBenchmark for (2761ds/182295Mi) % 218.65/31.46 % Detected minimum model sizes of [447] % 218.65/31.46 % Detected maximum model sizes of [max] % 218.65/31.46 % (4114914)Cannot represent all propositional literals internally % 218.65/31.46 % (4114914)Refutation not found, incomplete strategy % 218.65/31.46 % (4114914)------------------------------ % 218.65/31.46 % (4114914)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 218.65/31.46 % (4114914)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 218.65/31.46 % (4114914)CaDiCaL version: 2.1.3 % 218.65/31.46 % (4114914)Termination reason: Refutation not found, incomplete strategy % 218.65/31.46 % (4114914)Time elapsed: 2.548 s % 218.65/31.46 % (4114914)Peak memory usage: 139 MB % 218.65/31.46 % (4114914)Instructions burned: 5354 (million) % 218.65/31.46 % (4114914)------------------------------ % 218.65/31.46 % (4114914)------------------------------ % 218.65/31.46 % (4114920)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=3731122641:i=44625:gsp=on_2749 on theBenchmark for (2749ds/44625Mi) % 232.57/33.42 % Detected minimum model sizes of [447] % 232.57/33.42 % Detected maximum model sizes of [max] % 232.57/33.42 % (4114918)Cannot represent all propositional literals internally % 232.57/33.42 % (4114918)Refutation not found, incomplete strategy % 232.57/33.42 % (4114918)------------------------------ % 232.57/33.42 % (4114918)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 232.57/33.42 % (4114918)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 232.57/33.42 % (4114918)CaDiCaL version: 2.1.3 % 232.57/33.42 % (4114918)Termination reason: Refutation not found, incomplete strategy % 232.57/33.42 % (4114918)Time elapsed: 2.494 s % 232.57/33.42 % (4114918)Peak memory usage: 139 MB % 232.57/33.42 % (4114918)Instructions burned: 5346 (million) % 232.57/33.42 % (4114918)------------------------------ % 232.57/33.42 % (4114918)------------------------------ % 232.57/33.42 % (4114922)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=2410432328:i=160505_2735 on theBenchmark for (2735ds/160505Mi) % 232.57/33.42 % (4114910)Instruction limit reached! % 232.57/33.42 % (4114910)------------------------------ % 232.57/33.42 % (4114910)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 232.57/33.42 % (4114910)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 232.57/33.42 % (4114910)CaDiCaL version: 2.1.3 % 232.57/33.42 % (4114910)Termination reason: Instruction limit % 232.57/33.42 % (4114910)Termination phase: Saturation % 232.57/33.42 % (4114910)Time elapsed: 6.144 s % 232.57/33.42 % (4114910)Peak memory usage: 466 MB % 232.57/33.42 % (4114910)Instructions burned: 17629 (million) % 232.57/33.42 % (4114924)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=1583348908:fmbsr=1.3:i=225729_2726 on theBenchmark for (2726ds/225729Mi) % 232.57/33.42 % Detected minimum model sizes of [447] % 232.57/33.42 % Detected maximum model sizes of [max] % 232.57/33.42 % (4114920)Cannot represent all propositional literals internally % 232.57/33.42 % (4114920)Refutation not found, incomplete strategy % 232.57/33.42 % (4114920)------------------------------ % 232.57/33.42 % (4114920)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 232.57/33.42 % (4114920)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 232.57/33.42 % (4114920)CaDiCaL version: 2.1.3 % 232.57/33.42 % (4114920)Termination reason: Refutation not found, incomplete strategy % 232.57/33.42 % (4114920)Time elapsed: 2.826 s % 232.57/33.42 % (4114920)Peak memory usage: 164 MB % 232.57/33.42 % (4114920)Instructions burned: 5977 (million) % 232.57/33.42 % (4114920)------------------------------ % 232.57/33.42 % (4114920)------------------------------ % 232.57/33.42 % (4114926)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=3548307460:fmbsr=2:i=185024:ins=7_2720 on theBenchmark for (2720ds/185024Mi) % 232.57/33.42 % Detected minimum model sizes of [447] % 232.57/33.42 % Detected maximum model sizes of [max] % 232.57/33.42 % (4114924)Cannot represent all propositional literals internally % 232.57/33.42 % (4114924)Refutation not found, incomplete strategy % 232.57/33.42 % (4114924)------------------------------ % 232.57/33.42 % (4114924)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 232.57/33.42 % (4114924)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 232.57/33.42 % (4114924)CaDiCaL version: 2.1.3 % 232.57/33.42 % (4114924)Termination reason: Refutation not found, incomplete strategy % 232.57/33.42 % (4114924)Time elapsed: 1.366 s % 232.57/33.42 % (4114924)Peak memory usage: 139 MB % 232.57/33.42 % (4114924)Instructions burned: 5348 (million) % 232.57/33.42 % (4114924)------------------------------ % 232.57/33.42 % (4114924)------------------------------ % 232.57/33.42 % (4114928)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=4147381167:rtra=on_2712 on theBenchmark for (2712ds/0Mi) % 232.57/33.42 % Detected minimum model sizes of [447] % 232.57/33.42 % Detected maximum model sizes of [max] % 232.57/33.42 % (4114922)Cannot represent all propositional literals internally % 232.57/33.42 % (4114922)Refutation not found, incomplete strategy % 232.57/33.42 % (4114922)------------------------------ % 232.57/33.42 % (4114922)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 232.57/33.42 % (4114922)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 232.57/33.42 % (4114922)CaDiCaL version: 2.1.3 % 232.57/33.42 % (4114922)Termination reason: Refutation not found, incomplete strategy % 232.57/33.42 % (4114922)Time elapsed: 2.486 s % 232.57/33.42 % (4114922)Peak memory usage: 139 MB % 232.57/33.42 % (4114922)Instructions burned: 5346 (million) % 232.57/33.42 % (4114922)------------------------------ % 267.73/38.38 % (4114922)------------------------------ % 267.73/38.38 % (4114930)% WARNING: option uhcvi not known. % 267.73/38.38 % (4114930)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1051045993:i=271062:add=off:rtra=on:rawr=on_2710 on theBenchmark for (2710ds/271062Mi) % 267.73/38.38 % Detected minimum model sizes of [447] % 267.73/38.38 % Detected maximum model sizes of [max] % 267.73/38.38 % (4114926)Cannot represent all propositional literals internally % 267.73/38.38 % (4114926)Refutation not found, incomplete strategy % 267.73/38.38 % (4114926)------------------------------ % 267.73/38.38 % (4114926)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 267.73/38.38 % (4114926)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 267.73/38.38 % (4114926)CaDiCaL version: 2.1.3 % 267.73/38.38 % (4114926)Termination reason: Refutation not found, incomplete strategy % 267.73/38.38 % (4114926)Time elapsed: 2.487 s % 267.73/38.38 % (4114926)Peak memory usage: 139 MB % 267.73/38.38 % (4114926)Instructions burned: 5355 (million) % 267.73/38.38 % (4114926)------------------------------ % 267.73/38.38 % (4114926)------------------------------ % 267.73/38.38 % (4114932)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2892987885:i=176048:add=on:rtra=on:rawr=on_2694 on theBenchmark for (2694ds/176048Mi) % 267.73/38.38 % Detected minimum model sizes of [447] % 267.73/38.38 % Detected maximum model sizes of [max] % 267.73/38.38 % (4114928)Cannot represent all propositional literals internally % 267.73/38.38 % (4114928)Refutation not found, incomplete strategy % 267.73/38.38 % (4114928)------------------------------ % 267.73/38.38 % (4114928)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 267.73/38.38 % (4114928)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 267.73/38.38 % (4114928)CaDiCaL version: 2.1.3 % 267.73/38.38 % (4114928)Termination reason: Refutation not found, incomplete strategy % 267.73/38.38 % (4114928)Time elapsed: 1.978 s % 267.73/38.38 % (4114928)Peak memory usage: 163 MB % 267.73/38.38 % (4114928)Instructions burned: 6070 (million) % 267.73/38.38 % (4114928)------------------------------ % 267.73/38.38 % (4114928)------------------------------ % 267.73/38.38 % (4114934)dis+10_1_sil=32000:si=on:sp=arity:random_seed=3841471912:i=206:fgj=on:rtra=on_2692 on theBenchmark for (2692ds/206Mi) % 267.73/38.38 % (4114934)Instruction limit reached! % 267.73/38.38 % (4114934)------------------------------ % 267.73/38.38 % (4114934)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 267.73/38.38 % (4114934)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 267.73/38.38 % (4114934)CaDiCaL version: 2.1.3 % 267.73/38.38 % (4114934)Termination reason: Instruction limit % 267.73/38.38 % (4114934)Termination phase: Preprocessing 3 % 267.73/38.38 % (4114934)Time elapsed: 0.112 s % 267.73/38.38 % (4114934)Peak memory usage: 43 MB % 267.73/38.38 % (4114934)Instructions burned: 207 (million) % 267.73/38.38 % (4114936)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=3481621634:i=232:rtra=on_2690 on theBenchmark for (2690ds/232Mi) % 267.73/38.38 % (4114936)Instruction limit reached! % 267.73/38.38 % (4114936)------------------------------ % 267.73/38.38 % (4114936)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 267.73/38.38 % (4114936)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 267.73/38.38 % (4114936)CaDiCaL version: 2.1.3 % 267.73/38.38 % (4114936)Termination reason: Instruction limit % 267.73/38.38 % (4114936)Termination phase: NewCNF % 267.73/38.38 % (4114936)Time elapsed: 0.121 s % 267.73/38.38 % (4114936)Peak memory usage: 45 MB % 267.73/38.38 % (4114936)Instructions burned: 232 (million) % 267.73/38.38 % (4114938)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=2772045958:i=262:rtra=on_2689 on theBenchmark for (2689ds/262Mi) % 267.73/38.38 % (4114938)Instruction limit reached! % 267.73/38.38 % (4114938)------------------------------ % 267.73/38.38 % (4114938)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 267.73/38.38 % (4114938)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 267.73/38.38 % (4114938)CaDiCaL version: 2.1.3 % 267.73/38.38 % (4114938)Termination reason: Instruction limit % 267.73/38.38 % (4114938)Termination phase: Property scanning % 267.73/38.38 % (4114938)Time elapsed: 0.146 s % 267.73/38.38 % (4114938)Peak memory usage: 47 MB % 267.73/38.38 % (4114938)Instructions burned: 264 (million) % 267.73/38.38 % (4114940)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=1170912746:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2687 on theTerminated %------------------------------------------------------------------------------