Anne is furry. Anne is red. Anne is rough. Anne is smart. Anne is not white. Dave is not nice. Dave is red. Dave is rough. Dave is smart. Dave is white. Dave is young. Erin is furry. Erin is red. Erin is smart. Erin is not white. Erin is not young. If someone is young and white then they are furry. If someone is young then they are smart. All red people are smart. If someone is white and furry then they are smart. If Dave is young then Dave is not nice. If someone is white then they are rough. All white people are rough. If someone is furry and not young then they are nice.
Anne is furry.
("Anne" "is" "furry" "+")
Anne is red.
("Anne" "is" "red" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Anne is not white.
("Anne" "is" "white" "-")
Dave is not nice.
("Dave" "is" "nice" "-")
Dave is red.
("Dave" "is" "red" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Dave is white.
("Dave" "is" "white" "+")
Dave is young.
("Dave" "is" "young" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is red.
("Erin" "is" "red" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Erin is not white.
("Erin" "is" "white" "-")
Erin is not young.
("Erin" "is" "young" "-")
If someone is young and white then they are furry.
((("someone" "is" "young" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "furry" "+"))
If someone is young then they are smart.
((("someone" "is" "young" "+")) -> ("someone" "is" "smart" "+"))
All red people are smart.
((("someone" "is" "red" "+")) -> ("someone" "is" "smart" "+"))
If someone is white and furry then they are smart.
((("someone" "is" "white" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "smart" "+"))
If Dave is young then Dave is not nice.
((("Dave" "is" "young" "+")) -> ("Dave" "is" "nice" "-"))
If someone is white then they are rough.
((("someone" "is" "white" "+")) -> ("someone" "is" "rough" "+"))
All white people are rough.
((("someone" "is" "white" "+")) -> ("someone" "is" "rough" "+"))
If someone is furry and not young then they are nice.
((("someone" "is" "furry" "+") ("someone" "is" "young" "~")) -> ("someone" "is" "nice" "+"))
Dave is smart.
True
1
proof
[(triple9 OR ((triple11) -> rule2) OR ((triple7) -> rule3) OR ((triple10 ((triple11 triple10) -> rule1)) -> rule4))]
("Dave" "is" "smart" "+")
triple9
((triple11) -> (rule2 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
((triple7) -> (rule3 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
((triple10 ((triple11 triple10) -> (rule1 % int2))) -> (rule4 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Anne is white.
False
1
inv-proof
[(triple5)]
("Anne" "is" "white" "+")
triple5
Erin is nice.
True
3
proof
[(((triple12 triple16) -> rule8))]
("Erin" "is" "nice" "+")
((triple12 triple16) -> (rule8 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Dave is not furry.
False
3
inv-proof
[(((triple11 triple10) -> rule1))]
("Dave" "is" "furry" "-")
((triple11 triple10) -> (rule1 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Anne is not nice.
Unknown
inv-rconc
[@1: Anne is nice.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Anne" "is" "nice" "-")
Erin is rough.
Unknown
rconc
[@1: Erin is rough.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Erin" "is" "rough" "+")
@0: Anne is furry.[(triple1)] Anne is not white.[(triple5)] Anne is red.[(triple2)] Anne is rough.[(triple3)] Anne is smart.[(triple4 OR ((triple2) -> rule3))] Dave is not nice.[(triple6 OR ((triple11) -> rule5))] Dave is red.[(triple7)] Dave is rough.[(triple8 OR ((triple10) -> rule6) OR ((triple10) -> rule7))] Dave is smart.[(triple9 OR ((triple11) -> rule2) OR ((triple7) -> rule3) OR ((triple10 ((triple11 triple10) -> rule1)) -> rule4))] Dave is white.[(triple10)] Dave is young.[(triple11)] Erin is furry.[(triple12)] Erin is not white.[(triple15)] Erin is not young.[(triple16)] Erin is red.[(triple13)] Erin is smart.[(triple14 OR ((triple13) -> rule3))] @1: Dave is furry.[(((triple11 triple10) -> rule1))] Erin is nice.[(((triple12 triple16) -> rule8))]
Anne is furry.
("Anne" "is" "furry" "+")
triple1
Anne is not white.
("Anne" "is" "white" "-")
triple5
Anne is red.
("Anne" "is" "red" "+")
triple2
Anne is rough.
("Anne" "is" "rough" "+")
triple3
Anne is smart.
("Anne" "is" "smart" "+")
triple4
((triple2) -> (rule3 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Dave is not nice.
("Dave" "is" "nice" "-")
triple6
((triple11) -> (rule5 % int1))
Dave is not nice.
("Dave" "is" "nice" "-")
int1
Dave is red.
("Dave" "is" "red" "+")
triple7
Dave is rough.
("Dave" "is" "rough" "+")
triple8
((triple10) -> (rule6 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
((triple10) -> (rule7 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
triple9
((triple11) -> (rule2 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
((triple7) -> (rule3 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
((triple10 ((triple11 triple10) -> (rule1 % int2))) -> (rule4 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
triple10
Dave is young.
("Dave" "is" "young" "+")
triple11
Erin is furry.
("Erin" "is" "furry" "+")
triple12
Erin is not white.
("Erin" "is" "white" "-")
triple15
Erin is not young.
("Erin" "is" "young" "-")
triple16
Erin is red.
("Erin" "is" "red" "+")
triple13
Erin is smart.
("Erin" "is" "smart" "+")
triple14
((triple13) -> (rule3 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
((triple11 triple10) -> (rule1 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
((triple12 triple16) -> (rule8 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1