Dave is furry. Dave is green. Dave is kind. Dave is not red. Dave is rough. Dave is smart. Dave is young. Gary is furry. Gary is green. Gary is kind. Gary is not red. Gary is rough. Gary is smart. Gary is young. Rough people are green. All rough, young people are green. If someone is green and not smart then they are furry. If someone is kind then they are rough. If someone is smart then they are kind. Red, furry people are young.
Dave is furry.
("Dave" "is" "furry" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is not red.
("Dave" "is" "red" "-")
Dave is rough.
("Dave" "is" "rough" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Dave is young.
("Dave" "is" "young" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is not red.
("Gary" "is" "red" "-")
Gary is rough.
("Gary" "is" "rough" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Gary is young.
("Gary" "is" "young" "+")
Rough people are green.
((("someone" "is" "rough" "+")) -> ("someone" "is" "green" "+"))
All rough, young people are green.
((("someone" "is" "rough" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "green" "+"))
If someone is green and not smart then they are furry.
((("someone" "is" "green" "+") ("someone" "is" "smart" "~")) -> ("someone" "is" "furry" "+"))
If someone is kind then they are rough.
((("someone" "is" "kind" "+")) -> ("someone" "is" "rough" "+"))
If someone is smart then they are kind.
((("someone" "is" "smart" "+")) -> ("someone" "is" "kind" "+"))
Red, furry people are young.
((("someone" "is" "red" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "young" "+"))
Gary is young.
True
1
proof
[(triple14)]
("Gary" "is" "young" "+")
triple14
Dave is not furry.
False
1
inv-proof
[(triple1)]
("Dave" "is" "furry" "-")
triple1
@0: Dave is furry.[(triple1)] Dave is green.[(triple2 OR ((triple5) -> rule1) OR ((triple5 triple7) -> rule2) OR ((((triple3) -> rule4)) -> rule1) OR ((((triple3) -> rule4) triple7) -> rule2) OR ((((((triple6) -> rule5)) -> rule4)) -> rule1) OR ((((((triple6) -> rule5)) -> rule4) triple7) -> rule2))] Dave is kind.[(triple3 OR ((triple6) -> rule5))] Dave is not red.[(triple4)] Dave is rough.[(triple5 OR ((triple3) -> rule4) OR ((((triple6) -> rule5)) -> rule4))] Dave is smart.[(triple6)] Dave is young.[(triple7)] Gary is furry.[(triple8)] Gary is green.[(triple9 OR ((triple12) -> rule1) OR ((triple12 triple14) -> rule2) OR ((((triple10) -> rule4)) -> rule1) OR ((((triple10) -> rule4) triple14) -> rule2) OR ((((((triple13) -> rule5)) -> rule4)) -> rule1) OR ((((((triple13) -> rule5)) -> rule4) triple14) -> rule2))] Gary is kind.[(triple10 OR ((triple13) -> rule5))] Gary is not red.[(triple11)] Gary is rough.[(triple12 OR ((triple10) -> rule4) OR ((((triple13) -> rule5)) -> rule4))] Gary is smart.[(triple13)] Gary is young.[(triple14)]
Dave is furry.
("Dave" "is" "furry" "+")
triple1
Dave is green.
("Dave" "is" "green" "+")
triple2
((triple5) -> (rule1 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
((triple5 triple7) -> (rule2 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
((((triple3) -> (rule4 % int2))) -> (rule1 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
((((triple3) -> (rule4 % int2)) triple7) -> (rule2 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
((((((triple6) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
int3
((((((triple6) -> (rule5 % int3))) -> (rule4 % int2)) triple7) -> (rule2 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
int3
Dave is kind.
("Dave" "is" "kind" "+")
triple3
((triple6) -> (rule5 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is not red.
("Dave" "is" "red" "-")
triple4
Dave is rough.
("Dave" "is" "rough" "+")
triple5
((triple3) -> (rule4 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
((((triple6) -> (rule5 % int2))) -> (rule4 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
triple6
Dave is young.
("Dave" "is" "young" "+")
triple7
Gary is furry.
("Gary" "is" "furry" "+")
triple8
Gary is green.
("Gary" "is" "green" "+")
triple9
((triple12) -> (rule1 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
((triple12 triple14) -> (rule2 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
((((triple10) -> (rule4 % int2))) -> (rule1 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
((((triple10) -> (rule4 % int2)) triple14) -> (rule2 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
((((((triple13) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is kind.
("Gary" "is" "kind" "+")
int3
((((((triple13) -> (rule5 % int3))) -> (rule4 % int2)) triple14) -> (rule2 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is kind.
("Gary" "is" "kind" "+")
int3
Gary is kind.
("Gary" "is" "kind" "+")
triple10
((triple13) -> (rule5 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is not red.
("Gary" "is" "red" "-")
triple11
Gary is rough.
("Gary" "is" "rough" "+")
triple12
((triple10) -> (rule4 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
((((triple13) -> (rule5 % int2))) -> (rule4 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
triple13
Gary is young.
("Gary" "is" "young" "+")
triple14