Anne is big. Charlie is red. Dave is nice. Gary is red. If Dave is nice and Dave is kind then Dave is young. All red people are nice. If Dave is red then Dave is cold.
Anne is big.
("Anne" "is" "big" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Gary is red.
("Gary" "is" "red" "+")
If Dave is nice and Dave is kind then Dave is young.
((("Dave" "is" "nice" "+") ("Dave" "is" "kind" "+")) -> ("Dave" "is" "young" "+"))
All red people are nice.
((("someone" "is" "red" "+")) -> ("someone" "is" "nice" "+"))
If Dave is red then Dave is cold.
((("Dave" "is" "red" "+")) -> ("Dave" "is" "cold" "+"))
Dave is nice.
True
1
proof
[(triple3)]
("Dave" "is" "nice" "+")
triple3
Charlie is not red.
False
1
inv-proof
[(triple2)]
("Charlie" "is" "red" "-")
triple2
Gary is nice.
True
2
proof
[(((triple4) -> rule2))]
("Gary" "is" "nice" "+")
((triple4) -> (rule2 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is not nice.
False
2
inv-proof
[(((triple4) -> rule2))]
("Gary" "is" "nice" "-")
((triple4) -> (rule2 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Anne is not nice.
Unknown
inv-rconc
[@1: Anne is nice.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Anne" "is" "nice" "-")
Dave is young.
Unknown
rconc
[@1: Dave is young.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Dave" "is" "young" "+")
Anne is not red.
Unknown
inv-random
[@0: Anne is red.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "red" "-")
Charlie is young.
Unknown
random
[@0: Charlie is young.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "young" "+")
@0: Anne is big.[(triple1)] Charlie is red.[(triple2)] Dave is nice.[(triple3)] Gary is red.[(triple4)] @1: Charlie is nice.[(((triple2) -> rule2))] Gary is nice.[(((triple4) -> rule2))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Charlie is red.
("Charlie" "is" "red" "+")
triple2
Dave is nice.
("Dave" "is" "nice" "+")
triple3
Gary is red.
("Gary" "is" "red" "+")
triple4
Charlie is nice.
("Charlie" "is" "nice" "+")
((triple2) -> (rule2 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
((triple4) -> (rule2 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1