Update: removal of redundant comparison rules
@@ -112,12 +112,8 @@ R2( (M --> S), (M --> (P - S)), |-, (M --> P), Truth_DecomposeNNN )
//NAL4 rules
R2( ((A * B) --> R), ((C * B) --> R), |-, (C --> A), Truth_Abduction )
R2( ((A * B) --> R), ((A * C) --> R), |-, (C --> B), Truth_Abduction )
-R2( ((A * B) --> R), ((C * B) --> R), |-, (C <-> A), Truth_Comparison )
-R2( ((A * B) --> R), ((A * C) --> R), |-, (C <-> B), Truth_Comparison )
R2( (R --> (A * B)), (R --> (C * B)), |-, (C --> A), Truth_Induction )
R2( (R --> (A * B)), (R --> (A * C)), |-, (C --> B), Truth_Induction )
-R2( (R --> (A * B)), (R --> (C * B)), |-, (C <-> A), Truth_Comparison )
-R2( (R --> (A * B)), (R --> (A * C)), |-, (C <-> B), Truth_Comparison )
R2( ((A * B) --> R), (C --> A), |-, ((C * B) --> R), Truth_Deduction )
R2( ((A * B) --> R), (A --> C), |-, ((C * B) --> R), Truth_Induction )
R2( ((A * B) --> R), (C <-> A), |-, ((C * B) --> R), Truth_Analogy )
