Dave is big. Dave is blue. Dave is kind. Dave is nice. Dave is young. Gary is big. Gary is nice. Gary is smart. Gary is white. Harry is blue. Harry is kind. Harry is not smart. If Gary is young then Gary is nice. If Dave is young and Dave is nice then Dave is not white. If someone is nice and not white then they are not smart.
Dave is big.
("Dave" "is" "big" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is young.
("Dave" "is" "young" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Gary is white.
("Gary" "is" "white" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is not smart.
("Harry" "is" "smart" "-")
If Gary is young then Gary is nice.
((("Gary" "is" "young" "+")) -> ("Gary" "is" "nice" "+"))
If Dave is young and Dave is nice then Dave is not white.
((("Dave" "is" "young" "+") ("Dave" "is" "nice" "+")) -> ("Dave" "is" "white" "-"))
If someone is nice and not white then they are not smart.
((("someone" "is" "nice" "+") ("someone" "is" "white" "~")) -> ("someone" "is" "smart" "-"))
Harry is blue.
True
1
proof
[(triple10)]
("Harry" "is" "blue" "+")
triple10
Dave is not kind.
False
1
inv-proof
[(triple3)]
("Dave" "is" "kind" "-")
triple3
Dave is not white.
True
3
proof
[(((triple5 triple4) -> rule2))]
("Dave" "is" "white" "-")
((triple5 triple4) -> (rule2 % int1))
Dave is not white.
("Dave" "is" "white" "-")
int1
Dave is white.
False
3
inv-proof
[(((triple5 triple4) -> rule2))]
("Dave" "is" "white" "+")
((triple5 triple4) -> (rule2 % int1))
Dave is not white.
("Dave" "is" "white" "-")
int1
Dave is not smart.
True
5
proof
[(((triple4 ((triple5 triple4) -> rule2)) -> rule3))]
("Dave" "is" "smart" "-")
((triple4 ((triple5 triple4) -> (rule2 % int2))) -> (rule3 % int1))
Dave is not smart.
("Dave" "is" "smart" "-")
int1
Dave is not white.
("Dave" "is" "white" "-")
int2
Dave is smart.
False
5
inv-proof
[(((triple4 ((triple5 triple4) -> rule2)) -> rule3))]
("Dave" "is" "smart" "+")
((triple4 ((triple5 triple4) -> (rule2 % int2))) -> (rule3 % int1))
Dave is not smart.
("Dave" "is" "smart" "-")
int1
Dave is not white.
("Dave" "is" "white" "-")
int2
Gary is not kind.
Unknown
inv-random
[@0: Gary is kind.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "kind" "-")
Harry is white.
Unknown
random
[@0: Harry is white.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "white" "+")
Gary is not blue.
Unknown
inv-random
[@0: Gary is blue.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "blue" "-")
Harry is nice.
Unknown
random
[@0: Harry is nice.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "nice" "+")
Gary is not young.
Unknown
inv-random
[@0: Gary is young.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "young" "-")
Harry is big.
Unknown
random
[@0: Harry is big.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "big" "+")
@0: Dave is big.[(triple1)] Dave is blue.[(triple2)] Dave is kind.[(triple3)] Dave is nice.[(triple4)] Dave is young.[(triple5)] Gary is big.[(triple6)] Gary is nice.[(triple7)] Gary is smart.[(triple8)] Gary is white.[(triple9)] Harry is blue.[(triple10)] Harry is kind.[(triple11)] Harry is not smart.[(triple12)] @1: Dave is not white.[(((triple5 triple4) -> rule2))] @2: Dave is not smart.[(((triple4 ((triple5 triple4) -> rule2)) -> rule3))]
Dave is big.
("Dave" "is" "big" "+")
triple1
Dave is blue.
("Dave" "is" "blue" "+")
triple2
Dave is kind.
("Dave" "is" "kind" "+")
triple3
Dave is nice.
("Dave" "is" "nice" "+")
triple4
Dave is young.
("Dave" "is" "young" "+")
triple5
Gary is big.
("Gary" "is" "big" "+")
triple6
Gary is nice.
("Gary" "is" "nice" "+")
triple7
Gary is smart.
("Gary" "is" "smart" "+")
triple8
Gary is white.
("Gary" "is" "white" "+")
triple9
Harry is blue.
("Harry" "is" "blue" "+")
triple10
Harry is kind.
("Harry" "is" "kind" "+")
triple11
Harry is not smart.
("Harry" "is" "smart" "-")
triple12
Dave is not white.
("Dave" "is" "white" "-")
((triple5 triple4) -> (rule2 % int1))
Dave is not white.
("Dave" "is" "white" "-")
int1
Dave is not smart.
("Dave" "is" "smart" "-")
((triple4 ((triple5 triple4) -> (rule2 % int2))) -> (rule3 % int1))
Dave is not smart.
("Dave" "is" "smart" "-")
int1
Dave is not white.
("Dave" "is" "white" "-")
int2