Dave is kind. Dave is red. Dave is rough. Dave is round. Gary is green. Gary is nice. Gary is red. Gary is rough. Gary is round. Gary is young. If someone is kind then they are nice. All nice, red people are young.
Dave is kind.
("Dave" "is" "kind" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Dave is round.
("Dave" "is" "round" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Gary is round.
("Gary" "is" "round" "+")
Gary is young.
("Gary" "is" "young" "+")
If someone is kind then they are nice.
((("someone" "is" "kind" "+")) -> ("someone" "is" "nice" "+"))
All nice, red people are young.
((("someone" "is" "nice" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "young" "+"))
Dave is kind.
True
1
proof
[(triple1)]
("Dave" "is" "kind" "+")
triple1
Gary is not red.
False
1
inv-proof
[(triple7)]
("Gary" "is" "red" "-")
triple7
Dave is nice.
True
2
proof
[(((triple1) -> rule1))]
("Dave" "is" "nice" "+")
((triple1) -> (rule1 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is not nice.
False
2
inv-proof
[(((triple1) -> rule1))]
("Dave" "is" "nice" "-")
((triple1) -> (rule1 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is young.
True
4
proof
[(((((triple1) -> rule1) triple2) -> rule2))]
("Dave" "is" "young" "+")
((((triple1) -> (rule1 % int2)) triple2) -> (rule2 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is not young.
False
4
inv-proof
[(((((triple1) -> rule1) triple2) -> rule2))]
("Dave" "is" "young" "-")
((((triple1) -> (rule1 % int2)) triple2) -> (rule2 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is not green.
Unknown
inv-random
[@0: Dave is green.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "green" "-")
Gary is kind.
Unknown
random
[@0: Gary is kind.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "kind" "+")
@0: Dave is kind.[(triple1)] Dave is red.[(triple2)] Dave is rough.[(triple3)] Dave is round.[(triple4)] Gary is green.[(triple5)] Gary is nice.[(triple6)] Gary is red.[(triple7)] Gary is rough.[(triple8)] Gary is round.[(triple9)] Gary is young.[(triple10 OR ((triple6 triple7) -> rule2))] @1: Dave is nice.[(((triple1) -> rule1))] @2: Dave is young.[(((((triple1) -> rule1) triple2) -> rule2))]
Dave is kind.
("Dave" "is" "kind" "+")
triple1
Dave is red.
("Dave" "is" "red" "+")
triple2
Dave is rough.
("Dave" "is" "rough" "+")
triple3
Dave is round.
("Dave" "is" "round" "+")
triple4
Gary is green.
("Gary" "is" "green" "+")
triple5
Gary is nice.
("Gary" "is" "nice" "+")
triple6
Gary is red.
("Gary" "is" "red" "+")
triple7
Gary is rough.
("Gary" "is" "rough" "+")
triple8
Gary is round.
("Gary" "is" "round" "+")
triple9
Gary is young.
("Gary" "is" "young" "+")
triple10
((triple6 triple7) -> (rule2 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
((triple1) -> (rule1 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
((((triple1) -> (rule1 % int2)) triple2) -> (rule2 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2