Bob is blue. Bob is furry. Bob is nice. Bob is red. Bob is rough. Bob is smart. Bob is white. If Bob is blue then Bob is nice.
Bob is blue.
("Bob" "is" "blue" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is nice.
("Bob" "is" "nice" "+")
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 blue then Bob is nice.
((("Bob" "is" "blue" "+")) -> ("Bob" "is" "nice" "+"))
Bob is white.
True
1
proof
[(triple7)]
("Bob" "is" "white" "+")
triple7
Bob is not red.
False
1
inv-proof
[(triple4)]
("Bob" "is" "red" "-")
triple4
@0: Bob is blue.[(triple1)] Bob is furry.[(triple2)] Bob is nice.[(triple3 OR ((triple1) -> rule1))] Bob is red.[(triple4)] Bob is rough.[(triple5)] Bob is smart.[(triple6)] Bob is white.[(triple7)]
Bob is blue.
("Bob" "is" "blue" "+")
triple1
Bob is furry.
("Bob" "is" "furry" "+")
triple2
Bob is nice.
("Bob" "is" "nice" "+")
triple3
((triple1) -> (rule1 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
triple4
Bob is rough.
("Bob" "is" "rough" "+")
triple5
Bob is smart.
("Bob" "is" "smart" "+")
triple6
Bob is white.
("Bob" "is" "white" "+")
triple7