Anne is not blue. Anne is furry. Anne is not green. Anne is kind. Anne is nice. Anne is white. Anne is young. Dave is blue. Dave is furry. Dave is green. Dave is kind. Dave is nice. Dave is white. Dave is young. All blue, white people are nice. If Anne is young and Anne is white then Anne is kind.
Anne is not blue.
("Anne" "is" "blue" "-")
Anne is furry.
("Anne" "is" "furry" "+")
Anne is not green.
("Anne" "is" "green" "-")
Anne is kind.
("Anne" "is" "kind" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Anne is white.
("Anne" "is" "white" "+")
Anne is young.
("Anne" "is" "young" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is white.
("Dave" "is" "white" "+")
Dave is young.
("Dave" "is" "young" "+")
All blue, white people are nice.
((("someone" "is" "blue" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "nice" "+"))
If Anne is young and Anne is white then Anne is kind.
((("Anne" "is" "young" "+") ("Anne" "is" "white" "+")) -> ("Anne" "is" "kind" "+"))
Dave is nice.
True
1
proof
[(triple12 OR ((triple8 triple13) -> rule1))]
("Dave" "is" "nice" "+")
triple12
((triple8 triple13) -> (rule1 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is not blue.
False
1
inv-proof
[(triple8)]
("Dave" "is" "blue" "-")
triple8
@0: Anne is furry.[(triple2)] Anne is kind.[(triple4 OR ((triple7 triple6) -> rule2))] Anne is nice.[(triple5)] Anne is not blue.[(triple1)] Anne is not green.[(triple3)] Anne is white.[(triple6)] Anne is young.[(triple7)] Dave is blue.[(triple8)] Dave is furry.[(triple9)] Dave is green.[(triple10)] Dave is kind.[(triple11)] Dave is nice.[(triple12 OR ((triple8 triple13) -> rule1))] Dave is white.[(triple13)] Dave is young.[(triple14)]
Anne is furry.
("Anne" "is" "furry" "+")
triple2
Anne is kind.
("Anne" "is" "kind" "+")
triple4
((triple7 triple6) -> (rule2 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
triple5
Anne is not blue.
("Anne" "is" "blue" "-")
triple1
Anne is not green.
("Anne" "is" "green" "-")
triple3
Anne is white.
("Anne" "is" "white" "+")
triple6
Anne is young.
("Anne" "is" "young" "+")
triple7
Dave is blue.
("Dave" "is" "blue" "+")
triple8
Dave is furry.
("Dave" "is" "furry" "+")
triple9
Dave is green.
("Dave" "is" "green" "+")
triple10
Dave is kind.
("Dave" "is" "kind" "+")
triple11
Dave is nice.
("Dave" "is" "nice" "+")
triple12
((triple8 triple13) -> (rule1 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
triple13
Dave is young.
("Dave" "is" "young" "+")
triple14