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