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