Harry is green. Harry is kind. Harry is rough. All green, rough people are not round. Furry people are not quiet. If someone is rough and not round then they are furry.
Harry is green.
("Harry" "is" "green" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is rough.
("Harry" "is" "rough" "+")
All green, rough people are not round.
((("someone" "is" "green" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "round" "-"))
Furry people are not quiet.
((("someone" "is" "furry" "+")) -> ("someone" "is" "quiet" "-"))
If someone is rough and not round then they are furry.
((("someone" "is" "rough" "+") ("someone" "is" "round" "~")) -> ("someone" "is" "furry" "+"))
Harry is kind.
True
1
proof
[(triple2)]
("Harry" "is" "kind" "+")
triple2
Harry is not rough.
False
1
inv-proof
[(triple3)]
("Harry" "is" "rough" "-")
triple3
Harry is not round.
True
3
proof
[(((triple1 triple3) -> rule1))]
("Harry" "is" "round" "-")
((triple1 triple3) -> (rule1 % int1))
Harry is not round.
("Harry" "is" "round" "-")
int1
Harry is round.
False
3
inv-proof
[(((triple1 triple3) -> rule1))]
("Harry" "is" "round" "+")
((triple1 triple3) -> (rule1 % int1))
Harry is not round.
("Harry" "is" "round" "-")
int1
Harry is furry.
True
5
proof
[(((triple3 ((triple1 triple3) -> rule1)) -> rule3))]
("Harry" "is" "furry" "+")
((triple3 ((triple1 triple3) -> (rule1 % int2))) -> (rule3 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is not round.
("Harry" "is" "round" "-")
int2
Harry is not furry.
False
5
inv-proof
[(((triple3 ((triple1 triple3) -> rule1)) -> rule3))]
("Harry" "is" "furry" "-")
((triple3 ((triple1 triple3) -> (rule1 % int2))) -> (rule3 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is not round.
("Harry" "is" "round" "-")
int2
Harry is not quiet.
True
6
proof
[(((((triple3 ((triple1 triple3) -> rule1)) -> rule3)) -> rule2))]
("Harry" "is" "quiet" "-")
((((triple3 ((triple1 triple3) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Harry is not quiet.
("Harry" "is" "quiet" "-")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is not round.
("Harry" "is" "round" "-")
int3
Harry is quiet.
False
6
inv-proof
[(((((triple3 ((triple1 triple3) -> rule1)) -> rule3)) -> rule2))]
("Harry" "is" "quiet" "+")
((((triple3 ((triple1 triple3) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Harry is not quiet.
("Harry" "is" "quiet" "-")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is not round.
("Harry" "is" "round" "-")
int3
@0: Harry is green.[(triple1)] Harry is kind.[(triple2)] Harry is rough.[(triple3)] @1: Harry is not round.[(((triple1 triple3) -> rule1))] @2: Harry is furry.[(((triple3 ((triple1 triple3) -> rule1)) -> rule3))] @3: Harry is not quiet.[(((((triple3 ((triple1 triple3) -> rule1)) -> rule3)) -> rule2))]
Harry is green.
("Harry" "is" "green" "+")
triple1
Harry is kind.
("Harry" "is" "kind" "+")
triple2
Harry is rough.
("Harry" "is" "rough" "+")
triple3
Harry is not round.
("Harry" "is" "round" "-")
((triple1 triple3) -> (rule1 % int1))
Harry is not round.
("Harry" "is" "round" "-")
int1
Harry is furry.
("Harry" "is" "furry" "+")
((triple3 ((triple1 triple3) -> (rule1 % int2))) -> (rule3 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is not round.
("Harry" "is" "round" "-")
int2
Harry is not quiet.
("Harry" "is" "quiet" "-")
((((triple3 ((triple1 triple3) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Harry is not quiet.
("Harry" "is" "quiet" "-")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is not round.
("Harry" "is" "round" "-")
int3