Bob is big. Bob is blue. Bob is furry. Bob is kind. Bob is quiet. Bob is red. Bob is young. Quiet, red people are furry. If Bob is big and Bob is not young then Bob is red.
Bob is big.
("Bob" "is" "big" "+")
Bob is blue.
("Bob" "is" "blue" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is young.
("Bob" "is" "young" "+")
Quiet, red people are furry.
((("someone" "is" "quiet" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "furry" "+"))
If Bob is big and Bob is not young then Bob is red.
((("Bob" "is" "big" "+") ("Bob" "is" "young" "~")) -> ("Bob" "is" "red" "+"))
Bob is big.
True
1
proof
[(triple1)]
("Bob" "is" "big" "+")
triple1
Bob is not red.
False
1
inv-proof
[(triple6)]
("Bob" "is" "red" "-")
triple6
@0: Bob is big.[(triple1)] Bob is blue.[(triple2)] Bob is furry.[(triple3 OR ((triple5 triple6) -> rule1))] Bob is kind.[(triple4)] Bob is quiet.[(triple5)] Bob is red.[(triple6)] Bob is young.[(triple7)]
Bob is big.
("Bob" "is" "big" "+")
triple1
Bob is blue.
("Bob" "is" "blue" "+")
triple2
Bob is furry.
("Bob" "is" "furry" "+")
triple3
((triple5 triple6) -> (rule1 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
triple4
Bob is quiet.
("Bob" "is" "quiet" "+")
triple5
Bob is red.
("Bob" "is" "red" "+")
triple6
Bob is young.
("Bob" "is" "young" "+")
triple7