Anne is big. Anne is cold. Anne is furry. Anne is kind. Anne is quiet. Anne is red. Anne is rough. Erin is big. Erin is cold. Erin is furry. Erin is kind. Erin is quiet. Erin is red. Erin is rough. All red people are quiet. All big, furry people are cold. Quiet people are kind. Red people are cold. Cold people are furry. Kind, quiet people are red. All cold, big people are kind. Big, rough people are kind.
Anne is big.
("Anne" "is" "big" "+")
Anne is cold.
("Anne" "is" "cold" "+")
Anne is furry.
("Anne" "is" "furry" "+")
Anne is kind.
("Anne" "is" "kind" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is red.
("Anne" "is" "red" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is red.
("Erin" "is" "red" "+")
Erin is rough.
("Erin" "is" "rough" "+")
All red people are quiet.
((("someone" "is" "red" "+")) -> ("someone" "is" "quiet" "+"))
All big, furry people are cold.
((("someone" "is" "big" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "cold" "+"))
Quiet people are kind.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "kind" "+"))
Red people are cold.
((("someone" "is" "red" "+")) -> ("someone" "is" "cold" "+"))
Cold people are furry.
((("someone" "is" "cold" "+")) -> ("someone" "is" "furry" "+"))
Kind, quiet people are red.
((("someone" "is" "kind" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "red" "+"))
All cold, big people are kind.
((("someone" "is" "cold" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "kind" "+"))
Big, rough people are kind.
((("someone" "is" "big" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "kind" "+"))
Anne is big.
True
1
proof
[(triple1)]
("Anne" "is" "big" "+")
triple1
Erin is not quiet.
False
1
inv-proof
[(triple12 OR ((triple13) -> rule1))]
("Erin" "is" "quiet" "-")
triple12
((triple13) -> (rule1 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
@0: Anne is big.[(triple1)] Anne is cold.[(triple2 OR ((triple6) -> rule4) OR ((triple1 triple3) -> rule2) OR ((((triple4 triple5) -> rule6)) -> rule4) OR ((((((triple5) -> rule3) triple5) -> rule6)) -> rule4) OR ((((((triple1 triple7) -> rule8) triple5) -> rule6)) -> rule4))] Anne is furry.[(triple3 OR ((triple2) -> rule5) OR ((((triple6) -> rule4)) -> rule5) OR ((((((triple4 triple5) -> rule6)) -> rule4)) -> rule5) OR ((((((((triple5) -> rule3) triple5) -> rule6)) -> rule4)) -> rule5) OR ((((((((triple1 triple7) -> rule8) triple5) -> rule6)) -> rule4)) -> rule5))] Anne is kind.[(triple4 OR ((triple5) -> rule3) OR ((triple1 triple7) -> rule8) OR ((triple2 triple1) -> rule7) OR ((((triple6) -> rule1)) -> rule3) OR ((((triple6) -> rule4) triple1) -> rule7) OR ((((triple1 triple3) -> rule2) triple1) -> rule7))] Anne is quiet.[(triple5 OR ((triple6) -> rule1))] Anne is red.[(triple6 OR ((triple4 triple5) -> rule6) OR ((((triple5) -> rule3) triple5) -> rule6) OR ((((triple1 triple7) -> rule8) triple5) -> rule6) OR ((((triple2 triple1) -> rule7) triple5) -> rule6) OR ((((((triple1 triple3) -> rule2) triple1) -> rule7) triple5) -> rule6))] Anne is rough.[(triple7)] Erin is big.[(triple8)] Erin is cold.[(triple9 OR ((triple13) -> rule4) OR ((triple8 triple10) -> rule2) OR ((((triple11 triple12) -> rule6)) -> rule4) OR ((((((triple12) -> rule3) triple12) -> rule6)) -> rule4) OR ((((((triple8 triple14) -> rule8) triple12) -> rule6)) -> rule4))] Erin is furry.[(triple10 OR ((triple9) -> rule5) OR ((((triple13) -> rule4)) -> rule5) OR ((((((triple11 triple12) -> rule6)) -> rule4)) -> rule5) OR ((((((((triple12) -> rule3) triple12) -> rule6)) -> rule4)) -> rule5) OR ((((((((triple8 triple14) -> rule8) triple12) -> rule6)) -> rule4)) -> rule5))] Erin is kind.[(triple11 OR ((triple12) -> rule3) OR ((triple8 triple14) -> rule8) OR ((triple9 triple8) -> rule7) OR ((((triple13) -> rule1)) -> rule3) OR ((((triple13) -> rule4) triple8) -> rule7) OR ((((triple8 triple10) -> rule2) triple8) -> rule7))] Erin is quiet.[(triple12 OR ((triple13) -> rule1))] Erin is red.[(triple13 OR ((triple11 triple12) -> rule6) OR ((((triple12) -> rule3) triple12) -> rule6) OR ((((triple8 triple14) -> rule8) triple12) -> rule6) OR ((((triple9 triple8) -> rule7) triple12) -> rule6) OR ((((((triple8 triple10) -> rule2) triple8) -> rule7) triple12) -> rule6))] Erin is rough.[(triple14)]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is cold.
("Anne" "is" "cold" "+")
triple2
((triple6) -> (rule4 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
((triple1 triple3) -> (rule2 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
((((triple4 triple5) -> (rule6 % int2))) -> (rule4 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
((((((triple5) -> (rule3 % int3)) triple5) -> (rule6 % int2))) -> (rule4 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is kind.
("Anne" "is" "kind" "+")
int3
((((((triple1 triple7) -> (rule8 % int3)) triple5) -> (rule6 % int2))) -> (rule4 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is kind.
("Anne" "is" "kind" "+")
int3
Anne is furry.
("Anne" "is" "furry" "+")
triple3
((triple2) -> (rule5 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
((((triple6) -> (rule4 % int2))) -> (rule5 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
((((((triple4 triple5) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
int3
((((((((triple5) -> (rule3 % int4)) triple5) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
int3
Anne is kind.
("Anne" "is" "kind" "+")
int4
((((((((triple1 triple7) -> (rule8 % int4)) triple5) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
int3
Anne is kind.
("Anne" "is" "kind" "+")
int4
Anne is kind.
("Anne" "is" "kind" "+")
triple4
((triple5) -> (rule3 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
((triple1 triple7) -> (rule8 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
((triple2 triple1) -> (rule7 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
((((triple6) -> (rule1 % int2))) -> (rule3 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
((((triple6) -> (rule4 % int2)) triple1) -> (rule7 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
((((triple1 triple3) -> (rule2 % int2)) triple1) -> (rule7 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
triple5
((triple6) -> (rule1 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
triple6
((triple4 triple5) -> (rule6 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
((((triple5) -> (rule3 % int2)) triple5) -> (rule6 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
((((triple1 triple7) -> (rule8 % int2)) triple5) -> (rule6 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
((((triple2 triple1) -> (rule7 % int2)) triple5) -> (rule6 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
((((((triple1 triple3) -> (rule2 % int3)) triple1) -> (rule7 % int2)) triple5) -> (rule6 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3
Anne is rough.
("Anne" "is" "rough" "+")
triple7
Erin is big.
("Erin" "is" "big" "+")
triple8
Erin is cold.
("Erin" "is" "cold" "+")
triple9
((triple13) -> (rule4 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
((triple8 triple10) -> (rule2 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
((((triple11 triple12) -> (rule6 % int2))) -> (rule4 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
((((((triple12) -> (rule3 % int3)) triple12) -> (rule6 % int2))) -> (rule4 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
((((((triple8 triple14) -> (rule8 % int3)) triple12) -> (rule6 % int2))) -> (rule4 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
Erin is furry.
("Erin" "is" "furry" "+")
triple10
((triple9) -> (rule5 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
((((triple13) -> (rule4 % int2))) -> (rule5 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
((((((triple11 triple12) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
int3
((((((((triple12) -> (rule3 % int4)) triple12) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
int3
Erin is kind.
("Erin" "is" "kind" "+")
int4
((((((((triple8 triple14) -> (rule8 % int4)) triple12) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
int3
Erin is kind.
("Erin" "is" "kind" "+")
int4
Erin is kind.
("Erin" "is" "kind" "+")
triple11
((triple12) -> (rule3 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
((triple8 triple14) -> (rule8 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
((triple9 triple8) -> (rule7 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
((((triple13) -> (rule1 % int2))) -> (rule3 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
((((triple13) -> (rule4 % int2)) triple8) -> (rule7 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
((((triple8 triple10) -> (rule2 % int2)) triple8) -> (rule7 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
triple12
((triple13) -> (rule1 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
triple13
((triple11 triple12) -> (rule6 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
((((triple12) -> (rule3 % int2)) triple12) -> (rule6 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
((((triple8 triple14) -> (rule8 % int2)) triple12) -> (rule6 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
((((triple9 triple8) -> (rule7 % int2)) triple12) -> (rule6 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
((((((triple8 triple10) -> (rule2 % int3)) triple8) -> (rule7 % int2)) triple12) -> (rule6 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
int3
Erin is rough.
("Erin" "is" "rough" "+")
triple14