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