Dave is smart. If Dave is green and Dave is smart then Dave is nice. If something is rough then it is green. White things are not nice. If something is smart and white then it is not kind. If Dave is smart then Dave is rough. If Dave is kind then Dave is white.
Dave is smart.
("Dave" "is" "smart" "+")
If Dave is green and Dave is smart then Dave is nice.
((("Dave" "is" "green" "+") ("Dave" "is" "smart" "+")) -> ("Dave" "is" "nice" "+"))
If something is rough then it is green.
((("something" "is" "rough" "+")) -> ("something" "is" "green" "+"))
White things are not nice.
((("something" "is" "white" "+")) -> ("something" "is" "nice" "-"))
If something is smart and white then it is not kind.
((("something" "is" "smart" "+") ("something" "is" "white" "+")) -> ("something" "is" "kind" "-"))
If Dave is smart then Dave is rough.
((("Dave" "is" "smart" "+")) -> ("Dave" "is" "rough" "+"))
If Dave is kind then Dave is white.
((("Dave" "is" "kind" "+")) -> ("Dave" "is" "white" "+"))
Dave is smart.
True
1
proof
[(triple1)]
("Dave" "is" "smart" "+")
triple1
Dave is not smart.
False
1
inv-proof
[(triple1)]
("Dave" "is" "smart" "-")
triple1
Dave is rough.
True
2
proof
[(((triple1) -> rule5))]
("Dave" "is" "rough" "+")
((triple1) -> (rule5 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is not rough.
False
2
inv-proof
[(((triple1) -> rule5))]
("Dave" "is" "rough" "-")
((triple1) -> (rule5 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is green.
True
3
proof
[(((((triple1) -> rule5)) -> rule2))]
("Dave" "is" "green" "+")
((((triple1) -> (rule5 % int2))) -> (rule2 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is not green.
False
3
inv-proof
[(((((triple1) -> rule5)) -> rule2))]
("Dave" "is" "green" "-")
((((triple1) -> (rule5 % int2))) -> (rule2 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is nice.
True
5
proof
[(((((((triple1) -> rule5)) -> rule2) triple1) -> rule1))]
("Dave" "is" "nice" "+")
((((((triple1) -> (rule5 % int3))) -> (rule2 % int2)) triple1) -> (rule1 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
Dave is not nice.
False
5
inv-proof
[(((((((triple1) -> rule5)) -> rule2) triple1) -> rule1))]
("Dave" "is" "nice" "-")
((((((triple1) -> (rule5 % int3))) -> (rule2 % int2)) triple1) -> (rule1 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
Dave is not white.
Unknown
inv-rconc
[@1: Dave is white.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Dave" "is" "white" "-")
Dave is young.
Unknown
random
[@0: Dave is young.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "young" "+")
@0: Dave is smart.[(triple1)] @1: Dave is rough.[(((triple1) -> rule5))] @2: Dave is green.[(((((triple1) -> rule5)) -> rule2))] @3: Dave is nice.[(((((((triple1) -> rule5)) -> rule2) triple1) -> rule1))]
Dave is smart.
("Dave" "is" "smart" "+")
triple1
Dave is rough.
("Dave" "is" "rough" "+")
((triple1) -> (rule5 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
((((triple1) -> (rule5 % int2))) -> (rule2 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
((((((triple1) -> (rule5 % int3))) -> (rule2 % int2)) triple1) -> (rule1 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3