Dave is blue. Dave is cold. Dave is furry. Dave is green. Dave is kind. Dave is round. Dave is white. Round things are cold. If something is white then it is kind. All blue, furry things are cold.
Dave is blue.
("Dave" "is" "blue" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is round.
("Dave" "is" "round" "+")
Dave is white.
("Dave" "is" "white" "+")
Round things are cold.
((("something" "is" "round" "+")) -> ("something" "is" "cold" "+"))
If something is white then it is kind.
((("something" "is" "white" "+")) -> ("something" "is" "kind" "+"))
All blue, furry things are cold.
((("something" "is" "blue" "+") ("something" "is" "furry" "+")) -> ("something" "is" "cold" "+"))
Dave is green.
True
1
proof
[(triple4)]
("Dave" "is" "green" "+")
triple4
Dave is not green.
False
1
inv-proof
[(triple4)]
("Dave" "is" "green" "-")
triple4
@0: Dave is blue.[(triple1)] Dave is cold.[(triple2 OR ((triple6) -> rule1) OR ((triple1 triple3) -> rule3))] Dave is furry.[(triple3)] Dave is green.[(triple4)] Dave is kind.[(triple5 OR ((triple7) -> rule2))] Dave is round.[(triple6)] Dave is white.[(triple7)]
Dave is blue.
("Dave" "is" "blue" "+")
triple1
Dave is cold.
("Dave" "is" "cold" "+")
triple2
((triple6) -> (rule1 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
((triple1 triple3) -> (rule3 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
triple3
Dave is green.
("Dave" "is" "green" "+")
triple4
Dave is kind.
("Dave" "is" "kind" "+")
triple5
((triple7) -> (rule2 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
triple6
Dave is white.
("Dave" "is" "white" "+")
triple7