// To run the test please issue:
// cargo run -- -f test.txt
// Contingent
(p -> (!p & r))
// Contingent
!p -> q
// Logically True
p | q | !p
// Contingent
a -> b -> c -> d
// Logically True
((p & q) -> p)
// Contingent
((p | q) -> (r -> p))
// Logically True
p -> (q -> r | p)
// Logically True
p & q -> p
// Logically True
(p -> q) -> ((q -> r) -> (p -> r))
// Contingent
!((!p | !q) & (p <-> !r) -> !(q & r))
// Logically False
p & q <-> !(p & q) | !q
// Logically False
p & !p
// Logically True
p | !p
// Contingent
(!p | !q) & (p <-> !r) -> !(q & r)
// Logically True
!(p & q <-> !(p & q) | !q)
// Contingent
q & (p -> q) -> p
// Logically True
p -> q -> (p & r -> p)
// Logically True
p & (!q -> !p) -> q
// -----------------------------------
// Some important valid argument forms
// -----------------------------------
// Logically True - Modus Ponens
p & (p -> q) -> q
// Logically True - Modus Tollens
!q & (p -> q) -> !p
// Logically True - Disjunctive syllogism
(p | q) & !p -> q
// as well as
(p | q) & !q -> p
// Logically True - Addition
p -> (p | q)
// as well as
p -> (q | p)
// Logically True - Simplification
p & q -> p
// as well as
p & q -> q
// Logically True - Double negation
!!p -> p
// Logically True - Transitivity of implication
((p -> q) & (q -> r)) -> (p -> r)
// Logically True - "Dreierschluss"
(p -> (q -> r)) -> ((p -> q) -> (p -> r))
// Logically True - "Constructive dilemma"
((p -> q) & (r -> s) & (p | r)) -> q | s
// Logically True - "Destructive dilemma"
(p -> q) & (r -> s) & (!q | !s) -> !p | !r
// Logically True - Reiteration, trivial argument
p -> p
// Logically True - mEFQ
!p -> (p -> q)
// Logically True - mVEQ
q -> (p -> q)
// Logically True - lEFQ
p & !p -> q
// Logically True - lVEQ
p -> (q | !q)