Bob is furry. Bob is rough. Erin is furry. All furry, round people are white. All white, furry people are quiet. All red people are smart. All furry people are white. All quiet, furry people are smart. If someone is quiet and white then they are round. Red, quiet people are round. If Bob is red then Bob is rough.
Bob is furry.
("Bob" "is" "furry" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Erin is furry.
("Erin" "is" "furry" "+")
All furry, round people are white.
((("someone" "is" "furry" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "white" "+"))
All white, furry people are quiet.
((("someone" "is" "white" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "quiet" "+"))
All red people are smart.
((("someone" "is" "red" "+")) -> ("someone" "is" "smart" "+"))
All furry people are white.
((("someone" "is" "furry" "+")) -> ("someone" "is" "white" "+"))
All quiet, furry people are smart.
((("someone" "is" "quiet" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "smart" "+"))
If someone is quiet and white then they are round.
((("someone" "is" "quiet" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "round" "+"))
Red, quiet people are round.
((("someone" "is" "red" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "round" "+"))
If Bob is red then Bob is rough.
((("Bob" "is" "red" "+")) -> ("Bob" "is" "rough" "+"))
Bob is furry.
True
1
proof
[(triple1)]
("Bob" "is" "furry" "+")
triple1
Bob is not rough.
False
1
inv-proof
[(triple2)]
("Bob" "is" "rough" "-")
triple2
Bob is white.
True
2
proof
[(((triple1) -> rule4))]
("Bob" "is" "white" "+")
((triple1) -> (rule4 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Erin is not white.
False
2
inv-proof
[(((triple3) -> rule4))]
("Erin" "is" "white" "-")
((triple3) -> (rule4 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Bob is quiet.
True
4
proof
[(((((triple1) -> rule4) triple1) -> rule2))]
("Bob" "is" "quiet" "+")
((((triple1) -> (rule4 % int2)) triple1) -> (rule2 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Erin is not quiet.
False
4
inv-proof
[(((((triple3) -> rule4) triple3) -> rule2))]
("Erin" "is" "quiet" "-")
((((triple3) -> (rule4 % int2)) triple3) -> (rule2 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Bob is round.
True
7
proof
[(((((((triple1) -> rule4) triple1) -> rule2) ((triple1) -> rule4)) -> rule6))]
("Bob" "is" "round" "+")
((((((triple1) -> (rule4 % int3)) triple1) -> (rule2 % int2)) ((triple1) -> (rule4 % int3))) -> (rule6 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
Erin is not smart.
False
6
inv-proof
[(((((((triple3) -> rule4) triple3) -> rule2) triple3) -> rule5))]
("Erin" "is" "smart" "-")
((((((triple3) -> (rule4 % int3)) triple3) -> (rule2 % int2)) triple3) -> (rule5 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is white.
("Erin" "is" "white" "+")
int3
Bob is not red.
Unknown
inv-random
[@0: Bob is red.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "red" "-")
Erin is red.
Unknown
random
[@0: Erin is red.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "red" "+")
@0: Bob is furry.[(triple1)] Bob is rough.[(triple2)] Erin is furry.[(triple3)] @1: Bob is white.[(((triple1) -> rule4))] Erin is white.[(((triple3) -> rule4))] @2: Bob is quiet.[(((((triple1) -> rule4) triple1) -> rule2))] Erin is quiet.[(((((triple3) -> rule4) triple3) -> rule2))] @3: Bob is round.[(((((((triple1) -> rule4) triple1) -> rule2) ((triple1) -> rule4)) -> rule6))] Bob is smart.[(((((((triple1) -> rule4) triple1) -> rule2) triple1) -> rule5))] Erin is round.[(((((((triple3) -> rule4) triple3) -> rule2) ((triple3) -> rule4)) -> rule6))] Erin is smart.[(((((((triple3) -> rule4) triple3) -> rule2) triple3) -> rule5))]
Bob is furry.
("Bob" "is" "furry" "+")
triple1
Bob is rough.
("Bob" "is" "rough" "+")
triple2
Erin is furry.
("Erin" "is" "furry" "+")
triple3
Bob is white.
("Bob" "is" "white" "+")
((triple1) -> (rule4 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
((triple3) -> (rule4 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
((((triple1) -> (rule4 % int2)) triple1) -> (rule2 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
((((triple3) -> (rule4 % int2)) triple3) -> (rule2 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
((((((triple1) -> (rule4 % int3)) triple1) -> (rule2 % int2)) ((triple1) -> (rule4 % int3))) -> (rule6 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
Bob is smart.
("Bob" "is" "smart" "+")
((((((triple1) -> (rule4 % int3)) triple1) -> (rule2 % int2)) triple1) -> (rule5 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
Erin is round.
("Erin" "is" "round" "+")
((((((triple3) -> (rule4 % int3)) triple3) -> (rule2 % int2)) ((triple3) -> (rule4 % int3))) -> (rule6 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is white.
("Erin" "is" "white" "+")
int3
Erin is smart.
("Erin" "is" "smart" "+")
((((((triple3) -> (rule4 % int3)) triple3) -> (rule2 % int2)) triple3) -> (rule5 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is white.
("Erin" "is" "white" "+")
int3