%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWV912-1 : TPTP v9.3.1. Released v4.1.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % Computer : n006.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 29 01:26:39 PM UTC 2026 % Result : Timeout 300.06s 42.63s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWV912-1 : TPTP v9.3.1. Released v4.1.0. % 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.08/0.17 % Computer : n006.cluster.edu % 0.08/0.17 % Model : x86_64 x86_64 % 0.08/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.08/0.17 % Memory : 8046.5625MB % 0.08/0.17 % OS : Linux 6.8.0-71-generic % 0.08/0.17 % CPULimit : 300 % 0.08/0.17 % WCLimit : 300 % 0.08/0.17 % DateTime : Mon Sep 28 12:52:55 UTC 2026 % 0.08/0.17 % CPUTime : % 0.08/0.17 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.08/0.20 Running first-order model finding % 0.08/0.20 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 % 7.81/1.43 % (3938496)Will run a generic schedule for satisfiability detection. % 7.81/1.43 % (3938504)dis+10_1_sil=32000:sp=arity:random_seed=1634342212:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 7.81/1.43 % (3938502)% WARNING: option uhcvi not known. % 7.81/1.43 % (3938501)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=583590432_2999 on theBenchmark for (2999ds/0Mi) % 7.81/1.43 % (3938502)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2606463755:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 7.81/1.43 % (3938505)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3821677989:i=116_2999 on theBenchmark for (2999ds/116Mi) % 7.81/1.43 % (3938503)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2694875735:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 7.81/1.43 % (3938506)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3996617414:i=131_2999 on theBenchmark for (2999ds/131Mi) % 7.81/1.43 % (3938507)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=4026238783:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 7.81/1.43 % (3938504)Instruction limit reached! % 7.81/1.43 % (3938504)------------------------------ % 7.81/1.43 % (3938504)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.81/1.43 % (3938504)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.81/1.43 % (3938504)CaDiCaL version: 2.1.3 % 7.81/1.43 % (3938504)Termination reason: Instruction limit % 7.81/1.43 % (3938504)Termination phase: Saturation % 7.81/1.43 % (3938504)Time elapsed: 0.036 s % 7.81/1.43 % (3938504)Peak memory usage: 12 MB % 7.81/1.43 % (3938504)Instructions burned: 104 (million) % 7.81/1.43 % (3938515)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1777418402:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 7.81/1.43 % (3938505)Instruction limit reached! % 7.81/1.43 % (3938505)------------------------------ % 7.81/1.43 % (3938505)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.81/1.43 % (3938505)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.81/1.43 % (3938505)CaDiCaL version: 2.1.3 % 7.81/1.43 % (3938505)Termination reason: Instruction limit % 7.81/1.43 % (3938505)Termination phase: Saturation % 7.81/1.43 % (3938505)Time elapsed: 0.070 s % 7.81/1.43 % (3938505)Peak memory usage: 13 MB % 7.81/1.43 % (3938505)Instructions burned: 116 (million) % 7.81/1.43 % (3938506)Instruction limit reached! % 7.81/1.43 % (3938506)------------------------------ % 7.81/1.43 % (3938506)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.81/1.43 % (3938506)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.81/1.43 % (3938506)CaDiCaL version: 2.1.3 % 7.81/1.43 % (3938506)Termination reason: Instruction limit % 7.81/1.43 % (3938506)Termination phase: Saturation % 7.81/1.43 % (3938506)Time elapsed: 0.081 s % 7.81/1.43 % (3938506)Peak memory usage: 13 MB % 7.81/1.43 % (3938506)Instructions burned: 131 (million) % 7.81/1.43 % (3938517)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2083779637:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi) % 7.81/1.43 % (3938507)Instruction limit reached! % 7.81/1.43 % (3938507)------------------------------ % 7.81/1.43 % (3938507)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.81/1.43 % (3938507)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.81/1.43 % (3938507)CaDiCaL version: 2.1.3 % 7.81/1.43 % (3938507)Termination reason: Instruction limit % 7.81/1.43 % (3938507)Termination phase: Saturation % 7.81/1.43 % (3938507)Time elapsed: 0.094 s % 7.81/1.43 % (3938507)Peak memory usage: 13 MB % 7.81/1.43 % (3938507)Instructions burned: 159 (million) % 7.81/1.43 % (3938518)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=3302538549:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi) % 7.81/1.43 % (3938520)ott-21_1_sil=16000:fs=off:random_seed=2441364691:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 7.81/1.43 % TRYING [1] % 7.81/1.43 % TRYING [2] % 7.81/1.43 % (3938517)Instruction limit reached! % 7.81/1.43 % (3938517)------------------------------ % 7.81/1.43 % (3938517)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.81/1.43 % (3938517)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.56/5.81 % (3938517)CaDiCaL version: 2.1.3 % 39.56/5.81 % (3938517)Termination reason: Instruction limit % 39.56/5.81 % (3938517)Termination phase: Saturation % 39.56/5.81 % (3938517)Time elapsed: 0.082 s % 39.56/5.81 % (3938517)Peak memory usage: 13 MB % 39.56/5.81 % (3938517)Instructions burned: 132 (million) % 39.56/5.81 % (3938523)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=515575941:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi) % 39.56/5.81 % (3938515)Instruction limit reached! % 39.56/5.81 % (3938515)------------------------------ % 39.56/5.81 % (3938515)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 39.56/5.81 % (3938515)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.56/5.81 % (3938515)CaDiCaL version: 2.1.3 % 39.56/5.81 % (3938515)Termination reason: Instruction limit % 39.56/5.81 % (3938515)Termination phase: Finite model building constraint generation % 39.56/5.81 % (3938515)Time elapsed: 0.163 s % 39.56/5.81 % (3938515)Peak memory usage: 23 MB % 39.56/5.81 % (3938515)Instructions burned: 715 (million) % 39.56/5.81 % TRYING [1] % 39.56/5.81 % TRYING [2] % 39.56/5.81 % (3938525)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1756078291:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi) % 39.56/5.81 % (3938520)Instruction limit reached! % 39.56/5.81 % (3938520)------------------------------ % 39.56/5.81 % (3938520)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 39.56/5.81 % (3938520)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.56/5.81 % (3938520)CaDiCaL version: 2.1.3 % 39.56/5.81 % (3938520)Termination reason: Instruction limit % 39.56/5.81 % (3938520)Termination phase: Saturation % 39.56/5.81 % (3938520)Time elapsed: 0.099 s % 39.56/5.81 % (3938520)Peak memory usage: 13 MB % 39.56/5.81 % (3938520)Instructions burned: 180 (million) % 39.56/5.81 % (3938527)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3514920646:i=1179_2997 on theBenchmark for (2997ds/1179Mi) % 39.56/5.81 % TRYING [1] % 39.56/5.81 % TRYING [2] % 39.56/5.81 % TRYING [3] % 39.56/5.81 % (3938525)Instruction limit reached! % 39.56/5.81 % (3938525)------------------------------ % 39.56/5.81 % (3938525)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 39.56/5.81 % (3938525)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.56/5.81 % (3938525)CaDiCaL version: 2.1.3 % 39.56/5.81 % (3938525)Termination reason: Instruction limit % 39.56/5.81 % (3938525)Termination phase: Finite model building SAT solving % 39.56/5.81 % (3938525)Time elapsed: 0.208 s % 39.56/5.81 % (3938525)Peak memory usage: 34 MB % 39.56/5.81 % (3938525)Instructions burned: 866 (million) % 39.56/5.81 % (3938529)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1792822052:i=889:ins=1_2995 on theBenchmark for (2995ds/889Mi) % 39.56/5.81 % (3938518)Instruction limit reached! % 39.56/5.81 % (3938518)------------------------------ % 39.56/5.81 % (3938518)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 39.56/5.81 % (3938518)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.56/5.81 % (3938518)CaDiCaL version: 2.1.3 % 39.56/5.81 % (3938518)Termination reason: Instruction limit % 39.56/5.81 % (3938518)Termination phase: Saturation % 39.56/5.81 % (3938518)Time elapsed: 0.370 s % 39.56/5.81 % (3938518)Peak memory usage: 16 MB % 39.56/5.81 % (3938518)Instructions burned: 685 (million) % 39.56/5.81 % (3938531)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=2067414432: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) % 39.56/5.81 % (3938523)Instruction limit reached! % 39.56/5.81 % (3938523)------------------------------ % 39.56/5.81 % (3938523)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 39.56/5.81 % (3938523)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.56/5.81 % (3938523)CaDiCaL version: 2.1.3 % 39.56/5.81 % (3938523)Termination reason: Instruction limit % 39.56/5.81 % (3938523)Termination phase: Saturation % 39.56/5.81 % (3938523)Time elapsed: 0.307 s % 39.56/5.81 % (3938523)Peak memory usage: 14 MB % 39.56/5.81 % (3938523)Instructions burned: 477 (million) % 39.56/5.81 % (3938533)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1900223457:i=879:kws=inv_precedence:fsr=off_2994 on theBenchmark for (2994ds/879Mi) % 39.56/5.81 % (3938529)Cannot represent all propositional literals internally % 39.56/5.81 % (3938529)Refutation not found, incomplete strategy % 39.56/5.81 % (3938529)------------------------------ % 57.01/8.38 % (3938529)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 57.01/8.38 % (3938529)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 57.01/8.38 % (3938529)CaDiCaL version: 2.1.3 % 57.01/8.38 % (3938529)Termination reason: Refutation not found, incomplete strategy % 57.01/8.38 % (3938529)Time elapsed: 0.117 s % 57.01/8.38 % (3938529)Peak memory usage: 16 MB % 57.01/8.38 % (3938529)Instructions burned: 431 (million) % 57.01/8.38 % (3938529)------------------------------ % 57.01/8.38 % (3938529)------------------------------ % 57.01/8.38 % (3938535)fmb+10_1_sil=64000:random_seed=133895850:i=22061:nm=2:gsp=on_2993 on theBenchmark for (2993ds/22061Mi) % 57.01/8.38 % TRYING [1] % 57.01/8.38 % TRYING [2] % 57.01/8.38 % (3938531)Instruction limit reached! % 57.01/8.38 % (3938531)------------------------------ % 57.01/8.38 % (3938531)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 57.01/8.38 % (3938531)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 57.01/8.38 % (3938531)CaDiCaL version: 2.1.3 % 57.01/8.38 % (3938531)Termination reason: Instruction limit % 57.01/8.38 % (3938531)Termination phase: Saturation % 57.01/8.38 % (3938531)Time elapsed: 0.423 s % 57.01/8.38 % (3938531)Peak memory usage: 18 MB % 57.01/8.38 % (3938531)Instructions burned: 692 (million) % 57.01/8.38 % (3938527)Instruction limit reached! % 57.01/8.38 % (3938527)------------------------------ % 57.01/8.38 % (3938527)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 57.01/8.38 % (3938527)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 57.01/8.38 % (3938527)CaDiCaL version: 2.1.3 % 57.01/8.38 % (3938527)Termination reason: Instruction limit % 57.01/8.38 % (3938527)Termination phase: Saturation % 57.01/8.38 % (3938527)Time elapsed: 0.692 s % 57.01/8.38 % (3938527)Peak memory usage: 22 MB % 57.01/8.38 % (3938527)Instructions burned: 1180 (million) % 57.01/8.38 % (3938538)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3976716050:i=9515:nm=5_2990 on theBenchmark for (2990ds/9515Mi) % 57.01/8.38 % (3938539)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2894324034:fmbsr=1.7:i=920_2990 on theBenchmark for (2990ds/920Mi) % 57.01/8.38 % (3938533)Instruction limit reached! % 57.01/8.38 % (3938533)------------------------------ % 57.01/8.38 % (3938533)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 57.01/8.38 % (3938533)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 57.01/8.38 % (3938533)CaDiCaL version: 2.1.3 % 57.01/8.38 % (3938533)Termination reason: Instruction limit % 57.01/8.38 % (3938533)Termination phase: Saturation % 57.01/8.38 % (3938533)Time elapsed: 0.501 s % 57.01/8.38 % (3938533)Peak memory usage: 19 MB % 57.01/8.38 % (3938533)Instructions burned: 879 (million) % 57.01/8.38 % (3938542)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1720835480:i=5131_2989 on theBenchmark for (2989ds/5131Mi) % 57.01/8.38 % (3938538)Cannot represent all propositional literals internally % 57.01/8.38 % (3938538)Refutation not found, incomplete strategy % 57.01/8.38 % (3938538)------------------------------ % 57.01/8.38 % (3938538)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 57.01/8.38 % (3938538)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 57.01/8.38 % (3938538)CaDiCaL version: 2.1.3 % 57.01/8.38 % (3938538)Termination reason: Refutation not found, incomplete strategy % 57.01/8.39 % (3938538)Time elapsed: 0.213 s % 57.01/8.39 % (3938538)Peak memory usage: 16 MB % 57.01/8.39 % (3938538)Instructions burned: 430 (million) % 57.01/8.39 % (3938538)------------------------------ % 57.01/8.39 % (3938538)------------------------------ % 57.01/8.39 % (3938539)Cannot represent all propositional literals internally % 57.01/8.39 % (3938539)Refutation not found, incomplete strategy % 57.01/8.39 % (3938539)------------------------------ % 57.01/8.39 % (3938539)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 57.01/8.39 % (3938539)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 57.01/8.39 % (3938539)CaDiCaL version: 2.1.3 % 57.01/8.39 % (3938539)Termination reason: Refutation not found, incomplete strategy % 57.01/8.39 % (3938539)Time elapsed: 0.213 s % 57.01/8.39 % (3938539)Peak memory usage: 16 MB % 57.01/8.39 % (3938539)Instructions burned: 431 (million) % 57.01/8.39 % (3938539)------------------------------ % 57.01/8.39 % (3938539)------------------------------ % 57.01/8.39 % (3938544)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1184583803:i=1472:ins=7:fdi=8:gsp=on_2988 on theBenchmark for (2988ds/1472Mi) % 92.26/14.34 % (3938545)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=4249011782:i=6324_2987 on theBenchmark for (2987ds/6324Mi) % 92.26/14.34 % TRYING [3] % 92.26/14.34 % (3938545)Cannot represent all propositional literals internally % 92.26/14.34 % (3938545)Refutation not found, incomplete strategy % 92.26/14.34 % (3938545)------------------------------ % 92.26/14.34 % (3938545)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 92.26/14.34 % (3938545)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 92.26/14.34 % (3938545)CaDiCaL version: 2.1.3 % 92.26/14.34 % (3938545)Termination reason: Refutation not found, incomplete strategy % 92.26/14.34 % (3938545)Time elapsed: 0.203 s % 92.26/14.34 % (3938545)Peak memory usage: 16 MB % 92.26/14.34 % (3938545)Instructions burned: 413 (million) % 92.26/14.34 % (3938545)------------------------------ % 92.26/14.34 % (3938545)------------------------------ % 92.26/14.34 % (3938548)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=887019547:fmbsr=2.30978:i=2174_2985 on theBenchmark for (2985ds/2174Mi) % 92.26/14.34 % (3938544)Instruction limit reached! % 92.26/14.34 % (3938544)------------------------------ % 92.26/14.34 % (3938544)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 92.26/14.34 % (3938544)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 92.26/14.34 % (3938544)CaDiCaL version: 2.1.3 % 92.26/14.34 % (3938544)Termination reason: Instruction limit % 92.26/14.34 % (3938544)Termination phase: Saturation % 92.26/14.34 % (3938544)Time elapsed: 0.813 s % 92.26/14.34 % (3938544)Peak memory usage: 29 MB % 92.26/14.34 % (3938544)Instructions burned: 1474 (million) % 92.26/14.34 % (3938550)ott-2_1_sil=16000:newcnf=on:random_seed=3982517587:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2979 on theBenchmark for (2979ds/869Mi) % 92.26/14.34 % (3938548)Cannot represent all propositional literals internally % 92.26/14.34 % (3938548)Refutation not found, incomplete strategy % 92.26/14.34 % (3938548)------------------------------ % 92.26/14.34 % (3938548)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 92.26/14.34 % (3938548)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 92.26/14.34 % (3938548)CaDiCaL version: 2.1.3 % 92.26/14.34 % (3938548)Termination reason: Refutation not found, incomplete strategy % 92.26/14.34 % (3938548)Time elapsed: 0.966 s % 92.26/14.34 % (3938548)Peak memory usage: 25 MB % 92.26/14.34 % (3938548)Instructions burned: 1960 (million) % 92.26/14.34 % (3938548)------------------------------ % 92.26/14.34 % (3938548)------------------------------ % 92.26/14.34 % (3938552)ott+10_1_sil=32000:tgt=ground:random_seed=2127286494:i=5114:av=off_2975 on theBenchmark for (2975ds/5114Mi) % 92.26/14.34 % (3938550)Instruction limit reached! % 92.26/14.34 % (3938550)------------------------------ % 92.26/14.34 % (3938550)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 92.26/14.34 % (3938550)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 92.26/14.34 % (3938550)CaDiCaL version: 2.1.3 % 92.26/14.34 % (3938550)Termination reason: Instruction limit % 92.26/14.34 % (3938550)Termination phase: Saturation % 92.26/14.34 % (3938550)Time elapsed: 0.466 s % 92.26/14.34 % (3938550)Peak memory usage: 15 MB % 92.26/14.34 % (3938550)Instructions burned: 870 (million) % 92.26/14.34 % (3938554)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=1297745383:i=54282_2974 on theBenchmark for (2974ds/54282Mi) % 92.26/14.34 % TRYING [1] % 92.26/14.34 % TRYING [2] % 92.26/14.34 % TRYING [3] % 92.26/14.34 % (3938542)Instruction limit reached! % 92.26/14.34 % (3938542)------------------------------ % 92.26/14.34 % (3938542)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 92.26/14.34 % (3938542)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 92.26/14.34 % (3938542)CaDiCaL version: 2.1.3 % 92.26/14.34 % (3938542)Termination reason: Instruction limit % 92.26/14.34 % (3938542)Termination phase: Saturation % 92.26/14.34 % (3938542)Time elapsed: 2.906 s % 92.26/14.34 % (3938542)Peak memory usage: 35 MB % 92.26/14.34 % (3938542)Instructions burned: 5133 (million) % 92.26/14.34 % (3938556)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=2943194910:i=3512:aac=none_2960 on theBenchmark for (2960ds/3512Mi) % 92.26/14.34 % (3938552)Instruction limit reached! % 92.26/14.34 % (3938552)------------------------------ % 92.26/14.34 % (3938552)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 92.26/14.34 % (3938552)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 92.26/14.34 % (3938552)CaDiCaL version: 2.1.3 % 92.26/14.34 % (3938552)Termination reason: Instruction limit % 144.08/23.58 % (3938552)Termination phase: Saturation % 144.08/23.58 % (3938552)Time elapsed: 3.161 s % 144.08/23.58 % (3938552)Peak memory usage: 35 MB % 144.08/23.58 % (3938552)Instructions burned: 5115 (million) % 144.08/23.58 % (3938558)dis+21_1_sil=32000:sas=cadical:random_seed=1580372452:i=3773:amm=off_2943 on theBenchmark for (2943ds/3773Mi) % 144.08/23.58 % (3938535)Instruction limit reached! % 144.08/23.58 % (3938535)------------------------------ % 144.08/23.58 % (3938535)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 144.08/23.58 % (3938535)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 144.08/23.58 % (3938535)CaDiCaL version: 2.1.3 % 144.08/23.58 % (3938535)Termination reason: Instruction limit % 144.08/23.58 % (3938535)Termination phase: Finite model building constraint generation % 144.08/23.58 % (3938535)Time elapsed: 5.255 s % 144.08/23.58 % (3938535)Peak memory usage: 992 MB % 144.08/23.58 % (3938535)Instructions burned: 22061 (million) % 144.08/23.58 % (3938560)ott+11_1_sil=16000:gs=on:random_seed=3677334517:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2940 on theBenchmark for (2940ds/2251Mi) % 144.08/23.58 % (3938556)Instruction limit reached! % 144.08/23.58 % (3938556)------------------------------ % 144.08/23.58 % (3938556)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 144.08/23.58 % (3938556)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 144.08/23.58 % (3938556)CaDiCaL version: 2.1.3 % 144.08/23.58 % (3938556)Termination reason: Instruction limit % 144.08/23.58 % (3938556)Termination phase: Saturation % 144.08/23.58 % (3938556)Time elapsed: 2.107 s % 144.08/23.58 % (3938556)Peak memory usage: 35 MB % 144.08/23.58 % (3938556)Instructions burned: 3513 (million) % 144.08/23.58 % (3938562)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=2088302725:fmbsr=1.6:i=67534_2938 on theBenchmark for (2938ds/67534Mi) % 144.08/23.58 % (3938562)Cannot represent all propositional literals internally % 144.08/23.58 % (3938562)Refutation not found, incomplete strategy % 144.08/23.58 % (3938562)------------------------------ % 144.08/23.58 % (3938562)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 144.08/23.58 % (3938562)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 144.08/23.58 % (3938562)CaDiCaL version: 2.1.3 % 144.08/23.58 % (3938562)Termination reason: Refutation not found, incomplete strategy % 144.08/23.58 % (3938562)Time elapsed: 0.215 s % 144.08/23.58 % (3938562)Peak memory usage: 15 MB % 144.08/23.58 % (3938562)Instructions burned: 446 (million) % 144.08/23.58 % (3938562)------------------------------ % 144.08/23.58 % (3938562)------------------------------ % 144.08/23.58 % (3938564)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=3700929999:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2936 on theBenchmark for (2936ds/4591Mi) % 144.08/23.58 % (3938560)Instruction limit reached! % 144.08/23.58 % (3938560)------------------------------ % 144.08/23.58 % (3938560)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 144.08/23.58 % (3938560)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 144.08/23.58 % (3938560)CaDiCaL version: 2.1.3 % 144.08/23.58 % (3938560)Termination reason: Instruction limit % 144.08/23.58 % (3938560)Termination phase: Saturation % 144.08/23.58 % (3938560)Time elapsed: 0.641 s % 144.08/23.58 % (3938560)Peak memory usage: 20 MB % 144.08/23.58 % (3938560)Instructions burned: 2253 (million) % 144.08/23.58 % (3938566)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=3156891492:i=29340_2934 on theBenchmark for (2934ds/29340Mi) % 144.08/23.58 % (3938558)Instruction limit reached! % 144.08/23.58 % (3938558)------------------------------ % 144.08/23.58 % (3938558)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 144.08/23.58 % (3938558)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 144.08/23.58 % (3938558)CaDiCaL version: 2.1.3 % 144.08/23.58 % (3938558)Termination reason: Instruction limit % 144.08/23.58 % (3938558)Termination phase: Saturation % 144.08/23.58 % (3938558)Time elapsed: 2.179 s % 144.08/23.58 % (3938558)Peak memory usage: 34 MB % 144.08/23.58 % (3938558)Instructions burned: 3774 (million) % 144.08/23.58 % (3938568)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=3726512553:i=5211_2921 on theBenchmark for (2921ds/5211Mi) % 144.08/23.58 % (3938564)Instruction limit reached! % 144.08/23.58 % (3938564)------------------------------ % 144.08/23.58 % (3938564)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 144.08/23.58 % (3938564)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 213.76/30.40 % (3938564)CaDiCaL version: 2.1.3 % 213.76/30.40 % (3938564)Termination reason: Instruction limit % 213.76/30.40 % (3938564)Termination phase: Saturation % 213.76/30.40 % (3938564)Time elapsed: 1.792 s % 213.76/30.40 % (3938564)Peak memory usage: 31 MB % 213.76/30.40 % (3938564)Instructions burned: 4593 (million) % 213.76/30.40 % (3938570)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=2955436557:i=5497:nm=2_2918 on theBenchmark for (2918ds/5497Mi) % 213.76/30.40 % (3938570)Cannot represent all propositional literals internally % 213.76/30.40 % (3938570)Refutation not found, incomplete strategy % 213.76/30.40 % (3938570)------------------------------ % 213.76/30.40 % (3938570)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 213.76/30.40 % (3938570)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 213.76/30.40 % (3938570)CaDiCaL version: 2.1.3 % 213.76/30.40 % (3938570)Termination reason: Refutation not found, incomplete strategy % 213.76/30.40 % (3938570)Time elapsed: 0.204 s % 213.76/30.40 % (3938570)Peak memory usage: 16 MB % 213.76/30.40 % (3938570)Instructions burned: 413 (million) % 213.76/30.40 % (3938570)------------------------------ % 213.76/30.40 % (3938570)------------------------------ % 213.76/30.40 % (3938572)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=38469815:fmbsr=2:i=46332_2915 on theBenchmark for (2915ds/46332Mi) % 213.76/30.40 % (3938572)Cannot represent all propositional literals internally % 213.76/30.40 % (3938572)Refutation not found, incomplete strategy % 213.76/30.40 % (3938572)------------------------------ % 213.76/30.40 % (3938572)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 213.76/30.40 % (3938572)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 213.76/30.40 % (3938572)CaDiCaL version: 2.1.3 % 213.76/30.40 % (3938572)Termination reason: Refutation not found, incomplete strategy % 213.76/30.40 % (3938572)Time elapsed: 0.217 s % 213.76/30.40 % (3938572)Peak memory usage: 15 MB % 213.76/30.40 % (3938572)Instructions burned: 446 (million) % 213.76/30.40 % (3938572)------------------------------ % 213.76/30.40 % (3938572)------------------------------ % 213.76/30.40 % (3938574)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=2476883339:i=14071_2913 on theBenchmark for (2913ds/14071Mi) % 213.76/30.40 % (3938574)Cannot represent all propositional literals internally % 213.76/30.40 % (3938574)Refutation not found, incomplete strategy % 213.76/30.40 % (3938574)------------------------------ % 213.76/30.40 % (3938574)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 213.76/30.40 % (3938574)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 213.76/30.40 % (3938574)CaDiCaL version: 2.1.3 % 213.76/30.40 % (3938574)Termination reason: Refutation not found, incomplete strategy % 213.76/30.40 % (3938574)Time elapsed: 0.214 s % 213.76/30.40 % (3938574)Peak memory usage: 16 MB % 213.76/30.40 % (3938574)Instructions burned: 431 (million) % 213.76/30.40 % (3938574)------------------------------ % 213.76/30.40 % (3938574)------------------------------ % 213.76/30.40 % (3938576)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2228529021:i=22565:add=on:rawr=on_2911 on theBenchmark for (2911ds/22565Mi) % 213.76/30.40 % (3938568)Instruction limit reached! % 213.76/30.40 % (3938568)------------------------------ % 213.76/30.40 % (3938568)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 213.76/30.40 % (3938568)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 213.76/30.40 % (3938568)CaDiCaL version: 2.1.3 % 213.76/30.40 % (3938568)Termination reason: Instruction limit % 213.76/30.40 % (3938568)Termination phase: Saturation % 213.76/30.40 % (3938568)Time elapsed: 2.677 s % 213.76/30.40 % (3938568)Peak memory usage: 44 MB % 213.76/30.40 % (3938568)Instructions burned: 5213 (million) % 213.76/30.40 % (3938578)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=2504425639:i=8173:av=off_2894 on theBenchmark for (2894ds/8173Mi) % 213.76/30.40 % (3938566)Instruction limit reached! % 213.76/30.40 % (3938566)------------------------------ % 213.76/30.40 % (3938566)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 213.76/30.40 % (3938566)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 213.76/30.40 % (3938566)CaDiCaL version: 2.1.3 % 213.76/30.40 % (3938566)Termination reason: Instruction limit % 213.76/30.40 % (3938566)Termination phase: Saturation % 213.76/30.40 % (3938566)Time elapsed: 7.481 s % 213.76/30.40 % (3938566)Peak memory usage: 313 MB % 213.76/30.40 % (3938566)Instructions burned: 29341 (million) % 213.76/30.40 % (3938580)dis+10_16:1_sil=16000:random_seed=3018292176:i=9155:fsr=off_2858 on theBenchmark for (2858ds/9155Mi) % 273.54/38.88 % TRYING [4] % 273.54/38.88 % (3938578)Instruction limit reached! % 273.54/38.88 % (3938578)------------------------------ % 273.54/38.88 % (3938578)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 273.54/38.88 % (3938578)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 273.54/38.88 % (3938578)CaDiCaL version: 2.1.3 % 273.54/38.88 % (3938578)Termination reason: Instruction limit % 273.54/38.88 % (3938578)Termination phase: Saturation % 273.54/38.88 % (3938578)Time elapsed: 5.219 s % 273.54/38.88 % (3938578)Peak memory usage: 79 MB % 273.54/38.88 % (3938578)Instructions burned: 8173 (million) % 273.54/38.88 % (3938734)ott-3_8_sil=64000:random_seed=4018736710:i=20139:bs=on_2842 on theBenchmark for (2842ds/20139Mi) % 273.54/38.88 % (3938580)Instruction limit reached! % 273.54/38.88 % (3938580)------------------------------ % 273.54/38.88 % (3938580)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 273.54/38.88 % (3938580)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 273.54/38.88 % (3938580)CaDiCaL version: 2.1.3 % 273.54/38.88 % (3938580)Termination reason: Instruction limit % 273.54/38.88 % (3938580)Termination phase: Saturation % 273.54/38.88 % (3938580)Time elapsed: 2.767 s % 273.54/38.88 % (3938580)Peak memory usage: 59 MB % 273.54/38.88 % (3938580)Instructions burned: 9157 (million) % 273.54/38.88 % (3938736)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=514193933:fmbsr=2:i=32576_2831 on theBenchmark for (2831ds/32576Mi) % 273.54/38.88 % (3938736)Cannot represent all propositional literals internally % 273.54/38.88 % (3938736)Refutation not found, incomplete strategy % 273.54/38.88 % (3938736)------------------------------ % 273.54/38.88 % (3938736)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 273.54/38.88 % (3938736)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 273.54/38.88 % (3938736)CaDiCaL version: 2.1.3 % 273.54/38.88 % (3938736)Termination reason: Refutation not found, incomplete strategy % 273.54/38.88 % (3938736)Time elapsed: 0.109 s % 273.54/38.88 % (3938736)Peak memory usage: 16 MB % 273.54/38.88 % (3938736)Instructions burned: 413 (million) % 273.54/38.88 % (3938736)------------------------------ % 273.54/38.88 % (3938736)------------------------------ % 273.54/38.88 % (3938738)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=2475502946:i=11404_2829 on theBenchmark for (2829ds/11404Mi) % 273.54/38.88 % TRYING [4] % 273.54/38.88 % (3938576)Instruction limit reached! % 273.54/38.88 % (3938576)------------------------------ % 273.54/38.88 % (3938576)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 273.54/38.88 % (3938576)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 273.54/38.88 % (3938576)CaDiCaL version: 2.1.3 % 273.54/38.88 % (3938576)Termination reason: Instruction limit % 273.54/38.88 % (3938576)Termination phase: Saturation % 273.54/38.88 % (3938576)Time elapsed: 11.664 s % 273.54/38.88 % (3938576)Peak memory usage: 204 MB % 273.54/38.88 % (3938576)Instructions burned: 22565 (million) % 273.54/38.88 % (3938740)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=1315499132:i=14134_2794 on theBenchmark for (2794ds/14134Mi) % 273.54/38.88 % (3938738)Instruction limit reached! % 273.54/38.88 % (3938738)------------------------------ % 273.54/38.88 % (3938738)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 273.54/38.88 % (3938738)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 273.54/38.88 % (3938738)CaDiCaL version: 2.1.3 % 273.54/38.88 % (3938738)Termination reason: Instruction limit % 273.54/38.88 % (3938738)Termination phase: Saturation % 273.54/38.88 % (3938738)Time elapsed: 3.828 s % 273.54/38.88 % (3938738)Peak memory usage: 68 MB % 273.54/38.88 % (3938738)Instructions burned: 11405 (million) % 273.54/38.88 % (3938742)dis+33_16_sil=32000:sac=on:random_seed=800558308:i=15851:nm=0_2791 on theBenchmark for (2791ds/15851Mi) % 273.54/38.88 % (3938554)Instruction limit reached! % 273.54/38.88 % (3938554)------------------------------ % 273.54/38.88 % (3938554)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 273.54/38.88 % (3938554)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 273.54/38.88 % (3938554)CaDiCaL version: 2.1.3 % 273.54/38.88 % (3938554)Termination reason: Instruction limit % 273.54/38.88 % (3938554)Termination phase: Finite model building constraint generation % 273.54/38.88 % (3938554)Time elapsed: 20.605 s % 273.54/38.88 % (3938554)Peak memory usage: 1712 MB % 273.54/38.88 % (3938554)Instructions burned: 54283 (million) % 273.54/38.88 % (3938744)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=4016151720:avsq=on:i=17627:add=on:amm=off_2766 on theBenchmark for (2766ds/17627Mi) % 285.22/40.51 % (3938742)Instruction limit reached! % 285.22/40.51 % (3938742)------------------------------ % 285.22/40.51 % (3938742)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 285.22/40.51 % (3938742)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 285.22/40.51 % (3938742)CaDiCaL version: 2.1.3 % 285.22/40.51 % (3938742)Termination reason: Instruction limit % 285.22/40.51 % (3938742)Termination phase: Saturation % 285.22/40.51 % (3938742)Time elapsed: 4.207 s % 285.22/40.51 % (3938742)Peak memory usage: 203 MB % 285.22/40.51 % (3938742)Instructions burned: 15853 (million) % 285.22/40.51 % (3938746)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=2230570368:s2a=on:i=53295_2749 on theBenchmark for (2749ds/53295Mi) % 285.22/40.51 % (3938734)Instruction limit reached! % 285.22/40.51 % (3938734)------------------------------ % 285.22/40.51 % (3938734)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 285.22/40.51 % (3938734)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 285.22/40.51 % (3938734)CaDiCaL version: 2.1.3 % 285.22/40.51 % (3938734)Termination reason: Instruction limit % 285.22/40.51 % (3938734)Termination phase: Saturation % 285.22/40.51 % (3938734)Time elapsed: 12.786 s % 285.22/40.51 % (3938734)Peak memory usage: 69 MB % 285.22/40.51 % (3938734)Instructions burned: 20140 (million) % 285.22/40.51 % (3938778)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=2468645461:i=26857:ins=20_2714 on theBenchmark for (2714ds/26857Mi) % 285.22/40.51 % (3938778)Cannot represent all propositional literals internally % 285.22/40.51 % (3938778)Refutation not found, incomplete strategy % 285.22/40.51 % (3938778)------------------------------ % 285.22/40.51 % (3938778)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 285.22/40.51 % (3938778)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 285.22/40.51 % (3938778)CaDiCaL version: 2.1.3 % 285.22/40.51 % (3938778)Termination reason: Refutation not found, incomplete strategy % 285.22/40.51 % (3938778)Time elapsed: 0.215 s % 285.22/40.51 % (3938778)Peak memory usage: 16 MB % 285.22/40.51 % (3938778)Instructions burned: 431 (million) % 285.22/40.51 % (3938778)------------------------------ % 285.22/40.51 % (3938778)------------------------------ % 285.22/40.51 % (3938846)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=2968948843:i=28120:bs=on:fsr=off_2711 on theBenchmark for (2711ds/28120Mi) % 285.22/40.51 % (3938740)Instruction limit reached! % 285.22/40.51 % (3938740)------------------------------ % 285.22/40.51 % (3938740)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 285.22/40.51 % (3938740)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 285.22/40.51 % (3938740)CaDiCaL version: 2.1.3 % 285.22/40.51 % (3938740)Termination reason: Instruction limit % 285.22/40.51 % (3938740)Termination phase: Saturation % 285.22/40.51 % (3938740)Time elapsed: 8.976 s % 285.22/40.51 % (3938740)Peak memory usage: 74 MB % 285.22/40.51 % (3938740)Instructions burned: 14135 (million) % 285.22/40.51 % (3938958)fmb+10_1_sil=256000:fmbss=7:random_seed=1291474754:fmbsr=1.6:i=182295_2704 on theBenchmark for (2704ds/182295Mi) % 285.22/40.51 % (3938958)Cannot represent all propositional literals internally % 285.22/40.51 % (3938958)Refutation not found, incomplete strategy % 285.22/40.51 % (3938958)------------------------------ % 285.22/40.51 % (3938958)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 285.22/40.51 % (3938958)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 285.22/40.51 % (3938958)CaDiCaL version: 2.1.3 % 285.22/40.51 % (3938958)Termination reason: Refutation not found, incomplete strategy % 285.22/40.51 % (3938958)Time elapsed: 0.320 s % 285.22/40.51 % (3938958)Peak memory usage: 16 MB % 285.22/40.51 % (3938958)Instructions burned: 430 (million) % 285.22/40.51 % (3938958)------------------------------ % 285.22/40.51 % (3938958)------------------------------ % 285.22/40.51 % (3939001)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=264642740:i=44625:gsp=on_2700 on theBenchmark for (2700ds/44625Mi) % 285.22/40.51 % (3939001)Cannot represent all propositional literals internally % 285.22/40.51 % (3939001)Refutation not found, incomplete strategy % 285.22/40.51 % (3939001)------------------------------ % 285.22/40.51 % (3939001)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 285.22/40.51 % (3939001)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 285.22/40.51 % (3939001)CaDiCaL version: 2.1.3 % 285.22/40.51 % (3939001)TTerminated % 300.06/42.63 % Vampire exiting %------------------------------------------------------------------------------