Dave is big. Dave is blue. Dave is furry. Dave is green. Dave is not nice. Dave is red. Dave is not rough. If someone is furry and blue then they are green.
Dave is big.
("Dave" "is" "big" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is not nice.
("Dave" "is" "nice" "-")
Dave is red.
("Dave" "is" "red" "+")
Dave is not rough.
("Dave" "is" "rough" "-")
If someone is furry and blue then they are green.
((("someone" "is" "furry" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "green" "+"))
Dave is furry.
True
1
proof
[(triple3)]
("Dave" "is" "furry" "+")
triple3
Dave is not red.
False
1
inv-proof
[(triple6)]
("Dave" "is" "red" "-")
triple6
@0: Dave is big.[(triple1)] Dave is blue.[(triple2)] Dave is furry.[(triple3)] Dave is green.[(triple4 OR ((triple3 triple2) -> rule1))] Dave is not nice.[(triple5)] Dave is not rough.[(triple7)] Dave is red.[(triple6)]
Dave is big.
("Dave" "is" "big" "+")
triple1
Dave is blue.
("Dave" "is" "blue" "+")
triple2
Dave is furry.
("Dave" "is" "furry" "+")
triple3
Dave is green.
("Dave" "is" "green" "+")
triple4
((triple3 triple2) -> (rule1 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is not nice.
("Dave" "is" "nice" "-")
triple5
Dave is not rough.
("Dave" "is" "rough" "-")
triple7
Dave is red.
("Dave" "is" "red" "+")
triple6