Erin is furry. Erin is red. Erin is young. If Erin is blue and Erin is nice then Erin is cold. All blue people are not young. All nice, smart people are cold. If someone is smart then they are cold. If Erin is smart and Erin is nice then Erin is blue. Furry, red people are nice.
Erin is furry.
("Erin" "is" "furry" "+")
Erin is red.
("Erin" "is" "red" "+")
Erin is young.
("Erin" "is" "young" "+")
If Erin is blue and Erin is nice then Erin is cold.
((("Erin" "is" "blue" "+") ("Erin" "is" "nice" "+")) -> ("Erin" "is" "cold" "+"))
All blue people are not young.
((("someone" "is" "blue" "+")) -> ("someone" "is" "young" "-"))
All nice, smart people are cold.
((("someone" "is" "nice" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "cold" "+"))
If someone is smart then they are cold.
((("someone" "is" "smart" "+")) -> ("someone" "is" "cold" "+"))
If Erin is smart and Erin is nice then Erin is blue.
((("Erin" "is" "smart" "+") ("Erin" "is" "nice" "+")) -> ("Erin" "is" "blue" "+"))
Furry, red people are nice.
((("someone" "is" "furry" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "nice" "+"))
Erin is furry.
True
1
proof
[(triple1)]
("Erin" "is" "furry" "+")
triple1
Erin is not red.
False
1
inv-proof
[(triple2)]
("Erin" "is" "red" "-")
triple2
Erin is nice.
True
3
proof
[(((triple1 triple2) -> rule6))]
("Erin" "is" "nice" "+")
((triple1 triple2) -> (rule6 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is not nice.
False
3
inv-proof
[(((triple1 triple2) -> rule6))]
("Erin" "is" "nice" "-")
((triple1 triple2) -> (rule6 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is not blue.
Unknown
inv-rconc
[@1: Erin is blue.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Erin" "is" "blue" "-")
Erin is cold.
Unknown
rconc
[@2: Erin is cold.[CWA. Example of deepest failure = (rule1 <- rule5 <- FAIL)]]
("Erin" "is" "cold" "+")
@0: Erin is furry.[(triple1)] Erin is red.[(triple2)] Erin is young.[(triple3)] @1: Erin is nice.[(((triple1 triple2) -> rule6))]
Erin is furry.
("Erin" "is" "furry" "+")
triple1
Erin is red.
("Erin" "is" "red" "+")
triple2
Erin is young.
("Erin" "is" "young" "+")
triple3
Erin is nice.
("Erin" "is" "nice" "+")
((triple1 triple2) -> (rule6 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1