Dave is quiet. Gary is white. All red, cold things are white. If something is red then it is white. If something is quiet then it is kind. If Dave is red and Dave is white then Dave is cold. If Dave is smart and Dave is rough then Dave is red. Smart things are rough.
Dave is quiet.
("Dave" "is" "quiet" "+")
Gary is white.
("Gary" "is" "white" "+")
All red, cold things are white.
((("something" "is" "red" "+") ("something" "is" "cold" "+")) -> ("something" "is" "white" "+"))
If something is red then it is white.
((("something" "is" "red" "+")) -> ("something" "is" "white" "+"))
If something is quiet then it is kind.
((("something" "is" "quiet" "+")) -> ("something" "is" "kind" "+"))
If Dave is red and Dave is white then Dave is cold.
((("Dave" "is" "red" "+") ("Dave" "is" "white" "+")) -> ("Dave" "is" "cold" "+"))
If Dave is smart and Dave is rough then Dave is red.
((("Dave" "is" "smart" "+") ("Dave" "is" "rough" "+")) -> ("Dave" "is" "red" "+"))
Smart things are rough.
((("something" "is" "smart" "+")) -> ("something" "is" "rough" "+"))
Dave is quiet.
True
1
proof
[(triple1)]
("Dave" "is" "quiet" "+")
triple1
Gary is not white.
False
1
inv-proof
[(triple2)]
("Gary" "is" "white" "-")
triple2
Gary is not rough.
Unknown
inv-rconc
[@1: Gary is rough.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Gary" "is" "rough" "-")
Gary is smart.
Unknown
random
[@0: Gary is smart.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "smart" "+")
@0: Dave is quiet.[(triple1)] Gary is white.[(triple2)] @1: Dave is kind.[(((triple1) -> rule3))]
Dave is quiet.
("Dave" "is" "quiet" "+")
triple1
Gary is white.
("Gary" "is" "white" "+")
triple2
Dave is kind.
("Dave" "is" "kind" "+")
((triple1) -> (rule3 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1