Erin is quiet. Erin is smart. Harry is furry. If Erin is red and Erin is not quiet then Erin is not smart. If Erin is smart then Erin is cold. If someone is quiet and smart then they are cold.
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Harry is furry.
("Harry" "is" "furry" "+")
If Erin is red and Erin is not quiet then Erin is not smart.
((("Erin" "is" "red" "+") ("Erin" "is" "quiet" "~")) -> ("Erin" "is" "smart" "-"))
If Erin is smart then Erin is cold.
((("Erin" "is" "smart" "+")) -> ("Erin" "is" "cold" "+"))
If someone is quiet and smart then they are cold.
((("someone" "is" "quiet" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "cold" "+"))
Erin is smart.
True
1
proof
[(triple2)]
("Erin" "is" "smart" "+")
triple2
Erin is not smart.
False
1
inv-proof
[(triple2)]
("Erin" "is" "smart" "-")
triple2
Erin is cold.
True
2
proof
[(((triple2) -> rule2) OR ((triple1 triple2) -> rule3))]
("Erin" "is" "cold" "+")
((triple2) -> (rule2 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
((triple1 triple2) -> (rule3 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is not cold.
False
2
inv-proof
[(((triple2) -> rule2) OR ((triple1 triple2) -> rule3))]
("Erin" "is" "cold" "-")
((triple2) -> (rule2 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
((triple1 triple2) -> (rule3 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Harry is not cold.
Unknown
inv-rconc
[@1: Harry is cold.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Harry" "is" "cold" "-")
Erin is white.
Unknown
random
[@0: Erin is white.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "white" "+")
Erin is not red.
Unknown
inv-random
[@0: Erin is red.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "red" "-")
Erin is big.
Unknown
random
[@0: Erin is big.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "big" "+")
@0: Erin is quiet.[(triple1)] Erin is smart.[(triple2)] Harry is furry.[(triple3)] @1: Erin is cold.[(((triple2) -> rule2) OR ((triple1 triple2) -> rule3))]
Erin is quiet.
("Erin" "is" "quiet" "+")
triple1
Erin is smart.
("Erin" "is" "smart" "+")
triple2
Harry is furry.
("Harry" "is" "furry" "+")
triple3
Erin is cold.
("Erin" "is" "cold" "+")
((triple2) -> (rule2 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
((triple1 triple2) -> (rule3 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1