Erin is not blue. Erin is cold. Erin is not furry. Erin is green. Erin is kind. Erin is not nice. Erin is red. If Erin is green and Erin is red then Erin is not blue. If Erin is furry and Erin is kind then Erin is not blue. All nice people are not green. If someone is cold and nice then they are green. If Erin is kind and Erin is cold then Erin is green. If someone is nice and furry then they are cold.
Erin is not blue.
("Erin" "is" "blue" "-")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is not furry.
("Erin" "is" "furry" "-")
Erin is green.
("Erin" "is" "green" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is not nice.
("Erin" "is" "nice" "-")
Erin is red.
("Erin" "is" "red" "+")
If Erin is green and Erin is red then Erin is not blue.
((("Erin" "is" "green" "+") ("Erin" "is" "red" "+")) -> ("Erin" "is" "blue" "-"))
If Erin is furry and Erin is kind then Erin is not blue.
((("Erin" "is" "furry" "+") ("Erin" "is" "kind" "+")) -> ("Erin" "is" "blue" "-"))
All nice people are not green.
((("someone" "is" "nice" "+")) -> ("someone" "is" "green" "-"))
If someone is cold and nice then they are green.
((("someone" "is" "cold" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "green" "+"))
If Erin is kind and Erin is cold then Erin is green.
((("Erin" "is" "kind" "+") ("Erin" "is" "cold" "+")) -> ("Erin" "is" "green" "+"))
If someone is nice and furry then they are cold.
((("someone" "is" "nice" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "cold" "+"))
Erin is not furry.
True
1
proof
[(triple3)]
("Erin" "is" "furry" "-")
triple3
Erin is not red.
False
1
inv-proof
[(triple7)]
("Erin" "is" "red" "-")
triple7
@0: Erin is cold.[(triple2)] Erin is green.[(triple4 OR ((triple5 triple2) -> rule5))] Erin is kind.[(triple5)] Erin is not blue.[(triple1 OR ((triple4 triple7) -> rule1) OR ((((triple5 triple2) -> rule5) triple7) -> rule1))] Erin is not furry.[(triple3)] Erin is not nice.[(triple6)] Erin is red.[(triple7)]
Erin is cold.
("Erin" "is" "cold" "+")
triple2
Erin is green.
("Erin" "is" "green" "+")
triple4
((triple5 triple2) -> (rule5 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
triple5
Erin is not blue.
("Erin" "is" "blue" "-")
triple1
((triple4 triple7) -> (rule1 % int1))
Erin is not blue.
("Erin" "is" "blue" "-")
int1
((((triple5 triple2) -> (rule5 % int2)) triple7) -> (rule1 % int1))
Erin is not blue.
("Erin" "is" "blue" "-")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is not furry.
("Erin" "is" "furry" "-")
triple3
Erin is not nice.
("Erin" "is" "nice" "-")
triple6
Erin is red.
("Erin" "is" "red" "+")
triple7