Anne is big. Anne is nice. Anne is quiet. Anne is young. Dave is kind. Dave is nice. Dave is quiet. Dave is round. Dave is young. Gary is big. Gary is nice. Gary is round. If someone is kind then they are nice. If Gary is young then Gary is nice. All kind people are green.
Anne is big.
("Anne" "is" "big" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is young.
("Anne" "is" "young" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is round.
("Dave" "is" "round" "+")
Dave is young.
("Dave" "is" "young" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is round.
("Gary" "is" "round" "+")
If someone is kind then they are nice.
((("someone" "is" "kind" "+")) -> ("someone" "is" "nice" "+"))
If Gary is young then Gary is nice.
((("Gary" "is" "young" "+")) -> ("Gary" "is" "nice" "+"))
All kind people are green.
((("someone" "is" "kind" "+")) -> ("someone" "is" "green" "+"))
Dave is nice.
True
1
proof
[(triple6 OR ((triple5) -> rule1))]
("Dave" "is" "nice" "+")
triple6
((triple5) -> (rule1 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Gary is not nice.
False
1
inv-proof
[(triple11)]
("Gary" "is" "nice" "-")
triple11
Dave is green.
True
2
proof
[(((triple5) -> rule3))]
("Dave" "is" "green" "+")
((triple5) -> (rule3 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is not green.
False
2
inv-proof
[(((triple5) -> rule3))]
("Dave" "is" "green" "-")
((triple5) -> (rule3 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Anne is not green.
Unknown
inv-rconc
[@1: Anne is green.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Anne" "is" "green" "-")
Gary is green.
Unknown
rconc
[@1: Gary is green.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Gary" "is" "green" "+")
Dave is not big.
Unknown
inv-random
[@0: Dave is big.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "big" "-")
Gary is kind.
Unknown
random
[@0: Gary is kind.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "kind" "+")
@0: Anne is big.[(triple1)] Anne is nice.[(triple2)] Anne is quiet.[(triple3)] Anne is young.[(triple4)] Dave is kind.[(triple5)] Dave is nice.[(triple6 OR ((triple5) -> rule1))] Dave is quiet.[(triple7)] Dave is round.[(triple8)] Dave is young.[(triple9)] Gary is big.[(triple10)] Gary is nice.[(triple11)] Gary is round.[(triple12)] @1: Dave is green.[(((triple5) -> rule3))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is nice.
("Anne" "is" "nice" "+")
triple2
Anne is quiet.
("Anne" "is" "quiet" "+")
triple3
Anne is young.
("Anne" "is" "young" "+")
triple4
Dave is kind.
("Dave" "is" "kind" "+")
triple5
Dave is nice.
("Dave" "is" "nice" "+")
triple6
((triple5) -> (rule1 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
triple7
Dave is round.
("Dave" "is" "round" "+")
triple8
Dave is young.
("Dave" "is" "young" "+")
triple9
Gary is big.
("Gary" "is" "big" "+")
triple10
Gary is nice.
("Gary" "is" "nice" "+")
triple11
Gary is round.
("Gary" "is" "round" "+")
triple12
Dave is green.
("Dave" "is" "green" "+")
((triple5) -> (rule3 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1