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