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