89033f975314284d642808fdfc2ae678ef272f54Alexis Tsogiasthf(con,conjecture,( mvalid @ ( mbox @ fool @ ^ [X: $i] : ! [Z: reg,Y: reg] : ( ( ( p @ Z @ spain ) & ( p @ Y @ france ) ) => ~ ( o @ Z @ Y ) ) ) )).
89033f975314284d642808fdfc2ae678ef272f54Alexis Tsogias%thf(t_axiom_for_fool,axiom,( mvalid @ ( mforall_prop @ ^ [A: $i > $o] : ( mimplies @ ( mbox @ fool @ A ) @ A ) ) )).
89033f975314284d642808fdfc2ae678ef272f54Alexis TsogiasTPTP_THF_Annotated_Formula {
89033f975314284d642808fdfc2ae678ef272f54Alexis Tsogias ttaf_name = N_Atomic_Word "t_axiom_for_fool",
89033f975314284d642808fdfc2ae678ef272f54Alexis Tsogias ttaf_formula_role = Axiom,
89033f975314284d642808fdfc2ae678ef272f54Alexis Tsogias ttaf_thf_formula = TF_THF_Logic_Formula (
89033f975314284d642808fdfc2ae678ef272f54Alexis Tsogias TLF_THF_Unitary_Formula (
89033f975314284d642808fdfc2ae678ef272f54Alexis Tsogias TUF_THF_Logic_Formula (
89033f975314284d642808fdfc2ae678ef272f54Alexis Tsogias TLF_THF_Binary_Formula (
89033f975314284d642808fdfc2ae678ef272f54Alexis Tsogias TBF_THF_Binary_Tuple (
89033f975314284d642808fdfc2ae678ef272f54Alexis Tsogias TBT_THF_Apply_Formula (
89033f975314284d642808fdfc2ae678ef272f54Alexis Tsogias TApF_THF_Apply_Formula (
89033f975314284d642808fdfc2ae678ef272f54Alexis Tsogias TUF_THF_atom (
89033f975314284d642808fdfc2ae678ef272f54Alexis Tsogias T_Function_Term (
89033f975314284d642808fdfc2ae678ef272f54Alexis Tsogias FT_Plain_Term (
89033f975314284d642808fdfc2ae678ef272f54Alexis Tsogias PT_Constant "mvalid"
89033f975314284d642808fdfc2ae678ef272f54Alexis Tsogias ) [TUF_THF_Logic_Formula (
89033f975314284d642808fdfc2ae678ef272f54Alexis Tsogias TLF_THF_Binary_Formula (
89033f975314284d642808fdfc2ae678ef272f54Alexis Tsogias TBF_THF_Binary_Tuple (
89033f975314284d642808fdfc2ae678ef272f54Alexis Tsogias TBT_THF_Apply_Formula (
89033f975314284d642808fdfc2ae678ef272f54Alexis Tsogias TApF_THF_Apply_Formula (
89033f975314284d642808fdfc2ae678ef272f54Alexis Tsogias TUF_THF_atom (
89033f975314284d642808fdfc2ae678ef272f54Alexis Tsogias T_Function_Term (
89033f975314284d642808fdfc2ae678ef272f54Alexis Tsogias FT_Plain_Term (
89033f975314284d642808fdfc2ae678ef272f54Alexis Tsogias PT_Constant "mforall_prop"
89033f975314284d642808fdfc2ae678ef272f54Alexis Tsogias ) [TUF_THF_Quantified_Formula
89033f975314284d642808fdfc2ae678ef272f54Alexis Tsogias (TQF_THF_Quantified_Formula {
89033f975314284d642808fdfc2ae678ef272f54Alexis Tsogias thf_quantifier = Lambda_Binder,
89033f975314284d642808fdfc2ae678ef272f54Alexis Tsogias thf_variable_list = [TV_THF_Typed_Variable (
89033f975314284d642808fdfc2ae678ef272f54Alexis Tsogias TTV_THF_Typed_Variable {
89033f975314284d642808fdfc2ae678ef272f54Alexis Tsogias ttv_variable = "A",
89033f975314284d642808fdfc2ae678ef272f54Alexis Tsogias ttv_thf_top_level_type = TLF_THF_Binary_Formula (
89033f975314284d642808fdfc2ae678ef272f54Alexis Tsogias TBF_THF_Binary_Type (
89033f975314284d642808fdfc2ae678ef272f54Alexis Tsogias TBT_THF_Mapping_Type (
89033f975314284d642808fdfc2ae678ef272f54Alexis Tsogias TMT_THF_Mapping_Type (
89033f975314284d642808fdfc2ae678ef272f54Alexis Tsogias TUF_THF_atom (
89033f975314284d642808fdfc2ae678ef272f54Alexis Tsogias TA_Defined_Type DT_i
89033f975314284d642808fdfc2ae678ef272f54Alexis Tsogias ) [TUF_THF_atom (
89033f975314284d642808fdfc2ae678ef272f54Alexis Tsogias TA_Defined_Type DT_o
89033f975314284d642808fdfc2ae678ef272f54Alexis Tsogias thf_unitary_formula = TUF_THF_Logic_Formula (
89033f975314284d642808fdfc2ae678ef272f54Alexis Tsogias TLF_THF_Binary_Formula (
89033f975314284d642808fdfc2ae678ef272f54Alexis Tsogias TBF_THF_Binary_Tuple (
89033f975314284d642808fdfc2ae678ef272f54Alexis Tsogias TBT_THF_Apply_Formula (
89033f975314284d642808fdfc2ae678ef272f54Alexis Tsogias TApF_THF_Apply_Formula (
89033f975314284d642808fdfc2ae678ef272f54Alexis Tsogias TUF_THF_atom (
89033f975314284d642808fdfc2ae678ef272f54Alexis Tsogias T_Function_Term (
89033f975314284d642808fdfc2ae678ef272f54Alexis Tsogias FT_Plain_Term (
89033f975314284d642808fdfc2ae678ef272f54Alexis Tsogias PT_Constant "mimplies"
89033f975314284d642808fdfc2ae678ef272f54Alexis Tsogias ) [TUF_THF_Logic_Formula (
89033f975314284d642808fdfc2ae678ef272f54Alexis Tsogias TLF_THF_Binary_Formula (
89033f975314284d642808fdfc2ae678ef272f54Alexis Tsogias TBF_THF_Binary_Tuple (
89033f975314284d642808fdfc2ae678ef272f54Alexis Tsogias TBT_THF_Apply_Formula (
89033f975314284d642808fdfc2ae678ef272f54Alexis Tsogias TApF_THF_Apply_Formula (
89033f975314284d642808fdfc2ae678ef272f54Alexis Tsogias TUF_THF_atom (
89033f975314284d642808fdfc2ae678ef272f54Alexis Tsogias T_Function_Term (
89033f975314284d642808fdfc2ae678ef272f54Alexis Tsogias FT_Plain_Term (
89033f975314284d642808fdfc2ae678ef272f54Alexis Tsogias PT_Constant "mbox"
89033f975314284d642808fdfc2ae678ef272f54Alexis Tsogias ) [TUF_THF_atom (
89033f975314284d642808fdfc2ae678ef272f54Alexis Tsogias T_Function_Term (
89033f975314284d642808fdfc2ae678ef272f54Alexis Tsogias FT_Plain_Term (
89033f975314284d642808fdfc2ae678ef272f54Alexis Tsogias PT_Constant "fool"
89033f975314284d642808fdfc2ae678ef272f54Alexis Tsogias TUF_THF_atom (
89033f975314284d642808fdfc2ae678ef272f54Alexis Tsogias T_Variable "A"
89033f975314284d642808fdfc2ae678ef272f54Alexis Tsogias TUF_THF_atom (
89033f975314284d642808fdfc2ae678ef272f54Alexis Tsogias T_Variable "A"
89033f975314284d642808fdfc2ae678ef272f54Alexis Tsogias ttaf_annotations = Null