Anne is blue. Anne is green. Anne is not kind. Anne is not red. Anne is smart. Anne is not white. Anne is young. If someone is smart then they are not red. Red, blue people are not green. If Anne is blue and Anne is green then Anne is not kind. If Anne is red then Anne is blue. If Anne is kind then Anne is not young. If someone is kind and not red then they are young. If someone is red and not green then they are kind. If someone is young and red then they are kind.
Anne is blue.
("Anne" "is" "blue" "+")
Anne is green.
("Anne" "is" "green" "+")
Anne is not kind.
("Anne" "is" "kind" "-")
Anne is not red.
("Anne" "is" "red" "-")
Anne is smart.
("Anne" "is" "smart" "+")
Anne is not white.
("Anne" "is" "white" "-")
Anne is young.
("Anne" "is" "young" "+")
If someone is smart then they are not red.
((("someone" "is" "smart" "+")) -> ("someone" "is" "red" "-"))
Red, blue people are not green.
((("someone" "is" "red" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "green" "-"))
If Anne is blue and Anne is green then Anne is not kind.
((("Anne" "is" "blue" "+") ("Anne" "is" "green" "+")) -> ("Anne" "is" "kind" "-"))
If Anne is red then Anne is blue.
((("Anne" "is" "red" "+")) -> ("Anne" "is" "blue" "+"))
If Anne is kind then Anne is not young.
((("Anne" "is" "kind" "+")) -> ("Anne" "is" "young" "-"))
If someone is kind and not red then they are young.
((("someone" "is" "kind" "+") ("someone" "is" "red" "~")) -> ("someone" "is" "young" "+"))
If someone is red and not green then they are kind.
((("someone" "is" "red" "+") ("someone" "is" "green" "~")) -> ("someone" "is" "kind" "+"))
If someone is young and red then they are kind.
((("someone" "is" "young" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "kind" "+"))
Anne is young.
True
1
proof
[(triple7)]
("Anne" "is" "young" "+")
triple7
Anne is kind.
False
1
inv-proof
[(triple3 OR ((triple1 triple2) -> rule3))]
("Anne" "is" "kind" "+")
triple3
((triple1 triple2) -> (rule3 % int1))
Anne is not kind.
("Anne" "is" "kind" "-")
int1
@0: Anne is blue.[(triple1)] Anne is green.[(triple2)] Anne is not kind.[(triple3 OR ((triple1 triple2) -> rule3))] Anne is not red.[(triple4 OR ((triple5) -> rule1))] Anne is not white.[(triple6)] Anne is smart.[(triple5)] Anne is young.[(triple7)]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Anne is green.
("Anne" "is" "green" "+")
triple2
Anne is not kind.
("Anne" "is" "kind" "-")
triple3
((triple1 triple2) -> (rule3 % int1))
Anne is not kind.
("Anne" "is" "kind" "-")
int1
Anne is not red.
("Anne" "is" "red" "-")
triple4
((triple5) -> (rule1 % int1))
Anne is not red.
("Anne" "is" "red" "-")
int1
Anne is not white.
("Anne" "is" "white" "-")
triple6
Anne is smart.
("Anne" "is" "smart" "+")
triple5
Anne is young.
("Anne" "is" "young" "+")
triple7