Dave is nice. Dave is rough. Dave is young. Rough, white people are smart. If Dave is nice then Dave is white. If someone is white then they are nice. Young, furry people are white. White people are young. If Dave is white then Dave is nice. Furry, white people are rough. If Dave is young then Dave is white.
Dave is nice.
("Dave" "is" "nice" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Dave is young.
("Dave" "is" "young" "+")
Rough, white people are smart.
((("someone" "is" "rough" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "smart" "+"))
If Dave is nice then Dave is white.
((("Dave" "is" "nice" "+")) -> ("Dave" "is" "white" "+"))
If someone is white then they are nice.
((("someone" "is" "white" "+")) -> ("someone" "is" "nice" "+"))
Young, furry people are white.
((("someone" "is" "young" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "white" "+"))
White people are young.
((("someone" "is" "white" "+")) -> ("someone" "is" "young" "+"))
If Dave is white then Dave is nice.
((("Dave" "is" "white" "+")) -> ("Dave" "is" "nice" "+"))
Furry, white people are rough.
((("someone" "is" "furry" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "rough" "+"))
If Dave is young then Dave is white.
((("Dave" "is" "young" "+")) -> ("Dave" "is" "white" "+"))
Dave is nice.
True
1
proof
[(triple1 OR ((((triple3) -> rule8)) -> rule3) OR ((((triple3) -> rule8)) -> rule6))]
("Dave" "is" "nice" "+")
triple1
((((triple3) -> (rule8 % int2))) -> (rule3 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
((((triple3) -> (rule8 % int2))) -> (rule6 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is not nice.
False
1
inv-proof
[(triple1 OR ((((triple3) -> rule8)) -> rule3) OR ((((triple3) -> rule8)) -> rule6))]
("Dave" "is" "nice" "-")
triple1
((((triple3) -> (rule8 % int2))) -> (rule3 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
((((triple3) -> (rule8 % int2))) -> (rule6 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is white.
True
2
proof
[(((triple1) -> rule2) OR ((triple3) -> rule8))]
("Dave" "is" "white" "+")
((triple1) -> (rule2 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
((triple3) -> (rule8 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is not white.
False
2
inv-proof
[(((triple1) -> rule2) OR ((triple3) -> rule8))]
("Dave" "is" "white" "-")
((triple1) -> (rule2 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
((triple3) -> (rule8 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is not quiet.
Unknown
inv-random
[@0: Dave is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "quiet" "-")
Dave is furry.
Unknown
random
[@0: Dave is furry.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "furry" "+")
@0: Dave is nice.[(triple1 OR ((((triple3) -> rule8)) -> rule3) OR ((((triple3) -> rule8)) -> rule6))] Dave is rough.[(triple2)] Dave is young.[(triple3 OR ((((triple1) -> rule2)) -> rule5))] @1: Dave is white.[(((triple1) -> rule2) OR ((triple3) -> rule8))] @2: Dave is smart.[(((triple2 ((triple1) -> rule2)) -> rule1) OR ((triple2 ((triple3) -> rule8)) -> rule1))]
Dave is nice.
("Dave" "is" "nice" "+")
triple1
((((triple3) -> (rule8 % int2))) -> (rule3 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
((((triple3) -> (rule8 % int2))) -> (rule6 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
triple2
Dave is young.
("Dave" "is" "young" "+")
triple3
((((triple1) -> (rule2 % int2))) -> (rule5 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
((triple1) -> (rule2 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
((triple3) -> (rule8 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
((triple2 ((triple1) -> (rule2 % int2))) -> (rule1 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
((triple2 ((triple3) -> (rule8 % int2))) -> (rule1 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2