Harry is furry. Harry is green. Harry is young. If someone is red and not smart then they are not green. If Harry is young and Harry is rough then Harry is kind. If Harry is young then Harry is kind. If someone is furry then they are rough. If Harry is smart then Harry is furry. All kind people are not red. If Harry is smart then Harry is red. If Harry is not kind and Harry is not furry then Harry is green.
Harry is furry.
("Harry" "is" "furry" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is young.
("Harry" "is" "young" "+")
If someone is red and not smart then they are not green.
((("someone" "is" "red" "+") ("someone" "is" "smart" "~")) -> ("someone" "is" "green" "-"))
If Harry is young and Harry is rough then Harry is kind.
((("Harry" "is" "young" "+") ("Harry" "is" "rough" "+")) -> ("Harry" "is" "kind" "+"))
If Harry is young then Harry is kind.
((("Harry" "is" "young" "+")) -> ("Harry" "is" "kind" "+"))
If someone is furry then they are rough.
((("someone" "is" "furry" "+")) -> ("someone" "is" "rough" "+"))
If Harry is smart then Harry is furry.
((("Harry" "is" "smart" "+")) -> ("Harry" "is" "furry" "+"))
All kind people are not red.
((("someone" "is" "kind" "+")) -> ("someone" "is" "red" "-"))
If Harry is smart then Harry is red.
((("Harry" "is" "smart" "+")) -> ("Harry" "is" "red" "+"))
If Harry is not kind and Harry is not furry then Harry is green.
((("Harry" "is" "kind" "~") ("Harry" "is" "furry" "~")) -> ("Harry" "is" "green" "+"))
Harry is green.
True
1
proof
[(triple2)]
("Harry" "is" "green" "+")
triple2
Harry is not young.
False
1
inv-proof
[(triple3)]
("Harry" "is" "young" "-")
triple3
Harry is rough.
True
2
proof
[(((triple1) -> rule4))]
("Harry" "is" "rough" "+")
((triple1) -> (rule4 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is not rough.
False
2
inv-proof
[(((triple1) -> rule4))]
("Harry" "is" "rough" "-")
((triple1) -> (rule4 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is not red.
True
3
proof
[(((((triple3) -> rule3)) -> rule6) OR ((((triple3 ((triple1) -> rule4)) -> rule2)) -> rule6))]
("Harry" "is" "red" "-")
((((triple3) -> (rule3 % int2))) -> (rule6 % int1))
Harry is not red.
("Harry" "is" "red" "-")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
((((triple3 ((triple1) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Harry is not red.
("Harry" "is" "red" "-")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3
Harry is red.
False
3
inv-proof
[(((((triple3) -> rule3)) -> rule6) OR ((((triple3 ((triple1) -> rule4)) -> rule2)) -> rule6))]
("Harry" "is" "red" "+")
((((triple3) -> (rule3 % int2))) -> (rule6 % int1))
Harry is not red.
("Harry" "is" "red" "-")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
((((triple3 ((triple1) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Harry is not red.
("Harry" "is" "red" "-")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3
@0: Harry is furry.[(triple1)] Harry is green.[(triple2)] Harry is young.[(triple3)] @1: Harry is kind.[(((triple3) -> rule3) OR ((triple3 ((triple1) -> rule4)) -> rule2))] Harry is rough.[(((triple1) -> rule4))] @2: Harry is not red.[(((((triple3) -> rule3)) -> rule6) OR ((((triple3 ((triple1) -> rule4)) -> rule2)) -> rule6))]
Harry is furry.
("Harry" "is" "furry" "+")
triple1
Harry is green.
("Harry" "is" "green" "+")
triple2
Harry is young.
("Harry" "is" "young" "+")
triple3
Harry is kind.
("Harry" "is" "kind" "+")
((triple3) -> (rule3 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
((triple3 ((triple1) -> (rule4 % int2))) -> (rule2 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
((triple1) -> (rule4 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is not red.
("Harry" "is" "red" "-")
((((triple3) -> (rule3 % int2))) -> (rule6 % int1))
Harry is not red.
("Harry" "is" "red" "-")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
((((triple3 ((triple1) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Harry is not red.
("Harry" "is" "red" "-")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3