Dave is blue. Gary is cold. Harry is big. Harry is not furry. Harry is not quiet. Harry is not smart. Harry is not white. Quiet, cold things are smart. If something is quiet and white then it is not cold.
Dave is blue.
("Dave" "is" "blue" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is not furry.
("Harry" "is" "furry" "-")
Harry is not quiet.
("Harry" "is" "quiet" "-")
Harry is not smart.
("Harry" "is" "smart" "-")
Harry is not white.
("Harry" "is" "white" "-")
Quiet, cold things are smart.
((("something" "is" "quiet" "+") ("something" "is" "cold" "+")) -> ("something" "is" "smart" "+"))
If something is quiet and white then it is not cold.
((("something" "is" "quiet" "+") ("something" "is" "white" "+")) -> ("something" "is" "cold" "-"))
Harry is not smart.
True
1
proof
[(triple6)]
("Harry" "is" "smart" "-")
triple6
Dave is not blue.
False
1
inv-proof
[(triple1)]
("Dave" "is" "blue" "-")
triple1
Dave is not smart.
Unknown
inv-rconc
[@1: Dave is smart.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Dave" "is" "smart" "-")
Dave is quiet.
Unknown
random
[@0: Dave is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "quiet" "+")
@0: Dave is blue.[(triple1)] Gary is cold.[(triple2)] Harry is big.[(triple3)] Harry is not furry.[(triple4)] Harry is not quiet.[(triple5)] Harry is not smart.[(triple6)] Harry is not white.[(triple7)]
Dave is blue.
("Dave" "is" "blue" "+")
triple1
Gary is cold.
("Gary" "is" "cold" "+")
triple2
Harry is big.
("Harry" "is" "big" "+")
triple3
Harry is not furry.
("Harry" "is" "furry" "-")
triple4
Harry is not quiet.
("Harry" "is" "quiet" "-")
triple5
Harry is not smart.
("Harry" "is" "smart" "-")
triple6
Harry is not white.
("Harry" "is" "white" "-")
triple7