%------------------------------------------------------------------------------ % File : PUZ149:1 : TPTP v9.0.0. Released v9.0.0. % Domain : Puzzles % Problem : The Bungling Chemist % Version : Especial. % English : Assume that a chemical compound c is made by pouring the elements % a and b into the same beaker. The two elements a and b are not % acid. It is possible that after making the compound c it results % acid. Then it is possible that pouring element a results not acid % and pouring a and b in the beaker results acid % Refs : [Bal98] Baldoni (1998), Normal Multimodal Logics: Automatic De % Source : [TPTP] % Names : % Status : Theorem % Rating : ? v9.0.0 % Syntax : TBA % SPC : THN_THM_NEQ % Comments : Long connectives %------------------------------------------------------------------------------ thf(simple_s5,logic,( \$alethic_modal == [ \$constants == \$rigid, \$quantification == \$cumulative, \$modalities == \$modal_system_S5 ] )). thf(acid_type,type,acid: \$o). thf(pour_ab_make_axiom_1,axiom,( ( ( {\$necessary(#pour_a)} @ ( {\$necessary(#pour_b)} @ acid ) ) => ( {\$necessary(#make_c)} @ acid ) ) )). thf(pour_ab_make_axiom_2,axiom,( ( ( {\$necessary(#pour_a)} @ ( {\$necessary(#pour_b)} @ (~ acid) ) ) => ( {\$necessary(#make_c)} @ (~ acid) ) ) )). thf(pour_ba_make_axiom_1,axiom,( ( ( {\$necessary(#pour_b)} @ ( {\$necessary(#pour_a)} @ acid ) ) => ( {\$necessary(#make_c)} @ acid ) ) )). thf(pour_ba_make_axiom_2,axiom,( ( ( {\$necessary(#pour_b)} @ ( {\$necessary(#pour_a)} @ (~ acid) ) ) => ( {\$necessary(#make_c)} @ (~ acid) ) ) )). thf(pour_a_not_acid,axiom,( {\$necessary(#pour_a)} @ (~ acid) )). thf(pour_b_not_acid,axiom,( {\$necessary(#pour_b)} @ (~ acid) )). thf(make_c_acid,axiom,( {\$possible(#make_c)} @ (acid) )). thf(possible_acid,conjecture,( ( ( {\$possible(#pour_a)} @ (~ acid) ) & ( {\$possible(#pour_a)} @ ( {\$possible(#pour_b)} @ acid ) ) ) )). %------------------------------------------------------------------------------