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