Anne is big. Anne is kind. Anne is quiet. Anne is red. Anne is rough. Anne is smart. Gary is not kind. Gary is red. Gary is rough. Gary is young. Harry is big. Harry is kind. Harry is red. Harry is rough. Harry is not smart. Harry is young. All red people are big. If someone is kind and not smart then they are big. If Gary is red then Gary is rough.
Anne is big.
("Anne" "is" "big" "+")
Anne is kind.
("Anne" "is" "kind" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is red.
("Anne" "is" "red" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Gary is not kind.
("Gary" "is" "kind" "-")
Gary is red.
("Gary" "is" "red" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Gary is young.
("Gary" "is" "young" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is not smart.
("Harry" "is" "smart" "-")
Harry is young.
("Harry" "is" "young" "+")
All red people are big.
((("someone" "is" "red" "+")) -> ("someone" "is" "big" "+"))
If someone is kind and not smart then they are big.
((("someone" "is" "kind" "+") ("someone" "is" "smart" "~")) -> ("someone" "is" "big" "+"))
If Gary is red then Gary is rough.
((("Gary" "is" "red" "+")) -> ("Gary" "is" "rough" "+"))
Anne is smart.
True
1
proof
[(triple6)]
("Anne" "is" "smart" "+")
triple6
Anne is not rough.
False
1
inv-proof
[(triple5)]
("Anne" "is" "rough" "-")
triple5
Gary is big.
True
2
proof
[(((triple8) -> rule1))]
("Gary" "is" "big" "+")
((triple8) -> (rule1 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is not big.
False
2
inv-proof
[(((triple8) -> rule1))]
("Gary" "is" "big" "-")
((triple8) -> (rule1 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Harry is not quiet.
Unknown
inv-random
[@0: Harry is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "quiet" "-")
Gary is smart.
Unknown
random
[@0: Gary is smart.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "smart" "+")
Anne is not young.
Unknown
inv-random
[@0: Anne is young.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "young" "-")
Gary is quiet.
Unknown
random
[@0: Gary is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "quiet" "+")
@0: Anne is big.[(triple1 OR ((triple4) -> rule1))] Anne is kind.[(triple2)] Anne is quiet.[(triple3)] Anne is red.[(triple4)] Anne is rough.[(triple5)] Anne is smart.[(triple6)] Gary is not kind.[(triple7)] Gary is red.[(triple8)] Gary is rough.[(triple9 OR ((triple8) -> rule3))] Gary is young.[(triple10)] Harry is big.[(triple11 OR ((triple13) -> rule1) OR ((triple12 triple15) -> rule2))] Harry is kind.[(triple12)] Harry is not smart.[(triple15)] Harry is red.[(triple13)] Harry is rough.[(triple14)] Harry is young.[(triple16)] @1: Gary is big.[(((triple8) -> rule1))]
Anne is big.
("Anne" "is" "big" "+")
triple1
((triple4) -> (rule1 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
triple2
Anne is quiet.
("Anne" "is" "quiet" "+")
triple3
Anne is red.
("Anne" "is" "red" "+")
triple4
Anne is rough.
("Anne" "is" "rough" "+")
triple5
Anne is smart.
("Anne" "is" "smart" "+")
triple6
Gary is not kind.
("Gary" "is" "kind" "-")
triple7
Gary is red.
("Gary" "is" "red" "+")
triple8
Gary is rough.
("Gary" "is" "rough" "+")
triple9
((triple8) -> (rule3 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
triple10
Harry is big.
("Harry" "is" "big" "+")
triple11
((triple13) -> (rule1 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
((triple12 triple15) -> (rule2 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
triple12
Harry is not smart.
("Harry" "is" "smart" "-")
triple15
Harry is red.
("Harry" "is" "red" "+")
triple13
Harry is rough.
("Harry" "is" "rough" "+")
triple14
Harry is young.
("Harry" "is" "young" "+")
triple16
Gary is big.
("Gary" "is" "big" "+")
((triple8) -> (rule1 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1