Gary is kind. All kind, cold things are blue. All big things are kind. All big, blue things are kind. Blue things are young. All kind things are red. Red things are big. Blue, round things are big. All kind things are cold.
Gary is kind.
("Gary" "is" "kind" "+")
All kind, cold things are blue.
((("something" "is" "kind" "+") ("something" "is" "cold" "+")) -> ("something" "is" "blue" "+"))
All big things are kind.
((("something" "is" "big" "+")) -> ("something" "is" "kind" "+"))
All big, blue things are kind.
((("something" "is" "big" "+") ("something" "is" "blue" "+")) -> ("something" "is" "kind" "+"))
Blue things are young.
((("something" "is" "blue" "+")) -> ("something" "is" "young" "+"))
All kind things are red.
((("something" "is" "kind" "+")) -> ("something" "is" "red" "+"))
Red things are big.
((("something" "is" "red" "+")) -> ("something" "is" "big" "+"))
Blue, round things are big.
((("something" "is" "blue" "+") ("something" "is" "round" "+")) -> ("something" "is" "big" "+"))
All kind things are cold.
((("something" "is" "kind" "+")) -> ("something" "is" "cold" "+"))
Gary is kind.
True
1
proof
[(triple1)]
("Gary" "is" "kind" "+")
triple1
Gary is not kind.
False
1
inv-proof
[(triple1)]
("Gary" "is" "kind" "-")
triple1
Gary is cold.
True
2
proof
[(((triple1) -> rule8))]
("Gary" "is" "cold" "+")
((triple1) -> (rule8 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is not red.
False
2
inv-proof
[(((triple1) -> rule5))]
("Gary" "is" "red" "-")
((triple1) -> (rule5 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
@0: Gary is kind.[(triple1)] @1: Gary is cold.[(((triple1) -> rule8))] Gary is red.[(((triple1) -> rule5))] @2: Gary is big.[(((((triple1) -> rule5)) -> rule6))] Gary is blue.[(((triple1 ((triple1) -> rule8)) -> rule1))] @3: Gary is young.[(((((triple1 ((triple1) -> rule8)) -> rule1)) -> rule4))]
Gary is kind.
("Gary" "is" "kind" "+")
triple1
Gary is cold.
("Gary" "is" "cold" "+")
((triple1) -> (rule8 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
((triple1) -> (rule5 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
((((triple1) -> (rule5 % int2))) -> (rule6 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
((triple1 ((triple1) -> (rule8 % int2))) -> (rule1 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is young.
("Gary" "is" "young" "+")
((((triple1 ((triple1) -> (rule8 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
int3