Anne is nice. Anne is red. Anne is round. Charlie is kind. Erin is red. Gary is blue. Gary is young. If someone is nice and round then they are red. Round, nice people are not young. If someone is round and not young then they are kind.
Anne is nice.
("Anne" "is" "nice" "+")
Anne is red.
("Anne" "is" "red" "+")
Anne is round.
("Anne" "is" "round" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Erin is red.
("Erin" "is" "red" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is young.
("Gary" "is" "young" "+")
If someone is nice and round then they are red.
((("someone" "is" "nice" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "red" "+"))
Round, nice people are not young.
((("someone" "is" "round" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "young" "-"))
If someone is round and not young then they are kind.
((("someone" "is" "round" "+") ("someone" "is" "young" "~")) -> ("someone" "is" "kind" "+"))
Anne is red.
True
1
proof
[(triple2 OR ((triple1 triple3) -> rule1))]
("Anne" "is" "red" "+")
triple2
((triple1 triple3) -> (rule1 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is not nice.
False
1
inv-proof
[(triple1)]
("Anne" "is" "nice" "-")
triple1
Anne is not young.
True
3
proof
[(((triple3 triple1) -> rule2))]
("Anne" "is" "young" "-")
((triple3 triple1) -> (rule2 % int1))
Anne is not young.
("Anne" "is" "young" "-")
int1
Anne is young.
False
3
inv-proof
[(((triple3 triple1) -> rule2))]
("Anne" "is" "young" "+")
((triple3 triple1) -> (rule2 % int1))
Anne is not young.
("Anne" "is" "young" "-")
int1
Anne is kind.
True
5
proof
[(((triple3 ((triple3 triple1) -> rule2)) -> rule3))]
("Anne" "is" "kind" "+")
((triple3 ((triple3 triple1) -> (rule2 % int2))) -> (rule3 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is not young.
("Anne" "is" "young" "-")
int2
Anne is not kind.
False
5
inv-proof
[(((triple3 ((triple3 triple1) -> rule2)) -> rule3))]
("Anne" "is" "kind" "-")
((triple3 ((triple3 triple1) -> (rule2 % int2))) -> (rule3 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is not young.
("Anne" "is" "young" "-")
int2
Gary is not red.
Unknown
inv-rconc
[@1: Gary is red.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Gary" "is" "red" "-")
Gary is kind.
Unknown
rconc
[@1: Gary is kind.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Gary" "is" "kind" "+")
Charlie is not red.
Unknown
inv-rconc
[@1: Charlie is red.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Charlie" "is" "red" "-")
Gary is round.
Unknown
random
[@0: Gary is round.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "round" "+")
Erin is not round.
Unknown
inv-random
[@0: Erin is round.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "round" "-")
Charlie is young.
Unknown
random
[@0: Charlie is young.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "young" "+")
@0: Anne is nice.[(triple1)] Anne is red.[(triple2 OR ((triple1 triple3) -> rule1))] Anne is round.[(triple3)] Charlie is kind.[(triple4)] Erin is red.[(triple5)] Gary is blue.[(triple6)] Gary is young.[(triple7)] @1: Anne is not young.[(((triple3 triple1) -> rule2))] @2: Anne is kind.[(((triple3 ((triple3 triple1) -> rule2)) -> rule3))]
Anne is nice.
("Anne" "is" "nice" "+")
triple1
Anne is red.
("Anne" "is" "red" "+")
triple2
((triple1 triple3) -> (rule1 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
triple3
Charlie is kind.
("Charlie" "is" "kind" "+")
triple4
Erin is red.
("Erin" "is" "red" "+")
triple5
Gary is blue.
("Gary" "is" "blue" "+")
triple6
Gary is young.
("Gary" "is" "young" "+")
triple7
Anne is not young.
("Anne" "is" "young" "-")
((triple3 triple1) -> (rule2 % int1))
Anne is not young.
("Anne" "is" "young" "-")
int1
Anne is kind.
("Anne" "is" "kind" "+")
((triple3 ((triple3 triple1) -> (rule2 % int2))) -> (rule3 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is not young.
("Anne" "is" "young" "-")
int2