VAMPIRE: close #22, improve test structure for #39, .vql file trouble

2 files changed, 5 insertions, 74 deletions

diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/output/FAMTest/Fam.logicproblem b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/output/FAMTest/Fam.logicproblem
index 18e58ab0..4f0bbdb1 100644
--- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/output/FAMTest/Fam.logicproblem
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/output/FAMTest/Fam.logicproblem
@@ -1,7 +1,7 @@
 <?xml version="1.0" encoding="ASCII"?>

 <language:LogicProblem xmi:version="2.0" xmlns:xmi="http://www.omg.org/XMI" xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" xmlns:ecore2logicannotations="http://www.bme.hu/mit/inf/dslreasoner/logic/model/language/ecore2logicannotation" xmlns:language="http://www.bme.hu/mit/inf/dslreasoner/logic/model/problem" xmlns:language_1="http://www.bme.hu/mit/inf/dslreasoner/logic/model/language">

   <types xsi:type="language_1:TypeDeclaration" name="FunctionalElement class" subtypes="//@types.2" isAbstract="true"/>

-  <types xsi:type="language_1:TypeDeclaration" name="FunctionalArchitectureModel class"/>

+  <types xsi:type="language_1:TypeDeclaration" name="FunctionalArchitectureModel class" subtypes="//@types.10 //@types.11" isAbstract="true"/>

   <types xsi:type="language_1:TypeDeclaration" name="Function class" supertypes="//@types.0"/>

   <types xsi:type="language_1:TypeDeclaration" name="FAMTerminator class"/>

   <types xsi:type="language_1:TypeDeclaration" name="InformationLink class"/>

@@ -10,6 +10,8 @@
   <types xsi:type="language_1:TypeDeclaration" name="FunctionalOutput class" supertypes="//@types.8"/>

   <types xsi:type="language_1:TypeDeclaration" name="FunctionalData class" subtypes="//@types.6 //@types.7" isAbstract="true"/>

   <types xsi:type="language_1:TypeDefinition" name="FunctionType enum" elements="//@elements.0 //@elements.1 //@elements.2"/>

+  <types xsi:type="language_1:TypeDefinition" name="FunctionalArchitectureModel class DefinedPart" supertypes="//@types.1" elements="//@elements.3"/>

+  <types xsi:type="language_1:TypeDeclaration" name="FunctionalArchitectureModel class UndefinedPart" supertypes="//@types.1"/>

   <assertions name="upperMultiplicity interface FunctionalElement" annotations="//@annotations.0">

     <value xsi:type="language_1:Forall">

       <quantifiedVariables name="src">

@@ -557,7 +559,8 @@
   <elements name="Root literal FunctionType" definedInType="//@types.9"/>

   <elements name="Intermediate literal FunctionType" definedInType="//@types.9"/>

   <elements name="Leaf literal FunctionType" definedInType="//@types.9"/>

-  <containmentHierarchies typesOrderedInHierarchy="//@types.8 //@types.5 //@types.4 //@types.6 //@types.1 //@types.7 //@types.3 //@types.2 //@types.0" containmentRelations="//@relations.0 //@relations.3 //@relations.4 //@relations.8 //@relations.11 //@relations.12"/>

+  <elements name="o 1" definedInType="//@types.10"/>

+  <containmentHierarchies typesOrderedInHierarchy="//@types.1 //@types.5 //@types.6 //@types.3 //@types.8 //@types.7 //@types.0 //@types.2 //@types.4 //@types.10 //@types.11" containmentRelations="//@relations.0 //@relations.3 //@relations.4 //@relations.8 //@relations.11 //@relations.12"/>

   <annotations xsi:type="ecore2logicannotations:UpperMultiplicityAssertion" target="//@assertions.0" relation="//@relations.0" upper="1"/>

   <annotations xsi:type="ecore2logicannotations:LowerMultiplicityAssertion" target="//@assertions.1" relation="//@relations.1" lower="1"/>

   <annotations xsi:type="ecore2logicannotations:UpperMultiplicityAssertion" target="//@assertions.2" relation="//@relations.1" upper="1"/>

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
deleted file mode 100644
index 3d49d42c..00000000
--- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/output/FAMTest/vampireProblem.tptp
+++ /dev/null
@@ -1,72 +0,0 @@
-% This is an initial Test Comment

-fof ( typeDef_FunctionType , axiom , ! [ A ] : ( t_FunctionType ( A ) <=> ( object ( A ) & ( ( e_Root_FunctionType ( A ) & ( ~ e_Intermediate_FunctionType ( A ) & ~ e_Leaf_FunctionType ( A ) ) ) | ( ( ~ e_Root_FunctionType ( A ) & ( e_Intermediate_FunctionType ( A ) & ~ e_Leaf_FunctionType ( A ) ) ) | ( ~ e_Root_FunctionType ( A ) & ( ~ e_Intermediate_FunctionType ( A ) & e_Leaf_FunctionType ( A ) ) ) ) ) ) ) ) .

-fof ( enumScope_FunctionType_Root , axiom , ! [ A ] : ( A = eo1 <=> e_Root_FunctionType ( A ) ) ) .

-fof ( enumScope_FunctionType_Intermediate , axiom , ! [ A ] : ( A = eo2 <=> e_Intermediate_FunctionType ( A ) ) ) .

-fof ( enumScope_FunctionType_Leaf , axiom , ! [ A ] : ( A = eo3 <=> e_Leaf_FunctionType ( A ) ) ) .

-fof ( notObjectHandler , axiom , ! [ A ] : ( ~ object ( A ) <=> ( ~ t_FunctionalElement ( A ) & ( ~ t_FunctionalArchitectureModel ( A ) & ( ~ t_Function ( A ) & ( ~ t_FAMTerminator ( A ) & ( ~ t_InformationLink ( A ) & ( ~ t_FunctionalInterface ( A ) & ( ~ t_FunctionalInput ( A ) & ( ~ t_FunctionalOutput ( A ) & ( ~ t_FunctionalData ( A ) & ~ t_FunctionType ( A ) ) ) ) ) ) ) ) ) ) ) ) .

-fof ( inheritanceHierarchyHandler , axiom , ! [ A ] : ( object ( A ) <=> ( ( t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionalInput ( A ) & ( ~ t_Function ( A ) & ( ~ t_FAMTerminator ( A ) & ( ~ t_FunctionType ( A ) & ( ~ t_FunctionalElement ( A ) & ( ~ t_FunctionalOutput ( A ) & ( ~ t_FunctionalData ( A ) & ( ~ t_InformationLink ( A ) & ~ t_FunctionalInterface ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_FunctionalArchitectureModel ( A ) & ( t_FunctionalInput ( A ) & ( ~ t_Function ( A ) & ( ~ t_FAMTerminator ( A ) & ( ~ t_FunctionType ( A ) & ( ~ t_FunctionalElement ( A ) & ( ~ t_FunctionalOutput ( A ) & ( t_FunctionalData ( A ) & ( ~ t_InformationLink ( A ) & ~ t_FunctionalInterface ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionalInput ( A ) & ( t_Function ( A ) & ( ~ t_FAMTerminator ( A ) & ( ~ t_FunctionType ( A ) & ( t_FunctionalElement ( A ) & ( ~ t_FunctionalOutput ( A ) & ( ~ t_FunctionalData ( A ) & ( ~ t_InformationLink ( A ) & ~ t_FunctionalInterface ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionalInput ( A ) & ( ~ t_Function ( A ) & ( t_FAMTerminator ( A ) & ( ~ t_FunctionType ( A ) & ( ~ t_FunctionalElement ( A ) & ( ~ t_FunctionalOutput ( A ) & ( ~ t_FunctionalData ( A ) & ( ~ t_InformationLink ( A ) & ~ t_FunctionalInterface ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionalInput ( A ) & ( ~ t_Function ( A ) & ( ~ t_FAMTerminator ( A ) & ( t_FunctionType ( A ) & ( ~ t_FunctionalElement ( A ) & ( ~ t_FunctionalOutput ( A ) & ( ~ t_FunctionalData ( A ) & ( ~ t_InformationLink ( A ) & ~ t_FunctionalInterface ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionalInput ( A ) & ( ~ t_Function ( A ) & ( ~ t_FAMTerminator ( A ) & ( ~ t_FunctionType ( A ) & ( ~ t_FunctionalElement ( A ) & ( t_FunctionalOutput ( A ) & ( t_FunctionalData ( A ) & ( ~ t_InformationLink ( A ) & ~ t_FunctionalInterface ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionalInput ( A ) & ( ~ t_Function ( A ) & ( ~ t_FAMTerminator ( A ) & ( ~ t_FunctionType ( A ) & ( ~ t_FunctionalElement ( A ) & ( ~ t_FunctionalOutput ( A ) & ( ~ t_FunctionalData ( A ) & ( t_InformationLink ( A ) & ~ t_FunctionalInterface ( A ) ) ) ) ) ) ) ) ) ) | ( ~ t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionalInput ( A ) & ( ~ t_Function ( A ) & ( ~ t_FAMTerminator ( A ) & ( ~ t_FunctionType ( A ) & ( ~ t_FunctionalElement ( A ) & ( ~ t_FunctionalOutput ( A ) & ( ~ t_FunctionalData ( A ) & ( ~ t_InformationLink ( A ) & t_FunctionalInterface ( A ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) .

-fof ( typeScope_min_object , axiom , ! [ A ] : ( ( A = o1 | ( A = o2 | ( A = o3 | ( A = o4 | ( A = eo1 | ( A = eo2 | A = eo3 ) ) ) ) ) ) => object ( A ) ) ) .

-fof ( typeScope_max_object , axiom , ! [ A ] : ( object ( A ) => ( A = eo1 | ( A = eo2 | ( A = eo3 | ( A = o1 | ( A = o2 | ( A = o3 | ( A = o4 | A = o5 ) ) ) ) ) ) ) ) ) .

-fof ( typeScope_min_t_Function , axiom , ! [ A ] : ( A = o2 => ( t_Function ( A ) & object ( A ) ) ) ) .

-fof ( typeScope_min_t_FunctionalOutput , axiom , ! [ A ] : ( ( A = o3 | ( A = o4 | A = o5 ) ) => ( t_FunctionalOutput ( A ) & object ( A ) ) ) ) .

-fof ( typeScope_min_t_FunctionalInterface , axiom , ! [ A ] : ( ( A = o6 | A = o7 ) => ( t_FunctionalInterface ( A ) & object ( A ) ) ) ) .

-fof ( typeScope_max_t_Function , axiom , ! [ A ] : ( ( t_Function ( A ) & object ( A ) ) => A = o2 ) ) .

-fof ( typeScope_max_t_FunctionalOutput , axiom , ! [ A ] : ( ( t_FunctionalOutput ( A ) & object ( A ) ) => ( A = o3 | ( A = o4 | A = o5 ) ) ) ) .

-fof ( t_uniqueness_eo1 , axiom , eo1 != eo2 & ( eo1 != eo3 & ( eo1 != o1 & ( eo1 != o2 & ( eo1 != o3 & ( eo1 != o4 & eo1 != o5 ) ) ) ) ) ) .

-fof ( t_uniqueness_eo2 , axiom , eo2 != eo3 & ( eo2 != o1 & ( eo2 != o2 & ( eo2 != o3 & ( eo2 != o4 & eo2 != o5 ) ) ) ) ) .

-fof ( t_uniqueness_eo3 , axiom , eo3 != o1 & ( eo3 != o2 & ( eo3 != o3 & ( eo3 != o4 & eo3 != o5 ) ) ) ) .

-fof ( t_uniqueness_o1 , axiom , o1 != o2 & ( o1 != o3 & ( o1 != o4 & o1 != o5 ) ) ) .

-fof ( t_uniqueness_o2 , axiom , o2 != o3 & ( o2 != o4 & o2 != o5 ) ) .

-fof ( t_uniqueness_o3 , axiom , o3 != o4 & o3 != o5 ) .

-fof ( t_uniqueness_o4 , axiom , o4 != o5 ) .

-fof ( compliance_interface_FunctionalElement , axiom , ! [ V_0 , V_1 ] : ( r_interface_FunctionalElement ( V_0 , V_1 ) => ( t_FunctionalElement ( V_0 ) & t_FunctionalInterface ( V_1 ) ) ) ) .

-fof ( compliance_model_FunctionalElement , axiom , ! [ V_0 , V_1 ] : ( r_model_FunctionalElement ( V_0 , V_1 ) => ( t_FunctionalElement ( V_0 ) & t_FunctionalArchitectureModel ( V_1 ) ) ) ) .

-fof ( compliance_parent_FunctionalElement , axiom , ! [ V_0 , V_1 ] : ( r_parent_FunctionalElement ( V_0 , V_1 ) => ( t_FunctionalElement ( V_0 ) & t_Function ( V_1 ) ) ) ) .

-fof ( compliance_rootElements_FunctionalArchitectureModel , axiom , ! [ V_0 , V_1 ] : ( r_rootElements_FunctionalArchitectureModel ( V_0 , V_1 ) => ( t_FunctionalArchitectureModel ( V_0 ) & t_FunctionalElement ( V_1 ) ) ) ) .

-fof ( compliance_subElements_Function , axiom , ! [ V_0 , V_1 ] : ( r_subElements_Function ( V_0 , V_1 ) => ( t_Function ( V_0 ) & t_FunctionalElement ( V_1 ) ) ) ) .

-fof ( compliance_data_FAMTerminator , axiom , ! [ V_0 , V_1 ] : ( r_data_FAMTerminator ( V_0 , V_1 ) => ( t_FAMTerminator ( V_0 ) & t_FunctionalData ( V_1 ) ) ) ) .

-fof ( compliance_from_InformationLink , axiom , ! [ V_0 , V_1 ] : ( r_from_InformationLink ( V_0 , V_1 ) => ( t_InformationLink ( V_0 ) & t_FunctionalOutput ( V_1 ) ) ) ) .

-fof ( compliance_to_InformationLink , axiom , ! [ V_0 , V_1 ] : ( r_to_InformationLink ( V_0 , V_1 ) => ( t_InformationLink ( V_0 ) & t_FunctionalInput ( V_1 ) ) ) ) .

-fof ( compliance_data_FunctionalInterface , axiom , ! [ V_0 , V_1 ] : ( r_data_FunctionalInterface ( V_0 , V_1 ) => ( t_FunctionalInterface ( V_0 ) & t_FunctionalData ( V_1 ) ) ) ) .

-fof ( compliance_element_FunctionalInterface , axiom , ! [ V_0 , V_1 ] : ( r_element_FunctionalInterface ( V_0 , V_1 ) => ( t_FunctionalInterface ( V_0 ) & t_FunctionalElement ( V_1 ) ) ) ) .

-fof ( compliance_IncomingLinks_FunctionalInput , axiom , ! [ V_0 , V_1 ] : ( r_IncomingLinks_FunctionalInput ( V_0 , V_1 ) => ( t_FunctionalInput ( V_0 ) & t_InformationLink ( V_1 ) ) ) ) .

-fof ( compliance_outgoingLinks_FunctionalOutput , axiom , ! [ V_0 , V_1 ] : ( r_outgoingLinks_FunctionalOutput ( V_0 , V_1 ) => ( t_FunctionalOutput ( V_0 ) & t_InformationLink ( V_1 ) ) ) ) .

-fof ( compliance_terminator_FunctionalData , axiom , ! [ V_0 , V_1 ] : ( r_terminator_FunctionalData ( V_0 , V_1 ) => ( t_FunctionalData ( V_0 ) & t_FAMTerminator ( V_1 ) ) ) ) .

-fof ( compliance_interface_FunctionalData , axiom , ! [ V_0 , V_1 ] : ( r_interface_FunctionalData ( V_0 , V_1 ) => ( t_FunctionalData ( V_0 ) & t_FunctionalInterface ( V_1 ) ) ) ) .

-fof ( compliance_type_Function , axiom , ! [ V_0 , V_1 ] : ( r_type_Function ( V_0 , V_1 ) => ( t_Function ( V_0 ) & t_FunctionType ( V_1 ) ) ) ) .

-fof ( containment_topLevel_t_FunctionalArchitectureModel , axiom , ! [ A ] : ( t_FunctionalArchitectureModel ( A ) <=> A = o1 ) ) .

-fof ( containment_noDup_r_interface_FunctionalElement , axiom , ? [ A , B ] : ( r_interface_FunctionalElement ( A , B ) => ~ ? [ C , B ] : r_interface_FunctionalElement ( C , B ) ) ) .

-fof ( containment_noDup_r_rootElements_FunctionalArchitectureModel , axiom , ? [ A , B ] : ( r_rootElements_FunctionalArchitectureModel ( A , B ) => ~ ? [ C , B ] : r_rootElements_FunctionalArchitectureModel ( C , B ) ) ) .

-fof ( containment_noDup_r_subElements_Function , axiom , ? [ A , B ] : ( r_subElements_Function ( A , B ) => ~ ? [ C , B ] : r_subElements_Function ( C , B ) ) ) .

-fof ( containment_noDup_r_data_FunctionalInterface , axiom , ? [ A , B ] : ( r_data_FunctionalInterface ( A , B ) => ~ ? [ C , B ] : r_data_FunctionalInterface ( C , B ) ) ) .

-fof ( containment_noDup_r_outgoingLinks_FunctionalOutput , axiom , ? [ A , B ] : ( r_outgoingLinks_FunctionalOutput ( A , B ) => ~ ? [ C , B ] : r_outgoingLinks_FunctionalOutput ( C , B ) ) ) .

-fof ( containment_noDup_r_terminator_FunctionalData , axiom , ? [ A , B ] : ( r_terminator_FunctionalData ( A , B ) => ~ ? [ C , B ] : r_terminator_FunctionalData ( C , B ) ) ) .

-fof ( containment_t_FunctionalElement , axiom , ! [ A ] : ( t_FunctionalElement ( A ) => ? [ B ] : ( ( r_rootElements_FunctionalArchitectureModel ( B , A ) & ~ r_subElements_Function ( B , A ) ) | ( ~ r_rootElements_FunctionalArchitectureModel ( B , A ) & r_subElements_Function ( B , A ) ) ) ) ) .

-fof ( containment_t_FunctionalData , axiom , ! [ A ] : ( t_FunctionalData ( A ) => ? [ B ] : r_data_FunctionalInterface ( B , A ) ) ) .

-fof ( containment_t_InformationLink , axiom , ! [ A ] : ( t_InformationLink ( A ) => ? [ B ] : r_outgoingLinks_FunctionalOutput ( B , A ) ) ) .

-fof ( containment_t_FunctionalInterface , axiom , ! [ A ] : ( t_FunctionalInterface ( A ) => ? [ B ] : r_interface_FunctionalElement ( B , A ) ) ) .

-fof ( containment_t_FAMTerminator , axiom , ! [ A ] : ( t_FAMTerminator ( A ) => ? [ B ] : r_terminator_FunctionalData ( B , A ) ) ) .

-fof ( containment_noCycle_1 , axiom , ~ ? [ V1 ] : ( r_interface_FunctionalElement ( V1 , V1 ) | ( r_rootElements_FunctionalArchitectureModel ( V1 , V1 ) | ( r_subElements_Function ( V1 , V1 ) | ( r_data_FunctionalInterface ( V1 , V1 ) | ( r_outgoingLinks_FunctionalOutput ( V1 , V1 ) | r_terminator_FunctionalData ( V1 , V1 ) ) ) ) ) ) ) .

-fof ( containment_noCycle_2 , axiom , ~ ? [ V1 , V2 ] : ( ( r_interface_FunctionalElement ( V1 , V2 ) | ( r_rootElements_FunctionalArchitectureModel ( V1 , V2 ) | ( r_subElements_Function ( V1 , V2 ) | ( r_data_FunctionalInterface ( V1 , V2 ) | ( r_outgoingLinks_FunctionalOutput ( V1 , V2 ) | r_terminator_FunctionalData ( V1 , V2 ) ) ) ) ) ) & ( r_interface_FunctionalElement ( V2 , V1 ) | ( r_rootElements_FunctionalArchitectureModel ( V2 , V1 ) | ( r_subElements_Function ( V2 , V1 ) | ( r_data_FunctionalInterface ( V2 , V1 ) | ( r_outgoingLinks_FunctionalOutput ( V2 , V1 ) | r_terminator_FunctionalData ( V2 , V1 ) ) ) ) ) ) ) ) .

-fof ( containment_noCycle_3 , axiom , ~ ? [ V1 , V2 , V3 ] : ( ( r_interface_FunctionalElement ( V1 , V2 ) | ( r_rootElements_FunctionalArchitectureModel ( V1 , V2 ) | ( r_subElements_Function ( V1 , V2 ) | ( r_data_FunctionalInterface ( V1 , V2 ) | ( r_outgoingLinks_FunctionalOutput ( V1 , V2 ) | r_terminator_FunctionalData ( V1 , V2 ) ) ) ) ) ) & ( ( r_interface_FunctionalElement ( V2 , V3 ) | ( r_rootElements_FunctionalArchitectureModel ( V2 , V3 ) | ( r_subElements_Function ( V2 , V3 ) | ( r_data_FunctionalInterface ( V2 , V3 ) | ( r_outgoingLinks_FunctionalOutput ( V2 , V3 ) | r_terminator_FunctionalData ( V2 , V3 ) ) ) ) ) ) & ( r_interface_FunctionalElement ( V3 , V1 ) | ( r_rootElements_FunctionalArchitectureModel ( V3 , V1 ) | ( r_subElements_Function ( V3 , V1 ) | ( r_data_FunctionalInterface ( V3 , V1 ) | ( r_outgoingLinks_FunctionalOutput ( V3 , V1 ) | r_terminator_FunctionalData ( V3 , V1 ) ) ) ) ) ) ) ) ) .

-fof ( containment_noCycle_4 , axiom , ~ ? [ V1 , V2 , V3 , V4 ] : ( ( r_interface_FunctionalElement ( V1 , V2 ) | ( r_rootElements_FunctionalArchitectureModel ( V1 , V2 ) | ( r_subElements_Function ( V1 , V2 ) | ( r_data_FunctionalInterface ( V1 , V2 ) | ( r_outgoingLinks_FunctionalOutput ( V1 , V2 ) | r_terminator_FunctionalData ( V1 , V2 ) ) ) ) ) ) & ( ( r_interface_FunctionalElement ( V2 , V3 ) | ( r_rootElements_FunctionalArchitectureModel ( V2 , V3 ) | ( r_subElements_Function ( V2 , V3 ) | ( r_data_FunctionalInterface ( V2 , V3 ) | ( r_outgoingLinks_FunctionalOutput ( V2 , V3 ) | r_terminator_FunctionalData ( V2 , V3 ) ) ) ) ) ) & ( ( r_interface_FunctionalElement ( V3 , V4 ) | ( r_rootElements_FunctionalArchitectureModel ( V3 , V4 ) | ( r_subElements_Function ( V3 , V4 ) | ( r_data_FunctionalInterface ( V3 , V4 ) | ( r_outgoingLinks_FunctionalOutput ( V3 , V4 ) | r_terminator_FunctionalData ( V3 , V4 ) ) ) ) ) ) & ( r_interface_FunctionalElement ( V4 , V1 ) | ( r_rootElements_FunctionalArchitectureModel ( V4 , V1 ) | ( r_subElements_Function ( V4 , V1 ) | ( r_data_FunctionalInterface ( V4 , V1 ) | ( r_outgoingLinks_FunctionalOutput ( V4 , V1 ) | r_terminator_FunctionalData ( V4 , V1 ) ) ) ) ) ) ) ) ) ) .

-fof ( containment_noCycle_5 , axiom , ~ ? [ V1 , V2 , V3 , V4 , V5 ] : ( ( r_interface_FunctionalElement ( V1 , V2 ) | ( r_rootElements_FunctionalArchitectureModel ( V1 , V2 ) | ( r_subElements_Function ( V1 , V2 ) | ( r_data_FunctionalInterface ( V1 , V2 ) | ( r_outgoingLinks_FunctionalOutput ( V1 , V2 ) | r_terminator_FunctionalData ( V1 , V2 ) ) ) ) ) ) & ( ( r_interface_FunctionalElement ( V2 , V3 ) | ( r_rootElements_FunctionalArchitectureModel ( V2 , V3 ) | ( r_subElements_Function ( V2 , V3 ) | ( r_data_FunctionalInterface ( V2 , V3 ) | ( r_outgoingLinks_FunctionalOutput ( V2 , V3 ) | r_terminator_FunctionalData ( V2 , V3 ) ) ) ) ) ) & ( ( r_interface_FunctionalElement ( V3 , V4 ) | ( r_rootElements_FunctionalArchitectureModel ( V3 , V4 ) | ( r_subElements_Function ( V3 , V4 ) | ( r_data_FunctionalInterface ( V3 , V4 ) | ( r_outgoingLinks_FunctionalOutput ( V3 , V4 ) | r_terminator_FunctionalData ( V3 , V4 ) ) ) ) ) ) & ( ( r_interface_FunctionalElement ( V4 , V5 ) | ( r_rootElements_FunctionalArchitectureModel ( V4 , V5 ) | ( r_subElements_Function ( V4 , V5 ) | ( r_data_FunctionalInterface ( V4 , V5 ) | ( r_outgoingLinks_FunctionalOutput ( V4 , V5 ) | r_terminator_FunctionalData ( V4 , V5 ) ) ) ) ) ) & ( r_interface_FunctionalElement ( V5 , V1 ) | ( r_rootElements_FunctionalArchitectureModel ( V5 , V1 ) | ( r_subElements_Function ( V5 , V1 ) | ( r_data_FunctionalInterface ( V5 , V1 ) | ( r_outgoingLinks_FunctionalOutput ( V5 , V1 ) | r_terminator_FunctionalData ( V5 , V1 ) ) ) ) ) ) ) ) ) ) ) .

-fof ( upperMultiplicity_interface_FunctionalElement , axiom , ! [ V_src , V_trg_1 , V_trg_2 ] : ( ( t_FunctionalElement ( V_src ) & ( t_FunctionalInterface ( V_trg_1 ) & t_FunctionalInterface ( V_trg_2 ) ) ) => ( ( r_interface_FunctionalElement ( V_src , V_trg_1 ) & r_interface_FunctionalElement ( V_src , V_trg_2 ) ) => ~ V_trg_1 != V_trg_2 ) ) ) .

-fof ( lowerMultiplicity_model_FunctionalElement , axiom , ! [ V_src ] : ( t_FunctionalElement ( V_src ) => ? [ V_trg_1 ] : ( t_FunctionalArchitectureModel ( V_trg_1 ) & r_model_FunctionalElement ( V_src , V_trg_1 ) ) ) ) .

-fof ( upperMultiplicity_model_FunctionalElement , axiom , ! [ V_src , V_trg_1 , V_trg_2 ] : ( ( t_FunctionalElement ( V_src ) & ( t_FunctionalArchitectureModel ( V_trg_1 ) & t_FunctionalArchitectureModel ( V_trg_2 ) ) ) => ( ( r_model_FunctionalElement ( V_src , V_trg_1 ) & r_model_FunctionalElement ( V_src , V_trg_2 ) ) => ~ V_trg_1 != V_trg_2 ) ) ) .

-fof ( upperMultiplicity_parent_FunctionalElement , axiom , ! [ V_src , V_trg_1 , V_trg_2 ] : ( ( t_FunctionalElement ( V_src ) & ( t_Function ( V_trg_1 ) & t_Function ( V_trg_2 ) ) ) => ( ( r_parent_FunctionalElement ( V_src , V_trg_1 ) & r_parent_FunctionalElement ( V_src , V_trg_2 ) ) => ~ V_trg_1 != V_trg_2 ) ) ) .

-fof ( upperMultiplicity_data_FAMTerminator , axiom , ! [ V_src , V_trg_1 , V_trg_2 ] : ( ( t_FAMTerminator ( V_src ) & ( t_FunctionalData ( V_trg_1 ) & t_FunctionalData ( V_trg_2 ) ) ) => ( ( r_data_FAMTerminator ( V_src , V_trg_1 ) & r_data_FAMTerminator ( V_src , V_trg_2 ) ) => ~ V_trg_1 != V_trg_2 ) ) ) .

-fof ( upperMultiplicity_from_InformationLink , axiom , ! [ V_src , V_trg_1 , V_trg_2 ] : ( ( t_InformationLink ( V_src ) & ( t_FunctionalOutput ( V_trg_1 ) & t_FunctionalOutput ( V_trg_2 ) ) ) => ( ( r_from_InformationLink ( V_src , V_trg_1 ) & r_from_InformationLink ( V_src , V_trg_2 ) ) => ~ V_trg_1 != V_trg_2 ) ) ) .

-fof ( lowerMultiplicity_to_InformationLink , axiom , ! [ V_src ] : ( t_InformationLink ( V_src ) => ? [ V_trg_1 ] : ( t_FunctionalInput ( V_trg_1 ) & r_to_InformationLink ( V_src , V_trg_1 ) ) ) ) .

-fof ( upperMultiplicity_to_InformationLink , axiom , ! [ V_src , V_trg_1 , V_trg_2 ] : ( ( t_InformationLink ( V_src ) & ( t_FunctionalInput ( V_trg_1 ) & t_FunctionalInput ( V_trg_2 ) ) ) => ( ( r_to_InformationLink ( V_src , V_trg_1 ) & r_to_InformationLink ( V_src , V_trg_2 ) ) => ~ V_trg_1 != V_trg_2 ) ) ) .

-fof ( upperMultiplicity_element_FunctionalInterface , axiom , ! [ V_src , V_trg_1 , V_trg_2 ] : ( ( t_FunctionalInterface ( V_src ) & ( t_FunctionalElement ( V_trg_1 ) & t_FunctionalElement ( V_trg_2 ) ) ) => ( ( r_element_FunctionalInterface ( V_src , V_trg_1 ) & r_element_FunctionalInterface ( V_src , V_trg_2 ) ) => ~ V_trg_1 != V_trg_2 ) ) ) .

-fof ( upperMultiplicity_terminator_FunctionalData , axiom , ! [ V_src , V_trg_1 , V_trg_2 ] : ( ( t_FunctionalData ( V_src ) & ( t_FAMTerminator ( V_trg_1 ) & t_FAMTerminator ( V_trg_2 ) ) ) => ( ( r_terminator_FunctionalData ( V_src , V_trg_1 ) & r_terminator_FunctionalData ( V_src , V_trg_2 ) ) => ~ V_trg_1 != V_trg_2 ) ) ) .

-fof ( upperMultiplicity_interface_FunctionalData , axiom , ! [ V_src , V_trg_1 , V_trg_2 ] : ( ( t_FunctionalData ( V_src ) & ( t_FunctionalInterface ( V_trg_1 ) & t_FunctionalInterface ( V_trg_2 ) ) ) => ( ( r_interface_FunctionalData ( V_src , V_trg_1 ) & r_interface_FunctionalData ( V_src , V_trg_2 ) ) => ~ V_trg_1 != V_trg_2 ) ) ) .

-fof ( oppositeReference_interface_FunctionalElement , axiom , ! [ V_src , V_trg ] : ( ( t_FunctionalElement ( V_src ) & t_FunctionalInterface ( V_trg ) ) => ( r_interface_FunctionalElement ( V_src , V_trg ) <=> r_element_FunctionalInterface ( V_trg , V_src ) ) ) ) .

-fof ( oppositeReference_parent_FunctionalElement , axiom , ! [ V_src , V_trg ] : ( ( t_FunctionalElement ( V_src ) & t_Function ( V_trg ) ) => ( r_parent_FunctionalElement ( V_src , V_trg ) <=> r_subElements_Function ( V_trg , V_src ) ) ) ) .

-fof ( oppositeReference_data_FAMTerminator , axiom , ! [ V_src , V_trg ] : ( ( t_FAMTerminator ( V_src ) & t_FunctionalData ( V_trg ) ) => ( r_data_FAMTerminator ( V_src , V_trg ) <=> r_terminator_FunctionalData ( V_trg , V_src ) ) ) ) .

-fof ( oppositeReference_from_InformationLink , axiom , ! [ V_src , V_trg ] : ( ( t_InformationLink ( V_src ) & t_FunctionalOutput ( V_trg ) ) => ( r_from_InformationLink ( V_src , V_trg ) <=> r_outgoingLinks_FunctionalOutput ( V_trg , V_src ) ) ) ) .

-fof ( oppositeReference_to_InformationLink , axiom , ! [ V_src , V_trg ] : ( ( t_InformationLink ( V_src ) & t_FunctionalInput ( V_trg ) ) => ( r_to_InformationLink ( V_src , V_trg ) <=> r_IncomingLinks_FunctionalInput ( V_trg , V_src ) ) ) ) .

-fof ( oppositeReference_data_FunctionalInterface , axiom , ! [ V_src , V_trg ] : ( ( t_FunctionalInterface ( V_src ) & t_FunctionalData ( V_trg ) ) => ( r_data_FunctionalInterface ( V_src , V_trg ) <=> r_interface_FunctionalData ( V_trg , V_src ) ) ) ) .

-fof ( lowerMultiplicity_type_Function , axiom , ! [ V_src ] : ( t_Function ( V_src ) => ? [ V_trg_1 ] : ( t_FunctionType ( V_trg_1 ) & r_type_Function ( V_src , V_trg_1 ) ) ) ) .

-fof ( upperMultiplicity_type_Function , axiom , ! [ V_src , V_trg_1 , V_trg_2 ] : ( ( t_Function ( V_src ) & ( t_FunctionType ( V_trg_1 ) & t_FunctionType ( V_trg_2 ) ) ) => ( ( r_type_Function ( V_src , V_trg_1 ) & r_type_Function ( V_src , V_trg_2 ) ) => ~ V_trg_1 != V_trg_2 ) ) ) .