Dave is cold. If something is quiet then it is cold. If something is young and nice then it is cold. All nice things are smart.
Dave is cold.
("Dave" "is" "cold" "+")
If something is quiet then it is cold.
((("something" "is" "quiet" "+")) -> ("something" "is" "cold" "+"))
If something is young and nice then it is cold.
((("something" "is" "young" "+") ("something" "is" "nice" "+")) -> ("something" "is" "cold" "+"))
All nice things are smart.
((("something" "is" "nice" "+")) -> ("something" "is" "smart" "+"))
Dave is cold.
True
1
proof
[(triple1)]
("Dave" "is" "cold" "+")
triple1
Dave is not cold.
False
1
inv-proof
[(triple1)]
("Dave" "is" "cold" "-")
triple1
Dave is not smart.
Unknown
inv-rconc
[@1: Dave is smart.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Dave" "is" "smart" "-")
Dave is nice.
Unknown
random
[@0: Dave is nice.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "nice" "+")
@0: Dave is cold.[(triple1)]
Dave is cold.
("Dave" "is" "cold" "+")
triple1