%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : NUM694+4 : TPTP v9.3.1. Released v7.3.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:25:24 PM UTC 2026 % Result : Timeout 292.89s 41.90s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.04 % Problem : NUM694+4 : TPTP v9.3.1. Released v7.3.0. % 0.00/0.07 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.16/0.42 % Computer : n013.cluster.edu % 0.16/0.42 % Model : x86_64 x86_64 % 0.16/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.16/0.42 % Memory : 8046.5625MB % 0.16/0.42 % OS : Linux 6.8.0-71-generic % 0.16/0.42 % CPULimit : 300 % 0.16/0.42 % WCLimit : 300 % 0.16/0.42 % DateTime : Sun Sep 27 21:07:06 UTC 2026 % 0.16/0.42 % CPUTime : % 0.16/0.42 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.20/0.48 Running first-order model finding % 0.20/0.48 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 % 28.63/4.64 % (549911)Will run a generic schedule for satisfiability detection. % 28.63/4.64 % (549917)% WARNING: option uhcvi not known. % 28.63/4.64 % (549922)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=4255314003:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 28.63/4.64 % (549917)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2969148092:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 28.63/4.64 % (549916)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1948669165_2999 on theBenchmark for (2999ds/0Mi) % 28.63/4.64 % (549918)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2592615274:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 28.63/4.64 % (549919)dis+10_1_sil=32000:sp=arity:random_seed=2270231066:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 28.63/4.64 % (549920)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2617966988:i=116_2999 on theBenchmark for (2999ds/116Mi) % 28.63/4.64 % (549921)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2465591768:i=131_2999 on theBenchmark for (2999ds/131Mi) % 28.63/4.64 % (549922)Instruction limit reached! % 28.63/4.64 % (549922)------------------------------ % 28.63/4.64 % (549922)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 28.63/4.64 % (549922)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.63/4.64 % (549922)CaDiCaL version: 2.1.3 % 28.63/4.64 % (549922)Termination reason: Instruction limit % 28.63/4.64 % (549922)Termination phase: Saturation % 28.63/4.64 % (549922)Time elapsed: 0.084 s % 28.63/4.64 % (549922)Peak memory usage: 15 MB % 28.63/4.64 % (549922)Instructions burned: 160 (million) % 28.63/4.64 % (549930)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3437779646:i=714:nm=2_2998 on theBenchmark for (2998ds/714Mi) % 28.63/4.64 % (549919)Instruction limit reached! % 28.63/4.64 % (549919)------------------------------ % 28.63/4.64 % (549919)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 28.63/4.64 % (549919)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.63/4.64 % (549919)CaDiCaL version: 2.1.3 % 28.63/4.64 % (549919)Termination reason: Instruction limit % 28.63/4.64 % (549919)Termination phase: Saturation % 28.63/4.64 % (549919)Time elapsed: 0.096 s % 28.63/4.64 % (549919)Peak memory usage: 13 MB % 28.63/4.64 % (549919)Instructions burned: 103 (million) % 28.63/4.64 % (549920)Instruction limit reached! % 28.63/4.64 % (549920)------------------------------ % 28.63/4.64 % (549920)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 28.63/4.64 % (549920)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.63/4.64 % (549920)CaDiCaL version: 2.1.3 % 28.63/4.64 % (549920)Termination reason: Instruction limit % 28.63/4.64 % (549920)Termination phase: Saturation % 28.63/4.64 % (549920)Time elapsed: 0.100 s % 28.63/4.64 % (549920)Peak memory usage: 13 MB % 28.63/4.64 % (549920)Instructions burned: 116 (million) % 28.63/4.64 % (549921)Instruction limit reached! % 28.63/4.64 % (549921)------------------------------ % 28.63/4.64 % (549921)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 28.63/4.64 % (549921)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.63/4.64 % (549921)CaDiCaL version: 2.1.3 % 28.63/4.64 % (549921)Termination reason: Instruction limit % 28.63/4.64 % (549921)Termination phase: Saturation % 28.63/4.64 % (549921)Time elapsed: 0.120 s % 28.63/4.64 % (549921)Peak memory usage: 14 MB % 28.63/4.64 % (549921)Instructions burned: 131 (million) % 28.63/4.64 % (549933)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=482745931:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi) % 28.63/4.64 % (549932)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=214143302:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi) % 28.63/4.64 % (549934)ott-21_1_sil=16000:fs=off:random_seed=281413507:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 28.63/4.64 % (549932)Instruction limit reached! % 28.63/4.64 % (549932)------------------------------ % 28.63/4.64 % (549932)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 28.63/4.64 % (549932)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.63/4.64 % (549932)CaDiCaL version: 2.1.3 % 28.63/4.64 % (549932)Termination reason: Instruction limit % 80.17/11.82 % (549932)Termination phase: Saturation % 80.17/11.82 % (549932)Time elapsed: 0.115 s % 80.17/11.82 % (549932)Peak memory usage: 14 MB % 80.17/11.82 % (549932)Instructions burned: 131 (million) % 80.17/11.82 % (549938)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=840111938:i=477:bd=all_2996 on theBenchmark for (2996ds/477Mi) % 80.17/11.82 % (549934)Instruction limit reached! % 80.17/11.82 % (549934)------------------------------ % 80.17/11.82 % (549934)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 80.17/11.82 % (549934)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 80.17/11.82 % (549934)CaDiCaL version: 2.1.3 % 80.17/11.82 % (549934)Termination reason: Instruction limit % 80.17/11.82 % (549934)Termination phase: Saturation % 80.17/11.82 % (549934)Time elapsed: 0.164 s % 80.17/11.82 % (549934)Peak memory usage: 13 MB % 80.17/11.82 % (549934)Instructions burned: 180 (million) % 80.17/11.82 % TRYING [1] % 80.17/11.82 % (549940)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=993821533:fmbsr=1.3:i=865:ins=25_2996 on theBenchmark for (2996ds/865Mi) % 80.17/11.82 % TRYING [2] % 80.17/11.82 % (549930)Instruction limit reached! % 80.17/11.82 % (549930)------------------------------ % 80.17/11.82 % (549930)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 80.17/11.82 % (549930)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 80.17/11.82 % (549930)CaDiCaL version: 2.1.3 % 80.17/11.82 % (549930)Termination reason: Instruction limit % 80.17/11.82 % (549930)Termination phase: Finite model building constraint generation % 80.17/11.82 % (549930)Time elapsed: 0.322 s % 80.17/11.82 % (549930)Peak memory usage: 35 MB % 80.17/11.82 % (549930)Instructions burned: 716 (million) % 80.17/11.82 % (549942)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=4276568689:i=1179_2995 on theBenchmark for (2995ds/1179Mi) % 80.17/11.82 % TRYING [1] % 80.17/11.82 % TRYING [2] % 80.17/11.82 % (549933)Instruction limit reached! % 80.17/11.82 % (549933)------------------------------ % 80.17/11.82 % (549933)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 80.17/11.82 % (549933)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 80.17/11.82 % (549933)CaDiCaL version: 2.1.3 % 80.17/11.82 % (549933)Termination reason: Instruction limit % 80.17/11.82 % (549933)Termination phase: Saturation % 80.17/11.82 % (549933)Time elapsed: 0.514 s % 80.17/11.82 % (549933)Peak memory usage: 17 MB % 80.17/11.82 % (549933)Instructions burned: 684 (million) % 80.17/11.82 % (549946)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3879531994:i=889:ins=1_2993 on theBenchmark for (2993ds/889Mi) % 80.17/11.82 % (549938)Instruction limit reached! % 80.17/11.82 % (549938)------------------------------ % 80.17/11.82 % (549938)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 80.17/11.82 % (549938)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 80.17/11.82 % (549938)CaDiCaL version: 2.1.3 % 80.17/11.82 % (549938)Termination reason: Instruction limit % 80.17/11.82 % (549938)Termination phase: Saturation % 80.17/11.82 % (549938)Time elapsed: 0.471 s % 80.17/11.82 % (549938)Peak memory usage: 16 MB % 80.17/11.82 % (549938)Instructions burned: 477 (million) % 80.17/11.82 % TRYING [3] % 80.17/11.82 % (549948)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=3401573148: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) % 80.17/11.82 % TRYING [1] % 80.17/11.82 % TRYING [2] % 80.17/11.82 % (549942)Instruction limit reached! % 80.17/11.82 % (549942)------------------------------ % 80.17/11.82 % (549942)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 80.17/11.82 % (549942)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 80.17/11.82 % (549942)CaDiCaL version: 2.1.3 % 80.17/11.82 % (549942)Termination reason: Instruction limit % 80.17/11.82 % (549942)Termination phase: Saturation % 80.17/11.82 % (549942)Time elapsed: 0.620 s % 80.17/11.82 % (549942)Peak memory usage: 25 MB % 80.17/11.82 % (549942)Instructions burned: 1179 (million) % 80.17/11.82 % (549950)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1606090254:i=879:kws=inv_precedence:fsr=off_2988 on theBenchmark for (2988ds/879Mi) % 80.17/11.82 % (549940)Instruction limit reached! % 80.17/11.82 % (549940)------------------------------ % 80.17/11.82 % (549940)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 80.17/11.82 % (549940)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 80.17/11.82 % (549940)CaDiCaL version: 2.1.3 % 135.47/19.66 % (549940)Termination reason: Instruction limit % 135.47/19.66 % (549940)Termination phase: Finite model building constraint generation % 135.47/19.66 % (549940)Time elapsed: 0.742 s % 135.47/19.66 % (549940)Peak memory usage: 35 MB % 135.47/19.66 % (549940)Instructions burned: 866 (million) % 135.47/19.66 % (549954)fmb+10_1_sil=64000:random_seed=1784526181:i=22061:nm=2:gsp=on_2988 on theBenchmark for (2988ds/22061Mi) % 135.47/19.66 % TRYING [1] % 135.47/19.66 % TRYING [2] % 135.47/19.66 % (549946)Instruction limit reached! % 135.47/19.66 % (549946)------------------------------ % 135.47/19.66 % (549946)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 135.47/19.66 % (549946)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 135.47/19.66 % (549946)CaDiCaL version: 2.1.3 % 135.47/19.66 % (549946)Termination reason: Instruction limit % 135.47/19.66 % (549946)Termination phase: Finite model building constraint generation % 135.47/19.66 % (549946)Time elapsed: 0.814 s % 135.47/19.66 % (549946)Peak memory usage: 65 MB % 135.47/19.66 % (549946)Instructions burned: 890 (million) % 135.47/19.66 % (549948)Instruction limit reached! % 135.47/19.66 % (549948)------------------------------ % 135.47/19.66 % (549948)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 135.47/19.66 % (549948)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 135.47/19.66 % (549948)CaDiCaL version: 2.1.3 % 135.47/19.66 % (549948)Termination reason: Instruction limit % 135.47/19.66 % (549948)Termination phase: Saturation % 135.47/19.66 % (549948)Time elapsed: 0.704 s % 135.47/19.66 % (549948)Peak memory usage: 20 MB % 135.47/19.66 % (549948)Instructions burned: 692 (million) % 135.47/19.66 % (549956)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2065142325:i=9515:nm=5_2984 on theBenchmark for (2984ds/9515Mi) % 135.47/19.66 % (549957)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=884651486:fmbsr=1.7:i=920_2984 on theBenchmark for (2984ds/920Mi) % 135.47/19.66 % (549950)Instruction limit reached! % 135.47/19.66 % (549950)------------------------------ % 135.47/19.66 % (549950)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 135.47/19.66 % (549950)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 135.47/19.66 % (549950)CaDiCaL version: 2.1.3 % 135.47/19.66 % (549950)Termination reason: Instruction limit % 135.47/19.66 % (549950)Termination phase: Saturation % 135.47/19.66 % (549950)Time elapsed: 0.574 s % 135.47/19.66 % (549950)Peak memory usage: 20 MB % 135.47/19.66 % (549950)Instructions burned: 879 (million) % 135.47/19.66 % (549960)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=98743977:i=5131_2982 on theBenchmark for (2982ds/5131Mi) % 135.47/19.66 % TRYING [4] % 135.47/19.66 % TRYING [3] % 135.47/19.66 % TRYING [20] % 135.47/19.66 % TRYING [8] % 135.47/19.66 % (549957)Instruction limit reached! % 135.47/19.66 % (549957)------------------------------ % 135.47/19.66 % (549957)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 135.47/19.66 % (549957)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 135.47/19.66 % (549957)CaDiCaL version: 2.1.3 % 135.47/19.66 % (549957)Termination reason: Instruction limit % 135.47/19.66 % (549957)Termination phase: Finite model building constraint generation % 135.47/19.66 % (549957)Time elapsed: 0.759 s % 135.47/19.66 % (549957)Peak memory usage: 45 MB % 135.47/19.66 % (549957)Instructions burned: 920 (million) % 135.47/19.66 % (549964)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2313709996:i=1472:ins=7:fdi=8:gsp=on_2976 on theBenchmark for (2976ds/1472Mi) % 135.47/19.66 % (549964)Instruction limit reached! % 135.47/19.66 % (549964)------------------------------ % 135.47/19.66 % (549964)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 135.47/19.66 % (549964)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 135.47/19.66 % (549964)CaDiCaL version: 2.1.3 % 135.47/19.66 % (549964)Termination reason: Instruction limit % 135.47/19.66 % (549964)Termination phase: Saturation % 135.47/19.66 % (549964)Time elapsed: 1.248 s % 135.47/19.66 % (549964)Peak memory usage: 28 MB % 135.47/19.66 % (549964)Instructions burned: 1472 (million) % 135.47/19.66 % TRYING [4] % 135.47/19.66 % (549966)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3480609332:i=6324_2963 on theBenchmark for (2963ds/6324Mi) % 135.47/19.66 % (549966)Cannot represent all propositional literals internally % 135.47/19.66 % (549966)Refutation not found, incomplete strategy % 135.47/19.66 % (549966)------------------------------ % 135.47/19.66 % (549966)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 135.47/19.66 % (549966)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 292.89/41.90 % (549966)CaDiCaL version: 2.1.3 % 292.89/41.90 % (549966)Termination reason: Refutation not found, incomplete strategy % 292.89/41.90 % (549966)Time elapsed: 0.485 s % 292.89/41.90 % (549966)Peak memory usage: 23 MB % 292.89/41.90 % (549966)Instructions burned: 606 (million) % 292.89/41.90 % (549966)------------------------------ % 292.89/41.90 % (549966)------------------------------ % 292.89/41.90 % (549968)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1362296787:fmbsr=2.30978:i=2174_2958 on theBenchmark for (2958ds/2174Mi) % 292.89/41.90 % TRYING [16] % 292.89/41.90 % TRYING [5] % 292.89/41.90 % (549968)Instruction limit reached! % 292.89/41.90 % (549968)------------------------------ % 292.89/41.90 % (549968)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 292.89/41.90 % (549968)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 292.89/41.90 % (549968)CaDiCaL version: 2.1.3 % 292.89/41.90 % (549968)Termination reason: Instruction limit % 292.89/41.90 % (549968)Termination phase: Finite model building constraint generation % 292.89/41.90 % (549968)Time elapsed: 1.447 s % 292.89/41.90 % (549968)Peak memory usage: 115 MB % 292.89/41.90 % (549968)Instructions burned: 2175 (million) % 292.89/41.90 % (549976)ott-2_1_sil=16000:newcnf=on:random_seed=2320464417:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2943 on theBenchmark for (2943ds/869Mi) % 292.89/41.90 % (549976)Instruction limit reached! % 292.89/41.90 % (549976)------------------------------ % 292.89/41.90 % (549976)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 292.89/41.90 % (549976)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 292.89/41.90 % (549976)CaDiCaL version: 2.1.3 % 292.89/41.90 % (549976)Termination reason: Instruction limit % 292.89/41.90 % (549976)Termination phase: Saturation % 292.89/41.90 % (549976)Time elapsed: 0.698 s % 292.89/41.90 % (549976)Peak memory usage: 16 MB % 292.89/41.90 % (549976)Instructions burned: 870 (million) % 292.89/41.90 % (549978)ott+10_1_sil=32000:tgt=ground:random_seed=1766897918:i=5114:av=off_2936 on theBenchmark for (2936ds/5114Mi) % 292.89/41.90 % (549960)Instruction limit reached! % 292.89/41.90 % (549960)------------------------------ % 292.89/41.90 % (549960)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 292.89/41.90 % (549960)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 292.89/41.90 % (549960)CaDiCaL version: 2.1.3 % 292.89/41.90 % (549960)Termination reason: Instruction limit % 292.89/41.90 % (549960)Termination phase: Saturation % 292.89/41.90 % (549960)Time elapsed: 4.700 s % 292.89/41.90 % (549960)Peak memory usage: 54 MB % 292.89/41.90 % (549960)Instructions burned: 5131 (million) % 292.89/41.90 % (549980)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2338171962:i=54282_2935 on theBenchmark for (2935ds/54282Mi) % 292.89/41.90 % TRYING [1] % 292.89/41.90 % TRYING [2] % 292.89/41.90 % TRYING [3] % 292.89/41.90 % TRYING [4] % 292.89/41.90 % TRYING [5] % 292.89/41.90 % (549956)Instruction limit reached! % 292.89/41.90 % (549956)------------------------------ % 292.89/41.90 % (549956)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 292.89/41.90 % (549956)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 292.89/41.90 % (549956)CaDiCaL version: 2.1.3 % 292.89/41.90 % (549956)Termination reason: Instruction limit % 292.89/41.90 % (549956)Termination phase: Finite model building constraint generation % 292.89/41.90 % (549956)Time elapsed: 7.317 s % 292.89/41.90 % (549956)Peak memory usage: 642 MB % 292.89/41.90 % (549956)Instructions burned: 9516 (million) % 292.89/41.90 % (549986)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3977071253:i=3512:aac=none_2909 on theBenchmark for (2909ds/3512Mi) % 292.89/41.90 % (549954)Instruction limit reached! % 292.89/41.90 % (549954)------------------------------ % 292.89/41.90 % (549954)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 292.89/41.90 % (549954)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 292.89/41.90 % (549954)CaDiCaL version: 2.1.3 % 292.89/41.90 % (549954)Termination reason: Instruction limit % 292.89/41.90 % (549954)Termination phase: Finite model building constraint generation % 292.89/41.90 % (549954)Time elapsed: 9.006 s % 292.89/41.90 % (549954)Peak memory usage: 336 MB % 292.89/41.90 % (549954)Instructions burned: 22062 (million) % 292.89/41.90 % (549994)dis+21_1_sil=32000:sas=cadical:random_seed=2014208809:i=3773:amm=off_2897 on theBenchmark for (2897ds/3773Mi) % 292.89/41.90 % (549978)Instruction limit reached! % 292.89/41.90 % (549978)------------------------------ % 292.89/41.90 % (549978)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 292.89/41.90 % (549978)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.62/42.95 % (549978)CaDiCaL version: 2.1.3 % 300.62/42.95 % (549978)Termination reason: Instruction limit % 300.62/42.95 % (549978)Termination phase: Saturation % 300.62/42.95 % (549978)Time elapsed: 4.921 s % 300.62/42.95 % (549978)Peak memory usage: 62 MB % 300.62/42.95 % (549978)Instructions burned: 5115 (million) % 300.62/42.95 % (549996)ott+11_1_sil=16000:gs=on:random_seed=2657410460:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2886 on theBenchmark for (2886ds/2251Mi) % 300.62/42.95 % TRYING [5] % 300.62/42.95 % (549994)Instruction limit reached! % 300.62/42.95 % (549994)------------------------------ % 300.62/42.95 % (549994)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.62/42.95 % (549994)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.62/42.95 % (549994)CaDiCaL version: 2.1.3 % 300.62/42.95 % (549994)Termination reason: Instruction limit % 300.62/42.95 % (549994)Termination phase: Saturation % 300.62/42.95 % (549994)Time elapsed: 1.961 s % 300.62/42.95 % (549994)Peak memory usage: 46 MB % 300.62/42.95 % (549994)Instructions burned: 3773 (million) % 300.62/42.95 % (549998)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=3931071624:fmbsr=1.6:i=67534_2877 on theBenchmark for (2877ds/67534Mi) % 300.62/42.95 % (549986)Instruction limit reached! % 300.62/42.95 % (549986)------------------------------ % 300.62/42.95 % (549986)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.62/42.95 % (549986)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.62/42.95 % (549986)CaDiCaL version: 2.1.3 % 300.62/42.95 % (549986)Termination reason: Instruction limit % 300.62/42.95 % (549986)Termination phase: Saturation % 300.62/42.95 % (549986)Time elapsed: 3.189 s % 300.62/42.95 % (549986)Peak memory usage: 49 MB % 300.62/42.95 % (549986)Instructions burned: 3513 (million) % 300.62/42.95 % (550000)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=1202980012:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2877 on theBenchmark for (2877ds/4591Mi) % 300.62/42.95 % TRYING [7] % 300.62/42.95 % (549996)Instruction limit reached! % 300.62/42.95 % (549996)------------------------------ % 300.62/42.95 % (549996)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.62/42.95 % (549996)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.62/42.95 % (549996)CaDiCaL version: 2.1.3 % 300.62/42.95 % (549996)Termination reason: Instruction limit % 300.62/42.95 % (549996)Termination phase: Saturation % 300.62/42.95 % (549996)Time elapsed: 1.705 s % 300.62/42.95 % (549996)Peak memory usage: 29 MB % 300.62/42.95 % (549996)Instructions burned: 2252 (million) % 300.62/42.95 % (550121)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=200964899:i=29340_2869 on theBenchmark for (2869ds/29340Mi) % 300.62/42.95 % TRYING [6] % 300.62/42.95 % (550000)Instruction limit reached! % 300.62/42.95 % (550000)------------------------------ % 300.62/42.95 % (550000)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.62/42.95 % (550000)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.62/42.95 % (550000)CaDiCaL version: 2.1.3 % 300.62/42.95 % (550000)Termination reason: Instruction limit % 300.62/42.95 % (550000)Termination phase: Saturation % 300.62/42.95 % (550000)Time elapsed: 2.455 s % 300.62/42.95 % (550000)Peak memory usage: 52 MB % 300.62/42.95 % (550000)Instructions burned: 4591 (million) % 300.62/42.95 % (550165)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=3793805702:i=5211_2852 on theBenchmark for (2852ds/5211Mi) % 300.62/42.95 % (550165)Instruction limit reached! % 300.62/42.95 % (550165)------------------------------ % 300.62/42.95 % (550165)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.62/42.95 % (550165)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.62/42.95 % (550165)CaDiCaL version: 2.1.3 % 300.62/42.95 % (550165)Termination reason: Instruction limit % 300.62/42.95 % (550165)Termination phase: Saturation % 300.62/42.95 % (550165)Time elapsed: 2.316 s % 300.62/42.95 % (550165)Peak memory usage: 41 MB % 300.62/42.95 % (550165)Instructions burned: 5213 (million) % 300.62/42.95 % (550167)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=2628144410:i=5497:nm=2_2829 on theBenchmark for (2829ds/5497Mi) % 300.62/42.95 % TRYING [6] % 300.62/42.95 % TRYING [17] % 300.62/42.95 % (550167)Instruction limit reached! % 300.62/42.95 % (550167)------------------------------ % 300.62/42.95 % (550167)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.62/42.95 % (550167)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.62/42.95 % (550167)CaDiCaL ver % 300.62/42.95 Terminated % 300.62/42.95 % Vampire exiting % 300.62/42.95 Terminated %------------------------------------------------------------------------------