Gary is furry. Gary is green. Gary is not rough. All big, furry people are kind. Furry, smart people are kind. All kind people are big. If Gary is kind and Gary is not green then Gary is furry. If someone is green and not rough then they are smart. Rough, kind people are smart.
Gary is furry.
("Gary" "is" "furry" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is not rough.
("Gary" "is" "rough" "-")
All big, furry people are kind.
((("someone" "is" "big" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "kind" "+"))
Furry, smart people are kind.
((("someone" "is" "furry" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "kind" "+"))
All kind people are big.
((("someone" "is" "kind" "+")) -> ("someone" "is" "big" "+"))
If Gary is kind and Gary is not green then Gary is furry.
((("Gary" "is" "kind" "+") ("Gary" "is" "green" "~")) -> ("Gary" "is" "furry" "+"))
If someone is green and not rough then they are smart.
((("someone" "is" "green" "+") ("someone" "is" "rough" "~")) -> ("someone" "is" "smart" "+"))
Rough, kind people are smart.
((("someone" "is" "rough" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "smart" "+"))
Gary is not rough.
True
1
proof
[(triple3)]
("Gary" "is" "rough" "-")
triple3
Gary is not furry.
False
1
inv-proof
[(triple1)]
("Gary" "is" "furry" "-")
triple1
Gary is smart.
True
3
proof
[(((triple2 triple3) -> rule5))]
("Gary" "is" "smart" "+")
((triple2 triple3) -> (rule5 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is not smart.
False
3
inv-proof
[(((triple2 triple3) -> rule5))]
("Gary" "is" "smart" "-")
((triple2 triple3) -> (rule5 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is kind.
True
5
proof
[(((triple1 ((triple2 triple3) -> rule5)) -> rule2))]
("Gary" "is" "kind" "+")
((triple1 ((triple2 triple3) -> (rule5 % int2))) -> (rule2 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is not kind.
False
5
inv-proof
[(((triple1 ((triple2 triple3) -> rule5)) -> rule2))]
("Gary" "is" "kind" "-")
((triple1 ((triple2 triple3) -> (rule5 % int2))) -> (rule2 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is big.
True
6
proof
[(((((triple1 ((triple2 triple3) -> rule5)) -> rule2)) -> rule3))]
("Gary" "is" "big" "+")
((((triple1 ((triple2 triple3) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3
Gary is not big.
False
6
inv-proof
[(((((triple1 ((triple2 triple3) -> rule5)) -> rule2)) -> rule3))]
("Gary" "is" "big" "-")
((((triple1 ((triple2 triple3) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3
@0: Gary is furry.[(triple1)] Gary is green.[(triple2)] Gary is not rough.[(triple3)] @1: Gary is smart.[(((triple2 triple3) -> rule5))] @2: Gary is kind.[(((triple1 ((triple2 triple3) -> rule5)) -> rule2))] @3: Gary is big.[(((((triple1 ((triple2 triple3) -> rule5)) -> rule2)) -> rule3))]
Gary is furry.
("Gary" "is" "furry" "+")
triple1
Gary is green.
("Gary" "is" "green" "+")
triple2
Gary is not rough.
("Gary" "is" "rough" "-")
triple3
Gary is smart.
("Gary" "is" "smart" "+")
((triple2 triple3) -> (rule5 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
((triple1 ((triple2 triple3) -> (rule5 % int2))) -> (rule2 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
((((triple1 ((triple2 triple3) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3