Anne is blue. Anne is furry. Anne is kind. Anne is quiet. Anne is rough. Anne is white. Anne is young. If Anne is blue then Anne is rough. All quiet, furry people are kind. If someone is rough then they are furry.
Anne is blue.
("Anne" "is" "blue" "+")
Anne is furry.
("Anne" "is" "furry" "+")
Anne is kind.
("Anne" "is" "kind" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Anne is white.
("Anne" "is" "white" "+")
Anne is young.
("Anne" "is" "young" "+")
If Anne is blue then Anne is rough.
((("Anne" "is" "blue" "+")) -> ("Anne" "is" "rough" "+"))
All quiet, furry people are kind.
((("someone" "is" "quiet" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "kind" "+"))
If someone is rough then they are furry.
((("someone" "is" "rough" "+")) -> ("someone" "is" "furry" "+"))
Anne is furry.
True
1
proof
[(triple2 OR ((triple5) -> rule3) OR ((((triple1) -> rule1)) -> rule3))]
("Anne" "is" "furry" "+")
triple2
((triple5) -> (rule3 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
((((triple1) -> (rule1 % int2))) -> (rule3 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is not blue.
False
1
inv-proof
[(triple1)]
("Anne" "is" "blue" "-")
triple1
@0: Anne is blue.[(triple1)] Anne is furry.[(triple2 OR ((triple5) -> rule3) OR ((((triple1) -> rule1)) -> rule3))] Anne is kind.[(triple3 OR ((triple4 triple2) -> rule2) OR ((triple4 ((triple5) -> rule3)) -> rule2) OR ((triple4 ((((triple1) -> rule1)) -> rule3)) -> rule2))] Anne is quiet.[(triple4)] Anne is rough.[(triple5 OR ((triple1) -> rule1))] Anne is white.[(triple6)] Anne is young.[(triple7)]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Anne is furry.
("Anne" "is" "furry" "+")
triple2
((triple5) -> (rule3 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
((((triple1) -> (rule1 % int2))) -> (rule3 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is kind.
("Anne" "is" "kind" "+")
triple3
((triple4 triple2) -> (rule2 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
((triple4 ((triple5) -> (rule3 % int2))) -> (rule2 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
((triple4 ((((triple1) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is rough.
("Anne" "is" "rough" "+")
int3
Anne is quiet.
("Anne" "is" "quiet" "+")
triple4
Anne is rough.
("Anne" "is" "rough" "+")
triple5
((triple1) -> (rule1 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
triple6
Anne is young.
("Anne" "is" "young" "+")
triple7