Bob is big. Bob is green. Bob is kind. Bob is red. Bob is rough. Bob is smart. Bob is white. If Bob is white then Bob is smart.
Bob is big.
("Bob" "is" "big" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Bob is white.
("Bob" "is" "white" "+")
If Bob is white then Bob is smart.
((("Bob" "is" "white" "+")) -> ("Bob" "is" "smart" "+"))
Bob is smart.
True
1
proof
[(triple6 OR ((triple7) -> rule1))]
("Bob" "is" "smart" "+")
triple6
((triple7) -> (rule1 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is not big.
False
1
inv-proof
[(triple1)]
("Bob" "is" "big" "-")
triple1
@0: Bob is big.[(triple1)] Bob is green.[(triple2)] Bob is kind.[(triple3)] Bob is red.[(triple4)] Bob is rough.[(triple5)] Bob is smart.[(triple6 OR ((triple7) -> rule1))] Bob is white.[(triple7)]
Bob is big.
("Bob" "is" "big" "+")
triple1
Bob is green.
("Bob" "is" "green" "+")
triple2
Bob is kind.
("Bob" "is" "kind" "+")
triple3
Bob is red.
("Bob" "is" "red" "+")
triple4
Bob is rough.
("Bob" "is" "rough" "+")
triple5
Bob is smart.
("Bob" "is" "smart" "+")
triple6
((triple7) -> (rule1 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
triple7