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