Anne is blue. Anne is nice. Dave is blue. Dave is kind. Dave is nice. Dave is quiet. Dave is round. If someone is quiet and blue then they are kind. Smart, red people are blue.
Anne is blue.
("Anne" "is" "blue" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is round.
("Dave" "is" "round" "+")
If someone is quiet and blue then they are kind.
((("someone" "is" "quiet" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "kind" "+"))
Smart, red people are blue.
((("someone" "is" "smart" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "blue" "+"))
Dave is quiet.
True
1
proof
[(triple6)]
("Dave" "is" "quiet" "+")
triple6
Dave is not nice.
False
1
inv-proof
[(triple5)]
("Dave" "is" "nice" "-")
triple5
Anne is not kind.
Unknown
inv-rconc
[@1: Anne is kind.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Anne" "is" "kind" "-")
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 nice.[(triple2)] Dave is blue.[(triple3)] Dave is kind.[(triple4 OR ((triple6 triple3) -> rule1))] Dave is nice.[(triple5)] Dave is quiet.[(triple6)] Dave is round.[(triple7)]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Anne is nice.
("Anne" "is" "nice" "+")
triple2
Dave is blue.
("Dave" "is" "blue" "+")
triple3
Dave is kind.
("Dave" "is" "kind" "+")
triple4
((triple6 triple3) -> (rule1 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
triple5
Dave is quiet.
("Dave" "is" "quiet" "+")
triple6
Dave is round.
("Dave" "is" "round" "+")
triple7