Harry is furry. Harry is quiet. Harry is smart. If someone is quiet and not smart then they are kind. All nice people are kind. All furry people are nice.
Harry is furry.
("Harry" "is" "furry" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is smart.
("Harry" "is" "smart" "+")
If someone is quiet and not smart then they are kind.
((("someone" "is" "quiet" "+") ("someone" "is" "smart" "~")) -> ("someone" "is" "kind" "+"))
All nice people are kind.
((("someone" "is" "nice" "+")) -> ("someone" "is" "kind" "+"))
All furry people are nice.
((("someone" "is" "furry" "+")) -> ("someone" "is" "nice" "+"))
Harry is quiet.
True
1
proof
[(triple2)]
("Harry" "is" "quiet" "+")
triple2
Harry is not smart.
False
1
inv-proof
[(triple3)]
("Harry" "is" "smart" "-")
triple3
Harry is nice.
True
2
proof
[(((triple1) -> rule3))]
("Harry" "is" "nice" "+")
((triple1) -> (rule3 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is not nice.
False
2
inv-proof
[(((triple1) -> rule3))]
("Harry" "is" "nice" "-")
((triple1) -> (rule3 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is kind.
True
3
proof
[(((((triple1) -> rule3)) -> rule2))]
("Harry" "is" "kind" "+")
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is not kind.
False
3
inv-proof
[(((((triple1) -> rule3)) -> rule2))]
("Harry" "is" "kind" "-")
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is not rough.
Unknown
inv-random
[@0: Harry is rough.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "rough" "-")
Harry is young.
Unknown
random
[@0: Harry is young.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "young" "+")
@0: Harry is furry.[(triple1)] Harry is quiet.[(triple2)] Harry is smart.[(triple3)] @1: Harry is nice.[(((triple1) -> rule3))] @2: Harry is kind.[(((((triple1) -> rule3)) -> rule2))]
Harry is furry.
("Harry" "is" "furry" "+")
triple1
Harry is quiet.
("Harry" "is" "quiet" "+")
triple2
Harry is smart.
("Harry" "is" "smart" "+")
triple3
Harry is nice.
("Harry" "is" "nice" "+")
((triple1) -> (rule3 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2