Gary is blue. Gary is green. Gary is rough. Rough, furry people are green. Rough, green people are cold. All cold people are young. If someone is green and blue then they are furry. All green, blue people are young. Furry people are blue. If Gary is green and Gary is blue then Gary is cold. If someone is rough then they are quiet.
Gary is blue.
("Gary" "is" "blue" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Rough, furry people are green.
((("someone" "is" "rough" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "green" "+"))
Rough, green people are cold.
((("someone" "is" "rough" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "cold" "+"))
All cold people are young.
((("someone" "is" "cold" "+")) -> ("someone" "is" "young" "+"))
If someone is green and blue then they are furry.
((("someone" "is" "green" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "furry" "+"))
All green, blue people are young.
((("someone" "is" "green" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "young" "+"))
Furry people are blue.
((("someone" "is" "furry" "+")) -> ("someone" "is" "blue" "+"))
If Gary is green and Gary is blue then Gary is cold.
((("Gary" "is" "green" "+") ("Gary" "is" "blue" "+")) -> ("Gary" "is" "cold" "+"))
If someone is rough then they are quiet.
((("someone" "is" "rough" "+")) -> ("someone" "is" "quiet" "+"))
Gary is blue.
True
1
proof
[(triple1)]
("Gary" "is" "blue" "+")
triple1
Gary is not rough.
False
1
inv-proof
[(triple3)]
("Gary" "is" "rough" "-")
triple3
@0: Gary is blue.[(triple1)] Gary is green.[(triple2)] Gary is rough.[(triple3)] @1: Gary is cold.[(((triple2 triple1) -> rule7) OR ((triple3 triple2) -> rule2))] Gary is furry.[(((triple2 triple1) -> rule4))] Gary is quiet.[(((triple3) -> rule8))] Gary is young.[(((triple2 triple1) -> rule5) OR ((((triple2 triple1) -> rule7)) -> rule3) OR ((((triple3 triple2) -> rule2)) -> rule3))]
Gary is blue.
("Gary" "is" "blue" "+")
triple1
Gary is green.
("Gary" "is" "green" "+")
triple2
Gary is rough.
("Gary" "is" "rough" "+")
triple3
Gary is cold.
("Gary" "is" "cold" "+")
((triple2 triple1) -> (rule7 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
((triple3 triple2) -> (rule2 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
((triple2 triple1) -> (rule4 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
((triple3) -> (rule8 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
((triple2 triple1) -> (rule5 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
((((triple2 triple1) -> (rule7 % int2))) -> (rule3 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
((((triple3 triple2) -> (rule2 % int2))) -> (rule3 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2