Harry is furry. Harry is green. Harry is nice. Harry is quiet. Harry is rough. Harry is white. Harry is young. If something is rough and white then it is nice. All young, white things are green.
Harry is furry.
("Harry" "is" "furry" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is white.
("Harry" "is" "white" "+")
Harry is young.
("Harry" "is" "young" "+")
If something is rough and white then it is nice.
((("something" "is" "rough" "+") ("something" "is" "white" "+")) -> ("something" "is" "nice" "+"))
All young, white things are green.
((("something" "is" "young" "+") ("something" "is" "white" "+")) -> ("something" "is" "green" "+"))
Harry is white.
True
1
proof
[(triple6)]
("Harry" "is" "white" "+")
triple6
Harry is not green.
False
1
inv-proof
[(triple2 OR ((triple7 triple6) -> rule2))]
("Harry" "is" "green" "-")
triple2
((triple7 triple6) -> (rule2 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
@0: Harry is furry.[(triple1)] Harry is green.[(triple2 OR ((triple7 triple6) -> rule2))] Harry is nice.[(triple3 OR ((triple5 triple6) -> rule1))] Harry is quiet.[(triple4)] Harry is rough.[(triple5)] Harry is white.[(triple6)] Harry is young.[(triple7)]
Harry is furry.
("Harry" "is" "furry" "+")
triple1
Harry is green.
("Harry" "is" "green" "+")
triple2
((triple7 triple6) -> (rule2 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
triple3
((triple5 triple6) -> (rule1 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
triple4
Harry is rough.
("Harry" "is" "rough" "+")
triple5
Harry is white.
("Harry" "is" "white" "+")
triple6
Harry is young.
("Harry" "is" "young" "+")
triple7