Gary is big. Gary is nice. Gary is smart. All nice, kind people are rough. All nice people are quiet. If Gary is furry and Gary is smart then Gary is nice. Rough people are furry. Kind, furry people are quiet. If Gary is smart and Gary is quiet then Gary is rough. Kind, smart people are big. All kind, rough people are big.
Gary is big.
("Gary" "is" "big" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is smart.
("Gary" "is" "smart" "+")
All nice, kind people are rough.
((("someone" "is" "nice" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "rough" "+"))
All nice people are quiet.
((("someone" "is" "nice" "+")) -> ("someone" "is" "quiet" "+"))
If Gary is furry and Gary is smart then Gary is nice.
((("Gary" "is" "furry" "+") ("Gary" "is" "smart" "+")) -> ("Gary" "is" "nice" "+"))
Rough people are furry.
((("someone" "is" "rough" "+")) -> ("someone" "is" "furry" "+"))
Kind, furry people are quiet.
((("someone" "is" "kind" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "quiet" "+"))
If Gary is smart and Gary is quiet then Gary is rough.
((("Gary" "is" "smart" "+") ("Gary" "is" "quiet" "+")) -> ("Gary" "is" "rough" "+"))
Kind, smart people are big.
((("someone" "is" "kind" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "big" "+"))
All kind, rough people are big.
((("someone" "is" "kind" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "big" "+"))
Gary is smart.
True
1
proof
[(triple3)]
("Gary" "is" "smart" "+")
triple3
Gary is not smart.
False
1
inv-proof
[(triple3)]
("Gary" "is" "smart" "-")
triple3
Gary is quiet.
True
2
proof
[(((triple2) -> rule2))]
("Gary" "is" "quiet" "+")
((triple2) -> (rule2 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is not quiet.
False
2
inv-proof
[(((triple2) -> rule2))]
("Gary" "is" "quiet" "-")
((triple2) -> (rule2 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is rough.
True
4
proof
[(((triple3 ((triple2) -> rule2)) -> rule6))]
("Gary" "is" "rough" "+")
((triple3 ((triple2) -> (rule2 % int2))) -> (rule6 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is not rough.
False
4
inv-proof
[(((triple3 ((triple2) -> rule2)) -> rule6))]
("Gary" "is" "rough" "-")
((triple3 ((triple2) -> (rule2 % int2))) -> (rule6 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is furry.
True
5
proof
[(((((triple3 ((triple2) -> rule2)) -> rule6)) -> rule4))]
("Gary" "is" "furry" "+")
((((triple3 ((triple2) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3
Gary is not furry.
False
5
inv-proof
[(((((triple3 ((triple2) -> rule2)) -> rule6)) -> rule4))]
("Gary" "is" "furry" "-")
((((triple3 ((triple2) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3
@0: Gary is big.[(triple1)] Gary is nice.[(triple2)] Gary is smart.[(triple3)] @1: Gary is quiet.[(((triple2) -> rule2))] @2: Gary is rough.[(((triple3 ((triple2) -> rule2)) -> rule6))] @3: Gary is furry.[(((((triple3 ((triple2) -> rule2)) -> rule6)) -> rule4))]
Gary is big.
("Gary" "is" "big" "+")
triple1
Gary is nice.
("Gary" "is" "nice" "+")
triple2
Gary is smart.
("Gary" "is" "smart" "+")
triple3
Gary is quiet.
("Gary" "is" "quiet" "+")
((triple2) -> (rule2 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
((triple3 ((triple2) -> (rule2 % int2))) -> (rule6 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
((((triple3 ((triple2) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3