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