Fiona is furry. Fiona is kind. Fiona is nice. Fiona is rough. Fiona is smart. Fiona is white. Fiona is young. Gary is furry. Gary is kind. Gary is nice. Gary is rough. Gary is smart. Gary is white. Gary is young. If Gary is white and Gary is rough then Gary is smart. Furry, young things are rough.
Fiona is furry.
("Fiona" "is" "furry" "+")
Fiona is kind.
("Fiona" "is" "kind" "+")
Fiona is nice.
("Fiona" "is" "nice" "+")
Fiona is rough.
("Fiona" "is" "rough" "+")
Fiona is smart.
("Fiona" "is" "smart" "+")
Fiona is white.
("Fiona" "is" "white" "+")
Fiona is young.
("Fiona" "is" "young" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Gary is white.
("Gary" "is" "white" "+")
Gary is young.
("Gary" "is" "young" "+")
If Gary is white and Gary is rough then Gary is smart.
((("Gary" "is" "white" "+") ("Gary" "is" "rough" "+")) -> ("Gary" "is" "smart" "+"))
Furry, young things are rough.
((("something" "is" "furry" "+") ("something" "is" "young" "+")) -> ("something" "is" "rough" "+"))
Gary is rough.
True
1
proof
[(triple11 OR ((triple8 triple14) -> rule2))]
("Gary" "is" "rough" "+")
triple11
((triple8 triple14) -> (rule2 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is not white.
False
1
inv-proof
[(triple13)]
("Gary" "is" "white" "-")
triple13
@0: Fiona is furry.[(triple1)] Fiona is kind.[(triple2)] Fiona is nice.[(triple3)] Fiona is rough.[(triple4 OR ((triple1 triple7) -> rule2))] Fiona is smart.[(triple5)] Fiona is white.[(triple6)] Fiona is young.[(triple7)] Gary is furry.[(triple8)] Gary is kind.[(triple9)] Gary is nice.[(triple10)] Gary is rough.[(triple11 OR ((triple8 triple14) -> rule2))] Gary is smart.[(triple12 OR ((triple13 triple11) -> rule1) OR ((triple13 ((triple8 triple14) -> rule2)) -> rule1))] Gary is white.[(triple13)] Gary is young.[(triple14)]
Fiona is furry.
("Fiona" "is" "furry" "+")
triple1
Fiona is kind.
("Fiona" "is" "kind" "+")
triple2
Fiona is nice.
("Fiona" "is" "nice" "+")
triple3
Fiona is rough.
("Fiona" "is" "rough" "+")
triple4
((triple1 triple7) -> (rule2 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
triple5
Fiona is white.
("Fiona" "is" "white" "+")
triple6
Fiona is young.
("Fiona" "is" "young" "+")
triple7
Gary is furry.
("Gary" "is" "furry" "+")
triple8
Gary is kind.
("Gary" "is" "kind" "+")
triple9
Gary is nice.
("Gary" "is" "nice" "+")
triple10
Gary is rough.
("Gary" "is" "rough" "+")
triple11
((triple8 triple14) -> (rule2 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
triple12
((triple13 triple11) -> (rule1 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
((triple13 ((triple8 triple14) -> (rule2 % int2))) -> (rule1 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
triple13
Gary is young.
("Gary" "is" "young" "+")
triple14