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