Harry is blue. Harry is cold. Harry is green. Harry is kind. Harry is nice. Harry is rough. Harry is not young. If something is kind and not young then it is cold.
Harry is blue.
("Harry" "is" "blue" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is not young.
("Harry" "is" "young" "-")
If something is kind and not young then it is cold.
((("something" "is" "kind" "+") ("something" "is" "young" "~")) -> ("something" "is" "cold" "+"))
Harry is cold.
True
1
proof
[(triple2 OR ((triple4 triple7) -> rule1))]
("Harry" "is" "cold" "+")
triple2
((triple4 triple7) -> (rule1 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is not rough.
False
1
inv-proof
[(triple6)]
("Harry" "is" "rough" "-")
triple6
@0: Harry is blue.[(triple1)] Harry is cold.[(triple2 OR ((triple4 triple7) -> rule1))] Harry is green.[(triple3)] Harry is kind.[(triple4)] Harry is nice.[(triple5)] Harry is not young.[(triple7)] Harry is rough.[(triple6)]
Harry is blue.
("Harry" "is" "blue" "+")
triple1
Harry is cold.
("Harry" "is" "cold" "+")
triple2
((triple4 triple7) -> (rule1 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
triple3
Harry is kind.
("Harry" "is" "kind" "+")
triple4
Harry is nice.
("Harry" "is" "nice" "+")
triple5
Harry is not young.
("Harry" "is" "young" "-")
triple7
Harry is rough.
("Harry" "is" "rough" "+")
triple6