Bob is furry. Bob is green. Bob is kind. Bob is nice. Bob is round. Bob is smart. Bob is young. Gary is furry. Gary is green. Gary is kind. Gary is nice. Gary is round. Gary is smart. Gary is young. If Gary is furry then Gary is smart. If something is nice then it is round. All furry, green things are kind.
Bob is furry.
("Bob" "is" "furry" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is round.
("Bob" "is" "round" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Bob is young.
("Bob" "is" "young" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is round.
("Gary" "is" "round" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Gary is young.
("Gary" "is" "young" "+")
If Gary is furry then Gary is smart.
((("Gary" "is" "furry" "+")) -> ("Gary" "is" "smart" "+"))
If something is nice then it is round.
((("something" "is" "nice" "+")) -> ("something" "is" "round" "+"))
All furry, green things are kind.
((("something" "is" "furry" "+") ("something" "is" "green" "+")) -> ("something" "is" "kind" "+"))
Bob is green.
True
1
proof
[(triple2)]
("Bob" "is" "green" "+")
triple2
Gary is not nice.
False
1
inv-proof
[(triple11)]
("Gary" "is" "nice" "-")
triple11
@0: Bob is furry.[(triple1)] Bob is green.[(triple2)] Bob is kind.[(triple3 OR ((triple1 triple2) -> rule3))] Bob is nice.[(triple4)] Bob is round.[(triple5 OR ((triple4) -> rule2))] Bob is smart.[(triple6)] Bob is young.[(triple7)] Gary is furry.[(triple8)] Gary is green.[(triple9)] Gary is kind.[(triple10 OR ((triple8 triple9) -> rule3))] Gary is nice.[(triple11)] Gary is round.[(triple12 OR ((triple11) -> rule2))] Gary is smart.[(triple13 OR ((triple8) -> rule1))] Gary is young.[(triple14)]
Bob is furry.
("Bob" "is" "furry" "+")
triple1
Bob is green.
("Bob" "is" "green" "+")
triple2
Bob is kind.
("Bob" "is" "kind" "+")
triple3
((triple1 triple2) -> (rule3 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
triple4
Bob is round.
("Bob" "is" "round" "+")
triple5
((triple4) -> (rule2 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
triple6
Bob is young.
("Bob" "is" "young" "+")
triple7
Gary is furry.
("Gary" "is" "furry" "+")
triple8
Gary is green.
("Gary" "is" "green" "+")
triple9
Gary is kind.
("Gary" "is" "kind" "+")
triple10
((triple8 triple9) -> (rule3 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
triple11
Gary is round.
("Gary" "is" "round" "+")
triple12
((triple11) -> (rule2 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
triple13
((triple8) -> (rule1 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
triple14