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