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