Bob is big. Bob is furry. Bob is green. Bob is red. Bob is rough. Bob is round. Bob is smart. All big, smart things are red. All smart, green things are red. All green, round things are furry.
Bob is big.
("Bob" "is" "big" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Bob is round.
("Bob" "is" "round" "+")
Bob is smart.
("Bob" "is" "smart" "+")
All big, smart things are red.
((("something" "is" "big" "+") ("something" "is" "smart" "+")) -> ("something" "is" "red" "+"))
All smart, green things are red.
((("something" "is" "smart" "+") ("something" "is" "green" "+")) -> ("something" "is" "red" "+"))
All green, round things are furry.
((("something" "is" "green" "+") ("something" "is" "round" "+")) -> ("something" "is" "furry" "+"))
Bob is furry.
True
1
proof
[(triple2 OR ((triple3 triple6) -> rule3))]
("Bob" "is" "furry" "+")
triple2
((triple3 triple6) -> (rule3 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is not green.
False
1
inv-proof
[(triple3)]
("Bob" "is" "green" "-")
triple3
@0: Bob is big.[(triple1)] Bob is furry.[(triple2 OR ((triple3 triple6) -> rule3))] Bob is green.[(triple3)] Bob is red.[(triple4 OR ((triple1 triple7) -> rule1) OR ((triple7 triple3) -> rule2))] Bob is rough.[(triple5)] Bob is round.[(triple6)] Bob is smart.[(triple7)]
Bob is big.
("Bob" "is" "big" "+")
triple1
Bob is furry.
("Bob" "is" "furry" "+")
triple2
((triple3 triple6) -> (rule3 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
triple3
Bob is red.
("Bob" "is" "red" "+")
triple4
((triple1 triple7) -> (rule1 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
((triple7 triple3) -> (rule2 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
triple5
Bob is round.
("Bob" "is" "round" "+")
triple6
Bob is smart.
("Bob" "is" "smart" "+")
triple7