Dave is green. Dave is white. Dave is young. If something is white and young then it is kind. If Dave is kind then Dave is rough.
Dave is green.
("Dave" "is" "green" "+")
Dave is white.
("Dave" "is" "white" "+")
Dave is young.
("Dave" "is" "young" "+")
If something is white and young then it is kind.
((("something" "is" "white" "+") ("something" "is" "young" "+")) -> ("something" "is" "kind" "+"))
If Dave is kind then Dave is rough.
((("Dave" "is" "kind" "+")) -> ("Dave" "is" "rough" "+"))
Dave is green.
True
1
proof
[(triple1)]
("Dave" "is" "green" "+")
triple1
Dave is not young.
False
1
inv-proof
[(triple3)]
("Dave" "is" "young" "-")
triple3
Dave is kind.
True
3
proof
[(((triple2 triple3) -> rule1))]
("Dave" "is" "kind" "+")
((triple2 triple3) -> (rule1 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is not kind.
False
3
inv-proof
[(((triple2 triple3) -> rule1))]
("Dave" "is" "kind" "-")
((triple2 triple3) -> (rule1 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is rough.
True
4
proof
[(((((triple2 triple3) -> rule1)) -> rule2))]
("Dave" "is" "rough" "+")
((((triple2 triple3) -> (rule1 % int2))) -> (rule2 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is not rough.
False
4
inv-proof
[(((((triple2 triple3) -> rule1)) -> rule2))]
("Dave" "is" "rough" "-")
((((triple2 triple3) -> (rule1 % int2))) -> (rule2 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is not quiet.
Unknown
inv-random
[@0: Dave is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "quiet" "-")
Dave is nice.
Unknown
random
[@0: Dave is nice.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "nice" "+")
@0: Dave is green.[(triple1)] Dave is white.[(triple2)] Dave is young.[(triple3)] @1: Dave is kind.[(((triple2 triple3) -> rule1))] @2: Dave is rough.[(((((triple2 triple3) -> rule1)) -> rule2))]
Dave is green.
("Dave" "is" "green" "+")
triple1
Dave is white.
("Dave" "is" "white" "+")
triple2
Dave is young.
("Dave" "is" "young" "+")
triple3
Dave is kind.
("Dave" "is" "kind" "+")
((triple2 triple3) -> (rule1 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
((((triple2 triple3) -> (rule1 % int2))) -> (rule2 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2