Dave is blue. Dave is not furry. Dave is green. Dave is not kind. Dave is nice. Dave is rough. Dave is not young. All young, green things are furry. All blue things are not young. If something is nice and not blue then it is kind. If something is young and not furry then it is nice. If something is young and not blue then it is nice. All kind things are nice.
Dave is blue.
("Dave" "is" "blue" "+")
Dave is not furry.
("Dave" "is" "furry" "-")
Dave is green.
("Dave" "is" "green" "+")
Dave is not kind.
("Dave" "is" "kind" "-")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Dave is not young.
("Dave" "is" "young" "-")
All young, green things are furry.
((("something" "is" "young" "+") ("something" "is" "green" "+")) -> ("something" "is" "furry" "+"))
All blue things are not young.
((("something" "is" "blue" "+")) -> ("something" "is" "young" "-"))
If something is nice and not blue then it is kind.
((("something" "is" "nice" "+") ("something" "is" "blue" "~")) -> ("something" "is" "kind" "+"))
If something is young and not furry then it is nice.
((("something" "is" "young" "+") ("something" "is" "furry" "~")) -> ("something" "is" "nice" "+"))
If something is young and not blue then it is nice.
((("something" "is" "young" "+") ("something" "is" "blue" "~")) -> ("something" "is" "nice" "+"))
All kind things are nice.
((("something" "is" "kind" "+")) -> ("something" "is" "nice" "+"))
Dave is rough.
True
1
proof
[(triple6)]
("Dave" "is" "rough" "+")
triple6
Dave is furry.
False
1
inv-proof
[(triple2)]
("Dave" "is" "furry" "+")
triple2
@0: Dave is blue.[(triple1)] Dave is green.[(triple3)] Dave is nice.[(triple5)] Dave is not furry.[(triple2)] Dave is not kind.[(triple4)] Dave is not young.[(triple7 OR ((triple1) -> rule2))] Dave is rough.[(triple6)]
Dave is blue.
("Dave" "is" "blue" "+")
triple1
Dave is green.
("Dave" "is" "green" "+")
triple3
Dave is nice.
("Dave" "is" "nice" "+")
triple5
Dave is not furry.
("Dave" "is" "furry" "-")
triple2
Dave is not kind.
("Dave" "is" "kind" "-")
triple4
Dave is not young.
("Dave" "is" "young" "-")
triple7
((triple1) -> (rule2 % int1))
Dave is not young.
("Dave" "is" "young" "-")
int1
Dave is rough.
("Dave" "is" "rough" "+")
triple6