Dave is furry. Dave is round. Dave is smart. Erin is furry. Erin is kind. Erin is white. Fiona is furry. Fiona is smart. Harry is kind. Harry is quiet. Harry is smart. Harry is white. If someone is red and kind then they are white. Kind, red people are white. Quiet, furry people are white. All white, quiet people are round. If someone is furry and smart then they are quiet. White, round people are furry.
Dave is furry.
("Dave" "is" "furry" "+")
Dave is round.
("Dave" "is" "round" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is white.
("Erin" "is" "white" "+")
Fiona is furry.
("Fiona" "is" "furry" "+")
Fiona is smart.
("Fiona" "is" "smart" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is smart.
("Harry" "is" "smart" "+")
Harry is white.
("Harry" "is" "white" "+")
If someone is red and kind then they are white.
((("someone" "is" "red" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "white" "+"))
Kind, red people are white.
((("someone" "is" "kind" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "white" "+"))
Quiet, furry people are white.
((("someone" "is" "quiet" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "white" "+"))
All white, quiet people are round.
((("someone" "is" "white" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "round" "+"))
If someone is furry and smart then they are quiet.
((("someone" "is" "furry" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "quiet" "+"))
White, round people are furry.
((("someone" "is" "white" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "furry" "+"))
Harry is kind.
True
1
proof
[(triple9)]
("Harry" "is" "kind" "+")
triple9
Erin is not white.
False
1
inv-proof
[(triple6)]
("Erin" "is" "white" "-")
triple6
Harry is round.
True
3
proof
[(((triple12 triple10) -> rule4))]
("Harry" "is" "round" "+")
((triple12 triple10) -> (rule4 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Dave is not quiet.
False
3
inv-proof
[(((triple1 triple3) -> rule5))]
("Dave" "is" "quiet" "-")
((triple1 triple3) -> (rule5 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is white.
True
5
proof
[(((((triple1 triple3) -> rule5) triple1) -> rule3))]
("Dave" "is" "white" "+")
((((triple1 triple3) -> (rule5 % int2)) triple1) -> (rule3 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is not white.
False
5
inv-proof
[(((((triple1 triple3) -> rule5) triple1) -> rule3))]
("Dave" "is" "white" "-")
((((triple1 triple3) -> (rule5 % int2)) triple1) -> (rule3 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Fiona is round.
True
9
proof
[(((((((triple7 triple8) -> rule5) triple7) -> rule3) ((triple7 triple8) -> rule5)) -> rule4))]
("Fiona" "is" "round" "+")
((((((triple7 triple8) -> (rule5 % int3)) triple7) -> (rule3 % int2)) ((triple7 triple8) -> (rule5 % int3))) -> (rule4 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
int2
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int3
Fiona is not round.
False
9
inv-proof
[(((((((triple7 triple8) -> rule5) triple7) -> rule3) ((triple7 triple8) -> rule5)) -> rule4))]
("Fiona" "is" "round" "-")
((((((triple7 triple8) -> (rule5 % int3)) triple7) -> (rule3 % int2)) ((triple7 triple8) -> (rule5 % int3))) -> (rule4 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
int2
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int3
Erin is not round.
Unknown
inv-rconc
[@2: Erin is round.[CWA. Example of deepest failure = (rule4 <- rule5 <- FAIL)]]
("Erin" "is" "round" "-")
Erin is quiet.
Unknown
rconc
[@1: Erin is quiet.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Erin" "is" "quiet" "+")
Dave is not red.
Unknown
inv-random
[@0: Dave is red.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "red" "-")
Dave is kind.
Unknown
random
[@0: Dave is kind.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "kind" "+")
Harry is not red.
Unknown
inv-random
[@0: Harry is red.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "red" "-")
Erin is smart.
Unknown
random
[@0: Erin is smart.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "smart" "+")
Erin is not red.
Unknown
inv-random
[@0: Erin is red.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "red" "-")
Fiona is red.
Unknown
random
[@0: Fiona is red.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "red" "+")
@0: Dave is furry.[(triple1)] Dave is round.[(triple2 OR ((((((triple1 triple3) -> rule5) triple1) -> rule3) ((triple1 triple3) -> rule5)) -> rule4))] Dave is smart.[(triple3)] Erin is furry.[(triple4)] Erin is kind.[(triple5)] Erin is white.[(triple6)] Fiona is furry.[(triple7)] Fiona is smart.[(triple8)] Harry is kind.[(triple9)] Harry is quiet.[(triple10)] Harry is smart.[(triple11)] Harry is white.[(triple12)] @1: Dave is quiet.[(((triple1 triple3) -> rule5))] Fiona is quiet.[(((triple7 triple8) -> rule5))] Harry is round.[(((triple12 triple10) -> rule4))] @2: Dave is white.[(((((triple1 triple3) -> rule5) triple1) -> rule3))] Fiona is white.[(((((triple7 triple8) -> rule5) triple7) -> rule3))] Harry is furry.[(((triple12 ((triple12 triple10) -> rule4)) -> rule6))] @3: Fiona is round.[(((((((triple7 triple8) -> rule5) triple7) -> rule3) ((triple7 triple8) -> rule5)) -> rule4))]
Dave is furry.
("Dave" "is" "furry" "+")
triple1
Dave is round.
("Dave" "is" "round" "+")
triple2
((((((triple1 triple3) -> (rule5 % int3)) triple1) -> (rule3 % int2)) ((triple1 triple3) -> (rule5 % int3))) -> (rule4 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
int3
Dave is smart.
("Dave" "is" "smart" "+")
triple3
Erin is furry.
("Erin" "is" "furry" "+")
triple4
Erin is kind.
("Erin" "is" "kind" "+")
triple5
Erin is white.
("Erin" "is" "white" "+")
triple6
Fiona is furry.
("Fiona" "is" "furry" "+")
triple7
Fiona is smart.
("Fiona" "is" "smart" "+")
triple8
Harry is kind.
("Harry" "is" "kind" "+")
triple9
Harry is quiet.
("Harry" "is" "quiet" "+")
triple10
Harry is smart.
("Harry" "is" "smart" "+")
triple11
Harry is white.
("Harry" "is" "white" "+")
triple12
Dave is quiet.
("Dave" "is" "quiet" "+")
((triple1 triple3) -> (rule5 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
((triple7 triple8) -> (rule5 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
((triple12 triple10) -> (rule4 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
((((triple1 triple3) -> (rule5 % int2)) triple1) -> (rule3 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Fiona is white.
("Fiona" "is" "white" "+")
((((triple7 triple8) -> (rule5 % int2)) triple7) -> (rule3 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
((triple12 ((triple12 triple10) -> (rule4 % int2))) -> (rule6 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Fiona is round.
("Fiona" "is" "round" "+")
((((((triple7 triple8) -> (rule5 % int3)) triple7) -> (rule3 % int2)) ((triple7 triple8) -> (rule5 % int3))) -> (rule4 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
int2
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int3