aboutsummaryrefslogtreecommitdiffstats
path: root/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/output/files/vampireCode.tptp
diff options
context:
space:
mode:
Diffstat (limited to 'Tests/ca.mcgill.ecse.dslreasoner.vampire.test/output/files/vampireCode.tptp')
-rw-r--r--Tests/ca.mcgill.ecse.dslreasoner.vampire.test/output/files/vampireCode.tptp39
1 files changed, 38 insertions, 1 deletions
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/output/files/vampireCode.tptp b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/output/files/vampireCode.tptp
index ddeec4f4..6decf070 100644
--- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/output/files/vampireCode.tptp
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/output/files/vampireCode.tptp
@@ -1 +1,38 @@
1%This is an initial Test Comment fof ( assertion1 , axiom , ~ ( constant1 & constant2 ) <=> ( ~ constant1 | ~ constant2 ) ) . 1% This is an initial Test Comment
2fof ( typeDef_FunctionType_enum , axiom , ! [ A ] : ( type_FunctionType_enum ( A ) <=> ( A = "aRoot literal FunctionType" | ( A = "aIntermediate literal FunctionType" | A = "aLeaf literal FunctionType" ) ) ) ) .
3fof ( hierarchyHandler , axiom , ! [ A ] : ( object ( A ) <=> ( ( type_InformationLink_class ( A ) & ( ~ type_FunctionalElement_class ( A ) & ( ~ type_FunctionalInput_class ( A ) & ( ~ type_FunctionType_enum ( A ) & ( ~ type_FAMTerminator_class ( A ) & ( ~ type_FunctionalData_class ( A ) & ( ~ type_FunctionalInterface_class ( A ) & ( ~ type_Function_class ( A ) & ( ~ type_FunctionalOutput_class ( A ) & ~ type_FunctionalArchitectureModel_class ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ type_InformationLink_class ( A ) & ( ~ type_FunctionalElement_class ( A ) & ( type_FunctionalInput_class ( A ) & ( ~ type_FunctionType_enum ( A ) & ( ~ type_FAMTerminator_class ( A ) & ( type_FunctionalData_class ( A ) & ( ~ type_FunctionalInterface_class ( A ) & ( ~ type_Function_class ( A ) & ( ~ type_FunctionalOutput_class ( A ) & ~ type_FunctionalArchitectureModel_class ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ type_InformationLink_class ( A ) & ( ~ type_FunctionalElement_class ( A ) & ( ~ type_FunctionalInput_class ( A ) & ( type_FunctionType_enum ( A ) & ( ~ type_FAMTerminator_class ( A ) & ( ~ type_FunctionalData_class ( A ) & ( ~ type_FunctionalInterface_class ( A ) & ( ~ type_Function_class ( A ) & ( ~ type_FunctionalOutput_class ( A ) & ~ type_FunctionalArchitectureModel_class ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ type_InformationLink_class ( A ) & ( ~ type_FunctionalElement_class ( A ) & ( ~ type_FunctionalInput_class ( A ) & ( ~ type_FunctionType_enum ( A ) & ( type_FAMTerminator_class ( A ) & ( ~ type_FunctionalData_class ( A ) & ( ~ type_FunctionalInterface_class ( A ) & ( ~ type_Function_class ( A ) & ( ~ type_FunctionalOutput_class ( A ) & ~ type_FunctionalArchitectureModel_class ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ type_InformationLink_class ( A ) & ( ~ type_FunctionalElement_class ( A ) & ( ~ type_FunctionalInput_class ( A ) & ( ~ type_FunctionType_enum ( A ) & ( ~ type_FAMTerminator_class ( A ) & ( ~ type_FunctionalData_class ( A ) & ( type_FunctionalInterface_class ( A ) & ( ~ type_Function_class ( A ) & ( ~ type_FunctionalOutput_class ( A ) & ~ type_FunctionalArchitectureModel_class ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ type_InformationLink_class ( A ) & ( type_FunctionalElement_class ( A ) & ( ~ type_FunctionalInput_class ( A ) & ( ~ type_FunctionType_enum ( A ) & ( ~ type_FAMTerminator_class ( A ) & ( ~ type_FunctionalData_class ( A ) & ( ~ type_FunctionalInterface_class ( A ) & ( type_Function_class ( A ) & ( ~ type_FunctionalOutput_class ( A ) & ~ type_FunctionalArchitectureModel_class ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ type_InformationLink_class ( A ) & ( ~ type_FunctionalElement_class ( A ) & ( ~ type_FunctionalInput_class ( A ) & ( ~ type_FunctionType_enum ( A ) & ( ~ type_FAMTerminator_class ( A ) & ( type_FunctionalData_class ( A ) & ( ~ type_FunctionalInterface_class ( A ) & ( ~ type_Function_class ( A ) & ( type_FunctionalOutput_class ( A ) & ~ type_FunctionalArchitectureModel_class ( A ) ) ) ) ) ) ) ) ) ) | ( ~ type_InformationLink_class ( A ) & ( ~ type_FunctionalElement_class ( A ) & ( ~ type_FunctionalInput_class ( A ) & ( ~ type_FunctionType_enum ( A ) & ( ~ type_FAMTerminator_class ( A ) & ( ~ type_FunctionalData_class ( A ) & ( ~ type_FunctionalInterface_class ( A ) & ( ~ type_Function_class ( A ) & ( ~ type_FunctionalOutput_class ( A ) & type_FunctionalArchitectureModel_class ( A ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) .
4fof ( compliance_interface_reference_FunctionalElement , axiom , ! [ Var_0 , Var_1 ] : ( rel_interface_reference_FunctionalElement ( Var_0 , Var_1 ) => ( type_FunctionalElement_class ( Var_0 ) & type_FunctionalInterface_class ( Var_1 ) ) ) ) .
5fof ( compliance_model_reference_FunctionalElement , axiom , ! [ Var_0 , Var_1 ] : ( rel_model_reference_FunctionalElement ( Var_0 , Var_1 ) => ( type_FunctionalElement_class ( Var_0 ) & type_FunctionalArchitectureModel_class ( Var_1 ) ) ) ) .
6fof ( compliance_parent_reference_FunctionalElement , axiom , ! [ Var_0 , Var_1 ] : ( rel_parent_reference_FunctionalElement ( Var_0 , Var_1 ) => ( type_FunctionalElement_class ( Var_0 ) & type_Function_class ( Var_1 ) ) ) ) .
7fof ( compliance_rootElements_reference_FunctionalArchitectureModel , axiom , ! [ Var_0 , Var_1 ] : ( rel_rootElements_reference_FunctionalArchitectureModel ( Var_0 , Var_1 ) => ( type_FunctionalArchitectureModel_class ( Var_0 ) & type_FunctionalElement_class ( Var_1 ) ) ) ) .
8fof ( compliance_subElements_reference_Function , axiom , ! [ Var_0 , Var_1 ] : ( rel_subElements_reference_Function ( Var_0 , Var_1 ) => ( type_Function_class ( Var_0 ) & type_FunctionalElement_class ( Var_1 ) ) ) ) .
9fof ( compliance_data_reference_FAMTerminator , axiom , ! [ Var_0 , Var_1 ] : ( rel_data_reference_FAMTerminator ( Var_0 , Var_1 ) => ( type_FAMTerminator_class ( Var_0 ) & type_FunctionalData_class ( Var_1 ) ) ) ) .
10fof ( compliance_from_reference_InformationLink , axiom , ! [ Var_0 , Var_1 ] : ( rel_from_reference_InformationLink ( Var_0 , Var_1 ) => ( type_InformationLink_class ( Var_0 ) & type_FunctionalOutput_class ( Var_1 ) ) ) ) .
11fof ( compliance_to_reference_InformationLink , axiom , ! [ Var_0 , Var_1 ] : ( rel_to_reference_InformationLink ( Var_0 , Var_1 ) => ( type_InformationLink_class ( Var_0 ) & type_FunctionalInput_class ( Var_1 ) ) ) ) .
12fof ( compliance_data_reference_FunctionalInterface , axiom , ! [ Var_0 , Var_1 ] : ( rel_data_reference_FunctionalInterface ( Var_0 , Var_1 ) => ( type_FunctionalInterface_class ( Var_0 ) & type_FunctionalData_class ( Var_1 ) ) ) ) .
13fof ( compliance_element_reference_FunctionalInterface , axiom , ! [ Var_0 , Var_1 ] : ( rel_element_reference_FunctionalInterface ( Var_0 , Var_1 ) => ( type_FunctionalInterface_class ( Var_0 ) & type_FunctionalElement_class ( Var_1 ) ) ) ) .
14fof ( compliance_IncomingLinks_reference_FunctionalInput , axiom , ! [ Var_0 , Var_1 ] : ( rel_IncomingLinks_reference_FunctionalInput ( Var_0 , Var_1 ) => ( type_FunctionalInput_class ( Var_0 ) & type_InformationLink_class ( Var_1 ) ) ) ) .
15fof ( compliance_outgoingLinks_reference_FunctionalOutput , axiom , ! [ Var_0 , Var_1 ] : ( rel_outgoingLinks_reference_FunctionalOutput ( Var_0 , Var_1 ) => ( type_FunctionalOutput_class ( Var_0 ) & type_InformationLink_class ( Var_1 ) ) ) ) .
16fof ( compliance_terminator_reference_FunctionalData , axiom , ! [ Var_0 , Var_1 ] : ( rel_terminator_reference_FunctionalData ( Var_0 , Var_1 ) => ( type_FunctionalData_class ( Var_0 ) & type_FAMTerminator_class ( Var_1 ) ) ) ) .
17fof ( compliance_interface_reference_FunctionalData , axiom , ! [ Var_0 , Var_1 ] : ( rel_interface_reference_FunctionalData ( Var_0 , Var_1 ) => ( type_FunctionalData_class ( Var_0 ) & type_FunctionalInterface_class ( Var_1 ) ) ) ) .
18fof ( compliance_type_attribute_Function , axiom , ! [ Var_0 , Var_1 ] : ( rel_type_attribute_Function ( Var_0 , Var_1 ) => ( type_Function_class ( Var_0 ) & type_FunctionType_enum ( Var_1 ) ) ) ) .
19fof ( upperMultiplicity_interface_FunctionalElement , axiom , ! [ Var_src , Var_trg_1 , Var_trg_2 ] : ( ( type_FunctionalElement_class ( Var_src ) & ( type_FunctionalInterface_class ( Var_trg_1 ) & type_FunctionalInterface_class ( Var_trg_2 ) ) ) => ( ( rel_interface_reference_FunctionalElement ( Var_src , Var_trg_1 ) & rel_interface_reference_FunctionalElement ( Var_src , Var_trg_2 ) ) => ~ Var_trg_1 != Var_trg_2 ) ) ) .
20fof ( lowerMultiplicity_model_FunctionalElement , axiom , ! [ Var_src ] : ( type_FunctionalElement_class ( Var_src ) => ? [ Var_trg_1 ] : ( type_FunctionalArchitectureModel_class ( Var_trg_1 ) & rel_model_reference_FunctionalElement ( Var_src , Var_trg_1 ) ) ) ) .
21fof ( upperMultiplicity_model_FunctionalElement , axiom , ! [ Var_src , Var_trg_1 , Var_trg_2 ] : ( ( type_FunctionalElement_class ( Var_src ) & ( type_FunctionalArchitectureModel_class ( Var_trg_1 ) & type_FunctionalArchitectureModel_class ( Var_trg_2 ) ) ) => ( ( rel_model_reference_FunctionalElement ( Var_src , Var_trg_1 ) & rel_model_reference_FunctionalElement ( Var_src , Var_trg_2 ) ) => ~ Var_trg_1 != Var_trg_2 ) ) ) .
22fof ( upperMultiplicity_parent_FunctionalElement , axiom , ! [ Var_src , Var_trg_1 , Var_trg_2 ] : ( ( type_FunctionalElement_class ( Var_src ) & ( type_Function_class ( Var_trg_1 ) & type_Function_class ( Var_trg_2 ) ) ) => ( ( rel_parent_reference_FunctionalElement ( Var_src , Var_trg_1 ) & rel_parent_reference_FunctionalElement ( Var_src , Var_trg_2 ) ) => ~ Var_trg_1 != Var_trg_2 ) ) ) .
23fof ( upperMultiplicity_data_FAMTerminator , axiom , ! [ Var_src , Var_trg_1 , Var_trg_2 ] : ( ( type_FAMTerminator_class ( Var_src ) & ( type_FunctionalData_class ( Var_trg_1 ) & type_FunctionalData_class ( Var_trg_2 ) ) ) => ( ( rel_data_reference_FAMTerminator ( Var_src , Var_trg_1 ) & rel_data_reference_FAMTerminator ( Var_src , Var_trg_2 ) ) => ~ Var_trg_1 != Var_trg_2 ) ) ) .
24fof ( upperMultiplicity_from_InformationLink , axiom , ! [ Var_src , Var_trg_1 , Var_trg_2 ] : ( ( type_InformationLink_class ( Var_src ) & ( type_FunctionalOutput_class ( Var_trg_1 ) & type_FunctionalOutput_class ( Var_trg_2 ) ) ) => ( ( rel_from_reference_InformationLink ( Var_src , Var_trg_1 ) & rel_from_reference_InformationLink ( Var_src , Var_trg_2 ) ) => ~ Var_trg_1 != Var_trg_2 ) ) ) .
25fof ( lowerMultiplicity_to_InformationLink , axiom , ! [ Var_src ] : ( type_InformationLink_class ( Var_src ) => ? [ Var_trg_1 ] : ( type_FunctionalInput_class ( Var_trg_1 ) & rel_to_reference_InformationLink ( Var_src , Var_trg_1 ) ) ) ) .
26fof ( upperMultiplicity_to_InformationLink , axiom , ! [ Var_src , Var_trg_1 , Var_trg_2 ] : ( ( type_InformationLink_class ( Var_src ) & ( type_FunctionalInput_class ( Var_trg_1 ) & type_FunctionalInput_class ( Var_trg_2 ) ) ) => ( ( rel_to_reference_InformationLink ( Var_src , Var_trg_1 ) & rel_to_reference_InformationLink ( Var_src , Var_trg_2 ) ) => ~ Var_trg_1 != Var_trg_2 ) ) ) .
27fof ( upperMultiplicity_element_FunctionalInterface , axiom , ! [ Var_src , Var_trg_1 , Var_trg_2 ] : ( ( type_FunctionalInterface_class ( Var_src ) & ( type_FunctionalElement_class ( Var_trg_1 ) & type_FunctionalElement_class ( Var_trg_2 ) ) ) => ( ( rel_element_reference_FunctionalInterface ( Var_src , Var_trg_1 ) & rel_element_reference_FunctionalInterface ( Var_src , Var_trg_2 ) ) => ~ Var_trg_1 != Var_trg_2 ) ) ) .
28fof ( upperMultiplicity_terminator_FunctionalData , axiom , ! [ Var_src , Var_trg_1 , Var_trg_2 ] : ( ( type_FunctionalData_class ( Var_src ) & ( type_FAMTerminator_class ( Var_trg_1 ) & type_FAMTerminator_class ( Var_trg_2 ) ) ) => ( ( rel_terminator_reference_FunctionalData ( Var_src , Var_trg_1 ) & rel_terminator_reference_FunctionalData ( Var_src , Var_trg_2 ) ) => ~ Var_trg_1 != Var_trg_2 ) ) ) .
29fof ( upperMultiplicity_interface_FunctionalData , axiom , ! [ Var_src , Var_trg_1 , Var_trg_2 ] : ( ( type_FunctionalData_class ( Var_src ) & ( type_FunctionalInterface_class ( Var_trg_1 ) & type_FunctionalInterface_class ( Var_trg_2 ) ) ) => ( ( rel_interface_reference_FunctionalData ( Var_src , Var_trg_1 ) & rel_interface_reference_FunctionalData ( Var_src , Var_trg_2 ) ) => ~ Var_trg_1 != Var_trg_2 ) ) ) .
30fof ( oppositeReference_interface_FunctionalElement , axiom , ! [ Var_src , Var_trg ] : ( ( type_FunctionalElement_class ( Var_src ) & type_FunctionalInterface_class ( Var_trg ) ) => ( rel_interface_reference_FunctionalElement ( Var_src , Var_trg ) <=> rel_element_reference_FunctionalInterface ( Var_trg , Var_src ) ) ) ) .
31fof ( oppositeReference_parent_FunctionalElement , axiom , ! [ Var_src , Var_trg ] : ( ( type_FunctionalElement_class ( Var_src ) & type_Function_class ( Var_trg ) ) => ( rel_parent_reference_FunctionalElement ( Var_src , Var_trg ) <=> rel_subElements_reference_Function ( Var_trg , Var_src ) ) ) ) .
32fof ( oppositeReference_data_FAMTerminator , axiom , ! [ Var_src , Var_trg ] : ( ( type_FAMTerminator_class ( Var_src ) & type_FunctionalData_class ( Var_trg ) ) => ( rel_data_reference_FAMTerminator ( Var_src , Var_trg ) <=> rel_terminator_reference_FunctionalData ( Var_trg , Var_src ) ) ) ) .
33fof ( oppositeReference_from_InformationLink , axiom , ! [ Var_src , Var_trg ] : ( ( type_InformationLink_class ( Var_src ) & type_FunctionalOutput_class ( Var_trg ) ) => ( rel_from_reference_InformationLink ( Var_src , Var_trg ) <=> rel_outgoingLinks_reference_FunctionalOutput ( Var_trg , Var_src ) ) ) ) .
34fof ( oppositeReference_to_InformationLink , axiom , ! [ Var_src , Var_trg ] : ( ( type_InformationLink_class ( Var_src ) & type_FunctionalInput_class ( Var_trg ) ) => ( rel_to_reference_InformationLink ( Var_src , Var_trg ) <=> rel_IncomingLinks_reference_FunctionalInput ( Var_trg , Var_src ) ) ) ) .
35fof ( oppositeReference_data_FunctionalInterface , axiom , ! [ Var_src , Var_trg ] : ( ( type_FunctionalInterface_class ( Var_src ) & type_FunctionalData_class ( Var_trg ) ) => ( rel_data_reference_FunctionalInterface ( Var_src , Var_trg ) <=> rel_interface_reference_FunctionalData ( Var_trg , Var_src ) ) ) ) .
36fof ( lowerMultiplicity_type_Function , axiom , ! [ Var_src ] : ( type_Function_class ( Var_src ) => ? [ Var_trg_1 ] : ( type_FunctionType_enum ( Var_trg_1 ) & rel_type_attribute_Function ( Var_src , Var_trg_1 ) ) ) ) .
37fof ( upperMultiplicity_type_Function , axiom , ! [ Var_src , Var_trg_1 , Var_trg_2 ] : ( ( type_Function_class ( Var_src ) & ( type_FunctionType_enum ( Var_trg_1 ) & type_FunctionType_enum ( Var_trg_2 ) ) ) => ( ( rel_type_attribute_Function ( Var_src , Var_trg_1 ) & rel_type_attribute_Function ( Var_src , Var_trg_2 ) ) => ~ Var_trg_1 != Var_trg_2 ) ) ) .
38
generated by cgit v1.2.3-70-g09d2 (git 2.46.0) at 2024-09-27 16:34:15 +0000