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