Bob is big. Bob is furry. Bob is green. Bob is nice. Bob is round. Bob is smart. Bob is white. If someone is smart then they are nice. All green, smart people are furry. All green, big people are nice.
Bob is big.
("Bob" "is" "big" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is round.
("Bob" "is" "round" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Bob is white.
("Bob" "is" "white" "+")
If someone is smart then they are nice.
((("someone" "is" "smart" "+")) -> ("someone" "is" "nice" "+"))
All green, smart people are furry.
((("someone" "is" "green" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "furry" "+"))
All green, big people are nice.
((("someone" "is" "green" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "nice" "+"))
Bob is nice.
True
1
proof
[(triple4 OR ((triple6) -> rule1) OR ((triple3 triple1) -> rule3))]
("Bob" "is" "nice" "+")
triple4
((triple6) -> (rule1 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
((triple3 triple1) -> (rule3 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is not furry.
False
1
inv-proof
[(triple2 OR ((triple3 triple6) -> rule2))]
("Bob" "is" "furry" "-")
triple2
((triple3 triple6) -> (rule2 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
@0: Bob is big.[(triple1)] Bob is furry.[(triple2 OR ((triple3 triple6) -> rule2))] Bob is green.[(triple3)] Bob is nice.[(triple4 OR ((triple6) -> rule1) OR ((triple3 triple1) -> rule3))] Bob is round.[(triple5)] Bob is smart.[(triple6)] Bob is white.[(triple7)]
Bob is big.
("Bob" "is" "big" "+")
triple1
Bob is furry.
("Bob" "is" "furry" "+")
triple2
((triple3 triple6) -> (rule2 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
triple3
Bob is nice.
("Bob" "is" "nice" "+")
triple4
((triple6) -> (rule1 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
((triple3 triple1) -> (rule3 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
triple5
Bob is smart.
("Bob" "is" "smart" "+")
triple6
Bob is white.
("Bob" "is" "white" "+")
triple7