% SZS status Theorem for Vampire---4 % SZS output start Proof for Vampire---4 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, mix: beverage > syrup > beverage). thf(func_def_4, type, heat: beverage > beverage). thf(func_def_5, type, heated_mix: beverage > syrup > beverage). thf(func_def_6, type, hot: beverage > \$o). thf(func_def_7, type, d_beverage: \$tType). thf(func_def_8, type, d_syrup: \$tType). thf(func_def_9, type, d2beverage: d_beverage > beverage). thf(func_def_10, type, d2syrup: d_syrup > syrup). thf(func_def_11, type, d_coffee: d_beverage). thf(func_def_12, type, d_date: d_syrup). thf(func_def_19, type, sK0: syrup). thf(func_def_20, type, sK1: beverage). thf(func_def_21, type, sK2: syrup). thf(func_def_22, type, sK3: syrup > beverage). thf(func_def_23, type, sK4: syrup > d_syrup). thf(func_def_24, type, sK5: beverage > d_beverage). thf(func_def_26, type, inv_d2beverage_7: beverage > d_beverage). thf(func_def_27, type, inv_d2syrup_8: syrup > d_syrup). thf(func_def_28, type, ph9: !>[X0: \$tType]:(X0)). thf(func_def_29, type, sK10: beverage). thf(func_def_30, type, sK11: syrup). thf(f144,plain,( \$false), inference(avatar_sat_refutation,[],[f45,f50,f138,f140,f143])). thf(f143,plain,( ~spl6_2), inference(avatar_contradiction_clause,[],[f142])). thf(f142,plain,( \$false | ~spl6_2), inference(subsumption_resolution,[],[f141,f84])). thf(f84,plain,( ( ! [X0 : beverage] : ((\$true = (hot @ X0))) )), inference(superposition,[],[f29,f59])). thf(f59,plain,( ( ! [X0 : beverage,X1 : beverage] : ((X0 = X1)) )), inference(superposition,[],[f46,f46])). thf(f46,plain,( ( ! [X7 : beverage] : (((d2beverage @ d_coffee) = X7)) )), inference(backward_demodulation,[],[f21,f20])). thf(f20,plain,( ( ! [X9 : d_beverage] : ((d_coffee = X9)) )), inference(cnf_transformation,[],[f18])). thf(f18,plain,( ((hot @ (d2beverage @ d_coffee)) = \$true) & ((d2beverage @ d_coffee) = (heated_mix @ (d2beverage @ d_coffee) @ (d2syrup @ d_date))) & ((d2beverage @ d_coffee) = (heat @ (d2beverage @ d_coffee))) & ((d2beverage @ d_coffee) = (mix @ (d2beverage @ d_coffee) @ (d2syrup @ d_date))) & ! [X0 : d_syrup] : (d_date = X0) & ! [X1 : syrup] : ((d2syrup @ (sK4 @ X1)) = X1) & ! [X3 : d_syrup,X4 : d_syrup] : ((X3 = X4) | ((d2syrup @ X3) != (d2syrup @ X4))) & ! [X5 : d_beverage,X6 : d_beverage] : (((d2beverage @ X5) != (d2beverage @ X6)) | (X5 = X6)) & ! [X7 : beverage] : ((d2beverage @ (sK5 @ X7)) = X7) & ! [X9 : d_beverage] : (d_coffee = X9)), inference(skolemisation,[status(esa),new_symbols(skolem,[sK4,sK5])],[f15,f17,f16])). thf(f16,plain,( ! [X1 : syrup] : (? [X2 : d_syrup] : ((d2syrup @ X2) = X1) => ((d2syrup @ (sK4 @ X1)) = X1))), introduced(choice_axiom,[])). thf(f17,plain,( ! [X7 : beverage] : (? [X8 : d_beverage] : ((d2beverage @ X8) = X7) => ((d2beverage @ (sK5 @ X7)) = X7))), introduced(choice_axiom,[])). thf(f15,plain,( ((hot @ (d2beverage @ d_coffee)) = \$true) & ((d2beverage @ d_coffee) = (heated_mix @ (d2beverage @ d_coffee) @ (d2syrup @ d_date))) & ((d2beverage @ d_coffee) = (heat @ (d2beverage @ d_coffee))) & ((d2beverage @ d_coffee) = (mix @ (d2beverage @ d_coffee) @ (d2syrup @ d_date))) & ! [X0 : d_syrup] : (d_date = X0) & ! [X1 : syrup] : ? [X2 : d_syrup] : ((d2syrup @ X2) = X1) & ! [X3 : d_syrup,X4 : d_syrup] : ((X3 = X4) | ((d2syrup @ X3) != (d2syrup @ X4))) & ! [X5 : d_beverage,X6 : d_beverage] : (((d2beverage @ X5) != (d2beverage @ X6)) | (X5 = X6)) & ! [X7 : beverage] : ? [X8 : d_beverage] : ((d2beverage @ X8) = X7) & ! [X9 : d_beverage] : (d_coffee = X9)), inference(rectify,[],[f10])). thf(f10,plain,( ((hot @ (d2beverage @ d_coffee)) = \$true) & ((d2beverage @ d_coffee) = (heated_mix @ (d2beverage @ d_coffee) @ (d2syrup @ d_date))) & ((d2beverage @ d_coffee) = (heat @ (d2beverage @ d_coffee))) & ((d2beverage @ d_coffee) = (mix @ (d2beverage @ d_coffee) @ (d2syrup @ d_date))) & ! [X0 : d_syrup] : (d_date = X0) & ! [X1 : syrup] : ? [X2 : d_syrup] : ((d2syrup @ X2) = X1) & ! [X8 : d_syrup,X9 : d_syrup] : ((X8 = X9) | ((d2syrup @ X9) != (d2syrup @ X8))) & ! [X5 : d_beverage,X6 : d_beverage] : (((d2beverage @ X5) != (d2beverage @ X6)) | (X5 = X6)) & ! [X3 : beverage] : ? [X4 : d_beverage] : ((d2beverage @ X4) = X3) & ! [X7 : d_beverage] : (d_coffee = X7)), inference(ennf_transformation,[],[f6])). thf(f6,plain,( ! [X5 : d_beverage,X6 : d_beverage] : (((d2beverage @ X5) = (d2beverage @ X6)) => (X5 = X6)) & ! [X0 : d_syrup] : (d_date = X0) & ! [X8 : d_syrup,X9 : d_syrup] : (((d2syrup @ X9) = (d2syrup @ X8)) => (X8 = X9)) & ((d2beverage @ d_coffee) = (heated_mix @ (d2beverage @ d_coffee) @ (d2syrup @ d_date))) & ! [X1 : syrup] : ? [X2 : d_syrup] : ((d2syrup @ X2) = X1) & ((hot @ (d2beverage @ d_coffee)) = \$true) & ! [X7 : d_beverage] : (d_coffee = X7) & ((d2beverage @ d_coffee) = (mix @ (d2beverage @ d_coffee) @ (d2syrup @ d_date))) & ((d2beverage @ d_coffee) = (heat @ (d2beverage @ d_coffee))) & ! [X3 : beverage] : ? [X4 : d_beverage] : ((d2beverage @ X4) = X3)), inference(fool_elimination,[],[f5])). thf(f5,plain,( (hot @ (d2beverage @ d_coffee)) & ((d2beverage @ d_coffee) = (mix @ (d2beverage @ d_coffee) @ (d2syrup @ d_date))) & ! [X0 : d_syrup] : (d_date = X0) & ! [X1 : syrup] : ? [X2 : d_syrup] : ((d2syrup @ X2) = X1) & ((d2beverage @ d_coffee) = (heat @ (d2beverage @ d_coffee))) & ((d2beverage @ d_coffee) = (heated_mix @ (d2beverage @ d_coffee) @ (d2syrup @ d_date))) & ! [X3 : beverage] : ? [X4 : d_beverage] : ((d2beverage @ X4) = X3) & ! [X5 : d_beverage,X6 : d_beverage] : (((d2beverage @ X5) = (d2beverage @ X6)) => (X5 = X6)) & ! [X7 : d_beverage] : (d_coffee = X7) & ! [X8 : d_syrup,X9 : d_syrup] : (((d2syrup @ X9) = (d2syrup @ X8)) => (X8 = X9))), inference(rectify,[],[f1])). thf(f1,axiom,( (hot @ (d2beverage @ d_coffee)) & ((d2beverage @ d_coffee) = (mix @ (d2beverage @ d_coffee) @ (d2syrup @ d_date))) & ! [X5 : d_syrup] : (d_date = X5) & ! [X4 : syrup] : ? [X5 : d_syrup] : ((d2syrup @ X5) = X4) & ((d2beverage @ d_coffee) = (heat @ (d2beverage @ d_coffee))) & ((d2beverage @ d_coffee) = (heated_mix @ (d2beverage @ d_coffee) @ (d2syrup @ d_date))) & ! [X0 : beverage] : ? [X1 : d_beverage] : ((d2beverage @ X1) = X0) & ! [X3 : d_beverage,X2 : d_beverage] : (((d2beverage @ X2) = (d2beverage @ X3)) => (X2 = X3)) & ! [X1 : d_beverage] : (d_coffee = X1) & ! [X6 : d_syrup,X7 : d_syrup] : (((d2syrup @ X6) = (d2syrup @ X7)) => (X6 = X7))), file('/tmp/tmp.55zkt07uQX/Vampire---4.8_7177',hot_coffee)). thf(f21,plain,( ( ! [X7 : beverage] : (((d2beverage @ (sK5 @ X7)) = X7)) )), inference(cnf_transformation,[],[f18])). thf(f29,plain,( ((hot @ (d2beverage @ d_coffee)) = \$true)), inference(cnf_transformation,[],[f18])). thf(f141,plain,( ( ! [X4 : syrup] : ((\$true != (hot @ (sK3 @ X4)))) ) | ~spl6_2), inference(subsumption_resolution,[],[f36,f59])). thf(f36,plain,( ( ! [X4 : syrup] : ((coffee != (sK3 @ X4)) | (\$true != (hot @ (sK3 @ X4)))) ) | ~spl6_2), inference(avatar_component_clause,[],[f35])). thf(f35,plain,( spl6_2 <=> ! [X4 : syrup] : ((coffee != (sK3 @ X4)) | (\$true != (hot @ (sK3 @ X4))))), introduced(avatar_definition,[new_symbols(naming,[spl6_2])])). thf(f140,plain,( spl6_4), inference(avatar_contradiction_clause,[],[f139])). thf(f139,plain,( \$false | spl6_4), inference(subsumption_resolution,[],[f44,f59])). thf(f44,plain,( (coffee != (heated_mix @ coffee @ sK2)) | spl6_4), inference(avatar_component_clause,[],[f42])). thf(f42,plain,( spl6_4 <=> (coffee = (heated_mix @ coffee @ sK2))), introduced(avatar_definition,[new_symbols(naming,[spl6_4])])). thf(f138,plain,( spl6_3), inference(avatar_contradiction_clause,[],[f137])). thf(f137,plain,( \$false | spl6_3), inference(subsumption_resolution,[],[f136,f59])). thf(f136,plain,( ((heat @ (mix @ sK10 @ sK11)) != (heated_mix @ sK10 @ sK11)) | spl6_3), inference(beta_eta_normalization,[],[f135])). thf(f135,plain,( (((^[Y0 : syrup]: (heat @ (mix @ sK10 @ Y0))) @ sK11) != (heated_mix @ sK10 @ sK11)) | spl6_3), inference(negative_extensionality,[],[f134])). thf(f134,plain,( ((heated_mix @ sK10) != (^[Y0 : syrup]: (heat @ (mix @ sK10 @ Y0)))) | spl6_3), inference(beta_eta_normalization,[],[f133])). thf(f133,plain,( ((heated_mix @ sK10) != ((^[Y0 : beverage]: ((^[Y1 : syrup]: (heat @ (mix @ Y0 @ Y1))))) @ sK10)) | spl6_3), inference(negative_extensionality,[],[f40])). thf(f40,plain,( (heated_mix != (^[Y0 : beverage]: ((^[Y1 : syrup]: (heat @ (mix @ Y0 @ Y1)))))) | spl6_3), inference(avatar_component_clause,[],[f38])). thf(f38,plain,( spl6_3 <=> (heated_mix = (^[Y0 : beverage]: ((^[Y1 : syrup]: (heat @ (mix @ Y0 @ Y1))))))), introduced(avatar_definition,[new_symbols(naming,[spl6_3])])). thf(f50,plain,( spl6_1), inference(avatar_contradiction_clause,[],[f49])). thf(f49,plain,( \$false | spl6_1), inference(subsumption_resolution,[],[f48,f29])). thf(f48,plain,( ((hot @ (d2beverage @ d_coffee)) != \$true) | spl6_1), inference(forward_demodulation,[],[f33,f46])). thf(f33,plain,( ((hot @ (heated_mix @ sK1 @ sK0)) != \$true) | spl6_1), inference(avatar_component_clause,[],[f31])). thf(f31,plain,( spl6_1 <=> ((hot @ (heated_mix @ sK1 @ sK0)) = \$true)), introduced(avatar_definition,[new_symbols(naming,[spl6_1])])). thf(f45,plain,( ~spl6_1 | spl6_2 | ~spl6_3 | ~spl6_4), inference(avatar_split_clause,[],[f19,f42,f38,f35,f31])). thf(f19,plain,( ( ! [X4 : syrup] : ((coffee != (sK3 @ X4)) | (coffee != (heated_mix @ coffee @ sK2)) | (heated_mix != (^[Y0 : beverage]: ((^[Y1 : syrup]: (heat @ (mix @ Y0 @ Y1)))))) | ((hot @ (heated_mix @ sK1 @ sK0)) != \$true) | (\$true != (hot @ (sK3 @ X4)))) )), inference(cnf_transformation,[],[f14])). thf(f14,plain,( (heated_mix != (^[Y0 : beverage]: ((^[Y1 : syrup]: (heat @ (mix @ Y0 @ Y1)))))) | ((hot @ (heated_mix @ sK1 @ sK0)) != \$true) | (coffee != (heated_mix @ coffee @ sK2)) | ! [X4 : syrup] : ((coffee != (sK3 @ X4)) | (\$true != (hot @ (sK3 @ X4))))), inference(skolemisation,[status(esa),new_symbols(skolem,[sK0,sK1,sK2,sK3])],[f9,f13,f12,f11])). thf(f11,plain,( ? [X0 : syrup,X1 : beverage] : ((hot @ (heated_mix @ X1 @ X0)) != \$true) => ((hot @ (heated_mix @ sK1 @ sK0)) != \$true)), introduced(choice_axiom,[])). thf(f12,plain,( ? [X2 : syrup] : (coffee != (heated_mix @ coffee @ X2)) => (coffee != (heated_mix @ coffee @ sK2))), introduced(choice_axiom,[])). thf(f13,plain,( ? [X3 : syrup > beverage] : ! [X4 : syrup] : ((coffee != (X3 @ X4)) | (\$true != (hot @ (X3 @ X4)))) => ! [X4 : syrup] : ((coffee != (sK3 @ X4)) | (\$true != (hot @ (sK3 @ X4))))), introduced(choice_axiom,[])). thf(f9,plain,( (heated_mix != (^[Y0 : beverage]: ((^[Y1 : syrup]: (heat @ (mix @ Y0 @ Y1)))))) | ? [X0 : syrup,X1 : beverage] : ((hot @ (heated_mix @ X1 @ X0)) != \$true) | ? [X2 : syrup] : (coffee != (heated_mix @ coffee @ X2)) | ? [X3 : syrup > beverage] : ! [X4 : syrup] : ((coffee != (X3 @ X4)) | (\$true != (hot @ (X3 @ X4))))), inference(ennf_transformation,[],[f8])). thf(f8,plain,( ~(! [X2 : syrup] : (coffee = (heated_mix @ coffee @ X2)) & ! [X0 : syrup,X1 : beverage] : ((hot @ (heated_mix @ X1 @ X0)) = \$true) & ~? [X3 : syrup > beverage] : ~? [X4 : syrup] : ((coffee = (X3 @ X4)) & (\$true = (hot @ (X3 @ X4)))) & (heated_mix = (^[Y0 : beverage]: ((^[Y1 : syrup]: (heat @ (mix @ Y0 @ Y1)))))))), inference(fool_elimination,[],[f7])). thf(f7,plain,( ~(! [X0 : syrup,X1 : beverage] : (hot @ (heated_mix @ X1 @ X0)) & ! [X2 : syrup] : (coffee = (heated_mix @ coffee @ X2)) & ~? [X3 : syrup > beverage] : ~? [X4 : syrup] : ((hot @ (X3 @ X4)) & (coffee = (X3 @ X4))) & (heated_mix = (^[X5 : beverage, X6 : syrup] : (heat @ (mix @ X5 @ X6)))))), inference(rectify,[],[f3])). thf(f3,negated_conjecture,( ~(! [X4 : syrup,X0 : beverage] : (hot @ (heated_mix @ X0 @ X4)) & ! [X4 : syrup] : (coffee = (heated_mix @ coffee @ X4)) & ~? [X8 : syrup > beverage] : ~? [X4 : syrup] : ((hot @ (X8 @ X4)) & (coffee = (X8 @ X4))) & (heated_mix = (^[X0 : beverage, X4 : syrup] : (heat @ (mix @ X0 @ X4)))))), inference(negated_conjecture,[],[f2])). thf(f2,conjecture,( ! [X4 : syrup,X0 : beverage] : (hot @ (heated_mix @ X0 @ X4)) & ! [X4 : syrup] : (coffee = (heated_mix @ coffee @ X4)) & ~? [X8 : syrup > beverage] : ~? [X4 : syrup] : ((hot @ (X8 @ X4)) & (coffee = (X8 @ X4))) & (heated_mix = (^[X0 : beverage, X4 : syrup] : (heat @ (mix @ X0 @ X4))))), file('/tmp/tmp.55zkt07uQX/Vampire---4.8_7177',verify)). % SZS output end Proof for Vampire---4