Dave is not furry. Dave is green. Dave is kind. Dave is quiet. Dave is red. Dave is round. Dave is not smart. Gary is furry. Gary is green. Gary is kind. Gary is quiet. Gary is red. Gary is not round. Gary is not smart. If Gary is green then Gary is red. If Gary is smart then Gary is red.
Dave is not furry.
("Dave" "is" "furry" "-")
Dave is green.
("Dave" "is" "green" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is round.
("Dave" "is" "round" "+")
Dave is not smart.
("Dave" "is" "smart" "-")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is not round.
("Gary" "is" "round" "-")
Gary is not smart.
("Gary" "is" "smart" "-")
If Gary is green then Gary is red.
((("Gary" "is" "green" "+")) -> ("Gary" "is" "red" "+"))
If Gary is smart then Gary is red.
((("Gary" "is" "smart" "+")) -> ("Gary" "is" "red" "+"))
Dave is kind.
True
1
proof
[(triple3)]
("Dave" "is" "kind" "+")
triple3
Gary is not green.
False
1
inv-proof
[(triple9)]
("Gary" "is" "green" "-")
triple9
@0: Dave is green.[(triple2)] Dave is kind.[(triple3)] Dave is not furry.[(triple1)] Dave is not smart.[(triple7)] Dave is quiet.[(triple4)] Dave is red.[(triple5)] Dave is round.[(triple6)] Gary is furry.[(triple8)] Gary is green.[(triple9)] Gary is kind.[(triple10)] Gary is not round.[(triple13)] Gary is not smart.[(triple14)] Gary is quiet.[(triple11)] Gary is red.[(triple12 OR ((triple9) -> rule1))]
Dave is green.
("Dave" "is" "green" "+")
triple2
Dave is kind.
("Dave" "is" "kind" "+")
triple3
Dave is not furry.
("Dave" "is" "furry" "-")
triple1
Dave is not smart.
("Dave" "is" "smart" "-")
triple7
Dave is quiet.
("Dave" "is" "quiet" "+")
triple4
Dave is red.
("Dave" "is" "red" "+")
triple5
Dave is round.
("Dave" "is" "round" "+")
triple6
Gary is furry.
("Gary" "is" "furry" "+")
triple8
Gary is green.
("Gary" "is" "green" "+")
triple9
Gary is kind.
("Gary" "is" "kind" "+")
triple10
Gary is not round.
("Gary" "is" "round" "-")
triple13
Gary is not smart.
("Gary" "is" "smart" "-")
triple14
Gary is quiet.
("Gary" "is" "quiet" "+")
triple11
Gary is red.
("Gary" "is" "red" "+")
triple12
((triple9) -> (rule1 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1