Dave is big. Dave is furry. Dave is green. Dave is kind. Dave is quiet. Dave is rough. Dave is white. All quiet, rough things are white.
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 quiet.
("Dave" "is" "quiet" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Dave is white.
("Dave" "is" "white" "+")
All quiet, rough things are white.
((("something" "is" "quiet" "+") ("something" "is" "rough" "+")) -> ("something" "is" "white" "+"))
Dave is white.
True
1
proof
[(triple7 OR ((triple5 triple6) -> rule1))]
("Dave" "is" "white" "+")
triple7
((triple5 triple6) -> (rule1 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is not rough.
False
1
inv-proof
[(triple6)]
("Dave" "is" "rough" "-")
triple6
@0: Dave is big.[(triple1)] Dave is furry.[(triple2)] Dave is green.[(triple3)] Dave is kind.[(triple4)] Dave is quiet.[(triple5)] Dave is rough.[(triple6)] Dave is white.[(triple7 OR ((triple5 triple6) -> 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 quiet.
("Dave" "is" "quiet" "+")
triple5
Dave is rough.
("Dave" "is" "rough" "+")
triple6
Dave is white.
("Dave" "is" "white" "+")
triple7
((triple5 triple6) -> (rule1 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1