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