Anne is green. Anne is kind. Anne is nice. Anne is rough. Anne is young. Charlie is green. Charlie is kind. Charlie is nice. Charlie is rough. Charlie is young. Dave is big. Dave is nice. Dave is quiet. Dave is rough. Dave is young. Young, quiet people are rough. If Dave is quiet then Dave is young. Young, quiet people are kind.
Anne is green.
("Anne" "is" "green" "+")
Anne is kind.
("Anne" "is" "kind" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Anne is young.
("Anne" "is" "young" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Dave is young.
("Dave" "is" "young" "+")
Young, quiet people are rough.
((("someone" "is" "young" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "rough" "+"))
If Dave is quiet then Dave is young.
((("Dave" "is" "quiet" "+")) -> ("Dave" "is" "young" "+"))
Young, quiet people are kind.
((("someone" "is" "young" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "kind" "+"))
Charlie is kind.
True
1
proof
[(triple7)]
("Charlie" "is" "kind" "+")
triple7
Dave is not young.
False
1
inv-proof
[(triple15 OR ((triple13) -> rule2))]
("Dave" "is" "young" "-")
triple15
((triple13) -> (rule2 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is kind.
True
3
proof
[(((triple15 triple13) -> rule3) OR ((((triple13) -> rule2) triple13) -> rule3))]
("Dave" "is" "kind" "+")
((triple15 triple13) -> (rule3 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
((((triple13) -> (rule2 % int2)) triple13) -> (rule3 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is not kind.
False
3
inv-proof
[(((triple15 triple13) -> rule3) OR ((((triple13) -> rule2) triple13) -> rule3))]
("Dave" "is" "kind" "-")
((triple15 triple13) -> (rule3 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
((((triple13) -> (rule2 % int2)) triple13) -> (rule3 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Anne is not big.
Unknown
inv-random
[@0: Anne is big.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "big" "-")
Charlie is big.
Unknown
random
[@0: Charlie is big.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "big" "+")
Dave is not green.
Unknown
inv-random
[@0: Dave is green.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "green" "-")
Charlie is quiet.
Unknown
random
[@0: Charlie is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "quiet" "+")
@0: Anne is green.[(triple1)] Anne is kind.[(triple2)] Anne is nice.[(triple3)] Anne is rough.[(triple4)] Anne is young.[(triple5)] Charlie is green.[(triple6)] Charlie is kind.[(triple7)] Charlie is nice.[(triple8)] Charlie is rough.[(triple9)] Charlie is young.[(triple10)] Dave is big.[(triple11)] Dave is nice.[(triple12)] Dave is quiet.[(triple13)] Dave is rough.[(triple14 OR ((triple15 triple13) -> rule1) OR ((((triple13) -> rule2) triple13) -> rule1))] Dave is young.[(triple15 OR ((triple13) -> rule2))] @1: Dave is kind.[(((triple15 triple13) -> rule3) OR ((((triple13) -> rule2) triple13) -> rule3))]
Anne is green.
("Anne" "is" "green" "+")
triple1
Anne is kind.
("Anne" "is" "kind" "+")
triple2
Anne is nice.
("Anne" "is" "nice" "+")
triple3
Anne is rough.
("Anne" "is" "rough" "+")
triple4
Anne is young.
("Anne" "is" "young" "+")
triple5
Charlie is green.
("Charlie" "is" "green" "+")
triple6
Charlie is kind.
("Charlie" "is" "kind" "+")
triple7
Charlie is nice.
("Charlie" "is" "nice" "+")
triple8
Charlie is rough.
("Charlie" "is" "rough" "+")
triple9
Charlie is young.
("Charlie" "is" "young" "+")
triple10
Dave is big.
("Dave" "is" "big" "+")
triple11
Dave is nice.
("Dave" "is" "nice" "+")
triple12
Dave is quiet.
("Dave" "is" "quiet" "+")
triple13
Dave is rough.
("Dave" "is" "rough" "+")
triple14
((triple15 triple13) -> (rule1 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
((((triple13) -> (rule2 % int2)) triple13) -> (rule1 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
triple15
((triple13) -> (rule2 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
((triple15 triple13) -> (rule3 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
((((triple13) -> (rule2 % int2)) triple13) -> (rule3 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2