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