Anne is big. Anne is furry. Anne is nice. Anne is quiet. Anne is white. Gary is big. Gary is furry. Gary is nice. Gary is quiet. Gary is round. Gary is smart. Gary is white. If someone is round then they are quiet. If someone is quiet and big then they are smart.
Anne is big.
("Anne" "is" "big" "+")
Anne is furry.
("Anne" "is" "furry" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is white.
("Anne" "is" "white" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is round.
("Gary" "is" "round" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Gary is white.
("Gary" "is" "white" "+")
If someone is round then they are quiet.
((("someone" "is" "round" "+")) -> ("someone" "is" "quiet" "+"))
If someone is quiet and big then they are smart.
((("someone" "is" "quiet" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "smart" "+"))
Gary is furry.
True
1
proof
[(triple7)]
("Gary" "is" "furry" "+")
triple7
Anne is not big.
False
1
inv-proof
[(triple1)]
("Anne" "is" "big" "-")
triple1
Anne is smart.
True
3
proof
[(((triple4 triple1) -> rule2))]
("Anne" "is" "smart" "+")
((triple4 triple1) -> (rule2 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is not smart.
False
3
inv-proof
[(((triple4 triple1) -> rule2))]
("Anne" "is" "smart" "-")
((triple4 triple1) -> (rule2 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
@0: Anne is big.[(triple1)] Anne is furry.[(triple2)] Anne is nice.[(triple3)] Anne is quiet.[(triple4)] Anne is white.[(triple5)] Gary is big.[(triple6)] Gary is furry.[(triple7)] Gary is nice.[(triple8)] Gary is quiet.[(triple9 OR ((triple10) -> rule1))] Gary is round.[(triple10)] Gary is smart.[(triple11 OR ((triple9 triple6) -> rule2) OR ((((triple10) -> rule1) triple6) -> rule2))] Gary is white.[(triple12)] @1: Anne is smart.[(((triple4 triple1) -> rule2))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is furry.
("Anne" "is" "furry" "+")
triple2
Anne is nice.
("Anne" "is" "nice" "+")
triple3
Anne is quiet.
("Anne" "is" "quiet" "+")
triple4
Anne is white.
("Anne" "is" "white" "+")
triple5
Gary is big.
("Gary" "is" "big" "+")
triple6
Gary is furry.
("Gary" "is" "furry" "+")
triple7
Gary is nice.
("Gary" "is" "nice" "+")
triple8
Gary is quiet.
("Gary" "is" "quiet" "+")
triple9
((triple10) -> (rule1 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
triple10
Gary is smart.
("Gary" "is" "smart" "+")
triple11
((triple9 triple6) -> (rule2 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
((((triple10) -> (rule1 % int2)) triple6) -> (rule2 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
triple12
Anne is smart.
("Anne" "is" "smart" "+")
((triple4 triple1) -> (rule2 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1