Gary is blue. Gary is cold. Gary is kind. Gary is nice. Gary is quiet. Gary is smart. Gary is young. Harry is not blue. Harry is not cold. Harry is kind. Harry is nice. Harry is quiet. Harry is not smart. Harry is young. Quiet, young things are nice.
Gary is blue.
("Gary" "is" "blue" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Gary is young.
("Gary" "is" "young" "+")
Harry is not blue.
("Harry" "is" "blue" "-")
Harry is not cold.
("Harry" "is" "cold" "-")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is not smart.
("Harry" "is" "smart" "-")
Harry is young.
("Harry" "is" "young" "+")
Quiet, young things are nice.
((("something" "is" "quiet" "+") ("something" "is" "young" "+")) -> ("something" "is" "nice" "+"))
Harry is not blue.
True
1
proof
[(triple8)]
("Harry" "is" "blue" "-")
triple8
Gary is not kind.
False
1
inv-proof
[(triple3)]
("Gary" "is" "kind" "-")
triple3
@0: Gary is blue.[(triple1)] Gary is cold.[(triple2)] Gary is kind.[(triple3)] Gary is nice.[(triple4 OR ((triple5 triple7) -> rule1))] Gary is quiet.[(triple5)] Gary is smart.[(triple6)] Gary is young.[(triple7)] Harry is kind.[(triple10)] Harry is nice.[(triple11 OR ((triple12 triple14) -> rule1))] Harry is not blue.[(triple8)] Harry is not cold.[(triple9)] Harry is not smart.[(triple13)] Harry is quiet.[(triple12)] Harry is young.[(triple14)]
Gary is blue.
("Gary" "is" "blue" "+")
triple1
Gary is cold.
("Gary" "is" "cold" "+")
triple2
Gary is kind.
("Gary" "is" "kind" "+")
triple3
Gary is nice.
("Gary" "is" "nice" "+")
triple4
((triple5 triple7) -> (rule1 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
triple5
Gary is smart.
("Gary" "is" "smart" "+")
triple6
Gary is young.
("Gary" "is" "young" "+")
triple7
Harry is kind.
("Harry" "is" "kind" "+")
triple10
Harry is nice.
("Harry" "is" "nice" "+")
triple11
((triple12 triple14) -> (rule1 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is not blue.
("Harry" "is" "blue" "-")
triple8
Harry is not cold.
("Harry" "is" "cold" "-")
triple9
Harry is not smart.
("Harry" "is" "smart" "-")
triple13
Harry is quiet.
("Harry" "is" "quiet" "+")
triple12
Harry is young.
("Harry" "is" "young" "+")
triple14