Gary is cold. Gary is furry. Gary is green. Gary is not nice. Gary is red. Gary is round. Gary is smart. If someone is green and not nice then they are round. Round, nice people are smart. All smart people are green.
Gary is cold.
("Gary" "is" "cold" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is not nice.
("Gary" "is" "nice" "-")
Gary is red.
("Gary" "is" "red" "+")
Gary is round.
("Gary" "is" "round" "+")
Gary is smart.
("Gary" "is" "smart" "+")
If someone is green and not nice then they are round.
((("someone" "is" "green" "+") ("someone" "is" "nice" "~")) -> ("someone" "is" "round" "+"))
Round, nice people are smart.
((("someone" "is" "round" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "smart" "+"))
All smart people are green.
((("someone" "is" "smart" "+")) -> ("someone" "is" "green" "+"))
Gary is round.
True
1
proof
[(triple6 OR ((triple3 triple4) -> rule1) OR ((((triple7) -> rule3) triple4) -> rule1))]
("Gary" "is" "round" "+")
triple6
((triple3 triple4) -> (rule1 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
((((triple7) -> (rule3 % int2)) triple4) -> (rule1 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is not smart.
False
1
inv-proof
[(triple7)]
("Gary" "is" "smart" "-")
triple7
@0: Gary is cold.[(triple1)] Gary is furry.[(triple2)] Gary is green.[(triple3 OR ((triple7) -> rule3))] Gary is not nice.[(triple4)] Gary is red.[(triple5)] Gary is round.[(triple6 OR ((triple3 triple4) -> rule1) OR ((((triple7) -> rule3) triple4) -> rule1))] Gary is smart.[(triple7)]
Gary is cold.
("Gary" "is" "cold" "+")
triple1
Gary is furry.
("Gary" "is" "furry" "+")
triple2
Gary is green.
("Gary" "is" "green" "+")
triple3
((triple7) -> (rule3 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is not nice.
("Gary" "is" "nice" "-")
triple4
Gary is red.
("Gary" "is" "red" "+")
triple5
Gary is round.
("Gary" "is" "round" "+")
triple6
((triple3 triple4) -> (rule1 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
((((triple7) -> (rule3 % int2)) triple4) -> (rule1 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
triple7