Gary is kind. Gary is nice. Gary is round. Gary is smart. Gary is young. Harry is kind. Harry is nice. Harry is quiet. Harry is rough. Harry is round. Harry is smart. Harry is young. All nice people are smart. If Harry is rough and Harry is smart then Harry is quiet. Smart people are quiet.
Gary is kind.
("Gary" "is" "kind" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is round.
("Gary" "is" "round" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Gary is young.
("Gary" "is" "young" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is round.
("Harry" "is" "round" "+")
Harry is smart.
("Harry" "is" "smart" "+")
Harry is young.
("Harry" "is" "young" "+")
All nice people are smart.
((("someone" "is" "nice" "+")) -> ("someone" "is" "smart" "+"))
If Harry is rough and Harry is smart then Harry is quiet.
((("Harry" "is" "rough" "+") ("Harry" "is" "smart" "+")) -> ("Harry" "is" "quiet" "+"))
Smart people are quiet.
((("someone" "is" "smart" "+")) -> ("someone" "is" "quiet" "+"))
Harry is quiet.
True
1
proof
[(triple8 OR ((triple11) -> rule3) OR ((triple9 triple11) -> rule2) OR ((((triple7) -> rule1)) -> rule3) OR ((triple9 ((triple7) -> rule1)) -> rule2))]
("Harry" "is" "quiet" "+")
triple8
((triple11) -> (rule3 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
((triple9 triple11) -> (rule2 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
((((triple7) -> (rule1 % int2))) -> (rule3 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
((triple9 ((triple7) -> (rule1 % int2))) -> (rule2 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Gary is not kind.
False
1
inv-proof
[(triple1)]
("Gary" "is" "kind" "-")
triple1
@0: Gary is kind.[(triple1)] Gary is nice.[(triple2)] Gary is round.[(triple3)] Gary is smart.[(triple4 OR ((triple2) -> rule1))] Gary is young.[(triple5)] Harry is kind.[(triple6)] Harry is nice.[(triple7)] Harry is quiet.[(triple8 OR ((triple11) -> rule3) OR ((triple9 triple11) -> rule2) OR ((((triple7) -> rule1)) -> rule3) OR ((triple9 ((triple7) -> rule1)) -> rule2))] Harry is rough.[(triple9)] Harry is round.[(triple10)] Harry is smart.[(triple11 OR ((triple7) -> rule1))] Harry is young.[(triple12)] @1: Gary is quiet.[(((triple4) -> rule3) OR ((((triple2) -> rule1)) -> rule3))]
Gary is kind.
("Gary" "is" "kind" "+")
triple1
Gary is nice.
("Gary" "is" "nice" "+")
triple2
Gary is round.
("Gary" "is" "round" "+")
triple3
Gary is smart.
("Gary" "is" "smart" "+")
triple4
((triple2) -> (rule1 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
triple5
Harry is kind.
("Harry" "is" "kind" "+")
triple6
Harry is nice.
("Harry" "is" "nice" "+")
triple7
Harry is quiet.
("Harry" "is" "quiet" "+")
triple8
((triple11) -> (rule3 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
((triple9 triple11) -> (rule2 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
((((triple7) -> (rule1 % int2))) -> (rule3 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
((triple9 ((triple7) -> (rule1 % int2))) -> (rule2 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
triple9
Harry is round.
("Harry" "is" "round" "+")
triple10
Harry is smart.
("Harry" "is" "smart" "+")
triple11
((triple7) -> (rule1 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
triple12
Gary is quiet.
("Gary" "is" "quiet" "+")
((triple4) -> (rule3 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
((((triple2) -> (rule1 % int2))) -> (rule3 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2