Anne is kind. Anne is not red. Anne is round. Anne is not smart. Anne is white. Erin is furry. Erin is kind. Erin is not smart. Fiona is kind. Fiona is round. Fiona is smart. Fiona is white. Harry is furry. Harry is red. Harry is smart. Harry is white. All smart, kind things are white. Kind, red things are white. All white, kind things are round. Round, furry things are red. If Harry is red then Harry is round. If Erin is kind then Erin is white. If Fiona is kind and Fiona is smart then Fiona is round. If something is kind then it is not quiet.
Anne is kind.
("Anne" "is" "kind" "+")
Anne is not red.
("Anne" "is" "red" "-")
Anne is round.
("Anne" "is" "round" "+")
Anne is not smart.
("Anne" "is" "smart" "-")
Anne is white.
("Anne" "is" "white" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is not smart.
("Erin" "is" "smart" "-")
Fiona is kind.
("Fiona" "is" "kind" "+")
Fiona is round.
("Fiona" "is" "round" "+")
Fiona is smart.
("Fiona" "is" "smart" "+")
Fiona is white.
("Fiona" "is" "white" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is smart.
("Harry" "is" "smart" "+")
Harry is white.
("Harry" "is" "white" "+")
All smart, kind things are white.
((("something" "is" "smart" "+") ("something" "is" "kind" "+")) -> ("something" "is" "white" "+"))
Kind, red things are white.
((("something" "is" "kind" "+") ("something" "is" "red" "+")) -> ("something" "is" "white" "+"))
All white, kind things are round.
((("something" "is" "white" "+") ("something" "is" "kind" "+")) -> ("something" "is" "round" "+"))
Round, furry things are red.
((("something" "is" "round" "+") ("something" "is" "furry" "+")) -> ("something" "is" "red" "+"))
If Harry is red then Harry is round.
((("Harry" "is" "red" "+")) -> ("Harry" "is" "round" "+"))
If Erin is kind then Erin is white.
((("Erin" "is" "kind" "+")) -> ("Erin" "is" "white" "+"))
If Fiona is kind and Fiona is smart then Fiona is round.
((("Fiona" "is" "kind" "+") ("Fiona" "is" "smart" "+")) -> ("Fiona" "is" "round" "+"))
If something is kind then it is not quiet.
((("something" "is" "kind" "+")) -> ("something" "is" "quiet" "-"))
Harry is white.
True
1
proof
[(triple16)]
("Harry" "is" "white" "+")
triple16
Harry is not red.
False
1
inv-proof
[(triple14)]
("Harry" "is" "red" "-")
triple14
Harry is round.
True
2
proof
[(((triple14) -> rule5))]
("Harry" "is" "round" "+")
((triple14) -> (rule5 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Erin is quiet.
False
2
inv-proof
[(((triple7) -> rule8))]
("Erin" "is" "quiet" "+")
((triple7) -> (rule8 % int1))
Erin is not quiet.
("Erin" "is" "quiet" "-")
int1
Erin is round.
True
4
proof
[(((((triple7) -> rule6) triple7) -> rule3))]
("Erin" "is" "round" "+")
((((triple7) -> (rule6 % int2)) triple7) -> (rule3 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is not round.
False
4
inv-proof
[(((((triple7) -> rule6) triple7) -> rule3))]
("Erin" "is" "round" "-")
((((triple7) -> (rule6 % int2)) triple7) -> (rule3 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is red.
True
6
proof
[(((((((triple7) -> rule6) triple7) -> rule3) triple6) -> rule4))]
("Erin" "is" "red" "+")
((((((triple7) -> (rule6 % int3)) triple7) -> (rule3 % int2)) triple6) -> (rule4 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is white.
("Erin" "is" "white" "+")
int3
Erin is not red.
False
6
inv-proof
[(((((((triple7) -> rule6) triple7) -> rule3) triple6) -> rule4))]
("Erin" "is" "red" "-")
((((((triple7) -> (rule6 % int3)) triple7) -> (rule3 % int2)) triple6) -> (rule4 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is white.
("Erin" "is" "white" "+")
int3
Fiona is not red.
Unknown
inv-rconc
[@1: Fiona is red.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Fiona" "is" "red" "-")
Fiona is furry.
Unknown
random
[@0: Fiona is furry.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "furry" "+")
Harry is not kind.
Unknown
inv-random
[@0: Harry is kind.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "kind" "-")
Anne is furry.
Unknown
random
[@0: Anne is furry.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "furry" "+")
@0: Anne is kind.[(triple1)] Anne is not red.[(triple2)] Anne is not smart.[(triple4)] Anne is round.[(triple3 OR ((triple5 triple1) -> rule3))] Anne is white.[(triple5)] Erin is furry.[(triple6)] Erin is kind.[(triple7)] Erin is not smart.[(triple8)] Fiona is kind.[(triple9)] Fiona is round.[(triple10 OR ((triple12 triple9) -> rule3) OR ((triple9 triple11) -> rule7) OR ((((triple11 triple9) -> rule1) triple9) -> rule3))] Fiona is smart.[(triple11)] Fiona is white.[(triple12 OR ((triple11 triple9) -> rule1))] Harry is furry.[(triple13)] Harry is red.[(triple14)] Harry is smart.[(triple15)] Harry is white.[(triple16)] @1: Anne is not quiet.[(((triple1) -> rule8))] Erin is not quiet.[(((triple7) -> rule8))] Erin is white.[(((triple7) -> rule6))] Fiona is not quiet.[(((triple9) -> rule8))] Harry is round.[(((triple14) -> rule5))] @2: Erin is round.[(((((triple7) -> rule6) triple7) -> rule3))] @3: Erin is red.[(((((((triple7) -> rule6) triple7) -> rule3) triple6) -> rule4))]
Anne is kind.
("Anne" "is" "kind" "+")
triple1
Anne is not red.
("Anne" "is" "red" "-")
triple2
Anne is not smart.
("Anne" "is" "smart" "-")
triple4
Anne is round.
("Anne" "is" "round" "+")
triple3
((triple5 triple1) -> (rule3 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
triple5
Erin is furry.
("Erin" "is" "furry" "+")
triple6
Erin is kind.
("Erin" "is" "kind" "+")
triple7
Erin is not smart.
("Erin" "is" "smart" "-")
triple8
Fiona is kind.
("Fiona" "is" "kind" "+")
triple9
Fiona is round.
("Fiona" "is" "round" "+")
triple10
((triple12 triple9) -> (rule3 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
((triple9 triple11) -> (rule7 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
((((triple11 triple9) -> (rule1 % int2)) triple9) -> (rule3 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
int2
Fiona is smart.
("Fiona" "is" "smart" "+")
triple11
Fiona is white.
("Fiona" "is" "white" "+")
triple12
((triple11 triple9) -> (rule1 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
triple13
Harry is red.
("Harry" "is" "red" "+")
triple14
Harry is smart.
("Harry" "is" "smart" "+")
triple15
Harry is white.
("Harry" "is" "white" "+")
triple16
Anne is not quiet.
("Anne" "is" "quiet" "-")
((triple1) -> (rule8 % int1))
Anne is not quiet.
("Anne" "is" "quiet" "-")
int1
Erin is not quiet.
("Erin" "is" "quiet" "-")
((triple7) -> (rule8 % int1))
Erin is not quiet.
("Erin" "is" "quiet" "-")
int1
Erin is white.
("Erin" "is" "white" "+")
((triple7) -> (rule6 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Fiona is not quiet.
("Fiona" "is" "quiet" "-")
((triple9) -> (rule8 % int1))
Fiona is not quiet.
("Fiona" "is" "quiet" "-")
int1
Harry is round.
("Harry" "is" "round" "+")
((triple14) -> (rule5 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
((((triple7) -> (rule6 % int2)) triple7) -> (rule3 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
((((((triple7) -> (rule6 % int3)) triple7) -> (rule3 % int2)) triple6) -> (rule4 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is white.
("Erin" "is" "white" "+")
int3