Charlie is quiet. Gary is furry. All furry people are rough. If someone is green then they are not furry. If Charlie is nice then Charlie is not green.
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Gary is furry.
("Gary" "is" "furry" "+")
All furry people are rough.
((("someone" "is" "furry" "+")) -> ("someone" "is" "rough" "+"))
If someone is green then they are not furry.
((("someone" "is" "green" "+")) -> ("someone" "is" "furry" "-"))
If Charlie is nice then Charlie is not green.
((("Charlie" "is" "nice" "+")) -> ("Charlie" "is" "green" "-"))
Gary is furry.
True
1
proof
[(triple2)]
("Gary" "is" "furry" "+")
triple2
Gary is not furry.
False
1
inv-proof
[(triple2)]
("Gary" "is" "furry" "-")
triple2
Gary is rough.
True
2
proof
[(((triple2) -> rule1))]
("Gary" "is" "rough" "+")
((triple2) -> (rule1 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is not rough.
False
2
inv-proof
[(((triple2) -> rule1))]
("Gary" "is" "rough" "-")
((triple2) -> (rule1 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Charlie is not rough.
Unknown
inv-rconc
[@1: Charlie is rough.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Charlie" "is" "rough" "-")
Charlie is kind.
Unknown
random
[@0: Charlie is kind.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "kind" "+")
Charlie is not green.
Unknown
inv-random
[@0: Charlie is green.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "green" "-")
Gary is red.
Unknown
random
[@0: Gary is red.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "red" "+")
@0: Charlie is quiet.[(triple1)] Gary is furry.[(triple2)] @1: Gary is rough.[(((triple2) -> rule1))]
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple1
Gary is furry.
("Gary" "is" "furry" "+")
triple2
Gary is rough.
("Gary" "is" "rough" "+")
((triple2) -> (rule1 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1