Bob is not blue. Bob is not cold. Bob is furry. Bob is green. Bob is kind. Bob is white. Bob is young. Dave is not blue. Dave is furry. Dave is green. Dave is kind. Dave is young. If Dave is green and Dave is not furry then Dave is not kind. If something is young and not furry then it is kind. All blue things are not kind. If something is blue and furry then it is cold. All young things are not cold. All kind things are not blue.
Bob is not blue.
("Bob" "is" "blue" "-")
Bob is not cold.
("Bob" "is" "cold" "-")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is white.
("Bob" "is" "white" "+")
Bob is young.
("Bob" "is" "young" "+")
Dave is not blue.
("Dave" "is" "blue" "-")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is young.
("Dave" "is" "young" "+")
If Dave is green and Dave is not furry then Dave is not kind.
((("Dave" "is" "green" "+") ("Dave" "is" "furry" "~")) -> ("Dave" "is" "kind" "-"))
If something is young and not furry then it is kind.
((("something" "is" "young" "+") ("something" "is" "furry" "~")) -> ("something" "is" "kind" "+"))
All blue things are not kind.
((("something" "is" "blue" "+")) -> ("something" "is" "kind" "-"))
If something is blue and furry then it is cold.
((("something" "is" "blue" "+") ("something" "is" "furry" "+")) -> ("something" "is" "cold" "+"))
All young things are not cold.
((("something" "is" "young" "+")) -> ("something" "is" "cold" "-"))
All kind things are not blue.
((("something" "is" "kind" "+")) -> ("something" "is" "blue" "-"))
Dave is kind.
True
1
proof
[(triple11)]
("Dave" "is" "kind" "+")
triple11
Bob is cold.
False
1
inv-proof
[(triple2 OR ((triple7) -> rule5))]
("Bob" "is" "cold" "+")
triple2
((triple7) -> (rule5 % int1))
Bob is not cold.
("Bob" "is" "cold" "-")
int1
@0: Bob is furry.[(triple3)] Bob is green.[(triple4)] Bob is kind.[(triple5)] Bob is not blue.[(triple1 OR ((triple5) -> rule6))] Bob is not cold.[(triple2 OR ((triple7) -> rule5))] Bob is white.[(triple6)] Bob is young.[(triple7)] Dave is furry.[(triple9)] Dave is green.[(triple10)] Dave is kind.[(triple11)] Dave is not blue.[(triple8 OR ((triple11) -> rule6))] Dave is young.[(triple12)] @1: Dave is not cold.[(((triple12) -> rule5))]
Bob is furry.
("Bob" "is" "furry" "+")
triple3
Bob is green.
("Bob" "is" "green" "+")
triple4
Bob is kind.
("Bob" "is" "kind" "+")
triple5
Bob is not blue.
("Bob" "is" "blue" "-")
triple1
((triple5) -> (rule6 % int1))
Bob is not blue.
("Bob" "is" "blue" "-")
int1
Bob is not cold.
("Bob" "is" "cold" "-")
triple2
((triple7) -> (rule5 % int1))
Bob is not cold.
("Bob" "is" "cold" "-")
int1
Bob is white.
("Bob" "is" "white" "+")
triple6
Bob is young.
("Bob" "is" "young" "+")
triple7
Dave is furry.
("Dave" "is" "furry" "+")
triple9
Dave is green.
("Dave" "is" "green" "+")
triple10
Dave is kind.
("Dave" "is" "kind" "+")
triple11
Dave is not blue.
("Dave" "is" "blue" "-")
triple8
((triple11) -> (rule6 % int1))
Dave is not blue.
("Dave" "is" "blue" "-")
int1
Dave is young.
("Dave" "is" "young" "+")
triple12
Dave is not cold.
("Dave" "is" "cold" "-")
((triple12) -> (rule5 % int1))
Dave is not cold.
("Dave" "is" "cold" "-")
int1