Anne is furry. Anne is kind. Anne is rough. Anne is round. Anne is white. Bob is furry. Bob is kind. Bob is quiet. Bob is red. Bob is rough. Bob is round. Erin is furry. Erin is rough. Erin is round. Erin is white. If someone is white and round then they are kind. Furry people are red. Rough people are red. If someone is furry then they are round. All white people are quiet. All rough, kind people are white. All round people are furry. If someone is red and kind then they are round.
Anne is furry.
("Anne" "is" "furry" "+")
Anne is kind.
("Anne" "is" "kind" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Anne is round.
("Anne" "is" "round" "+")
Anne is white.
("Anne" "is" "white" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Bob is round.
("Bob" "is" "round" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Erin is round.
("Erin" "is" "round" "+")
Erin is white.
("Erin" "is" "white" "+")
If someone is white and round then they are kind.
((("someone" "is" "white" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "kind" "+"))
Furry people are red.
((("someone" "is" "furry" "+")) -> ("someone" "is" "red" "+"))
Rough people are red.
((("someone" "is" "rough" "+")) -> ("someone" "is" "red" "+"))
If someone is furry then they are round.
((("someone" "is" "furry" "+")) -> ("someone" "is" "round" "+"))
All white people are quiet.
((("someone" "is" "white" "+")) -> ("someone" "is" "quiet" "+"))
All rough, kind people are white.
((("someone" "is" "rough" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "white" "+"))
All round people are furry.
((("someone" "is" "round" "+")) -> ("someone" "is" "furry" "+"))
If someone is red and kind then they are round.
((("someone" "is" "red" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "round" "+"))
Anne is rough.
True
1
proof
[(triple3)]
("Anne" "is" "rough" "+")
triple3
Anne is not white.
False
1
inv-proof
[(triple5 OR ((triple3 triple2) -> rule6))]
("Anne" "is" "white" "-")
triple5
((triple3 triple2) -> (rule6 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
@0: Anne is furry.[(triple1 OR ((triple4) -> rule7) OR ((((((triple3) -> rule3) triple2) -> rule8)) -> rule7))] Anne is kind.[(triple2 OR ((triple5 triple4) -> rule1) OR ((triple5 ((triple1) -> rule4)) -> rule1))] Anne is rough.[(triple3)] Anne is round.[(triple4 OR ((triple1) -> rule4) OR ((((triple1) -> rule2) triple2) -> rule8) OR ((((triple3) -> rule3) triple2) -> rule8))] Anne is white.[(triple5 OR ((triple3 triple2) -> rule6))] Bob is furry.[(triple6 OR ((triple11) -> rule7) OR ((((triple9 triple7) -> rule8)) -> rule7) OR ((((((triple10) -> rule3) triple7) -> rule8)) -> rule7))] Bob is kind.[(triple7)] Bob is quiet.[(triple8 OR ((((triple10 triple7) -> rule6)) -> rule5))] Bob is red.[(triple9 OR ((triple10) -> rule3) OR ((triple6) -> rule2) OR ((((triple11) -> rule7)) -> rule2))] Bob is rough.[(triple10)] Bob is round.[(triple11 OR ((triple6) -> rule4) OR ((triple9 triple7) -> rule8) OR ((((triple10) -> rule3) triple7) -> rule8) OR ((((triple6) -> rule2) triple7) -> rule8))] Erin is furry.[(triple12 OR ((triple14) -> rule7))] Erin is rough.[(triple13)] Erin is round.[(triple14 OR ((triple12) -> rule4))] Erin is white.[(triple15)] @1: Anne is quiet.[(((triple5) -> rule5) OR ((((triple3 triple2) -> rule6)) -> rule5))] Anne is red.[(((triple1) -> rule2) OR ((triple3) -> rule3) OR ((((triple4) -> rule7)) -> rule2))] Bob is white.[(((triple10 triple7) -> rule6))] Erin is kind.[(((triple15 triple14) -> rule1) OR ((triple15 ((triple12) -> rule4)) -> rule1))] Erin is quiet.[(((triple15) -> rule5))] Erin is red.[(((triple12) -> rule2) OR ((triple13) -> rule3) OR ((((triple14) -> rule7)) -> rule2))]
Anne is furry.
("Anne" "is" "furry" "+")
triple1
((triple4) -> (rule7 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
((((((triple3) -> (rule3 % int3)) triple2) -> (rule8 % int2))) -> (rule7 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
int3
Anne is kind.
("Anne" "is" "kind" "+")
triple2
((triple5 triple4) -> (rule1 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
((triple5 ((triple1) -> (rule4 % int2))) -> (rule1 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is rough.
("Anne" "is" "rough" "+")
triple3
Anne is round.
("Anne" "is" "round" "+")
triple4
((triple1) -> (rule4 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
((((triple1) -> (rule2 % int2)) triple2) -> (rule8 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
((((triple3) -> (rule3 % int2)) triple2) -> (rule8 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
triple5
((triple3 triple2) -> (rule6 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
triple6
((triple11) -> (rule7 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
((((triple9 triple7) -> (rule8 % int2))) -> (rule7 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
((((((triple10) -> (rule3 % int3)) triple7) -> (rule8 % int2))) -> (rule7 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
int3
Bob is kind.
("Bob" "is" "kind" "+")
triple7
Bob is quiet.
("Bob" "is" "quiet" "+")
triple8
((((triple10 triple7) -> (rule6 % int2))) -> (rule5 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
triple9
((triple10) -> (rule3 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
((triple6) -> (rule2 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
((((triple11) -> (rule7 % int2))) -> (rule2 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
triple10
Bob is round.
("Bob" "is" "round" "+")
triple11
((triple6) -> (rule4 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
((triple9 triple7) -> (rule8 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
((((triple10) -> (rule3 % int2)) triple7) -> (rule8 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
((((triple6) -> (rule2 % int2)) triple7) -> (rule8 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Erin is furry.
("Erin" "is" "furry" "+")
triple12
((triple14) -> (rule7 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
triple13
Erin is round.
("Erin" "is" "round" "+")
triple14
((triple12) -> (rule4 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
triple15
Anne is quiet.
("Anne" "is" "quiet" "+")
((triple5) -> (rule5 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
((((triple3 triple2) -> (rule6 % int2))) -> (rule5 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
((triple1) -> (rule2 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
((triple3) -> (rule3 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
((((triple4) -> (rule7 % int2))) -> (rule2 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
((triple10 triple7) -> (rule6 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
((triple15 triple14) -> (rule1 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
((triple15 ((triple12) -> (rule4 % int2))) -> (rule1 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
((triple15) -> (rule5 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
((triple12) -> (rule2 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
((triple13) -> (rule3 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
((((triple14) -> (rule7 % int2))) -> (rule2 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2