Harry is blue. Harry is furry. Harry is kind. Harry is quiet. Harry is red. Harry is smart. Harry is young. Furry things are blue.
Harry is blue.
("Harry" "is" "blue" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is smart.
("Harry" "is" "smart" "+")
Harry is young.
("Harry" "is" "young" "+")
Furry things are blue.
((("something" "is" "furry" "+")) -> ("something" "is" "blue" "+"))
Harry is blue.
True
1
proof
[(triple1 OR ((triple2) -> rule1))]
("Harry" "is" "blue" "+")
triple1
((triple2) -> (rule1 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is not furry.
False
1
inv-proof
[(triple2)]
("Harry" "is" "furry" "-")
triple2
@0: Harry is blue.[(triple1 OR ((triple2) -> rule1))] Harry is furry.[(triple2)] Harry is kind.[(triple3)] Harry is quiet.[(triple4)] Harry is red.[(triple5)] Harry is smart.[(triple6)] Harry is young.[(triple7)]
Harry is blue.
("Harry" "is" "blue" "+")
triple1
((triple2) -> (rule1 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
triple2
Harry is kind.
("Harry" "is" "kind" "+")
triple3
Harry is quiet.
("Harry" "is" "quiet" "+")
triple4
Harry is red.
("Harry" "is" "red" "+")
triple5
Harry is smart.
("Harry" "is" "smart" "+")
triple6
Harry is young.
("Harry" "is" "young" "+")
triple7