Erin is big. Erin is cold. Erin is kind. Erin is red. Erin is not rough. Erin is round. Erin is white. All rough things are kind. All cold things are kind.
Erin is big.
("Erin" "is" "big" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is red.
("Erin" "is" "red" "+")
Erin is not rough.
("Erin" "is" "rough" "-")
Erin is round.
("Erin" "is" "round" "+")
Erin is white.
("Erin" "is" "white" "+")
All rough things are kind.
((("something" "is" "rough" "+")) -> ("something" "is" "kind" "+"))
All cold things are kind.
((("something" "is" "cold" "+")) -> ("something" "is" "kind" "+"))
Erin is kind.
True
1
proof
[(triple3 OR ((triple2) -> rule2))]
("Erin" "is" "kind" "+")
triple3
((triple2) -> (rule2 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is rough.
False
1
inv-proof
[(triple5)]
("Erin" "is" "rough" "+")
triple5
@0: Erin is big.[(triple1)] Erin is cold.[(triple2)] Erin is kind.[(triple3 OR ((triple2) -> rule2))] Erin is not rough.[(triple5)] Erin is red.[(triple4)] Erin is round.[(triple6)] Erin is white.[(triple7)]
Erin is big.
("Erin" "is" "big" "+")
triple1
Erin is cold.
("Erin" "is" "cold" "+")
triple2
Erin is kind.
("Erin" "is" "kind" "+")
triple3
((triple2) -> (rule2 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is not rough.
("Erin" "is" "rough" "-")
triple5
Erin is red.
("Erin" "is" "red" "+")
triple4
Erin is round.
("Erin" "is" "round" "+")
triple6
Erin is white.
("Erin" "is" "white" "+")
triple7