Anne is furry. Anne is kind. Anne is quiet. Anne is red. Anne is rough. Anne is round. Anne is smart. Charlie is furry. Charlie is kind. Charlie is red. Charlie is rough. Charlie is round. Charlie is smart. Gary is rough. Gary is smart. Harry is kind. If someone is smart then they are rough. Round, red people are kind.
Anne is furry.
("Anne" "is" "furry" "+")
Anne is kind.
("Anne" "is" "kind" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is red.
("Anne" "is" "red" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Anne is round.
("Anne" "is" "round" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Harry is kind.
("Harry" "is" "kind" "+")
If someone is smart then they are rough.
((("someone" "is" "smart" "+")) -> ("someone" "is" "rough" "+"))
Round, red people are kind.
((("someone" "is" "round" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "kind" "+"))
Anne is rough.
True
1
proof
[(triple5 OR ((triple7) -> rule1))]
("Anne" "is" "rough" "+")
triple5
((triple7) -> (rule1 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is not furry.
False
1
inv-proof
[(triple1)]
("Anne" "is" "furry" "-")
triple1
Gary is not kind.
Unknown
inv-rconc
[@1: Gary is kind.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Gary" "is" "kind" "-")
Charlie is quiet.
Unknown
random
[@0: Charlie is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "quiet" "+")
@0: Anne is furry.[(triple1)] Anne is kind.[(triple2 OR ((triple6 triple4) -> rule2))] Anne is quiet.[(triple3)] Anne is red.[(triple4)] Anne is rough.[(triple5 OR ((triple7) -> rule1))] Anne is round.[(triple6)] Anne is smart.[(triple7)] Charlie is furry.[(triple8)] Charlie is kind.[(triple9 OR ((triple12 triple10) -> rule2))] Charlie is red.[(triple10)] Charlie is rough.[(triple11 OR ((triple13) -> rule1))] Charlie is round.[(triple12)] Charlie is smart.[(triple13)] Gary is rough.[(triple14 OR ((triple15) -> rule1))] Gary is smart.[(triple15)] Harry is kind.[(triple16)]
Anne is furry.
("Anne" "is" "furry" "+")
triple1
Anne is kind.
("Anne" "is" "kind" "+")
triple2
((triple6 triple4) -> (rule2 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
triple3
Anne is red.
("Anne" "is" "red" "+")
triple4
Anne is rough.
("Anne" "is" "rough" "+")
triple5
((triple7) -> (rule1 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
triple6
Anne is smart.
("Anne" "is" "smart" "+")
triple7
Charlie is furry.
("Charlie" "is" "furry" "+")
triple8
Charlie is kind.
("Charlie" "is" "kind" "+")
triple9
((triple12 triple10) -> (rule2 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
triple10
Charlie is rough.
("Charlie" "is" "rough" "+")
triple11
((triple13) -> (rule1 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
triple12
Charlie is smart.
("Charlie" "is" "smart" "+")
triple13
Gary is rough.
("Gary" "is" "rough" "+")
triple14
((triple15) -> (rule1 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
triple15
Harry is kind.
("Harry" "is" "kind" "+")
triple16