1 files changed, 41 insertions, 54 deletions

diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/output/FAMTest/vampireProblem.tptp b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/output/FAMTest/vampireProblem.tptp
index 242c404c..1f220d6f 100644
--- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/output/FAMTest/vampireProblem.tptp
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/output/FAMTest/vampireProblem.tptp
@@ -1,55 +1,42 @@
 % This is an initial Test Comment

-fof ( typeDef_FunctionType_enum , axiom , ! [ A ] : ( type_FunctionType_enum ( A ) <=> ( A = "aRoot literal FunctionType" | ( A = "aIntermediate literal FunctionType" | A = "aLeaf literal FunctionType" ) ) ) ) .

-fof ( typeDef_FunctionalArchitectureModel_class_DefinedPart , axiom , ! [ A ] : ( type_FunctionalArchitectureModel_class_DefinedPart ( A ) <=> A = "ao 1" ) ) .

-fof ( hierarchyHandler , axiom , ! [ A ] : ( object ( A ) <=> ( ( type_FunctionType_enum ( A ) & ( ~ type_FunctionalData_class ( A ) & ( ~ type_Function_class ( A ) & ( ~ type_InformationLink_class ( A ) & ( ~ type_FunctionalOutput_class ( A ) & ( ~ type_FunctionalArchitectureModel_class ( A ) & ( ~ type_FunctionalElement_class ( A ) & ( ~ type_FunctionalArchitectureModel_class_DefinedPart ( A ) & ( ~ type_FAMTerminator_class ( A ) & ( ~ type_FunctionalArchitectureModel_class_UndefinedPart ( A ) & ( ~ type_FunctionalInput_class ( A ) & ~ type_FunctionalInterface_class ( A ) ) ) ) ) ) ) ) ) ) ) ) | ( ( ~ type_FunctionType_enum ( A ) & ( ~ type_FunctionalData_class ( A ) & ( type_Function_class ( A ) & ( ~ type_InformationLink_class ( A ) & ( ~ type_FunctionalOutput_class ( A ) & ( ~ type_FunctionalArchitectureModel_class ( A ) & ( type_FunctionalElement_class ( A ) & ( ~ type_FunctionalArchitectureModel_class_DefinedPart ( A ) & ( ~ type_FAMTerminator_class ( A ) & ( ~ type_FunctionalArchitectureModel_class_UndefinedPart ( A ) & ( ~ type_FunctionalInput_class ( A ) & ~ type_FunctionalInterface_class ( A ) ) ) ) ) ) ) ) ) ) ) ) | ( ( ~ type_FunctionType_enum ( A ) & ( ~ type_FunctionalData_class ( A ) & ( ~ type_Function_class ( A ) & ( type_InformationLink_class ( A ) & ( ~ type_FunctionalOutput_class ( A ) & ( ~ type_FunctionalArchitectureModel_class ( A ) & ( ~ type_FunctionalElement_class ( A ) & ( ~ type_FunctionalArchitectureModel_class_DefinedPart ( A ) & ( ~ type_FAMTerminator_class ( A ) & ( ~ type_FunctionalArchitectureModel_class_UndefinedPart ( A ) & ( ~ type_FunctionalInput_class ( A ) & ~ type_FunctionalInterface_class ( A ) ) ) ) ) ) ) ) ) ) ) ) | ( ( ~ type_FunctionType_enum ( A ) & ( type_FunctionalData_class ( A ) & ( ~ type_Function_class ( A ) & ( ~ type_InformationLink_class ( A ) & ( type_FunctionalOutput_class ( A ) & ( ~ type_FunctionalArchitectureModel_class ( A ) & ( ~ type_FunctionalElement_class ( A ) & ( ~ type_FunctionalArchitectureModel_class_DefinedPart ( A ) & ( ~ type_FAMTerminator_class ( A ) & ( ~ type_FunctionalArchitectureModel_class_UndefinedPart ( A ) & ( ~ type_FunctionalInput_class ( A ) & ~ type_FunctionalInterface_class ( A ) ) ) ) ) ) ) ) ) ) ) ) | ( ( ~ type_FunctionType_enum ( A ) & ( ~ type_FunctionalData_class ( A ) & ( ~ type_Function_class ( A ) & ( ~ type_InformationLink_class ( A ) & ( ~ type_FunctionalOutput_class ( A ) & ( type_FunctionalArchitectureModel_class ( A ) & ( ~ type_FunctionalElement_class ( A ) & ( type_FunctionalArchitectureModel_class_DefinedPart ( A ) & ( ~ type_FAMTerminator_class ( A ) & ( ~ type_FunctionalArchitectureModel_class_UndefinedPart ( A ) & ( ~ type_FunctionalInput_class ( A ) & ~ type_FunctionalInterface_class ( A ) ) ) ) ) ) ) ) ) ) ) ) | ( ( ~ type_FunctionType_enum ( A ) & ( ~ type_FunctionalData_class ( A ) & ( ~ type_Function_class ( A ) & ( ~ type_InformationLink_class ( A ) & ( ~ type_FunctionalOutput_class ( A ) & ( ~ type_FunctionalArchitectureModel_class ( A ) & ( ~ type_FunctionalElement_class ( A ) & ( ~ type_FunctionalArchitectureModel_class_DefinedPart ( A ) & ( type_FAMTerminator_class ( A ) & ( ~ type_FunctionalArchitectureModel_class_UndefinedPart ( A ) & ( ~ type_FunctionalInput_class ( A ) & ~ type_FunctionalInterface_class ( A ) ) ) ) ) ) ) ) ) ) ) ) | ( ( ~ type_FunctionType_enum ( A ) & ( ~ type_FunctionalData_class ( A ) & ( ~ type_Function_class ( A ) & ( ~ type_InformationLink_class ( A ) & ( ~ type_FunctionalOutput_class ( A ) & ( type_FunctionalArchitectureModel_class ( A ) & ( ~ type_FunctionalElement_class ( A ) & ( ~ type_FunctionalArchitectureModel_class_DefinedPart ( A ) & ( ~ type_FAMTerminator_class ( A ) & ( type_FunctionalArchitectureModel_class_UndefinedPart ( A ) & ( ~ type_FunctionalInput_class ( A ) & ~ type_FunctionalInterface_class ( A ) ) ) ) ) ) ) ) ) ) ) ) | ( ( ~ type_FunctionType_enum ( A ) & ( type_FunctionalData_class ( A ) & ( ~ type_Function_class ( A ) & ( ~ type_InformationLink_class ( A ) & ( ~ type_FunctionalOutput_class ( A ) & ( ~ type_FunctionalArchitectureModel_class ( A ) & ( ~ type_FunctionalElement_class ( A ) & ( ~ type_FunctionalArchitectureModel_class_DefinedPart ( A ) & ( ~ type_FAMTerminator_class ( A ) & ( ~ type_FunctionalArchitectureModel_class_UndefinedPart ( A ) & ( type_FunctionalInput_class ( A ) & ~ type_FunctionalInterface_class ( A ) ) ) ) ) ) ) ) ) ) ) ) | ( ~ type_FunctionType_enum ( A ) & ( ~ type_FunctionalData_class ( A ) & ( ~ type_Function_class ( A ) & ( ~ type_InformationLink_class ( A ) & ( ~ type_FunctionalOutput_class ( A ) & ( ~ type_FunctionalArchitectureModel_class ( A ) & ( ~ type_FunctionalElement_class ( A ) & ( ~ type_FunctionalArchitectureModel_class_DefinedPart ( A ) & ( ~ type_FAMTerminator_class ( A ) & ( ~ type_FunctionalArchitectureModel_class_UndefinedPart ( A ) & ( ~ type_FunctionalInput_class ( A ) & type_FunctionalInterface_class ( A ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) .

-fof ( compliance_interface_reference_FunctionalElement , axiom , ! [ Var_0 , Var_1 ] : ( rel_interface_reference_FunctionalElement ( Var_0 , Var_1 ) => ( type_FunctionalElement_class ( Var_0 ) & type_FunctionalInterface_class ( Var_1 ) ) ) ) .

-fof ( compliance_model_reference_FunctionalElement , axiom , ! [ Var_0 , Var_1 ] : ( rel_model_reference_FunctionalElement ( Var_0 , Var_1 ) => ( type_FunctionalElement_class ( Var_0 ) & type_FunctionalArchitectureModel_class ( Var_1 ) ) ) ) .

-fof ( compliance_parent_reference_FunctionalElement , axiom , ! [ Var_0 , Var_1 ] : ( rel_parent_reference_FunctionalElement ( Var_0 , Var_1 ) => ( type_FunctionalElement_class ( Var_0 ) & type_Function_class ( Var_1 ) ) ) ) .

-fof ( compliance_rootElements_reference_FunctionalArchitectureModel , axiom , ! [ Var_0 , Var_1 ] : ( rel_rootElements_reference_FunctionalArchitectureModel ( Var_0 , Var_1 ) => ( type_FunctionalArchitectureModel_class ( Var_0 ) & type_FunctionalElement_class ( Var_1 ) ) ) ) .

-fof ( compliance_subElements_reference_Function , axiom , ! [ Var_0 , Var_1 ] : ( rel_subElements_reference_Function ( Var_0 , Var_1 ) => ( type_Function_class ( Var_0 ) & type_FunctionalElement_class ( Var_1 ) ) ) ) .

-fof ( compliance_data_reference_FAMTerminator , axiom , ! [ Var_0 , Var_1 ] : ( rel_data_reference_FAMTerminator ( Var_0 , Var_1 ) => ( type_FAMTerminator_class ( Var_0 ) & type_FunctionalData_class ( Var_1 ) ) ) ) .

-fof ( compliance_from_reference_InformationLink , axiom , ! [ Var_0 , Var_1 ] : ( rel_from_reference_InformationLink ( Var_0 , Var_1 ) => ( type_InformationLink_class ( Var_0 ) & type_FunctionalOutput_class ( Var_1 ) ) ) ) .

-fof ( compliance_to_reference_InformationLink , axiom , ! [ Var_0 , Var_1 ] : ( rel_to_reference_InformationLink ( Var_0 , Var_1 ) => ( type_InformationLink_class ( Var_0 ) & type_FunctionalInput_class ( Var_1 ) ) ) ) .

-fof ( compliance_data_reference_FunctionalInterface , axiom , ! [ Var_0 , Var_1 ] : ( rel_data_reference_FunctionalInterface ( Var_0 , Var_1 ) => ( type_FunctionalInterface_class ( Var_0 ) & type_FunctionalData_class ( Var_1 ) ) ) ) .

-fof ( compliance_element_reference_FunctionalInterface , axiom , ! [ Var_0 , Var_1 ] : ( rel_element_reference_FunctionalInterface ( Var_0 , Var_1 ) => ( type_FunctionalInterface_class ( Var_0 ) & type_FunctionalElement_class ( Var_1 ) ) ) ) .

-fof ( compliance_IncomingLinks_reference_FunctionalInput , axiom , ! [ Var_0 , Var_1 ] : ( rel_IncomingLinks_reference_FunctionalInput ( Var_0 , Var_1 ) => ( type_FunctionalInput_class ( Var_0 ) & type_InformationLink_class ( Var_1 ) ) ) ) .

-fof ( compliance_outgoingLinks_reference_FunctionalOutput , axiom , ! [ Var_0 , Var_1 ] : ( rel_outgoingLinks_reference_FunctionalOutput ( Var_0 , Var_1 ) => ( type_FunctionalOutput_class ( Var_0 ) & type_InformationLink_class ( Var_1 ) ) ) ) .

-fof ( compliance_terminator_reference_FunctionalData , axiom , ! [ Var_0 , Var_1 ] : ( rel_terminator_reference_FunctionalData ( Var_0 , Var_1 ) => ( type_FunctionalData_class ( Var_0 ) & type_FAMTerminator_class ( Var_1 ) ) ) ) .

-fof ( compliance_interface_reference_FunctionalData , axiom , ! [ Var_0 , Var_1 ] : ( rel_interface_reference_FunctionalData ( Var_0 , Var_1 ) => ( type_FunctionalData_class ( Var_0 ) & type_FunctionalInterface_class ( Var_1 ) ) ) ) .

-fof ( compliance_type_attribute_Function , axiom , ! [ Var_0 , Var_1 ] : ( rel_type_attribute_Function ( Var_0 , Var_1 ) => ( type_Function_class ( Var_0 ) & type_FunctionType_enum ( Var_1 ) ) ) ) .

-fof ( compliance_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_hasRoot , axiom , ! [ Var_parameter_F ] : ( rel_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_hasRoot ( Var_parameter_F ) => type_Function_class ( Var_parameter_F ) ) ) .

-fof ( relation_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_hasRoot , axiom , ! [ Var_parameter_F ] : ( type_Function_class ( Var_parameter_F ) => ( rel_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_hasRoot ( Var_parameter_F ) <=> ? [ Var_variable_Model ] : ( type_FunctionalArchitectureModel_class ( Var_variable_Model ) & rel_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_rootElements ( Var_variable_Model , Var_parameter_F ) ) ) ) ) .

-fof ( compliance_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_hasInt , axiom , ! [ Var_parameter_F ] : ( rel_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_hasInt ( Var_parameter_F ) => type_Function_class ( Var_parameter_F ) ) ) .

-fof ( relation_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_hasInt , axiom , ! [ Var_parameter_F ] : ( type_Function_class ( Var_parameter_F ) => ( rel_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_hasInt ( Var_parameter_F ) <=> ! [ Var_variable_Child , Var_variable_Model ] : ( ( type_Function_class ( Var_variable_Child ) & type_FunctionalArchitectureModel_class ( Var_variable_Model ) ) => ( type_Function_class ( Var_parameter_F ) & ( ~ rel_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_parent ( Var_variable_Child , Var_parameter_F ) & ~ rel_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_rootElements ( Var_variable_Model , Var_parameter_F ) ) ) ) ) ) ) .

-fof ( compliance_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_hasLeaf , axiom , ! [ Var_parameter_F ] : ( rel_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_hasLeaf ( Var_parameter_F ) => type_Function_class ( Var_parameter_F ) ) ) .

-fof ( relation_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_hasLeaf , axiom , ! [ Var_parameter_F ] : ( type_Function_class ( Var_parameter_F ) => ( rel_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_hasLeaf ( Var_parameter_F ) <=> ? [ Var_variable_Par , Var_variable_Child ] : ( type_Function_class ( Var_variable_Par ) & ( type_Function_class ( Var_variable_Child ) & ( rel_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_parent ( Var_parameter_F , Var_variable_Par ) & rel_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_parent ( Var_variable_Child , Var_parameter_F ) ) ) ) ) ) ) .

-fof ( compliance_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_model , axiom , ! [ Var_parameter_This , Var_parameter_Target ] : ( rel_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_model ( Var_parameter_This , Var_parameter_Target ) => ( type_FunctionalArchitectureModel_class ( Var_parameter_Target ) & type_FunctionalElement_class ( Var_parameter_This ) ) ) ) .

-fof ( relation_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_model , axiom , ! [ Var_parameter_This , Var_parameter_Target ] : ( ( type_FunctionalArchitectureModel_class ( Var_parameter_Target ) & type_FunctionalElement_class ( Var_parameter_This ) ) => ( rel_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_model ( Var_parameter_This , Var_parameter_Target ) <=> ( type_FunctionalElement_class ( Var_parameter_This ) & type_FunctionalArchitectureModel_class ( Var_parameter_Target ) ) ) ) ) .

-fof ( compliance_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_rootElements , axiom , ! [ Var_parameter_Model , Var_parameter_Root ] : ( rel_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_rootElements ( Var_parameter_Model , Var_parameter_Root ) => ( type_FunctionalArchitectureModel_class ( Var_parameter_Model ) & type_Function_class ( Var_parameter_Root ) ) ) ) .

-fof ( relation_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_rootElements , axiom , ! [ Var_parameter_Model , Var_parameter_Root ] : ( ( type_FunctionalArchitectureModel_class ( Var_parameter_Model ) & type_Function_class ( Var_parameter_Root ) ) => ( rel_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_rootElements ( Var_parameter_Model , Var_parameter_Root ) <=> ( type_Function_class ( Var_parameter_Root ) & rel_rootElements_reference_FunctionalArchitectureModel ( Var_parameter_Model , Var_parameter_Root ) ) ) ) ) .

-fof ( compliance_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_type , axiom , ! [ Var_parameter_This , Var_parameter_Target ] : ( rel_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_type ( Var_parameter_This , Var_parameter_Target ) => ( type_FunctionType_enum ( Var_parameter_Target ) & type_Function_class ( Var_parameter_This ) ) ) ) .

-fof ( relation_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_type , axiom , ! [ Var_parameter_This , Var_parameter_Target ] : ( ( type_FunctionType_enum ( Var_parameter_Target ) & type_Function_class ( Var_parameter_This ) ) => ( rel_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_type ( Var_parameter_This , Var_parameter_Target ) <=> ( ? [ Var_variable_Model ] : ( type_FunctionalArchitectureModel_class ( Var_variable_Model ) & ( rel_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_rootElements ( Var_variable_Model , Var_parameter_This ) & Var_parameter_Target = "aRoot literal FunctionType" ) ) | ( ! [ Var_variable_Child , Var_variable_Model ] : ( ( type_Function_class ( Var_variable_Child ) & type_FunctionalArchitectureModel_class ( Var_variable_Model ) ) => ( type_Function_class ( Var_parameter_This ) & ( ~ rel_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_parent ( Var_variable_Child , Var_parameter_This ) & ( ~ rel_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_rootElements ( Var_variable_Model , Var_parameter_This ) & Var_parameter_Target = "aLeaf literal FunctionType" ) ) ) ) | ? [ Var_variable_Par , Var_variable_Child ] : ( type_Function_class ( Var_variable_Par ) & ( type_Function_class ( Var_variable_Child ) & ( rel_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_parent ( Var_parameter_This , Var_variable_Par ) & ( rel_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_parent ( Var_variable_Child , Var_parameter_This ) & Var_parameter_Target = "aIntermediate literal FunctionType" ) ) ) ) ) ) ) ) ) .

-fof ( compliance_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_parent , axiom , ! [ Var_parameter_Func , Var_parameter_Par ] : ( rel_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_parent ( Var_parameter_Func , Var_parameter_Par ) => ( type_Function_class ( Var_parameter_Par ) & type_Function_class ( Var_parameter_Func ) ) ) ) .

-fof ( relation_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_parent , axiom , ! [ Var_parameter_Func , Var_parameter_Par ] : ( ( type_Function_class ( Var_parameter_Par ) & type_Function_class ( Var_parameter_Func ) ) => ( rel_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_parent ( Var_parameter_Func , Var_parameter_Par ) <=> ( type_Function_class ( Var_parameter_Func ) & ( rel_parent_reference_FunctionalElement ( Var_parameter_Func , Var_parameter_Par ) & type_Function_class ( Var_parameter_Par ) ) ) ) ) ) .

-fof ( compliance_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_terminatorAndInformation , axiom , ! [ Var_parameter_T , Var_parameter_I ] : ( rel_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_terminatorAndInformation ( Var_parameter_T , Var_parameter_I ) => ( type_FAMTerminator_class ( Var_parameter_T ) & type_InformationLink_class ( Var_parameter_I ) ) ) ) .

-fof ( relation_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_terminatorAndInformation , axiom , ! [ Var_parameter_T , Var_parameter_I ] : ( ( type_FAMTerminator_class ( Var_parameter_T ) & type_InformationLink_class ( Var_parameter_I ) ) => ( rel_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_terminatorAndInformation ( Var_parameter_T , Var_parameter_I ) <=> ( ? [ Var_variable_Out ] : ( type_FunctionalOutput_class ( Var_variable_Out ) & ( rel_outgoingLinks_reference_FunctionalOutput ( Var_variable_Out , Var_parameter_I ) & rel_terminator_reference_FunctionalData ( Var_variable_Out , Var_parameter_T ) ) ) | ? [ Var_variable_In ] : ( type_FunctionalInput_class ( Var_variable_In ) & ( rel_to_reference_InformationLink ( Var_parameter_I , Var_variable_In ) & ( type_FunctionalInput_class ( Var_variable_In ) & rel_terminator_reference_FunctionalData ( Var_variable_In , Var_parameter_T ) ) ) ) ) ) ) ) .

-fof ( upperMultiplicity_interface_FunctionalElement , axiom , ! [ Var_src , Var_trg_1 , Var_trg_2 ] : ( ( type_FunctionalElement_class ( Var_src ) & ( type_FunctionalInterface_class ( Var_trg_1 ) & type_FunctionalInterface_class ( Var_trg_2 ) ) ) => ( ( rel_interface_reference_FunctionalElement ( Var_src , Var_trg_1 ) & rel_interface_reference_FunctionalElement ( Var_src , Var_trg_2 ) ) => ~ Var_trg_1 != Var_trg_2 ) ) ) .

-fof ( lowerMultiplicity_model_FunctionalElement , axiom , ! [ Var_src ] : ( type_FunctionalElement_class ( Var_src ) => ? [ Var_trg_1 ] : ( type_FunctionalArchitectureModel_class ( Var_trg_1 ) & rel_model_reference_FunctionalElement ( Var_src , Var_trg_1 ) ) ) ) .

-fof ( upperMultiplicity_model_FunctionalElement , axiom , ! [ Var_src , Var_trg_1 , Var_trg_2 ] : ( ( type_FunctionalElement_class ( Var_src ) & ( type_FunctionalArchitectureModel_class ( Var_trg_1 ) & type_FunctionalArchitectureModel_class ( Var_trg_2 ) ) ) => ( ( rel_model_reference_FunctionalElement ( Var_src , Var_trg_1 ) & rel_model_reference_FunctionalElement ( Var_src , Var_trg_2 ) ) => ~ Var_trg_1 != Var_trg_2 ) ) ) .

-fof ( upperMultiplicity_parent_FunctionalElement , axiom , ! [ Var_src , Var_trg_1 , Var_trg_2 ] : ( ( type_FunctionalElement_class ( Var_src ) & ( type_Function_class ( Var_trg_1 ) & type_Function_class ( Var_trg_2 ) ) ) => ( ( rel_parent_reference_FunctionalElement ( Var_src , Var_trg_1 ) & rel_parent_reference_FunctionalElement ( Var_src , Var_trg_2 ) ) => ~ Var_trg_1 != Var_trg_2 ) ) ) .

-fof ( upperMultiplicity_data_FAMTerminator , axiom , ! [ Var_src , Var_trg_1 , Var_trg_2 ] : ( ( type_FAMTerminator_class ( Var_src ) & ( type_FunctionalData_class ( Var_trg_1 ) & type_FunctionalData_class ( Var_trg_2 ) ) ) => ( ( rel_data_reference_FAMTerminator ( Var_src , Var_trg_1 ) & rel_data_reference_FAMTerminator ( Var_src , Var_trg_2 ) ) => ~ Var_trg_1 != Var_trg_2 ) ) ) .

-fof ( upperMultiplicity_from_InformationLink , axiom , ! [ Var_src , Var_trg_1 , Var_trg_2 ] : ( ( type_InformationLink_class ( Var_src ) & ( type_FunctionalOutput_class ( Var_trg_1 ) & type_FunctionalOutput_class ( Var_trg_2 ) ) ) => ( ( rel_from_reference_InformationLink ( Var_src , Var_trg_1 ) & rel_from_reference_InformationLink ( Var_src , Var_trg_2 ) ) => ~ Var_trg_1 != Var_trg_2 ) ) ) .

-fof ( lowerMultiplicity_to_InformationLink , axiom , ! [ Var_src ] : ( type_InformationLink_class ( Var_src ) => ? [ Var_trg_1 ] : ( type_FunctionalInput_class ( Var_trg_1 ) & rel_to_reference_InformationLink ( Var_src , Var_trg_1 ) ) ) ) .

-fof ( upperMultiplicity_to_InformationLink , axiom , ! [ Var_src , Var_trg_1 , Var_trg_2 ] : ( ( type_InformationLink_class ( Var_src ) & ( type_FunctionalInput_class ( Var_trg_1 ) & type_FunctionalInput_class ( Var_trg_2 ) ) ) => ( ( rel_to_reference_InformationLink ( Var_src , Var_trg_1 ) & rel_to_reference_InformationLink ( Var_src , Var_trg_2 ) ) => ~ Var_trg_1 != Var_trg_2 ) ) ) .

-fof ( upperMultiplicity_element_FunctionalInterface , axiom , ! [ Var_src , Var_trg_1 , Var_trg_2 ] : ( ( type_FunctionalInterface_class ( Var_src ) & ( type_FunctionalElement_class ( Var_trg_1 ) & type_FunctionalElement_class ( Var_trg_2 ) ) ) => ( ( rel_element_reference_FunctionalInterface ( Var_src , Var_trg_1 ) & rel_element_reference_FunctionalInterface ( Var_src , Var_trg_2 ) ) => ~ Var_trg_1 != Var_trg_2 ) ) ) .

-fof ( upperMultiplicity_terminator_FunctionalData , axiom , ! [ Var_src , Var_trg_1 , Var_trg_2 ] : ( ( type_FunctionalData_class ( Var_src ) & ( type_FAMTerminator_class ( Var_trg_1 ) & type_FAMTerminator_class ( Var_trg_2 ) ) ) => ( ( rel_terminator_reference_FunctionalData ( Var_src , Var_trg_1 ) & rel_terminator_reference_FunctionalData ( Var_src , Var_trg_2 ) ) => ~ Var_trg_1 != Var_trg_2 ) ) ) .

-fof ( upperMultiplicity_interface_FunctionalData , axiom , ! [ Var_src , Var_trg_1 , Var_trg_2 ] : ( ( type_FunctionalData_class ( Var_src ) & ( type_FunctionalInterface_class ( Var_trg_1 ) & type_FunctionalInterface_class ( Var_trg_2 ) ) ) => ( ( rel_interface_reference_FunctionalData ( Var_src , Var_trg_1 ) & rel_interface_reference_FunctionalData ( Var_src , Var_trg_2 ) ) => ~ Var_trg_1 != Var_trg_2 ) ) ) .

-fof ( oppositeReference_interface_FunctionalElement , axiom , ! [ Var_src , Var_trg ] : ( ( type_FunctionalElement_class ( Var_src ) & type_FunctionalInterface_class ( Var_trg ) ) => ( rel_interface_reference_FunctionalElement ( Var_src , Var_trg ) <=> rel_element_reference_FunctionalInterface ( Var_trg , Var_src ) ) ) ) .

-fof ( oppositeReference_parent_FunctionalElement , axiom , ! [ Var_src , Var_trg ] : ( ( type_FunctionalElement_class ( Var_src ) & type_Function_class ( Var_trg ) ) => ( rel_parent_reference_FunctionalElement ( Var_src , Var_trg ) <=> rel_subElements_reference_Function ( Var_trg , Var_src ) ) ) ) .

-fof ( oppositeReference_data_FAMTerminator , axiom , ! [ Var_src , Var_trg ] : ( ( type_FAMTerminator_class ( Var_src ) & type_FunctionalData_class ( Var_trg ) ) => ( rel_data_reference_FAMTerminator ( Var_src , Var_trg ) <=> rel_terminator_reference_FunctionalData ( Var_trg , Var_src ) ) ) ) .

-fof ( oppositeReference_from_InformationLink , axiom , ! [ Var_src , Var_trg ] : ( ( type_InformationLink_class ( Var_src ) & type_FunctionalOutput_class ( Var_trg ) ) => ( rel_from_reference_InformationLink ( Var_src , Var_trg ) <=> rel_outgoingLinks_reference_FunctionalOutput ( Var_trg , Var_src ) ) ) ) .

-fof ( oppositeReference_to_InformationLink , axiom , ! [ Var_src , Var_trg ] : ( ( type_InformationLink_class ( Var_src ) & type_FunctionalInput_class ( Var_trg ) ) => ( rel_to_reference_InformationLink ( Var_src , Var_trg ) <=> rel_IncomingLinks_reference_FunctionalInput ( Var_trg , Var_src ) ) ) ) .

-fof ( oppositeReference_data_FunctionalInterface , axiom , ! [ Var_src , Var_trg ] : ( ( type_FunctionalInterface_class ( Var_src ) & type_FunctionalData_class ( Var_trg ) ) => ( rel_data_reference_FunctionalInterface ( Var_src , Var_trg ) <=> rel_interface_reference_FunctionalData ( Var_trg , Var_src ) ) ) ) .

-fof ( lowerMultiplicity_type_Function , axiom , ! [ Var_src ] : ( type_Function_class ( Var_src ) => ? [ Var_trg_1 ] : ( type_FunctionType_enum ( Var_trg_1 ) & rel_type_attribute_Function ( Var_src , Var_trg_1 ) ) ) ) .

-fof ( upperMultiplicity_type_Function , axiom , ! [ Var_src , Var_trg_1 , Var_trg_2 ] : ( ( type_Function_class ( Var_src ) & ( type_FunctionType_enum ( Var_trg_1 ) & type_FunctionType_enum ( Var_trg_2 ) ) ) => ( ( rel_type_attribute_Function ( Var_src , Var_trg_1 ) & rel_type_attribute_Function ( Var_src , Var_trg_2 ) ) => ~ Var_trg_1 != Var_trg_2 ) ) ) .

-fof ( errorpattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_terminatorAndInformation , axiom , ! [ Var_p0 , Var_p1 ] : ( ( type_FAMTerminator_class ( Var_p0 ) & type_InformationLink_class ( Var_p1 ) ) => ~ rel_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_terminatorAndInformation ( Var_p0 , Var_p1 ) ) ) .

+fof ( typeDef_FunctionType_enum , axiom , ! [ A ] : ( t_FunctionType_enum ( A ) <=> ( e_Root_literal_FunctionType_FunctionType_enum ( A ) | ( e_Intermediate_literal_FunctionType_FunctionType_enum ( A ) | e_Leaf_literal_FunctionType_FunctionType_enum ( A ) ) ) ) ) .

+fof ( hierarchyHandler , axiom , ! [ A ] : ( object ( A ) <=> ( ( t_InformationLink_class ( A ) & ( ~ t_FunctionType_enum ( A ) & ( ~ t_FunctionalData_class ( A ) & ( ~ t_FunctionalOutput_class ( A ) & ( ~ t_Function_class ( A ) & ( ~ t_FunctionalInput_class ( A ) & ( ~ t_FunctionalArchitectureModel_class ( A ) & ( ~ t_FunctionalElement_class ( A ) & ( ~ t_FunctionalInterface_class ( A ) & ~ t_FAMTerminator_class ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_InformationLink_class ( A ) & ( t_FunctionType_enum ( A ) & ( ~ t_FunctionalData_class ( A ) & ( ~ t_FunctionalOutput_class ( A ) & ( ~ t_Function_class ( A ) & ( ~ t_FunctionalInput_class ( A ) & ( ~ t_FunctionalArchitectureModel_class ( A ) & ( ~ t_FunctionalElement_class ( A ) & ( ~ t_FunctionalInterface_class ( A ) & ~ t_FAMTerminator_class ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_InformationLink_class ( A ) & ( ~ t_FunctionType_enum ( A ) & ( t_FunctionalData_class ( A ) & ( t_FunctionalOutput_class ( A ) & ( ~ t_Function_class ( A ) & ( ~ t_FunctionalInput_class ( A ) & ( ~ t_FunctionalArchitectureModel_class ( A ) & ( ~ t_FunctionalElement_class ( A ) & ( ~ t_FunctionalInterface_class ( A ) & ~ t_FAMTerminator_class ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_InformationLink_class ( A ) & ( ~ t_FunctionType_enum ( A ) & ( ~ t_FunctionalData_class ( A ) & ( ~ t_FunctionalOutput_class ( A ) & ( t_Function_class ( A ) & ( ~ t_FunctionalInput_class ( A ) & ( ~ t_FunctionalArchitectureModel_class ( A ) & ( t_FunctionalElement_class ( A ) & ( ~ t_FunctionalInterface_class ( A ) & ~ t_FAMTerminator_class ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_InformationLink_class ( A ) & ( ~ t_FunctionType_enum ( A ) & ( t_FunctionalData_class ( A ) & ( ~ t_FunctionalOutput_class ( A ) & ( ~ t_Function_class ( A ) & ( t_FunctionalInput_class ( A ) & ( ~ t_FunctionalArchitectureModel_class ( A ) & ( ~ t_FunctionalElement_class ( A ) & ( ~ t_FunctionalInterface_class ( A ) & ~ t_FAMTerminator_class ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_InformationLink_class ( A ) & ( ~ t_FunctionType_enum ( A ) & ( ~ t_FunctionalData_class ( A ) & ( ~ t_FunctionalOutput_class ( A ) & ( ~ t_Function_class ( A ) & ( ~ t_FunctionalInput_class ( A ) & ( t_FunctionalArchitectureModel_class ( A ) & ( ~ t_FunctionalElement_class ( A ) & ( ~ t_FunctionalInterface_class ( A ) & ~ t_FAMTerminator_class ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_InformationLink_class ( A ) & ( ~ t_FunctionType_enum ( A ) & ( ~ t_FunctionalData_class ( A ) & ( ~ t_FunctionalOutput_class ( A ) & ( ~ t_Function_class ( A ) & ( ~ t_FunctionalInput_class ( A ) & ( ~ t_FunctionalArchitectureModel_class ( A ) & ( ~ t_FunctionalElement_class ( A ) & ( t_FunctionalInterface_class ( A ) & ~ t_FAMTerminator_class ( A ) ) ) ) ) ) ) ) ) ) | ( ~ t_InformationLink_class ( A ) & ( ~ t_FunctionType_enum ( A ) & ( ~ t_FunctionalData_class ( A ) & ( ~ t_FunctionalOutput_class ( A ) & ( ~ t_Function_class ( A ) & ( ~ t_FunctionalInput_class ( A ) & ( ~ t_FunctionalArchitectureModel_class ( A ) & ( ~ t_FunctionalElement_class ( A ) & ( ~ t_FunctionalInterface_class ( A ) & t_FAMTerminator_class ( A ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) .

+fof ( typeScope , axiom , ! [ A ] : ( object ( A ) <=> ( A = o1 | ( A = o2 | ( A = o3 | ( A = o4 | A = o5 ) ) ) ) ) ) .

+fof ( typeUniqueness , axiom , o1 != o2 & ( o1 != o3 & ( o2 != o3 & ( o1 != o4 & ( o2 != o4 & ( o3 != o4 & ( o1 != o5 & ( o2 != o5 & ( o3 != o5 & o4 != o5 ) ) ) ) ) ) ) ) ) .

+fof ( compliance_interface_reference_FunctionalElement , axiom , ! [ Var_0 , Var_1 ] : ( rel_interface_reference_FunctionalElement ( Var_0 , Var_1 ) => ( t_FunctionalElement_class ( Var_0 ) & t_FunctionalInterface_class ( Var_1 ) ) ) ) .

+fof ( compliance_model_reference_FunctionalElement , axiom , ! [ Var_0 , Var_1 ] : ( rel_model_reference_FunctionalElement ( Var_0 , Var_1 ) => ( t_FunctionalElement_class ( Var_0 ) & t_FunctionalArchitectureModel_class ( Var_1 ) ) ) ) .

+fof ( compliance_parent_reference_FunctionalElement , axiom , ! [ Var_0 , Var_1 ] : ( rel_parent_reference_FunctionalElement ( Var_0 , Var_1 ) => ( t_FunctionalElement_class ( Var_0 ) & t_Function_class ( Var_1 ) ) ) ) .

+fof ( compliance_rootElements_reference_FunctionalArchitectureModel , axiom , ! [ Var_0 , Var_1 ] : ( rel_rootElements_reference_FunctionalArchitectureModel ( Var_0 , Var_1 ) => ( t_FunctionalArchitectureModel_class ( Var_0 ) & t_FunctionalElement_class ( Var_1 ) ) ) ) .

+fof ( compliance_subElements_reference_Function , axiom , ! [ Var_0 , Var_1 ] : ( rel_subElements_reference_Function ( Var_0 , Var_1 ) => ( t_Function_class ( Var_0 ) & t_FunctionalElement_class ( Var_1 ) ) ) ) .

+fof ( compliance_data_reference_FAMTerminator , axiom , ! [ Var_0 , Var_1 ] : ( rel_data_reference_FAMTerminator ( Var_0 , Var_1 ) => ( t_FAMTerminator_class ( Var_0 ) & t_FunctionalData_class ( Var_1 ) ) ) ) .

+fof ( compliance_from_reference_InformationLink , axiom , ! [ Var_0 , Var_1 ] : ( rel_from_reference_InformationLink ( Var_0 , Var_1 ) => ( t_InformationLink_class ( Var_0 ) & t_FunctionalOutput_class ( Var_1 ) ) ) ) .

+fof ( compliance_to_reference_InformationLink , axiom , ! [ Var_0 , Var_1 ] : ( rel_to_reference_InformationLink ( Var_0 , Var_1 ) => ( t_InformationLink_class ( Var_0 ) & t_FunctionalInput_class ( Var_1 ) ) ) ) .

+fof ( compliance_data_reference_FunctionalInterface , axiom , ! [ Var_0 , Var_1 ] : ( rel_data_reference_FunctionalInterface ( Var_0 , Var_1 ) => ( t_FunctionalInterface_class ( Var_0 ) & t_FunctionalData_class ( Var_1 ) ) ) ) .

+fof ( compliance_element_reference_FunctionalInterface , axiom , ! [ Var_0 , Var_1 ] : ( rel_element_reference_FunctionalInterface ( Var_0 , Var_1 ) => ( t_FunctionalInterface_class ( Var_0 ) & t_FunctionalElement_class ( Var_1 ) ) ) ) .

+fof ( compliance_IncomingLinks_reference_FunctionalInput , axiom , ! [ Var_0 , Var_1 ] : ( rel_IncomingLinks_reference_FunctionalInput ( Var_0 , Var_1 ) => ( t_FunctionalInput_class ( Var_0 ) & t_InformationLink_class ( Var_1 ) ) ) ) .

+fof ( compliance_outgoingLinks_reference_FunctionalOutput , axiom , ! [ Var_0 , Var_1 ] : ( rel_outgoingLinks_reference_FunctionalOutput ( Var_0 , Var_1 ) => ( t_FunctionalOutput_class ( Var_0 ) & t_InformationLink_class ( Var_1 ) ) ) ) .

+fof ( compliance_terminator_reference_FunctionalData , axiom , ! [ Var_0 , Var_1 ] : ( rel_terminator_reference_FunctionalData ( Var_0 , Var_1 ) => ( t_FunctionalData_class ( Var_0 ) & t_FAMTerminator_class ( Var_1 ) ) ) ) .

+fof ( compliance_interface_reference_FunctionalData , axiom , ! [ Var_0 , Var_1 ] : ( rel_interface_reference_FunctionalData ( Var_0 , Var_1 ) => ( t_FunctionalData_class ( Var_0 ) & t_FunctionalInterface_class ( Var_1 ) ) ) ) .

+fof ( compliance_type_attribute_Function , axiom , ! [ Var_0 , Var_1 ] : ( rel_type_attribute_Function ( Var_0 , Var_1 ) => ( t_Function_class ( Var_0 ) & t_FunctionType_enum ( Var_1 ) ) ) ) .

+fof ( compliance_pattern_ca_mcgill_ecse_dslreasoner_vampire_queries_terminatorAndInformation , axiom , ! [ Var_parameter_T , Var_parameter_I ] : ( rel_pattern_ca_mcgill_ecse_dslreasoner_vampire_queries_terminatorAndInformation ( Var_parameter_T , Var_parameter_I ) => ( t_FAMTerminator_class ( Var_parameter_T ) & t_InformationLink_class ( Var_parameter_I ) ) ) ) .

+fof ( relation_pattern_ca_mcgill_ecse_dslreasoner_vampire_queries_terminatorAndInformation , axiom , ! [ Var_parameter_T , Var_parameter_I ] : ( ( t_FAMTerminator_class ( Var_parameter_T ) & t_InformationLink_class ( Var_parameter_I ) ) => ( rel_pattern_ca_mcgill_ecse_dslreasoner_vampire_queries_terminatorAndInformation ( Var_parameter_T , Var_parameter_I ) <=> ( ? [ Var_variable_Out ] : ( t_FunctionalOutput_class ( Var_variable_Out ) & ( rel_outgoingLinks_reference_FunctionalOutput ( Var_variable_Out , Var_parameter_I ) & rel_terminator_reference_FunctionalData ( Var_variable_Out , Var_parameter_T ) ) ) | ? [ Var_variable_In ] : ( t_FunctionalInput_class ( Var_variable_In ) & ( rel_to_reference_InformationLink ( Var_parameter_I , Var_variable_In ) & rel_terminator_reference_FunctionalData ( Var_variable_In , Var_parameter_T ) ) ) ) ) ) ) .

+fof ( upperMultiplicity_interface_FunctionalElement , axiom , ! [ Var_src , Var_trg_1 , Var_trg_2 ] : ( ( t_FunctionalElement_class ( Var_src ) & ( t_FunctionalInterface_class ( Var_trg_1 ) & t_FunctionalInterface_class ( Var_trg_2 ) ) ) => ( ( rel_interface_reference_FunctionalElement ( Var_src , Var_trg_1 ) & rel_interface_reference_FunctionalElement ( Var_src , Var_trg_2 ) ) => ~ Var_trg_1 != Var_trg_2 ) ) ) .

+fof ( lowerMultiplicity_model_FunctionalElement , axiom , ! [ Var_src ] : ( t_FunctionalElement_class ( Var_src ) => ? [ Var_trg_1 ] : ( t_FunctionalArchitectureModel_class ( Var_trg_1 ) & rel_model_reference_FunctionalElement ( Var_src , Var_trg_1 ) ) ) ) .

+fof ( upperMultiplicity_model_FunctionalElement , axiom , ! [ Var_src , Var_trg_1 , Var_trg_2 ] : ( ( t_FunctionalElement_class ( Var_src ) & ( t_FunctionalArchitectureModel_class ( Var_trg_1 ) & t_FunctionalArchitectureModel_class ( Var_trg_2 ) ) ) => ( ( rel_model_reference_FunctionalElement ( Var_src , Var_trg_1 ) & rel_model_reference_FunctionalElement ( Var_src , Var_trg_2 ) ) => ~ Var_trg_1 != Var_trg_2 ) ) ) .

+fof ( upperMultiplicity_parent_FunctionalElement , axiom , ! [ Var_src , Var_trg_1 , Var_trg_2 ] : ( ( t_FunctionalElement_class ( Var_src ) & ( t_Function_class ( Var_trg_1 ) & t_Function_class ( Var_trg_2 ) ) ) => ( ( rel_parent_reference_FunctionalElement ( Var_src , Var_trg_1 ) & rel_parent_reference_FunctionalElement ( Var_src , Var_trg_2 ) ) => ~ Var_trg_1 != Var_trg_2 ) ) ) .

+fof ( upperMultiplicity_data_FAMTerminator , axiom , ! [ Var_src , Var_trg_1 , Var_trg_2 ] : ( ( t_FAMTerminator_class ( Var_src ) & ( t_FunctionalData_class ( Var_trg_1 ) & t_FunctionalData_class ( Var_trg_2 ) ) ) => ( ( rel_data_reference_FAMTerminator ( Var_src , Var_trg_1 ) & rel_data_reference_FAMTerminator ( Var_src , Var_trg_2 ) ) => ~ Var_trg_1 != Var_trg_2 ) ) ) .

+fof ( upperMultiplicity_from_InformationLink , axiom , ! [ Var_src , Var_trg_1 , Var_trg_2 ] : ( ( t_InformationLink_class ( Var_src ) & ( t_FunctionalOutput_class ( Var_trg_1 ) & t_FunctionalOutput_class ( Var_trg_2 ) ) ) => ( ( rel_from_reference_InformationLink ( Var_src , Var_trg_1 ) & rel_from_reference_InformationLink ( Var_src , Var_trg_2 ) ) => ~ Var_trg_1 != Var_trg_2 ) ) ) .

+fof ( lowerMultiplicity_to_InformationLink , axiom , ! [ Var_src ] : ( t_InformationLink_class ( Var_src ) => ? [ Var_trg_1 ] : ( t_FunctionalInput_class ( Var_trg_1 ) & rel_to_reference_InformationLink ( Var_src , Var_trg_1 ) ) ) ) .

+fof ( upperMultiplicity_to_InformationLink , axiom , ! [ Var_src , Var_trg_1 , Var_trg_2 ] : ( ( t_InformationLink_class ( Var_src ) & ( t_FunctionalInput_class ( Var_trg_1 ) & t_FunctionalInput_class ( Var_trg_2 ) ) ) => ( ( rel_to_reference_InformationLink ( Var_src , Var_trg_1 ) & rel_to_reference_InformationLink ( Var_src , Var_trg_2 ) ) => ~ Var_trg_1 != Var_trg_2 ) ) ) .

+fof ( upperMultiplicity_element_FunctionalInterface , axiom , ! [ Var_src , Var_trg_1 , Var_trg_2 ] : ( ( t_FunctionalInterface_class ( Var_src ) & ( t_FunctionalElement_class ( Var_trg_1 ) & t_FunctionalElement_class ( Var_trg_2 ) ) ) => ( ( rel_element_reference_FunctionalInterface ( Var_src , Var_trg_1 ) & rel_element_reference_FunctionalInterface ( Var_src , Var_trg_2 ) ) => ~ Var_trg_1 != Var_trg_2 ) ) ) .

+fof ( upperMultiplicity_terminator_FunctionalData , axiom , ! [ Var_src , Var_trg_1 , Var_trg_2 ] : ( ( t_FunctionalData_class ( Var_src ) & ( t_FAMTerminator_class ( Var_trg_1 ) & t_FAMTerminator_class ( Var_trg_2 ) ) ) => ( ( rel_terminator_reference_FunctionalData ( Var_src , Var_trg_1 ) & rel_terminator_reference_FunctionalData ( Var_src , Var_trg_2 ) ) => ~ Var_trg_1 != Var_trg_2 ) ) ) .

+fof ( upperMultiplicity_interface_FunctionalData , axiom , ! [ Var_src , Var_trg_1 , Var_trg_2 ] : ( ( t_FunctionalData_class ( Var_src ) & ( t_FunctionalInterface_class ( Var_trg_1 ) & t_FunctionalInterface_class ( Var_trg_2 ) ) ) => ( ( rel_interface_reference_FunctionalData ( Var_src , Var_trg_1 ) & rel_interface_reference_FunctionalData ( Var_src , Var_trg_2 ) ) => ~ Var_trg_1 != Var_trg_2 ) ) ) .

+fof ( oppositeReference_interface_FunctionalElement , axiom , ! [ Var_src , Var_trg ] : ( ( t_FunctionalElement_class ( Var_src ) & t_FunctionalInterface_class ( Var_trg ) ) => ( rel_interface_reference_FunctionalElement ( Var_src , Var_trg ) <=> rel_element_reference_FunctionalInterface ( Var_trg , Var_src ) ) ) ) .

+fof ( oppositeReference_parent_FunctionalElement , axiom , ! [ Var_src , Var_trg ] : ( ( t_FunctionalElement_class ( Var_src ) & t_Function_class ( Var_trg ) ) => ( rel_parent_reference_FunctionalElement ( Var_src , Var_trg ) <=> rel_subElements_reference_Function ( Var_trg , Var_src ) ) ) ) .

+fof ( oppositeReference_data_FAMTerminator , axiom , ! [ Var_src , Var_trg ] : ( ( t_FAMTerminator_class ( Var_src ) & t_FunctionalData_class ( Var_trg ) ) => ( rel_data_reference_FAMTerminator ( Var_src , Var_trg ) <=> rel_terminator_reference_FunctionalData ( Var_trg , Var_src ) ) ) ) .

+fof ( oppositeReference_from_InformationLink , axiom , ! [ Var_src , Var_trg ] : ( ( t_InformationLink_class ( Var_src ) & t_FunctionalOutput_class ( Var_trg ) ) => ( rel_from_reference_InformationLink ( Var_src , Var_trg ) <=> rel_outgoingLinks_reference_FunctionalOutput ( Var_trg , Var_src ) ) ) ) .

+fof ( oppositeReference_to_InformationLink , axiom , ! [ Var_src , Var_trg ] : ( ( t_InformationLink_class ( Var_src ) & t_FunctionalInput_class ( Var_trg ) ) => ( rel_to_reference_InformationLink ( Var_src , Var_trg ) <=> rel_IncomingLinks_reference_FunctionalInput ( Var_trg , Var_src ) ) ) ) .

+fof ( oppositeReference_data_FunctionalInterface , axiom , ! [ Var_src , Var_trg ] : ( ( t_FunctionalInterface_class ( Var_src ) & t_FunctionalData_class ( Var_trg ) ) => ( rel_data_reference_FunctionalInterface ( Var_src , Var_trg ) <=> rel_interface_reference_FunctionalData ( Var_trg , Var_src ) ) ) ) .

+fof ( lowerMultiplicity_type_Function , axiom , ! [ Var_src ] : ( t_Function_class ( Var_src ) => ? [ Var_trg_1 ] : ( t_FunctionType_enum ( Var_trg_1 ) & rel_type_attribute_Function ( Var_src , Var_trg_1 ) ) ) ) .

+fof ( upperMultiplicity_type_Function , axiom , ! [ Var_src , Var_trg_1 , Var_trg_2 ] : ( ( t_Function_class ( Var_src ) & ( t_FunctionType_enum ( Var_trg_1 ) & t_FunctionType_enum ( Var_trg_2 ) ) ) => ( ( rel_type_attribute_Function ( Var_src , Var_trg_1 ) & rel_type_attribute_Function ( Var_src , Var_trg_2 ) ) => ~ Var_trg_1 != Var_trg_2 ) ) ) .

+fof ( errorpattern_ca_mcgill_ecse_dslreasoner_vampire_queries_terminatorAndInformation , axiom , ! [ Var_p0 , Var_p1 ] : ( ( t_FAMTerminator_class ( Var_p0 ) & t_InformationLink_class ( Var_p1 ) ) => ~ rel_pattern_ca_mcgill_ecse_dslreasoner_vampire_queries_terminatorAndInformation ( Var_p0 , Var_p1 ) ) ) .