Dave is rough. Red things are not kind. All furry things are not kind. If something is green and furry then it is red. If Dave is rough then Dave is green. Green things are furry. If something is kind then it is rough.
Dave is rough.
("Dave" "is" "rough" "+")
Red things are not kind.
((("something" "is" "red" "+")) -> ("something" "is" "kind" "-"))
All furry things are not kind.
((("something" "is" "furry" "+")) -> ("something" "is" "kind" "-"))
If something is green and furry then it is red.
((("something" "is" "green" "+") ("something" "is" "furry" "+")) -> ("something" "is" "red" "+"))
If Dave is rough then Dave is green.
((("Dave" "is" "rough" "+")) -> ("Dave" "is" "green" "+"))
Green things are furry.
((("something" "is" "green" "+")) -> ("something" "is" "furry" "+"))
If something is kind then it is rough.
((("something" "is" "kind" "+")) -> ("something" "is" "rough" "+"))
Dave is rough.
True
1
proof
[(triple1)]
("Dave" "is" "rough" "+")
triple1
Dave is not rough.
False
1
inv-proof
[(triple1)]
("Dave" "is" "rough" "-")
triple1
Dave is green.
True
2
proof
[(((triple1) -> rule4))]
("Dave" "is" "green" "+")
((triple1) -> (rule4 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is not green.
False
2
inv-proof
[(((triple1) -> rule4))]
("Dave" "is" "green" "-")
((triple1) -> (rule4 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is furry.
True
3
proof
[(((((triple1) -> rule4)) -> rule5))]
("Dave" "is" "furry" "+")
((((triple1) -> (rule4 % int2))) -> (rule5 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is not furry.
False
3
inv-proof
[(((((triple1) -> rule4)) -> rule5))]
("Dave" "is" "furry" "-")
((((triple1) -> (rule4 % int2))) -> (rule5 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is red.
True
6
proof
[(((((triple1) -> rule4) ((((triple1) -> rule4)) -> rule5)) -> rule3))]
("Dave" "is" "red" "+")
((((triple1) -> (rule4 % int3)) ((((triple1) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
int3
Dave is kind.
False
4
inv-proof
[(((((((triple1) -> rule4)) -> rule5)) -> rule2) OR ((((((triple1) -> rule4) ((((triple1) -> rule4)) -> rule5)) -> rule3)) -> rule1))]
("Dave" "is" "kind" "+")
((((((triple1) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Dave is not kind.
("Dave" "is" "kind" "-")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
int3
((((((triple1) -> (rule4 % int4)) ((((triple1) -> (rule4 % int4))) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Dave is not kind.
("Dave" "is" "kind" "-")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
int3
Dave is green.
("Dave" "is" "green" "+")
int4
Dave is not young.
Unknown
inv-random
[@0: Dave is young.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "young" "-")
Dave is blue.
Unknown
random
[@0: Dave is blue.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "blue" "+")
@0: Dave is rough.[(triple1)] @1: Dave is green.[(((triple1) -> rule4))] @2: Dave is furry.[(((((triple1) -> rule4)) -> rule5))] @3: Dave is not kind.[(((((((triple1) -> rule4)) -> rule5)) -> rule2) OR ((((((triple1) -> rule4) ((((triple1) -> rule4)) -> rule5)) -> rule3)) -> rule1))] Dave is red.[(((((triple1) -> rule4) ((((triple1) -> rule4)) -> rule5)) -> rule3))]
Dave is rough.
("Dave" "is" "rough" "+")
triple1
Dave is green.
("Dave" "is" "green" "+")
((triple1) -> (rule4 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
((((triple1) -> (rule4 % int2))) -> (rule5 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is not kind.
("Dave" "is" "kind" "-")
((((((triple1) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Dave is not kind.
("Dave" "is" "kind" "-")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
int3
((((((triple1) -> (rule4 % int4)) ((((triple1) -> (rule4 % int4))) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Dave is not kind.
("Dave" "is" "kind" "-")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
int3
Dave is green.
("Dave" "is" "green" "+")
int4
Dave is red.
("Dave" "is" "red" "+")
((((triple1) -> (rule4 % int3)) ((((triple1) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
int3