Anne is blue. Anne is furry. Anne is kind. Anne is not nice. Anne is rough. Gary is red. Gary is rough. All blue things are red. Nice, quiet things are rough. If something is kind and quiet then it is blue.
Anne is blue.
("Anne" "is" "blue" "+")
Anne is furry.
("Anne" "is" "furry" "+")
Anne is kind.
("Anne" "is" "kind" "+")
Anne is not nice.
("Anne" "is" "nice" "-")
Anne is rough.
("Anne" "is" "rough" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is rough.
("Gary" "is" "rough" "+")
All blue things are red.
((("something" "is" "blue" "+")) -> ("something" "is" "red" "+"))
Nice, quiet things are rough.
((("something" "is" "nice" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "rough" "+"))
If something is kind and quiet then it is blue.
((("something" "is" "kind" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "blue" "+"))
Anne is rough.
True
1
proof
[(triple5)]
("Anne" "is" "rough" "+")
triple5
Anne is nice.
False
1
inv-proof
[(triple4)]
("Anne" "is" "nice" "+")
triple4
Anne is red.
True
2
proof
[(((triple1) -> rule1))]
("Anne" "is" "red" "+")
((triple1) -> (rule1 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is not red.
False
2
inv-proof
[(((triple1) -> rule1))]
("Anne" "is" "red" "-")
((triple1) -> (rule1 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Gary is not blue.
Unknown
inv-rconc
[@1: Gary is blue.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Gary" "is" "blue" "-")
Gary is nice.
Unknown
random
[@0: Gary is nice.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "nice" "+")
Gary is not quiet.
Unknown
inv-random
[@0: Gary is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "quiet" "-")
Anne is quiet.
Unknown
random
[@0: Anne is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "quiet" "+")
@0: Anne is blue.[(triple1)] Anne is furry.[(triple2)] Anne is kind.[(triple3)] Anne is not nice.[(triple4)] Anne is rough.[(triple5)] Gary is red.[(triple6)] Gary is rough.[(triple7)] @1: Anne is red.[(((triple1) -> rule1))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Anne is furry.
("Anne" "is" "furry" "+")
triple2
Anne is kind.
("Anne" "is" "kind" "+")
triple3
Anne is not nice.
("Anne" "is" "nice" "-")
triple4
Anne is rough.
("Anne" "is" "rough" "+")
triple5
Gary is red.
("Gary" "is" "red" "+")
triple6
Gary is rough.
("Gary" "is" "rough" "+")
triple7
Anne is red.
("Anne" "is" "red" "+")
((triple1) -> (rule1 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1