Bob is big. Bob is blue. Bob is cold. Bob is furry. Bob is nice. Bob is red. Bob is white. All nice things are blue. All big things are furry.
Bob is big.
("Bob" "is" "big" "+")
Bob is blue.
("Bob" "is" "blue" "+")
Bob is cold.
("Bob" "is" "cold" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is white.
("Bob" "is" "white" "+")
All nice things are blue.
((("something" "is" "nice" "+")) -> ("something" "is" "blue" "+"))
All big things are furry.
((("something" "is" "big" "+")) -> ("something" "is" "furry" "+"))
Bob is big.
True
1
proof
[(triple1)]
("Bob" "is" "big" "+")
triple1
Bob is not furry.
False
1
inv-proof
[(triple4 OR ((triple1) -> rule2))]
("Bob" "is" "furry" "-")
triple4
((triple1) -> (rule2 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
@0: Bob is big.[(triple1)] Bob is blue.[(triple2 OR ((triple5) -> rule1))] Bob is cold.[(triple3)] Bob is furry.[(triple4 OR ((triple1) -> rule2))] Bob is nice.[(triple5)] Bob is red.[(triple6)] Bob is white.[(triple7)]
Bob is big.
("Bob" "is" "big" "+")
triple1
Bob is blue.
("Bob" "is" "blue" "+")
triple2
((triple5) -> (rule1 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
triple3
Bob is furry.
("Bob" "is" "furry" "+")
triple4
((triple1) -> (rule2 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
triple5
Bob is red.
("Bob" "is" "red" "+")
triple6
Bob is white.
("Bob" "is" "white" "+")
triple7