Anne is blue. Anne is furry. Anne is young. If someone is young and blue then they are white. All young, furry people are white. If someone is white then they are blue. If someone is cold and not young then they are blue. If Anne is furry then Anne is cold. If someone is young and not cold then they are rough. If someone is young and not white then they are rough. White, blue people are not rough.
Anne is blue.
("Anne" "is" "blue" "+")
Anne is furry.
("Anne" "is" "furry" "+")
Anne is young.
("Anne" "is" "young" "+")
If someone is young and blue then they are white.
((("someone" "is" "young" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "white" "+"))
All young, furry people are white.
((("someone" "is" "young" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "white" "+"))
If someone is white then they are blue.
((("someone" "is" "white" "+")) -> ("someone" "is" "blue" "+"))
If someone is cold and not young then they are blue.
((("someone" "is" "cold" "+") ("someone" "is" "young" "~")) -> ("someone" "is" "blue" "+"))
If Anne is furry then Anne is cold.
((("Anne" "is" "furry" "+")) -> ("Anne" "is" "cold" "+"))
If someone is young and not cold then they are rough.
((("someone" "is" "young" "+") ("someone" "is" "cold" "~")) -> ("someone" "is" "rough" "+"))
If someone is young and not white then they are rough.
((("someone" "is" "young" "+") ("someone" "is" "white" "~")) -> ("someone" "is" "rough" "+"))
White, blue people are not rough.
((("someone" "is" "white" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "rough" "-"))
Anne is young.
True
1
proof
[(triple3)]
("Anne" "is" "young" "+")
triple3
Anne is not blue.
False
1
inv-proof
[(triple1 OR ((((triple3 triple2) -> rule2)) -> rule3))]
("Anne" "is" "blue" "-")
triple1
((((triple3 triple2) -> (rule2 % int2))) -> (rule3 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
@0: Anne is blue.[(triple1 OR ((((triple3 triple2) -> rule2)) -> rule3))] Anne is furry.[(triple2)] Anne is young.[(triple3)] @1: Anne is cold.[(((triple2) -> rule5))] Anne is white.[(((triple3 triple1) -> rule1) OR ((triple3 triple2) -> rule2))] @2: Anne is not rough.[(((((triple3 triple1) -> rule1) triple1) -> rule8) OR ((((triple3 triple2) -> rule2) triple1) -> rule8) OR ((((triple3 triple1) -> rule1) ((((triple3 triple2) -> rule2)) -> rule3)) -> rule8) OR ((((triple3 triple2) -> rule2) ((((triple3 triple2) -> rule2)) -> rule3)) -> rule8))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
((((triple3 triple2) -> (rule2 % int2))) -> (rule3 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
triple2
Anne is young.
("Anne" "is" "young" "+")
triple3
Anne is cold.
("Anne" "is" "cold" "+")
((triple2) -> (rule5 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
((triple3 triple1) -> (rule1 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
((triple3 triple2) -> (rule2 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is not rough.
("Anne" "is" "rough" "-")
((((triple3 triple1) -> (rule1 % int2)) triple1) -> (rule8 % int1))
Anne is not rough.
("Anne" "is" "rough" "-")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
((((triple3 triple2) -> (rule2 % int2)) triple1) -> (rule8 % int1))
Anne is not rough.
("Anne" "is" "rough" "-")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
((((triple3 triple1) -> (rule1 % int3)) ((((triple3 triple2) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule8 % int1))
Anne is not rough.
("Anne" "is" "rough" "-")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
int3
((((triple3 triple2) -> (rule2 % int3)) ((((triple3 triple2) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule8 % int1))
Anne is not rough.
("Anne" "is" "rough" "-")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
int3