Gary is big. Gary is furry. Gary is quiet. Gary is red. Gary is rough. Gary is white. Gary is young. All quiet, white people are young. If someone is young and rough then they are red.
Gary is big.
("Gary" "is" "big" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Gary is white.
("Gary" "is" "white" "+")
Gary is young.
("Gary" "is" "young" "+")
All quiet, white people are young.
((("someone" "is" "quiet" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "young" "+"))
If someone is young and rough then they are red.
((("someone" "is" "young" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "red" "+"))
Gary is furry.
True
1
proof
[(triple2)]
("Gary" "is" "furry" "+")
triple2
Gary is not red.
False
1
inv-proof
[(triple4 OR ((triple7 triple5) -> rule2) OR ((((triple3 triple6) -> rule1) triple5) -> rule2))]
("Gary" "is" "red" "-")
triple4
((triple7 triple5) -> (rule2 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
((((triple3 triple6) -> (rule1 % int2)) triple5) -> (rule2 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
@0: Gary is big.[(triple1)] Gary is furry.[(triple2)] Gary is quiet.[(triple3)] Gary is red.[(triple4 OR ((triple7 triple5) -> rule2) OR ((((triple3 triple6) -> rule1) triple5) -> rule2))] Gary is rough.[(triple5)] Gary is white.[(triple6)] Gary is young.[(triple7 OR ((triple3 triple6) -> rule1))]
Gary is big.
("Gary" "is" "big" "+")
triple1
Gary is furry.
("Gary" "is" "furry" "+")
triple2
Gary is quiet.
("Gary" "is" "quiet" "+")
triple3
Gary is red.
("Gary" "is" "red" "+")
triple4
((triple7 triple5) -> (rule2 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
((((triple3 triple6) -> (rule1 % int2)) triple5) -> (rule2 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
triple5
Gary is white.
("Gary" "is" "white" "+")
triple6
Gary is young.
("Gary" "is" "young" "+")
triple7
((triple3 triple6) -> (rule1 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1