Gary is blue. Gary is furry. Gary is not rough. Blue things are green. If Gary is young and Gary is green then Gary is furry. Green things are white. Green, white things are cold. All cold, rough things are furry. If something is green and not white then it is furry.
Gary is blue.
("Gary" "is" "blue" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is not rough.
("Gary" "is" "rough" "-")
Blue things are green.
((("something" "is" "blue" "+")) -> ("something" "is" "green" "+"))
If Gary is young and Gary is green then Gary is furry.
((("Gary" "is" "young" "+") ("Gary" "is" "green" "+")) -> ("Gary" "is" "furry" "+"))
Green things are white.
((("something" "is" "green" "+")) -> ("something" "is" "white" "+"))
Green, white things are cold.
((("something" "is" "green" "+") ("something" "is" "white" "+")) -> ("something" "is" "cold" "+"))
All cold, rough things are furry.
((("something" "is" "cold" "+") ("something" "is" "rough" "+")) -> ("something" "is" "furry" "+"))
If something is green and not white then it is furry.
((("something" "is" "green" "+") ("something" "is" "white" "~")) -> ("something" "is" "furry" "+"))
Gary is furry.
True
1
proof
[(triple2)]
("Gary" "is" "furry" "+")
triple2
Gary is rough.
False
1
inv-proof
[(triple3)]
("Gary" "is" "rough" "+")
triple3
Gary is green.
True
2
proof
[(((triple1) -> rule1))]
("Gary" "is" "green" "+")
((triple1) -> (rule1 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is not green.
False
2
inv-proof
[(((triple1) -> rule1))]
("Gary" "is" "green" "-")
((triple1) -> (rule1 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is white.
True
3
proof
[(((((triple1) -> rule1)) -> rule3))]
("Gary" "is" "white" "+")
((((triple1) -> (rule1 % int2))) -> (rule3 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is not white.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule3))]
("Gary" "is" "white" "-")
((((triple1) -> (rule1 % int2))) -> (rule3 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is cold.
True
6
proof
[(((((triple1) -> rule1) ((((triple1) -> rule1)) -> rule3)) -> rule4))]
("Gary" "is" "cold" "+")
((((triple1) -> (rule1 % int3)) ((((triple1) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
int3
Gary is not cold.
False
6
inv-proof
[(((((triple1) -> rule1) ((((triple1) -> rule1)) -> rule3)) -> rule4))]
("Gary" "is" "cold" "-")
((((triple1) -> (rule1 % int3)) ((((triple1) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
int3
@0: Gary is blue.[(triple1)] Gary is furry.[(triple2)] Gary is not rough.[(triple3)] @1: Gary is green.[(((triple1) -> rule1))] @2: Gary is white.[(((((triple1) -> rule1)) -> rule3))] @3: Gary is cold.[(((((triple1) -> rule1) ((((triple1) -> rule1)) -> rule3)) -> rule4))]
Gary is blue.
("Gary" "is" "blue" "+")
triple1
Gary is furry.
("Gary" "is" "furry" "+")
triple2
Gary is not rough.
("Gary" "is" "rough" "-")
triple3
Gary is green.
("Gary" "is" "green" "+")
((triple1) -> (rule1 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
((((triple1) -> (rule1 % int2))) -> (rule3 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
((((triple1) -> (rule1 % int3)) ((((triple1) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
int3