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