Dave is cold. Dave is furry. Dave is nice. Dave is not quiet. Dave is smart. Dave is white. Dave is not young. If Dave is smart then Dave is furry.
Dave is cold.
("Dave" "is" "cold" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is not quiet.
("Dave" "is" "quiet" "-")
Dave is smart.
("Dave" "is" "smart" "+")
Dave is white.
("Dave" "is" "white" "+")
Dave is not young.
("Dave" "is" "young" "-")
If Dave is smart then Dave is furry.
((("Dave" "is" "smart" "+")) -> ("Dave" "is" "furry" "+"))
Dave is furry.
True
1
proof
[(triple2 OR ((triple5) -> rule1))]
("Dave" "is" "furry" "+")
triple2
((triple5) -> (rule1 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is quiet.
False
1
inv-proof
[(triple4)]
("Dave" "is" "quiet" "+")
triple4
@0: Dave is cold.[(triple1)] Dave is furry.[(triple2 OR ((triple5) -> rule1))] Dave is nice.[(triple3)] Dave is not quiet.[(triple4)] Dave is not young.[(triple7)] Dave is smart.[(triple5)] Dave is white.[(triple6)]
Dave is cold.
("Dave" "is" "cold" "+")
triple1
Dave is furry.
("Dave" "is" "furry" "+")
triple2
((triple5) -> (rule1 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
triple3
Dave is not quiet.
("Dave" "is" "quiet" "-")
triple4
Dave is not young.
("Dave" "is" "young" "-")
triple7
Dave is smart.
("Dave" "is" "smart" "+")
triple5
Dave is white.
("Dave" "is" "white" "+")
triple6