Erin is not cold. Erin is kind. Erin is smart. If Erin is red then Erin is quiet. If Erin is smart and Erin is kind then Erin is quiet. Smart, furry things are not red. If something is green and not kind then it is red. If Erin is not smart then Erin is not red. Cold things are quiet.
Erin is not cold.
("Erin" "is" "cold" "-")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is smart.
("Erin" "is" "smart" "+")
If Erin is red then Erin is quiet.
((("Erin" "is" "red" "+")) -> ("Erin" "is" "quiet" "+"))
If Erin is smart and Erin is kind then Erin is quiet.
((("Erin" "is" "smart" "+") ("Erin" "is" "kind" "+")) -> ("Erin" "is" "quiet" "+"))
Smart, furry things are not red.
((("something" "is" "smart" "+") ("something" "is" "furry" "+")) -> ("something" "is" "red" "-"))
If something is green and not kind then it is red.
((("something" "is" "green" "+") ("something" "is" "kind" "~")) -> ("something" "is" "red" "+"))
If Erin is not smart then Erin is not red.
((("Erin" "is" "smart" "~")) -> ("Erin" "is" "red" "-"))
Cold things are quiet.
((("something" "is" "cold" "+")) -> ("something" "is" "quiet" "+"))
Erin is kind.
True
1
proof
[(triple2)]
("Erin" "is" "kind" "+")
triple2
Erin is not smart.
False
1
inv-proof
[(triple3)]
("Erin" "is" "smart" "-")
triple3
Erin is quiet.
True
3
proof
[(((triple3 triple2) -> rule2))]
("Erin" "is" "quiet" "+")
((triple3 triple2) -> (rule2 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is not quiet.
False
3
inv-proof
[(((triple3 triple2) -> rule2))]
("Erin" "is" "quiet" "-")
((triple3 triple2) -> (rule2 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is not red.
Unknown
inv-rconc
[@1: Erin is red.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Erin" "is" "red" "-")
Erin is green.
Unknown
random
[@0: Erin is green.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "green" "+")
@0: Erin is kind.[(triple2)] Erin is not cold.[(triple1)] Erin is smart.[(triple3)] @1: Erin is quiet.[(((triple3 triple2) -> rule2))]
Erin is kind.
("Erin" "is" "kind" "+")
triple2
Erin is not cold.
("Erin" "is" "cold" "-")
triple1
Erin is smart.
("Erin" "is" "smart" "+")
triple3
Erin is quiet.
("Erin" "is" "quiet" "+")
((triple3 triple2) -> (rule2 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1