%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : NUM050-1 : TPTP v9.3.1. Bugfixed v2.1.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % Computer : n013.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 12:17:53 PM UTC 2026 % Result : Timeout 300.24s 42.83s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : NUM050-1 : TPTP v9.3.1. Bugfixed v2.1.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.09/0.36 % Computer : n013.cluster.edu % 0.09/0.36 % Model : x86_64 x86_64 % 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.36 % Memory : 8046.5625MB % 0.09/0.36 % OS : Linux 6.8.0-71-generic % 0.09/0.36 % CPULimit : 300 % 0.09/0.36 % WCLimit : 300 % 0.09/0.36 % DateTime : Sun Sep 27 18:44:25 UTC 2026 % 0.09/0.36 % CPUTime : % 0.09/0.37 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.09/0.40 Running first-order model finding % 0.09/0.40 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 % 15.34/2.66 % (483538)Will run a generic schedule for satisfiability detection. % 15.34/2.66 % (483547)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1844595362:i=116_2999 on theBenchmark for (2999ds/116Mi) % 15.34/2.66 % (483544)% WARNING: option uhcvi not known. % 15.34/2.66 % (483543)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1866184000_2999 on theBenchmark for (2999ds/0Mi) % 15.34/2.66 % (483545)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1440100224:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 15.34/2.66 % (483546)dis+10_1_sil=32000:sp=arity:random_seed=1272654855:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 15.34/2.66 % (483548)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1010577817:i=131_2999 on theBenchmark for (2999ds/131Mi) % 15.34/2.66 % (483549)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2301096746:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 15.34/2.66 % (483544)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=27646760:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 15.34/2.66 % (483547)Instruction limit reached! % 15.34/2.66 % (483547)------------------------------ % 15.34/2.66 % (483547)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 15.34/2.66 % (483547)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.34/2.66 % (483547)CaDiCaL version: 2.1.3 % 15.34/2.66 % (483547)Termination reason: Instruction limit % 15.34/2.66 % (483547)Termination phase: Saturation % 15.34/2.66 % (483547)Time elapsed: 0.039 s % 15.34/2.66 % (483547)Peak memory usage: 13 MB % 15.34/2.66 % (483547)Instructions burned: 118 (million) % 15.34/2.66 % (483557)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3745557127:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 15.34/2.66 % (483546)Instruction limit reached! % 15.34/2.66 % (483546)------------------------------ % 15.34/2.66 % (483546)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 15.34/2.66 % (483546)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.34/2.66 % (483546)CaDiCaL version: 2.1.3 % 15.34/2.66 % (483546)Termination reason: Instruction limit % 15.34/2.66 % (483546)Termination phase: Saturation % 15.34/2.66 % (483546)Time elapsed: 0.072 s % 15.34/2.66 % (483546)Peak memory usage: 13 MB % 15.34/2.66 % (483546)Instructions burned: 103 (million) % 15.34/2.66 % (483548)Instruction limit reached! % 15.34/2.66 % (483548)------------------------------ % 15.34/2.66 % (483548)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 15.34/2.66 % (483548)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.34/2.66 % (483548)CaDiCaL version: 2.1.3 % 15.34/2.66 % (483548)Termination reason: Instruction limit % 15.34/2.66 % (483548)Termination phase: Saturation % 15.34/2.66 % (483548)Time elapsed: 0.085 s % 15.34/2.66 % (483548)Peak memory usage: 13 MB % 15.34/2.66 % (483548)Instructions burned: 131 (million) % 15.34/2.66 % (483559)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=242191343:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi) % 15.34/2.66 % (483560)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=3421952970:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi) % 15.34/2.66 % (483549)Instruction limit reached! % 15.34/2.66 % (483549)------------------------------ % 15.34/2.66 % (483549)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 15.34/2.66 % (483549)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.34/2.66 % (483549)CaDiCaL version: 2.1.3 % 15.34/2.66 % (483549)Termination reason: Instruction limit % 15.34/2.66 % (483549)Termination phase: Saturation % 15.34/2.66 % (483549)Time elapsed: 0.112 s % 15.34/2.66 % (483549)Peak memory usage: 14 MB % 15.34/2.66 % (483549)Instructions burned: 159 (million) % 15.34/2.66 % (483563)ott-21_1_sil=16000:fs=off:random_seed=1106554204:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 15.34/2.66 % TRYING [1] % 15.34/2.66 % TRYING [2] % 15.34/2.66 % TRYING [3] % 15.34/2.66 % (483559)Instruction limit reached! % 15.34/2.66 % (483559)------------------------------ % 15.34/2.66 % (483559)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 15.34/2.66 % (483559)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.34/2.66 % (483559)CaDiCaL version: 2.1.3 % 45.30/6.93 % (483559)Termination reason: Instruction limit % 45.30/6.93 % (483559)Termination phase: Saturation % 45.30/6.93 % (483559)Time elapsed: 0.093 s % 45.30/6.93 % (483559)Peak memory usage: 13 MB % 45.30/6.93 % (483559)Instructions burned: 134 (million) % 45.30/6.93 % (483565)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2683162093:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi) % 45.30/6.93 % TRYING [1] % 45.30/6.93 % TRYING [2] % 45.30/6.93 % (483557)Instruction limit reached! % 45.30/6.93 % (483557)------------------------------ % 45.30/6.93 % (483557)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 45.30/6.93 % (483557)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 45.30/6.93 % (483557)CaDiCaL version: 2.1.3 % 45.30/6.93 % (483557)Termination reason: Instruction limit % 45.30/6.93 % (483557)Termination phase: Finite model building constraint generation % 45.30/6.93 % (483557)Time elapsed: 0.176 s % 45.30/6.93 % (483557)Peak memory usage: 31 MB % 45.30/6.93 % (483557)Instructions burned: 714 (million) % 45.30/6.93 % (483563)Instruction limit reached! % 45.30/6.93 % (483563)------------------------------ % 45.30/6.93 % (483563)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 45.30/6.93 % (483563)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 45.30/6.93 % (483563)CaDiCaL version: 2.1.3 % 45.30/6.93 % (483563)Termination reason: Instruction limit % 45.30/6.93 % (483563)Termination phase: Saturation % 45.30/6.93 % (483563)Time elapsed: 0.100 s % 45.30/6.93 % (483563)Peak memory usage: 13 MB % 45.30/6.93 % (483563)Instructions burned: 180 (million) % 45.30/6.93 % (483567)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=982419172:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi) % 45.30/6.93 % TRYING [3] % 45.30/6.93 % (483569)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2148161946:i=1179_2997 on theBenchmark for (2997ds/1179Mi) % 45.30/6.93 % TRYING [1] % 45.30/6.93 % TRYING [2] % 45.30/6.93 % TRYING [4] % 45.30/6.93 % TRYING [3] % 45.30/6.93 % (483567)Instruction limit reached! % 45.30/6.93 % (483567)------------------------------ % 45.30/6.93 % (483567)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 45.30/6.93 % (483567)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 45.30/6.93 % (483567)CaDiCaL version: 2.1.3 % 45.30/6.93 % (483567)Termination reason: Instruction limit % 45.30/6.93 % (483567)Termination phase: Finite model building constraint generation % 45.30/6.93 % (483567)Time elapsed: 0.217 s % 45.30/6.93 % (483567)Peak memory usage: 26 MB % 45.30/6.93 % (483567)Instructions burned: 868 (million) % 45.30/6.93 % (483571)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3018761718:i=889:ins=1_2995 on theBenchmark for (2995ds/889Mi) % 45.30/6.93 % (483560)Instruction limit reached! % 45.30/6.93 % (483560)------------------------------ % 45.30/6.93 % (483560)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 45.30/6.93 % (483560)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 45.30/6.93 % (483560)CaDiCaL version: 2.1.3 % 45.30/6.93 % (483560)Termination reason: Instruction limit % 45.30/6.93 % (483560)Termination phase: Saturation % 45.30/6.93 % (483560)Time elapsed: 0.420 s % 45.30/6.93 % (483560)Peak memory usage: 17 MB % 45.30/6.93 % (483560)Instructions burned: 684 (million) % 45.30/6.93 % (483573)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=270174371:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2994 on theBenchmark for (2994ds/692Mi) % 45.30/6.93 % (483565)Instruction limit reached! % 45.30/6.93 % (483565)------------------------------ % 45.30/6.93 % (483565)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 45.30/6.93 % (483565)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 45.30/6.93 % (483565)CaDiCaL version: 2.1.3 % 45.30/6.93 % (483565)Termination reason: Instruction limit % 45.30/6.93 % (483565)Termination phase: Saturation % 45.30/6.93 % (483565)Time elapsed: 0.340 s % 45.30/6.93 % (483565)Peak memory usage: 14 MB % 45.30/6.93 % (483565)Instructions burned: 478 (million) % 45.30/6.93 % (483575)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2717937916:i=879:kws=inv_precedence:fsr=off_2994 on theBenchmark for (2994ds/879Mi) % 45.30/6.93 % (483571)Instruction limit reached! % 45.30/6.93 % (483571)------------------------------ % 45.30/6.93 % (483571)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 45.30/6.93 % (483571)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 101.35/14.76 % (483571)CaDiCaL version: 2.1.3 % 101.35/14.76 % (483571)Termination reason: Instruction limit % 101.35/14.76 % (483571)Termination phase: Finite model building constraint generation % 101.35/14.76 % (483571)Time elapsed: 0.248 s % 101.35/14.76 % (483571)Peak memory usage: 75 MB % 101.35/14.76 % (483571)Instructions burned: 894 (million) % 101.35/14.76 % (483577)fmb+10_1_sil=64000:random_seed=4114993505:i=22061:nm=2:gsp=on_2992 on theBenchmark for (2992ds/22061Mi) % 101.35/14.76 % TRYING [1] % 101.35/14.76 % TRYING [2] % 101.35/14.76 % TRYING [3] % 101.35/14.76 % (483573)Instruction limit reached! % 101.35/14.76 % (483573)------------------------------ % 101.35/14.76 % (483573)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 101.35/14.76 % (483573)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 101.35/14.76 % (483573)CaDiCaL version: 2.1.3 % 101.35/14.76 % (483573)Termination reason: Instruction limit % 101.35/14.76 % (483573)Termination phase: Saturation % 101.35/14.76 % (483573)Time elapsed: 0.436 s % 101.35/14.76 % (483573)Peak memory usage: 20 MB % 101.35/14.76 % (483573)Instructions burned: 693 (million) % 101.35/14.76 % (483569)Instruction limit reached! % 101.35/14.76 % (483569)------------------------------ % 101.35/14.76 % (483569)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 101.35/14.76 % (483569)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 101.35/14.76 % (483569)CaDiCaL version: 2.1.3 % 101.35/14.76 % (483569)Termination reason: Instruction limit % 101.35/14.76 % (483569)Termination phase: Saturation % 101.35/14.76 % (483569)Time elapsed: 0.732 s % 101.35/14.76 % (483569)Peak memory usage: 22 MB % 101.35/14.76 % (483569)Instructions burned: 1180 (million) % 101.35/14.76 % (483579)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2328795684:i=9515:nm=5_2989 on theBenchmark for (2989ds/9515Mi) % 101.35/14.76 % (483580)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1529189302:fmbsr=1.7:i=920_2989 on theBenchmark for (2989ds/920Mi) % 101.35/14.76 % (483575)Instruction limit reached! % 101.35/14.76 % (483575)------------------------------ % 101.35/14.76 % (483575)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 101.35/14.76 % (483575)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 101.35/14.76 % (483575)CaDiCaL version: 2.1.3 % 101.35/14.76 % (483575)Termination reason: Instruction limit % 101.35/14.76 % (483575)Termination phase: Saturation % 101.35/14.76 % (483575)Time elapsed: 0.493 s % 101.35/14.76 % (483575)Peak memory usage: 18 MB % 101.35/14.76 % (483575)Instructions burned: 880 (million) % 101.35/14.76 % (483583)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=3238992285:i=5131_2988 on theBenchmark for (2988ds/5131Mi) % 101.35/14.76 % TRYING [20] % 101.35/14.76 % TRYING [8] % 101.35/14.76 % TRYING [5] % 101.35/14.76 % TRYING [4] % 101.35/14.76 % (483580)Instruction limit reached! % 101.35/14.76 % (483580)------------------------------ % 101.35/14.76 % (483580)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 101.35/14.76 % (483580)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 101.35/14.76 % (483580)CaDiCaL version: 2.1.3 % 101.35/14.76 % (483580)Termination reason: Instruction limit % 101.35/14.76 % (483580)Termination phase: Finite model building constraint generation % 101.35/14.76 % (483580)Time elapsed: 0.384 s % 101.35/14.76 % (483580)Peak memory usage: 46 MB % 101.35/14.76 % (483580)Instructions burned: 923 (million) % 101.35/14.76 % (483585)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2302216465:i=1472:ins=7:fdi=8:gsp=on_2985 on theBenchmark for (2985ds/1472Mi) % 101.35/14.76 % (483585)Instruction limit reached! % 101.35/14.76 % (483585)------------------------------ % 101.35/14.76 % (483585)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 101.35/14.76 % (483585)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 101.35/14.76 % (483585)CaDiCaL version: 2.1.3 % 101.35/14.76 % (483585)Termination reason: Instruction limit % 101.35/14.76 % (483585)Termination phase: Saturation % 101.35/14.76 % (483585)Time elapsed: 0.572 s % 101.35/14.76 % (483585)Peak memory usage: 20 MB % 101.35/14.76 % (483585)Instructions burned: 1472 (million) % 101.35/14.76 % (483587)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=1549716648:i=6324_2979 on theBenchmark for (2979ds/6324Mi) % 101.35/14.76 % (483587)Cannot represent all propositional literals internally % 101.35/14.76 % (483587)Refutation not found, incomplete strategy % 101.35/14.76 % (483587)------------------------------ % 101.35/14.76 % (483587)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 101.35/14.76 % (483587)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 213.41/30.52 % (483587)CaDiCaL version: 2.1.3 % 213.41/30.52 % (483587)Termination reason: Refutation not found, incomplete strategy % 213.41/30.52 % (483587)Time elapsed: 0.212 s % 213.41/30.52 % (483587)Peak memory usage: 13 MB % 213.41/30.52 % (483587)Instructions burned: 406 (million) % 213.41/30.52 % (483587)------------------------------ % 213.41/30.52 % (483587)------------------------------ % 213.41/30.52 % (483589)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=3282470988:fmbsr=2.30978:i=2174_2977 on theBenchmark for (2977ds/2174Mi) % 213.41/30.52 % (483589)Cannot represent all propositional literals internally % 213.41/30.52 % (483589)Refutation not found, incomplete strategy % 213.41/30.52 % (483589)------------------------------ % 213.41/30.52 % (483589)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 213.41/30.52 % (483589)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 213.41/30.52 % (483589)CaDiCaL version: 2.1.3 % 213.41/30.52 % (483589)Termination reason: Refutation not found, incomplete strategy % 213.41/30.52 % (483589)Time elapsed: 1.116 s % 213.41/30.52 % (483589)Peak memory usage: 18 MB % 213.41/30.52 % (483589)Instructions burned: 2060 (million) % 213.41/30.52 % (483589)------------------------------ % 213.41/30.52 % (483589)------------------------------ % 213.41/30.52 % (483591)ott-2_1_sil=16000:newcnf=on:random_seed=2885916684:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2966 on theBenchmark for (2966ds/869Mi) % 213.41/30.52 % TRYING [5] % 213.41/30.52 % (483591)Instruction limit reached! % 213.41/30.52 % (483591)------------------------------ % 213.41/30.52 % (483591)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 213.41/30.52 % (483591)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 213.41/30.52 % (483591)CaDiCaL version: 2.1.3 % 213.41/30.52 % (483591)Termination reason: Instruction limit % 213.41/30.52 % (483591)Termination phase: Saturation % 213.41/30.52 % (483591)Time elapsed: 0.533 s % 213.41/30.52 % (483591)Peak memory usage: 19 MB % 213.41/30.52 % (483591)Instructions burned: 871 (million) % 213.41/30.52 % (483593)ott+10_1_sil=32000:tgt=ground:random_seed=945612836:i=5114:av=off_2960 on theBenchmark for (2960ds/5114Mi) % 213.41/30.52 % (483583)Instruction limit reached! % 213.41/30.52 % (483583)------------------------------ % 213.41/30.52 % (483583)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 213.41/30.52 % (483583)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 213.41/30.52 % (483583)CaDiCaL version: 2.1.3 % 213.41/30.52 % (483583)Termination reason: Instruction limit % 213.41/30.52 % (483583)Termination phase: Saturation % 213.41/30.52 % (483583)Time elapsed: 3.027 s % 213.41/30.52 % (483583)Peak memory usage: 35 MB % 213.41/30.52 % (483583)Instructions burned: 5131 (million) % 213.41/30.52 % (483595)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2008816511:i=54282_2958 on theBenchmark for (2958ds/54282Mi) % 213.41/30.52 % TRYING [1] % 213.41/30.52 % TRYING [2] % 213.41/30.52 % (483579)Instruction limit reached! % 213.41/30.52 % (483579)------------------------------ % 213.41/30.52 % (483579)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 213.41/30.52 % (483579)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 213.41/30.52 % (483579)CaDiCaL version: 2.1.3 % 213.41/30.52 % (483579)Termination reason: Instruction limit % 213.41/30.52 % (483579)Termination phase: Finite model building constraint generation % 213.41/30.52 % (483579)Time elapsed: 3.350 s % 213.41/30.52 % (483579)Peak memory usage: 538 MB % 213.41/30.52 % (483579)Instructions burned: 9516 (million) % 213.41/30.52 % TRYING [3] % 213.41/30.52 % (483597)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=2491544032:i=3512:aac=none_2955 on theBenchmark for (2955ds/3512Mi) % 213.41/30.52 % TRYING [4] % 213.41/30.52 % TRYING [6] % 213.41/30.52 % TRYING [5] % 213.41/30.52 % (483577)Instruction limit reached! % 213.41/30.52 % (483577)------------------------------ % 213.41/30.52 % (483577)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 213.41/30.52 % (483577)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 213.41/30.52 % (483577)CaDiCaL version: 2.1.3 % 213.41/30.52 % (483577)Termination reason: Instruction limit % 213.41/30.52 % (483577)Termination phase: Finite model building SAT solving % 213.41/30.52 % (483577)Time elapsed: 4.991 s % 213.41/30.52 % (483577)Peak memory usage: 436 MB % 213.41/30.52 % (483577)Instructions burned: 22063 (million) % 213.41/30.52 % (483599)dis+21_1_sil=32000:sas=cadical:random_seed=3499701068:i=3773:amm=off_2942 on theBenchmark for (2942ds/3773Mi) % 213.41/30.52 % (483597)Instruction limit reached! % 213.41/30.52 % (483597)------------------------------ % 213.41/30.52 % (483597)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.24/42.83 % (483597)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.24/42.83 % (483597)CaDiCaL version: 2.1.3 % 300.24/42.83 % (483597)Termination reason: Instruction limit % 300.24/42.83 % (483597)Termination phase: Saturation % 300.24/42.83 % (483597)Time elapsed: 2.041 s % 300.24/42.83 % (483597)Peak memory usage: 36 MB % 300.24/42.83 % (483597)Instructions burned: 3513 (million) % 300.24/42.83 % (483601)ott+11_1_sil=16000:gs=on:random_seed=18509424:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2934 on theBenchmark for (2934ds/2251Mi) % 300.24/42.83 % (483599)Instruction limit reached! % 300.24/42.83 % (483599)------------------------------ % 300.24/42.83 % (483599)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.24/42.83 % (483599)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.24/42.83 % (483599)CaDiCaL version: 2.1.3 % 300.24/42.83 % (483599)Termination reason: Instruction limit % 300.24/42.83 % (483599)Termination phase: Saturation % 300.24/42.83 % (483599)Time elapsed: 1.142 s % 300.24/42.83 % (483599)Peak memory usage: 30 MB % 300.24/42.83 % (483599)Instructions burned: 3776 (million) % 300.24/42.83 % (483603)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=2900665434:fmbsr=1.6:i=67534_2930 on theBenchmark for (2930ds/67534Mi) % 300.24/42.83 % (483593)Instruction limit reached! % 300.24/42.83 % (483593)------------------------------ % 300.24/42.83 % (483593)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.24/42.83 % (483593)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.24/42.83 % (483593)CaDiCaL version: 2.1.3 % 300.24/42.83 % (483593)Termination reason: Instruction limit % 300.24/42.83 % (483593)Termination phase: Saturation % 300.24/42.83 % (483593)Time elapsed: 3.278 s % 300.24/42.83 % (483593)Peak memory usage: 49 MB % 300.24/42.83 % (483593)Instructions burned: 5114 (million) % 300.24/42.83 % (483605)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=3901421414:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2927 on theBenchmark for (2927ds/4591Mi) % 300.24/42.83 % TRYING [7] % 300.24/42.83 % (483601)Instruction limit reached! % 300.24/42.83 % (483601)------------------------------ % 300.24/42.83 % (483601)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.24/42.83 % (483601)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.24/42.83 % (483601)CaDiCaL version: 2.1.3 % 300.24/42.83 % (483601)Termination reason: Instruction limit % 300.24/42.83 % (483601)Termination phase: Saturation % 300.24/42.83 % (483601)Time elapsed: 1.073 s % 300.24/42.83 % (483601)Peak memory usage: 22 MB % 300.24/42.83 % (483601)Instructions burned: 2252 (million) % 300.24/42.83 % (483607)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=1941676721:i=29340_2923 on theBenchmark for (2923ds/29340Mi) % 300.24/42.83 % TRYING [6] % 300.24/42.83 % (483605)Instruction limit reached! % 300.24/42.83 % (483605)------------------------------ % 300.24/42.83 % (483605)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.24/42.83 % (483605)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.24/42.83 % (483605)CaDiCaL version: 2.1.3 % 300.24/42.83 % (483605)Termination reason: Instruction limit % 300.24/42.83 % (483605)Termination phase: Saturation % 300.24/42.83 % (483605)Time elapsed: 2.529 s % 300.24/42.83 % (483605)Peak memory usage: 52 MB % 300.24/42.83 % (483605)Instructions burned: 4592 (million) % 300.24/42.83 % (483609)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=3300241970:i=5211_2901 on theBenchmark for (2901ds/5211Mi) % 300.24/42.83 % (483609)Instruction limit reached! % 300.24/42.83 % (483609)------------------------------ % 300.24/42.83 % (483609)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.24/42.83 % (483609)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.24/42.83 % (483609)CaDiCaL version: 2.1.3 % 300.24/42.83 % (483609)Termination reason: Instruction limit % 300.24/42.83 % (483609)Termination phase: Saturation % 300.24/42.83 % (483609)Time elapsed: 2.563 s % 300.24/42.83 % (483609)Peak memory usage: 44 MB % 300.24/42.83 % (483609)Instructions burned: 5217 (million) % 300.24/42.83 % (483611)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=2879902527:i=5497:nm=2_2876 on theBenchmark for (2876ds/5497Mi) % 300.24/42.83 % TRYING [17] % 300.24/42.83 % (483611)Instruction limit reached! % 300.24/42.83 % (483611)------------------------------ % 300.24/42.83 % (483611)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.24/42.83 % (4836 % 300.24/42.83 Terminated % 300.24/42.83 % Vampire exiting %------------------------------------------------------------------------------