Anne is rough. Bob is furry. Charlie is red. Gary is kind. If something is kind and not white then it is not smart. Furry, green things are smart. If something is kind then it is not green.
Anne is rough.
("Anne" "is" "rough" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Gary is kind.
("Gary" "is" "kind" "+")
If something is kind and not white then it is not smart.
((("something" "is" "kind" "+") ("something" "is" "white" "~")) -> ("something" "is" "smart" "-"))
Furry, green things are smart.
((("something" "is" "furry" "+") ("something" "is" "green" "+")) -> ("something" "is" "smart" "+"))
If something is kind then it is not green.
((("something" "is" "kind" "+")) -> ("something" "is" "green" "-"))
Charlie is red.
True
1
proof
[(triple3)]
("Charlie" "is" "red" "+")
triple3
Gary is not kind.
False
1
inv-proof
[(triple4)]
("Gary" "is" "kind" "-")
triple4
Gary is not green.
True
2
proof
[(((triple4) -> rule3))]
("Gary" "is" "green" "-")
((triple4) -> (rule3 % int1))
Gary is not green.
("Gary" "is" "green" "-")
int1
Gary is green.
False
2
inv-proof
[(((triple4) -> rule3))]
("Gary" "is" "green" "+")
((triple4) -> (rule3 % int1))
Gary is not green.
("Gary" "is" "green" "-")
int1
Gary is not smart.
Unknown
inv-rconc
[@1: Gary is smart.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Gary" "is" "smart" "-")
Bob is smart.
Unknown
rconc
[@1: Bob is smart.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Bob" "is" "smart" "+")
Gary is not furry.
Unknown
inv-random
[@0: Gary is furry.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "furry" "-")
Anne is white.
Unknown
random
[@0: Anne is white.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "white" "+")
@0: Anne is rough.[(triple1)] Bob is furry.[(triple2)] Charlie is red.[(triple3)] Gary is kind.[(triple4)] @1: Gary is not green.[(((triple4) -> rule3))]
Anne is rough.
("Anne" "is" "rough" "+")
triple1
Bob is furry.
("Bob" "is" "furry" "+")
triple2
Charlie is red.
("Charlie" "is" "red" "+")
triple3
Gary is kind.
("Gary" "is" "kind" "+")
triple4
Gary is not green.
("Gary" "is" "green" "-")
((triple4) -> (rule3 % int1))
Gary is not green.
("Gary" "is" "green" "-")
int1