Erin is blue. Erin is cold. Erin is not nice. Erin is rough. Erin is round. Erin is smart. Erin is young. If Erin is rough and Erin is not blue then Erin is not cold. All smart people are cold.
Erin is blue.
("Erin" "is" "blue" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is not nice.
("Erin" "is" "nice" "-")
Erin is rough.
("Erin" "is" "rough" "+")
Erin is round.
("Erin" "is" "round" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Erin is young.
("Erin" "is" "young" "+")
If Erin is rough and Erin is not blue then Erin is not cold.
((("Erin" "is" "rough" "+") ("Erin" "is" "blue" "~")) -> ("Erin" "is" "cold" "-"))
All smart people are cold.
((("someone" "is" "smart" "+")) -> ("someone" "is" "cold" "+"))
Erin is cold.
True
1
proof
[(triple2 OR ((triple6) -> rule2))]
("Erin" "is" "cold" "+")
triple2
((triple6) -> (rule2 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is not cold.
False
1
inv-proof
[(triple2 OR ((triple6) -> rule2))]
("Erin" "is" "cold" "-")
triple2
((triple6) -> (rule2 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
@0: Erin is blue.[(triple1)] Erin is cold.[(triple2 OR ((triple6) -> rule2))] Erin is not nice.[(triple3)] Erin is rough.[(triple4)] Erin is round.[(triple5)] Erin is smart.[(triple6)] Erin is young.[(triple7)]
Erin is blue.
("Erin" "is" "blue" "+")
triple1
Erin is cold.
("Erin" "is" "cold" "+")
triple2
((triple6) -> (rule2 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is not nice.
("Erin" "is" "nice" "-")
triple3
Erin is rough.
("Erin" "is" "rough" "+")
triple4
Erin is round.
("Erin" "is" "round" "+")
triple5
Erin is smart.
("Erin" "is" "smart" "+")
triple6
Erin is young.
("Erin" "is" "young" "+")
triple7