Dave is blue. Dave is cold. Dave is not furry. Dave is green. Dave is not nice. Dave is smart. Dave is white. Harry is cold. Harry is furry. Harry is green. Harry is nice. Harry is smart. If something is blue and nice then it is green. Nice things are blue.
Dave is blue.
("Dave" "is" "blue" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is not furry.
("Dave" "is" "furry" "-")
Dave is green.
("Dave" "is" "green" "+")
Dave is not nice.
("Dave" "is" "nice" "-")
Dave is smart.
("Dave" "is" "smart" "+")
Dave is white.
("Dave" "is" "white" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is smart.
("Harry" "is" "smart" "+")
If something is blue and nice then it is green.
((("something" "is" "blue" "+") ("something" "is" "nice" "+")) -> ("something" "is" "green" "+"))
Nice things are blue.
((("something" "is" "nice" "+")) -> ("something" "is" "blue" "+"))
Dave is smart.
True
1
proof
[(triple6)]
("Dave" "is" "smart" "+")
triple6
Dave is not blue.
False
1
inv-proof
[(triple1)]
("Dave" "is" "blue" "-")
triple1
@0: Dave is blue.[(triple1)] Dave is cold.[(triple2)] Dave is green.[(triple4)] Dave is not furry.[(triple3)] Dave is not nice.[(triple5)] Dave is smart.[(triple6)] Dave is white.[(triple7)] Harry is cold.[(triple8)] Harry is furry.[(triple9)] Harry is green.[(triple10 OR ((((triple11) -> rule2) triple11) -> rule1))] Harry is nice.[(triple11)] Harry is smart.[(triple12)] @1: Harry is blue.[(((triple11) -> rule2))]
Dave is blue.
("Dave" "is" "blue" "+")
triple1
Dave is cold.
("Dave" "is" "cold" "+")
triple2
Dave is green.
("Dave" "is" "green" "+")
triple4
Dave is not furry.
("Dave" "is" "furry" "-")
triple3
Dave is not nice.
("Dave" "is" "nice" "-")
triple5
Dave is smart.
("Dave" "is" "smart" "+")
triple6
Dave is white.
("Dave" "is" "white" "+")
triple7
Harry is cold.
("Harry" "is" "cold" "+")
triple8
Harry is furry.
("Harry" "is" "furry" "+")
triple9
Harry is green.
("Harry" "is" "green" "+")
triple10
((((triple11) -> (rule2 % int2)) triple11) -> (rule1 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
triple11
Harry is smart.
("Harry" "is" "smart" "+")
triple12
Harry is blue.
("Harry" "is" "blue" "+")
((triple11) -> (rule2 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1