Anne is cold. Dave is cold. Dave is red. Dave is smart. Erin is big. Erin is red. Harry is white. All smart, red people are cold.
Anne is cold.
("Anne" "is" "cold" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is red.
("Erin" "is" "red" "+")
Harry is white.
("Harry" "is" "white" "+")
All smart, red people are cold.
((("someone" "is" "smart" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "cold" "+"))
Dave is smart.
True
1
proof
[(triple4)]
("Dave" "is" "smart" "+")
triple4
Dave is not smart.
False
1
inv-proof
[(triple4)]
("Dave" "is" "smart" "-")
triple4
Harry is not cold.
Unknown
inv-rconc
[@1: Harry is cold.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Harry" "is" "cold" "-")
Anne is smart.
Unknown
random
[@0: Anne is smart.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "smart" "+")
@0: Anne is cold.[(triple1)] Dave is cold.[(triple2 OR ((triple4 triple3) -> rule1))] Dave is red.[(triple3)] Dave is smart.[(triple4)] Erin is big.[(triple5)] Erin is red.[(triple6)] Harry is white.[(triple7)]
Anne is cold.
("Anne" "is" "cold" "+")
triple1
Dave is cold.
("Dave" "is" "cold" "+")
triple2
((triple4 triple3) -> (rule1 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
triple3
Dave is smart.
("Dave" "is" "smart" "+")
triple4
Erin is big.
("Erin" "is" "big" "+")
triple5
Erin is red.
("Erin" "is" "red" "+")
triple6
Harry is white.
("Harry" "is" "white" "+")
triple7