Gary is furry. Gary is nice. Gary is round. Round, nice people are blue. If someone is blue and kind then they are quiet. If someone is smart then they are furry. All smart people are nice. If someone is furry and blue then they are smart. All blue, smart people are quiet.
Gary is furry.
("Gary" "is" "furry" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is round.
("Gary" "is" "round" "+")
Round, nice people are blue.
((("someone" "is" "round" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "blue" "+"))
If someone is blue and kind then they are quiet.
((("someone" "is" "blue" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "quiet" "+"))
If someone is smart then they are furry.
((("someone" "is" "smart" "+")) -> ("someone" "is" "furry" "+"))
All smart people are nice.
((("someone" "is" "smart" "+")) -> ("someone" "is" "nice" "+"))
If someone is furry and blue then they are smart.
((("someone" "is" "furry" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "smart" "+"))
All blue, smart people are quiet.
((("someone" "is" "blue" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "quiet" "+"))
Gary is nice.
True
1
proof
[(triple2)]
("Gary" "is" "nice" "+")
triple2
Gary is not round.
False
1
inv-proof
[(triple3)]
("Gary" "is" "round" "-")
triple3
Gary is blue.
True
3
proof
[(((triple3 triple2) -> rule1))]
("Gary" "is" "blue" "+")
((triple3 triple2) -> (rule1 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is not blue.
False
3
inv-proof
[(((triple3 triple2) -> rule1))]
("Gary" "is" "blue" "-")
((triple3 triple2) -> (rule1 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is smart.
True
5
proof
[(((triple1 ((triple3 triple2) -> rule1)) -> rule5))]
("Gary" "is" "smart" "+")
((triple1 ((triple3 triple2) -> (rule1 % int2))) -> (rule5 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is not smart.
False
5
inv-proof
[(((triple1 ((triple3 triple2) -> rule1)) -> rule5))]
("Gary" "is" "smart" "-")
((triple1 ((triple3 triple2) -> (rule1 % int2))) -> (rule5 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is quiet.
True
9
proof
[(((((triple3 triple2) -> rule1) ((triple1 ((triple3 triple2) -> rule1)) -> rule5)) -> rule6))]
("Gary" "is" "quiet" "+")
((((triple3 triple2) -> (rule1 % int3)) ((triple1 ((triple3 triple2) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
int3
Gary is not quiet.
False
9
inv-proof
[(((((triple3 triple2) -> rule1) ((triple1 ((triple3 triple2) -> rule1)) -> rule5)) -> rule6))]
("Gary" "is" "quiet" "-")
((((triple3 triple2) -> (rule1 % int3)) ((triple1 ((triple3 triple2) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
int3
@0: Gary is furry.[(triple1)] Gary is nice.[(triple2)] Gary is round.[(triple3)] @1: Gary is blue.[(((triple3 triple2) -> rule1))] @2: Gary is smart.[(((triple1 ((triple3 triple2) -> rule1)) -> rule5))] @3: Gary is quiet.[(((((triple3 triple2) -> rule1) ((triple1 ((triple3 triple2) -> rule1)) -> rule5)) -> rule6))]
Gary is furry.
("Gary" "is" "furry" "+")
triple1
Gary is nice.
("Gary" "is" "nice" "+")
triple2
Gary is round.
("Gary" "is" "round" "+")
triple3
Gary is blue.
("Gary" "is" "blue" "+")
((triple3 triple2) -> (rule1 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
((triple1 ((triple3 triple2) -> (rule1 % int2))) -> (rule5 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
((((triple3 triple2) -> (rule1 % int3)) ((triple1 ((triple3 triple2) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
int3