Gary is big. Gary is furry. Gary is kind. Gary is quiet. Gary is rough. Gary is smart. Gary is young. Harry is big. Harry is furry. Harry is kind. Harry is quiet. Harry is rough. Young people are furry. All quiet, big people are kind. If Gary is rough and Gary is quiet then Gary is young. All rough, big people are young. If Harry is big then Harry is furry. If someone is rough then they are kind. If Gary is big then Gary is young. If someone is smart and kind then they are furry.
Gary is big.
("Gary" "is" "big" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Gary is young.
("Gary" "is" "young" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Young people are furry.
((("someone" "is" "young" "+")) -> ("someone" "is" "furry" "+"))
All quiet, big people are kind.
((("someone" "is" "quiet" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "kind" "+"))
If Gary is rough and Gary is quiet then Gary is young.
((("Gary" "is" "rough" "+") ("Gary" "is" "quiet" "+")) -> ("Gary" "is" "young" "+"))
All rough, big people are young.
((("someone" "is" "rough" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "young" "+"))
If Harry is big then Harry is furry.
((("Harry" "is" "big" "+")) -> ("Harry" "is" "furry" "+"))
If someone is rough then they are kind.
((("someone" "is" "rough" "+")) -> ("someone" "is" "kind" "+"))
If Gary is big then Gary is young.
((("Gary" "is" "big" "+")) -> ("Gary" "is" "young" "+"))
If someone is smart and kind then they are furry.
((("someone" "is" "smart" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "furry" "+"))
Harry is furry.
True
1
proof
[(triple9 OR ((triple8) -> rule5) OR ((((triple12 triple8) -> rule4)) -> rule1))]
("Harry" "is" "furry" "+")
triple9
((triple8) -> (rule5 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
((((triple12 triple8) -> (rule4 % int2))) -> (rule1 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Gary is not quiet.
False
1
inv-proof
[(triple4)]
("Gary" "is" "quiet" "-")
triple4
Harry is young.
True
3
proof
[(((triple12 triple8) -> rule4))]
("Harry" "is" "young" "+")
((triple12 triple8) -> (rule4 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is not young.
False
3
inv-proof
[(((triple12 triple8) -> rule4))]
("Harry" "is" "young" "-")
((triple12 triple8) -> (rule4 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
@0: Gary is big.[(triple1)] Gary is furry.[(triple2 OR ((triple7) -> rule1) OR ((triple6 triple3) -> rule8) OR ((((triple1) -> rule7)) -> rule1) OR ((((triple5 triple1) -> rule4)) -> rule1) OR ((((triple5 triple4) -> rule3)) -> rule1) OR ((triple6 ((triple5) -> rule6)) -> rule8) OR ((triple6 ((triple4 triple1) -> rule2)) -> rule8))] Gary is kind.[(triple3 OR ((triple5) -> rule6) OR ((triple4 triple1) -> rule2))] Gary is quiet.[(triple4)] Gary is rough.[(triple5)] Gary is smart.[(triple6)] Gary is young.[(triple7 OR ((triple1) -> rule7) OR ((triple5 triple1) -> rule4) OR ((triple5 triple4) -> rule3))] Harry is big.[(triple8)] Harry is furry.[(triple9 OR ((triple8) -> rule5) OR ((((triple12 triple8) -> rule4)) -> rule1))] Harry is kind.[(triple10 OR ((triple12) -> rule6) OR ((triple11 triple8) -> rule2))] Harry is quiet.[(triple11)] Harry is rough.[(triple12)] @1: Harry is young.[(((triple12 triple8) -> rule4))]
Gary is big.
("Gary" "is" "big" "+")
triple1
Gary is furry.
("Gary" "is" "furry" "+")
triple2
((triple7) -> (rule1 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
((triple6 triple3) -> (rule8 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
((((triple1) -> (rule7 % int2))) -> (rule1 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
((((triple5 triple1) -> (rule4 % int2))) -> (rule1 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
((((triple5 triple4) -> (rule3 % int2))) -> (rule1 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
((triple6 ((triple5) -> (rule6 % int2))) -> (rule8 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
((triple6 ((triple4 triple1) -> (rule2 % int2))) -> (rule8 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is kind.
("Gary" "is" "kind" "+")
triple3
((triple5) -> (rule6 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
((triple4 triple1) -> (rule2 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
triple4
Gary is rough.
("Gary" "is" "rough" "+")
triple5
Gary is smart.
("Gary" "is" "smart" "+")
triple6
Gary is young.
("Gary" "is" "young" "+")
triple7
((triple1) -> (rule7 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
((triple5 triple1) -> (rule4 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
((triple5 triple4) -> (rule3 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
triple8
Harry is furry.
("Harry" "is" "furry" "+")
triple9
((triple8) -> (rule5 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
((((triple12 triple8) -> (rule4 % int2))) -> (rule1 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
triple10
((triple12) -> (rule6 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
((triple11 triple8) -> (rule2 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
triple11
Harry is rough.
("Harry" "is" "rough" "+")
triple12
Harry is young.
("Harry" "is" "young" "+")
((triple12 triple8) -> (rule4 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1