Anne is furry. Anne is kind. Anne is not nice. Anne is rough. Anne is smart. Anne is white. Dave is furry. Dave is kind. Dave is nice. Dave is rough. Dave is white. Dave is young. If something is kind then it is white.
Anne is furry.
("Anne" "is" "furry" "+")
Anne is kind.
("Anne" "is" "kind" "+")
Anne is not nice.
("Anne" "is" "nice" "-")
Anne is rough.
("Anne" "is" "rough" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Anne is white.
("Anne" "is" "white" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Dave is white.
("Dave" "is" "white" "+")
Dave is young.
("Dave" "is" "young" "+")
If something is kind then it is white.
((("something" "is" "kind" "+")) -> ("something" "is" "white" "+"))
Dave is young.
True
1
proof
[(triple12)]
("Dave" "is" "young" "+")
triple12
Anne is not white.
False
1
inv-proof
[(triple6 OR ((triple2) -> rule1))]
("Anne" "is" "white" "-")
triple6
((triple2) -> (rule1 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is not young.
Unknown
inv-random
[@0: Anne is young.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "young" "-")
Dave is smart.
Unknown
random
[@0: Dave is smart.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "smart" "+")
@0: Anne is furry.[(triple1)] Anne is kind.[(triple2)] Anne is not nice.[(triple3)] Anne is rough.[(triple4)] Anne is smart.[(triple5)] Anne is white.[(triple6 OR ((triple2) -> rule1))] Dave is furry.[(triple7)] Dave is kind.[(triple8)] Dave is nice.[(triple9)] Dave is rough.[(triple10)] Dave is white.[(triple11 OR ((triple8) -> rule1))] Dave is young.[(triple12)]
Anne is furry.
("Anne" "is" "furry" "+")
triple1
Anne is kind.
("Anne" "is" "kind" "+")
triple2
Anne is not nice.
("Anne" "is" "nice" "-")
triple3
Anne is rough.
("Anne" "is" "rough" "+")
triple4
Anne is smart.
("Anne" "is" "smart" "+")
triple5
Anne is white.
("Anne" "is" "white" "+")
triple6
((triple2) -> (rule1 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
triple7
Dave is kind.
("Dave" "is" "kind" "+")
triple8
Dave is nice.
("Dave" "is" "nice" "+")
triple9
Dave is rough.
("Dave" "is" "rough" "+")
triple10
Dave is white.
("Dave" "is" "white" "+")
triple11
((triple8) -> (rule1 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
triple12