Gary is cold. Gary is furry. Gary is kind. Gary is nice. Gary is red. Gary is white. Gary is young. All white, kind things are furry. If something is red and kind then it is white. If something is cold and red then it is kind.
Gary is cold.
("Gary" "is" "cold" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is white.
("Gary" "is" "white" "+")
Gary is young.
("Gary" "is" "young" "+")
All white, kind things are furry.
((("something" "is" "white" "+") ("something" "is" "kind" "+")) -> ("something" "is" "furry" "+"))
If something is red and kind then it is white.
((("something" "is" "red" "+") ("something" "is" "kind" "+")) -> ("something" "is" "white" "+"))
If something is cold and red then it is kind.
((("something" "is" "cold" "+") ("something" "is" "red" "+")) -> ("something" "is" "kind" "+"))
Gary is kind.
True
1
proof
[(triple3 OR ((triple1 triple5) -> rule3))]
("Gary" "is" "kind" "+")
triple3
((triple1 triple5) -> (rule3 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is not cold.
False
1
inv-proof
[(triple1)]
("Gary" "is" "cold" "-")
triple1
@0: Gary is cold.[(triple1)] Gary is furry.[(triple2 OR ((triple6 triple3) -> rule1) OR ((triple6 ((triple1 triple5) -> rule3)) -> rule1) OR ((((triple5 triple3) -> rule2) triple3) -> rule1) OR ((((triple5 triple3) -> rule2) ((triple1 triple5) -> rule3)) -> rule1) OR ((((triple5 ((triple1 triple5) -> rule3)) -> rule2) triple3) -> rule1) OR ((((triple5 ((triple1 triple5) -> rule3)) -> rule2) ((triple1 triple5) -> rule3)) -> rule1))] Gary is kind.[(triple3 OR ((triple1 triple5) -> rule3))] Gary is nice.[(triple4)] Gary is red.[(triple5)] Gary is white.[(triple6 OR ((triple5 triple3) -> rule2) OR ((triple5 ((triple1 triple5) -> rule3)) -> rule2))] Gary is young.[(triple7)]
Gary is cold.
("Gary" "is" "cold" "+")
triple1
Gary is furry.
("Gary" "is" "furry" "+")
triple2
((triple6 triple3) -> (rule1 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
((triple6 ((triple1 triple5) -> (rule3 % int2))) -> (rule1 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
((((triple5 triple3) -> (rule2 % int2)) triple3) -> (rule1 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
((((triple5 triple3) -> (rule2 % int3)) ((triple1 triple5) -> (rule3 % int2))) -> (rule1 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
int3
((((triple5 ((triple1 triple5) -> (rule3 % int3))) -> (rule2 % int2)) triple3) -> (rule1 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is kind.
("Gary" "is" "kind" "+")
int3
((((triple5 ((triple1 triple5) -> (rule3 % int3))) -> (rule2 % int2)) ((triple1 triple5) -> (rule3 % int3))) -> (rule1 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is kind.
("Gary" "is" "kind" "+")
int3
Gary is kind.
("Gary" "is" "kind" "+")
triple3
((triple1 triple5) -> (rule3 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
triple4
Gary is red.
("Gary" "is" "red" "+")
triple5
Gary is white.
("Gary" "is" "white" "+")
triple6
((triple5 triple3) -> (rule2 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
((triple5 ((triple1 triple5) -> (rule3 % int2))) -> (rule2 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is young.
("Gary" "is" "young" "+")
triple7