diff options
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.tptp | 13 |
1 files changed, 9 insertions, 4 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 f55667e4..265e7762 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,10 +1,15 @@ | |||
| 1 | % This is an initial Test Comment | 1 | % This is an initial Test Comment |
| 2 | fof ( typeDef_FunctionType , axiom , ! [ A ] : ( t_FunctionType ( A ) <=> ( e_Root_FunctionType ( A ) | ( e_Intermediate_FunctionType ( A ) | e_Leaf_FunctionType ( A ) ) ) ) ) . | 2 | fof ( typeDef_FunctionType , axiom , ! [ A ] : ( t_FunctionType ( A ) <=> ( e_Root_FunctionType ( A ) | ( e_Intermediate_FunctionType ( A ) | e_Leaf_FunctionType ( A ) ) ) ) ) . |
| 3 | fof ( enumScope_FunctionType , axiom , e_Root_FunctionType ( eo1 ) & ( ~ e_Intermediate_FunctionType ( eo1 ) & ( ~ e_Leaf_FunctionType ( eo1 ) & ( e_Intermediate_FunctionType ( eo2 ) & ( ~ e_Root_FunctionType ( eo2 ) & ( ~ e_Leaf_FunctionType ( eo2 ) & ( e_Leaf_FunctionType ( eo3 ) & ( ~ e_Root_FunctionType ( eo3 ) & ~ e_Intermediate_FunctionType ( eo3 ) ) ) ) ) ) ) ) ) . | 3 | fof ( enumScope_FunctionType , axiom , e_Root_FunctionType ( eo1 ) & ( ~ e_Intermediate_FunctionType ( eo1 ) & ( ~ e_Leaf_FunctionType ( eo1 ) & ( e_Intermediate_FunctionType ( eo2 ) & ( ~ e_Root_FunctionType ( eo2 ) & ( ~ e_Leaf_FunctionType ( eo2 ) & ( e_Leaf_FunctionType ( eo3 ) & ( ~ e_Root_FunctionType ( eo3 ) & ~ e_Intermediate_FunctionType ( eo3 ) ) ) ) ) ) ) ) ) . |
| 4 | fof ( inheritanceHierarchyHandler , axiom , ! [ A ] : ( object ( A ) <=> ( ( ~ t_FunctionType ( A ) & ( t_FunctionalInput ( A ) & ( ~ t_InformationLink ( A ) & ( ~ t_FunctionalInterface ( A ) & ( ~ t_FAMTerminator ( A ) & ( ~ t_Function ( A ) & ( ~ t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionalOutput ( A ) & ( ~ t_FunctionalElement ( A ) & t_FunctionalData ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_FunctionType ( A ) & ( ~ t_FunctionalInput ( A ) & ( t_InformationLink ( A ) & ( ~ t_FunctionalInterface ( A ) & ( ~ t_FAMTerminator ( A ) & ( ~ t_Function ( A ) & ( ~ t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionalOutput ( A ) & ( ~ t_FunctionalElement ( A ) & ~ t_FunctionalData ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_FunctionType ( A ) & ( ~ t_FunctionalInput ( A ) & ( ~ t_InformationLink ( A ) & ( t_FunctionalInterface ( A ) & ( ~ t_FAMTerminator ( A ) & ( ~ t_Function ( A ) & ( ~ t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionalOutput ( A ) & ( ~ t_FunctionalElement ( A ) & ~ t_FunctionalData ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_FunctionType ( A ) & ( ~ t_FunctionalInput ( A ) & ( ~ t_InformationLink ( A ) & ( ~ t_FunctionalInterface ( A ) & ( t_FAMTerminator ( A ) & ( ~ t_Function ( A ) & ( ~ t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionalOutput ( A ) & ( ~ t_FunctionalElement ( A ) & ~ t_FunctionalData ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_FunctionType ( A ) & ( ~ t_FunctionalInput ( A ) & ( ~ t_InformationLink ( A ) & ( ~ t_FunctionalInterface ( A ) & ( ~ t_FAMTerminator ( A ) & ( t_Function ( A ) & ( ~ t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionalOutput ( A ) & ( t_FunctionalElement ( A ) & ~ t_FunctionalData ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_FunctionType ( A ) & ( ~ t_FunctionalInput ( A ) & ( ~ t_InformationLink ( A ) & ( ~ t_FunctionalInterface ( A ) & ( ~ t_FAMTerminator ( A ) & ( ~ t_Function ( A ) & ( t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionalOutput ( A ) & ( ~ t_FunctionalElement ( A ) & ~ t_FunctionalData ( A ) ) ) ) ) ) ) ) ) ) | ( ~ t_FunctionType ( A ) & ( ~ t_FunctionalInput ( A ) & ( ~ t_InformationLink ( A ) & ( ~ t_FunctionalInterface ( A ) & ( ~ t_FAMTerminator ( A ) & ( ~ t_Function ( A ) & ( ~ t_FunctionalArchitectureModel ( A ) & ( t_FunctionalOutput ( A ) & ( ~ t_FunctionalElement ( A ) & t_FunctionalData ( A ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) . | 4 | fof ( inheritanceHierarchyHandler , axiom , ! [ A ] : ( object ( A ) <=> ( ( t_FunctionalInput ( A ) & ( ~ t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionalElement ( A ) & ( ~ t_FunctionalOutput ( A ) & ( ~ t_Function ( A ) & ( t_FunctionalData ( A ) & ( ~ t_FunctionalInterface ( A ) & ( ~ t_FAMTerminator ( A ) & ( ~ t_InformationLink ( A ) & ~ t_FunctionType ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_FunctionalInput ( A ) & ( t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionalElement ( A ) & ( ~ t_FunctionalOutput ( A ) & ( ~ t_Function ( A ) & ( ~ t_FunctionalData ( A ) & ( ~ t_FunctionalInterface ( A ) & ( ~ t_FAMTerminator ( A ) & ( ~ t_InformationLink ( A ) & ~ t_FunctionType ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_FunctionalInput ( A ) & ( ~ t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionalElement ( A ) & ( t_FunctionalOutput ( A ) & ( ~ t_Function ( A ) & ( t_FunctionalData ( A ) & ( ~ t_FunctionalInterface ( A ) & ( ~ t_FAMTerminator ( A ) & ( ~ t_InformationLink ( A ) & ~ t_FunctionType ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_FunctionalInput ( A ) & ( ~ t_FunctionalArchitectureModel ( A ) & ( t_FunctionalElement ( A ) & ( ~ t_FunctionalOutput ( A ) & ( t_Function ( A ) & ( ~ t_FunctionalData ( A ) & ( ~ t_FunctionalInterface ( A ) & ( ~ t_FAMTerminator ( A ) & ( ~ t_InformationLink ( A ) & ~ t_FunctionType ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_FunctionalInput ( A ) & ( ~ t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionalElement ( A ) & ( ~ t_FunctionalOutput ( A ) & ( ~ t_Function ( A ) & ( ~ t_FunctionalData ( A ) & ( t_FunctionalInterface ( A ) & ( ~ t_FAMTerminator ( A ) & ( ~ t_InformationLink ( A ) & ~ t_FunctionType ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_FunctionalInput ( A ) & ( ~ t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionalElement ( A ) & ( ~ t_FunctionalOutput ( A ) & ( ~ t_Function ( A ) & ( ~ t_FunctionalData ( A ) & ( ~ t_FunctionalInterface ( A ) & ( t_FAMTerminator ( A ) & ( ~ t_InformationLink ( A ) & ~ t_FunctionType ( A ) ) ) ) ) ) ) ) ) ) | ( ~ t_FunctionalInput ( A ) & ( ~ t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionalElement ( A ) & ( ~ t_FunctionalOutput ( A ) & ( ~ t_Function ( A ) & ( ~ t_FunctionalData ( A ) & ( ~ t_FunctionalInterface ( A ) & ( ~ t_FAMTerminator ( A ) & ( t_InformationLink ( A ) & ~ t_FunctionType ( A ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) . |
| 5 | fof ( typeScope_min_object , axiom , ! [ A ] : ( ( A = o1 | ( A = o2 | A = o3 ) ) => object ( A ) ) ) . | 5 | fof ( typeScope_min_object , axiom , ! [ A ] : ( ( A = o1 | ( A = o2 | ( A = o3 | ( A = o4 | ( A = o5 | A = o6 ) ) ) ) ) => object ( A ) ) ) . |
| 6 | fof ( typeScope_max_object , axiom , ! [ A ] : ( object ( A ) => ( A = o1 | ( A = o2 | ( A = o3 | ( A = o4 | ( A = o5 | A = o6 ) ) ) ) ) ) ) . | 6 | fof ( typeScope_max_object , axiom , ! [ A ] : ( object ( A ) => ( A = o1 | ( A = o2 | ( A = o3 | ( A = o4 | ( A = o5 | ( A = o6 | ( A = o7 | A = o8 ) ) ) ) ) ) ) ) ) . |
| 7 | fof ( 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 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) . | 7 | fof ( typeScope_min_t_FunctionalOutput , axiom , ! [ A ] : ( A = o1 => t_FunctionalOutput ( A ) ) ) . |
| 8 | fof ( typeScope_min_t_Function , axiom , ! [ A ] : ( ( A = o2 | ( A = o3 | A = o4 ) ) => t_Function ( A ) ) ) . | ||
| 9 | fof ( typeScope_min_t_FunctionalInterface , axiom , ! [ A ] : ( ( A = o5 | A = o6 ) => t_FunctionalInterface ( A ) ) ) . | ||
| 10 | fof ( typeScope_max_t_FunctionalOutput , axiom , ! [ A ] : ( t_FunctionalOutput ( A ) => ( A = o1 | ( A = o7 | A = o8 ) ) ) ) . | ||
| 11 | fof ( typeScope_max_t_Function , axiom , ! [ A ] : ( t_Function ( A ) => ( A = o2 | ( A = o3 | ( A = o4 | ( A = o7 | A = o8 ) ) ) ) ) ) . | ||
| 12 | fof ( 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 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) . | ||
| 8 | fof ( compliance_interface_FunctionalElement , axiom , ! [ V_0 , V_1 ] : ( r_interface_FunctionalElement ( V_0 , V_1 ) => ( t_FunctionalElement ( V_0 ) & t_FunctionalInterface ( V_1 ) ) ) ) . | 13 | fof ( compliance_interface_FunctionalElement , axiom , ! [ V_0 , V_1 ] : ( r_interface_FunctionalElement ( V_0 , V_1 ) => ( t_FunctionalElement ( V_0 ) & t_FunctionalInterface ( V_1 ) ) ) ) . |
| 9 | fof ( compliance_model_FunctionalElement , axiom , ! [ V_0 , V_1 ] : ( r_model_FunctionalElement ( V_0 , V_1 ) => ( t_FunctionalElement ( V_0 ) & t_FunctionalArchitectureModel ( V_1 ) ) ) ) . | 14 | fof ( compliance_model_FunctionalElement , axiom , ! [ V_0 , V_1 ] : ( r_model_FunctionalElement ( V_0 , V_1 ) => ( t_FunctionalElement ( V_0 ) & t_FunctionalArchitectureModel ( V_1 ) ) ) ) . |
| 10 | fof ( compliance_parent_FunctionalElement , axiom , ! [ V_0 , V_1 ] : ( r_parent_FunctionalElement ( V_0 , V_1 ) => ( t_FunctionalElement ( V_0 ) & t_Function ( V_1 ) ) ) ) . | 15 | fof ( compliance_parent_FunctionalElement , axiom , ! [ V_0 , V_1 ] : ( r_parent_FunctionalElement ( V_0 , V_1 ) => ( t_FunctionalElement ( V_0 ) & t_Function ( V_1 ) ) ) ) . |