Anne is furry. Anne is nice. Anne is rough. Anne is round. Anne is smart. Gary is not furry. Gary is not nice. Gary is quiet. Gary is not red. Gary is rough. Gary is round. Gary is smart. If something is red and round then it is quiet. If something is rough then it is quiet. If Anne is red and Anne is not furry then Anne is not nice. If Gary is red then Gary is smart. If Gary is round and Gary is not rough then Gary is smart. If something is furry then it is smart.
Anne is furry.
("Anne" "is" "furry" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Anne is round.
("Anne" "is" "round" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Gary is not furry.
("Gary" "is" "furry" "-")
Gary is not nice.
("Gary" "is" "nice" "-")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is not red.
("Gary" "is" "red" "-")
Gary is rough.
("Gary" "is" "rough" "+")
Gary is round.
("Gary" "is" "round" "+")
Gary is smart.
("Gary" "is" "smart" "+")
If something is red and round then it is quiet.
((("something" "is" "red" "+") ("something" "is" "round" "+")) -> ("something" "is" "quiet" "+"))
If something is rough then it is quiet.
((("something" "is" "rough" "+")) -> ("something" "is" "quiet" "+"))
If Anne is red and Anne is not furry then Anne is not nice.
((("Anne" "is" "red" "+") ("Anne" "is" "furry" "~")) -> ("Anne" "is" "nice" "-"))
If Gary is red then Gary is smart.
((("Gary" "is" "red" "+")) -> ("Gary" "is" "smart" "+"))
If Gary is round and Gary is not rough then Gary is smart.
((("Gary" "is" "round" "+") ("Gary" "is" "rough" "~")) -> ("Gary" "is" "smart" "+"))
If something is furry then it is smart.
((("something" "is" "furry" "+")) -> ("something" "is" "smart" "+"))
Anne is round.
True
1
proof
[(triple4)]
("Anne" "is" "round" "+")
triple4
Anne is not nice.
False
1
inv-proof
[(triple2)]
("Anne" "is" "nice" "-")
triple2
Anne is quiet.
True
2
proof
[(((triple3) -> rule2))]
("Anne" "is" "quiet" "+")
((triple3) -> (rule2 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is not quiet.
False
2
inv-proof
[(((triple3) -> rule2))]
("Anne" "is" "quiet" "-")
((triple3) -> (rule2 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
@0: Anne is furry.[(triple1)] Anne is nice.[(triple2)] Anne is rough.[(triple3)] Anne is round.[(triple4)] Anne is smart.[(triple5 OR ((triple1) -> rule6))] Gary is not furry.[(triple6)] Gary is not nice.[(triple7)] Gary is not red.[(triple9)] Gary is quiet.[(triple8 OR ((triple10) -> rule2))] Gary is rough.[(triple10)] Gary is round.[(triple11)] Gary is smart.[(triple12)] @1: Anne is quiet.[(((triple3) -> rule2))]
Anne is furry.
("Anne" "is" "furry" "+")
triple1
Anne is nice.
("Anne" "is" "nice" "+")
triple2
Anne is rough.
("Anne" "is" "rough" "+")
triple3
Anne is round.
("Anne" "is" "round" "+")
triple4
Anne is smart.
("Anne" "is" "smart" "+")
triple5
((triple1) -> (rule6 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Gary is not furry.
("Gary" "is" "furry" "-")
triple6
Gary is not nice.
("Gary" "is" "nice" "-")
triple7
Gary is not red.
("Gary" "is" "red" "-")
triple9
Gary is quiet.
("Gary" "is" "quiet" "+")
triple8
((triple10) -> (rule2 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
triple10
Gary is round.
("Gary" "is" "round" "+")
triple11
Gary is smart.
("Gary" "is" "smart" "+")
triple12
Anne is quiet.
("Anne" "is" "quiet" "+")
((triple3) -> (rule2 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1