Bob is blue. Bob is cold. Bob is green. Bob is kind. Bob is quiet. Bob is red. Bob is smart. All red people are cold. If Bob is cold then Bob is quiet. Cold people are quiet.
Bob is blue.
("Bob" "is" "blue" "+")
Bob is cold.
("Bob" "is" "cold" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is smart.
("Bob" "is" "smart" "+")
All red people are cold.
((("someone" "is" "red" "+")) -> ("someone" "is" "cold" "+"))
If Bob is cold then Bob is quiet.
((("Bob" "is" "cold" "+")) -> ("Bob" "is" "quiet" "+"))
Cold people are quiet.
((("someone" "is" "cold" "+")) -> ("someone" "is" "quiet" "+"))
Bob is blue.
True
1
proof
[(triple1)]
("Bob" "is" "blue" "+")
triple1
Bob is not cold.
False
1
inv-proof
[(triple2 OR ((triple6) -> rule1))]
("Bob" "is" "cold" "-")
triple2
((triple6) -> (rule1 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
@0: Bob is blue.[(triple1)] Bob is cold.[(triple2 OR ((triple6) -> rule1))] Bob is green.[(triple3)] Bob is kind.[(triple4)] Bob is quiet.[(triple5 OR ((triple2) -> rule2) OR ((triple2) -> rule3) OR ((((triple6) -> rule1)) -> rule2) OR ((((triple6) -> rule1)) -> rule3))] Bob is red.[(triple6)] Bob is smart.[(triple7)]
Bob is blue.
("Bob" "is" "blue" "+")
triple1
Bob is cold.
("Bob" "is" "cold" "+")
triple2
((triple6) -> (rule1 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
triple3
Bob is kind.
("Bob" "is" "kind" "+")
triple4
Bob is quiet.
("Bob" "is" "quiet" "+")
triple5
((triple2) -> (rule2 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
((triple2) -> (rule3 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
((((triple6) -> (rule1 % int2))) -> (rule2 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
((((triple6) -> (rule1 % int2))) -> (rule3 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
triple6
Bob is smart.
("Bob" "is" "smart" "+")
triple7