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