Vampire---5.0 system information being retrieved Vampire---5.0's non-default parameters being retrieved Vampire---5.0's THF_Finite.s does not need preparation Vampire---5.0 being executed on THF_Finite.s using /home/tptp/Systems/Vampire---5.0/run_vampire 'THF_Finite.s.p' 60 THM % START OF SYSTEM OUTPUT Running higher-order theorem proving Running: /home/tptp/Systems/Vampire---5.0/vampire-hol --cores 7 --input_syntax tptp --proof tptp --output_axiom_names on --print_def_sorts on --mode portfolio --schedule snake_tptp_hol /tmp/tmp.1gVJCcgpU5/Vampire_2428107.p -m 16384 -t 60 % (2428149)lrs+1002_1:128_aac=none:au=on:cnfonf=lazy_not_gen_be_off:sos=all:i=2:si=on:rtra=on_0 on Vampire_2428107 for (1ds/2Mi) % (2428145)lrs+1002_1:8_bd=off:fd=off:hud=10:tnu=1:i=183:si=on:rtra=on_0 on Vampire_2428107 for (1ds/183Mi) % (2428146)lrs+10_1:1_c=on:cnfonf=conj_eager:fd=off:fe=off:kws=frequency:spb=intro:i=4:si=on:rtra=on_0 on Vampire_2428107 for (1ds/4Mi) % (2428149)Refutation not found, incomplete strategy % (2428149)------------------------------ % (2428149)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100) % (2428149)Termination reason: Refutation not found, incomplete strategy % (2428149)Memory used [KB]: 5628 % (2428149)Time elapsed: 0.003 s % (2428149)------------------------------ % (2428149)------------------------------ % (2428147)dis+1010_1:1_au=on:cbe=off:chr=on:fsr=off:hfsq=on:nm=64:sos=theory:sp=weighted_frequency:i=27:si=on:rtra=on_0 on Vampire_2428107 for (1ds/27Mi) % (2428148)lrs+10_1:1_au=on:inj=on:i=2:si=on:rtra=on_0 on Vampire_2428107 for (1ds/2Mi) % (2428150)lrs+1002_1:1_au=on:bd=off:e2e=on:sd=2:sos=on:ss=axioms:i=275:si=on:rtra=on_0 on Vampire_2428107 for (1ds/275Mi) % (2428145)First to succeed. % (2428150)Refutation not found, incomplete strategy % (2428150)------------------------------ % (2428150)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100) % (2428150)Termination reason: Refutation not found, incomplete strategy % (2428150)Memory used [KB]: 5500 % (2428150)Time elapsed: 0.001 s % (2428150)------------------------------ % (2428150)------------------------------ % (2428146)Also succeeded, but the first one will report. % (2428151)lrs+1004_1:128_cond=on:e2e=on:sp=weighted_frequency:i=18:si=on:rtra=on_0 on Vampire_2428107 for (1ds/18Mi) % (2428147)Also succeeded, but the first one will report. % (2428145)Refutation found. Thanks to Tanya! % SZS status Theorem for Vampire_2428107 % SZS output start Proof for Vampire_2428107 thf(type_def_5, type, beverage: $tType). thf(type_def_6, type, syrup: $tType). thf(type_def_8, type, d_beverage: $tType). thf(type_def_9, type, d_syrup: $tType). thf(func_def_0, type, beverage: $tType). thf(func_def_1, type, syrup: $tType). thf(func_def_2, type, coffee: beverage). thf(func_def_3, type, vanilla: syrup). thf(func_def_4, type, mix: (syrup > beverage) > beverage). thf(func_def_5, type, heat: beverage > beverage). thf(func_def_6, type, heated_mix: (syrup > beverage) > beverage). thf(func_def_7, type, hot: beverage > $o). thf(func_def_8, type, d_beverage: $tType). thf(func_def_9, type, d_syrup: $tType). thf(func_def_10, type, d2beverage: d_beverage > beverage). thf(func_def_11, type, d2syrup: d_syrup > syrup). thf(func_def_12, type, d_coffee: d_beverage). thf(func_def_13, type, d_vanilla: d_syrup). thf(func_def_19, type, sK0: syrup > d_syrup). thf(func_def_20, type, sK1: beverage > d_beverage). thf(func_def_21, type, sK2: syrup > beverage). thf(func_def_22, type, sK3: syrup > beverage). thf(func_def_23, type, sK4: syrup > beverage). thf(func_def_25, type, ph6: !>[X0: $tType]:(X0)). thf(func_def_26, type, sK7: syrup > beverage). thf(f132,plain,( $false), inference(avatar_sat_refutation,[status(thm)],[f49,f50,f128,f131])). thf(f131,plain,( ~spl5_1 | ~spl5_3), inference(avatar_contradiction_clause,[status(thm)],[f130])). thf(f130,plain,( $false | (~spl5_1 | ~spl5_3)), inference(subsumption_resolution,[status(thm)],[f129,f60])). thf(f60,plain,( ( ! [X0 : beverage,X1 : d_beverage] : (((d2beverage @ X1) = X0)) )), inference(superposition,[status(thm)],[f32,f51])). thf(f51,plain,( ( ! [X0 : d_beverage,X1 : d_beverage] : ((X0 = X1)) )), inference(superposition,[status(thm)],[f24,f24])). thf(f24,plain,( ( ! [X7 : d_beverage] : ((d_coffee = X7)) )), inference(cnf_transformation,[status(thm)],[f16])). thf(f16,plain,( ! [X0 : syrup] : ((d2syrup @ (sK0 @ X0)) = X0) & ! [X2 : beverage] : ((d2beverage @ (sK1 @ X2)) = X2) & ! [X4 : d_syrup] : (d_vanilla = X4) & ((d2beverage @ d_coffee) = (heat @ (d2beverage @ d_coffee))) & (mix = (^[Y0 : syrup > beverage]: (d2beverage @ d_coffee))) & (heated_mix = (^[Y0 : syrup > beverage]: (d2beverage @ d_coffee))) & ! [X5 : d_beverage,X6 : d_beverage] : (((d2beverage @ X5) != (d2beverage @ X6)) | (X5 = X6)) & ((hot @ (d2beverage @ d_coffee)) = $true) & (coffee = (d2beverage @ d_coffee)) & ! [X7 : d_beverage] : (d_coffee = X7) & ! [X8 : d_syrup,X9 : d_syrup] : ((X8 = X9) | ((d2syrup @ X9) != (d2syrup @ X8))) & (vanilla = (d2syrup @ d_vanilla))), inference(skolemisation,[status(esa),new_symbols(skolem,[sK0,sK1])],[f13,f15,f14])). thf(f14,plain,( ! [X0 : syrup] : (? [X1 : d_syrup] : ((d2syrup @ X1) = X0) => ((d2syrup @ (sK0 @ X0)) = X0))), introduced(definition,[],[choice_axiom])). thf(f15,plain,( ! [X2 : beverage] : (? [X3 : d_beverage] : ((d2beverage @ X3) = X2) => ((d2beverage @ (sK1 @ X2)) = X2))), introduced(definition,[],[choice_axiom])). thf(f13,plain,( ! [X0 : syrup] : ? [X1 : d_syrup] : ((d2syrup @ X1) = X0) & ! [X2 : beverage] : ? [X3 : d_beverage] : ((d2beverage @ X3) = X2) & ! [X4 : d_syrup] : (d_vanilla = X4) & ((d2beverage @ d_coffee) = (heat @ (d2beverage @ d_coffee))) & (mix = (^[Y0 : syrup > beverage]: (d2beverage @ d_coffee))) & (heated_mix = (^[Y0 : syrup > beverage]: (d2beverage @ d_coffee))) & ! [X5 : d_beverage,X6 : d_beverage] : (((d2beverage @ X5) != (d2beverage @ X6)) | (X5 = X6)) & ((hot @ (d2beverage @ d_coffee)) = $true) & (coffee = (d2beverage @ d_coffee)) & ! [X7 : d_beverage] : (d_coffee = X7) & ! [X8 : d_syrup,X9 : d_syrup] : ((X8 = X9) | ((d2syrup @ X9) != (d2syrup @ X8))) & (vanilla = (d2syrup @ d_vanilla))), inference(rectify,[status(thm)],[f11])). thf(f11,plain,( ! [X6 : syrup] : ? [X7 : d_syrup] : ((d2syrup @ X7) = X6) & ! [X4 : beverage] : ? [X5 : d_beverage] : ((d2beverage @ X5) = X4) & ! [X9 : d_syrup] : (d_vanilla = X9) & ((d2beverage @ d_coffee) = (heat @ (d2beverage @ d_coffee))) & (mix = (^[Y0 : syrup > beverage]: (d2beverage @ d_coffee))) & (heated_mix = (^[Y0 : syrup > beverage]: (d2beverage @ d_coffee))) & ! [X0 : d_beverage,X1 : d_beverage] : (((d2beverage @ X1) != (d2beverage @ X0)) | (X0 = X1)) & ((hot @ (d2beverage @ d_coffee)) = $true) & (coffee = (d2beverage @ d_coffee)) & ! [X8 : d_beverage] : (d_coffee = X8) & ! [X2 : d_syrup,X3 : d_syrup] : ((X2 = X3) | ((d2syrup @ X2) != (d2syrup @ X3))) & (vanilla = (d2syrup @ d_vanilla))), inference(ennf_transformation,[status(thm)],[f10])). thf(f10,plain,( ! [X9 : d_syrup] : (d_vanilla = X9) & (vanilla = (d2syrup @ d_vanilla)) & ((hot @ (d2beverage @ d_coffee)) = $true) & ! [X4 : beverage] : ? [X5 : d_beverage] : ((d2beverage @ X5) = X4) & (coffee = (d2beverage @ d_coffee)) & ! [X2 : d_syrup,X3 : d_syrup] : (((d2syrup @ X2) = (d2syrup @ X3)) => (X2 = X3)) & ! [X0 : d_beverage,X1 : d_beverage] : (((d2beverage @ X1) = (d2beverage @ X0)) => (X0 = X1)) & ((d2beverage @ d_coffee) = (heat @ (d2beverage @ d_coffee))) & (heated_mix = (^[Y0 : syrup > beverage]: (d2beverage @ d_coffee))) & ! [X6 : syrup] : ? [X7 : d_syrup] : ((d2syrup @ X7) = X6) & ! [X8 : d_beverage] : (d_coffee = X8) & (mix = (^[Y0 : syrup > beverage]: (d2beverage @ d_coffee)))), inference(rectify,[status(thm)],[f8])). thf(f8,plain,( (vanilla = (d2syrup @ d_vanilla)) & ! [X0 : d_beverage,X1 : d_beverage] : (((d2beverage @ X1) = (d2beverage @ X0)) => (X0 = X1)) & (coffee = (d2beverage @ d_coffee)) & ! [X2 : d_syrup,X3 : d_syrup] : (((d2syrup @ X2) = (d2syrup @ X3)) => (X2 = X3)) & ! [X4 : beverage] : ? [X5 : d_beverage] : ((d2beverage @ X5) = X4) & ((d2beverage @ d_coffee) = (heat @ (d2beverage @ d_coffee))) & ! [X6 : syrup] : ? [X7 : d_syrup] : ((d2syrup @ X7) = X6) & (mix = (^[Y0 : syrup > beverage]: (d2beverage @ d_coffee))) & ! [X9 : d_beverage] : (d_coffee = X9) & (heated_mix = (^[Y0 : syrup > beverage]: (d2beverage @ d_coffee))) & ! [X11 : d_syrup] : (d_vanilla = X11) & ((hot @ (d2beverage @ d_coffee)) = $true)), inference(fool_elimination,[status(thm)],[f7])). thf(f7,plain,( (vanilla = (d2syrup @ d_vanilla)) & ! [X0 : d_beverage,X1 : d_beverage] : (((d2beverage @ X1) = (d2beverage @ X0)) => (X0 = X1)) & (coffee = (d2beverage @ d_coffee)) & ! [X2 : d_syrup,X3 : d_syrup] : (((d2syrup @ X2) = (d2syrup @ X3)) => (X2 = X3)) & ! [X4 : beverage] : ? [X5 : d_beverage] : ((d2beverage @ X5) = X4) & ((d2beverage @ d_coffee) = (heat @ (d2beverage @ d_coffee))) & ! [X6 : syrup] : ? [X7 : d_syrup] : ((d2syrup @ X7) = X6) & (mix = (^[X8 : syrup > beverage] : (d2beverage @ d_coffee))) & ! [X9 : d_beverage] : (d_coffee = X9) & ((^[X10 : syrup > beverage] : (d2beverage @ d_coffee)) = heated_mix) & ! [X11 : d_syrup] : (d_vanilla = X11) & (hot @ (d2beverage @ d_coffee))), inference(rectify,[status(thm)],[f1])). thf(f1,axiom,( (vanilla = (d2syrup @ d_vanilla)) & ! [X3 : d_beverage,X2 : d_beverage] : (((d2beverage @ X2) = (d2beverage @ X3)) => (X2 = X3)) & (coffee = (d2beverage @ d_coffee)) & ! [X6 : d_syrup,X7 : d_syrup] : (((d2syrup @ X6) = (d2syrup @ X7)) => (X6 = X7)) & ! [X0 : beverage] : ? [X1 : d_beverage] : ((d2beverage @ X1) = X0) & ((d2beverage @ d_coffee) = (heat @ (d2beverage @ d_coffee))) & ! [X4 : syrup] : ? [X5 : d_syrup] : ((d2syrup @ X5) = X4) & (mix = (^[X8 : syrup > beverage] : (d2beverage @ d_coffee))) & ! [X1 : d_beverage] : (d_coffee = X1) & ((^[X8 : syrup > beverage] : (d2beverage @ d_coffee)) = heated_mix) & ! [X5 : d_syrup] : (d_vanilla = X5) & (hot @ (d2beverage @ d_coffee))), file('/tmp/tmp.1gVJCcgpU5/Vampire_2428107.p',model)). thf(f32,plain,( ( ! [X2 : beverage] : (((d2beverage @ (sK1 @ X2)) = X2)) )), inference(cnf_transformation,[status(thm)],[f16])). thf(f129,plain,( ( ! [X3 : syrup] : (((d2beverage @ d_coffee) != (sK4 @ X3))) ) | (~spl5_1 | ~spl5_3)), inference(subsumption_resolution,[status(thm)],[f40,f66])). thf(f66,plain,( ( ! [X0 : beverage] : (($true = (hot @ X0))) ) | ~spl5_3), inference(superposition,[status(thm)],[f47,f60])). thf(f47,plain,( ((hot @ (d2beverage @ d_coffee)) = $true) | ~spl5_3), inference(avatar_component_clause,[status(thm)],[f46])). thf(f46,definition,( spl5_3 <=> ((hot @ (d2beverage @ d_coffee)) = $true)), introduced(definition,[new_symbols(naming,[spl5_3])],[avatar_definition])). thf(f40,plain,( ( ! [X3 : syrup] : (($true != (hot @ (sK4 @ X3))) | ((d2beverage @ d_coffee) != (sK4 @ X3))) ) | ~spl5_1), inference(avatar_component_clause,[status(thm)],[f39])). thf(f39,definition,( spl5_1 <=> ! [X3 : syrup] : (((d2beverage @ d_coffee) != (sK4 @ X3)) | ($true != (hot @ (sK4 @ X3))))), introduced(definition,[new_symbols(naming,[spl5_1])],[avatar_definition])). thf(f128,plain,( spl5_2), inference(avatar_contradiction_clause,[status(thm)],[f127])). thf(f127,plain,( $false | spl5_2), inference(subsumption_resolution,[status(thm)],[f126,f30])). thf(f30,plain,( ((d2beverage @ d_coffee) = (heat @ (d2beverage @ d_coffee)))), inference(cnf_transformation,[status(thm)],[f16])). thf(f126,plain,( ((d2beverage @ d_coffee) != (heat @ (d2beverage @ d_coffee))) | spl5_2), inference(beta_eta_normalization,[status(thm)],[f125])). thf(f125,plain,( (((^[Y0 : syrup > beverage]: (heat @ (d2beverage @ d_coffee))) @ sK7) != ((^[Y0 : syrup > beverage]: (d2beverage @ d_coffee)) @ sK7)) | spl5_2), inference(negative_extensionality,[status(thm)],[f44])). thf(f44,plain,( ((^[Y0 : syrup > beverage]: (heat @ (d2beverage @ d_coffee))) != (^[Y0 : syrup > beverage]: (d2beverage @ d_coffee))) | spl5_2), inference(avatar_component_clause,[status(thm)],[f42])). thf(f42,definition,( spl5_2 <=> ((^[Y0 : syrup > beverage]: (heat @ (d2beverage @ d_coffee))) = (^[Y0 : syrup > beverage]: (d2beverage @ d_coffee)))), introduced(definition,[new_symbols(naming,[spl5_2])],[avatar_definition])). thf(f50,plain,( spl5_3), inference(avatar_split_clause,[status(thm)],[f26,f46])). thf(f26,plain,( ((hot @ (d2beverage @ d_coffee)) = $true)), inference(cnf_transformation,[status(thm)],[f16])). thf(f49,plain,( spl5_1 | ~spl5_2 | ~spl5_3), inference(avatar_split_clause,[status(thm)],[f37,f46,f42,f39])). thf(f37,plain,( ( ! [X3 : syrup] : (((^[Y0 : syrup > beverage]: (heat @ (d2beverage @ d_coffee))) != (^[Y0 : syrup > beverage]: (d2beverage @ d_coffee))) | ((hot @ (d2beverage @ d_coffee)) != $true) | ((d2beverage @ d_coffee) != (sK4 @ X3)) | ($true != (hot @ (sK4 @ X3)))) )), inference(trivial_inequality_removal,[status(thm)],[f36])). thf(f36,plain,( ( ! [X3 : syrup] : (((hot @ (d2beverage @ d_coffee)) != $true) | ($true != (hot @ (sK4 @ X3))) | ((d2beverage @ d_coffee) != (sK4 @ X3)) | ((d2beverage @ d_coffee) != (d2beverage @ d_coffee)) | ((^[Y0 : syrup > beverage]: (heat @ (d2beverage @ d_coffee))) != (^[Y0 : syrup > beverage]: (d2beverage @ d_coffee)))) )), inference(beta_eta_normalization,[status(thm)],[f35])). thf(f35,plain,( ( ! [X3 : syrup] : (((d2beverage @ d_coffee) != ((^[Y0 : syrup > beverage]: (d2beverage @ d_coffee)) @ sK2)) | ((hot @ ((^[Y0 : syrup > beverage]: (d2beverage @ d_coffee)) @ sK3)) != $true) | ((^[Y0 : syrup > beverage]: (heat @ ((^[Y1 : syrup > beverage]: (d2beverage @ d_coffee)) @ Y0))) != (^[Y0 : syrup > beverage]: (d2beverage @ d_coffee))) | ($true != (hot @ (sK4 @ X3))) | ((d2beverage @ d_coffee) != (sK4 @ X3))) )), inference(definition_unfolding,[status(thm)],[f34,f25,f28,f28,f25,f28,f29])). thf(f29,plain,( (mix = (^[Y0 : syrup > beverage]: (d2beverage @ d_coffee)))), inference(cnf_transformation,[status(thm)],[f16])). thf(f28,plain,( (heated_mix = (^[Y0 : syrup > beverage]: (d2beverage @ d_coffee)))), inference(cnf_transformation,[status(thm)],[f16])). thf(f25,plain,( (coffee = (d2beverage @ d_coffee))), inference(cnf_transformation,[status(thm)],[f16])). thf(f34,plain,( ( ! [X3 : syrup] : ((coffee != (heated_mix @ sK2)) | ($true != (hot @ (heated_mix @ sK3))) | ($true != (hot @ (sK4 @ X3))) | (coffee != (sK4 @ X3)) | (heated_mix != (^[Y0 : syrup > beverage]: (heat @ (mix @ Y0))))) )), inference(cnf_transformation,[status(thm)],[f21])). thf(f21,plain,( (coffee != (heated_mix @ sK2)) | ($true != (hot @ (heated_mix @ sK3))) | ! [X3 : syrup] : (($true != (hot @ (sK4 @ X3))) | (coffee != (sK4 @ X3))) | (heated_mix != (^[Y0 : syrup > beverage]: (heat @ (mix @ Y0))))), inference(skolemisation,[status(esa),new_symbols(skolem,[sK2,sK3,sK4])],[f17,f20,f19,f18])). thf(f18,plain,( ? [X0 : syrup > beverage] : (coffee != (heated_mix @ X0)) => (coffee != (heated_mix @ sK2))), introduced(definition,[],[choice_axiom])). thf(f19,plain,( ? [X1 : syrup > beverage] : ($true != (hot @ (heated_mix @ X1))) => ($true != (hot @ (heated_mix @ sK3)))), introduced(definition,[],[choice_axiom])). thf(f20,plain,( ? [X2 : syrup > beverage] : ! [X3 : syrup] : (($true != (hot @ (X2 @ X3))) | (coffee != (X2 @ X3))) => ! [X3 : syrup] : (($true != (hot @ (sK4 @ X3))) | (coffee != (sK4 @ X3)))), introduced(definition,[],[choice_axiom])). thf(f17,plain,( ? [X0 : syrup > beverage] : (coffee != (heated_mix @ X0)) | ? [X1 : syrup > beverage] : ($true != (hot @ (heated_mix @ X1))) | ? [X2 : syrup > beverage] : ! [X3 : syrup] : (($true != (hot @ (X2 @ X3))) | (coffee != (X2 @ X3))) | (heated_mix != (^[Y0 : syrup > beverage]: (heat @ (mix @ Y0))))), inference(rectify,[status(thm)],[f12])). thf(f12,plain,( ? [X2 : syrup > beverage] : (coffee != (heated_mix @ X2)) | ? [X3 : syrup > beverage] : ($true != (hot @ (heated_mix @ X3))) | ? [X0 : syrup > beverage] : ! [X1 : syrup] : (($true != (hot @ (X0 @ X1))) | (coffee != (X0 @ X1))) | (heated_mix != (^[Y0 : syrup > beverage]: (heat @ (mix @ Y0))))), inference(ennf_transformation,[status(thm)],[f9])). thf(f9,plain,( ~(~? [X0 : syrup > beverage] : ~? [X1 : syrup] : (($true = (hot @ (X0 @ X1))) & (coffee = (X0 @ X1))) & ! [X3 : syrup > beverage] : ($true = (hot @ (heated_mix @ X3))) & ! [X2 : syrup > beverage] : (coffee = (heated_mix @ X2)) & (heated_mix = (^[Y0 : syrup > beverage]: (heat @ (mix @ Y0)))))), inference(rectify,[status(thm)],[f6])). thf(f6,plain,( ~(~? [X0 : syrup > beverage] : ~? [X1 : syrup] : (($true = (hot @ (X0 @ X1))) & (coffee = (X0 @ X1))) & (heated_mix = (^[Y0 : syrup > beverage]: (heat @ (mix @ Y0)))) & ! [X3 : syrup > beverage] : (coffee = (heated_mix @ X3)) & ! [X4 : syrup > beverage] : ($true = (hot @ (heated_mix @ X4))))), inference(fool_elimination,[status(thm)],[f5])). thf(f5,plain,( ~(~? [X0 : syrup > beverage] : ~? [X1 : syrup] : ((coffee = (X0 @ X1)) & (hot @ (X0 @ X1))) & (heated_mix = (^[X2 : syrup > beverage] : (heat @ (mix @ X2)))) & ! [X3 : syrup > beverage] : (coffee = (heated_mix @ X3)) & ! [X4 : syrup > beverage] : (hot @ (heated_mix @ X4)))), inference(rectify,[status(thm)],[f3])). thf(f3,negated_conjecture,( ~(~? [X9 : syrup > beverage] : ~? [X4 : syrup] : ((coffee = (X9 @ X4)) & (hot @ (X9 @ X4))) & (heated_mix = (^[X8 : syrup > beverage] : (heat @ (mix @ X8)))) & ! [X8 : syrup > beverage] : (coffee = (heated_mix @ X8)) & ! [X8 : syrup > beverage] : (hot @ (heated_mix @ X8)))), inference(negated_conjecture,[status(cth)],[f2])). thf(f2,conjecture,( ~? [X9 : syrup > beverage] : ~? [X4 : syrup] : ((coffee = (X9 @ X4)) & (hot @ (X9 @ X4))) & (heated_mix = (^[X8 : syrup > beverage] : (heat @ (mix @ X8)))) & ! [X8 : syrup > beverage] : (coffee = (heated_mix @ X8)) & ! [X8 : syrup > beverage] : (hot @ (heated_mix @ X8))), file('/tmp/tmp.1gVJCcgpU5/Vampire_2428107.p',verify)). % SZS output end Proof for Vampire_2428107 % (2428145)------------------------------ % (2428145)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100) % (2428145)Termination reason: Refutation % (2428145)Memory used [KB]: 5628 % (2428145)Time elapsed: 0.003 s % (2428145)------------------------------ % (2428145)------------------------------ % (2428140)Success in time 0.017 s % Vampire exiting % END OF SYSTEM OUTPUT RESULT: THF_Finite.s - Vampire---5.0 says Theorem - CPU = 0.02 WC = 0.11 OUTPUT: THF_Finite.s - Vampire---5.0 says Refutation - CPU = 0.02 WC = 0.12