Dave is cold. Erin is cold. If someone is cold and not red then they are round. Smart, red people are round. If Dave is smart and Dave is cold then Dave is not big. If someone is young and not red then they are not smart. If Dave is young and Dave is kind then Dave is round. If Erin is young then Erin is smart.
Dave is cold.
("Dave" "is" "cold" "+")
Erin is cold.
("Erin" "is" "cold" "+")
If someone is cold and not red then they are round.
((("someone" "is" "cold" "+") ("someone" "is" "red" "~")) -> ("someone" "is" "round" "+"))
Smart, red people are round.
((("someone" "is" "smart" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "round" "+"))
If Dave is smart and Dave is cold then Dave is not big.
((("Dave" "is" "smart" "+") ("Dave" "is" "cold" "+")) -> ("Dave" "is" "big" "-"))
If someone is young and not red then they are not smart.
((("someone" "is" "young" "+") ("someone" "is" "red" "~")) -> ("someone" "is" "smart" "-"))
If Dave is young and Dave is kind then Dave is round.
((("Dave" "is" "young" "+") ("Dave" "is" "kind" "+")) -> ("Dave" "is" "round" "+"))
If Erin is young then Erin is smart.
((("Erin" "is" "young" "+")) -> ("Erin" "is" "smart" "+"))
Erin is cold.
True
1
proof
[(triple2)]
("Erin" "is" "cold" "+")
triple2
Erin is not cold.
False
1
inv-proof
[(triple2)]
("Erin" "is" "cold" "-")
triple2
Dave is not round.
Unknown
inv-rconc
[@1: Dave is round.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Dave" "is" "round" "-")
Dave is red.
Unknown
random
[@0: Dave is red.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "red" "+")
@0: Dave is cold.[(triple1)] Erin is cold.[(triple2)]
Dave is cold.
("Dave" "is" "cold" "+")
triple1
Erin is cold.
("Erin" "is" "cold" "+")
triple2