aboutsummaryrefslogtreecommitdiffstats
path: root/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/output/FAMTest/vampireProblem.tptp
diff options
context:
space:
mode:
Diffstat (limited to 'Tests/ca.mcgill.ecse.dslreasoner.vampire.test/output/FAMTest/vampireProblem.tptp')
-rw-r--r--Tests/ca.mcgill.ecse.dslreasoner.vampire.test/output/FAMTest/vampireProblem.tptp22
1 files changed, 13 insertions, 9 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 3109ccc2..5c3ef527 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
@@ -5,13 +5,13 @@ fof ( enumScope_FunctionType_Intermediate , axiom , ! [ A ] : ( A = eo2 <=> e_In
5fof ( enumScope_FunctionType_Leaf , axiom , ! [ A ] : ( A = eo3 <=> e_Leaf_FunctionType ( A ) ) ) . 5fof ( enumScope_FunctionType_Leaf , axiom , ! [ A ] : ( A = eo3 <=> e_Leaf_FunctionType ( A ) ) ) .
6fof ( inheritanceHierarchyHandler , axiom , ! [ A ] : ( object ( A ) <=> ( ( t_FAMTerminator ( A ) & ( ~ t_FunctionalData ( A ) & ( ~ t_FunctionalInterface ( A ) & ( ~ t_Function ( A ) & ( ~ t_InformationLink ( A ) & ( ~ t_FunctionalElement ( A ) & ( ~ t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionType ( A ) & ( ~ t_FunctionalInput ( A ) & ~ t_FunctionalOutput ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_FAMTerminator ( A ) & ( ~ t_FunctionalData ( A ) & ( t_FunctionalInterface ( A ) & ( ~ t_Function ( A ) & ( ~ t_InformationLink ( A ) & ( ~ t_FunctionalElement ( A ) & ( ~ t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionType ( A ) & ( ~ t_FunctionalInput ( A ) & ~ t_FunctionalOutput ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_FAMTerminator ( A ) & ( ~ t_FunctionalData ( A ) & ( ~ t_FunctionalInterface ( A ) & ( t_Function ( A ) & ( ~ t_InformationLink ( A ) & ( t_FunctionalElement ( A ) & ( ~ t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionType ( A ) & ( ~ t_FunctionalInput ( A ) & ~ t_FunctionalOutput ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_FAMTerminator ( A ) & ( ~ t_FunctionalData ( A ) & ( ~ t_FunctionalInterface ( A ) & ( ~ t_Function ( A ) & ( t_InformationLink ( A ) & ( ~ t_FunctionalElement ( A ) & ( ~ t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionType ( A ) & ( ~ t_FunctionalInput ( A ) & ~ t_FunctionalOutput ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_FAMTerminator ( A ) & ( ~ t_FunctionalData ( A ) & ( ~ t_FunctionalInterface ( A ) & ( ~ t_Function ( A ) & ( ~ t_InformationLink ( A ) & ( ~ t_FunctionalElement ( A ) & ( t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionType ( A ) & ( ~ t_FunctionalInput ( A ) & ~ t_FunctionalOutput ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_FAMTerminator ( A ) & ( ~ t_FunctionalData ( A ) & ( ~ t_FunctionalInterface ( A ) & ( ~ t_Function ( A ) & ( ~ t_InformationLink ( A ) & ( ~ t_FunctionalElement ( A ) & ( ~ t_FunctionalArchitectureModel ( A ) & ( t_FunctionType ( A ) & ( ~ t_FunctionalInput ( A ) & ~ t_FunctionalOutput ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_FAMTerminator ( A ) & ( t_FunctionalData ( A ) & ( ~ t_FunctionalInterface ( A ) & ( ~ t_Function ( A ) & ( ~ t_InformationLink ( A ) & ( ~ t_FunctionalElement ( A ) & ( ~ t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionType ( A ) & ( t_FunctionalInput ( A ) & ~ t_FunctionalOutput ( A ) ) ) ) ) ) ) ) ) ) | ( ~ t_FAMTerminator ( A ) & ( t_FunctionalData ( A ) & ( ~ t_FunctionalInterface ( A ) & ( ~ t_Function ( A ) & ( ~ t_InformationLink ( A ) & ( ~ t_FunctionalElement ( A ) & ( ~ t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionType ( A ) & ( ~ t_FunctionalInput ( A ) & t_FunctionalOutput ( A ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) . 6fof ( inheritanceHierarchyHandler , axiom , ! [ A ] : ( object ( A ) <=> ( ( t_FAMTerminator ( A ) & ( ~ t_FunctionalData ( A ) & ( ~ t_FunctionalInterface ( A ) & ( ~ t_Function ( A ) & ( ~ t_InformationLink ( A ) & ( ~ t_FunctionalElement ( A ) & ( ~ t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionType ( A ) & ( ~ t_FunctionalInput ( A ) & ~ t_FunctionalOutput ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_FAMTerminator ( A ) & ( ~ t_FunctionalData ( A ) & ( t_FunctionalInterface ( A ) & ( ~ t_Function ( A ) & ( ~ t_InformationLink ( A ) & ( ~ t_FunctionalElement ( A ) & ( ~ t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionType ( A ) & ( ~ t_FunctionalInput ( A ) & ~ t_FunctionalOutput ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_FAMTerminator ( A ) & ( ~ t_FunctionalData ( A ) & ( ~ t_FunctionalInterface ( A ) & ( t_Function ( A ) & ( ~ t_InformationLink ( A ) & ( t_FunctionalElement ( A ) & ( ~ t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionType ( A ) & ( ~ t_FunctionalInput ( A ) & ~ t_FunctionalOutput ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_FAMTerminator ( A ) & ( ~ t_FunctionalData ( A ) & ( ~ t_FunctionalInterface ( A ) & ( ~ t_Function ( A ) & ( t_InformationLink ( A ) & ( ~ t_FunctionalElement ( A ) & ( ~ t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionType ( A ) & ( ~ t_FunctionalInput ( A ) & ~ t_FunctionalOutput ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_FAMTerminator ( A ) & ( ~ t_FunctionalData ( A ) & ( ~ t_FunctionalInterface ( A ) & ( ~ t_Function ( A ) & ( ~ t_InformationLink ( A ) & ( ~ t_FunctionalElement ( A ) & ( t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionType ( A ) & ( ~ t_FunctionalInput ( A ) & ~ t_FunctionalOutput ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_FAMTerminator ( A ) & ( ~ t_FunctionalData ( A ) & ( ~ t_FunctionalInterface ( A ) & ( ~ t_Function ( A ) & ( ~ t_InformationLink ( A ) & ( ~ t_FunctionalElement ( A ) & ( ~ t_FunctionalArchitectureModel ( A ) & ( t_FunctionType ( A ) & ( ~ t_FunctionalInput ( A ) & ~ t_FunctionalOutput ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_FAMTerminator ( A ) & ( t_FunctionalData ( A ) & ( ~ t_FunctionalInterface ( A ) & ( ~ t_Function ( A ) & ( ~ t_InformationLink ( A ) & ( ~ t_FunctionalElement ( A ) & ( ~ t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionType ( A ) & ( t_FunctionalInput ( A ) & ~ t_FunctionalOutput ( A ) ) ) ) ) ) ) ) ) ) | ( ~ t_FAMTerminator ( A ) & ( t_FunctionalData ( A ) & ( ~ t_FunctionalInterface ( A ) & ( ~ t_Function ( A ) & ( ~ t_InformationLink ( A ) & ( ~ t_FunctionalElement ( A ) & ( ~ t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionType ( A ) & ( ~ t_FunctionalInput ( A ) & t_FunctionalOutput ( A ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) .
7fof ( typeScope_min_object , axiom , ! [ A ] : ( ( A = o1 | ( A = o2 | ( A = o3 | ( A = o4 | ( A = o5 | ( A = o6 | ( A = eo1 | ( A = eo2 | A = eo3 ) ) ) ) ) ) ) ) => object ( A ) ) ) . 7fof ( typeScope_min_object , axiom , ! [ A ] : ( ( A = o1 | ( A = o2 | ( A = o3 | ( A = o4 | ( A = o5 | ( A = o6 | ( A = eo1 | ( A = eo2 | A = eo3 ) ) ) ) ) ) ) ) => object ( A ) ) ) .
8fof ( typeScope_max_object , axiom , ! [ A ] : ( object ( A ) => ( A = eo1 | ( A = eo2 | ( A = eo3 | ( A = o1 | ( A = o2 | ( A = o3 | ( A = o4 | ( A = o5 | ( A = o6 | ( A = o7 | A = o8 ) ) ) ) ) ) ) ) ) ) ) ) . 8fof ( typeScope_max_object , axiom , ! [ A ] : ( object ( A ) => ( A = eo1 | ( A = eo2 | ( A = eo3 | ( A = o1 | ( A = o2 | ( A = o3 | ( A = o4 | ( A = o5 | ( A = o6 | ( A = o7 | ( A = o8 | ( A = o9 | ( A = o10 | ( A = o11 | ( A = o12 | ( A = o13 | ( A = o14 | ( A = o15 | ( A = o16 | ( A = o17 | ( A = o18 | ( A = o19 | ( A = o20 | ( A = o21 | ( A = o22 | ( A = o23 | ( A = o24 | ( A = o25 | ( A = o26 | ( A = o27 | ( A = o28 | ( A = o29 | ( A = o30 | ( A = o31 | ( A = o32 | ( A = o33 | ( A = o34 | ( A = o35 | ( A = o36 | ( A = o37 | ( A = o38 | ( A = o39 | A = o40 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) .
9fof ( typeScope_min_t_FunctionalInterface , axiom , ! [ A ] : ( ( A = o2 | A = o3 ) => ( t_FunctionalInterface ( A ) & object ( A ) ) ) ) . 9fof ( typeScope_min_t_FunctionalInterface , axiom , ! [ A ] : ( ( A = o2 | A = o3 ) => ( t_FunctionalInterface ( A ) & object ( A ) ) ) ) .
10fof ( typeScope_min_t_Function , axiom , ! [ A ] : ( A = o4 => ( t_Function ( A ) & object ( A ) ) ) ) . 10fof ( typeScope_min_t_Function , axiom , ! [ A ] : ( A = o4 => ( t_Function ( A ) & object ( A ) ) ) ) .
11fof ( typeScope_min_t_FunctionalOutput , axiom , ! [ A ] : ( ( A = o5 | ( A = o6 | A = o7 ) ) => ( t_FunctionalOutput ( A ) & object ( A ) ) ) ) . 11fof ( typeScope_min_t_FunctionalOutput , axiom , ! [ A ] : ( ( A = o5 | ( A = o6 | A = o7 ) ) => ( t_FunctionalOutput ( A ) & object ( A ) ) ) ) .
12fof ( typeScope_max_t_Function , axiom , ! [ A ] : ( ( t_Function ( A ) & object ( A ) ) => ( A = o4 | A = o8 ) ) ) . 12fof ( typeScope_max_t_Function , axiom , ! [ A ] : ( ( t_Function ( A ) & object ( A ) ) => ( A = o4 | ( A = o8 | ( A = o9 | ( A = o10 | A = o11 ) ) ) ) ) ) .
13fof ( typeScope_max_t_FunctionalOutput , axiom , ! [ A ] : ( ( t_FunctionalOutput ( A ) & object ( A ) ) => ( A = o5 | ( A = o6 | ( A = o7 | A = o8 ) ) ) ) ) . 13fof ( typeScope_max_t_FunctionalOutput , axiom , ! [ A ] : ( ( t_FunctionalOutput ( A ) & object ( A ) ) => ( A = o5 | ( A = o6 | ( A = o7 | A = o8 ) ) ) ) ) .
14fof ( typeUniqueness , axiom , eo1 != eo2 & ( eo1 != eo3 & ( eo2 != eo3 & ( eo1 != o1 & ( eo2 != o1 & ( eo3 != o1 & ( eo1 != o2 & ( eo2 != o2 & ( eo3 != o2 & ( o1 != o2 & ( eo1 != o3 & ( eo2 != o3 & ( eo3 != o3 & ( o1 != o3 & ( o2 != o3 & ( eo1 != o4 & ( eo2 != o4 & ( eo3 != o4 & ( o1 != o4 & ( o2 != o4 & ( o3 != o4 & ( eo1 != o5 & ( eo2 != o5 & ( eo3 != o5 & ( o1 != o5 & ( o2 != o5 & ( o3 != o5 & ( o4 != o5 & ( eo1 != o6 & ( eo2 != o6 & ( eo3 != o6 & ( o1 != o6 & ( o2 != o6 & ( o3 != o6 & ( o4 != o6 & ( o5 != o6 & ( eo1 != o7 & ( eo2 != o7 & ( eo3 != o7 & ( o1 != o7 & ( o2 != o7 & ( o3 != o7 & ( o4 != o7 & ( o5 != o7 & ( o6 != o7 & ( eo1 != o8 & ( eo2 != o8 & ( eo3 != o8 & ( o1 != o8 & ( o2 != o8 & ( o3 != o8 & ( o4 != o8 & ( o5 != o8 & ( o6 != o8 & o7 != o8 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) . 14fof ( typeUniqueness , axiom , eo1 != eo2 & ( eo1 != eo3 & ( eo2 != eo3 & ( eo1 != o1 & ( eo2 != o1 & ( eo3 != o1 & ( eo1 != o2 & ( eo2 != o2 & ( eo3 != o2 & ( o1 != o2 & ( eo1 != o3 & ( eo2 != o3 & ( eo3 != o3 & ( o1 != o3 & ( o2 != o3 & ( eo1 != o4 & ( eo2 != o4 & ( eo3 != o4 & ( o1 != o4 & ( o2 != o4 & ( o3 != o4 & ( eo1 != o5 & ( eo2 != o5 & ( eo3 != o5 & ( o1 != o5 & ( o2 != o5 & ( o3 != o5 & ( o4 != o5 & ( eo1 != o6 & ( eo2 != o6 & ( eo3 != o6 & ( o1 != o6 & ( o2 != o6 & ( o3 != o6 & ( o4 != o6 & ( o5 != o6 & ( eo1 != o7 & ( eo2 != o7 & ( eo3 != o7 & ( o1 != o7 & ( o2 != o7 & ( o3 != o7 & ( o4 != o7 & ( o5 != o7 & ( o6 != o7 & ( eo1 != o8 & ( eo2 != o8 & ( eo3 != o8 & ( o1 != o8 & ( o2 != o8 & ( o3 != o8 & ( o4 != o8 & ( o5 != o8 & ( o6 != o8 & ( o7 != o8 & ( eo1 != o9 & ( eo2 != o9 & ( eo3 != o9 & ( o1 != o9 & ( o2 != o9 & ( o3 != o9 & ( o4 != o9 & ( o5 != o9 & ( o6 != o9 & ( o7 != o9 & ( o8 != o9 & ( eo1 != o10 & ( eo2 != o10 & ( eo3 != o10 & ( o1 != o10 & ( o2 != o10 & ( o3 != o10 & ( o4 != o10 & ( o5 != o10 & ( o6 != o10 & ( o7 != o10 & ( o8 != o10 & ( o9 != o10 & ( eo1 != o11 & ( eo2 != o11 & ( eo3 != o11 & ( o1 != o11 & ( o2 != o11 & ( o3 != o11 & ( o4 != o11 & ( o5 != o11 & ( o6 != o11 & ( o7 != o11 & ( o8 != o11 & ( o9 != o11 & ( o10 != o11 & ( eo1 != o12 & ( eo2 != o12 & ( eo3 != o12 & ( o1 != o12 & ( o2 != o12 & ( o3 != o12 & ( o4 != o12 & ( o5 != o12 & ( o6 != o12 & ( o7 != o12 & ( o8 != o12 & ( o9 != o12 & ( o10 != o12 & ( o11 != o12 & ( eo1 != o13 & ( eo2 != o13 & ( eo3 != o13 & ( o1 != o13 & ( o2 != o13 & ( o3 != o13 & ( o4 != o13 & ( o5 != o13 & ( o6 != o13 & ( o7 != o13 & ( o8 != o13 & ( o9 != o13 & ( o10 != o13 & ( o11 != o13 & ( o12 != o13 & ( eo1 != o14 & ( eo2 != o14 & ( eo3 != o14 & ( o1 != o14 & ( o2 != o14 & ( o3 != o14 & ( o4 != o14 & ( o5 != o14 & ( o6 != o14 & ( o7 != o14 & ( o8 != o14 & ( o9 != o14 & ( o10 != o14 & ( o11 != o14 & ( o12 != o14 & ( o13 != o14 & ( eo1 != o15 & ( eo2 != o15 & ( eo3 != o15 & ( o1 != o15 & ( o2 != o15 & ( o3 != o15 & ( o4 != o15 & ( o5 != o15 & ( o6 != o15 & ( o7 != o15 & ( o8 != o15 & ( o9 != o15 & ( o10 != o15 & ( o11 != o15 & ( o12 != o15 & ( o13 != o15 & ( o14 != o15 & ( eo1 != o16 & ( eo2 != o16 & ( eo3 != o16 & ( o1 != o16 & ( o2 != o16 & ( o3 != o16 & ( o4 != o16 & ( o5 != o16 & ( o6 != o16 & ( o7 != o16 & ( o8 != o16 & ( o9 != o16 & ( o10 != o16 & ( o11 != o16 & ( o12 != o16 & ( o13 != o16 & ( o14 != o16 & ( o15 != o16 & ( eo1 != o17 & ( eo2 != o17 & ( eo3 != o17 & ( o1 != o17 & ( o2 != o17 & ( o3 != o17 & ( o4 != o17 & ( o5 != o17 & ( o6 != o17 & ( o7 != o17 & ( o8 != o17 & ( o9 != o17 & ( o10 != o17 & ( o11 != o17 & ( o12 != o17 & ( o13 != o17 & ( o14 != o17 & ( o15 != o17 & ( o16 != o17 & ( eo1 != o18 & ( eo2 != o18 & ( eo3 != o18 & ( o1 != o18 & ( o2 != o18 & ( o3 != o18 & ( o4 != o18 & ( o5 != o18 & ( o6 != o18 & ( o7 != o18 & ( o8 != o18 & ( o9 != o18 & ( o10 != o18 & ( o11 != o18 & ( o12 != o18 & ( o13 != o18 & ( o14 != o18 & ( o15 != o18 & ( o16 != o18 & ( o17 != o18 & ( eo1 != o19 & ( eo2 != o19 & ( eo3 != o19 & ( o1 != o19 & ( o2 != o19 & ( o3 != o19 & ( o4 != o19 & ( o5 != o19 & ( o6 != o19 & ( o7 != o19 & ( o8 != o19 & ( o9 != o19 & ( o10 != o19 & ( o11 != o19 & ( o12 != o19 & ( o13 != o19 & ( o14 != o19 & ( o15 != o19 & ( o16 != o19 & ( o17 != o19 & ( o18 != o19 & ( eo1 != o20 & ( eo2 != o20 & ( eo3 != o20 & ( o1 != o20 & ( o2 != o20 & ( o3 != o20 & ( o4 != o20 & ( o5 != o20 & ( o6 != o20 & ( o7 != o20 & ( o8 != o20 & ( o9 != o20 & ( o10 != o20 & ( o11 != o20 & ( o12 != o20 & ( o13 != o20 & ( o14 != o20 & ( o15 != o20 & ( o16 != o20 & ( o17 != o20 & ( o18 != o20 & ( o19 != o20 & ( eo1 != o21 & ( eo2 != o21 & ( eo3 != o21 & ( o1 != o21 & ( o2 != o21 & ( o3 != o21 & ( o4 != o21 & ( o5 != o21 & ( o6 != o21 & ( o7 != o21 & ( o8 != o21 & ( o9 != o21 & ( o10 != o21 & ( o11 != o21 & ( o12 != o21 & ( o13 != o21 & ( o14 != o21 & ( o15 != o21 & ( o16 != o21 & ( o17 != o21 & ( o18 != o21 & ( o19 != o21 & ( o20 != o21 & ( eo1 != o22 & ( eo2 != o22 & ( eo3 != o22 & ( o1 != o22 & ( o2 != o22 & ( o3 != o22 & ( o4 != o22 & ( o5 != o22 & ( o6 != o22 & ( o7 != o22 & ( o8 != o22 & ( o9 != o22 & ( o10 != o22 & ( o11 != o22 & ( o12 != o22 & ( o13 != o22 & ( o14 != o22 & ( o15 != o22 & ( o16 != o22 & ( o17 != o22 & ( o18 != o22 & ( o19 != o22 & ( o20 != o22 & ( o21 != o22 & ( eo1 != o23 & ( eo2 != o23 & ( eo3 != o23 & ( o1 != o23 & ( o2 != o23 & ( o3 != o23 & ( o4 != o23 & ( o5 != o23 & ( o6 != o23 & ( o7 != o23 & ( o8 != o23 & ( o9 != o23 & ( o10 != o23 & ( o11 != o23 & ( o12 != o23 & ( o13 != o23 & ( o14 != o23 & ( o15 != o23 & ( o16 != o23 & ( o17 != o23 & ( o18 != o23 & ( o19 != o23 & ( o20 != o23 & ( o21 != o23 & ( o22 != o23 & ( eo1 != o24 & ( eo2 != o24 & ( eo3 != o24 & ( o1 != o24 & ( o2 != o24 & ( o3 != o24 & ( o4 != o24 & ( o5 != o24 & ( o6 != o24 & ( o7 != o24 & ( o8 != o24 & ( o9 != o24 & ( o10 != o24 & ( o11 != o24 & ( o12 != o24 & ( o13 != o24 & ( o14 != o24 & ( o15 != o24 & ( o16 != o24 & ( o17 != o24 & ( o18 != o24 & ( o19 != o24 & ( o20 != o24 & ( o21 != o24 & ( o22 != o24 & ( o23 != o24 & ( eo1 != o25 & ( eo2 != o25 & ( eo3 != o25 & ( o1 != o25 & ( o2 != o25 & ( o3 != o25 & ( o4 != o25 & ( o5 != o25 & ( o6 != o25 & ( o7 != o25 & ( o8 != o25 & ( o9 != o25 & ( o10 != o25 & ( o11 != o25 & ( o12 != o25 & ( o13 != o25 & ( o14 != o25 & ( o15 != o25 & ( o16 != o25 & ( o17 != o25 & ( o18 != o25 & ( o19 != o25 & ( o20 != o25 & ( o21 != o25 & ( o22 != o25 & ( o23 != o25 & ( o24 != o25 & ( eo1 != o26 & ( eo2 != o26 & ( eo3 != o26 & ( o1 != o26 & ( o2 != o26 & ( o3 != o26 & ( o4 != o26 & ( o5 != o26 & ( o6 != o26 & ( o7 != o26 & ( o8 != o26 & ( o9 != o26 & ( o10 != o26 & ( o11 != o26 & ( o12 != o26 & ( o13 != o26 & ( o14 != o26 & ( o15 != o26 & ( o16 != o26 & ( o17 != o26 & ( o18 != o26 & ( o19 != o26 & ( o20 != o26 & ( o21 != o26 & ( o22 != o26 & ( o23 != o26 & ( o24 != o26 & ( o25 != o26 & ( eo1 != o27 & ( eo2 != o27 & ( eo3 != o27 & ( o1 != o27 & ( o2 != o27 & ( o3 != o27 & ( o4 != o27 & ( o5 != o27 & ( o6 != o27 & ( o7 != o27 & ( o8 != o27 & ( o9 != o27 & ( o10 != o27 & ( o11 != o27 & ( o12 != o27 & ( o13 != o27 & ( o14 != o27 & ( o15 != o27 & ( o16 != o27 & ( o17 != o27 & ( o18 != o27 & ( o19 != o27 & ( o20 != o27 & ( o21 != o27 & ( o22 != o27 & ( o23 != o27 & ( o24 != o27 & ( o25 != o27 & ( o26 != o27 & ( eo1 != o28 & ( eo2 != o28 & ( eo3 != o28 & ( o1 != o28 & ( o2 != o28 & ( o3 != o28 & ( o4 != o28 & ( o5 != o28 & ( o6 != o28 & ( o7 != o28 & ( o8 != o28 & ( o9 != o28 & ( o10 != o28 & ( o11 != o28 & ( o12 != o28 & ( o13 != o28 & ( o14 != o28 & ( o15 != o28 & ( o16 != o28 & ( o17 != o28 & ( o18 != o28 & ( o19 != o28 & ( o20 != o28 & ( o21 != o28 & ( o22 != o28 & ( o23 != o28 & ( o24 != o28 & ( o25 != o28 & ( o26 != o28 & ( o27 != o28 & ( eo1 != o29 & ( eo2 != o29 & ( eo3 != o29 & ( o1 != o29 & ( o2 != o29 & ( o3 != o29 & ( o4 != o29 & ( o5 != o29 & ( o6 != o29 & ( o7 != o29 & ( o8 != o29 & ( o9 != o29 & ( o10 != o29 & ( o11 != o29 & ( o12 != o29 & ( o13 != o29 & ( o14 != o29 & ( o15 != o29 & ( o16 != o29 & ( o17 != o29 & ( o18 != o29 & ( o19 != o29 & ( o20 != o29 & ( o21 != o29 & ( o22 != o29 & ( o23 != o29 & ( o24 != o29 & ( o25 != o29 & ( o26 != o29 & ( o27 != o29 & ( o28 != o29 & ( eo1 != o30 & ( eo2 != o30 & ( eo3 != o30 & ( o1 != o30 & ( o2 != o30 & ( o3 != o30 & ( o4 != o30 & ( o5 != o30 & ( o6 != o30 & ( o7 != o30 & ( o8 != o30 & ( o9 != o30 & ( o10 != o30 & ( o11 != o30 & ( o12 != o30 & ( o13 != o30 & ( o14 != o30 & ( o15 != o30 & ( o16 != o30 & ( o17 != o30 & ( o18 != o30 & ( o19 != o30 & ( o20 != o30 & ( o21 != o30 & ( o22 != o30 & ( o23 != o30 & ( o24 != o30 & ( o25 != o30 & ( o26 != o30 & ( o27 != o30 & ( o28 != o30 & ( o29 != o30 & ( eo1 != o31 & ( eo2 != o31 & ( eo3 != o31 & ( o1 != o31 & ( o2 != o31 & ( o3 != o31 & ( o4 != o31 & ( o5 != o31 & ( o6 != o31 & ( o7 != o31 & ( o8 != o31 & ( o9 != o31 & ( o10 != o31 & ( o11 != o31 & ( o12 != o31 & ( o13 != o31 & ( o14 != o31 & ( o15 != o31 & ( o16 != o31 & ( o17 != o31 & ( o18 != o31 & ( o19 != o31 & ( o20 != o31 & ( o21 != o31 & ( o22 != o31 & ( o23 != o31 & ( o24 != o31 & ( o25 != o31 & ( o26 != o31 & ( o27 != o31 & ( o28 != o31 & ( o29 != o31 & ( o30 != o31 & ( eo1 != o32 & ( eo2 != o32 & ( eo3 != o32 & ( o1 != o32 & ( o2 != o32 & ( o3 != o32 & ( o4 != o32 & ( o5 != o32 & ( o6 != o32 & ( o7 != o32 & ( o8 != o32 & ( o9 != o32 & ( o10 != o32 & ( o11 != o32 & ( o12 != o32 & ( o13 != o32 & ( o14 != o32 & ( o15 != o32 & ( o16 != o32 & ( o17 != o32 & ( o18 != o32 & ( o19 != o32 & ( o20 != o32 & ( o21 != o32 & ( o22 != o32 & ( o23 != o32 & ( o24 != o32 & ( o25 != o32 & ( o26 != o32 & ( o27 != o32 & ( o28 != o32 & ( o29 != o32 & ( o30 != o32 & ( o31 != o32 & ( eo1 != o33 & ( eo2 != o33 & ( eo3 != o33 & ( o1 != o33 & ( o2 != o33 & ( o3 != o33 & ( o4 != o33 & ( o5 != o33 & ( o6 != o33 & ( o7 != o33 & ( o8 != o33 & ( o9 != o33 & ( o10 != o33 & ( o11 != o33 & ( o12 != o33 & ( o13 != o33 & ( o14 != o33 & ( o15 != o33 & ( o16 != o33 & ( o17 != o33 & ( o18 != o33 & ( o19 != o33 & ( o20 != o33 & ( o21 != o33 & ( o22 != o33 & ( o23 != o33 & ( o24 != o33 & ( o25 != o33 & ( o26 != o33 & ( o27 != o33 & ( o28 != o33 & ( o29 != o33 & ( o30 != o33 & ( o31 != o33 & ( o32 != o33 & ( eo1 != o34 & ( eo2 != o34 & ( eo3 != o34 & ( o1 != o34 & ( o2 != o34 & ( o3 != o34 & ( o4 != o34 & ( o5 != o34 & ( o6 != o34 & ( o7 != o34 & ( o8 != o34 & ( o9 != o34 & ( o10 != o34 & ( o11 != o34 & ( o12 != o34 & ( o13 != o34 & ( o14 != o34 & ( o15 != o34 & ( o16 != o34 & ( o17 != o34 & ( o18 != o34 & ( o19 != o34 & ( o20 != o34 & ( o21 != o34 & ( o22 != o34 & ( o23 != o34 & ( o24 != o34 & ( o25 != o34 & ( o26 != o34 & ( o27 != o34 & ( o28 != o34 & ( o29 != o34 & ( o30 != o34 & ( o31 != o34 & ( o32 != o34 & ( o33 != o34 & ( eo1 != o35 & ( eo2 != o35 & ( eo3 != o35 & ( o1 != o35 & ( o2 != o35 & ( o3 != o35 & ( o4 != o35 & ( o5 != o35 & ( o6 != o35 & ( o7 != o35 & ( o8 != o35 & ( o9 != o35 & ( o10 != o35 & ( o11 != o35 & ( o12 != o35 & ( o13 != o35 & ( o14 != o35 & ( o15 != o35 & ( o16 != o35 & ( o17 != o35 & ( o18 != o35 & ( o19 != o35 & ( o20 != o35 & ( o21 != o35 & ( o22 != o35 & ( o23 != o35 & ( o24 != o35 & ( o25 != o35 & ( o26 != o35 & ( o27 != o35 & ( o28 != o35 & ( o29 != o35 & ( o30 != o35 & ( o31 != o35 & ( o32 != o35 & ( o33 != o35 & ( o34 != o35 & ( eo1 != o36 & ( eo2 != o36 & ( eo3 != o36 & ( o1 != o36 & ( o2 != o36 & ( o3 != o36 & ( o4 != o36 & ( o5 != o36 & ( o6 != o36 & ( o7 != o36 & ( o8 != o36 & ( o9 != o36 & ( o10 != o36 & ( o11 != o36 & ( o12 != o36 & ( o13 != o36 & ( o14 != o36 & ( o15 != o36 & ( o16 != o36 & ( o17 != o36 & ( o18 != o36 & ( o19 != o36 & ( o20 != o36 & ( o21 != o36 & ( o22 != o36 & ( o23 != o36 & ( o24 != o36 & ( o25 != o36 & ( o26 != o36 & ( o27 != o36 & ( o28 != o36 & ( o29 != o36 & ( o30 != o36 & ( o31 != o36 & ( o32 != o36 & ( o33 != o36 & ( o34 != o36 & ( o35 != o36 & ( eo1 != o37 & ( eo2 != o37 & ( eo3 != o37 & ( o1 != o37 & ( o2 != o37 & ( o3 != o37 & ( o4 != o37 & ( o5 != o37 & ( o6 != o37 & ( o7 != o37 & ( o8 != o37 & ( o9 != o37 & ( o10 != o37 & ( o11 != o37 & ( o12 != o37 & ( o13 != o37 & ( o14 != o37 & ( o15 != o37 & ( o16 != o37 & ( o17 != o37 & ( o18 != o37 & ( o19 != o37 & ( o20 != o37 & ( o21 != o37 & ( o22 != o37 & ( o23 != o37 & ( o24 != o37 & ( o25 != o37 & ( o26 != o37 & ( o27 != o37 & ( o28 != o37 & ( o29 != o37 & ( o30 != o37 & ( o31 != o37 & ( o32 != o37 & ( o33 != o37 & ( o34 != o37 & ( o35 != o37 & ( o36 != o37 & ( eo1 != o38 & ( eo2 != o38 & ( eo3 != o38 & ( o1 != o38 & ( o2 != o38 & ( o3 != o38 & ( o4 != o38 & ( o5 != o38 & ( o6 != o38 & ( o7 != o38 & ( o8 != o38 & ( o9 != o38 & ( o10 != o38 & ( o11 != o38 & ( o12 != o38 & ( o13 != o38 & ( o14 != o38 & ( o15 != o38 & ( o16 != o38 & ( o17 != o38 & ( o18 != o38 & ( o19 != o38 & ( o20 != o38 & ( o21 != o38 & ( o22 != o38 & ( o23 != o38 & ( o24 != o38 & ( o25 != o38 & ( o26 != o38 & ( o27 != o38 & ( o28 != o38 & ( o29 != o38 & ( o30 != o38 & ( o31 != o38 & ( o32 != o38 & ( o33 != o38 & ( o34 != o38 & ( o35 != o38 & ( o36 != o38 & ( o37 != o38 & ( eo1 != o39 & ( eo2 != o39 & ( eo3 != o39 & ( o1 != o39 & ( o2 != o39 & ( o3 != o39 & ( o4 != o39 & ( o5 != o39 & ( o6 != o39 & ( o7 != o39 & ( o8 != o39 & ( o9 != o39 & ( o10 != o39 & ( o11 != o39 & ( o12 != o39 & ( o13 != o39 & ( o14 != o39 & ( o15 != o39 & ( o16 != o39 & ( o17 != o39 & ( o18 != o39 & ( o19 != o39 & ( o20 != o39 & ( o21 != o39 & ( o22 != o39 & ( o23 != o39 & ( o24 != o39 & ( o25 != o39 & ( o26 != o39 & ( o27 != o39 & ( o28 != o39 & ( o29 != o39 & ( o30 != o39 & ( o31 != o39 & ( o32 != o39 & ( o33 != o39 & ( o34 != o39 & ( o35 != o39 & ( o36 != o39 & ( o37 != o39 & ( o38 != o39 & ( eo1 != o40 & ( eo2 != o40 & ( eo3 != o40 & ( o1 != o40 & ( o2 != o40 & ( o3 != o40 & ( o4 != o40 & ( o5 != o40 & ( o6 != o40 & ( o7 != o40 & ( o8 != o40 & ( o9 != o40 & ( o10 != o40 & ( o11 != o40 & ( o12 != o40 & ( o13 != o40 & ( o14 != o40 & ( o15 != o40 & ( o16 != o40 & ( o17 != o40 & ( o18 != o40 & ( o19 != o40 & ( o20 != o40 & ( o21 != o40 & ( o22 != o40 & ( o23 != o40 & ( o24 != o40 & ( o25 != o40 & ( o26 != o40 & ( o27 != o40 & ( o28 != o40 & ( o29 != o40 & ( o30 != o40 & ( o31 != o40 & ( o32 != o40 & ( o33 != o40 & ( o34 != o40 & ( o35 != o40 & ( o36 != o40 & ( o37 != o40 & ( o38 != o40 & o39 != o40 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) .
15fof ( compliance_interface_FunctionalElement , axiom , ! [ V_0 , V_1 ] : ( r_interface_FunctionalElement ( V_0 , V_1 ) => ( t_FunctionalElement ( V_0 ) & t_FunctionalInterface ( V_1 ) ) ) ) . 15fof ( compliance_interface_FunctionalElement , axiom , ! [ V_0 , V_1 ] : ( r_interface_FunctionalElement ( V_0 , V_1 ) => ( t_FunctionalElement ( V_0 ) & t_FunctionalInterface ( V_1 ) ) ) ) .
16fof ( compliance_model_FunctionalElement , axiom , ! [ V_0 , V_1 ] : ( r_model_FunctionalElement ( V_0 , V_1 ) => ( t_FunctionalElement ( V_0 ) & t_FunctionalArchitectureModel ( V_1 ) ) ) ) . 16fof ( compliance_model_FunctionalElement , axiom , ! [ V_0 , V_1 ] : ( r_model_FunctionalElement ( V_0 , V_1 ) => ( t_FunctionalElement ( V_0 ) & t_FunctionalArchitectureModel ( V_1 ) ) ) ) .
17fof ( compliance_parent_FunctionalElement , axiom , ! [ V_0 , V_1 ] : ( r_parent_FunctionalElement ( V_0 , V_1 ) => ( t_FunctionalElement ( V_0 ) & t_Function ( V_1 ) ) ) ) . 17fof ( compliance_parent_FunctionalElement , axiom , ! [ V_0 , V_1 ] : ( r_parent_FunctionalElement ( V_0 , V_1 ) => ( t_FunctionalElement ( V_0 ) & t_Function ( V_1 ) ) ) ) .
@@ -28,12 +28,16 @@ fof ( compliance_terminator_FunctionalData , axiom , ! [ V_0 , V_1 ] : ( r_termi
28fof ( compliance_interface_FunctionalData , axiom , ! [ V_0 , V_1 ] : ( r_interface_FunctionalData ( V_0 , V_1 ) => ( t_FunctionalData ( V_0 ) & t_FunctionalInterface ( V_1 ) ) ) ) . 28fof ( compliance_interface_FunctionalData , axiom , ! [ V_0 , V_1 ] : ( r_interface_FunctionalData ( V_0 , V_1 ) => ( t_FunctionalData ( V_0 ) & t_FunctionalInterface ( V_1 ) ) ) ) .
29fof ( compliance_type_Function , axiom , ! [ V_0 , V_1 ] : ( r_type_Function ( V_0 , V_1 ) => ( t_Function ( V_0 ) & t_FunctionType ( V_1 ) ) ) ) . 29fof ( compliance_type_Function , axiom , ! [ V_0 , V_1 ] : ( r_type_Function ( V_0 , V_1 ) => ( t_Function ( V_0 ) & t_FunctionType ( V_1 ) ) ) ) .
30fof ( containment_topLevel_t_FunctionalArchitectureModel , axiom , ! [ A ] : ( t_FunctionalArchitectureModel ( A ) <=> A = o1 ) ) . 30fof ( containment_topLevel_t_FunctionalArchitectureModel , axiom , ! [ A ] : ( t_FunctionalArchitectureModel ( A ) <=> A = o1 ) ) .
31fof ( containment_r_interface_FunctionalElement , axiom , ! [ A ] : ( t_FunctionalInterface ( A ) => ? [ B ] : ( t_FunctionalElement ( B ) & r_interface_FunctionalElement ( B , A ) ) ) ) . 31
32fof ( containment_r_rootElements_FunctionalArchitectureModel , axiom , ! [ A ] : ( t_FunctionalElement ( A ) => ? [ B ] : ( t_FunctionalArchitectureModel ( B ) & r_rootElements_FunctionalArchitectureModel ( B , A ) ) ) ) . 32
33fof ( containment_r_subElements_Function , axiom , ! [ A ] : ( t_FunctionalElement ( A ) => ? [ B ] : ( t_Function ( B ) & r_subElements_Function ( B , A ) ) ) ) . 33fof ( containment_r_interface_FunctionalElement , axiom , ! [ A ] : ( t_FunctionalInterface ( A ) => ? [ B ] : r_interface_FunctionalElement ( B , A ) ) ) .
34fof ( containment_r_data_FunctionalInterface , axiom , ! [ A ] : ( t_FunctionalData ( A ) => ? [ B ] : ( t_FunctionalInterface ( B ) & r_data_FunctionalInterface ( B , A ) ) ) ) . 34fof ( containment_r_rootElements_FunctionalArchitectureModel , axiom , ! [ A ] : ( t_FunctionalElement ( A ) => ? [ B ] : r_rootElements_FunctionalArchitectureModel ( B , A ) ) ) .
35fof ( containment_r_outgoingLinks_FunctionalOutput , axiom , ! [ A ] : ( t_InformationLink ( A ) => ? [ B ] : ( t_FunctionalOutput ( B ) & r_outgoingLinks_FunctionalOutput ( B , A ) ) ) ) . 35fof ( containment_r_subElements_Function , axiom , ! [ A ] : ( t_FunctionalElement ( A ) => ? [ B ] : r_subElements_Function ( B , A ) ) ) .
36fof ( containment_r_terminator_FunctionalData , axiom , ! [ A ] : ( t_FAMTerminator ( A ) => ? [ B ] : ( t_FunctionalData ( B ) & r_terminator_FunctionalData ( B , A ) ) ) ) . 36fof ( containment_r_data_FunctionalInterface , axiom , ! [ A ] : ( t_FunctionalData ( A ) => ? [ B ] : r_data_FunctionalInterface ( B , A ) ) ) .
37fof ( containment_r_outgoingLinks_FunctionalOutput , axiom , ! [ A ] : ( t_InformationLink ( A ) => ? [ B ] : r_outgoingLinks_FunctionalOutput ( B , A ) ) ) .
38fof ( containment_r_terminator_FunctionalData , axiom , ! [ A ] : ( t_FAMTerminator ( A ) => ? [ B ] : r_terminator_FunctionalData ( B , A ) ) ) .
39
40
37fof ( 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 ) ) ) . 41fof ( 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 ) ) ) .
38fof ( 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 ) ) ) ) . 42fof ( 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 ) ) ) ) .
39fof ( 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 ) ) ) . 43fof ( 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 ) ) ) .