Harry is nice. Harry is smart. Harry is young. All rough, young things are round. If something is young then it is rough. If something is quiet then it is young.
Harry is nice.
("Harry" "is" "nice" "+")
Harry is smart.
("Harry" "is" "smart" "+")
Harry is young.
("Harry" "is" "young" "+")
All rough, young things are round.
((("something" "is" "rough" "+") ("something" "is" "young" "+")) -> ("something" "is" "round" "+"))
If something is young then it is rough.
((("something" "is" "young" "+")) -> ("something" "is" "rough" "+"))
If something is quiet then it is young.
((("something" "is" "quiet" "+")) -> ("something" "is" "young" "+"))
Harry is nice.
True
1
proof
[(triple1)]
("Harry" "is" "nice" "+")
triple1
Harry is not smart.
False
1
inv-proof
[(triple2)]
("Harry" "is" "smart" "-")
triple2
Harry is rough.
True
2
proof
[(((triple3) -> rule2))]
("Harry" "is" "rough" "+")
((triple3) -> (rule2 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is not rough.
False
2
inv-proof
[(((triple3) -> rule2))]
("Harry" "is" "rough" "-")
((triple3) -> (rule2 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is round.
True
4
proof
[(((((triple3) -> rule2) triple3) -> rule1))]
("Harry" "is" "round" "+")
((((triple3) -> (rule2 % int2)) triple3) -> (rule1 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is not round.
False
4
inv-proof
[(((((triple3) -> rule2) triple3) -> rule1))]
("Harry" "is" "round" "-")
((((triple3) -> (rule2 % int2)) triple3) -> (rule1 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is not kind.
Unknown
inv-random
[@0: Harry is kind.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "kind" "-")
Harry is quiet.
Unknown
random
[@0: Harry is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "quiet" "+")
@0: Harry is nice.[(triple1)] Harry is smart.[(triple2)] Harry is young.[(triple3)] @1: Harry is rough.[(((triple3) -> rule2))] @2: Harry is round.[(((((triple3) -> rule2) triple3) -> rule1))]
Harry is nice.
("Harry" "is" "nice" "+")
triple1
Harry is smart.
("Harry" "is" "smart" "+")
triple2
Harry is young.
("Harry" "is" "young" "+")
triple3
Harry is rough.
("Harry" "is" "rough" "+")
((triple3) -> (rule2 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
((((triple3) -> (rule2 % int2)) triple3) -> (rule1 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2