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