Dave is big. Dave is furry. Dave is green. Dave is kind. Dave is rough. Dave is smart. Dave is white. Erin is big. Erin is furry. Erin is green. Erin is smart. Erin is white. All smart, big people are rough. If someone is green and furry then they are rough.
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 rough.
("Dave" "is" "rough" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Dave is white.
("Dave" "is" "white" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is green.
("Erin" "is" "green" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Erin is white.
("Erin" "is" "white" "+")
All smart, big people are rough.
((("someone" "is" "smart" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "rough" "+"))
If someone is green and furry then they are rough.
((("someone" "is" "green" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "rough" "+"))
Dave is green.
True
1
proof
[(triple3)]
("Dave" "is" "green" "+")
triple3
Dave is not white.
False
1
inv-proof
[(triple7)]
("Dave" "is" "white" "-")
triple7
@0: Dave is big.[(triple1)] Dave is furry.[(triple2)] Dave is green.[(triple3)] Dave is kind.[(triple4)] Dave is rough.[(triple5 OR ((triple3 triple2) -> rule2) OR ((triple6 triple1) -> rule1))] Dave is smart.[(triple6)] Dave is white.[(triple7)] Erin is big.[(triple8)] Erin is furry.[(triple9)] Erin is green.[(triple10)] Erin is smart.[(triple11)] Erin is white.[(triple12)] @1: Erin is rough.[(((triple10 triple9) -> rule2) OR ((triple11 triple8) -> rule1))]
Dave is big.
("Dave" "is" "big" "+")
triple1
Dave is furry.
("Dave" "is" "furry" "+")
triple2
Dave is green.
("Dave" "is" "green" "+")
triple3
Dave is kind.
("Dave" "is" "kind" "+")
triple4
Dave is rough.
("Dave" "is" "rough" "+")
triple5
((triple3 triple2) -> (rule2 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
((triple6 triple1) -> (rule1 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
triple6
Dave is white.
("Dave" "is" "white" "+")
triple7
Erin is big.
("Erin" "is" "big" "+")
triple8
Erin is furry.
("Erin" "is" "furry" "+")
triple9
Erin is green.
("Erin" "is" "green" "+")
triple10
Erin is smart.
("Erin" "is" "smart" "+")
triple11
Erin is white.
("Erin" "is" "white" "+")
triple12
Erin is rough.
("Erin" "is" "rough" "+")
((triple10 triple9) -> (rule2 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
((triple11 triple8) -> (rule1 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1