Gary is big. Gary is blue. Gary is not cold. Gary is green. Gary is kind. Gary is nice. Gary is not white. Harry is big. Harry is not blue. Harry is cold. Harry is kind. Harry is white. If someone is kind and white then they are not nice.
Gary is big.
("Gary" "is" "big" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is not cold.
("Gary" "is" "cold" "-")
Gary is green.
("Gary" "is" "green" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is not white.
("Gary" "is" "white" "-")
Harry is big.
("Harry" "is" "big" "+")
Harry is not blue.
("Harry" "is" "blue" "-")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is white.
("Harry" "is" "white" "+")
If someone is kind and white then they are not nice.
((("someone" "is" "kind" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "nice" "-"))
Harry is big.
True
1
proof
[(triple8)]
("Harry" "is" "big" "+")
triple8
Gary is cold.
False
1
inv-proof
[(triple3)]
("Gary" "is" "cold" "+")
triple3
Harry is not nice.
True
3
proof
[(((triple11 triple12) -> rule1))]
("Harry" "is" "nice" "-")
((triple11 triple12) -> (rule1 % int1))
Harry is not nice.
("Harry" "is" "nice" "-")
int1
Harry is nice.
False
3
inv-proof
[(((triple11 triple12) -> rule1))]
("Harry" "is" "nice" "+")
((triple11 triple12) -> (rule1 % int1))
Harry is not nice.
("Harry" "is" "nice" "-")
int1
@0: Gary is big.[(triple1)] Gary is blue.[(triple2)] Gary is green.[(triple4)] Gary is kind.[(triple5)] Gary is nice.[(triple6)] Gary is not cold.[(triple3)] Gary is not white.[(triple7)] Harry is big.[(triple8)] Harry is cold.[(triple10)] Harry is kind.[(triple11)] Harry is not blue.[(triple9)] Harry is white.[(triple12)] @1: Harry is not nice.[(((triple11 triple12) -> rule1))]
Gary is big.
("Gary" "is" "big" "+")
triple1
Gary is blue.
("Gary" "is" "blue" "+")
triple2
Gary is green.
("Gary" "is" "green" "+")
triple4
Gary is kind.
("Gary" "is" "kind" "+")
triple5
Gary is nice.
("Gary" "is" "nice" "+")
triple6
Gary is not cold.
("Gary" "is" "cold" "-")
triple3
Gary is not white.
("Gary" "is" "white" "-")
triple7
Harry is big.
("Harry" "is" "big" "+")
triple8
Harry is cold.
("Harry" "is" "cold" "+")
triple10
Harry is kind.
("Harry" "is" "kind" "+")
triple11
Harry is not blue.
("Harry" "is" "blue" "-")
triple9
Harry is white.
("Harry" "is" "white" "+")
triple12
Harry is not nice.
("Harry" "is" "nice" "-")
((triple11 triple12) -> (rule1 % int1))
Harry is not nice.
("Harry" "is" "nice" "-")
int1