Harry is round. Harry is smart. Harry is young. If Harry is young then Harry is white. If Harry is round and Harry is not smart then Harry is not white. White people are not big.
Harry is round.
("Harry" "is" "round" "+")
Harry is smart.
("Harry" "is" "smart" "+")
Harry is young.
("Harry" "is" "young" "+")
If Harry is young then Harry is white.
((("Harry" "is" "young" "+")) -> ("Harry" "is" "white" "+"))
If Harry is round and Harry is not smart then Harry is not white.
((("Harry" "is" "round" "+") ("Harry" "is" "smart" "~")) -> ("Harry" "is" "white" "-"))
White people are not big.
((("someone" "is" "white" "+")) -> ("someone" "is" "big" "-"))
Harry is round.
True
1
proof
[(triple1)]
("Harry" "is" "round" "+")
triple1
Harry is not round.
False
1
inv-proof
[(triple1)]
("Harry" "is" "round" "-")
triple1
Harry is white.
True
2
proof
[(((triple3) -> rule1))]
("Harry" "is" "white" "+")
((triple3) -> (rule1 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is not white.
False
2
inv-proof
[(((triple3) -> rule1))]
("Harry" "is" "white" "-")
((triple3) -> (rule1 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is not big.
True
3
proof
[(((((triple3) -> rule1)) -> rule3))]
("Harry" "is" "big" "-")
((((triple3) -> (rule1 % int2))) -> (rule3 % int1))
Harry is not big.
("Harry" "is" "big" "-")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is big.
False
3
inv-proof
[(((((triple3) -> rule1)) -> rule3))]
("Harry" "is" "big" "+")
((((triple3) -> (rule1 % int2))) -> (rule3 % int1))
Harry is not big.
("Harry" "is" "big" "-")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is not red.
Unknown
inv-random
[@0: Harry is red.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "red" "-")
Harry is kind.
Unknown
random
[@0: Harry is kind.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "kind" "+")
@0: Harry is round.[(triple1)] Harry is smart.[(triple2)] Harry is young.[(triple3)] @1: Harry is white.[(((triple3) -> rule1))] @2: Harry is not big.[(((((triple3) -> rule1)) -> rule3))]
Harry is round.
("Harry" "is" "round" "+")
triple1
Harry is smart.
("Harry" "is" "smart" "+")
triple2
Harry is young.
("Harry" "is" "young" "+")
triple3
Harry is white.
("Harry" "is" "white" "+")
((triple3) -> (rule1 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is not big.
("Harry" "is" "big" "-")
((((triple3) -> (rule1 % int2))) -> (rule3 % int1))
Harry is not big.
("Harry" "is" "big" "-")
int1
Harry is white.
("Harry" "is" "white" "+")
int2