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