Anne is furry. Anne is rough. Anne is not smart. Anne is white. Erin is red. Gary is nice. Harry is kind. Harry is not nice. Harry is rough. Harry is not smart. If Erin is rough and Erin is not smart then Erin is furry. If Harry is kind then Harry is rough. If someone is rough and not smart then they are furry. Rough, red people are furry. All furry people are white. If someone is smart and not nice then they are red.
Anne is furry.
("Anne" "is" "furry" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Anne is not smart.
("Anne" "is" "smart" "-")
Anne is white.
("Anne" "is" "white" "+")
Erin is red.
("Erin" "is" "red" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is not nice.
("Harry" "is" "nice" "-")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is not smart.
("Harry" "is" "smart" "-")
If Erin is rough and Erin is not smart then Erin is furry.
((("Erin" "is" "rough" "+") ("Erin" "is" "smart" "~")) -> ("Erin" "is" "furry" "+"))
If Harry is kind then Harry is rough.
((("Harry" "is" "kind" "+")) -> ("Harry" "is" "rough" "+"))
If someone is rough and not smart then they are furry.
((("someone" "is" "rough" "+") ("someone" "is" "smart" "~")) -> ("someone" "is" "furry" "+"))
Rough, red people are furry.
((("someone" "is" "rough" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "furry" "+"))
All furry people are white.
((("someone" "is" "furry" "+")) -> ("someone" "is" "white" "+"))
If someone is smart and not nice then they are red.
((("someone" "is" "smart" "+") ("someone" "is" "nice" "~")) -> ("someone" "is" "red" "+"))
Anne is white.
True
1
proof
[(triple4 OR ((triple1) -> rule5) OR ((((triple2 triple3) -> rule3)) -> rule5))]
("Anne" "is" "white" "+")
triple4
((triple1) -> (rule5 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
((((triple2 triple3) -> (rule3 % int2))) -> (rule5 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is not rough.
False
1
inv-proof
[(triple2)]
("Anne" "is" "rough" "-")
triple2
Harry is furry.
True
3
proof
[(((triple9 triple10) -> rule3) OR ((((triple7) -> rule2) triple10) -> rule3))]
("Harry" "is" "furry" "+")
((triple9 triple10) -> (rule3 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
((((triple7) -> (rule2 % int2)) triple10) -> (rule3 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is not furry.
False
3
inv-proof
[(((triple9 triple10) -> rule3) OR ((((triple7) -> rule2) triple10) -> rule3))]
("Harry" "is" "furry" "-")
((triple9 triple10) -> (rule3 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
((((triple7) -> (rule2 % int2)) triple10) -> (rule3 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is white.
True
4
proof
[(((((triple9 triple10) -> rule3)) -> rule5) OR ((((((triple7) -> rule2) triple10) -> rule3)) -> rule5))]
("Harry" "is" "white" "+")
((((triple9 triple10) -> (rule3 % int2))) -> (rule5 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
((((((triple7) -> (rule2 % int3)) triple10) -> (rule3 % int2))) -> (rule5 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3
Harry is not white.
False
4
inv-proof
[(((((triple9 triple10) -> rule3)) -> rule5) OR ((((((triple7) -> rule2) triple10) -> rule3)) -> rule5))]
("Harry" "is" "white" "-")
((((triple9 triple10) -> (rule3 % int2))) -> (rule5 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
((((((triple7) -> (rule2 % int3)) triple10) -> (rule3 % int2))) -> (rule5 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3
Erin is not white.
Unknown
inv-rconc
[@2: Erin is white.[CWA. Example of deepest failure = (rule5 <- rule1 <- FAIL)]]
("Erin" "is" "white" "-")
Gary is red.
Unknown
rconc
[@1: Gary is red.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Gary" "is" "red" "+")
Gary is not furry.
Unknown
inv-rconc
[@1: Gary is furry.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Gary" "is" "furry" "-")
Gary is rough.
Unknown
random
[@0: Gary is rough.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "rough" "+")
Erin is not rough.
Unknown
inv-random
[@0: Erin is rough.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "rough" "-")
Anne is kind.
Unknown
random
[@0: Anne is kind.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "kind" "+")
@0: Anne is furry.[(triple1 OR ((triple2 triple3) -> rule3))] Anne is not smart.[(triple3)] Anne is rough.[(triple2)] Anne is white.[(triple4 OR ((triple1) -> rule5) OR ((((triple2 triple3) -> rule3)) -> rule5))] Erin is red.[(triple5)] Gary is nice.[(triple6)] Harry is kind.[(triple7)] Harry is not nice.[(triple8)] Harry is not smart.[(triple10)] Harry is rough.[(triple9 OR ((triple7) -> rule2))] @1: Harry is furry.[(((triple9 triple10) -> rule3) OR ((((triple7) -> rule2) triple10) -> rule3))] @2: Harry is white.[(((((triple9 triple10) -> rule3)) -> rule5) OR ((((((triple7) -> rule2) triple10) -> rule3)) -> rule5))]
Anne is furry.
("Anne" "is" "furry" "+")
triple1
((triple2 triple3) -> (rule3 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is not smart.
("Anne" "is" "smart" "-")
triple3
Anne is rough.
("Anne" "is" "rough" "+")
triple2
Anne is white.
("Anne" "is" "white" "+")
triple4
((triple1) -> (rule5 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
((((triple2 triple3) -> (rule3 % int2))) -> (rule5 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
triple5
Gary is nice.
("Gary" "is" "nice" "+")
triple6
Harry is kind.
("Harry" "is" "kind" "+")
triple7
Harry is not nice.
("Harry" "is" "nice" "-")
triple8
Harry is not smart.
("Harry" "is" "smart" "-")
triple10
Harry is rough.
("Harry" "is" "rough" "+")
triple9
((triple7) -> (rule2 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
((triple9 triple10) -> (rule3 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
((((triple7) -> (rule2 % int2)) triple10) -> (rule3 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
((((triple9 triple10) -> (rule3 % int2))) -> (rule5 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
((((((triple7) -> (rule2 % int3)) triple10) -> (rule3 % int2))) -> (rule5 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3