Harry is quiet. All big people are kind. If Harry is quiet then Harry is blue. If Harry is white and Harry is red then Harry is blue. If someone is quiet then they are young. All big, quiet people are white. All red people are white. If someone is quiet then they are white. White people are kind.
Harry is quiet.
("Harry" "is" "quiet" "+")
All big people are kind.
((("someone" "is" "big" "+")) -> ("someone" "is" "kind" "+"))
If Harry is quiet then Harry is blue.
((("Harry" "is" "quiet" "+")) -> ("Harry" "is" "blue" "+"))
If Harry is white and Harry is red then Harry is blue.
((("Harry" "is" "white" "+") ("Harry" "is" "red" "+")) -> ("Harry" "is" "blue" "+"))
If someone is quiet then they are young.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "young" "+"))
All big, quiet people are white.
((("someone" "is" "big" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "white" "+"))
All red people are white.
((("someone" "is" "red" "+")) -> ("someone" "is" "white" "+"))
If someone is quiet then they are white.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "white" "+"))
White people are kind.
((("someone" "is" "white" "+")) -> ("someone" "is" "kind" "+"))
Harry is quiet.
True
1
proof
[(triple1)]
("Harry" "is" "quiet" "+")
triple1
Harry is not quiet.
False
1
inv-proof
[(triple1)]
("Harry" "is" "quiet" "-")
triple1
Harry is blue.
True
2
proof
[(((triple1) -> rule2))]
("Harry" "is" "blue" "+")
((triple1) -> (rule2 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is not blue.
False
2
inv-proof
[(((triple1) -> rule2))]
("Harry" "is" "blue" "-")
((triple1) -> (rule2 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is kind.
True
3
proof
[(((((triple1) -> rule7)) -> rule8))]
("Harry" "is" "kind" "+")
((((triple1) -> (rule7 % int2))) -> (rule8 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is not kind.
False
3
inv-proof
[(((((triple1) -> rule7)) -> rule8))]
("Harry" "is" "kind" "-")
((((triple1) -> (rule7 % int2))) -> (rule8 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is not big.
Unknown
inv-random
[@0: Harry is big.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "big" "-")
Harry is red.
Unknown
random
[@0: Harry is red.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "red" "+")
@0: Harry is quiet.[(triple1)] @1: Harry is blue.[(((triple1) -> rule2))] Harry is white.[(((triple1) -> rule7))] Harry is young.[(((triple1) -> rule4))] @2: Harry is kind.[(((((triple1) -> rule7)) -> rule8))]
Harry is quiet.
("Harry" "is" "quiet" "+")
triple1
Harry is blue.
("Harry" "is" "blue" "+")
((triple1) -> (rule2 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
((triple1) -> (rule7 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
((triple1) -> (rule4 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
((((triple1) -> (rule7 % int2))) -> (rule8 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2