diff options
author | ArenBabikian <aren.babikian@mail.mcgill.ca> | 2019-04-15 00:06:29 -0400 |
---|---|---|
committer | ArenBabikian <aren.babikian@mail.mcgill.ca> | 2020-06-07 19:36:48 -0400 |
commit | 85e6d0b8590f5aa22cd7065cb850b0f460da25dd (patch) | |
tree | fcc945827435f113aa9099d0be63d68551f7f5a3 /Tests/ca.mcgill.ecse.dslreasoner.vampire.test/output | |
parent | VAMPIRE: #39 Reorganise tests, working yakindu test, need debugging (diff) | |
download | VIATRA-Generator-85e6d0b8590f5aa22cd7065cb850b0f460da25dd.tar.gz VIATRA-Generator-85e6d0b8590f5aa22cd7065cb850b0f460da25dd.tar.zst VIATRA-Generator-85e6d0b8590f5aa22cd7065cb850b0f460da25dd.zip |
Diffstat (limited to 'Tests/ca.mcgill.ecse.dslreasoner.vampire.test/output')
-rw-r--r-- | Tests/ca.mcgill.ecse.dslreasoner.vampire.test/output/FAMTest/Fam.logicproblem | 7 | ||||
-rw-r--r-- | Tests/ca.mcgill.ecse.dslreasoner.vampire.test/output/FAMTest/vampireProblem.tptp | 72 |
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 @@ | |||
1 | <?xml version="1.0" encoding="ASCII"?> | 1 | <?xml version="1.0" encoding="ASCII"?> |
2 | <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"> | 2 | <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"> |
3 | <types xsi:type="language_1:TypeDeclaration" name="FunctionalElement class" subtypes="//@types.2" isAbstract="true"/> | 3 | <types xsi:type="language_1:TypeDeclaration" name="FunctionalElement class" subtypes="//@types.2" isAbstract="true"/> |
4 | <types xsi:type="language_1:TypeDeclaration" name="FunctionalArchitectureModel class"/> | 4 | <types xsi:type="language_1:TypeDeclaration" name="FunctionalArchitectureModel class" subtypes="//@types.10 //@types.11" isAbstract="true"/> |
5 | <types xsi:type="language_1:TypeDeclaration" name="Function class" supertypes="//@types.0"/> | 5 | <types xsi:type="language_1:TypeDeclaration" name="Function class" supertypes="//@types.0"/> |
6 | <types xsi:type="language_1:TypeDeclaration" name="FAMTerminator class"/> | 6 | <types xsi:type="language_1:TypeDeclaration" name="FAMTerminator class"/> |
7 | <types xsi:type="language_1:TypeDeclaration" name="InformationLink class"/> | 7 | <types xsi:type="language_1:TypeDeclaration" name="InformationLink class"/> |
@@ -10,6 +10,8 @@ | |||
10 | <types xsi:type="language_1:TypeDeclaration" name="FunctionalOutput class" supertypes="//@types.8"/> | 10 | <types xsi:type="language_1:TypeDeclaration" name="FunctionalOutput class" supertypes="//@types.8"/> |
11 | <types xsi:type="language_1:TypeDeclaration" name="FunctionalData class" subtypes="//@types.6 //@types.7" isAbstract="true"/> | 11 | <types xsi:type="language_1:TypeDeclaration" name="FunctionalData class" subtypes="//@types.6 //@types.7" isAbstract="true"/> |
12 | <types xsi:type="language_1:TypeDefinition" name="FunctionType enum" elements="//@elements.0 //@elements.1 //@elements.2"/> | 12 | <types xsi:type="language_1:TypeDefinition" name="FunctionType enum" elements="//@elements.0 //@elements.1 //@elements.2"/> |
13 | <types xsi:type="language_1:TypeDefinition" name="FunctionalArchitectureModel class DefinedPart" supertypes="//@types.1" elements="//@elements.3"/> | ||
14 | <types xsi:type="language_1:TypeDeclaration" name="FunctionalArchitectureModel class UndefinedPart" supertypes="//@types.1"/> | ||
13 | <assertions name="upperMultiplicity interface FunctionalElement" annotations="//@annotations.0"> | 15 | <assertions name="upperMultiplicity interface FunctionalElement" annotations="//@annotations.0"> |
14 | <value xsi:type="language_1:Forall"> | 16 | <value xsi:type="language_1:Forall"> |
15 | <quantifiedVariables name="src"> | 17 | <quantifiedVariables name="src"> |
@@ -557,7 +559,8 @@ | |||
557 | <elements name="Root literal FunctionType" definedInType="//@types.9"/> | 559 | <elements name="Root literal FunctionType" definedInType="//@types.9"/> |
558 | <elements name="Intermediate literal FunctionType" definedInType="//@types.9"/> | 560 | <elements name="Intermediate literal FunctionType" definedInType="//@types.9"/> |
559 | <elements name="Leaf literal FunctionType" definedInType="//@types.9"/> | 561 | <elements name="Leaf literal FunctionType" definedInType="//@types.9"/> |
560 | <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"/> | 562 | <elements name="o 1" definedInType="//@types.10"/> |
563 | <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"/> | ||
561 | <annotations xsi:type="ecore2logicannotations:UpperMultiplicityAssertion" target="//@assertions.0" relation="//@relations.0" upper="1"/> | 564 | <annotations xsi:type="ecore2logicannotations:UpperMultiplicityAssertion" target="//@assertions.0" relation="//@relations.0" upper="1"/> |
562 | <annotations xsi:type="ecore2logicannotations:LowerMultiplicityAssertion" target="//@assertions.1" relation="//@relations.1" lower="1"/> | 565 | <annotations xsi:type="ecore2logicannotations:LowerMultiplicityAssertion" target="//@assertions.1" relation="//@relations.1" lower="1"/> |
563 | <annotations xsi:type="ecore2logicannotations:UpperMultiplicityAssertion" target="//@assertions.2" relation="//@relations.1" upper="1"/> | 566 | <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 @@ | |||
1 | % This is an initial Test Comment | ||
2 | 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 ) ) ) ) ) ) ) ) . | ||
3 | fof ( enumScope_FunctionType_Root , axiom , ! [ A ] : ( A = eo1 <=> e_Root_FunctionType ( A ) ) ) . | ||
4 | fof ( enumScope_FunctionType_Intermediate , axiom , ! [ A ] : ( A = eo2 <=> e_Intermediate_FunctionType ( A ) ) ) . | ||
5 | fof ( enumScope_FunctionType_Leaf , axiom , ! [ A ] : ( A = eo3 <=> e_Leaf_FunctionType ( A ) ) ) . | ||
6 | 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 ) ) ) ) ) ) ) ) ) ) ) ) . | ||
7 | 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 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) . | ||
8 | fof ( typeScope_min_object , axiom , ! [ A ] : ( ( A = o1 | ( A = o2 | ( A = o3 | ( A = o4 | ( A = eo1 | ( A = eo2 | A = eo3 ) ) ) ) ) ) => object ( A ) ) ) . | ||
9 | fof ( typeScope_max_object , axiom , ! [ A ] : ( object ( A ) => ( A = eo1 | ( A = eo2 | ( A = eo3 | ( A = o1 | ( A = o2 | ( A = o3 | ( A = o4 | A = o5 ) ) ) ) ) ) ) ) ) . | ||
10 | fof ( typeScope_min_t_Function , axiom , ! [ A ] : ( A = o2 => ( t_Function ( A ) & object ( A ) ) ) ) . | ||
11 | fof ( typeScope_min_t_FunctionalOutput , axiom , ! [ A ] : ( ( A = o3 | ( A = o4 | A = o5 ) ) => ( t_FunctionalOutput ( A ) & object ( A ) ) ) ) . | ||
12 | fof ( typeScope_min_t_FunctionalInterface , axiom , ! [ A ] : ( ( A = o6 | A = o7 ) => ( t_FunctionalInterface ( A ) & object ( A ) ) ) ) . | ||
13 | fof ( typeScope_max_t_Function , axiom , ! [ A ] : ( ( t_Function ( A ) & object ( A ) ) => A = o2 ) ) . | ||
14 | fof ( typeScope_max_t_FunctionalOutput , axiom , ! [ A ] : ( ( t_FunctionalOutput ( A ) & object ( A ) ) => ( A = o3 | ( A = o4 | A = o5 ) ) ) ) . | ||
15 | fof ( t_uniqueness_eo1 , axiom , eo1 != eo2 & ( eo1 != eo3 & ( eo1 != o1 & ( eo1 != o2 & ( eo1 != o3 & ( eo1 != o4 & eo1 != o5 ) ) ) ) ) ) . | ||
16 | fof ( t_uniqueness_eo2 , axiom , eo2 != eo3 & ( eo2 != o1 & ( eo2 != o2 & ( eo2 != o3 & ( eo2 != o4 & eo2 != o5 ) ) ) ) ) . | ||
17 | fof ( t_uniqueness_eo3 , axiom , eo3 != o1 & ( eo3 != o2 & ( eo3 != o3 & ( eo3 != o4 & eo3 != o5 ) ) ) ) . | ||
18 | fof ( t_uniqueness_o1 , axiom , o1 != o2 & ( o1 != o3 & ( o1 != o4 & o1 != o5 ) ) ) . | ||
19 | fof ( t_uniqueness_o2 , axiom , o2 != o3 & ( o2 != o4 & o2 != o5 ) ) . | ||
20 | fof ( t_uniqueness_o3 , axiom , o3 != o4 & o3 != o5 ) . | ||
21 | fof ( t_uniqueness_o4 , axiom , o4 != o5 ) . | ||
22 | fof ( compliance_interface_FunctionalElement , axiom , ! [ V_0 , V_1 ] : ( r_interface_FunctionalElement ( V_0 , V_1 ) => ( t_FunctionalElement ( V_0 ) & t_FunctionalInterface ( V_1 ) ) ) ) . | ||
23 | fof ( compliance_model_FunctionalElement , axiom , ! [ V_0 , V_1 ] : ( r_model_FunctionalElement ( V_0 , V_1 ) => ( t_FunctionalElement ( V_0 ) & t_FunctionalArchitectureModel ( V_1 ) ) ) ) . | ||
24 | fof ( compliance_parent_FunctionalElement , axiom , ! [ V_0 , V_1 ] : ( r_parent_FunctionalElement ( V_0 , V_1 ) => ( t_FunctionalElement ( V_0 ) & t_Function ( V_1 ) ) ) ) . | ||
25 | fof ( compliance_rootElements_FunctionalArchitectureModel , axiom , ! [ V_0 , V_1 ] : ( r_rootElements_FunctionalArchitectureModel ( V_0 , V_1 ) => ( t_FunctionalArchitectureModel ( V_0 ) & t_FunctionalElement ( V_1 ) ) ) ) . | ||
26 | fof ( compliance_subElements_Function , axiom , ! [ V_0 , V_1 ] : ( r_subElements_Function ( V_0 , V_1 ) => ( t_Function ( V_0 ) & t_FunctionalElement ( V_1 ) ) ) ) . | ||
27 | fof ( compliance_data_FAMTerminator , axiom , ! [ V_0 , V_1 ] : ( r_data_FAMTerminator ( V_0 , V_1 ) => ( t_FAMTerminator ( V_0 ) & t_FunctionalData ( V_1 ) ) ) ) . | ||
28 | fof ( compliance_from_InformationLink , axiom , ! [ V_0 , V_1 ] : ( r_from_InformationLink ( V_0 , V_1 ) => ( t_InformationLink ( V_0 ) & t_FunctionalOutput ( V_1 ) ) ) ) . | ||
29 | fof ( compliance_to_InformationLink , axiom , ! [ V_0 , V_1 ] : ( r_to_InformationLink ( V_0 , V_1 ) => ( t_InformationLink ( V_0 ) & t_FunctionalInput ( V_1 ) ) ) ) . | ||
30 | fof ( compliance_data_FunctionalInterface , axiom , ! [ V_0 , V_1 ] : ( r_data_FunctionalInterface ( V_0 , V_1 ) => ( t_FunctionalInterface ( V_0 ) & t_FunctionalData ( V_1 ) ) ) ) . | ||
31 | fof ( compliance_element_FunctionalInterface , axiom , ! [ V_0 , V_1 ] : ( r_element_FunctionalInterface ( V_0 , V_1 ) => ( t_FunctionalInterface ( V_0 ) & t_FunctionalElement ( V_1 ) ) ) ) . | ||
32 | fof ( compliance_IncomingLinks_FunctionalInput , axiom , ! [ V_0 , V_1 ] : ( r_IncomingLinks_FunctionalInput ( V_0 , V_1 ) => ( t_FunctionalInput ( V_0 ) & t_InformationLink ( V_1 ) ) ) ) . | ||
33 | fof ( compliance_outgoingLinks_FunctionalOutput , axiom , ! [ V_0 , V_1 ] : ( r_outgoingLinks_FunctionalOutput ( V_0 , V_1 ) => ( t_FunctionalOutput ( V_0 ) & t_InformationLink ( V_1 ) ) ) ) . | ||
34 | fof ( compliance_terminator_FunctionalData , axiom , ! [ V_0 , V_1 ] : ( r_terminator_FunctionalData ( V_0 , V_1 ) => ( t_FunctionalData ( V_0 ) & t_FAMTerminator ( V_1 ) ) ) ) . | ||
35 | fof ( compliance_interface_FunctionalData , axiom , ! [ V_0 , V_1 ] : ( r_interface_FunctionalData ( V_0 , V_1 ) => ( t_FunctionalData ( V_0 ) & t_FunctionalInterface ( V_1 ) ) ) ) . | ||
36 | fof ( compliance_type_Function , axiom , ! [ V_0 , V_1 ] : ( r_type_Function ( V_0 , V_1 ) => ( t_Function ( V_0 ) & t_FunctionType ( V_1 ) ) ) ) . | ||
37 | fof ( containment_topLevel_t_FunctionalArchitectureModel , axiom , ! [ A ] : ( t_FunctionalArchitectureModel ( A ) <=> A = o1 ) ) . | ||
38 | fof ( containment_noDup_r_interface_FunctionalElement , axiom , ? [ A , B ] : ( r_interface_FunctionalElement ( A , B ) => ~ ? [ C , B ] : r_interface_FunctionalElement ( C , B ) ) ) . | ||
39 | fof ( containment_noDup_r_rootElements_FunctionalArchitectureModel , axiom , ? [ A , B ] : ( r_rootElements_FunctionalArchitectureModel ( A , B ) => ~ ? [ C , B ] : r_rootElements_FunctionalArchitectureModel ( C , B ) ) ) . | ||
40 | fof ( containment_noDup_r_subElements_Function , axiom , ? [ A , B ] : ( r_subElements_Function ( A , B ) => ~ ? [ C , B ] : r_subElements_Function ( C , B ) ) ) . | ||
41 | fof ( containment_noDup_r_data_FunctionalInterface , axiom , ? [ A , B ] : ( r_data_FunctionalInterface ( A , B ) => ~ ? [ C , B ] : r_data_FunctionalInterface ( C , B ) ) ) . | ||
42 | fof ( containment_noDup_r_outgoingLinks_FunctionalOutput , axiom , ? [ A , B ] : ( r_outgoingLinks_FunctionalOutput ( A , B ) => ~ ? [ C , B ] : r_outgoingLinks_FunctionalOutput ( C , B ) ) ) . | ||
43 | fof ( containment_noDup_r_terminator_FunctionalData , axiom , ? [ A , B ] : ( r_terminator_FunctionalData ( A , B ) => ~ ? [ C , B ] : r_terminator_FunctionalData ( C , B ) ) ) . | ||
44 | 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 ) ) ) ) ) . | ||
45 | fof ( containment_t_FunctionalData , axiom , ! [ A ] : ( t_FunctionalData ( A ) => ? [ B ] : r_data_FunctionalInterface ( B , A ) ) ) . | ||
46 | fof ( containment_t_InformationLink , axiom , ! [ A ] : ( t_InformationLink ( A ) => ? [ B ] : r_outgoingLinks_FunctionalOutput ( B , A ) ) ) . | ||
47 | fof ( containment_t_FunctionalInterface , axiom , ! [ A ] : ( t_FunctionalInterface ( A ) => ? [ B ] : r_interface_FunctionalElement ( B , A ) ) ) . | ||
48 | fof ( containment_t_FAMTerminator , axiom , ! [ A ] : ( t_FAMTerminator ( A ) => ? [ B ] : r_terminator_FunctionalData ( B , A ) ) ) . | ||
49 | 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 ) ) ) ) ) ) ) . | ||
50 | 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 ) ) ) ) ) ) ) ) . | ||
51 | 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 ) ) ) ) ) ) ) ) ) . | ||
52 | 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 ) ) ) ) ) ) ) ) ) ) . | ||
53 | 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 ) ) ) ) ) ) ) ) ) ) ) . | ||
54 | 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 ) ) ) . | ||
55 | 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 ) ) ) ) . | ||
56 | 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 ) ) ) . | ||
57 | 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 ) ) ) . | ||
58 | 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 ) ) ) . | ||
59 | 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 ) ) ) . | ||
60 | 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 ) ) ) ) . | ||
61 | 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 ) ) ) . | ||
62 | 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 ) ) ) . | ||
63 | 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 ) ) ) . | ||
64 | 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 ) ) ) . | ||
65 | 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 ) ) ) ) . | ||
66 | 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 ) ) ) ) . | ||
67 | 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 ) ) ) ) . | ||
68 | 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 ) ) ) ) . | ||
69 | 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 ) ) ) ) . | ||
70 | 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 ) ) ) ) . | ||
71 | 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 ) ) ) ) . | ||
72 | 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 ) ) ) . | ||