Dave is furry. Dave is nice. Dave is rough. Erin is blue. Erin is furry. Erin is kind. Erin is nice. Erin is quiet. Erin is rough. Gary is nice. Gary is quiet. Gary is white. All white people are blue. If someone is rough then they are white. If Dave is blue then Dave is kind.
Dave is furry.
("Dave" "is" "furry" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is white.
("Gary" "is" "white" "+")
All white people are blue.
((("someone" "is" "white" "+")) -> ("someone" "is" "blue" "+"))
If someone is rough then they are white.
((("someone" "is" "rough" "+")) -> ("someone" "is" "white" "+"))
If Dave is blue then Dave is kind.
((("Dave" "is" "blue" "+")) -> ("Dave" "is" "kind" "+"))
Dave is nice.
True
1
proof
[(triple2)]
("Dave" "is" "nice" "+")
triple2
Dave is not rough.
False
1
inv-proof
[(triple3)]
("Dave" "is" "rough" "-")
triple3
Dave is white.
True
2
proof
[(((triple3) -> rule2))]
("Dave" "is" "white" "+")
((triple3) -> (rule2 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Erin is not white.
False
2
inv-proof
[(((triple9) -> rule2))]
("Erin" "is" "white" "-")
((triple9) -> (rule2 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Dave is blue.
True
3
proof
[(((((triple3) -> rule2)) -> rule1))]
("Dave" "is" "blue" "+")
((((triple3) -> (rule2 % int2))) -> (rule1 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is not blue.
False
3
inv-proof
[(((((triple3) -> rule2)) -> rule1))]
("Dave" "is" "blue" "-")
((((triple3) -> (rule2 % int2))) -> (rule1 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is kind.
True
4
proof
[(((((((triple3) -> rule2)) -> rule1)) -> rule3))]
("Dave" "is" "kind" "+")
((((((triple3) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
int3
Dave is not kind.
False
4
inv-proof
[(((((((triple3) -> rule2)) -> rule1)) -> rule3))]
("Dave" "is" "kind" "-")
((((((triple3) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
int3
Dave is not quiet.
Unknown
inv-random
[@0: Dave is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "quiet" "-")
Gary is rough.
Unknown
random
[@0: Gary is rough.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "rough" "+")
Gary is not kind.
Unknown
inv-random
[@0: Gary is kind.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "kind" "-")
Gary is furry.
Unknown
random
[@0: Gary is furry.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "furry" "+")
@0: Dave is furry.[(triple1)] Dave is nice.[(triple2)] Dave is rough.[(triple3)] Erin is blue.[(triple4 OR ((((triple9) -> rule2)) -> rule1))] Erin is furry.[(triple5)] Erin is kind.[(triple6)] Erin is nice.[(triple7)] Erin is quiet.[(triple8)] Erin is rough.[(triple9)] Gary is nice.[(triple10)] Gary is quiet.[(triple11)] Gary is white.[(triple12)] @1: Dave is white.[(((triple3) -> rule2))] Erin is white.[(((triple9) -> rule2))] Gary is blue.[(((triple12) -> rule1))] @2: Dave is blue.[(((((triple3) -> rule2)) -> rule1))] @3: Dave is kind.[(((((((triple3) -> rule2)) -> rule1)) -> rule3))]
Dave is furry.
("Dave" "is" "furry" "+")
triple1
Dave is nice.
("Dave" "is" "nice" "+")
triple2
Dave is rough.
("Dave" "is" "rough" "+")
triple3
Erin is blue.
("Erin" "is" "blue" "+")
triple4
((((triple9) -> (rule2 % int2))) -> (rule1 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is furry.
("Erin" "is" "furry" "+")
triple5
Erin is kind.
("Erin" "is" "kind" "+")
triple6
Erin is nice.
("Erin" "is" "nice" "+")
triple7
Erin is quiet.
("Erin" "is" "quiet" "+")
triple8
Erin is rough.
("Erin" "is" "rough" "+")
triple9
Gary is nice.
("Gary" "is" "nice" "+")
triple10
Gary is quiet.
("Gary" "is" "quiet" "+")
triple11
Gary is white.
("Gary" "is" "white" "+")
triple12
Dave is white.
("Dave" "is" "white" "+")
((triple3) -> (rule2 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
((triple9) -> (rule2 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
((triple12) -> (rule1 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
((((triple3) -> (rule2 % int2))) -> (rule1 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
((((((triple3) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
int3