Dave is furry. Dave is green. Dave is nice. Dave is not red. Dave is rough. Dave is not smart. Dave is white. Gary is furry. Gary is not green. Gary is nice. Gary is red. Gary is rough. Gary is smart. Gary is white. Furry people are rough. If Dave is furry then Dave is nice. White people are furry. If someone is smart and green then they are furry. If someone is smart and not white then they are not nice. If Dave is furry and Dave is not green then Dave is not red.
Dave is furry.
("Dave" "is" "furry" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is not red.
("Dave" "is" "red" "-")
Dave is rough.
("Dave" "is" "rough" "+")
Dave is not smart.
("Dave" "is" "smart" "-")
Dave is white.
("Dave" "is" "white" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is not green.
("Gary" "is" "green" "-")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Gary is white.
("Gary" "is" "white" "+")
Furry people are rough.
((("someone" "is" "furry" "+")) -> ("someone" "is" "rough" "+"))
If Dave is furry then Dave is nice.
((("Dave" "is" "furry" "+")) -> ("Dave" "is" "nice" "+"))
White people are furry.
((("someone" "is" "white" "+")) -> ("someone" "is" "furry" "+"))
If someone is smart and green then they are furry.
((("someone" "is" "smart" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "furry" "+"))
If someone is smart and not white then they are not nice.
((("someone" "is" "smart" "+") ("someone" "is" "white" "~")) -> ("someone" "is" "nice" "-"))
If Dave is furry and Dave is not green then Dave is not red.
((("Dave" "is" "furry" "+") ("Dave" "is" "green" "~")) -> ("Dave" "is" "red" "-"))
Dave is rough.
True
1
proof
[(triple5 OR ((triple1) -> rule1) OR ((((triple7) -> rule3)) -> rule1))]
("Dave" "is" "rough" "+")
triple5
((triple1) -> (rule1 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
((((triple7) -> (rule3 % int2))) -> (rule1 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is smart.
False
1
inv-proof
[(triple6)]
("Dave" "is" "smart" "+")
triple6
@0: Dave is furry.[(triple1 OR ((triple7) -> rule3))] Dave is green.[(triple2)] Dave is nice.[(triple3 OR ((triple1) -> rule2) OR ((((triple7) -> rule3)) -> rule2))] Dave is not red.[(triple4)] Dave is not smart.[(triple6)] Dave is rough.[(triple5 OR ((triple1) -> rule1) OR ((((triple7) -> rule3)) -> rule1))] Dave is white.[(triple7)] Gary is furry.[(triple8 OR ((triple14) -> rule3))] Gary is nice.[(triple10)] Gary is not green.[(triple9)] Gary is red.[(triple11)] Gary is rough.[(triple12 OR ((triple8) -> rule1) OR ((((triple14) -> rule3)) -> rule1))] Gary is smart.[(triple13)] Gary is white.[(triple14)]
Dave is furry.
("Dave" "is" "furry" "+")
triple1
((triple7) -> (rule3 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
triple2
Dave is nice.
("Dave" "is" "nice" "+")
triple3
((triple1) -> (rule2 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
((((triple7) -> (rule3 % int2))) -> (rule2 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is not red.
("Dave" "is" "red" "-")
triple4
Dave is not smart.
("Dave" "is" "smart" "-")
triple6
Dave is rough.
("Dave" "is" "rough" "+")
triple5
((triple1) -> (rule1 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
((((triple7) -> (rule3 % int2))) -> (rule1 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
triple7
Gary is furry.
("Gary" "is" "furry" "+")
triple8
((triple14) -> (rule3 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
triple10
Gary is not green.
("Gary" "is" "green" "-")
triple9
Gary is red.
("Gary" "is" "red" "+")
triple11
Gary is rough.
("Gary" "is" "rough" "+")
triple12
((triple8) -> (rule1 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
((((triple14) -> (rule3 % int2))) -> (rule1 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
triple13
Gary is white.
("Gary" "is" "white" "+")
triple14