Gary is not blue. Gary is furry. Gary is rough. If someone is cold and not furry then they are young. If someone is rough and red then they are young. If someone is furry and cold then they are red. All furry, green people are blue. Rough people are cold. All cold, red people are not green.
Gary is not blue.
("Gary" "is" "blue" "-")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is rough.
("Gary" "is" "rough" "+")
If someone is cold and not furry then they are young.
((("someone" "is" "cold" "+") ("someone" "is" "furry" "~")) -> ("someone" "is" "young" "+"))
If someone is rough and red then they are young.
((("someone" "is" "rough" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "young" "+"))
If someone is furry and cold then they are red.
((("someone" "is" "furry" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "red" "+"))
All furry, green people are blue.
((("someone" "is" "furry" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "blue" "+"))
Rough people are cold.
((("someone" "is" "rough" "+")) -> ("someone" "is" "cold" "+"))
All cold, red people are not green.
((("someone" "is" "cold" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "green" "-"))
Gary is rough.
True
1
proof
[(triple3)]
("Gary" "is" "rough" "+")
triple3
Gary is not rough.
False
1
inv-proof
[(triple3)]
("Gary" "is" "rough" "-")
triple3
Gary is cold.
True
2
proof
[(((triple3) -> rule5))]
("Gary" "is" "cold" "+")
((triple3) -> (rule5 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is not cold.
False
2
inv-proof
[(((triple3) -> rule5))]
("Gary" "is" "cold" "-")
((triple3) -> (rule5 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is red.
True
4
proof
[(((triple2 ((triple3) -> rule5)) -> rule3))]
("Gary" "is" "red" "+")
((triple2 ((triple3) -> (rule5 % int2))) -> (rule3 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is not red.
False
4
inv-proof
[(((triple2 ((triple3) -> rule5)) -> rule3))]
("Gary" "is" "red" "-")
((triple2 ((triple3) -> (rule5 % int2))) -> (rule3 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is young.
True
6
proof
[(((triple3 ((triple2 ((triple3) -> rule5)) -> rule3)) -> rule2))]
("Gary" "is" "young" "+")
((triple3 ((triple2 ((triple3) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
int3
Gary is green.
False
7
inv-proof
[(((((triple3) -> rule5) ((triple2 ((triple3) -> rule5)) -> rule3)) -> rule6))]
("Gary" "is" "green" "+")
((((triple3) -> (rule5 % int3)) ((triple2 ((triple3) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Gary is not green.
("Gary" "is" "green" "-")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
int3
@0: Gary is furry.[(triple2)] Gary is not blue.[(triple1)] Gary is rough.[(triple3)] @1: Gary is cold.[(((triple3) -> rule5))] @2: Gary is red.[(((triple2 ((triple3) -> rule5)) -> rule3))] @3: Gary is not green.[(((((triple3) -> rule5) ((triple2 ((triple3) -> rule5)) -> rule3)) -> rule6))] Gary is young.[(((triple3 ((triple2 ((triple3) -> rule5)) -> rule3)) -> rule2))]
Gary is furry.
("Gary" "is" "furry" "+")
triple2
Gary is not blue.
("Gary" "is" "blue" "-")
triple1
Gary is rough.
("Gary" "is" "rough" "+")
triple3
Gary is cold.
("Gary" "is" "cold" "+")
((triple3) -> (rule5 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
((triple2 ((triple3) -> (rule5 % int2))) -> (rule3 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is not green.
("Gary" "is" "green" "-")
((((triple3) -> (rule5 % int3)) ((triple2 ((triple3) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Gary is not green.
("Gary" "is" "green" "-")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
int3
Gary is young.
("Gary" "is" "young" "+")
((triple3 ((triple2 ((triple3) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
int3