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