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